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∈ℙppCntA≤1

Proof

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