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