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 ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ ( 𝐴 gcd 𝐵 ) = 1 ) → ( μ ‘ ( 𝐴 · 𝐵 ) ) = ( ( μ ‘ 𝐴 ) · ( μ ‘ 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 simpl2 ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ ( 𝐴 gcd 𝐵 ) = 1 ) ∧ ( μ ‘ 𝐴 ) = 0 ) → 𝐵 ∈ ℕ )
2 mucl ⊢ ( 𝐵 ∈ ℕ → ( μ ‘ 𝐵 ) ∈ ℤ )
3 1 2 syl ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ ( 𝐴 gcd 𝐵 ) = 1 ) ∧ ( μ ‘ 𝐴 ) = 0 ) → ( μ ‘ 𝐵 ) ∈ ℤ )
4 3 zcnd ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ ( 𝐴 gcd 𝐵 ) = 1 ) ∧ ( μ ‘ 𝐴 ) = 0 ) → ( μ ‘ 𝐵 ) ∈ ℂ )
5 4 mul02d ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ ( 𝐴 gcd 𝐵 ) = 1 ) ∧ ( μ ‘ 𝐴 ) = 0 ) → ( 0 · ( μ ‘ 𝐵 ) ) = 0 )
6 simpr ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ ( 𝐴 gcd 𝐵 ) = 1 ) ∧ ( μ ‘ 𝐴 ) = 0 ) → ( μ ‘ 𝐴 ) = 0 )
7 6 oveq1d ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ ( 𝐴 gcd 𝐵 ) = 1 ) ∧ ( μ ‘ 𝐴 ) = 0 ) → ( ( μ ‘ 𝐴 ) · ( μ ‘ 𝐵 ) ) = ( 0 · ( μ ‘ 𝐵 ) ) )
8 mumullem1 ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) ∧ ( μ ‘ 𝐴 ) = 0 ) → ( μ ‘ ( 𝐴 · 𝐵 ) ) = 0 )
9 8 3adantl3 ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ ( 𝐴 gcd 𝐵 ) = 1 ) ∧ ( μ ‘ 𝐴 ) = 0 ) → ( μ ‘ ( 𝐴 · 𝐵 ) ) = 0 )
10 5 7 9 3eqtr4rd ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ ( 𝐴 gcd 𝐵 ) = 1 ) ∧ ( μ ‘ 𝐴 ) = 0 ) → ( μ ‘ ( 𝐴 · 𝐵 ) ) = ( ( μ ‘ 𝐴 ) · ( μ ‘ 𝐵 ) ) )
11 simpl1 ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ ( 𝐴 gcd 𝐵 ) = 1 ) ∧ ( μ ‘ 𝐵 ) = 0 ) → 𝐴 ∈ ℕ )
12 mucl ⊢ ( 𝐴 ∈ ℕ → ( μ ‘ 𝐴 ) ∈ ℤ )
13 11 12 syl ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ ( 𝐴 gcd 𝐵 ) = 1 ) ∧ ( μ ‘ 𝐵 ) = 0 ) → ( μ ‘ 𝐴 ) ∈ ℤ )
14 13 zcnd ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ ( 𝐴 gcd 𝐵 ) = 1 ) ∧ ( μ ‘ 𝐵 ) = 0 ) → ( μ ‘ 𝐴 ) ∈ ℂ )
15 14 mul01d ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ ( 𝐴 gcd 𝐵 ) = 1 ) ∧ ( μ ‘ 𝐵 ) = 0 ) → ( ( μ ‘ 𝐴 ) · 0 ) = 0 )
16 simpr ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ ( 𝐴 gcd 𝐵 ) = 1 ) ∧ ( μ ‘ 𝐵 ) = 0 ) → ( μ ‘ 𝐵 ) = 0 )
17 16 oveq2d ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ ( 𝐴 gcd 𝐵 ) = 1 ) ∧ ( μ ‘ 𝐵 ) = 0 ) → ( ( μ ‘ 𝐴 ) · ( μ ‘ 𝐵 ) ) = ( ( μ ‘ 𝐴 ) · 0 ) )
18 nncn ⊢ ( 𝐴 ∈ ℕ → 𝐴 ∈ ℂ )
19 nncn ⊢ ( 𝐵 ∈ ℕ → 𝐵 ∈ ℂ )
20 mulcom ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 · 𝐵 ) = ( 𝐵 · 𝐴 ) )
21 18 19 20 syl2an ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → ( 𝐴 · 𝐵 ) = ( 𝐵 · 𝐴 ) )
22 21 fveq2d ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → ( μ ‘ ( 𝐴 · 𝐵 ) ) = ( μ ‘ ( 𝐵 · 𝐴 ) ) )
23 22 adantr ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) ∧ ( μ ‘ 𝐵 ) = 0 ) → ( μ ‘ ( 𝐴 · 𝐵 ) ) = ( μ ‘ ( 𝐵 · 𝐴 ) ) )
24 mumullem1 ⊢ ( ( ( 𝐵 ∈ ℕ ∧ 𝐴 ∈ ℕ ) ∧ ( μ ‘ 𝐵 ) = 0 ) → ( μ ‘ ( 𝐵 · 𝐴 ) ) = 0 )
25 24 ancom1s ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) ∧ ( μ ‘ 𝐵 ) = 0 ) → ( μ ‘ ( 𝐵 · 𝐴 ) ) = 0 )
26 23 25 eqtrd ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) ∧ ( μ ‘ 𝐵 ) = 0 ) → ( μ ‘ ( 𝐴 · 𝐵 ) ) = 0 )
27 26 3adantl3 ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ ( 𝐴 gcd 𝐵 ) = 1 ) ∧ ( μ ‘ 𝐵 ) = 0 ) → ( μ ‘ ( 𝐴 · 𝐵 ) ) = 0 )
28 15 17 27 3eqtr4rd ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ ( 𝐴 gcd 𝐵 ) = 1 ) ∧ ( μ ‘ 𝐵 ) = 0 ) → ( μ ‘ ( 𝐴 · 𝐵 ) ) = ( ( μ ‘ 𝐴 ) · ( μ ‘ 𝐵 ) ) )
29 simpl1 ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ ( 𝐴 gcd 𝐵 ) = 1 ) ∧ ( ( μ ‘ 𝐴 ) ≠ 0 ∧ ( μ ‘ 𝐵 ) ≠ 0 ) ) → 𝐴 ∈ ℕ )
30 simpl2 ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ ( 𝐴 gcd 𝐵 ) = 1 ) ∧ ( ( μ ‘ 𝐴 ) ≠ 0 ∧ ( μ ‘ 𝐵 ) ≠ 0 ) ) → 𝐵 ∈ ℕ )
31 29 30 nnmulcld ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ ( 𝐴 gcd 𝐵 ) = 1 ) ∧ ( ( μ ‘ 𝐴 ) ≠ 0 ∧ ( μ ‘ 𝐵 ) ≠ 0 ) ) → ( 𝐴 · 𝐵 ) ∈ ℕ )
32 mumullem2 ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ ( 𝐴 gcd 𝐵 ) = 1 ) ∧ ( ( μ ‘ 𝐴 ) ≠ 0 ∧ ( μ ‘ 𝐵 ) ≠ 0 ) ) → ( μ ‘ ( 𝐴 · 𝐵 ) ) ≠ 0 )
33 muval2 ⊢ ( ( ( 𝐴 · 𝐵 ) ∈ ℕ ∧ ( μ ‘ ( 𝐴 · 𝐵 ) ) ≠ 0 ) → ( μ ‘ ( 𝐴 · 𝐵 ) ) = ( - 1 ↑ ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ ( 𝐴 · 𝐵 ) } ) ) )
34 31 32 33 syl2anc ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ ( 𝐴 gcd 𝐵 ) = 1 ) ∧ ( ( μ ‘ 𝐴 ) ≠ 0 ∧ ( μ ‘ 𝐵 ) ≠ 0 ) ) → ( μ ‘ ( 𝐴 · 𝐵 ) ) = ( - 1 ↑ ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ ( 𝐴 · 𝐵 ) } ) ) )
35 neg1cn ⊢ - 1 ∈ ℂ
36 35 a1i ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ ( 𝐴 gcd 𝐵 ) = 1 ) ∧ ( ( μ ‘ 𝐴 ) ≠ 0 ∧ ( μ ‘ 𝐵 ) ≠ 0 ) ) → - 1 ∈ ℂ )
37 fzfi ⊢ ( 1 ... 𝐵 ) ∈ Fin
38 prmssnn ⊢ ℙ ⊆ ℕ
39 rabss2 ⊢ ( ℙ ⊆ ℕ → { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐵 } ⊆ { 𝑝 ∈ ℕ ∣ 𝑝 ∥ 𝐵 } )
40 38 39 ax-mp ⊢ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐵 } ⊆ { 𝑝 ∈ ℕ ∣ 𝑝 ∥ 𝐵 }
41 dvdsssfz1 ⊢ ( 𝐵 ∈ ℕ → { 𝑝 ∈ ℕ ∣ 𝑝 ∥ 𝐵 } ⊆ ( 1 ... 𝐵 ) )
42 30 41 syl ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ ( 𝐴 gcd 𝐵 ) = 1 ) ∧ ( ( μ ‘ 𝐴 ) ≠ 0 ∧ ( μ ‘ 𝐵 ) ≠ 0 ) ) → { 𝑝 ∈ ℕ ∣ 𝑝 ∥ 𝐵 } ⊆ ( 1 ... 𝐵 ) )
43 40 42 sstrid ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ ( 𝐴 gcd 𝐵 ) = 1 ) ∧ ( ( μ ‘ 𝐴 ) ≠ 0 ∧ ( μ ‘ 𝐵 ) ≠ 0 ) ) → { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐵 } ⊆ ( 1 ... 𝐵 ) )
44 ssfi ⊢ ( ( ( 1 ... 𝐵 ) ∈ Fin ∧ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐵 } ⊆ ( 1 ... 𝐵 ) ) → { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐵 } ∈ Fin )
45 37 43 44 sylancr ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ ( 𝐴 gcd 𝐵 ) = 1 ) ∧ ( ( μ ‘ 𝐴 ) ≠ 0 ∧ ( μ ‘ 𝐵 ) ≠ 0 ) ) → { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐵 } ∈ Fin )
46 hashcl ⊢ ( { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐵 } ∈ Fin → ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐵 } ) ∈ ℕ0 )
47 45 46 syl ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ ( 𝐴 gcd 𝐵 ) = 1 ) ∧ ( ( μ ‘ 𝐴 ) ≠ 0 ∧ ( μ ‘ 𝐵 ) ≠ 0 ) ) → ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐵 } ) ∈ ℕ0 )
48 fzfi ⊢ ( 1 ... 𝐴 ) ∈ Fin
49 rabss2 ⊢ ( ℙ ⊆ ℕ → { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ⊆ { 𝑝 ∈ ℕ ∣ 𝑝 ∥ 𝐴 } )
50 38 49 ax-mp ⊢ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ⊆ { 𝑝 ∈ ℕ ∣ 𝑝 ∥ 𝐴 }
51 dvdsssfz1 ⊢ ( 𝐴 ∈ ℕ → { 𝑝 ∈ ℕ ∣ 𝑝 ∥ 𝐴 } ⊆ ( 1 ... 𝐴 ) )
52 29 51 syl ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ ( 𝐴 gcd 𝐵 ) = 1 ) ∧ ( ( μ ‘ 𝐴 ) ≠ 0 ∧ ( μ ‘ 𝐵 ) ≠ 0 ) ) → { 𝑝 ∈ ℕ ∣ 𝑝 ∥ 𝐴 } ⊆ ( 1 ... 𝐴 ) )
53 50 52 sstrid ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ ( 𝐴 gcd 𝐵 ) = 1 ) ∧ ( ( μ ‘ 𝐴 ) ≠ 0 ∧ ( μ ‘ 𝐵 ) ≠ 0 ) ) → { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ⊆ ( 1 ... 𝐴 ) )
54 ssfi ⊢ ( ( ( 1 ... 𝐴 ) ∈ Fin ∧ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ⊆ ( 1 ... 𝐴 ) ) → { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ∈ Fin )
55 48 53 54 sylancr ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ ( 𝐴 gcd 𝐵 ) = 1 ) ∧ ( ( μ ‘ 𝐴 ) ≠ 0 ∧ ( μ ‘ 𝐵 ) ≠ 0 ) ) → { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ∈ Fin )
56 hashcl ⊢ ( { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ∈ Fin → ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ) ∈ ℕ0 )
57 55 56 syl ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ ( 𝐴 gcd 𝐵 ) = 1 ) ∧ ( ( μ ‘ 𝐴 ) ≠ 0 ∧ ( μ ‘ 𝐵 ) ≠ 0 ) ) → ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ) ∈ ℕ0 )
58 36 47 57 expaddd ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ ( 𝐴 gcd 𝐵 ) = 1 ) ∧ ( ( μ ‘ 𝐴 ) ≠ 0 ∧ ( μ ‘ 𝐵 ) ≠ 0 ) ) → ( - 1 ↑ ( ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ) + ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐵 } ) ) ) = ( ( - 1 ↑ ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ) ) · ( - 1 ↑ ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐵 } ) ) ) )
59 simpr ⊢ ( ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ ( 𝐴 gcd 𝐵 ) = 1 ) ∧ ( ( μ ‘ 𝐴 ) ≠ 0 ∧ ( μ ‘ 𝐵 ) ≠ 0 ) ) ∧ 𝑝 ∈ ℙ ) → 𝑝 ∈ ℙ )
60 simpl1 ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ ( 𝐴 gcd 𝐵 ) = 1 ) ∧ 𝑝 ∈ ℙ ) → 𝐴 ∈ ℕ )
61 60 nnzd ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ ( 𝐴 gcd 𝐵 ) = 1 ) ∧ 𝑝 ∈ ℙ ) → 𝐴 ∈ ℤ )
62 61 adantlr ⊢ ( ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ ( 𝐴 gcd 𝐵 ) = 1 ) ∧ ( ( μ ‘ 𝐴 ) ≠ 0 ∧ ( μ ‘ 𝐵 ) ≠ 0 ) ) ∧ 𝑝 ∈ ℙ ) → 𝐴 ∈ ℤ )
63 simpl2 ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ ( 𝐴 gcd 𝐵 ) = 1 ) ∧ 𝑝 ∈ ℙ ) → 𝐵 ∈ ℕ )
64 63 nnzd ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ ( 𝐴 gcd 𝐵 ) = 1 ) ∧ 𝑝 ∈ ℙ ) → 𝐵 ∈ ℤ )
65 64 adantlr ⊢ ( ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ ( 𝐴 gcd 𝐵 ) = 1 ) ∧ ( ( μ ‘ 𝐴 ) ≠ 0 ∧ ( μ ‘ 𝐵 ) ≠ 0 ) ) ∧ 𝑝 ∈ ℙ ) → 𝐵 ∈ ℤ )
66 euclemma ⊢ ( ( 𝑝 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( 𝑝 ∥ ( 𝐴 · 𝐵 ) ↔ ( 𝑝 ∥ 𝐴 ∨ 𝑝 ∥ 𝐵 ) ) )
67 59 62 65 66 syl3anc ⊢ ( ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ ( 𝐴 gcd 𝐵 ) = 1 ) ∧ ( ( μ ‘ 𝐴 ) ≠ 0 ∧ ( μ ‘ 𝐵 ) ≠ 0 ) ) ∧ 𝑝 ∈ ℙ ) → ( 𝑝 ∥ ( 𝐴 · 𝐵 ) ↔ ( 𝑝 ∥ 𝐴 ∨ 𝑝 ∥ 𝐵 ) ) )
68 67 rabbidva ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ ( 𝐴 gcd 𝐵 ) = 1 ) ∧ ( ( μ ‘ 𝐴 ) ≠ 0 ∧ ( μ ‘ 𝐵 ) ≠ 0 ) ) → { 𝑝 ∈ ℙ ∣ 𝑝 ∥ ( 𝐴 · 𝐵 ) } = { 𝑝 ∈ ℙ ∣ ( 𝑝 ∥ 𝐴 ∨ 𝑝 ∥ 𝐵 ) } )
69 unrab ⊢ ( { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ∪ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐵 } ) = { 𝑝 ∈ ℙ ∣ ( 𝑝 ∥ 𝐴 ∨ 𝑝 ∥ 𝐵 ) }
70 68 69 eqtr4di ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ ( 𝐴 gcd 𝐵 ) = 1 ) ∧ ( ( μ ‘ 𝐴 ) ≠ 0 ∧ ( μ ‘ 𝐵 ) ≠ 0 ) ) → { 𝑝 ∈ ℙ ∣ 𝑝 ∥ ( 𝐴 · 𝐵 ) } = ( { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ∪ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐵 } ) )
71 70 fveq2d ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ ( 𝐴 gcd 𝐵 ) = 1 ) ∧ ( ( μ ‘ 𝐴 ) ≠ 0 ∧ ( μ ‘ 𝐵 ) ≠ 0 ) ) → ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ ( 𝐴 · 𝐵 ) } ) = ( ♯ ‘ ( { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ∪ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐵 } ) ) )
72 inrab ⊢ ( { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ∩ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐵 } ) = { 𝑝 ∈ ℙ ∣ ( 𝑝 ∥ 𝐴 ∧ 𝑝 ∥ 𝐵 ) }
73 nprmdvds1 ⊢ ( 𝑝 ∈ ℙ → ¬ 𝑝 ∥ 1 )
74 73 adantl ⊢ ( ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ ( 𝐴 gcd 𝐵 ) = 1 ) ∧ ( ( μ ‘ 𝐴 ) ≠ 0 ∧ ( μ ‘ 𝐵 ) ≠ 0 ) ) ∧ 𝑝 ∈ ℙ ) → ¬ 𝑝 ∥ 1 )
75 prmz ⊢ ( 𝑝 ∈ ℙ → 𝑝 ∈ ℤ )
76 75 adantl ⊢ ( ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ ( 𝐴 gcd 𝐵 ) = 1 ) ∧ ( ( μ ‘ 𝐴 ) ≠ 0 ∧ ( μ ‘ 𝐵 ) ≠ 0 ) ) ∧ 𝑝 ∈ ℙ ) → 𝑝 ∈ ℤ )
77 dvdsgcd ⊢ ( ( 𝑝 ∈ ℤ ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( ( 𝑝 ∥ 𝐴 ∧ 𝑝 ∥ 𝐵 ) → 𝑝 ∥ ( 𝐴 gcd 𝐵 ) ) )
78 76 62 65 77 syl3anc ⊢ ( ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ ( 𝐴 gcd 𝐵 ) = 1 ) ∧ ( ( μ ‘ 𝐴 ) ≠ 0 ∧ ( μ ‘ 𝐵 ) ≠ 0 ) ) ∧ 𝑝 ∈ ℙ ) → ( ( 𝑝 ∥ 𝐴 ∧ 𝑝 ∥ 𝐵 ) → 𝑝 ∥ ( 𝐴 gcd 𝐵 ) ) )
79 simpll3 ⊢ ( ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ ( 𝐴 gcd 𝐵 ) = 1 ) ∧ ( ( μ ‘ 𝐴 ) ≠ 0 ∧ ( μ ‘ 𝐵 ) ≠ 0 ) ) ∧ 𝑝 ∈ ℙ ) → ( 𝐴 gcd 𝐵 ) = 1 )
80 79 breq2d ⊢ ( ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ ( 𝐴 gcd 𝐵 ) = 1 ) ∧ ( ( μ ‘ 𝐴 ) ≠ 0 ∧ ( μ ‘ 𝐵 ) ≠ 0 ) ) ∧ 𝑝 ∈ ℙ ) → ( 𝑝 ∥ ( 𝐴 gcd 𝐵 ) ↔ 𝑝 ∥ 1 ) )
81 78 80 sylibd ⊢ ( ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ ( 𝐴 gcd 𝐵 ) = 1 ) ∧ ( ( μ ‘ 𝐴 ) ≠ 0 ∧ ( μ ‘ 𝐵 ) ≠ 0 ) ) ∧ 𝑝 ∈ ℙ ) → ( ( 𝑝 ∥ 𝐴 ∧ 𝑝 ∥ 𝐵 ) → 𝑝 ∥ 1 ) )
82 74 81 mtod ⊢ ( ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ ( 𝐴 gcd 𝐵 ) = 1 ) ∧ ( ( μ ‘ 𝐴 ) ≠ 0 ∧ ( μ ‘ 𝐵 ) ≠ 0 ) ) ∧ 𝑝 ∈ ℙ ) → ¬ ( 𝑝 ∥ 𝐴 ∧ 𝑝 ∥ 𝐵 ) )
83 82 ralrimiva ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ ( 𝐴 gcd 𝐵 ) = 1 ) ∧ ( ( μ ‘ 𝐴 ) ≠ 0 ∧ ( μ ‘ 𝐵 ) ≠ 0 ) ) → ∀ 𝑝 ∈ ℙ ¬ ( 𝑝 ∥ 𝐴 ∧ 𝑝 ∥ 𝐵 ) )
84 rabeq0 ⊢ ( { 𝑝 ∈ ℙ ∣ ( 𝑝 ∥ 𝐴 ∧ 𝑝 ∥ 𝐵 ) } = ∅ ↔ ∀ 𝑝 ∈ ℙ ¬ ( 𝑝 ∥ 𝐴 ∧ 𝑝 ∥ 𝐵 ) )
85 83 84 sylibr ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ ( 𝐴 gcd 𝐵 ) = 1 ) ∧ ( ( μ ‘ 𝐴 ) ≠ 0 ∧ ( μ ‘ 𝐵 ) ≠ 0 ) ) → { 𝑝 ∈ ℙ ∣ ( 𝑝 ∥ 𝐴 ∧ 𝑝 ∥ 𝐵 ) } = ∅ )
86 72 85 eqtrid ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ ( 𝐴 gcd 𝐵 ) = 1 ) ∧ ( ( μ ‘ 𝐴 ) ≠ 0 ∧ ( μ ‘ 𝐵 ) ≠ 0 ) ) → ( { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ∩ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐵 } ) = ∅ )
87 hashun ⊢ ( ( { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ∈ Fin ∧ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐵 } ∈ Fin ∧ ( { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ∩ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐵 } ) = ∅ ) → ( ♯ ‘ ( { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ∪ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐵 } ) ) = ( ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ) + ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐵 } ) ) )
88 55 45 86 87 syl3anc ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ ( 𝐴 gcd 𝐵 ) = 1 ) ∧ ( ( μ ‘ 𝐴 ) ≠ 0 ∧ ( μ ‘ 𝐵 ) ≠ 0 ) ) → ( ♯ ‘ ( { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ∪ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐵 } ) ) = ( ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ) + ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐵 } ) ) )
89 71 88 eqtrd ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ ( 𝐴 gcd 𝐵 ) = 1 ) ∧ ( ( μ ‘ 𝐴 ) ≠ 0 ∧ ( μ ‘ 𝐵 ) ≠ 0 ) ) → ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ ( 𝐴 · 𝐵 ) } ) = ( ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ) + ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐵 } ) ) )
90 89 oveq2d ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ ( 𝐴 gcd 𝐵 ) = 1 ) ∧ ( ( μ ‘ 𝐴 ) ≠ 0 ∧ ( μ ‘ 𝐵 ) ≠ 0 ) ) → ( - 1 ↑ ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ ( 𝐴 · 𝐵 ) } ) ) = ( - 1 ↑ ( ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ) + ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐵 } ) ) ) )
91 simprl ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ ( 𝐴 gcd 𝐵 ) = 1 ) ∧ ( ( μ ‘ 𝐴 ) ≠ 0 ∧ ( μ ‘ 𝐵 ) ≠ 0 ) ) → ( μ ‘ 𝐴 ) ≠ 0 )
92 muval2 ⊢ ( ( 𝐴 ∈ ℕ ∧ ( μ ‘ 𝐴 ) ≠ 0 ) → ( μ ‘ 𝐴 ) = ( - 1 ↑ ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ) ) )
93 29 91 92 syl2anc ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ ( 𝐴 gcd 𝐵 ) = 1 ) ∧ ( ( μ ‘ 𝐴 ) ≠ 0 ∧ ( μ ‘ 𝐵 ) ≠ 0 ) ) → ( μ ‘ 𝐴 ) = ( - 1 ↑ ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ) ) )
94 simprr ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ ( 𝐴 gcd 𝐵 ) = 1 ) ∧ ( ( μ ‘ 𝐴 ) ≠ 0 ∧ ( μ ‘ 𝐵 ) ≠ 0 ) ) → ( μ ‘ 𝐵 ) ≠ 0 )
95 muval2 ⊢ ( ( 𝐵 ∈ ℕ ∧ ( μ ‘ 𝐵 ) ≠ 0 ) → ( μ ‘ 𝐵 ) = ( - 1 ↑ ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐵 } ) ) )
96 30 94 95 syl2anc ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ ( 𝐴 gcd 𝐵 ) = 1 ) ∧ ( ( μ ‘ 𝐴 ) ≠ 0 ∧ ( μ ‘ 𝐵 ) ≠ 0 ) ) → ( μ ‘ 𝐵 ) = ( - 1 ↑ ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐵 } ) ) )
97 93 96 oveq12d ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ ( 𝐴 gcd 𝐵 ) = 1 ) ∧ ( ( μ ‘ 𝐴 ) ≠ 0 ∧ ( μ ‘ 𝐵 ) ≠ 0 ) ) → ( ( μ ‘ 𝐴 ) · ( μ ‘ 𝐵 ) ) = ( ( - 1 ↑ ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ) ) · ( - 1 ↑ ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐵 } ) ) ) )
98 58 90 97 3eqtr4rd ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ ( 𝐴 gcd 𝐵 ) = 1 ) ∧ ( ( μ ‘ 𝐴 ) ≠ 0 ∧ ( μ ‘ 𝐵 ) ≠ 0 ) ) → ( ( μ ‘ 𝐴 ) · ( μ ‘ 𝐵 ) ) = ( - 1 ↑ ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ ( 𝐴 · 𝐵 ) } ) ) )
99 34 98 eqtr4d ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ ( 𝐴 gcd 𝐵 ) = 1 ) ∧ ( ( μ ‘ 𝐴 ) ≠ 0 ∧ ( μ ‘ 𝐵 ) ≠ 0 ) ) → ( μ ‘ ( 𝐴 · 𝐵 ) ) = ( ( μ ‘ 𝐴 ) · ( μ ‘ 𝐵 ) ) )
100 10 28 99 pm2.61da2ne ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ ( 𝐴 gcd 𝐵 ) = 1 ) → ( μ ‘ ( 𝐴 · 𝐵 ) ) = ( ( μ ‘ 𝐴 ) · ( μ ‘ 𝐵 ) ) )