Theorem: primeOfPowFactorizationNeOne (FromTheBook/Ch02/Bertrand/CentralBinom.lean)

State before:
x n p : ℕ
⊢ p ^ ↑(Nat.factorization n) x ≠ 1 → Nat.Prime x
Tactic:
intro hx
State after:
x n p : ℕ
hx : p ^ ↑(Nat.factorization n) x ≠ 1
⊢ Nat.Prime x

State before:
x n p : ℕ
hx : p ^ ↑(Nat.factorization n) x ≠ 1
⊢ Nat.Prime x
Tactic:
rw [powNeOneIff'] at hx
State after:
x n p : ℕ
hx : ↑(Nat.factorization n) x ≠ 0 ∧ p ≠ 1
⊢ Nat.Prime x

State before:
x n p : ℕ
hx : ↑(Nat.factorization n) x ≠ 0 ∧ p ≠ 1
⊢ Nat.Prime x
Tactic:
by_contra hp
State after:
x n p : ℕ
hx : ↑(Nat.factorization n) x ≠ 0 ∧ p ≠ 1
hp : ¬Nat.Prime x
⊢ False

State before:
x n p : ℕ
hx : ↑(Nat.factorization n) x ≠ 0 ∧ p ≠ 1
hp : ¬Nat.Prime x
⊢ False
Tactic:
cases hx with | intro h hx =>
apply h
simp
exact Nat.factorization_eq_zero_of_non_prime _ hp
State after:
no goals

State before:
case intro
x n p : ℕ
hp : ¬Nat.Prime x
h : ↑(Nat.factorization n) x ≠ 0
hx : p ≠ 1
⊢ False
Tactic:
apply h
State after:
case intro
x n p : ℕ
hp : ¬Nat.Prime x
h : ↑(Nat.factorization n) x ≠ 0
hx : p ≠ 1
⊢ ↑(Nat.factorization n) x = 0

State before:
case intro
x n p : ℕ
hp : ¬Nat.Prime x
h : ↑(Nat.factorization n) x ≠ 0
hx : p ≠ 1
⊢ ↑(Nat.factorization n) x = 0
Tactic:
exact Nat.factorization_eq_zero_of_non_prime _ hp
State after:
no goals