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 ( 𝐴 ∈ ℕ → ( ( μ ‘ 𝐴 ) ≠ 0 ↔ ∀ 𝑝 ∈ ℙ ( 𝑝 pCnt 𝐴 ) ≤ 1 ) )

Proof

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