R : Type ?u.11956
inst✝ : CommMonoidWithZero R
n✝ p : R
k✝ n k : ℕ
hk : k ≠ 0
⊢ (∃! p, Nat.Prime p ∧ p ∣ n ^ k) ↔ ∃! p, Nat.Prime p ∧ p ∣ n
R : Type ?u.11956
inst✝ : CommMonoidWithZero R
n✝ p : R
k✝ n k : ℕ
hk : k ≠ 0
⊢ IsPrimePow (n ^ k) ↔ IsPrimePow n
simp only [isPrimePow_iff_unique_prime_dvd]
case h
R : Type ?u.11956
inst✝ : CommMonoidWithZero R
n✝ p : R
k✝ n k : ℕ
hk : k ≠ 0
⊢ ∀ (a : ℕ), Nat.Prime a ∧ a ∣ n ^ k ↔ Nat.Prime a ∧ a ∣ n
R : Type ?u.11956
inst✝ : CommMonoidWithZero R
n✝ p : R
k✝ n k : ℕ
hk : k ≠ 0
⊢ (∃! p, Nat.Prime p ∧ p ∣ n ^ k) ↔ ∃! p, Nat.Prime p ∧ p ∣ n
apply exists_unique_congr
case h
R : Type ?u.11956
inst✝ : CommMonoidWithZero R
n✝ p : R
k✝ n k : ℕ
hk : k ≠ 0
⊢ ∀ (a : ℕ), Nat.Prime a → (a ∣ n ^ k ↔ a ∣ n)
case h
R : Type ?u.11956
inst✝ : CommMonoidWithZero R
n✝ p : R
k✝ n k : ℕ
hk : k ≠ 0
⊢ ∀ (a : ℕ), Nat.Prime a ∧ a ∣ n ^ k ↔ Nat.Prime a ∧ a ∣ n
simp only [and_congr_right_iff]
case h
R : Type ?u.11956
inst✝ : CommMonoidWithZero R
n✝ p✝ : R
k✝ n k : ℕ
hk : k ≠ 0
p : ℕ
hp : Nat.Prime p
⊢ p ∣ n ^ k ↔ p ∣ n
case h
R : Type ?u.11956
inst✝ : CommMonoidWithZero R
n✝ p : R
k✝ n k : ℕ
hk : k ≠ 0
⊢ ∀ (a : ℕ), Nat.Prime a → (a ∣ n ^ k ↔ a ∣ n)
intro p hp
no goals
case h
R : Type ?u.11956
inst✝ : CommMonoidWithZero R
n✝ p✝ : R
k✝ n k : ℕ
hk : k ≠ 0
p : ℕ
hp : Nat.Prime p
⊢ p ∣ n ^ k ↔ p ∣ n
exact ⟨hp.dvd_of_dvd_pow, fun t => t.trans (dvd_pow_self _ hk)⟩