Metamath Proof Explorer

Theorem mumul

Description: The Möbius function is a multiplicative function. This is one of the primary interests of the Möbius function as an arithmetic function. (Contributed by Mario Carneiro, 3-Oct-2014)

Ref Expression
Assertion mumul 
|- ( ( A e. NN /\ B e. NN /\ ( A gcd B ) = 1 ) -> ( mmu ` ( A x. B ) ) = ( ( mmu ` A ) x. ( mmu ` B ) ) )

Proof

Step Hyp Ref Expression
1 simpl2 
 |-  ( ( ( A e. NN /\ B e. NN /\ ( A gcd B ) = 1 ) /\ ( mmu ` A ) = 0 ) -> B e. NN )
2 mucl 
 |-  ( B e. NN -> ( mmu ` B ) e. ZZ )
3 1 2 syl 
 |-  ( ( ( A e. NN /\ B e. NN /\ ( A gcd B ) = 1 ) /\ ( mmu ` A ) = 0 ) -> ( mmu ` B ) e. ZZ )
4 3 zcnd 
 |-  ( ( ( A e. NN /\ B e. NN /\ ( A gcd B ) = 1 ) /\ ( mmu ` A ) = 0 ) -> ( mmu ` B ) e. CC )
5 4 mul02d 
 |-  ( ( ( A e. NN /\ B e. NN /\ ( A gcd B ) = 1 ) /\ ( mmu ` A ) = 0 ) -> ( 0 x. ( mmu ` B ) ) = 0 )
6 simpr 
 |-  ( ( ( A e. NN /\ B e. NN /\ ( A gcd B ) = 1 ) /\ ( mmu ` A ) = 0 ) -> ( mmu ` A ) = 0 )
7 6 oveq1d 
 |-  ( ( ( A e. NN /\ B e. NN /\ ( A gcd B ) = 1 ) /\ ( mmu ` A ) = 0 ) -> ( ( mmu ` A ) x. ( mmu ` B ) ) = ( 0 x. ( mmu ` B ) ) )
8 mumullem1 
 |-  ( ( ( A e. NN /\ B e. NN ) /\ ( mmu ` A ) = 0 ) -> ( mmu ` ( A x. B ) ) = 0 )
9 8 3adantl3 
 |-  ( ( ( A e. NN /\ B e. NN /\ ( A gcd B ) = 1 ) /\ ( mmu ` A ) = 0 ) -> ( mmu ` ( A x. B ) ) = 0 )
10 5 7 9 3eqtr4rd 
 |-  ( ( ( A e. NN /\ B e. NN /\ ( A gcd B ) = 1 ) /\ ( mmu ` A ) = 0 ) -> ( mmu ` ( A x. B ) ) = ( ( mmu ` A ) x. ( mmu ` B ) ) )
11 simpl1 
 |-  ( ( ( A e. NN /\ B e. NN /\ ( A gcd B ) = 1 ) /\ ( mmu ` B ) = 0 ) -> A e. NN )
12 mucl 
 |-  ( A e. NN -> ( mmu ` A ) e. ZZ )
13 11 12 syl 
 |-  ( ( ( A e. NN /\ B e. NN /\ ( A gcd B ) = 1 ) /\ ( mmu ` B ) = 0 ) -> ( mmu ` A ) e. ZZ )
14 13 zcnd 
 |-  ( ( ( A e. NN /\ B e. NN /\ ( A gcd B ) = 1 ) /\ ( mmu ` B ) = 0 ) -> ( mmu ` A ) e. CC )
15 14 mul01d 
 |-  ( ( ( A e. NN /\ B e. NN /\ ( A gcd B ) = 1 ) /\ ( mmu ` B ) = 0 ) -> ( ( mmu ` A ) x. 0 ) = 0 )
16 simpr 
 |-  ( ( ( A e. NN /\ B e. NN /\ ( A gcd B ) = 1 ) /\ ( mmu ` B ) = 0 ) -> ( mmu ` B ) = 0 )
17 16 oveq2d 
 |-  ( ( ( A e. NN /\ B e. NN /\ ( A gcd B ) = 1 ) /\ ( mmu ` B ) = 0 ) -> ( ( mmu ` A ) x. ( mmu ` B ) ) = ( ( mmu ` A ) x. 0 ) )
18 nncn 
 |-  ( A e. NN -> A e. CC )
19 nncn 
 |-  ( B e. NN -> B e. CC )
20 mulcom 
 |-  ( ( A e. CC /\ B e. CC ) -> ( A x. B ) = ( B x. A ) )
21 18 19 20 syl2an 
 |-  ( ( A e. NN /\ B e. NN ) -> ( A x. B ) = ( B x. A ) )
22 21 fveq2d 
 |-  ( ( A e. NN /\ B e. NN ) -> ( mmu ` ( A x. B ) ) = ( mmu ` ( B x. A ) ) )
23 22 adantr 
 |-  ( ( ( A e. NN /\ B e. NN ) /\ ( mmu ` B ) = 0 ) -> ( mmu ` ( A x. B ) ) = ( mmu ` ( B x. A ) ) )
24 mumullem1 
 |-  ( ( ( B e. NN /\ A e. NN ) /\ ( mmu ` B ) = 0 ) -> ( mmu ` ( B x. A ) ) = 0 )
25 24 ancom1s 
 |-  ( ( ( A e. NN /\ B e. NN ) /\ ( mmu ` B ) = 0 ) -> ( mmu ` ( B x. A ) ) = 0 )
26 23 25 eqtrd 
 |-  ( ( ( A e. NN /\ B e. NN ) /\ ( mmu ` B ) = 0 ) -> ( mmu ` ( A x. B ) ) = 0 )
27 26 3adantl3 
 |-  ( ( ( A e. NN /\ B e. NN /\ ( A gcd B ) = 1 ) /\ ( mmu ` B ) = 0 ) -> ( mmu ` ( A x. B ) ) = 0 )
28 15 17 27 3eqtr4rd 
 |-  ( ( ( A e. NN /\ B e. NN /\ ( A gcd B ) = 1 ) /\ ( mmu ` B ) = 0 ) -> ( mmu ` ( A x. B ) ) = ( ( mmu ` A ) x. ( mmu ` B ) ) )
29 simpl1 
 |-  ( ( ( A e. NN /\ B e. NN /\ ( A gcd B ) = 1 ) /\ ( ( mmu ` A ) =/= 0 /\ ( mmu ` B ) =/= 0 ) ) -> A e. NN )
30 simpl2 
 |-  ( ( ( A e. NN /\ B e. NN /\ ( A gcd B ) = 1 ) /\ ( ( mmu ` A ) =/= 0 /\ ( mmu ` B ) =/= 0 ) ) -> B e. NN )
31 29 30 nnmulcld 
 |-  ( ( ( A e. NN /\ B e. NN /\ ( A gcd B ) = 1 ) /\ ( ( mmu ` A ) =/= 0 /\ ( mmu ` B ) =/= 0 ) ) -> ( A x. B ) e. NN )
32 mumullem2 
 |-  ( ( ( A e. NN /\ B e. NN /\ ( A gcd B ) = 1 ) /\ ( ( mmu ` A ) =/= 0 /\ ( mmu ` B ) =/= 0 ) ) -> ( mmu ` ( A x. B ) ) =/= 0 )
33 muval2 
 |-  ( ( ( A x. B ) e. NN /\ ( mmu ` ( A x. B ) ) =/= 0 ) -> ( mmu ` ( A x. B ) ) = ( -u 1 ^ ( # ` { p e. Prime | p || ( A x. B ) } ) ) )
34 31 32 33 syl2anc 
 |-  ( ( ( A e. NN /\ B e. NN /\ ( A gcd B ) = 1 ) /\ ( ( mmu ` A ) =/= 0 /\ ( mmu ` B ) =/= 0 ) ) -> ( mmu ` ( A x. B ) ) = ( -u 1 ^ ( # ` { p e. Prime | p || ( A x. B ) } ) ) )
35 neg1cn 
 |-  -u 1 e. CC
36 35 a1i 
 |-  ( ( ( A e. NN /\ B e. NN /\ ( A gcd B ) = 1 ) /\ ( ( mmu ` A ) =/= 0 /\ ( mmu ` B ) =/= 0 ) ) -> -u 1 e. CC )
37 fzfi 
 |-  ( 1 ... B ) e. Fin
38 prmssnn 
 |-  Prime C_ NN
39 rabss2 
 |-  ( Prime C_ NN -> { p e. Prime | p || B } C_ { p e. NN | p || B } )
40 38 39 ax-mp 
 |-  { p e. Prime | p || B } C_ { p e. NN | p || B }
41 dvdsssfz1 
 |-  ( B e. NN -> { p e. NN | p || B } C_ ( 1 ... B ) )
42 30 41 syl 
 |-  ( ( ( A e. NN /\ B e. NN /\ ( A gcd B ) = 1 ) /\ ( ( mmu ` A ) =/= 0 /\ ( mmu ` B ) =/= 0 ) ) -> { p e. NN | p || B } C_ ( 1 ... B ) )
43 40 42 sstrid 
 |-  ( ( ( A e. NN /\ B e. NN /\ ( A gcd B ) = 1 ) /\ ( ( mmu ` A ) =/= 0 /\ ( mmu ` B ) =/= 0 ) ) -> { p e. Prime | p || B } C_ ( 1 ... B ) )
44 ssfi 
 |-  ( ( ( 1 ... B ) e. Fin /\ { p e. Prime | p || B } C_ ( 1 ... B ) ) -> { p e. Prime | p || B } e. Fin )
45 37 43 44 sylancr 
 |-  ( ( ( A e. NN /\ B e. NN /\ ( A gcd B ) = 1 ) /\ ( ( mmu ` A ) =/= 0 /\ ( mmu ` B ) =/= 0 ) ) -> { p e. Prime | p || B } e. Fin )
46 hashcl 
 |-  ( { p e. Prime | p || B } e. Fin -> ( # ` { p e. Prime | p || B } ) e. NN0 )
47 45 46 syl 
 |-  ( ( ( A e. NN /\ B e. NN /\ ( A gcd B ) = 1 ) /\ ( ( mmu ` A ) =/= 0 /\ ( mmu ` B ) =/= 0 ) ) -> ( # ` { p e. Prime | p || B } ) e. NN0 )
48 fzfi 
 |-  ( 1 ... A ) e. Fin
49 rabss2 
 |-  ( Prime C_ NN -> { p e. Prime | p || A } C_ { p e. NN | p || A } )
50 38 49 ax-mp 
 |-  { p e. Prime | p || A } C_ { p e. NN | p || A }
51 dvdsssfz1 
 |-  ( A e. NN -> { p e. NN | p || A } C_ ( 1 ... A ) )
52 29 51 syl 
 |-  ( ( ( A e. NN /\ B e. NN /\ ( A gcd B ) = 1 ) /\ ( ( mmu ` A ) =/= 0 /\ ( mmu ` B ) =/= 0 ) ) -> { p e. NN | p || A } C_ ( 1 ... A ) )
53 50 52 sstrid 
 |-  ( ( ( A e. NN /\ B e. NN /\ ( A gcd B ) = 1 ) /\ ( ( mmu ` A ) =/= 0 /\ ( mmu ` B ) =/= 0 ) ) -> { p e. Prime | p || A } C_ ( 1 ... A ) )
54 ssfi 
 |-  ( ( ( 1 ... A ) e. Fin /\ { p e. Prime | p || A } C_ ( 1 ... A ) ) -> { p e. Prime | p || A } e. Fin )
55 48 53 54 sylancr 
 |-  ( ( ( A e. NN /\ B e. NN /\ ( A gcd B ) = 1 ) /\ ( ( mmu ` A ) =/= 0 /\ ( mmu ` B ) =/= 0 ) ) -> { p e. Prime | p || A } e. Fin )
56 hashcl 
 |-  ( { p e. Prime | p || A } e. Fin -> ( # ` { p e. Prime | p || A } ) e. NN0 )
57 55 56 syl 
 |-  ( ( ( A e. NN /\ B e. NN /\ ( A gcd B ) = 1 ) /\ ( ( mmu ` A ) =/= 0 /\ ( mmu ` B ) =/= 0 ) ) -> ( # ` { p e. Prime | p || A } ) e. NN0 )
58 36 47 57 expaddd 
 |-  ( ( ( A e. NN /\ B e. NN /\ ( A gcd B ) = 1 ) /\ ( ( mmu ` A ) =/= 0 /\ ( mmu ` B ) =/= 0 ) ) -> ( -u 1 ^ ( ( # ` { p e. Prime | p || A } ) + ( # ` { p e. Prime | p || B } ) ) ) = ( ( -u 1 ^ ( # ` { p e. Prime | p || A } ) ) x. ( -u 1 ^ ( # ` { p e. Prime | p || B } ) ) ) )
59 simpr 
 |-  ( ( ( ( A e. NN /\ B e. NN /\ ( A gcd B ) = 1 ) /\ ( ( mmu ` A ) =/= 0 /\ ( mmu ` B ) =/= 0 ) ) /\ p e. Prime ) -> p e. Prime )
60 simpl1 
 |-  ( ( ( A e. NN /\ B e. NN /\ ( A gcd B ) = 1 ) /\ p e. Prime ) -> A e. NN )
61 60 nnzd 
 |-  ( ( ( A e. NN /\ B e. NN /\ ( A gcd B ) = 1 ) /\ p e. Prime ) -> A e. ZZ )
62 61 adantlr 
 |-  ( ( ( ( A e. NN /\ B e. NN /\ ( A gcd B ) = 1 ) /\ ( ( mmu ` A ) =/= 0 /\ ( mmu ` B ) =/= 0 ) ) /\ p e. Prime ) -> A e. ZZ )
63 simpl2 
 |-  ( ( ( A e. NN /\ B e. NN /\ ( A gcd B ) = 1 ) /\ p e. Prime ) -> B e. NN )
64 63 nnzd 
 |-  ( ( ( A e. NN /\ B e. NN /\ ( A gcd B ) = 1 ) /\ p e. Prime ) -> B e. ZZ )
65 64 adantlr 
 |-  ( ( ( ( A e. NN /\ B e. NN /\ ( A gcd B ) = 1 ) /\ ( ( mmu ` A ) =/= 0 /\ ( mmu ` B ) =/= 0 ) ) /\ p e. Prime ) -> B e. ZZ )
66 euclemma 
 |-  ( ( p e. Prime /\ A e. ZZ /\ B e. ZZ ) -> ( p || ( A x. B ) <-> ( p || A \/ p || B ) ) )
67 59 62 65 66 syl3anc 
 |-  ( ( ( ( A e. NN /\ B e. NN /\ ( A gcd B ) = 1 ) /\ ( ( mmu ` A ) =/= 0 /\ ( mmu ` B ) =/= 0 ) ) /\ p e. Prime ) -> ( p || ( A x. B ) <-> ( p || A \/ p || B ) ) )
68 67 rabbidva 
 |-  ( ( ( A e. NN /\ B e. NN /\ ( A gcd B ) = 1 ) /\ ( ( mmu ` A ) =/= 0 /\ ( mmu ` B ) =/= 0 ) ) -> { p e. Prime | p || ( A x. B ) } = { p e. Prime | ( p || A \/ p || B ) } )
69 unrab 
 |-  ( { p e. Prime | p || A } u. { p e. Prime | p || B } ) = { p e. Prime | ( p || A \/ p || B ) }
70 68 69 eqtr4di 
 |-  ( ( ( A e. NN /\ B e. NN /\ ( A gcd B ) = 1 ) /\ ( ( mmu ` A ) =/= 0 /\ ( mmu ` B ) =/= 0 ) ) -> { p e. Prime | p || ( A x. B ) } = ( { p e. Prime | p || A } u. { p e. Prime | p || B } ) )
71 70 fveq2d 
 |-  ( ( ( A e. NN /\ B e. NN /\ ( A gcd B ) = 1 ) /\ ( ( mmu ` A ) =/= 0 /\ ( mmu ` B ) =/= 0 ) ) -> ( # ` { p e. Prime | p || ( A x. B ) } ) = ( # ` ( { p e. Prime | p || A } u. { p e. Prime | p || B } ) ) )
72 inrab 
 |-  ( { p e. Prime | p || A } i^i { p e. Prime | p || B } ) = { p e. Prime | ( p || A /\ p || B ) }
73 nprmdvds1 
 |-  ( p e. Prime -> -. p || 1 )
74 73 adantl 
 |-  ( ( ( ( A e. NN /\ B e. NN /\ ( A gcd B ) = 1 ) /\ ( ( mmu ` A ) =/= 0 /\ ( mmu ` B ) =/= 0 ) ) /\ p e. Prime ) -> -. p || 1 )
75 prmz 
 |-  ( p e. Prime -> p e. ZZ )
76 75 adantl 
 |-  ( ( ( ( A e. NN /\ B e. NN /\ ( A gcd B ) = 1 ) /\ ( ( mmu ` A ) =/= 0 /\ ( mmu ` B ) =/= 0 ) ) /\ p e. Prime ) -> p e. ZZ )
77 dvdsgcd 
 |-  ( ( p e. ZZ /\ A e. ZZ /\ B e. ZZ ) -> ( ( p || A /\ p || B ) -> p || ( A gcd B ) ) )
78 76 62 65 77 syl3anc 
 |-  ( ( ( ( A e. NN /\ B e. NN /\ ( A gcd B ) = 1 ) /\ ( ( mmu ` A ) =/= 0 /\ ( mmu ` B ) =/= 0 ) ) /\ p e. Prime ) -> ( ( p || A /\ p || B ) -> p || ( A gcd B ) ) )
79 simpll3 
 |-  ( ( ( ( A e. NN /\ B e. NN /\ ( A gcd B ) = 1 ) /\ ( ( mmu ` A ) =/= 0 /\ ( mmu ` B ) =/= 0 ) ) /\ p e. Prime ) -> ( A gcd B ) = 1 )
80 79 breq2d 
 |-  ( ( ( ( A e. NN /\ B e. NN /\ ( A gcd B ) = 1 ) /\ ( ( mmu ` A ) =/= 0 /\ ( mmu ` B ) =/= 0 ) ) /\ p e. Prime ) -> ( p || ( A gcd B ) <-> p || 1 ) )
81 78 80 sylibd 
 |-  ( ( ( ( A e. NN /\ B e. NN /\ ( A gcd B ) = 1 ) /\ ( ( mmu ` A ) =/= 0 /\ ( mmu ` B ) =/= 0 ) ) /\ p e. Prime ) -> ( ( p || A /\ p || B ) -> p || 1 ) )
82 74 81 mtod 
 |-  ( ( ( ( A e. NN /\ B e. NN /\ ( A gcd B ) = 1 ) /\ ( ( mmu ` A ) =/= 0 /\ ( mmu ` B ) =/= 0 ) ) /\ p e. Prime ) -> -. ( p || A /\ p || B ) )
83 82 ralrimiva 
 |-  ( ( ( A e. NN /\ B e. NN /\ ( A gcd B ) = 1 ) /\ ( ( mmu ` A ) =/= 0 /\ ( mmu ` B ) =/= 0 ) ) -> A. p e. Prime -. ( p || A /\ p || B ) )
84 rabeq0 
 |-  ( { p e. Prime | ( p || A /\ p || B ) } = (/) <-> A. p e. Prime -. ( p || A /\ p || B ) )
85 83 84 sylibr 
 |-  ( ( ( A e. NN /\ B e. NN /\ ( A gcd B ) = 1 ) /\ ( ( mmu ` A ) =/= 0 /\ ( mmu ` B ) =/= 0 ) ) -> { p e. Prime | ( p || A /\ p || B ) } = (/) )
86 72 85 syl5eq 
 |-  ( ( ( A e. NN /\ B e. NN /\ ( A gcd B ) = 1 ) /\ ( ( mmu ` A ) =/= 0 /\ ( mmu ` B ) =/= 0 ) ) -> ( { p e. Prime | p || A } i^i { p e. Prime | p || B } ) = (/) )
87 hashun 
 |-  ( ( { p e. Prime | p || A } e. Fin /\ { p e. Prime | p || B } e. Fin /\ ( { p e. Prime | p || A } i^i { p e. Prime | p || B } ) = (/) ) -> ( # ` ( { p e. Prime | p || A } u. { p e. Prime | p || B } ) ) = ( ( # ` { p e. Prime | p || A } ) + ( # ` { p e. Prime | p || B } ) ) )
88 55 45 86 87 syl3anc 
 |-  ( ( ( A e. NN /\ B e. NN /\ ( A gcd B ) = 1 ) /\ ( ( mmu ` A ) =/= 0 /\ ( mmu ` B ) =/= 0 ) ) -> ( # ` ( { p e. Prime | p || A } u. { p e. Prime | p || B } ) ) = ( ( # ` { p e. Prime | p || A } ) + ( # ` { p e. Prime | p || B } ) ) )
89 71 88 eqtrd 
 |-  ( ( ( A e. NN /\ B e. NN /\ ( A gcd B ) = 1 ) /\ ( ( mmu ` A ) =/= 0 /\ ( mmu ` B ) =/= 0 ) ) -> ( # ` { p e. Prime | p || ( A x. B ) } ) = ( ( # ` { p e. Prime | p || A } ) + ( # ` { p e. Prime | p || B } ) ) )
90 89 oveq2d 
 |-  ( ( ( A e. NN /\ B e. NN /\ ( A gcd B ) = 1 ) /\ ( ( mmu ` A ) =/= 0 /\ ( mmu ` B ) =/= 0 ) ) -> ( -u 1 ^ ( # ` { p e. Prime | p || ( A x. B ) } ) ) = ( -u 1 ^ ( ( # ` { p e. Prime | p || A } ) + ( # ` { p e. Prime | p || B } ) ) ) )
91 simprl 
 |-  ( ( ( A e. NN /\ B e. NN /\ ( A gcd B ) = 1 ) /\ ( ( mmu ` A ) =/= 0 /\ ( mmu ` B ) =/= 0 ) ) -> ( mmu ` A ) =/= 0 )
92 muval2 
 |-  ( ( A e. NN /\ ( mmu ` A ) =/= 0 ) -> ( mmu ` A ) = ( -u 1 ^ ( # ` { p e. Prime | p || A } ) ) )
93 29 91 92 syl2anc 
 |-  ( ( ( A e. NN /\ B e. NN /\ ( A gcd B ) = 1 ) /\ ( ( mmu ` A ) =/= 0 /\ ( mmu ` B ) =/= 0 ) ) -> ( mmu ` A ) = ( -u 1 ^ ( # ` { p e. Prime | p || A } ) ) )
94 simprr 
 |-  ( ( ( A e. NN /\ B e. NN /\ ( A gcd B ) = 1 ) /\ ( ( mmu ` A ) =/= 0 /\ ( mmu ` B ) =/= 0 ) ) -> ( mmu ` B ) =/= 0 )
95 muval2 
 |-  ( ( B e. NN /\ ( mmu ` B ) =/= 0 ) -> ( mmu ` B ) = ( -u 1 ^ ( # ` { p e. Prime | p || B } ) ) )
96 30 94 95 syl2anc 
 |-  ( ( ( A e. NN /\ B e. NN /\ ( A gcd B ) = 1 ) /\ ( ( mmu ` A ) =/= 0 /\ ( mmu ` B ) =/= 0 ) ) -> ( mmu ` B ) = ( -u 1 ^ ( # ` { p e. Prime | p || B } ) ) )
97 93 96 oveq12d 
 |-  ( ( ( A e. NN /\ B e. NN /\ ( A gcd B ) = 1 ) /\ ( ( mmu ` A ) =/= 0 /\ ( mmu ` B ) =/= 0 ) ) -> ( ( mmu ` A ) x. ( mmu ` B ) ) = ( ( -u 1 ^ ( # ` { p e. Prime | p || A } ) ) x. ( -u 1 ^ ( # ` { p e. Prime | p || B } ) ) ) )
98 58 90 97 3eqtr4rd 
 |-  ( ( ( A e. NN /\ B e. NN /\ ( A gcd B ) = 1 ) /\ ( ( mmu ` A ) =/= 0 /\ ( mmu ` B ) =/= 0 ) ) -> ( ( mmu ` A ) x. ( mmu ` B ) ) = ( -u 1 ^ ( # ` { p e. Prime | p || ( A x. B ) } ) ) )
99 34 98 eqtr4d 
 |-  ( ( ( A e. NN /\ B e. NN /\ ( A gcd B ) = 1 ) /\ ( ( mmu ` A ) =/= 0 /\ ( mmu ` B ) =/= 0 ) ) -> ( mmu ` ( A x. B ) ) = ( ( mmu ` A ) x. ( mmu ` B ) ) )
100 10 28 99 pm2.61da2ne 
 |-  ( ( A e. NN /\ B e. NN /\ ( A gcd B ) = 1 ) -> ( mmu ` ( A x. B ) ) = ( ( mmu ` A ) x. ( mmu ` B ) ) )