Theorem isnsqf

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

	Ref	Expression
Assertion	isnsqf	⊢ ( 𝐴 ∈ ℕ → ( ( μ ‘ 𝐴 ) = 0 ↔ ∃ 𝑝 ∈ ℙ ( 𝑝 ↑ 2 ) ∥ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		neg1cn	⊢ - 1 ∈ ℂ
2		neg1ne0	⊢ - 1 ≠ 0
3		prmdvdsfi	⊢ ( 𝐴 ∈ ℕ → { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ∈ Fin )
4		hashcl	⊢ ( { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ∈ Fin → ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ) ∈ ℕ0 )
5	3 4	syl	⊢ ( 𝐴 ∈ ℕ → ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ) ∈ ℕ0 )
6	5	nn0zd	⊢ ( 𝐴 ∈ ℕ → ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ) ∈ ℤ )
7		expne0i	⊢ ( ( - 1 ∈ ℂ ∧ - 1 ≠ 0 ∧ ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ) ∈ ℤ ) → ( - 1 ↑ ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ) ) ≠ 0 )
8	1 2 6 7	mp3an12i	⊢ ( 𝐴 ∈ ℕ → ( - 1 ↑ ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ) ) ≠ 0 )
9		iffalse	⊢ ( ¬ ∃ 𝑝 ∈ ℙ ( 𝑝 ↑ 2 ) ∥ 𝐴 → if ( ∃ 𝑝 ∈ ℙ ( 𝑝 ↑ 2 ) ∥ 𝐴 , 0 , ( - 1 ↑ ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ) ) ) = ( - 1 ↑ ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ) ) )
10	9	neeq1d	⊢ ( ¬ ∃ 𝑝 ∈ ℙ ( 𝑝 ↑ 2 ) ∥ 𝐴 → ( if ( ∃ 𝑝 ∈ ℙ ( 𝑝 ↑ 2 ) ∥ 𝐴 , 0 , ( - 1 ↑ ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ) ) ) ≠ 0 ↔ ( - 1 ↑ ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ) ) ≠ 0 ) )
11	8 10	syl5ibrcom	⊢ ( 𝐴 ∈ ℕ → ( ¬ ∃ 𝑝 ∈ ℙ ( 𝑝 ↑ 2 ) ∥ 𝐴 → if ( ∃ 𝑝 ∈ ℙ ( 𝑝 ↑ 2 ) ∥ 𝐴 , 0 , ( - 1 ↑ ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ) ) ) ≠ 0 ) )
12		muval	⊢ ( 𝐴 ∈ ℕ → ( μ ‘ 𝐴 ) = if ( ∃ 𝑝 ∈ ℙ ( 𝑝 ↑ 2 ) ∥ 𝐴 , 0 , ( - 1 ↑ ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ) ) ) )
13	12	neeq1d	⊢ ( 𝐴 ∈ ℕ → ( ( μ ‘ 𝐴 ) ≠ 0 ↔ if ( ∃ 𝑝 ∈ ℙ ( 𝑝 ↑ 2 ) ∥ 𝐴 , 0 , ( - 1 ↑ ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ) ) ) ≠ 0 ) )
14	11 13	sylibrd	⊢ ( 𝐴 ∈ ℕ → ( ¬ ∃ 𝑝 ∈ ℙ ( 𝑝 ↑ 2 ) ∥ 𝐴 → ( μ ‘ 𝐴 ) ≠ 0 ) )
15	14	necon4bd	⊢ ( 𝐴 ∈ ℕ → ( ( μ ‘ 𝐴 ) = 0 → ∃ 𝑝 ∈ ℙ ( 𝑝 ↑ 2 ) ∥ 𝐴 ) )
16		iftrue	⊢ ( ∃ 𝑝 ∈ ℙ ( 𝑝 ↑ 2 ) ∥ 𝐴 → if ( ∃ 𝑝 ∈ ℙ ( 𝑝 ↑ 2 ) ∥ 𝐴 , 0 , ( - 1 ↑ ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ) ) ) = 0 )
17	12	eqeq1d	⊢ ( 𝐴 ∈ ℕ → ( ( μ ‘ 𝐴 ) = 0 ↔ if ( ∃ 𝑝 ∈ ℙ ( 𝑝 ↑ 2 ) ∥ 𝐴 , 0 , ( - 1 ↑ ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ) ) ) = 0 ) )
18	16 17	syl5ibr	⊢ ( 𝐴 ∈ ℕ → ( ∃ 𝑝 ∈ ℙ ( 𝑝 ↑ 2 ) ∥ 𝐴 → ( μ ‘ 𝐴 ) = 0 ) )
19	15 18	impbid	⊢ ( 𝐴 ∈ ℕ → ( ( μ ‘ 𝐴 ) = 0 ↔ ∃ 𝑝 ∈ ℙ ( 𝑝 ↑ 2 ) ∥ 𝐴 ) )