| Step | Hyp | Ref
| Expression |
| 1 | | fveq2 6906 |
. . . . . . . 8
⊢ (𝑛 = 𝑘 → (μ‘𝑛) = (μ‘𝑘)) |
| 2 | 1 | neeq1d 3000 |
. . . . . . 7
⊢ (𝑛 = 𝑘 → ((μ‘𝑛) ≠ 0 ↔ (μ‘𝑘) ≠ 0)) |
| 3 | | breq1 5146 |
. . . . . . 7
⊢ (𝑛 = 𝑘 → (𝑛 ∥ 𝑁 ↔ 𝑘 ∥ 𝑁)) |
| 4 | 2, 3 | anbi12d 632 |
. . . . . 6
⊢ (𝑛 = 𝑘 → (((μ‘𝑛) ≠ 0 ∧ 𝑛 ∥ 𝑁) ↔ ((μ‘𝑘) ≠ 0 ∧ 𝑘 ∥ 𝑁))) |
| 5 | 4 | elrab 3692 |
. . . . 5
⊢ (𝑘 ∈ {𝑛 ∈ ℕ ∣ ((μ‘𝑛) ≠ 0 ∧ 𝑛 ∥ 𝑁)} ↔ (𝑘 ∈ ℕ ∧ ((μ‘𝑘) ≠ 0 ∧ 𝑘 ∥ 𝑁))) |
| 6 | | muval2 27177 |
. . . . . 6
⊢ ((𝑘 ∈ ℕ ∧
(μ‘𝑘) ≠ 0)
→ (μ‘𝑘) =
(-1↑(♯‘{𝑝
∈ ℙ ∣ 𝑝
∥ 𝑘}))) |
| 7 | 6 | adantrr 717 |
. . . . 5
⊢ ((𝑘 ∈ ℕ ∧
((μ‘𝑘) ≠ 0
∧ 𝑘 ∥ 𝑁)) → (μ‘𝑘) =
(-1↑(♯‘{𝑝
∈ ℙ ∣ 𝑝
∥ 𝑘}))) |
| 8 | 5, 7 | sylbi 217 |
. . . 4
⊢ (𝑘 ∈ {𝑛 ∈ ℕ ∣ ((μ‘𝑛) ≠ 0 ∧ 𝑛 ∥ 𝑁)} → (μ‘𝑘) = (-1↑(♯‘{𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑘}))) |
| 9 | 8 | adantl 481 |
. . 3
⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ {𝑛 ∈ ℕ ∣ ((μ‘𝑛) ≠ 0 ∧ 𝑛 ∥ 𝑁)}) → (μ‘𝑘) = (-1↑(♯‘{𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑘}))) |
| 10 | 9 | sumeq2dv 15738 |
. 2
⊢ (𝑁 ∈ ℕ →
Σ𝑘 ∈ {𝑛 ∈ ℕ ∣
((μ‘𝑛) ≠ 0
∧ 𝑛 ∥ 𝑁)} (μ‘𝑘) = Σ𝑘 ∈ {𝑛 ∈ ℕ ∣ ((μ‘𝑛) ≠ 0 ∧ 𝑛 ∥ 𝑁)} (-1↑(♯‘{𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑘}))) |
| 11 | | simpr 484 |
. . . . 5
⊢
(((μ‘𝑛)
≠ 0 ∧ 𝑛 ∥
𝑁) → 𝑛 ∥ 𝑁) |
| 12 | 11 | a1i 11 |
. . . 4
⊢ ((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℕ) →
(((μ‘𝑛) ≠ 0
∧ 𝑛 ∥ 𝑁) → 𝑛 ∥ 𝑁)) |
| 13 | 12 | ss2rabdv 4076 |
. . 3
⊢ (𝑁 ∈ ℕ → {𝑛 ∈ ℕ ∣
((μ‘𝑛) ≠ 0
∧ 𝑛 ∥ 𝑁)} ⊆ {𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑁}) |
| 14 | | ssrab2 4080 |
. . . . . 6
⊢ {𝑛 ∈ ℕ ∣
((μ‘𝑛) ≠ 0
∧ 𝑛 ∥ 𝑁)} ⊆
ℕ |
| 15 | | simpr 484 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ {𝑛 ∈ ℕ ∣ ((μ‘𝑛) ≠ 0 ∧ 𝑛 ∥ 𝑁)}) → 𝑘 ∈ {𝑛 ∈ ℕ ∣ ((μ‘𝑛) ≠ 0 ∧ 𝑛 ∥ 𝑁)}) |
| 16 | 14, 15 | sselid 3981 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ {𝑛 ∈ ℕ ∣ ((μ‘𝑛) ≠ 0 ∧ 𝑛 ∥ 𝑁)}) → 𝑘 ∈ ℕ) |
| 17 | | mucl 27184 |
. . . . 5
⊢ (𝑘 ∈ ℕ →
(μ‘𝑘) ∈
ℤ) |
| 18 | 16, 17 | syl 17 |
. . . 4
⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ {𝑛 ∈ ℕ ∣ ((μ‘𝑛) ≠ 0 ∧ 𝑛 ∥ 𝑁)}) → (μ‘𝑘) ∈ ℤ) |
| 19 | 18 | zcnd 12723 |
. . 3
⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ {𝑛 ∈ ℕ ∣ ((μ‘𝑛) ≠ 0 ∧ 𝑛 ∥ 𝑁)}) → (μ‘𝑘) ∈ ℂ) |
| 20 | | difrab 4318 |
. . . . . . 7
⊢ ({𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑁} ∖ {𝑛 ∈ ℕ ∣ ((μ‘𝑛) ≠ 0 ∧ 𝑛 ∥ 𝑁)}) = {𝑛 ∈ ℕ ∣ (𝑛 ∥ 𝑁 ∧ ¬ ((μ‘𝑛) ≠ 0 ∧ 𝑛 ∥ 𝑁))} |
| 21 | | pm3.21 471 |
. . . . . . . . . . 11
⊢ (𝑛 ∥ 𝑁 → ((μ‘𝑛) ≠ 0 → ((μ‘𝑛) ≠ 0 ∧ 𝑛 ∥ 𝑁))) |
| 22 | 21 | necon1bd 2958 |
. . . . . . . . . 10
⊢ (𝑛 ∥ 𝑁 → (¬ ((μ‘𝑛) ≠ 0 ∧ 𝑛 ∥ 𝑁) → (μ‘𝑛) = 0)) |
| 23 | 22 | imp 406 |
. . . . . . . . 9
⊢ ((𝑛 ∥ 𝑁 ∧ ¬ ((μ‘𝑛) ≠ 0 ∧ 𝑛 ∥ 𝑁)) → (μ‘𝑛) = 0) |
| 24 | 23 | a1i 11 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ → ((𝑛 ∥ 𝑁 ∧ ¬ ((μ‘𝑛) ≠ 0 ∧ 𝑛 ∥ 𝑁)) → (μ‘𝑛) = 0)) |
| 25 | 24 | ss2rabi 4077 |
. . . . . . 7
⊢ {𝑛 ∈ ℕ ∣ (𝑛 ∥ 𝑁 ∧ ¬ ((μ‘𝑛) ≠ 0 ∧ 𝑛 ∥ 𝑁))} ⊆ {𝑛 ∈ ℕ ∣ (μ‘𝑛) = 0} |
| 26 | 20, 25 | eqsstri 4030 |
. . . . . 6
⊢ ({𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑁} ∖ {𝑛 ∈ ℕ ∣ ((μ‘𝑛) ≠ 0 ∧ 𝑛 ∥ 𝑁)}) ⊆ {𝑛 ∈ ℕ ∣ (μ‘𝑛) = 0} |
| 27 | 26 | sseli 3979 |
. . . . 5
⊢ (𝑘 ∈ ({𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑁} ∖ {𝑛 ∈ ℕ ∣ ((μ‘𝑛) ≠ 0 ∧ 𝑛 ∥ 𝑁)}) → 𝑘 ∈ {𝑛 ∈ ℕ ∣ (μ‘𝑛) = 0}) |
| 28 | | fveqeq2 6915 |
. . . . . . 7
⊢ (𝑛 = 𝑘 → ((μ‘𝑛) = 0 ↔ (μ‘𝑘) = 0)) |
| 29 | 28 | elrab 3692 |
. . . . . 6
⊢ (𝑘 ∈ {𝑛 ∈ ℕ ∣ (μ‘𝑛) = 0} ↔ (𝑘 ∈ ℕ ∧
(μ‘𝑘) =
0)) |
| 30 | 29 | simprbi 496 |
. . . . 5
⊢ (𝑘 ∈ {𝑛 ∈ ℕ ∣ (μ‘𝑛) = 0} → (μ‘𝑘) = 0) |
| 31 | 27, 30 | syl 17 |
. . . 4
⊢ (𝑘 ∈ ({𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑁} ∖ {𝑛 ∈ ℕ ∣ ((μ‘𝑛) ≠ 0 ∧ 𝑛 ∥ 𝑁)}) → (μ‘𝑘) = 0) |
| 32 | 31 | adantl 481 |
. . 3
⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ ({𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑁} ∖ {𝑛 ∈ ℕ ∣ ((μ‘𝑛) ≠ 0 ∧ 𝑛 ∥ 𝑁)})) → (μ‘𝑘) = 0) |
| 33 | | dvdsfi 16826 |
. . 3
⊢ (𝑁 ∈ ℕ → {𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑁} ∈ Fin) |
| 34 | 13, 19, 32, 33 | fsumss 15761 |
. 2
⊢ (𝑁 ∈ ℕ →
Σ𝑘 ∈ {𝑛 ∈ ℕ ∣
((μ‘𝑛) ≠ 0
∧ 𝑛 ∥ 𝑁)} (μ‘𝑘) = Σ𝑘 ∈ {𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑁} (μ‘𝑘)) |
| 35 | | fveq2 6906 |
. . . . 5
⊢ (𝑥 = {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑘} → (♯‘𝑥) = (♯‘{𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑘})) |
| 36 | 35 | oveq2d 7447 |
. . . 4
⊢ (𝑥 = {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑘} → (-1↑(♯‘𝑥)) =
(-1↑(♯‘{𝑝
∈ ℙ ∣ 𝑝
∥ 𝑘}))) |
| 37 | 33, 13 | ssfid 9301 |
. . . 4
⊢ (𝑁 ∈ ℕ → {𝑛 ∈ ℕ ∣
((μ‘𝑛) ≠ 0
∧ 𝑛 ∥ 𝑁)} ∈ Fin) |
| 38 | | eqid 2737 |
. . . . 5
⊢ {𝑛 ∈ ℕ ∣
((μ‘𝑛) ≠ 0
∧ 𝑛 ∥ 𝑁)} = {𝑛 ∈ ℕ ∣ ((μ‘𝑛) ≠ 0 ∧ 𝑛 ∥ 𝑁)} |
| 39 | | eqid 2737 |
. . . . 5
⊢ (𝑚 ∈ {𝑛 ∈ ℕ ∣ ((μ‘𝑛) ≠ 0 ∧ 𝑛 ∥ 𝑁)} ↦ {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑚}) = (𝑚 ∈ {𝑛 ∈ ℕ ∣ ((μ‘𝑛) ≠ 0 ∧ 𝑛 ∥ 𝑁)} ↦ {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑚}) |
| 40 | | oveq1 7438 |
. . . . . . . 8
⊢ (𝑞 = 𝑝 → (𝑞 pCnt 𝑥) = (𝑝 pCnt 𝑥)) |
| 41 | 40 | cbvmptv 5255 |
. . . . . . 7
⊢ (𝑞 ∈ ℙ ↦ (𝑞 pCnt 𝑥)) = (𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑥)) |
| 42 | | oveq2 7439 |
. . . . . . . 8
⊢ (𝑥 = 𝑚 → (𝑝 pCnt 𝑥) = (𝑝 pCnt 𝑚)) |
| 43 | 42 | mpteq2dv 5244 |
. . . . . . 7
⊢ (𝑥 = 𝑚 → (𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑥)) = (𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑚))) |
| 44 | 41, 43 | eqtrid 2789 |
. . . . . 6
⊢ (𝑥 = 𝑚 → (𝑞 ∈ ℙ ↦ (𝑞 pCnt 𝑥)) = (𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑚))) |
| 45 | 44 | cbvmptv 5255 |
. . . . 5
⊢ (𝑥 ∈ ℕ ↦ (𝑞 ∈ ℙ ↦ (𝑞 pCnt 𝑥))) = (𝑚 ∈ ℕ ↦ (𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑚))) |
| 46 | 38, 39, 45 | sqff1o 27225 |
. . . 4
⊢ (𝑁 ∈ ℕ → (𝑚 ∈ {𝑛 ∈ ℕ ∣ ((μ‘𝑛) ≠ 0 ∧ 𝑛 ∥ 𝑁)} ↦ {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑚}):{𝑛 ∈ ℕ ∣ ((μ‘𝑛) ≠ 0 ∧ 𝑛 ∥ 𝑁)}–1-1-onto→𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}) |
| 47 | | breq2 5147 |
. . . . . . 7
⊢ (𝑚 = 𝑘 → (𝑝 ∥ 𝑚 ↔ 𝑝 ∥ 𝑘)) |
| 48 | 47 | rabbidv 3444 |
. . . . . 6
⊢ (𝑚 = 𝑘 → {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑚} = {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑘}) |
| 49 | | prmex 16714 |
. . . . . . 7
⊢ ℙ
∈ V |
| 50 | 49 | rabex 5339 |
. . . . . 6
⊢ {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑘} ∈ V |
| 51 | 48, 39, 50 | fvmpt 7016 |
. . . . 5
⊢ (𝑘 ∈ {𝑛 ∈ ℕ ∣ ((μ‘𝑛) ≠ 0 ∧ 𝑛 ∥ 𝑁)} → ((𝑚 ∈ {𝑛 ∈ ℕ ∣ ((μ‘𝑛) ≠ 0 ∧ 𝑛 ∥ 𝑁)} ↦ {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑚})‘𝑘) = {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑘}) |
| 52 | 51 | adantl 481 |
. . . 4
⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ {𝑛 ∈ ℕ ∣ ((μ‘𝑛) ≠ 0 ∧ 𝑛 ∥ 𝑁)}) → ((𝑚 ∈ {𝑛 ∈ ℕ ∣ ((μ‘𝑛) ≠ 0 ∧ 𝑛 ∥ 𝑁)} ↦ {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑚})‘𝑘) = {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑘}) |
| 53 | | neg1cn 12380 |
. . . . 5
⊢ -1 ∈
ℂ |
| 54 | | prmdvdsfi 27150 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ → {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁} ∈ Fin) |
| 55 | | elpwi 4607 |
. . . . . . 7
⊢ (𝑥 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁} → 𝑥 ⊆ {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}) |
| 56 | | ssfi 9213 |
. . . . . . 7
⊢ (({𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁} ∈ Fin ∧ 𝑥 ⊆ {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}) → 𝑥 ∈ Fin) |
| 57 | 54, 55, 56 | syl2an 596 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ 𝑥 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}) → 𝑥 ∈ Fin) |
| 58 | | hashcl 14395 |
. . . . . 6
⊢ (𝑥 ∈ Fin →
(♯‘𝑥) ∈
ℕ0) |
| 59 | 57, 58 | syl 17 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ 𝑥 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}) → (♯‘𝑥) ∈
ℕ0) |
| 60 | | expcl 14120 |
. . . . 5
⊢ ((-1
∈ ℂ ∧ (♯‘𝑥) ∈ ℕ0) →
(-1↑(♯‘𝑥))
∈ ℂ) |
| 61 | 53, 59, 60 | sylancr 587 |
. . . 4
⊢ ((𝑁 ∈ ℕ ∧ 𝑥 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}) → (-1↑(♯‘𝑥)) ∈
ℂ) |
| 62 | 36, 37, 46, 52, 61 | fsumf1o 15759 |
. . 3
⊢ (𝑁 ∈ ℕ →
Σ𝑥 ∈ 𝒫
{𝑝 ∈ ℙ ∣
𝑝 ∥ 𝑁} (-1↑(♯‘𝑥)) = Σ𝑘 ∈ {𝑛 ∈ ℕ ∣ ((μ‘𝑛) ≠ 0 ∧ 𝑛 ∥ 𝑁)} (-1↑(♯‘{𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑘}))) |
| 63 | | fzfid 14014 |
. . . . 5
⊢ (𝑁 ∈ ℕ →
(0...(♯‘{𝑝
∈ ℙ ∣ 𝑝
∥ 𝑁})) ∈
Fin) |
| 64 | 54 | adantr 480 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ 𝑧 ∈
(0...(♯‘{𝑝
∈ ℙ ∣ 𝑝
∥ 𝑁}))) → {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁} ∈ Fin) |
| 65 | | pwfi 9357 |
. . . . . . 7
⊢ ({𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁} ∈ Fin ↔ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁} ∈ Fin) |
| 66 | 64, 65 | sylib 218 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ 𝑧 ∈
(0...(♯‘{𝑝
∈ ℙ ∣ 𝑝
∥ 𝑁}))) →
𝒫 {𝑝 ∈ ℙ
∣ 𝑝 ∥ 𝑁} ∈ Fin) |
| 67 | | ssrab2 4080 |
. . . . . 6
⊢ {𝑠 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁} ∣ (♯‘𝑠) = 𝑧} ⊆ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁} |
| 68 | | ssfi 9213 |
. . . . . 6
⊢
((𝒫 {𝑝
∈ ℙ ∣ 𝑝
∥ 𝑁} ∈ Fin ∧
{𝑠 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁} ∣ (♯‘𝑠) = 𝑧} ⊆ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}) → {𝑠 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁} ∣ (♯‘𝑠) = 𝑧} ∈ Fin) |
| 69 | 66, 67, 68 | sylancl 586 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ 𝑧 ∈
(0...(♯‘{𝑝
∈ ℙ ∣ 𝑝
∥ 𝑁}))) → {𝑠 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁} ∣ (♯‘𝑠) = 𝑧} ∈ Fin) |
| 70 | | simprr 773 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ (𝑧 ∈
(0...(♯‘{𝑝
∈ ℙ ∣ 𝑝
∥ 𝑁})) ∧ 𝑥 ∈ {𝑠 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁} ∣ (♯‘𝑠) = 𝑧})) → 𝑥 ∈ {𝑠 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁} ∣ (♯‘𝑠) = 𝑧}) |
| 71 | | fveqeq2 6915 |
. . . . . . . . . 10
⊢ (𝑠 = 𝑥 → ((♯‘𝑠) = 𝑧 ↔ (♯‘𝑥) = 𝑧)) |
| 72 | 71 | elrab 3692 |
. . . . . . . . 9
⊢ (𝑥 ∈ {𝑠 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁} ∣ (♯‘𝑠) = 𝑧} ↔ (𝑥 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁} ∧ (♯‘𝑥) = 𝑧)) |
| 73 | 72 | simprbi 496 |
. . . . . . . 8
⊢ (𝑥 ∈ {𝑠 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁} ∣ (♯‘𝑠) = 𝑧} → (♯‘𝑥) = 𝑧) |
| 74 | 70, 73 | syl 17 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ (𝑧 ∈
(0...(♯‘{𝑝
∈ ℙ ∣ 𝑝
∥ 𝑁})) ∧ 𝑥 ∈ {𝑠 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁} ∣ (♯‘𝑠) = 𝑧})) → (♯‘𝑥) = 𝑧) |
| 75 | 74 | ralrimivva 3202 |
. . . . . 6
⊢ (𝑁 ∈ ℕ →
∀𝑧 ∈
(0...(♯‘{𝑝
∈ ℙ ∣ 𝑝
∥ 𝑁}))∀𝑥 ∈ {𝑠 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁} ∣ (♯‘𝑠) = 𝑧} (♯‘𝑥) = 𝑧) |
| 76 | | invdisj 5129 |
. . . . . 6
⊢
(∀𝑧 ∈
(0...(♯‘{𝑝
∈ ℙ ∣ 𝑝
∥ 𝑁}))∀𝑥 ∈ {𝑠 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁} ∣ (♯‘𝑠) = 𝑧} (♯‘𝑥) = 𝑧 → Disj 𝑧 ∈ (0...(♯‘{𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁})){𝑠 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁} ∣ (♯‘𝑠) = 𝑧}) |
| 77 | 75, 76 | syl 17 |
. . . . 5
⊢ (𝑁 ∈ ℕ →
Disj 𝑧 ∈
(0...(♯‘{𝑝
∈ ℙ ∣ 𝑝
∥ 𝑁})){𝑠 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁} ∣ (♯‘𝑠) = 𝑧}) |
| 78 | 54 | adantr 480 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ (𝑧 ∈
(0...(♯‘{𝑝
∈ ℙ ∣ 𝑝
∥ 𝑁})) ∧ 𝑥 ∈ {𝑠 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁} ∣ (♯‘𝑠) = 𝑧})) → {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁} ∈ Fin) |
| 79 | 67, 70 | sselid 3981 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ (𝑧 ∈
(0...(♯‘{𝑝
∈ ℙ ∣ 𝑝
∥ 𝑁})) ∧ 𝑥 ∈ {𝑠 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁} ∣ (♯‘𝑠) = 𝑧})) → 𝑥 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}) |
| 80 | 79, 55 | syl 17 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ (𝑧 ∈
(0...(♯‘{𝑝
∈ ℙ ∣ 𝑝
∥ 𝑁})) ∧ 𝑥 ∈ {𝑠 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁} ∣ (♯‘𝑠) = 𝑧})) → 𝑥 ⊆ {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}) |
| 81 | 78, 80 | ssfid 9301 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ (𝑧 ∈
(0...(♯‘{𝑝
∈ ℙ ∣ 𝑝
∥ 𝑁})) ∧ 𝑥 ∈ {𝑠 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁} ∣ (♯‘𝑠) = 𝑧})) → 𝑥 ∈ Fin) |
| 82 | 81, 58 | syl 17 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ (𝑧 ∈
(0...(♯‘{𝑝
∈ ℙ ∣ 𝑝
∥ 𝑁})) ∧ 𝑥 ∈ {𝑠 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁} ∣ (♯‘𝑠) = 𝑧})) → (♯‘𝑥) ∈
ℕ0) |
| 83 | 53, 82, 60 | sylancr 587 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ (𝑧 ∈
(0...(♯‘{𝑝
∈ ℙ ∣ 𝑝
∥ 𝑁})) ∧ 𝑥 ∈ {𝑠 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁} ∣ (♯‘𝑠) = 𝑧})) → (-1↑(♯‘𝑥)) ∈
ℂ) |
| 84 | 63, 69, 77, 83 | fsumiun 15857 |
. . . 4
⊢ (𝑁 ∈ ℕ →
Σ𝑥 ∈ ∪ 𝑧 ∈ (0...(♯‘{𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁})){𝑠 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁} ∣ (♯‘𝑠) = 𝑧} (-1↑(♯‘𝑥)) = Σ𝑧 ∈ (0...(♯‘{𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}))Σ𝑥 ∈ {𝑠 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁} ∣ (♯‘𝑠) = 𝑧} (-1↑(♯‘𝑥))) |
| 85 | | iunrab 5052 |
. . . . . 6
⊢ ∪ 𝑧 ∈ (0...(♯‘{𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁})){𝑠 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁} ∣ (♯‘𝑠) = 𝑧} = {𝑠 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁} ∣ ∃𝑧 ∈ (0...(♯‘{𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}))(♯‘𝑠) = 𝑧} |
| 86 | 54 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ ∧ 𝑠 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}) → {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁} ∈ Fin) |
| 87 | | elpwi 4607 |
. . . . . . . . . . . . 13
⊢ (𝑠 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁} → 𝑠 ⊆ {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}) |
| 88 | 87 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ ∧ 𝑠 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}) → 𝑠 ⊆ {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}) |
| 89 | | ssdomg 9040 |
. . . . . . . . . . . 12
⊢ ({𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁} ∈ Fin → (𝑠 ⊆ {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁} → 𝑠 ≼ {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁})) |
| 90 | 86, 88, 89 | sylc 65 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ 𝑠 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}) → 𝑠 ≼ {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}) |
| 91 | | ssfi 9213 |
. . . . . . . . . . . . 13
⊢ (({𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁} ∈ Fin ∧ 𝑠 ⊆ {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}) → 𝑠 ∈ Fin) |
| 92 | 54, 87, 91 | syl2an 596 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ ∧ 𝑠 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}) → 𝑠 ∈ Fin) |
| 93 | | hashdom 14418 |
. . . . . . . . . . . 12
⊢ ((𝑠 ∈ Fin ∧ {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁} ∈ Fin) → ((♯‘𝑠) ≤ (♯‘{𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}) ↔ 𝑠 ≼ {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁})) |
| 94 | 92, 86, 93 | syl2anc 584 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ 𝑠 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}) → ((♯‘𝑠) ≤ (♯‘{𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}) ↔ 𝑠 ≼ {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁})) |
| 95 | 90, 94 | mpbird 257 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ 𝑠 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}) → (♯‘𝑠) ≤ (♯‘{𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁})) |
| 96 | | hashcl 14395 |
. . . . . . . . . . . . 13
⊢ (𝑠 ∈ Fin →
(♯‘𝑠) ∈
ℕ0) |
| 97 | 92, 96 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ ∧ 𝑠 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}) → (♯‘𝑠) ∈
ℕ0) |
| 98 | | nn0uz 12920 |
. . . . . . . . . . . 12
⊢
ℕ0 = (ℤ≥‘0) |
| 99 | 97, 98 | eleqtrdi 2851 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ 𝑠 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}) → (♯‘𝑠) ∈
(ℤ≥‘0)) |
| 100 | | hashcl 14395 |
. . . . . . . . . . . . . 14
⊢ ({𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁} ∈ Fin → (♯‘{𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}) ∈
ℕ0) |
| 101 | 54, 100 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℕ →
(♯‘{𝑝 ∈
ℙ ∣ 𝑝 ∥
𝑁}) ∈
ℕ0) |
| 102 | 101 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ ∧ 𝑠 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}) → (♯‘{𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}) ∈
ℕ0) |
| 103 | 102 | nn0zd 12639 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ 𝑠 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}) → (♯‘{𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}) ∈ ℤ) |
| 104 | | elfz5 13556 |
. . . . . . . . . . 11
⊢
(((♯‘𝑠)
∈ (ℤ≥‘0) ∧ (♯‘{𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}) ∈ ℤ) →
((♯‘𝑠) ∈
(0...(♯‘{𝑝
∈ ℙ ∣ 𝑝
∥ 𝑁})) ↔
(♯‘𝑠) ≤
(♯‘{𝑝 ∈
ℙ ∣ 𝑝 ∥
𝑁}))) |
| 105 | 99, 103, 104 | syl2anc 584 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ 𝑠 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}) → ((♯‘𝑠) ∈ (0...(♯‘{𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁})) ↔ (♯‘𝑠) ≤ (♯‘{𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}))) |
| 106 | 95, 105 | mpbird 257 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ 𝑠 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}) → (♯‘𝑠) ∈ (0...(♯‘{𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}))) |
| 107 | | eqidd 2738 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ 𝑠 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}) → (♯‘𝑠) = (♯‘𝑠)) |
| 108 | | eqeq2 2749 |
. . . . . . . . . 10
⊢ (𝑧 = (♯‘𝑠) → ((♯‘𝑠) = 𝑧 ↔ (♯‘𝑠) = (♯‘𝑠))) |
| 109 | 108 | rspcev 3622 |
. . . . . . . . 9
⊢
(((♯‘𝑠)
∈ (0...(♯‘{𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁})) ∧ (♯‘𝑠) = (♯‘𝑠)) → ∃𝑧 ∈ (0...(♯‘{𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}))(♯‘𝑠) = 𝑧) |
| 110 | 106, 107,
109 | syl2anc 584 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝑠 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}) → ∃𝑧 ∈ (0...(♯‘{𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}))(♯‘𝑠) = 𝑧) |
| 111 | 110 | ralrimiva 3146 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ →
∀𝑠 ∈ 𝒫
{𝑝 ∈ ℙ ∣
𝑝 ∥ 𝑁}∃𝑧 ∈ (0...(♯‘{𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}))(♯‘𝑠) = 𝑧) |
| 112 | | rabid2 3470 |
. . . . . . 7
⊢
(𝒫 {𝑝 ∈
ℙ ∣ 𝑝 ∥
𝑁} = {𝑠 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁} ∣ ∃𝑧 ∈ (0...(♯‘{𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}))(♯‘𝑠) = 𝑧} ↔ ∀𝑠 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}∃𝑧 ∈ (0...(♯‘{𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}))(♯‘𝑠) = 𝑧) |
| 113 | 111, 112 | sylibr 234 |
. . . . . 6
⊢ (𝑁 ∈ ℕ → 𝒫
{𝑝 ∈ ℙ ∣
𝑝 ∥ 𝑁} = {𝑠 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁} ∣ ∃𝑧 ∈ (0...(♯‘{𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}))(♯‘𝑠) = 𝑧}) |
| 114 | 85, 113 | eqtr4id 2796 |
. . . . 5
⊢ (𝑁 ∈ ℕ → ∪ 𝑧 ∈ (0...(♯‘{𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁})){𝑠 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁} ∣ (♯‘𝑠) = 𝑧} = 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}) |
| 115 | 114 | sumeq1d 15736 |
. . . 4
⊢ (𝑁 ∈ ℕ →
Σ𝑥 ∈ ∪ 𝑧 ∈ (0...(♯‘{𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁})){𝑠 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁} ∣ (♯‘𝑠) = 𝑧} (-1↑(♯‘𝑥)) = Σ𝑥 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁} (-1↑(♯‘𝑥))) |
| 116 | | elfznn0 13660 |
. . . . . . . . . 10
⊢ (𝑧 ∈
(0...(♯‘{𝑝
∈ ℙ ∣ 𝑝
∥ 𝑁})) → 𝑧 ∈
ℕ0) |
| 117 | 116 | adantl 481 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ 𝑧 ∈
(0...(♯‘{𝑝
∈ ℙ ∣ 𝑝
∥ 𝑁}))) → 𝑧 ∈
ℕ0) |
| 118 | | expcl 14120 |
. . . . . . . . 9
⊢ ((-1
∈ ℂ ∧ 𝑧
∈ ℕ0) → (-1↑𝑧) ∈ ℂ) |
| 119 | 53, 117, 118 | sylancr 587 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝑧 ∈
(0...(♯‘{𝑝
∈ ℙ ∣ 𝑝
∥ 𝑁}))) →
(-1↑𝑧) ∈
ℂ) |
| 120 | | fsumconst 15826 |
. . . . . . . 8
⊢ (({𝑠 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁} ∣ (♯‘𝑠) = 𝑧} ∈ Fin ∧ (-1↑𝑧) ∈ ℂ) →
Σ𝑥 ∈ {𝑠 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁} ∣ (♯‘𝑠) = 𝑧} (-1↑𝑧) = ((♯‘{𝑠 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁} ∣ (♯‘𝑠) = 𝑧}) · (-1↑𝑧))) |
| 121 | 69, 119, 120 | syl2anc 584 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ 𝑧 ∈
(0...(♯‘{𝑝
∈ ℙ ∣ 𝑝
∥ 𝑁}))) →
Σ𝑥 ∈ {𝑠 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁} ∣ (♯‘𝑠) = 𝑧} (-1↑𝑧) = ((♯‘{𝑠 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁} ∣ (♯‘𝑠) = 𝑧}) · (-1↑𝑧))) |
| 122 | 73 | adantl 481 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ ∧ 𝑧 ∈
(0...(♯‘{𝑝
∈ ℙ ∣ 𝑝
∥ 𝑁}))) ∧ 𝑥 ∈ {𝑠 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁} ∣ (♯‘𝑠) = 𝑧}) → (♯‘𝑥) = 𝑧) |
| 123 | 122 | oveq2d 7447 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ ∧ 𝑧 ∈
(0...(♯‘{𝑝
∈ ℙ ∣ 𝑝
∥ 𝑁}))) ∧ 𝑥 ∈ {𝑠 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁} ∣ (♯‘𝑠) = 𝑧}) → (-1↑(♯‘𝑥)) = (-1↑𝑧)) |
| 124 | 123 | sumeq2dv 15738 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ 𝑧 ∈
(0...(♯‘{𝑝
∈ ℙ ∣ 𝑝
∥ 𝑁}))) →
Σ𝑥 ∈ {𝑠 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁} ∣ (♯‘𝑠) = 𝑧} (-1↑(♯‘𝑥)) = Σ𝑥 ∈ {𝑠 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁} ∣ (♯‘𝑠) = 𝑧} (-1↑𝑧)) |
| 125 | | elfzelz 13564 |
. . . . . . . . 9
⊢ (𝑧 ∈
(0...(♯‘{𝑝
∈ ℙ ∣ 𝑝
∥ 𝑁})) → 𝑧 ∈
ℤ) |
| 126 | | hashbc 14492 |
. . . . . . . . 9
⊢ (({𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁} ∈ Fin ∧ 𝑧 ∈ ℤ) →
((♯‘{𝑝 ∈
ℙ ∣ 𝑝 ∥
𝑁})C𝑧) = (♯‘{𝑠 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁} ∣ (♯‘𝑠) = 𝑧})) |
| 127 | 54, 125, 126 | syl2an 596 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝑧 ∈
(0...(♯‘{𝑝
∈ ℙ ∣ 𝑝
∥ 𝑁}))) →
((♯‘{𝑝 ∈
ℙ ∣ 𝑝 ∥
𝑁})C𝑧) = (♯‘{𝑠 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁} ∣ (♯‘𝑠) = 𝑧})) |
| 128 | 127 | oveq1d 7446 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ 𝑧 ∈
(0...(♯‘{𝑝
∈ ℙ ∣ 𝑝
∥ 𝑁}))) →
(((♯‘{𝑝 ∈
ℙ ∣ 𝑝 ∥
𝑁})C𝑧) · (-1↑𝑧)) = ((♯‘{𝑠 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁} ∣ (♯‘𝑠) = 𝑧}) · (-1↑𝑧))) |
| 129 | 121, 124,
128 | 3eqtr4d 2787 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ 𝑧 ∈
(0...(♯‘{𝑝
∈ ℙ ∣ 𝑝
∥ 𝑁}))) →
Σ𝑥 ∈ {𝑠 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁} ∣ (♯‘𝑠) = 𝑧} (-1↑(♯‘𝑥)) = (((♯‘{𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁})C𝑧) · (-1↑𝑧))) |
| 130 | 129 | sumeq2dv 15738 |
. . . . 5
⊢ (𝑁 ∈ ℕ →
Σ𝑧 ∈
(0...(♯‘{𝑝
∈ ℙ ∣ 𝑝
∥ 𝑁}))Σ𝑥 ∈ {𝑠 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁} ∣ (♯‘𝑠) = 𝑧} (-1↑(♯‘𝑥)) = Σ𝑧 ∈ (0...(♯‘{𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}))(((♯‘{𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁})C𝑧) · (-1↑𝑧))) |
| 131 | | 1pneg1e0 12385 |
. . . . . . 7
⊢ (1 + -1)
= 0 |
| 132 | 131 | oveq1i 7441 |
. . . . . 6
⊢ ((1 +
-1)↑(♯‘{𝑝
∈ ℙ ∣ 𝑝
∥ 𝑁})) =
(0↑(♯‘{𝑝
∈ ℙ ∣ 𝑝
∥ 𝑁})) |
| 133 | | binom1p 15867 |
. . . . . . 7
⊢ ((-1
∈ ℂ ∧ (♯‘{𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}) ∈ ℕ0) → ((1 +
-1)↑(♯‘{𝑝
∈ ℙ ∣ 𝑝
∥ 𝑁})) = Σ𝑧 ∈
(0...(♯‘{𝑝
∈ ℙ ∣ 𝑝
∥ 𝑁}))(((♯‘{𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁})C𝑧) · (-1↑𝑧))) |
| 134 | 53, 101, 133 | sylancr 587 |
. . . . . 6
⊢ (𝑁 ∈ ℕ → ((1 +
-1)↑(♯‘{𝑝
∈ ℙ ∣ 𝑝
∥ 𝑁})) = Σ𝑧 ∈
(0...(♯‘{𝑝
∈ ℙ ∣ 𝑝
∥ 𝑁}))(((♯‘{𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁})C𝑧) · (-1↑𝑧))) |
| 135 | 132, 134 | eqtr3id 2791 |
. . . . 5
⊢ (𝑁 ∈ ℕ →
(0↑(♯‘{𝑝
∈ ℙ ∣ 𝑝
∥ 𝑁})) = Σ𝑧 ∈
(0...(♯‘{𝑝
∈ ℙ ∣ 𝑝
∥ 𝑁}))(((♯‘{𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁})C𝑧) · (-1↑𝑧))) |
| 136 | | eqeq2 2749 |
. . . . . 6
⊢ (1 =
if(𝑁 = 1, 1, 0) →
((0↑(♯‘{𝑝
∈ ℙ ∣ 𝑝
∥ 𝑁})) = 1 ↔
(0↑(♯‘{𝑝
∈ ℙ ∣ 𝑝
∥ 𝑁})) = if(𝑁 = 1, 1, 0))) |
| 137 | | eqeq2 2749 |
. . . . . 6
⊢ (0 =
if(𝑁 = 1, 1, 0) →
((0↑(♯‘{𝑝
∈ ℙ ∣ 𝑝
∥ 𝑁})) = 0 ↔
(0↑(♯‘{𝑝
∈ ℙ ∣ 𝑝
∥ 𝑁})) = if(𝑁 = 1, 1, 0))) |
| 138 | | nprmdvds1 16743 |
. . . . . . . . . . . . 13
⊢ (𝑝 ∈ ℙ → ¬
𝑝 ∥
1) |
| 139 | | simpr 484 |
. . . . . . . . . . . . . . 15
⊢ ((𝑁 ∈ ℕ ∧ 𝑁 = 1) → 𝑁 = 1) |
| 140 | 139 | breq2d 5155 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℕ ∧ 𝑁 = 1) → (𝑝 ∥ 𝑁 ↔ 𝑝 ∥ 1)) |
| 141 | 140 | notbid 318 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℕ ∧ 𝑁 = 1) → (¬ 𝑝 ∥ 𝑁 ↔ ¬ 𝑝 ∥ 1)) |
| 142 | 138, 141 | imbitrrid 246 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ ∧ 𝑁 = 1) → (𝑝 ∈ ℙ → ¬ 𝑝 ∥ 𝑁)) |
| 143 | 142 | ralrimiv 3145 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ 𝑁 = 1) → ∀𝑝 ∈ ℙ ¬ 𝑝 ∥ 𝑁) |
| 144 | | rabeq0 4388 |
. . . . . . . . . . 11
⊢ ({𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁} = ∅ ↔ ∀𝑝 ∈ ℙ ¬ 𝑝 ∥ 𝑁) |
| 145 | 143, 144 | sylibr 234 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ 𝑁 = 1) → {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁} = ∅) |
| 146 | 145 | fveq2d 6910 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ 𝑁 = 1) →
(♯‘{𝑝 ∈
ℙ ∣ 𝑝 ∥
𝑁}) =
(♯‘∅)) |
| 147 | | hash0 14406 |
. . . . . . . . 9
⊢
(♯‘∅) = 0 |
| 148 | 146, 147 | eqtrdi 2793 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝑁 = 1) →
(♯‘{𝑝 ∈
ℙ ∣ 𝑝 ∥
𝑁}) = 0) |
| 149 | 148 | oveq2d 7447 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ 𝑁 = 1) →
(0↑(♯‘{𝑝
∈ ℙ ∣ 𝑝
∥ 𝑁})) =
(0↑0)) |
| 150 | | 0exp0e1 14107 |
. . . . . . 7
⊢
(0↑0) = 1 |
| 151 | 149, 150 | eqtrdi 2793 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ 𝑁 = 1) →
(0↑(♯‘{𝑝
∈ ℙ ∣ 𝑝
∥ 𝑁})) =
1) |
| 152 | | df-ne 2941 |
. . . . . . . . . . 11
⊢ (𝑁 ≠ 1 ↔ ¬ 𝑁 = 1) |
| 153 | | eluz2b3 12964 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈
(ℤ≥‘2) ↔ (𝑁 ∈ ℕ ∧ 𝑁 ≠ 1)) |
| 154 | 153 | biimpri 228 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ 𝑁 ≠ 1) → 𝑁 ∈
(ℤ≥‘2)) |
| 155 | 152, 154 | sylan2br 595 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ ¬
𝑁 = 1) → 𝑁 ∈
(ℤ≥‘2)) |
| 156 | | exprmfct 16741 |
. . . . . . . . . 10
⊢ (𝑁 ∈
(ℤ≥‘2) → ∃𝑝 ∈ ℙ 𝑝 ∥ 𝑁) |
| 157 | 155, 156 | syl 17 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ ¬
𝑁 = 1) → ∃𝑝 ∈ ℙ 𝑝 ∥ 𝑁) |
| 158 | | rabn0 4389 |
. . . . . . . . 9
⊢ ({𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁} ≠ ∅ ↔ ∃𝑝 ∈ ℙ 𝑝 ∥ 𝑁) |
| 159 | 157, 158 | sylibr 234 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ ¬
𝑁 = 1) → {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁} ≠ ∅) |
| 160 | 54 | adantr 480 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ ¬
𝑁 = 1) → {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁} ∈ Fin) |
| 161 | | hashnncl 14405 |
. . . . . . . . 9
⊢ ({𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁} ∈ Fin → ((♯‘{𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}) ∈ ℕ ↔ {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁} ≠ ∅)) |
| 162 | 160, 161 | syl 17 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ ¬
𝑁 = 1) →
((♯‘{𝑝 ∈
ℙ ∣ 𝑝 ∥
𝑁}) ∈ ℕ ↔
{𝑝 ∈ ℙ ∣
𝑝 ∥ 𝑁} ≠ ∅)) |
| 163 | 159, 162 | mpbird 257 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ ¬
𝑁 = 1) →
(♯‘{𝑝 ∈
ℙ ∣ 𝑝 ∥
𝑁}) ∈
ℕ) |
| 164 | 163 | 0expd 14179 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ ¬
𝑁 = 1) →
(0↑(♯‘{𝑝
∈ ℙ ∣ 𝑝
∥ 𝑁})) =
0) |
| 165 | 136, 137,
151, 164 | ifbothda 4564 |
. . . . 5
⊢ (𝑁 ∈ ℕ →
(0↑(♯‘{𝑝
∈ ℙ ∣ 𝑝
∥ 𝑁})) = if(𝑁 = 1, 1, 0)) |
| 166 | 130, 135,
165 | 3eqtr2d 2783 |
. . . 4
⊢ (𝑁 ∈ ℕ →
Σ𝑧 ∈
(0...(♯‘{𝑝
∈ ℙ ∣ 𝑝
∥ 𝑁}))Σ𝑥 ∈ {𝑠 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁} ∣ (♯‘𝑠) = 𝑧} (-1↑(♯‘𝑥)) = if(𝑁 = 1, 1, 0)) |
| 167 | 84, 115, 166 | 3eqtr3d 2785 |
. . 3
⊢ (𝑁 ∈ ℕ →
Σ𝑥 ∈ 𝒫
{𝑝 ∈ ℙ ∣
𝑝 ∥ 𝑁} (-1↑(♯‘𝑥)) = if(𝑁 = 1, 1, 0)) |
| 168 | 62, 167 | eqtr3d 2779 |
. 2
⊢ (𝑁 ∈ ℕ →
Σ𝑘 ∈ {𝑛 ∈ ℕ ∣
((μ‘𝑛) ≠ 0
∧ 𝑛 ∥ 𝑁)}
(-1↑(♯‘{𝑝
∈ ℙ ∣ 𝑝
∥ 𝑘})) = if(𝑁 = 1, 1, 0)) |
| 169 | 10, 34, 168 | 3eqtr3d 2785 |
1
⊢ (𝑁 ∈ ℕ →
Σ𝑘 ∈ {𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑁} (μ‘𝑘) = if(𝑁 = 1, 1, 0)) |