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) (Proof shortened by Timothy J. O'Malley, 9-Oct-2026)

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 nnmulcom 
 |-  ( ( A e. NN /\ B e. NN ) -> ( A x. B ) = ( B x. A ) )
19 18 fveq2d 
 |-  ( ( A e. NN /\ B e. NN ) -> ( mmu ` ( A x. B ) ) = ( mmu ` ( B x. A ) ) )
20 19 adantr 
 |-  ( ( ( A e. NN /\ B e. NN ) /\ ( mmu ` B ) = 0 ) -> ( mmu ` ( A x. B ) ) = ( mmu ` ( B x. A ) ) )
21 mumullem1 
 |-  ( ( ( B e. NN /\ A e. NN ) /\ ( mmu ` B ) = 0 ) -> ( mmu ` ( B x. A ) ) = 0 )
22 21 ancom1s 
 |-  ( ( ( A e. NN /\ B e. NN ) /\ ( mmu ` B ) = 0 ) -> ( mmu ` ( B x. A ) ) = 0 )
23 20 22 eqtrd 
 |-  ( ( ( A e. NN /\ B e. NN ) /\ ( mmu ` B ) = 0 ) -> ( mmu ` ( A x. B ) ) = 0 )
24 23 3adantl3 
 |-  ( ( ( A e. NN /\ B e. NN /\ ( A gcd B ) = 1 ) /\ ( mmu ` B ) = 0 ) -> ( mmu ` ( A x. B ) ) = 0 )
25 15 17 24 3eqtr4rd 
 |-  ( ( ( A e. NN /\ B e. NN /\ ( A gcd B ) = 1 ) /\ ( mmu ` B ) = 0 ) -> ( mmu ` ( A x. B ) ) = ( ( mmu ` A ) x. ( mmu ` B ) ) )
26 simpl1 
 |-  ( ( ( A e. NN /\ B e. NN /\ ( A gcd B ) = 1 ) /\ ( ( mmu ` A ) =/= 0 /\ ( mmu ` B ) =/= 0 ) ) -> A e. NN )
27 simpl2 
 |-  ( ( ( A e. NN /\ B e. NN /\ ( A gcd B ) = 1 ) /\ ( ( mmu ` A ) =/= 0 /\ ( mmu ` B ) =/= 0 ) ) -> B e. NN )
28 26 27 nnmulcld 
 |-  ( ( ( A e. NN /\ B e. NN /\ ( A gcd B ) = 1 ) /\ ( ( mmu ` A ) =/= 0 /\ ( mmu ` B ) =/= 0 ) ) -> ( A x. B ) e. NN )
29 mumullem2 
 |-  ( ( ( A e. NN /\ B e. NN /\ ( A gcd B ) = 1 ) /\ ( ( mmu ` A ) =/= 0 /\ ( mmu ` B ) =/= 0 ) ) -> ( mmu ` ( A x. B ) ) =/= 0 )
30 muval2 
 |-  ( ( ( A x. B ) e. NN /\ ( mmu ` ( A x. B ) ) =/= 0 ) -> ( mmu ` ( A x. B ) ) = ( -u 1 ^ ( # ` { p e. Prime | p || ( A x. B ) } ) ) )
31 28 29 30 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 ) } ) ) )
32 neg1cn 
 |-  -u 1 e. CC
33 32 a1i 
 |-  ( ( ( A e. NN /\ B e. NN /\ ( A gcd B ) = 1 ) /\ ( ( mmu ` A ) =/= 0 /\ ( mmu ` B ) =/= 0 ) ) -> -u 1 e. CC )
34 fzfi 
 |-  ( 1 ... B ) e. Fin
35 prmssnn 
 |-  Prime C_ NN
36 rabss2 
 |-  ( Prime C_ NN -> { p e. Prime | p || B } C_ { p e. NN | p || B } )
37 35 36 ax-mp 
 |-  { p e. Prime | p || B } C_ { p e. NN | p || B }
38 dvdsssfz1 
 |-  ( B e. NN -> { p e. NN | p || B } C_ ( 1 ... B ) )
39 27 38 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 ) )
40 37 39 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 ) )
41 ssfi 
 |-  ( ( ( 1 ... B ) e. Fin /\ { p e. Prime | p || B } C_ ( 1 ... B ) ) -> { p e. Prime | p || B } e. Fin )
42 34 40 41 sylancr 
 |-  ( ( ( A e. NN /\ B e. NN /\ ( A gcd B ) = 1 ) /\ ( ( mmu ` A ) =/= 0 /\ ( mmu ` B ) =/= 0 ) ) -> { p e. Prime | p || B } e. Fin )
43 hashcl 
 |-  ( { p e. Prime | p || B } e. Fin -> ( # ` { p e. Prime | p || B } ) e. NN0 )
44 42 43 syl 
 |-  ( ( ( A e. NN /\ B e. NN /\ ( A gcd B ) = 1 ) /\ ( ( mmu ` A ) =/= 0 /\ ( mmu ` B ) =/= 0 ) ) -> ( # ` { p e. Prime | p || B } ) e. NN0 )
45 prmdvdsfi 
 |-  ( A e. NN -> { p e. Prime | p || A } e. Fin )
46 26 45 syl 
 |-  ( ( ( A e. NN /\ B e. NN /\ ( A gcd B ) = 1 ) /\ ( ( mmu ` A ) =/= 0 /\ ( mmu ` B ) =/= 0 ) ) -> { p e. Prime | p || A } e. Fin )
47 hashcl 
 |-  ( { p e. Prime | p || A } e. Fin -> ( # ` { p e. Prime | p || A } ) e. NN0 )
48 46 47 syl 
 |-  ( ( ( A e. NN /\ B e. NN /\ ( A gcd B ) = 1 ) /\ ( ( mmu ` A ) =/= 0 /\ ( mmu ` B ) =/= 0 ) ) -> ( # ` { p e. Prime | p || A } ) e. NN0 )
49 33 44 48 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 } ) ) ) )
50 simpr 
 |-  ( ( ( ( A e. NN /\ B e. NN /\ ( A gcd B ) = 1 ) /\ ( ( mmu ` A ) =/= 0 /\ ( mmu ` B ) =/= 0 ) ) /\ p e. Prime ) -> p e. Prime )
51 simpl1 
 |-  ( ( ( A e. NN /\ B e. NN /\ ( A gcd B ) = 1 ) /\ p e. Prime ) -> A e. NN )
52 51 nnzd 
 |-  ( ( ( A e. NN /\ B e. NN /\ ( A gcd B ) = 1 ) /\ p e. Prime ) -> A e. ZZ )
53 52 adantlr 
 |-  ( ( ( ( A e. NN /\ B e. NN /\ ( A gcd B ) = 1 ) /\ ( ( mmu ` A ) =/= 0 /\ ( mmu ` B ) =/= 0 ) ) /\ p e. Prime ) -> A e. ZZ )
54 simpl2 
 |-  ( ( ( A e. NN /\ B e. NN /\ ( A gcd B ) = 1 ) /\ p e. Prime ) -> B e. NN )
55 54 nnzd 
 |-  ( ( ( A e. NN /\ B e. NN /\ ( A gcd B ) = 1 ) /\ p e. Prime ) -> B e. ZZ )
56 55 adantlr 
 |-  ( ( ( ( A e. NN /\ B e. NN /\ ( A gcd B ) = 1 ) /\ ( ( mmu ` A ) =/= 0 /\ ( mmu ` B ) =/= 0 ) ) /\ p e. Prime ) -> B e. ZZ )
57 euclemma 
 |-  ( ( p e. Prime /\ A e. ZZ /\ B e. ZZ ) -> ( p || ( A x. B ) <-> ( p || A \/ p || B ) ) )
58 50 53 56 57 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 ) ) )
59 58 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 ) } )
60 unrab 
 |-  ( { p e. Prime | p || A } u. { p e. Prime | p || B } ) = { p e. Prime | ( p || A \/ p || B ) }
61 59 60 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 } ) )
62 61 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 } ) ) )
63 inrab 
 |-  ( { p e. Prime | p || A } i^i { p e. Prime | p || B } ) = { p e. Prime | ( p || A /\ p || B ) }
64 nprmdvds1 
 |-  ( p e. Prime -> -. p || 1 )
65 64 adantl 
 |-  ( ( ( ( A e. NN /\ B e. NN /\ ( A gcd B ) = 1 ) /\ ( ( mmu ` A ) =/= 0 /\ ( mmu ` B ) =/= 0 ) ) /\ p e. Prime ) -> -. p || 1 )
66 prmz 
 |-  ( p e. Prime -> p e. ZZ )
67 66 adantl 
 |-  ( ( ( ( A e. NN /\ B e. NN /\ ( A gcd B ) = 1 ) /\ ( ( mmu ` A ) =/= 0 /\ ( mmu ` B ) =/= 0 ) ) /\ p e. Prime ) -> p e. ZZ )
68 dvdsgcd 
 |-  ( ( p e. ZZ /\ A e. ZZ /\ B e. ZZ ) -> ( ( p || A /\ p || B ) -> p || ( A gcd B ) ) )
69 67 53 56 68 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 ) ) )
70 simpll3 
 |-  ( ( ( ( A e. NN /\ B e. NN /\ ( A gcd B ) = 1 ) /\ ( ( mmu ` A ) =/= 0 /\ ( mmu ` B ) =/= 0 ) ) /\ p e. Prime ) -> ( A gcd B ) = 1 )
71 70 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 ) )
72 69 71 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 ) )
73 65 72 mtod 
 |-  ( ( ( ( A e. NN /\ B e. NN /\ ( A gcd B ) = 1 ) /\ ( ( mmu ` A ) =/= 0 /\ ( mmu ` B ) =/= 0 ) ) /\ p e. Prime ) -> -. ( p || A /\ p || B ) )
74 73 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 ) )
75 rabeq0 
 |-  ( { p e. Prime | ( p || A /\ p || B ) } = (/) <-> A. p e. Prime -. ( p || A /\ p || B ) )
76 74 75 sylibr 
 |-  ( ( ( A e. NN /\ B e. NN /\ ( A gcd B ) = 1 ) /\ ( ( mmu ` A ) =/= 0 /\ ( mmu ` B ) =/= 0 ) ) -> { p e. Prime | ( p || A /\ p || B ) } = (/) )
77 63 76 eqtrid 
 |-  ( ( ( 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 } ) = (/) )
78 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 } ) ) )
79 46 42 77 78 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 } ) ) )
80 62 79 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 } ) ) )
81 80 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 } ) ) ) )
82 simprl 
 |-  ( ( ( A e. NN /\ B e. NN /\ ( A gcd B ) = 1 ) /\ ( ( mmu ` A ) =/= 0 /\ ( mmu ` B ) =/= 0 ) ) -> ( mmu ` A ) =/= 0 )
83 muval2 
 |-  ( ( A e. NN /\ ( mmu ` A ) =/= 0 ) -> ( mmu ` A ) = ( -u 1 ^ ( # ` { p e. Prime | p || A } ) ) )
84 26 82 83 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 } ) ) )
85 simprr 
 |-  ( ( ( A e. NN /\ B e. NN /\ ( A gcd B ) = 1 ) /\ ( ( mmu ` A ) =/= 0 /\ ( mmu ` B ) =/= 0 ) ) -> ( mmu ` B ) =/= 0 )
86 muval2 
 |-  ( ( B e. NN /\ ( mmu ` B ) =/= 0 ) -> ( mmu ` B ) = ( -u 1 ^ ( # ` { p e. Prime | p || B } ) ) )
87 27 85 86 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 } ) ) )
88 84 87 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 } ) ) ) )
89 49 81 88 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 ) } ) ) )
90 31 89 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 ) ) )
91 10 25 90 pm2.61da2ne 
 |-  ( ( A e. NN /\ B e. NN /\ ( A gcd B ) = 1 ) -> ( mmu ` ( A x. B ) ) = ( ( mmu ` A ) x. ( mmu ` B ) ) )