| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | simpl2 1193 | . . . . . 6
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ (𝐴 gcd 𝐵) = 1) ∧ (μ‘𝐴) = 0) → 𝐵 ∈ ℕ) | 
| 2 |  | mucl 27184 | . . . . . 6
⊢ (𝐵 ∈ ℕ →
(μ‘𝐵) ∈
ℤ) | 
| 3 | 1, 2 | syl 17 | . . . . 5
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ (𝐴 gcd 𝐵) = 1) ∧ (μ‘𝐴) = 0) → (μ‘𝐵) ∈ ℤ) | 
| 4 | 3 | zcnd 12723 | . . . 4
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ (𝐴 gcd 𝐵) = 1) ∧ (μ‘𝐴) = 0) → (μ‘𝐵) ∈ ℂ) | 
| 5 | 4 | mul02d 11459 | . . 3
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ (𝐴 gcd 𝐵) = 1) ∧ (μ‘𝐴) = 0) → (0 · (μ‘𝐵)) = 0) | 
| 6 |  | simpr 484 | . . . 4
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ (𝐴 gcd 𝐵) = 1) ∧ (μ‘𝐴) = 0) → (μ‘𝐴) = 0) | 
| 7 | 6 | oveq1d 7446 | . . 3
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ (𝐴 gcd 𝐵) = 1) ∧ (μ‘𝐴) = 0) → ((μ‘𝐴) · (μ‘𝐵)) = (0 · (μ‘𝐵))) | 
| 8 |  | mumullem1 27222 | . . . 4
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧
(μ‘𝐴) = 0) →
(μ‘(𝐴 ·
𝐵)) = 0) | 
| 9 | 8 | 3adantl3 1169 | . . 3
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ (𝐴 gcd 𝐵) = 1) ∧ (μ‘𝐴) = 0) → (μ‘(𝐴 · 𝐵)) = 0) | 
| 10 | 5, 7, 9 | 3eqtr4rd 2788 | . 2
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ (𝐴 gcd 𝐵) = 1) ∧ (μ‘𝐴) = 0) → (μ‘(𝐴 · 𝐵)) = ((μ‘𝐴) · (μ‘𝐵))) | 
| 11 |  | simpl1 1192 | . . . . . 6
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ (𝐴 gcd 𝐵) = 1) ∧ (μ‘𝐵) = 0) → 𝐴 ∈ ℕ) | 
| 12 |  | mucl 27184 | . . . . . 6
⊢ (𝐴 ∈ ℕ →
(μ‘𝐴) ∈
ℤ) | 
| 13 | 11, 12 | syl 17 | . . . . 5
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ (𝐴 gcd 𝐵) = 1) ∧ (μ‘𝐵) = 0) → (μ‘𝐴) ∈ ℤ) | 
| 14 | 13 | zcnd 12723 | . . . 4
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ (𝐴 gcd 𝐵) = 1) ∧ (μ‘𝐵) = 0) → (μ‘𝐴) ∈ ℂ) | 
| 15 | 14 | mul01d 11460 | . . 3
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ (𝐴 gcd 𝐵) = 1) ∧ (μ‘𝐵) = 0) → ((μ‘𝐴) · 0) = 0) | 
| 16 |  | simpr 484 | . . . 4
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ (𝐴 gcd 𝐵) = 1) ∧ (μ‘𝐵) = 0) → (μ‘𝐵) = 0) | 
| 17 | 16 | oveq2d 7447 | . . 3
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ (𝐴 gcd 𝐵) = 1) ∧ (μ‘𝐵) = 0) → ((μ‘𝐴) · (μ‘𝐵)) = ((μ‘𝐴) · 0)) | 
| 18 |  | nncn 12274 | . . . . . . . 8
⊢ (𝐴 ∈ ℕ → 𝐴 ∈
ℂ) | 
| 19 |  | nncn 12274 | . . . . . . . 8
⊢ (𝐵 ∈ ℕ → 𝐵 ∈
ℂ) | 
| 20 |  | mulcom 11241 | . . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) = (𝐵 · 𝐴)) | 
| 21 | 18, 19, 20 | syl2an 596 | . . . . . . 7
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (𝐴 · 𝐵) = (𝐵 · 𝐴)) | 
| 22 | 21 | fveq2d 6910 | . . . . . 6
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) →
(μ‘(𝐴 ·
𝐵)) = (μ‘(𝐵 · 𝐴))) | 
| 23 | 22 | adantr 480 | . . . . 5
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧
(μ‘𝐵) = 0) →
(μ‘(𝐴 ·
𝐵)) = (μ‘(𝐵 · 𝐴))) | 
| 24 |  | mumullem1 27222 | . . . . . 6
⊢ (((𝐵 ∈ ℕ ∧ 𝐴 ∈ ℕ) ∧
(μ‘𝐵) = 0) →
(μ‘(𝐵 ·
𝐴)) = 0) | 
| 25 | 24 | ancom1s 653 | . . . . 5
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧
(μ‘𝐵) = 0) →
(μ‘(𝐵 ·
𝐴)) = 0) | 
| 26 | 23, 25 | eqtrd 2777 | . . . 4
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧
(μ‘𝐵) = 0) →
(μ‘(𝐴 ·
𝐵)) = 0) | 
| 27 | 26 | 3adantl3 1169 | . . 3
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ (𝐴 gcd 𝐵) = 1) ∧ (μ‘𝐵) = 0) → (μ‘(𝐴 · 𝐵)) = 0) | 
| 28 | 15, 17, 27 | 3eqtr4rd 2788 | . 2
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ (𝐴 gcd 𝐵) = 1) ∧ (μ‘𝐵) = 0) → (μ‘(𝐴 · 𝐵)) = ((μ‘𝐴) · (μ‘𝐵))) | 
| 29 |  | simpl1 1192 | . . . . 5
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ (𝐴 gcd 𝐵) = 1) ∧ ((μ‘𝐴) ≠ 0 ∧ (μ‘𝐵) ≠ 0)) → 𝐴 ∈ ℕ) | 
| 30 |  | simpl2 1193 | . . . . 5
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ (𝐴 gcd 𝐵) = 1) ∧ ((μ‘𝐴) ≠ 0 ∧ (μ‘𝐵) ≠ 0)) → 𝐵 ∈ ℕ) | 
| 31 | 29, 30 | nnmulcld 12319 | . . . 4
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ (𝐴 gcd 𝐵) = 1) ∧ ((μ‘𝐴) ≠ 0 ∧ (μ‘𝐵) ≠ 0)) → (𝐴 · 𝐵) ∈ ℕ) | 
| 32 |  | mumullem2 27223 | . . . 4
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ (𝐴 gcd 𝐵) = 1) ∧ ((μ‘𝐴) ≠ 0 ∧ (μ‘𝐵) ≠ 0)) → (μ‘(𝐴 · 𝐵)) ≠ 0) | 
| 33 |  | muval2 27177 | . . . 4
⊢ (((𝐴 · 𝐵) ∈ ℕ ∧ (μ‘(𝐴 · 𝐵)) ≠ 0) → (μ‘(𝐴 · 𝐵)) = (-1↑(♯‘{𝑝 ∈ ℙ ∣ 𝑝 ∥ (𝐴 · 𝐵)}))) | 
| 34 | 31, 32, 33 | syl2anc 584 | . . 3
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ (𝐴 gcd 𝐵) = 1) ∧ ((μ‘𝐴) ≠ 0 ∧ (μ‘𝐵) ≠ 0)) → (μ‘(𝐴 · 𝐵)) = (-1↑(♯‘{𝑝 ∈ ℙ ∣ 𝑝 ∥ (𝐴 · 𝐵)}))) | 
| 35 |  | neg1cn 12380 | . . . . . 6
⊢ -1 ∈
ℂ | 
| 36 | 35 | a1i 11 | . . . . 5
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ (𝐴 gcd 𝐵) = 1) ∧ ((μ‘𝐴) ≠ 0 ∧ (μ‘𝐵) ≠ 0)) → -1 ∈
ℂ) | 
| 37 |  | fzfi 14013 | . . . . . . 7
⊢
(1...𝐵) ∈
Fin | 
| 38 |  | prmssnn 16713 | . . . . . . . . 9
⊢ ℙ
⊆ ℕ | 
| 39 |  | rabss2 4078 | . . . . . . . . 9
⊢ (ℙ
⊆ ℕ → {𝑝
∈ ℙ ∣ 𝑝
∥ 𝐵} ⊆ {𝑝 ∈ ℕ ∣ 𝑝 ∥ 𝐵}) | 
| 40 | 38, 39 | ax-mp 5 | . . . . . . . 8
⊢ {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐵} ⊆ {𝑝 ∈ ℕ ∣ 𝑝 ∥ 𝐵} | 
| 41 |  | dvdsssfz1 16355 | . . . . . . . . 9
⊢ (𝐵 ∈ ℕ → {𝑝 ∈ ℕ ∣ 𝑝 ∥ 𝐵} ⊆ (1...𝐵)) | 
| 42 | 30, 41 | syl 17 | . . . . . . . 8
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ (𝐴 gcd 𝐵) = 1) ∧ ((μ‘𝐴) ≠ 0 ∧ (μ‘𝐵) ≠ 0)) → {𝑝 ∈ ℕ ∣ 𝑝 ∥ 𝐵} ⊆ (1...𝐵)) | 
| 43 | 40, 42 | sstrid 3995 | . . . . . . 7
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ (𝐴 gcd 𝐵) = 1) ∧ ((μ‘𝐴) ≠ 0 ∧ (μ‘𝐵) ≠ 0)) → {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐵} ⊆ (1...𝐵)) | 
| 44 |  | ssfi 9213 | . . . . . . 7
⊢
(((1...𝐵) ∈ Fin
∧ {𝑝 ∈ ℙ
∣ 𝑝 ∥ 𝐵} ⊆ (1...𝐵)) → {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐵} ∈ Fin) | 
| 45 | 37, 43, 44 | sylancr 587 | . . . . . 6
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ (𝐴 gcd 𝐵) = 1) ∧ ((μ‘𝐴) ≠ 0 ∧ (μ‘𝐵) ≠ 0)) → {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐵} ∈ Fin) | 
| 46 |  | hashcl 14395 | . . . . . 6
⊢ ({𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐵} ∈ Fin → (♯‘{𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐵}) ∈
ℕ0) | 
| 47 | 45, 46 | syl 17 | . . . . 5
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ (𝐴 gcd 𝐵) = 1) ∧ ((μ‘𝐴) ≠ 0 ∧ (μ‘𝐵) ≠ 0)) → (♯‘{𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐵}) ∈
ℕ0) | 
| 48 |  | fzfi 14013 | . . . . . . 7
⊢
(1...𝐴) ∈
Fin | 
| 49 |  | rabss2 4078 | . . . . . . . . 9
⊢ (ℙ
⊆ ℕ → {𝑝
∈ ℙ ∣ 𝑝
∥ 𝐴} ⊆ {𝑝 ∈ ℕ ∣ 𝑝 ∥ 𝐴}) | 
| 50 | 38, 49 | ax-mp 5 | . . . . . . . 8
⊢ {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴} ⊆ {𝑝 ∈ ℕ ∣ 𝑝 ∥ 𝐴} | 
| 51 |  | dvdsssfz1 16355 | . . . . . . . . 9
⊢ (𝐴 ∈ ℕ → {𝑝 ∈ ℕ ∣ 𝑝 ∥ 𝐴} ⊆ (1...𝐴)) | 
| 52 | 29, 51 | syl 17 | . . . . . . . 8
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ (𝐴 gcd 𝐵) = 1) ∧ ((μ‘𝐴) ≠ 0 ∧ (μ‘𝐵) ≠ 0)) → {𝑝 ∈ ℕ ∣ 𝑝 ∥ 𝐴} ⊆ (1...𝐴)) | 
| 53 | 50, 52 | sstrid 3995 | . . . . . . 7
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ (𝐴 gcd 𝐵) = 1) ∧ ((μ‘𝐴) ≠ 0 ∧ (μ‘𝐵) ≠ 0)) → {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴} ⊆ (1...𝐴)) | 
| 54 |  | ssfi 9213 | . . . . . . 7
⊢
(((1...𝐴) ∈ Fin
∧ {𝑝 ∈ ℙ
∣ 𝑝 ∥ 𝐴} ⊆ (1...𝐴)) → {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴} ∈ Fin) | 
| 55 | 48, 53, 54 | sylancr 587 | . . . . . 6
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ (𝐴 gcd 𝐵) = 1) ∧ ((μ‘𝐴) ≠ 0 ∧ (μ‘𝐵) ≠ 0)) → {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴} ∈ Fin) | 
| 56 |  | hashcl 14395 | . . . . . 6
⊢ ({𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴} ∈ Fin → (♯‘{𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴}) ∈
ℕ0) | 
| 57 | 55, 56 | syl 17 | . . . . 5
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ (𝐴 gcd 𝐵) = 1) ∧ ((μ‘𝐴) ≠ 0 ∧ (μ‘𝐵) ≠ 0)) → (♯‘{𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴}) ∈
ℕ0) | 
| 58 | 36, 47, 57 | expaddd 14188 | . . . 4
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ (𝐴 gcd 𝐵) = 1) ∧ ((μ‘𝐴) ≠ 0 ∧ (μ‘𝐵) ≠ 0)) →
(-1↑((♯‘{𝑝
∈ ℙ ∣ 𝑝
∥ 𝐴}) +
(♯‘{𝑝 ∈
ℙ ∣ 𝑝 ∥
𝐵}))) =
((-1↑(♯‘{𝑝
∈ ℙ ∣ 𝑝
∥ 𝐴})) ·
(-1↑(♯‘{𝑝
∈ ℙ ∣ 𝑝
∥ 𝐵})))) | 
| 59 |  | simpr 484 | . . . . . . . . . 10
⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ (𝐴 gcd 𝐵) = 1) ∧ ((μ‘𝐴) ≠ 0 ∧ (μ‘𝐵) ≠ 0)) ∧ 𝑝 ∈ ℙ) → 𝑝 ∈ ℙ) | 
| 60 |  | simpl1 1192 | . . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ (𝐴 gcd 𝐵) = 1) ∧ 𝑝 ∈ ℙ) → 𝐴 ∈ ℕ) | 
| 61 | 60 | nnzd 12640 | . . . . . . . . . . 11
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ (𝐴 gcd 𝐵) = 1) ∧ 𝑝 ∈ ℙ) → 𝐴 ∈ ℤ) | 
| 62 | 61 | adantlr 715 | . . . . . . . . . 10
⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ (𝐴 gcd 𝐵) = 1) ∧ ((μ‘𝐴) ≠ 0 ∧ (μ‘𝐵) ≠ 0)) ∧ 𝑝 ∈ ℙ) → 𝐴 ∈ ℤ) | 
| 63 |  | simpl2 1193 | . . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ (𝐴 gcd 𝐵) = 1) ∧ 𝑝 ∈ ℙ) → 𝐵 ∈ ℕ) | 
| 64 | 63 | nnzd 12640 | . . . . . . . . . . 11
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ (𝐴 gcd 𝐵) = 1) ∧ 𝑝 ∈ ℙ) → 𝐵 ∈ ℤ) | 
| 65 | 64 | adantlr 715 | . . . . . . . . . 10
⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ (𝐴 gcd 𝐵) = 1) ∧ ((μ‘𝐴) ≠ 0 ∧ (μ‘𝐵) ≠ 0)) ∧ 𝑝 ∈ ℙ) → 𝐵 ∈ ℤ) | 
| 66 |  | euclemma 16750 | . . . . . . . . . 10
⊢ ((𝑝 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝑝 ∥ (𝐴 · 𝐵) ↔ (𝑝 ∥ 𝐴 ∨ 𝑝 ∥ 𝐵))) | 
| 67 | 59, 62, 65, 66 | syl3anc 1373 | . . . . . . . . 9
⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ (𝐴 gcd 𝐵) = 1) ∧ ((μ‘𝐴) ≠ 0 ∧ (μ‘𝐵) ≠ 0)) ∧ 𝑝 ∈ ℙ) → (𝑝 ∥ (𝐴 · 𝐵) ↔ (𝑝 ∥ 𝐴 ∨ 𝑝 ∥ 𝐵))) | 
| 68 | 67 | rabbidva 3443 | . . . . . . . 8
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ (𝐴 gcd 𝐵) = 1) ∧ ((μ‘𝐴) ≠ 0 ∧ (μ‘𝐵) ≠ 0)) → {𝑝 ∈ ℙ ∣ 𝑝 ∥ (𝐴 · 𝐵)} = {𝑝 ∈ ℙ ∣ (𝑝 ∥ 𝐴 ∨ 𝑝 ∥ 𝐵)}) | 
| 69 |  | unrab 4315 | . . . . . . . 8
⊢ ({𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴} ∪ {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐵}) = {𝑝 ∈ ℙ ∣ (𝑝 ∥ 𝐴 ∨ 𝑝 ∥ 𝐵)} | 
| 70 | 68, 69 | eqtr4di 2795 | . . . . . . 7
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ (𝐴 gcd 𝐵) = 1) ∧ ((μ‘𝐴) ≠ 0 ∧ (μ‘𝐵) ≠ 0)) → {𝑝 ∈ ℙ ∣ 𝑝 ∥ (𝐴 · 𝐵)} = ({𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴} ∪ {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐵})) | 
| 71 | 70 | fveq2d 6910 | . . . . . 6
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ (𝐴 gcd 𝐵) = 1) ∧ ((μ‘𝐴) ≠ 0 ∧ (μ‘𝐵) ≠ 0)) → (♯‘{𝑝 ∈ ℙ ∣ 𝑝 ∥ (𝐴 · 𝐵)}) = (♯‘({𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴} ∪ {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐵}))) | 
| 72 |  | inrab 4316 | . . . . . . . 8
⊢ ({𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴} ∩ {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐵}) = {𝑝 ∈ ℙ ∣ (𝑝 ∥ 𝐴 ∧ 𝑝 ∥ 𝐵)} | 
| 73 |  | nprmdvds1 16743 | . . . . . . . . . . . 12
⊢ (𝑝 ∈ ℙ → ¬
𝑝 ∥
1) | 
| 74 | 73 | adantl 481 | . . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ (𝐴 gcd 𝐵) = 1) ∧ ((μ‘𝐴) ≠ 0 ∧ (μ‘𝐵) ≠ 0)) ∧ 𝑝 ∈ ℙ) → ¬ 𝑝 ∥ 1) | 
| 75 |  | prmz 16712 | . . . . . . . . . . . . . 14
⊢ (𝑝 ∈ ℙ → 𝑝 ∈
ℤ) | 
| 76 | 75 | adantl 481 | . . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ (𝐴 gcd 𝐵) = 1) ∧ ((μ‘𝐴) ≠ 0 ∧ (μ‘𝐵) ≠ 0)) ∧ 𝑝 ∈ ℙ) → 𝑝 ∈ ℤ) | 
| 77 |  | dvdsgcd 16581 | . . . . . . . . . . . . 13
⊢ ((𝑝 ∈ ℤ ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → ((𝑝 ∥ 𝐴 ∧ 𝑝 ∥ 𝐵) → 𝑝 ∥ (𝐴 gcd 𝐵))) | 
| 78 | 76, 62, 65, 77 | syl3anc 1373 | . . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ (𝐴 gcd 𝐵) = 1) ∧ ((μ‘𝐴) ≠ 0 ∧ (μ‘𝐵) ≠ 0)) ∧ 𝑝 ∈ ℙ) → ((𝑝 ∥ 𝐴 ∧ 𝑝 ∥ 𝐵) → 𝑝 ∥ (𝐴 gcd 𝐵))) | 
| 79 |  | simpll3 1215 | . . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ (𝐴 gcd 𝐵) = 1) ∧ ((μ‘𝐴) ≠ 0 ∧ (μ‘𝐵) ≠ 0)) ∧ 𝑝 ∈ ℙ) → (𝐴 gcd 𝐵) = 1) | 
| 80 | 79 | breq2d 5155 | . . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ (𝐴 gcd 𝐵) = 1) ∧ ((μ‘𝐴) ≠ 0 ∧ (μ‘𝐵) ≠ 0)) ∧ 𝑝 ∈ ℙ) → (𝑝 ∥ (𝐴 gcd 𝐵) ↔ 𝑝 ∥ 1)) | 
| 81 | 78, 80 | sylibd 239 | . . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ (𝐴 gcd 𝐵) = 1) ∧ ((μ‘𝐴) ≠ 0 ∧ (μ‘𝐵) ≠ 0)) ∧ 𝑝 ∈ ℙ) → ((𝑝 ∥ 𝐴 ∧ 𝑝 ∥ 𝐵) → 𝑝 ∥ 1)) | 
| 82 | 74, 81 | mtod 198 | . . . . . . . . . 10
⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ (𝐴 gcd 𝐵) = 1) ∧ ((μ‘𝐴) ≠ 0 ∧ (μ‘𝐵) ≠ 0)) ∧ 𝑝 ∈ ℙ) → ¬ (𝑝 ∥ 𝐴 ∧ 𝑝 ∥ 𝐵)) | 
| 83 | 82 | ralrimiva 3146 | . . . . . . . . 9
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ (𝐴 gcd 𝐵) = 1) ∧ ((μ‘𝐴) ≠ 0 ∧ (μ‘𝐵) ≠ 0)) → ∀𝑝 ∈ ℙ ¬ (𝑝 ∥ 𝐴 ∧ 𝑝 ∥ 𝐵)) | 
| 84 |  | rabeq0 4388 | . . . . . . . . 9
⊢ ({𝑝 ∈ ℙ ∣ (𝑝 ∥ 𝐴 ∧ 𝑝 ∥ 𝐵)} = ∅ ↔ ∀𝑝 ∈ ℙ ¬ (𝑝 ∥ 𝐴 ∧ 𝑝 ∥ 𝐵)) | 
| 85 | 83, 84 | sylibr 234 | . . . . . . . 8
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ (𝐴 gcd 𝐵) = 1) ∧ ((μ‘𝐴) ≠ 0 ∧ (μ‘𝐵) ≠ 0)) → {𝑝 ∈ ℙ ∣ (𝑝 ∥ 𝐴 ∧ 𝑝 ∥ 𝐵)} = ∅) | 
| 86 | 72, 85 | eqtrid 2789 | . . . . . . 7
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ (𝐴 gcd 𝐵) = 1) ∧ ((μ‘𝐴) ≠ 0 ∧ (μ‘𝐵) ≠ 0)) → ({𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴} ∩ {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐵}) = ∅) | 
| 87 |  | hashun 14421 | . . . . . . 7
⊢ (({𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴} ∈ Fin ∧ {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐵} ∈ Fin ∧ ({𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴} ∩ {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐵}) = ∅) → (♯‘({𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴} ∪ {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐵})) = ((♯‘{𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴}) + (♯‘{𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐵}))) | 
| 88 | 55, 45, 86, 87 | syl3anc 1373 | . . . . . 6
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ (𝐴 gcd 𝐵) = 1) ∧ ((μ‘𝐴) ≠ 0 ∧ (μ‘𝐵) ≠ 0)) → (♯‘({𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴} ∪ {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐵})) = ((♯‘{𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴}) + (♯‘{𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐵}))) | 
| 89 | 71, 88 | eqtrd 2777 | . . . . 5
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ (𝐴 gcd 𝐵) = 1) ∧ ((μ‘𝐴) ≠ 0 ∧ (μ‘𝐵) ≠ 0)) → (♯‘{𝑝 ∈ ℙ ∣ 𝑝 ∥ (𝐴 · 𝐵)}) = ((♯‘{𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴}) + (♯‘{𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐵}))) | 
| 90 | 89 | oveq2d 7447 | . . . 4
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ (𝐴 gcd 𝐵) = 1) ∧ ((μ‘𝐴) ≠ 0 ∧ (μ‘𝐵) ≠ 0)) →
(-1↑(♯‘{𝑝
∈ ℙ ∣ 𝑝
∥ (𝐴 · 𝐵)})) =
(-1↑((♯‘{𝑝
∈ ℙ ∣ 𝑝
∥ 𝐴}) +
(♯‘{𝑝 ∈
ℙ ∣ 𝑝 ∥
𝐵})))) | 
| 91 |  | simprl 771 | . . . . . 6
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ (𝐴 gcd 𝐵) = 1) ∧ ((μ‘𝐴) ≠ 0 ∧ (μ‘𝐵) ≠ 0)) → (μ‘𝐴) ≠ 0) | 
| 92 |  | muval2 27177 | . . . . . 6
⊢ ((𝐴 ∈ ℕ ∧
(μ‘𝐴) ≠ 0)
→ (μ‘𝐴) =
(-1↑(♯‘{𝑝
∈ ℙ ∣ 𝑝
∥ 𝐴}))) | 
| 93 | 29, 91, 92 | syl2anc 584 | . . . . 5
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ (𝐴 gcd 𝐵) = 1) ∧ ((μ‘𝐴) ≠ 0 ∧ (μ‘𝐵) ≠ 0)) → (μ‘𝐴) =
(-1↑(♯‘{𝑝
∈ ℙ ∣ 𝑝
∥ 𝐴}))) | 
| 94 |  | simprr 773 | . . . . . 6
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ (𝐴 gcd 𝐵) = 1) ∧ ((μ‘𝐴) ≠ 0 ∧ (μ‘𝐵) ≠ 0)) → (μ‘𝐵) ≠ 0) | 
| 95 |  | muval2 27177 | . . . . . 6
⊢ ((𝐵 ∈ ℕ ∧
(μ‘𝐵) ≠ 0)
→ (μ‘𝐵) =
(-1↑(♯‘{𝑝
∈ ℙ ∣ 𝑝
∥ 𝐵}))) | 
| 96 | 30, 94, 95 | syl2anc 584 | . . . . 5
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ (𝐴 gcd 𝐵) = 1) ∧ ((μ‘𝐴) ≠ 0 ∧ (μ‘𝐵) ≠ 0)) → (μ‘𝐵) =
(-1↑(♯‘{𝑝
∈ ℙ ∣ 𝑝
∥ 𝐵}))) | 
| 97 | 93, 96 | oveq12d 7449 | . . . 4
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ (𝐴 gcd 𝐵) = 1) ∧ ((μ‘𝐴) ≠ 0 ∧ (μ‘𝐵) ≠ 0)) → ((μ‘𝐴) · (μ‘𝐵)) =
((-1↑(♯‘{𝑝
∈ ℙ ∣ 𝑝
∥ 𝐴})) ·
(-1↑(♯‘{𝑝
∈ ℙ ∣ 𝑝
∥ 𝐵})))) | 
| 98 | 58, 90, 97 | 3eqtr4rd 2788 | . . 3
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ (𝐴 gcd 𝐵) = 1) ∧ ((μ‘𝐴) ≠ 0 ∧ (μ‘𝐵) ≠ 0)) → ((μ‘𝐴) · (μ‘𝐵)) =
(-1↑(♯‘{𝑝
∈ ℙ ∣ 𝑝
∥ (𝐴 · 𝐵)}))) | 
| 99 | 34, 98 | eqtr4d 2780 | . 2
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ (𝐴 gcd 𝐵) = 1) ∧ ((μ‘𝐴) ≠ 0 ∧ (μ‘𝐵) ≠ 0)) → (μ‘(𝐴 · 𝐵)) = ((μ‘𝐴) · (μ‘𝐵))) | 
| 100 | 10, 28, 99 | pm2.61da2ne 3030 | 1
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ (𝐴 gcd 𝐵) = 1) → (μ‘(𝐴 · 𝐵)) = ((μ‘𝐴) · (μ‘𝐵))) |