[GOAL]
R : Type u_1
inst✝ : CommMonoidWithZero R
n p✝ : R
k✝ : ℕ
x✝ : ∃ p k, Prime p ∧ 0 < k ∧ p ^ k = n
p : R
k : ℕ
hp : Prime p
hk : 0 < k
hn : p ^ k = n
⊢ p ^ (?m.60081 x✝ p k hp hk hn + 1) = n
[PROOFSTEP]
rwa [Nat.sub_add_cancel hk]
[GOAL]
R : Type u_1
inst✝¹ : CommMonoidWithZero R
n p : R
k : ℕ
inst✝ : NoZeroDivisors R
⊢ ¬IsPrimePow 0
[PROOFSTEP]
simp only [isPrimePow_def, not_exists, not_and', and_imp]
[GOAL]
R : Type u_1
inst✝¹ : CommMonoidWithZero R
n p : R
k : ℕ
inst✝ : NoZeroDivisors R
⊢ ∀ (x : R) (x_1 : ℕ), 0 < x_1 → x ^ x_1 = 0 → ¬Prime x
[PROOFSTEP]
intro x n _hn hx
[GOAL]
R : Type u_1
inst✝¹ : CommMonoidWithZero R
n✝ p : R
k : ℕ
inst✝ : NoZeroDivisors R
x : R
n : ℕ
_hn : 0 < n
hx : x ^ n = 0
⊢ ¬Prime x
[PROOFSTEP]
rw [pow_eq_zero hx]
[GOAL]
R : Type u_1
inst✝¹ : CommMonoidWithZero R
n✝ p : R
k : ℕ
inst✝ : NoZeroDivisors R
x : R
n : ℕ
_hn : 0 < n
hx : x ^ n = 0
⊢ ¬Prime 0
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
inst✝ : CommMonoidWithZero R
n p✝ : R
k : ℕ
p : R
hp : Prime p
⊢ p ^ 1 = p
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
inst✝ : CommMonoidWithZero R
n✝ p✝ : R
k✝ : ℕ
n : R
hn✝ : IsPrimePow n
k : ℕ
hk : k ≠ 0
p : R
k' : ℕ
hp : Prime p
hk' : 0 < k'
hn : p ^ k' = n
⊢ p ^ (k * k') = n ^ k
[PROOFSTEP]
rw [pow_mul', hn]
[GOAL]
R : Type u_1
inst✝ : CommMonoidWithZero R
n✝ p : R
k n : ℕ
⊢ IsPrimePow n ↔ ∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = n
[PROOFSTEP]
simp only [isPrimePow_def, Nat.prime_iff]
[GOAL]
R : Type u_1
inst✝ : CommMonoidWithZero R
n✝ p : R
k n : ℕ
⊢ IsPrimePow n ↔ ∃ p, p ≤ n ∧ ∃ k, k ≤ n ∧ Nat.Prime p ∧ 0 < k ∧ p ^ k = n
[PROOFSTEP]
rw [isPrimePow_nat_iff]
[GOAL]
R : Type u_1
inst✝ : CommMonoidWithZero R
n✝ p : R
k n : ℕ
⊢ (∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = n) ↔ ∃ p, p ≤ n ∧ ∃ k, k ≤ n ∧ Nat.Prime p ∧ 0 < k ∧ p ^ k = n
[PROOFSTEP]
refine' Iff.symm ⟨fun ⟨p, _, k, _, hp, hk, hn⟩ => ⟨p, k, hp, hk, hn⟩, _⟩
[GOAL]
R : Type u_1
inst✝ : CommMonoidWithZero R
n✝ p : R
k n : ℕ
⊢ (∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = n) → ∃ p, p ≤ n ∧ ∃ k, k ≤ n ∧ Nat.Prime p ∧ 0 < k ∧ p ^ k = n
[PROOFSTEP]
rintro ⟨p, k, hp, hk, rfl⟩
[GOAL]
case intro.intro.intro.intro
R : Type u_1
inst✝ : CommMonoidWithZero R
n p✝ : R
k✝ p k : ℕ
hp : Nat.Prime p
hk : 0 < k
⊢ ∃ p_1, p_1 ≤ p ^ k ∧ ∃ k_1, k_1 ≤ p ^ k ∧ Nat.Prime p_1 ∧ 0 < k_1 ∧ p_1 ^ k_1 = p ^ k
[PROOFSTEP]
refine' ⟨p, _, k, (Nat.lt_pow_self hp.one_lt _).le, hp, hk, rfl⟩
[GOAL]
case intro.intro.intro.intro
R : Type u_1
inst✝ : CommMonoidWithZero R
n p✝ : R
k✝ p k : ℕ
hp : Nat.Prime p
hk : 0 < k
⊢ p ≤ p ^ k
[PROOFSTEP]
conv => {lhs; rw [← (pow_one p)]}
[GOAL]
R : Type u_1
inst✝ : CommMonoidWithZero R
n p✝ : R
k✝ p k : ℕ
hp : Nat.Prime p
hk : 0 < k
| p ≤ p ^ k
[PROOFSTEP]
{lhs; rw [← (pow_one p)]}
[GOAL]
R : Type u_1
inst✝ : CommMonoidWithZero R
n p✝ : R
k✝ p k : ℕ
hp : Nat.Prime p
hk : 0 < k
| p ≤ p ^ k
[PROOFSTEP]
{lhs; rw [← (pow_one p)]}
[GOAL]
R : Type u_1
inst✝ : CommMonoidWithZero R
n p✝ : R
k✝ p k : ℕ
hp : Nat.Prime p
hk : 0 < k
| p ≤ p ^ k
[PROOFSTEP]
lhs
[GOAL]
R : Type u_1
inst✝ : CommMonoidWithZero R
n p✝ : R
k✝ p k : ℕ
hp : Nat.Prime p
hk : 0 < k
| p
[PROOFSTEP]
rw [← (pow_one p)]
[GOAL]
case intro.intro.intro.intro
R : Type u_1
inst✝ : CommMonoidWithZero R
n p✝ : R
k✝ p k : ℕ
hp : Nat.Prime p
hk : 0 < k
⊢ p ^ 1 ≤ p ^ k
[PROOFSTEP]
exact (Nat.pow_le_iff_le_right hp.two_le).mpr hk
[GOAL]
R : Type u_1
inst✝ : CommMonoidWithZero R
n✝ p : R
k n m : ℕ
hn : IsPrimePow n
hm : m ∣ n
hm₁ : m ≠ 1
⊢ IsPrimePow m
[PROOFSTEP]
rw [isPrimePow_nat_iff] at hn ⊢
[GOAL]
R : Type u_1
inst✝ : CommMonoidWithZero R
n✝ p : R
k n m : ℕ
hn : ∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = n
hm : m ∣ n
hm₁ : m ≠ 1
⊢ ∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = m
[PROOFSTEP]
rcases hn with ⟨p, k, hp, _hk, rfl⟩
[GOAL]
case intro.intro.intro.intro
R : Type u_1
inst✝ : CommMonoidWithZero R
n p✝ : R
k✝ m : ℕ
hm₁ : m ≠ 1
p k : ℕ
hp : Nat.Prime p
_hk : 0 < k
hm : m ∣ p ^ k
⊢ ∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = m
[PROOFSTEP]
obtain ⟨i, hik, rfl⟩ := (Nat.dvd_prime_pow hp).1 hm
[GOAL]
case intro.intro.intro.intro.intro.intro
R : Type u_1
inst✝ : CommMonoidWithZero R
n p✝ : R
k✝ p k : ℕ
hp : Nat.Prime p
_hk : 0 < k
i : ℕ
hik : i ≤ k
hm₁ : p ^ i ≠ 1
hm : p ^ i ∣ p ^ k
⊢ ∃ p_1 k, Nat.Prime p_1 ∧ 0 < k ∧ p_1 ^ k = p ^ i
[PROOFSTEP]
refine' ⟨p, i, hp, _, rfl⟩
[GOAL]
case intro.intro.intro.intro.intro.intro
R : Type u_1
inst✝ : CommMonoidWithZero R
n p✝ : R
k✝ p k : ℕ
hp : Nat.Prime p
_hk : 0 < k
i : ℕ
hik : i ≤ k
hm₁ : p ^ i ≠ 1
hm : p ^ i ∣ p ^ k
⊢ 0 < i
[PROOFSTEP]
apply Nat.pos_of_ne_zero
[GOAL]
case intro.intro.intro.intro.intro.intro.a
R : Type u_1
inst✝ : CommMonoidWithZero R
n p✝ : R
k✝ p k : ℕ
hp : Nat.Prime p
_hk : 0 < k
i : ℕ
hik : i ≤ k
hm₁ : p ^ i ≠ 1
hm : p ^ i ∣ p ^ k
⊢ i ≠ 0
[PROOFSTEP]
rintro rfl
[GOAL]
case intro.intro.intro.intro.intro.intro.a
R : Type u_1
inst✝ : CommMonoidWithZero R
n p✝ : R
k✝ p k : ℕ
hp : Nat.Prime p
_hk : 0 < k
hik : 0 ≤ k
hm₁ : p ^ 0 ≠ 1
hm : p ^ 0 ∣ p ^ k
⊢ False
[PROOFSTEP]
simp only [pow_zero, ne_eq] at hm₁ 
[GOAL]
R : Type u_1
inst✝ : CommMonoidWithZero R
n p : R
k a b : ℕ
hab : coprime a b
⊢ Disjoint (Finset.filter IsPrimePow (divisors a)) (Finset.filter IsPrimePow (divisors b))
[PROOFSTEP]
simp only [Finset.disjoint_left, Finset.mem_filter, and_imp, Nat.mem_divisors, not_and]
[GOAL]
R : Type u_1
inst✝ : CommMonoidWithZero R
n p : R
k a b : ℕ
hab : coprime a b
⊢ ∀ ⦃a_1 : ℕ⦄, a_1 ∣ a → a ≠ 0 → IsPrimePow a_1 → a_1 ∣ b → b ≠ 0 → ¬IsPrimePow a_1
[PROOFSTEP]
rintro n han _ha hn hbn _hb -
[GOAL]
R : Type u_1
inst✝ : CommMonoidWithZero R
n✝ p : R
k a b : ℕ
hab : coprime a b
n : ℕ
han : n ∣ a
_ha : a ≠ 0
hn : IsPrimePow n
hbn : n ∣ b
_hb : b ≠ 0
⊢ False
[PROOFSTEP]
exact hn.ne_one (Nat.eq_one_of_dvd_coprimes hab han hbn)
