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