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 
|- ( ( A e. NN /\ P e. ( ZZ>= ` 2 ) /\ ( P ^ 2 ) || A ) -> ( mmu ` A ) = 0 )

Proof

Step Hyp Ref Expression
1 muval 
 |-  ( A e. NN -> ( mmu ` A ) = if ( E. p e. Prime ( p ^ 2 ) || A , 0 , ( -u 1 ^ ( # ` { p e. Prime | p || A } ) ) ) )
2 1 3ad2ant1 
 |-  ( ( A e. NN /\ P e. ( ZZ>= ` 2 ) /\ ( P ^ 2 ) || A ) -> ( mmu ` A ) = if ( E. p e. Prime ( p ^ 2 ) || A , 0 , ( -u 1 ^ ( # ` { p e. Prime | p || A } ) ) ) )
3 exprmfct 
 |-  ( P e. ( ZZ>= ` 2 ) -> E. p e. Prime p || P )
4 3 3ad2ant2 
 |-  ( ( A e. NN /\ P e. ( ZZ>= ` 2 ) /\ ( P ^ 2 ) || A ) -> E. p e. Prime p || P )
5 prmnn 
 |-  ( p e. Prime -> p e. NN )
6 simpl2 
 |-  ( ( ( A e. NN /\ P e. ( ZZ>= ` 2 ) /\ ( P ^ 2 ) || A ) /\ p e. Prime ) -> P e. ( ZZ>= ` 2 ) )
7 eluz2b2 
 |-  ( P e. ( ZZ>= ` 2 ) <-> ( P e. NN /\ 1 < P ) )
8 6 7 sylib 
 |-  ( ( ( A e. NN /\ P e. ( ZZ>= ` 2 ) /\ ( P ^ 2 ) || A ) /\ p e. Prime ) -> ( P e. NN /\ 1 < P ) )
9 8 simpld 
 |-  ( ( ( A e. NN /\ P e. ( ZZ>= ` 2 ) /\ ( P ^ 2 ) || A ) /\ p e. Prime ) -> P e. NN )
10 dvdssqlem 
 |-  ( ( p e. NN /\ P e. NN ) -> ( p || P <-> ( p ^ 2 ) || ( P ^ 2 ) ) )
11 5 9 10 syl2an2 
 |-  ( ( ( A e. NN /\ P e. ( ZZ>= ` 2 ) /\ ( P ^ 2 ) || A ) /\ p e. Prime ) -> ( p || P <-> ( p ^ 2 ) || ( P ^ 2 ) ) )
12 simpl3 
 |-  ( ( ( A e. NN /\ P e. ( ZZ>= ` 2 ) /\ ( P ^ 2 ) || A ) /\ p e. Prime ) -> ( P ^ 2 ) || A )
13 prmz 
 |-  ( p e. Prime -> p e. ZZ )
14 13 adantl 
 |-  ( ( ( A e. NN /\ P e. ( ZZ>= ` 2 ) /\ ( P ^ 2 ) || A ) /\ p e. Prime ) -> p e. ZZ )
15 zsqcl 
 |-  ( p e. ZZ -> ( p ^ 2 ) e. ZZ )
16 14 15 syl 
 |-  ( ( ( A e. NN /\ P e. ( ZZ>= ` 2 ) /\ ( P ^ 2 ) || A ) /\ p e. Prime ) -> ( p ^ 2 ) e. ZZ )
17 eluzelz 
 |-  ( P e. ( ZZ>= ` 2 ) -> P e. ZZ )
18 zsqcl 
 |-  ( P e. ZZ -> ( P ^ 2 ) e. ZZ )
19 6 17 18 3syl 
 |-  ( ( ( A e. NN /\ P e. ( ZZ>= ` 2 ) /\ ( P ^ 2 ) || A ) /\ p e. Prime ) -> ( P ^ 2 ) e. ZZ )
20 simpl1 
 |-  ( ( ( A e. NN /\ P e. ( ZZ>= ` 2 ) /\ ( P ^ 2 ) || A ) /\ p e. Prime ) -> A e. NN )
21 20 nnzd 
 |-  ( ( ( A e. NN /\ P e. ( ZZ>= ` 2 ) /\ ( P ^ 2 ) || A ) /\ p e. Prime ) -> A e. ZZ )
22 dvdstr 
 |-  ( ( ( p ^ 2 ) e. ZZ /\ ( P ^ 2 ) e. ZZ /\ A e. ZZ ) -> ( ( ( p ^ 2 ) || ( P ^ 2 ) /\ ( P ^ 2 ) || A ) -> ( p ^ 2 ) || A ) )
23 16 19 21 22 syl3anc 
 |-  ( ( ( A e. NN /\ P e. ( ZZ>= ` 2 ) /\ ( P ^ 2 ) || A ) /\ p e. Prime ) -> ( ( ( p ^ 2 ) || ( P ^ 2 ) /\ ( P ^ 2 ) || A ) -> ( p ^ 2 ) || A ) )
24 12 23 mpan2d 
 |-  ( ( ( A e. NN /\ P e. ( ZZ>= ` 2 ) /\ ( P ^ 2 ) || A ) /\ p e. Prime ) -> ( ( p ^ 2 ) || ( P ^ 2 ) -> ( p ^ 2 ) || A ) )
25 11 24 sylbid 
 |-  ( ( ( A e. NN /\ P e. ( ZZ>= ` 2 ) /\ ( P ^ 2 ) || A ) /\ p e. Prime ) -> ( p || P -> ( p ^ 2 ) || A ) )
26 25 reximdva 
 |-  ( ( A e. NN /\ P e. ( ZZ>= ` 2 ) /\ ( P ^ 2 ) || A ) -> ( E. p e. Prime p || P -> E. p e. Prime ( p ^ 2 ) || A ) )
27 4 26 mpd 
 |-  ( ( A e. NN /\ P e. ( ZZ>= ` 2 ) /\ ( P ^ 2 ) || A ) -> E. p e. Prime ( p ^ 2 ) || A )
28 27 iftrued 
 |-  ( ( A e. NN /\ P e. ( ZZ>= ` 2 ) /\ ( P ^ 2 ) || A ) -> if ( E. p e. Prime ( p ^ 2 ) || A , 0 , ( -u 1 ^ ( # ` { p e. Prime | p || A } ) ) ) = 0 )
29 2 28 eqtrd 
 |-  ( ( A e. NN /\ P e. ( ZZ>= ` 2 ) /\ ( P ^ 2 ) || A ) -> ( mmu ` A ) = 0 )