This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ) )