Theorem: FactorizationCentralBinom.leOne (FromTheBook/Ch02/Bertrand/CentralBinom.lean)

State before:
n p : ℕ
hp : Nat.Prime p
⊢ 2 * n < p ^ 2 → ↑(Nat.factorization (Nat.centralBinom n)) p ≤ 1
Tactic:
intro hnp
State after:
n p : ℕ
hp : Nat.Prime p
hnp : 2 * n < p ^ 2
⊢ ↑(Nat.factorization (Nat.centralBinom n)) p ≤ 1

State before:
n p : ℕ
hp : Nat.Prime p
hnp : 2 * n < p ^ 2
⊢ ↑(Nat.factorization (Nat.centralBinom n)) p ≤ 1
Tactic:
apply le_trans (Nat.factorization_choose_le_log)
State after:
n p : ℕ
hp : Nat.Prime p
hnp : 2 * n < p ^ 2
⊢ Nat.log p (2 * n) ≤ 1

State before:
n p : ℕ
hp : Nat.Prime p
hnp : 2 * n < p ^ 2
⊢ Nat.log p (2 * n) ≤ 1
Tactic:
have hnp := Nat.le_pred_of_lt hnp
State after:
n p : ℕ
hp : Nat.Prime p
hnp✝ : 2 * n < p ^ 2
hnp : 2 * n ≤ p ^ 2 - 1
⊢ Nat.log p (2 * n) ≤ 1

State before:
n p : ℕ
hp : Nat.Prime p
hnp✝ : 2 * n < p ^ 2
hnp : 2 * n ≤ p ^ 2 - 1
⊢ Nat.log p (2 * n) ≤ 1
Tactic:
apply le_trans (Nat.log_mono_right hnp)
State after:
n p : ℕ
hp : Nat.Prime p
hnp✝ : 2 * n < p ^ 2
hnp : 2 * n ≤ p ^ 2 - 1
⊢ Nat.log p (p ^ 2 - 1) ≤ 1

State before:
n p : ℕ
hp : Nat.Prime p
hnp✝ : 2 * n < p ^ 2
hnp : 2 * n ≤ p ^ 2 - 1
⊢ Nat.log p (p ^ 2 - 1) ≤ 1
Tactic:
rw [← Nat.lt_succ_iff]
State after:
n p : ℕ
hp : Nat.Prime p
hnp✝ : 2 * n < p ^ 2
hnp : 2 * n ≤ p ^ 2 - 1
⊢ Nat.log p (p ^ 2 - 1) < Nat.succ 1

State before:
n p : ℕ
hp : Nat.Prime p
hnp✝ : 2 * n < p ^ 2
hnp : 2 * n ≤ p ^ 2 - 1
⊢ Nat.log p (p ^ 2 - 1) < Nat.succ 1
Tactic:
have hp := Nat.Prime.one_lt hp
State after:
n p : ℕ
hp✝ : Nat.Prime p
hnp✝ : 2 * n < p ^ 2
hnp : 2 * n ≤ p ^ 2 - 1
hp : 1 < p
⊢ Nat.log p (p ^ 2 - 1) < Nat.succ 1

State before:
n p : ℕ
hp✝ : Nat.Prime p
hnp✝ : 2 * n < p ^ 2
hnp : 2 * n ≤ p ^ 2 - 1
hp : 1 < p
⊢ Nat.log p (p ^ 2 - 1) < Nat.succ 1
Tactic:
apply Nat.log_lt_of_lt_pow
State after:
case hy
n p : ℕ
hp✝ : Nat.Prime p
hnp✝ : 2 * n < p ^ 2
hnp : 2 * n ≤ p ^ 2 - 1
hp : 1 < p
⊢ p ^ 2 - 1 ≠ 0

case a
n p : ℕ
hp✝ : Nat.Prime p
hnp✝ : 2 * n < p ^ 2
hnp : 2 * n ≤ p ^ 2 - 1
hp : 1 < p
⊢ p ^ 2 - 1 < p ^ Nat.succ 1

State before:
case hy
n p : ℕ
hp✝ : Nat.Prime p
hnp✝ : 2 * n < p ^ 2
hnp : 2 * n ≤ p ^ 2 - 1
hp : 1 < p
⊢ p ^ 2 - 1 ≠ 0

case a
n p : ℕ
hp✝ : Nat.Prime p
hnp✝ : 2 * n < p ^ 2
hnp : 2 * n ≤ p ^ 2 - 1
hp : 1 < p
⊢ p ^ 2 - 1 < p ^ Nat.succ 1
Tactic:
. simp [hp]
State after:
case a
n p : ℕ
hp✝ : Nat.Prime p
hnp✝ : 2 * n < p ^ 2
hnp : 2 * n ≤ p ^ 2 - 1
hp : 1 < p
⊢ p ^ 2 - 1 < p ^ Nat.succ 1

State before:
case a
n p : ℕ
hp✝ : Nat.Prime p
hnp✝ : 2 * n < p ^ 2
hnp : 2 * n ≤ p ^ 2 - 1
hp : 1 < p
⊢ p ^ 2 - 1 < p ^ Nat.succ 1
Tactic:
. apply Nat.pred_lt
  simp [hp]
  linarith
State after:
no goals

State before:
case hy
n p : ℕ
hp✝ : Nat.Prime p
hnp✝ : 2 * n < p ^ 2
hnp : 2 * n ≤ p ^ 2 - 1
hp : 1 < p
⊢ p ^ 2 - 1 ≠ 0
Tactic:
simp [hp]
State after:
no goals

State before:
case a
n p : ℕ
hp✝ : Nat.Prime p
hnp✝ : 2 * n < p ^ 2
hnp : 2 * n ≤ p ^ 2 - 1
hp : 1 < p
⊢ p ^ 2 - 1 < p ^ Nat.succ 1
Tactic:
apply Nat.pred_lt
State after:
case a.a
n p : ℕ
hp✝ : Nat.Prime p
hnp✝ : 2 * n < p ^ 2
hnp : 2 * n ≤ p ^ 2 - 1
hp : 1 < p
⊢ Nat.sub (p ^ 2) 0 ≠ 0

State before:
case a.a
n p : ℕ
hp✝ : Nat.Prime p
hnp✝ : 2 * n < p ^ 2
hnp : 2 * n ≤ p ^ 2 - 1
hp : 1 < p
⊢ Nat.sub (p ^ 2) 0 ≠ 0
Tactic:
simp [hp]
State after:
case a.a
n p : ℕ
hp✝ : Nat.Prime p
hnp✝ : 2 * n < p ^ 2
hnp : 2 * n ≤ p ^ 2 - 1
hp : 1 < p
⊢ ¬p = 0

State before:
case a.a
n p : ℕ
hp✝ : Nat.Prime p
hnp✝ : 2 * n < p ^ 2
hnp : 2 * n ≤ p ^ 2 - 1
hp : 1 < p
⊢ ¬p = 0
Tactic:
linarith
State after:
no goals