Theorem: Imo1989P5.not_prime_power_of_two_factors (Compfiles/Imo1989P5.lean)

State before:
n p q : ℕ
hp : p.Prime
hq : q.Prime
hpq : p ≠ q
hpn : p ∣ n
hqn : q ∣ n
⊢ ¬IsPrimePow n
Tactic:
intro hpp
State after:
n p q : ℕ
hp : p.Prime
hq : q.Prime
hpq : p ≠ q
hpn : p ∣ n
hqn : q ∣ n
hpp : IsPrimePow n
⊢ False

State before:
n p q : ℕ
hp : p.Prime
hq : q.Prime
hpq : p ≠ q
hpn : p ∣ n
hqn : q ∣ n
hpp : IsPrimePow n
⊢ False
Tactic:
have h0 : n ≠ 0 := IsPrimePow.ne_zero hpp
State after:
n p q : ℕ
hp : p.Prime
hq : q.Prime
hpq : p ≠ q
hpn : p ∣ n
hqn : q ∣ n
hpp : IsPrimePow n
h0 : n ≠ 0
⊢ False

State before:
n p q : ℕ
hp : p.Prime
hq : q.Prime
hpq : p ≠ q
hpn : p ∣ n
hqn : q ∣ n
hpp : IsPrimePow n
h0 : n ≠ 0
⊢ False
Tactic:
obtain ⟨r, k, hr, hk, hrk⟩ := hpp
State after:
case intro.intro.intro.intro
n p q : ℕ
hp : p.Prime
hq : q.Prime
hpq : p ≠ q
hpn : p ∣ n
hqn : q ∣ n
h0 : n ≠ 0
r k : ℕ
hr : Prime r
hk : 0 < k
hrk : r ^ k = n
⊢ False

State before:
case intro.intro.intro.intro
n p q : ℕ
hp : p.Prime
hq : q.Prime
hpq : p ≠ q
hpn : p ∣ n
hqn : q ∣ n
h0 : n ≠ 0
r k : ℕ
hr : Prime r
hk : 0 < k
hrk : r ^ k = n
⊢ False
Tactic:
rw [← Nat.prime_iff] at hr
State after:
case intro.intro.intro.intro
n p q : ℕ
hp : p.Prime
hq : q.Prime
hpq : p ≠ q
hpn : p ∣ n
hqn : q ∣ n
h0 : n ≠ 0
r k : ℕ
hr : r.Prime
hk : 0 < k
hrk : r ^ k = n
⊢ False

State before:
case intro.intro.intro.intro
n p q : ℕ
hp : p.Prime
hq : q.Prime
hpq : p ≠ q
hpn : p ∣ n
hqn : q ∣ n
h0 : n ≠ 0
r k : ℕ
hr : r.Prime
hk : 0 < k
hrk : r ^ k = n
⊢ False
Tactic:
rw [← hrk] at hqn hpn h0
State after:
case intro.intro.intro.intro
n p q : ℕ
hp : p.Prime
hq : q.Prime
hpq : p ≠ q
r k : ℕ
h0 : r ^ k ≠ 0
hpn : p ∣ r ^ k
hqn : q ∣ r ^ k
hr : r.Prime
hk : 0 < k
hrk : r ^ k = n
⊢ False

State before:
case intro.intro.intro.intro
n p q : ℕ
hp : p.Prime
hq : q.Prime
hpq : p ≠ q
r k : ℕ
h0 : r ^ k ≠ 0
hpn : p ∣ r ^ k
hqn : q ∣ r ^ k
hr : r.Prime
hk : 0 < k
hrk : r ^ k = n
⊢ False
Tactic:
clear hrk
State after:
case intro.intro.intro.intro
n p q : ℕ
hp : p.Prime
hq : q.Prime
hpq : p ≠ q
r k : ℕ
h0 : r ^ k ≠ 0
hpn : p ∣ r ^ k
hqn : q ∣ r ^ k
hr : r.Prime
hk : 0 < k
⊢ False

State before:
case intro.intro.intro.intro
n p q : ℕ
hp : p.Prime
hq : q.Prime
hpq : p ≠ q
r k : ℕ
h0 : r ^ k ≠ 0
hpn : p ∣ r ^ k
hqn : q ∣ r ^ k
hr : r.Prime
hk : 0 < k
⊢ False
Tactic:
have h1 := (Nat.mem_factors h0).mpr ⟨hp, hpn⟩
State after:
case intro.intro.intro.intro
n p q : ℕ
hp : p.Prime
hq : q.Prime
hpq : p ≠ q
r k : ℕ
h0 : r ^ k ≠ 0
hpn : p ∣ r ^ k
hqn : q ∣ r ^ k
hr : r.Prime
hk : 0 < k
h1 : p ∈ (r ^ k).factors
⊢ False

State before:
case intro.intro.intro.intro
n p q : ℕ
hp : p.Prime
hq : q.Prime
hpq : p ≠ q
r k : ℕ
h0 : r ^ k ≠ 0
hpn : p ∣ r ^ k
hqn : q ∣ r ^ k
hr : r.Prime
hk : 0 < k
h1 : p ∈ (r ^ k).factors
⊢ False
Tactic:
rw [Nat.Prime.factors_pow hr] at h1
State after:
case intro.intro.intro.intro
n p q : ℕ
hp : p.Prime
hq : q.Prime
hpq : p ≠ q
r k : ℕ
h0 : r ^ k ≠ 0
hpn : p ∣ r ^ k
hqn : q ∣ r ^ k
hr : r.Prime
hk : 0 < k
h1 : p ∈ List.replicate k r
⊢ False

State before:
case intro.intro.intro.intro
n p q : ℕ
hp : p.Prime
hq : q.Prime
hpq : p ≠ q
r k : ℕ
h0 : r ^ k ≠ 0
hpn : p ∣ r ^ k
hqn : q ∣ r ^ k
hr : r.Prime
hk : 0 < k
h1 : p ∈ List.replicate k r
⊢ False
Tactic:
have h3 := (List.mem_replicate.mp h1).2
State after:
case intro.intro.intro.intro
n p q : ℕ
hp : p.Prime
hq : q.Prime
hpq : p ≠ q
r k : ℕ
h0 : r ^ k ≠ 0
hpn : p ∣ r ^ k
hqn : q ∣ r ^ k
hr : r.Prime
hk : 0 < k
h1 : p ∈ List.replicate k r
h3 : p = r
⊢ False

State before:
case intro.intro.intro.intro
n p q : ℕ
hp : p.Prime
hq : q.Prime
hpq : p ≠ q
r k : ℕ
h0 : r ^ k ≠ 0
hpn : p ∣ r ^ k
hqn : q ∣ r ^ k
hr : r.Prime
hk : 0 < k
h1 : p ∈ List.replicate k r
h3 : p = r
⊢ False
Tactic:
have h2 := (Nat.mem_factors h0).mpr ⟨hq, hqn⟩
State after:
case intro.intro.intro.intro
n p q : ℕ
hp : p.Prime
hq : q.Prime
hpq : p ≠ q
r k : ℕ
h0 : r ^ k ≠ 0
hpn : p ∣ r ^ k
hqn : q ∣ r ^ k
hr : r.Prime
hk : 0 < k
h1 : p ∈ List.replicate k r
h3 : p = r
h2 : q ∈ (r ^ k).factors
⊢ False

State before:
case intro.intro.intro.intro
n p q : ℕ
hp : p.Prime
hq : q.Prime
hpq : p ≠ q
r k : ℕ
h0 : r ^ k ≠ 0
hpn : p ∣ r ^ k
hqn : q ∣ r ^ k
hr : r.Prime
hk : 0 < k
h1 : p ∈ List.replicate k r
h3 : p = r
h2 : q ∈ (r ^ k).factors
⊢ False
Tactic:
rw [Nat.Prime.factors_pow hr] at h2
State after:
case intro.intro.intro.intro
n p q : ℕ
hp : p.Prime
hq : q.Prime
hpq : p ≠ q
r k : ℕ
h0 : r ^ k ≠ 0
hpn : p ∣ r ^ k
hqn : q ∣ r ^ k
hr : r.Prime
hk : 0 < k
h1 : p ∈ List.replicate k r
h3 : p = r
h2 : q ∈ List.replicate k r
⊢ False

State before:
case intro.intro.intro.intro
n p q : ℕ
hp : p.Prime
hq : q.Prime
hpq : p ≠ q
r k : ℕ
h0 : r ^ k ≠ 0
hpn : p ∣ r ^ k
hqn : q ∣ r ^ k
hr : r.Prime
hk : 0 < k
h1 : p ∈ List.replicate k r
h3 : p = r
h2 : q ∈ List.replicate k r
⊢ False
Tactic:
have h4 := (List.mem_replicate.mp h2).2
State after:
case intro.intro.intro.intro
n p q : ℕ
hp : p.Prime
hq : q.Prime
hpq : p ≠ q
r k : ℕ
h0 : r ^ k ≠ 0
hpn : p ∣ r ^ k
hqn : q ∣ r ^ k
hr : r.Prime
hk : 0 < k
h1 : p ∈ List.replicate k r
h3 : p = r
h2 : q ∈ List.replicate k r
h4 : q = r
⊢ False

State before:
case intro.intro.intro.intro
n p q : ℕ
hp : p.Prime
hq : q.Prime
hpq : p ≠ q
r k : ℕ
h0 : r ^ k ≠ 0
hpn : p ∣ r ^ k
hqn : q ∣ r ^ k
hr : r.Prime
hk : 0 < k
h1 : p ∈ List.replicate k r
h3 : p = r
h2 : q ∈ List.replicate k r
h4 : q = r
⊢ False
Tactic:
rw [h3, h4] at hpq
State after:
case intro.intro.intro.intro
n p q : ℕ
hp : p.Prime
hq : q.Prime
r : ℕ
hpq : r ≠ r
k : ℕ
h0 : r ^ k ≠ 0
hpn : p ∣ r ^ k
hqn : q ∣ r ^ k
hr : r.Prime
hk : 0 < k
h1 : p ∈ List.replicate k r
h3 : p = r
h2 : q ∈ List.replicate k r
h4 : q = r
⊢ False

State before:
case intro.intro.intro.intro
n p q : ℕ
hp : p.Prime
hq : q.Prime
r : ℕ
hpq : r ≠ r
k : ℕ
h0 : r ^ k ≠ 0
hpn : p ∣ r ^ k
hqn : q ∣ r ^ k
hr : r.Prime
hk : 0 < k
h1 : p ∈ List.replicate k r
h3 : p = r
h2 : q ∈ List.replicate k r
h4 : q = r
⊢ False
Tactic:
exact hpq rfl
State after:
no goals