n p : ℕ
hp : Prime p
hn : n ≠ 0
⊢ ¬1 ≤ ↑(factorization (n / p ^ ↑(factorization n) p)) p
n p : ℕ
hp : Prime p
hn : n ≠ 0
⊢ ¬p ∣ n / p ^ ↑(factorization n) p
rw [Nat.Prime.dvd_iff_one_le_factorization hp (ord_compl_pos p hn).ne']
n p : ℕ
hp : Prime p
hn : n ≠ 0
⊢ ¬1 ≤ ↑(factorization n - factorization (p ^ ↑(factorization n) p)) p
n p : ℕ
hp : Prime p
hn : n ≠ 0
⊢ ¬1 ≤ ↑(factorization (n / p ^ ↑(factorization n) p)) p
rw [Nat.factorization_div (Nat.ord_proj_dvd n p)]
no goals
n p : ℕ
hp : Prime p
hn : n ≠ 0
⊢ ¬1 ≤ ↑(factorization n - factorization (p ^ ↑(factorization n) p)) p
simp [hp.factorization]