R : Type ?u.6665
inst✝ : CommMonoidWithZero R
n✝ p : R
k n : ℕ
hn : n ≠ 1
h : ∃ p, Nat.Prime p ∧ n / p ^ ↑(Nat.factorization n) p = 1
⊢ IsPrimePow n
R : Type ?u.6665
inst✝ : CommMonoidWithZero R
n✝ p : R
k n : ℕ
hn : n ≠ 1
⊢ IsPrimePow n ↔ ∃ p, Nat.Prime p ∧ n / p ^ ↑(Nat.factorization n) p = 1
refine' ⟨fun h => IsPrimePow.exists_ord_compl_eq_one h, fun h => _⟩
case intro.intro
R : Type ?u.6665
inst✝ : CommMonoidWithZero R
n✝ p✝ : R
k n : ℕ
hn : n ≠ 1
p : ℕ
pp : Nat.Prime p
h : n / p ^ ↑(Nat.factorization n) p = 1
⊢ IsPrimePow n
R : Type ?u.6665
inst✝ : CommMonoidWithZero R
n✝ p : R
k n : ℕ
hn : n ≠ 1
h : ∃ p, Nat.Prime p ∧ n / p ^ ↑(Nat.factorization n) p = 1
⊢ IsPrimePow n
rcases h with ⟨p, pp, h⟩
case intro.intro
R : Type ?u.6665
inst✝ : CommMonoidWithZero R
n✝ p✝ : R
k n : ℕ
hn : n ≠ 1
p : ℕ
pp : Nat.Prime p
h : n / p ^ ↑(Nat.factorization n) p = 1
⊢ ∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = n
case intro.intro
R : Type ?u.6665
inst✝ : CommMonoidWithZero R
n✝ p✝ : R
k n : ℕ
hn : n ≠ 1
p : ℕ
pp : Nat.Prime p
h : n / p ^ ↑(Nat.factorization n) p = 1
⊢ IsPrimePow n
rw [isPrimePow_nat_iff]
case intro.intro
R : Type ?u.6665
inst✝ : CommMonoidWithZero R
n✝ p✝ : R
k n p : ℕ
hn : p ^ ↑(Nat.factorization n) p ≠ 1
pp : Nat.Prime p
h : n / p ^ ↑(Nat.factorization n) p = 1
⊢ ∃ p_1 k, Nat.Prime p_1 ∧ 0 < k ∧ p_1 ^ k = p ^ ↑(Nat.factorization n) p
case intro.intro
R : Type ?u.6665
inst✝ : CommMonoidWithZero R
n✝ p✝ : R
k n : ℕ
hn : n ≠ 1
p : ℕ
pp : Nat.Prime p
h : n / p ^ ↑(Nat.factorization n) p = 1
⊢ ∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = n
rw [← Nat.eq_of_dvd_of_div_eq_one (Nat.ord_proj_dvd n p) h] at hn⊢
case intro.intro
R : Type ?u.6665
inst✝ : CommMonoidWithZero R
n✝ p✝ : R
k n p : ℕ
hn : p ^ ↑(Nat.factorization n) p ≠ 1
pp : Nat.Prime p
h : n / p ^ ↑(Nat.factorization n) p = 1
⊢ 0 < ↑(Nat.factorization n) p
case intro.intro
R : Type ?u.6665
inst✝ : CommMonoidWithZero R
n✝ p✝ : R
k n p : ℕ
hn : p ^ ↑(Nat.factorization n) p ≠ 1
pp : Nat.Prime p
h : n / p ^ ↑(Nat.factorization n) p = 1
⊢ ∃ p_1 k, Nat.Prime p_1 ∧ 0 < k ∧ p_1 ^ k = p ^ ↑(Nat.factorization n) p
refine' ⟨p, n.factorization p, pp, _, by simp⟩
case intro.intro
R : Type ?u.6665
inst✝ : CommMonoidWithZero R
n✝ p✝ : R
k n p : ℕ
pp : Nat.Prime p
h : n / p ^ ↑(Nat.factorization n) p = 1
hn : ↑(Nat.factorization n) p ≤ 0
⊢ p ^ ↑(Nat.factorization n) p = 1
case intro.intro
R : Type ?u.6665
inst✝ : CommMonoidWithZero R
n✝ p✝ : R
k n p : ℕ
hn : p ^ ↑(Nat.factorization n) p ≠ 1
pp : Nat.Prime p
h : n / p ^ ↑(Nat.factorization n) p = 1
⊢ 0 < ↑(Nat.factorization n) p
contrapose! hn
no goals
case intro.intro
R : Type ?u.6665
inst✝ : CommMonoidWithZero R
n✝ p✝ : R
k n p : ℕ
pp : Nat.Prime p
h : n / p ^ ↑(Nat.factorization n) p = 1
hn : ↑(Nat.factorization n) p ≤ 0
⊢ p ^ ↑(Nat.factorization n) p = 1
simp [le_zero_iff.1 hn]
no goals
R : Type ?u.6665
inst✝ : CommMonoidWithZero R
n✝ p✝ : R
k n p : ℕ
hn : p ^ ↑(Nat.factorization n) p ≠ 1
pp : Nat.Prime p
h : n / p ^ ↑(Nat.factorization n) p = 1
⊢ p ^ ↑(Nat.factorization n) p = p ^ ↑(Nat.factorization n) p
simp