Metamath Proof Explorer

Theorem issqf

Description: Two ways to say that a number is squarefree. (Contributed by Mario Carneiro, 3-Oct-2014)

Ref Expression
Assertion issqf ⊢ A ∈ ℕ → μ ⁡ A ≠ 0 ↔ ∀ p ∈ ℙ p pCnt A ≤ 1

Proof

Step Hyp Ref Expression
1 isnsqf ⊢ A ∈ ℕ → μ ⁡ A = 0 ↔ ∃ p ∈ ℙ p 2 ∥ A
2 1 necon3abid ⊢ A ∈ ℕ → μ ⁡ A ≠ 0 ↔ ¬ ∃ p ∈ ℙ p 2 ∥ A
3 ralnex ⊢ ∀ p ∈ ℙ ¬ p 2 ∥ A ↔ ¬ ∃ p ∈ ℙ p 2 ∥ A
4 1nn0 ⊢ 1 ∈ ℕ 0
5 pccl ⊢ p ∈ ℙ ∧ A ∈ ℕ → p pCnt A ∈ ℕ 0
6 5 ancoms ⊢ A ∈ ℕ ∧ p ∈ ℙ → p pCnt A ∈ ℕ 0
7 nn0ltp1le ⊢ 1 ∈ ℕ 0 ∧ p pCnt A ∈ ℕ 0 → 1 < p pCnt A ↔ 1 + 1 ≤ p pCnt A
8 4 6 7 sylancr ⊢ A ∈ ℕ ∧ p ∈ ℙ → 1 < p pCnt A ↔ 1 + 1 ≤ p pCnt A
9 1re ⊢ 1 ∈ ℝ
10 6 nn0red ⊢ A ∈ ℕ ∧ p ∈ ℙ → p pCnt A ∈ ℝ
11 ltnle ⊢ 1 ∈ ℝ ∧ p pCnt A ∈ ℝ → 1 < p pCnt A ↔ ¬ p pCnt A ≤ 1
12 9 10 11 sylancr ⊢ A ∈ ℕ ∧ p ∈ ℙ → 1 < p pCnt A ↔ ¬ p pCnt A ≤ 1
13 df-2 ⊢ 2 = 1 + 1
14 13 breq1i ⊢ 2 ≤ p pCnt A ↔ 1 + 1 ≤ p pCnt A
15 id ⊢ p ∈ ℙ → p ∈ ℙ
16 nnz ⊢ A ∈ ℕ → A ∈ ℤ
17 2nn0 ⊢ 2 ∈ ℕ 0
18 pcdvdsb ⊢ p ∈ ℙ ∧ A ∈ ℤ ∧ 2 ∈ ℕ 0 → 2 ≤ p pCnt A ↔ p 2 ∥ A
19 17 18 mp3an3 ⊢ p ∈ ℙ ∧ A ∈ ℤ → 2 ≤ p pCnt A ↔ p 2 ∥ A
20 15 16 19 syl2anr ⊢ A ∈ ℕ ∧ p ∈ ℙ → 2 ≤ p pCnt A ↔ p 2 ∥ A
21 14 20 bitr3id ⊢ A ∈ ℕ ∧ p ∈ ℙ → 1 + 1 ≤ p pCnt A ↔ p 2 ∥ A
22 8 12 21 3bitr3d ⊢ A ∈ ℕ ∧ p ∈ ℙ → ¬ p pCnt A ≤ 1 ↔ p 2 ∥ A
23 22 con1bid ⊢ A ∈ ℕ ∧ p ∈ ℙ → ¬ p 2 ∥ A ↔ p pCnt A ≤ 1
24 23 ralbidva ⊢ A ∈ ℕ → ∀ p ∈ ℙ ¬ p 2 ∥ A ↔ ∀ p ∈ ℙ p pCnt A ≤ 1
25 3 24 bitr3id ⊢ A ∈ ℕ → ¬ ∃ p ∈ ℙ p 2 ∥ A ↔ ∀ p ∈ ℙ p pCnt A ≤ 1
26 2 25 bitrd ⊢ A ∈ ℕ → μ ⁡ A ≠ 0 ↔ ∀ p ∈ ℙ p pCnt A ≤ 1