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

Metamath Proof Explorer

Theorem muval1

Description: The value of the Möbius function at a non-squarefree number. (Contributed by Mario Carneiro, 21-Sep-2014)

Ref Expression
Assertion muval1 ( ( 𝐴 ∈ ℕ ∧ 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑃 ↑ 2 ) ∥ 𝐴 ) → ( μ ‘ 𝐴 ) = 0 )

Proof

Step Hyp Ref Expression
1 muval ⊢ ( 𝐴 ∈ ℕ → ( μ ‘ 𝐴 ) = if ( ∃ 𝑝 ∈ ℙ ( 𝑝 ↑ 2 ) ∥ 𝐴 , 0 , ( - 1 ↑ ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ) ) ) )
2 1 3ad2ant1 ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑃 ↑ 2 ) ∥ 𝐴 ) → ( μ ‘ 𝐴 ) = if ( ∃ 𝑝 ∈ ℙ ( 𝑝 ↑ 2 ) ∥ 𝐴 , 0 , ( - 1 ↑ ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ) ) ) )
3 exprmfct ⊢ ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) → ∃ 𝑝 ∈ ℙ 𝑝 ∥ 𝑃 )
4 3 3ad2ant2 ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑃 ↑ 2 ) ∥ 𝐴 ) → ∃ 𝑝 ∈ ℙ 𝑝 ∥ 𝑃 )
5 prmnn ⊢ ( 𝑝 ∈ ℙ → 𝑝 ∈ ℕ )
6 simpl2 ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑃 ↑ 2 ) ∥ 𝐴 ) ∧ 𝑝 ∈ ℙ ) → 𝑃 ∈ ( ℤ≥ ‘ 2 ) )
7 eluz2b2 ⊢ ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ↔ ( 𝑃 ∈ ℕ ∧ 1 < 𝑃 ) )
8 6 7 sylib ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑃 ↑ 2 ) ∥ 𝐴 ) ∧ 𝑝 ∈ ℙ ) → ( 𝑃 ∈ ℕ ∧ 1 < 𝑃 ) )
9 8 simpld ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑃 ↑ 2 ) ∥ 𝐴 ) ∧ 𝑝 ∈ ℙ ) → 𝑃 ∈ ℕ )
10 dvdssqlem ⊢ ( ( 𝑝 ∈ ℕ ∧ 𝑃 ∈ ℕ ) → ( 𝑝 ∥ 𝑃 ↔ ( 𝑝 ↑ 2 ) ∥ ( 𝑃 ↑ 2 ) ) )
11 5 9 10 syl2an2 ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑃 ↑ 2 ) ∥ 𝐴 ) ∧ 𝑝 ∈ ℙ ) → ( 𝑝 ∥ 𝑃 ↔ ( 𝑝 ↑ 2 ) ∥ ( 𝑃 ↑ 2 ) ) )
12 simpl3 ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑃 ↑ 2 ) ∥ 𝐴 ) ∧ 𝑝 ∈ ℙ ) → ( 𝑃 ↑ 2 ) ∥ 𝐴 )
13 prmz ⊢ ( 𝑝 ∈ ℙ → 𝑝 ∈ ℤ )
14 13 adantl ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑃 ↑ 2 ) ∥ 𝐴 ) ∧ 𝑝 ∈ ℙ ) → 𝑝 ∈ ℤ )
15 zsqcl ⊢ ( 𝑝 ∈ ℤ → ( 𝑝 ↑ 2 ) ∈ ℤ )
16 14 15 syl ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑃 ↑ 2 ) ∥ 𝐴 ) ∧ 𝑝 ∈ ℙ ) → ( 𝑝 ↑ 2 ) ∈ ℤ )
17 eluzelz ⊢ ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) → 𝑃 ∈ ℤ )
18 zsqcl ⊢ ( 𝑃 ∈ ℤ → ( 𝑃 ↑ 2 ) ∈ ℤ )
19 6 17 18 3syl ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑃 ↑ 2 ) ∥ 𝐴 ) ∧ 𝑝 ∈ ℙ ) → ( 𝑃 ↑ 2 ) ∈ ℤ )
20 simpl1 ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑃 ↑ 2 ) ∥ 𝐴 ) ∧ 𝑝 ∈ ℙ ) → 𝐴 ∈ ℕ )
21 20 nnzd ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑃 ↑ 2 ) ∥ 𝐴 ) ∧ 𝑝 ∈ ℙ ) → 𝐴 ∈ ℤ )
22 dvdstr ⊢ ( ( ( 𝑝 ↑ 2 ) ∈ ℤ ∧ ( 𝑃 ↑ 2 ) ∈ ℤ ∧ 𝐴 ∈ ℤ ) → ( ( ( 𝑝 ↑ 2 ) ∥ ( 𝑃 ↑ 2 ) ∧ ( 𝑃 ↑ 2 ) ∥ 𝐴 ) → ( 𝑝 ↑ 2 ) ∥ 𝐴 ) )
23 16 19 21 22 syl3anc ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑃 ↑ 2 ) ∥ 𝐴 ) ∧ 𝑝 ∈ ℙ ) → ( ( ( 𝑝 ↑ 2 ) ∥ ( 𝑃 ↑ 2 ) ∧ ( 𝑃 ↑ 2 ) ∥ 𝐴 ) → ( 𝑝 ↑ 2 ) ∥ 𝐴 ) )
24 12 23 mpan2d ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑃 ↑ 2 ) ∥ 𝐴 ) ∧ 𝑝 ∈ ℙ ) → ( ( 𝑝 ↑ 2 ) ∥ ( 𝑃 ↑ 2 ) → ( 𝑝 ↑ 2 ) ∥ 𝐴 ) )
25 11 24 sylbid ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑃 ↑ 2 ) ∥ 𝐴 ) ∧ 𝑝 ∈ ℙ ) → ( 𝑝 ∥ 𝑃 → ( 𝑝 ↑ 2 ) ∥ 𝐴 ) )
26 25 reximdva ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑃 ↑ 2 ) ∥ 𝐴 ) → ( ∃ 𝑝 ∈ ℙ 𝑝 ∥ 𝑃 → ∃ 𝑝 ∈ ℙ ( 𝑝 ↑ 2 ) ∥ 𝐴 ) )
27 4 26 mpd ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑃 ↑ 2 ) ∥ 𝐴 ) → ∃ 𝑝 ∈ ℙ ( 𝑝 ↑ 2 ) ∥ 𝐴 )
28 27 iftrued ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑃 ↑ 2 ) ∥ 𝐴 ) → if ( ∃ 𝑝 ∈ ℙ ( 𝑝 ↑ 2 ) ∥ 𝐴 , 0 , ( - 1 ↑ ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ) ) ) = 0 )
29 2 28 eqtrd ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑃 ↑ 2 ) ∥ 𝐴 ) → ( μ ‘ 𝐴 ) = 0 )