Step | Hyp | Ref
| Expression |
1 | | fveq2 6191 |
. . . . . . . 8
⊢ (𝑛 = 𝑘 → (μ‘𝑛) = (μ‘𝑘)) |
2 | 1 | neeq1d 2853 |
. . . . . . 7
⊢ (𝑛 = 𝑘 → ((μ‘𝑛) ≠ 0 ↔ (μ‘𝑘) ≠ 0)) |
3 | | breq1 4656 |
. . . . . . 7
⊢ (𝑛 = 𝑘 → (𝑛 ∥ 𝑁 ↔ 𝑘 ∥ 𝑁)) |
4 | 2, 3 | anbi12d 747 |
. . . . . 6
⊢ (𝑛 = 𝑘 → (((μ‘𝑛) ≠ 0 ∧ 𝑛 ∥ 𝑁) ↔ ((μ‘𝑘) ≠ 0 ∧ 𝑘 ∥ 𝑁))) |
5 | 4 | elrab 3363 |
. . . . 5
⊢ (𝑘 ∈ {𝑛 ∈ ℕ ∣ ((μ‘𝑛) ≠ 0 ∧ 𝑛 ∥ 𝑁)} ↔ (𝑘 ∈ ℕ ∧ ((μ‘𝑘) ≠ 0 ∧ 𝑘 ∥ 𝑁))) |
6 | | muval2 24860 |
. . . . . 6
⊢ ((𝑘 ∈ ℕ ∧
(μ‘𝑘) ≠ 0)
→ (μ‘𝑘) =
(-1↑(#‘{𝑝 ∈
ℙ ∣ 𝑝 ∥
𝑘}))) |
7 | 6 | adantrr 753 |
. . . . 5
⊢ ((𝑘 ∈ ℕ ∧
((μ‘𝑘) ≠ 0
∧ 𝑘 ∥ 𝑁)) → (μ‘𝑘) = (-1↑(#‘{𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑘}))) |
8 | 5, 7 | sylbi 207 |
. . . 4
⊢ (𝑘 ∈ {𝑛 ∈ ℕ ∣ ((μ‘𝑛) ≠ 0 ∧ 𝑛 ∥ 𝑁)} → (μ‘𝑘) = (-1↑(#‘{𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑘}))) |
9 | 8 | adantl 482 |
. . 3
⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ {𝑛 ∈ ℕ ∣ ((μ‘𝑛) ≠ 0 ∧ 𝑛 ∥ 𝑁)}) → (μ‘𝑘) = (-1↑(#‘{𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑘}))) |
10 | 9 | sumeq2dv 14433 |
. 2
⊢ (𝑁 ∈ ℕ →
Σ𝑘 ∈ {𝑛 ∈ ℕ ∣
((μ‘𝑛) ≠ 0
∧ 𝑛 ∥ 𝑁)} (μ‘𝑘) = Σ𝑘 ∈ {𝑛 ∈ ℕ ∣ ((μ‘𝑛) ≠ 0 ∧ 𝑛 ∥ 𝑁)} (-1↑(#‘{𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑘}))) |
11 | | simpr 477 |
. . . . 5
⊢
(((μ‘𝑛)
≠ 0 ∧ 𝑛 ∥
𝑁) → 𝑛 ∥ 𝑁) |
12 | 11 | a1i 11 |
. . . 4
⊢ ((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℕ) →
(((μ‘𝑛) ≠ 0
∧ 𝑛 ∥ 𝑁) → 𝑛 ∥ 𝑁)) |
13 | 12 | ss2rabdv 3683 |
. . 3
⊢ (𝑁 ∈ ℕ → {𝑛 ∈ ℕ ∣
((μ‘𝑛) ≠ 0
∧ 𝑛 ∥ 𝑁)} ⊆ {𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑁}) |
14 | | ssrab2 3687 |
. . . . . 6
⊢ {𝑛 ∈ ℕ ∣
((μ‘𝑛) ≠ 0
∧ 𝑛 ∥ 𝑁)} ⊆
ℕ |
15 | | simpr 477 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ {𝑛 ∈ ℕ ∣ ((μ‘𝑛) ≠ 0 ∧ 𝑛 ∥ 𝑁)}) → 𝑘 ∈ {𝑛 ∈ ℕ ∣ ((μ‘𝑛) ≠ 0 ∧ 𝑛 ∥ 𝑁)}) |
16 | 14, 15 | sseldi 3601 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ {𝑛 ∈ ℕ ∣ ((μ‘𝑛) ≠ 0 ∧ 𝑛 ∥ 𝑁)}) → 𝑘 ∈ ℕ) |
17 | | mucl 24867 |
. . . . 5
⊢ (𝑘 ∈ ℕ →
(μ‘𝑘) ∈
ℤ) |
18 | 16, 17 | syl 17 |
. . . 4
⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ {𝑛 ∈ ℕ ∣ ((μ‘𝑛) ≠ 0 ∧ 𝑛 ∥ 𝑁)}) → (μ‘𝑘) ∈ ℤ) |
19 | 18 | zcnd 11483 |
. . 3
⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ {𝑛 ∈ ℕ ∣ ((μ‘𝑛) ≠ 0 ∧ 𝑛 ∥ 𝑁)}) → (μ‘𝑘) ∈ ℂ) |
20 | | difrab 3901 |
. . . . . . 7
⊢ ({𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑁} ∖ {𝑛 ∈ ℕ ∣ ((μ‘𝑛) ≠ 0 ∧ 𝑛 ∥ 𝑁)}) = {𝑛 ∈ ℕ ∣ (𝑛 ∥ 𝑁 ∧ ¬ ((μ‘𝑛) ≠ 0 ∧ 𝑛 ∥ 𝑁))} |
21 | | pm3.21 464 |
. . . . . . . . . . 11
⊢ (𝑛 ∥ 𝑁 → ((μ‘𝑛) ≠ 0 → ((μ‘𝑛) ≠ 0 ∧ 𝑛 ∥ 𝑁))) |
22 | 21 | necon1bd 2812 |
. . . . . . . . . 10
⊢ (𝑛 ∥ 𝑁 → (¬ ((μ‘𝑛) ≠ 0 ∧ 𝑛 ∥ 𝑁) → (μ‘𝑛) = 0)) |
23 | 22 | imp 445 |
. . . . . . . . 9
⊢ ((𝑛 ∥ 𝑁 ∧ ¬ ((μ‘𝑛) ≠ 0 ∧ 𝑛 ∥ 𝑁)) → (μ‘𝑛) = 0) |
24 | 23 | a1i 11 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ → ((𝑛 ∥ 𝑁 ∧ ¬ ((μ‘𝑛) ≠ 0 ∧ 𝑛 ∥ 𝑁)) → (μ‘𝑛) = 0)) |
25 | 24 | ss2rabi 3684 |
. . . . . . 7
⊢ {𝑛 ∈ ℕ ∣ (𝑛 ∥ 𝑁 ∧ ¬ ((μ‘𝑛) ≠ 0 ∧ 𝑛 ∥ 𝑁))} ⊆ {𝑛 ∈ ℕ ∣ (μ‘𝑛) = 0} |
26 | 20, 25 | eqsstri 3635 |
. . . . . 6
⊢ ({𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑁} ∖ {𝑛 ∈ ℕ ∣ ((μ‘𝑛) ≠ 0 ∧ 𝑛 ∥ 𝑁)}) ⊆ {𝑛 ∈ ℕ ∣ (μ‘𝑛) = 0} |
27 | 26 | sseli 3599 |
. . . . 5
⊢ (𝑘 ∈ ({𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑁} ∖ {𝑛 ∈ ℕ ∣ ((μ‘𝑛) ≠ 0 ∧ 𝑛 ∥ 𝑁)}) → 𝑘 ∈ {𝑛 ∈ ℕ ∣ (μ‘𝑛) = 0}) |
28 | 1 | eqeq1d 2624 |
. . . . . . 7
⊢ (𝑛 = 𝑘 → ((μ‘𝑛) = 0 ↔ (μ‘𝑘) = 0)) |
29 | 28 | elrab 3363 |
. . . . . 6
⊢ (𝑘 ∈ {𝑛 ∈ ℕ ∣ (μ‘𝑛) = 0} ↔ (𝑘 ∈ ℕ ∧
(μ‘𝑘) =
0)) |
30 | 29 | simprbi 480 |
. . . . 5
⊢ (𝑘 ∈ {𝑛 ∈ ℕ ∣ (μ‘𝑛) = 0} → (μ‘𝑘) = 0) |
31 | 27, 30 | syl 17 |
. . . 4
⊢ (𝑘 ∈ ({𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑁} ∖ {𝑛 ∈ ℕ ∣ ((μ‘𝑛) ≠ 0 ∧ 𝑛 ∥ 𝑁)}) → (μ‘𝑘) = 0) |
32 | 31 | adantl 482 |
. . 3
⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ ({𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑁} ∖ {𝑛 ∈ ℕ ∣ ((μ‘𝑛) ≠ 0 ∧ 𝑛 ∥ 𝑁)})) → (μ‘𝑘) = 0) |
33 | | fzfid 12772 |
. . . 4
⊢ (𝑁 ∈ ℕ →
(1...𝑁) ∈
Fin) |
34 | | dvdsssfz1 15040 |
. . . 4
⊢ (𝑁 ∈ ℕ → {𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑁} ⊆ (1...𝑁)) |
35 | | ssfi 8180 |
. . . 4
⊢
(((1...𝑁) ∈ Fin
∧ {𝑛 ∈ ℕ
∣ 𝑛 ∥ 𝑁} ⊆ (1...𝑁)) → {𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑁} ∈ Fin) |
36 | 33, 34, 35 | syl2anc 693 |
. . 3
⊢ (𝑁 ∈ ℕ → {𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑁} ∈ Fin) |
37 | 13, 19, 32, 36 | fsumss 14456 |
. 2
⊢ (𝑁 ∈ ℕ →
Σ𝑘 ∈ {𝑛 ∈ ℕ ∣
((μ‘𝑛) ≠ 0
∧ 𝑛 ∥ 𝑁)} (μ‘𝑘) = Σ𝑘 ∈ {𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑁} (μ‘𝑘)) |
38 | | fveq2 6191 |
. . . . 5
⊢ (𝑥 = {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑘} → (#‘𝑥) = (#‘{𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑘})) |
39 | 38 | oveq2d 6666 |
. . . 4
⊢ (𝑥 = {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑘} → (-1↑(#‘𝑥)) = (-1↑(#‘{𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑘}))) |
40 | | ssfi 8180 |
. . . . 5
⊢ (({𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑁} ∈ Fin ∧ {𝑛 ∈ ℕ ∣ ((μ‘𝑛) ≠ 0 ∧ 𝑛 ∥ 𝑁)} ⊆ {𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑁}) → {𝑛 ∈ ℕ ∣ ((μ‘𝑛) ≠ 0 ∧ 𝑛 ∥ 𝑁)} ∈ Fin) |
41 | 36, 13, 40 | syl2anc 693 |
. . . 4
⊢ (𝑁 ∈ ℕ → {𝑛 ∈ ℕ ∣
((μ‘𝑛) ≠ 0
∧ 𝑛 ∥ 𝑁)} ∈ Fin) |
42 | | eqid 2622 |
. . . . 5
⊢ {𝑛 ∈ ℕ ∣
((μ‘𝑛) ≠ 0
∧ 𝑛 ∥ 𝑁)} = {𝑛 ∈ ℕ ∣ ((μ‘𝑛) ≠ 0 ∧ 𝑛 ∥ 𝑁)} |
43 | | eqid 2622 |
. . . . 5
⊢ (𝑚 ∈ {𝑛 ∈ ℕ ∣ ((μ‘𝑛) ≠ 0 ∧ 𝑛 ∥ 𝑁)} ↦ {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑚}) = (𝑚 ∈ {𝑛 ∈ ℕ ∣ ((μ‘𝑛) ≠ 0 ∧ 𝑛 ∥ 𝑁)} ↦ {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑚}) |
44 | | oveq1 6657 |
. . . . . . . 8
⊢ (𝑞 = 𝑝 → (𝑞 pCnt 𝑥) = (𝑝 pCnt 𝑥)) |
45 | 44 | cbvmptv 4750 |
. . . . . . 7
⊢ (𝑞 ∈ ℙ ↦ (𝑞 pCnt 𝑥)) = (𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑥)) |
46 | | oveq2 6658 |
. . . . . . . 8
⊢ (𝑥 = 𝑚 → (𝑝 pCnt 𝑥) = (𝑝 pCnt 𝑚)) |
47 | 46 | mpteq2dv 4745 |
. . . . . . 7
⊢ (𝑥 = 𝑚 → (𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑥)) = (𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑚))) |
48 | 45, 47 | syl5eq 2668 |
. . . . . 6
⊢ (𝑥 = 𝑚 → (𝑞 ∈ ℙ ↦ (𝑞 pCnt 𝑥)) = (𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑚))) |
49 | 48 | cbvmptv 4750 |
. . . . 5
⊢ (𝑥 ∈ ℕ ↦ (𝑞 ∈ ℙ ↦ (𝑞 pCnt 𝑥))) = (𝑚 ∈ ℕ ↦ (𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑚))) |
50 | 42, 43, 49 | sqff1o 24908 |
. . . 4
⊢ (𝑁 ∈ ℕ → (𝑚 ∈ {𝑛 ∈ ℕ ∣ ((μ‘𝑛) ≠ 0 ∧ 𝑛 ∥ 𝑁)} ↦ {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑚}):{𝑛 ∈ ℕ ∣ ((μ‘𝑛) ≠ 0 ∧ 𝑛 ∥ 𝑁)}–1-1-onto→𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}) |
51 | | breq2 4657 |
. . . . . . 7
⊢ (𝑚 = 𝑘 → (𝑝 ∥ 𝑚 ↔ 𝑝 ∥ 𝑘)) |
52 | 51 | rabbidv 3189 |
. . . . . 6
⊢ (𝑚 = 𝑘 → {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑚} = {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑘}) |
53 | | zex 11386 |
. . . . . . . 8
⊢ ℤ
∈ V |
54 | | prmz 15389 |
. . . . . . . . 9
⊢ (𝑝 ∈ ℙ → 𝑝 ∈
ℤ) |
55 | 54 | ssriv 3607 |
. . . . . . . 8
⊢ ℙ
⊆ ℤ |
56 | 53, 55 | ssexi 4803 |
. . . . . . 7
⊢ ℙ
∈ V |
57 | 56 | rabex 4813 |
. . . . . 6
⊢ {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑘} ∈ V |
58 | 52, 43, 57 | fvmpt 6282 |
. . . . 5
⊢ (𝑘 ∈ {𝑛 ∈ ℕ ∣ ((μ‘𝑛) ≠ 0 ∧ 𝑛 ∥ 𝑁)} → ((𝑚 ∈ {𝑛 ∈ ℕ ∣ ((μ‘𝑛) ≠ 0 ∧ 𝑛 ∥ 𝑁)} ↦ {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑚})‘𝑘) = {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑘}) |
59 | 58 | adantl 482 |
. . . 4
⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ {𝑛 ∈ ℕ ∣ ((μ‘𝑛) ≠ 0 ∧ 𝑛 ∥ 𝑁)}) → ((𝑚 ∈ {𝑛 ∈ ℕ ∣ ((μ‘𝑛) ≠ 0 ∧ 𝑛 ∥ 𝑁)} ↦ {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑚})‘𝑘) = {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑘}) |
60 | | neg1cn 11124 |
. . . . 5
⊢ -1 ∈
ℂ |
61 | | prmdvdsfi 24833 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ → {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁} ∈ Fin) |
62 | | elpwi 4168 |
. . . . . . 7
⊢ (𝑥 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁} → 𝑥 ⊆ {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}) |
63 | | ssfi 8180 |
. . . . . . 7
⊢ (({𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁} ∈ Fin ∧ 𝑥 ⊆ {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}) → 𝑥 ∈ Fin) |
64 | 61, 62, 63 | syl2an 494 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ 𝑥 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}) → 𝑥 ∈ Fin) |
65 | | hashcl 13147 |
. . . . . 6
⊢ (𝑥 ∈ Fin →
(#‘𝑥) ∈
ℕ0) |
66 | 64, 65 | syl 17 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ 𝑥 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}) → (#‘𝑥) ∈
ℕ0) |
67 | | expcl 12878 |
. . . . 5
⊢ ((-1
∈ ℂ ∧ (#‘𝑥) ∈ ℕ0) →
(-1↑(#‘𝑥))
∈ ℂ) |
68 | 60, 66, 67 | sylancr 695 |
. . . 4
⊢ ((𝑁 ∈ ℕ ∧ 𝑥 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}) → (-1↑(#‘𝑥)) ∈
ℂ) |
69 | 39, 41, 50, 59, 68 | fsumf1o 14454 |
. . 3
⊢ (𝑁 ∈ ℕ →
Σ𝑥 ∈ 𝒫
{𝑝 ∈ ℙ ∣
𝑝 ∥ 𝑁} (-1↑(#‘𝑥)) = Σ𝑘 ∈ {𝑛 ∈ ℕ ∣ ((μ‘𝑛) ≠ 0 ∧ 𝑛 ∥ 𝑁)} (-1↑(#‘{𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑘}))) |
70 | | fzfid 12772 |
. . . . 5
⊢ (𝑁 ∈ ℕ →
(0...(#‘{𝑝 ∈
ℙ ∣ 𝑝 ∥
𝑁})) ∈
Fin) |
71 | 61 | adantr 481 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ 𝑧 ∈ (0...(#‘{𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}))) → {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁} ∈ Fin) |
72 | | pwfi 8261 |
. . . . . . 7
⊢ ({𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁} ∈ Fin ↔ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁} ∈ Fin) |
73 | 71, 72 | sylib 208 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ 𝑧 ∈ (0...(#‘{𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}))) → 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁} ∈ Fin) |
74 | | ssrab2 3687 |
. . . . . 6
⊢ {𝑠 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁} ∣ (#‘𝑠) = 𝑧} ⊆ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁} |
75 | | ssfi 8180 |
. . . . . 6
⊢
((𝒫 {𝑝
∈ ℙ ∣ 𝑝
∥ 𝑁} ∈ Fin ∧
{𝑠 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁} ∣ (#‘𝑠) = 𝑧} ⊆ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}) → {𝑠 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁} ∣ (#‘𝑠) = 𝑧} ∈ Fin) |
76 | 73, 74, 75 | sylancl 694 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ 𝑧 ∈ (0...(#‘{𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}))) → {𝑠 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁} ∣ (#‘𝑠) = 𝑧} ∈ Fin) |
77 | | simprr 796 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ (𝑧 ∈ (0...(#‘{𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁})) ∧ 𝑥 ∈ {𝑠 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁} ∣ (#‘𝑠) = 𝑧})) → 𝑥 ∈ {𝑠 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁} ∣ (#‘𝑠) = 𝑧}) |
78 | | fveq2 6191 |
. . . . . . . . . . 11
⊢ (𝑠 = 𝑥 → (#‘𝑠) = (#‘𝑥)) |
79 | 78 | eqeq1d 2624 |
. . . . . . . . . 10
⊢ (𝑠 = 𝑥 → ((#‘𝑠) = 𝑧 ↔ (#‘𝑥) = 𝑧)) |
80 | 79 | elrab 3363 |
. . . . . . . . 9
⊢ (𝑥 ∈ {𝑠 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁} ∣ (#‘𝑠) = 𝑧} ↔ (𝑥 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁} ∧ (#‘𝑥) = 𝑧)) |
81 | 80 | simprbi 480 |
. . . . . . . 8
⊢ (𝑥 ∈ {𝑠 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁} ∣ (#‘𝑠) = 𝑧} → (#‘𝑥) = 𝑧) |
82 | 77, 81 | syl 17 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ (𝑧 ∈ (0...(#‘{𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁})) ∧ 𝑥 ∈ {𝑠 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁} ∣ (#‘𝑠) = 𝑧})) → (#‘𝑥) = 𝑧) |
83 | 82 | ralrimivva 2971 |
. . . . . 6
⊢ (𝑁 ∈ ℕ →
∀𝑧 ∈
(0...(#‘{𝑝 ∈
ℙ ∣ 𝑝 ∥
𝑁}))∀𝑥 ∈ {𝑠 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁} ∣ (#‘𝑠) = 𝑧} (#‘𝑥) = 𝑧) |
84 | | invdisj 4638 |
. . . . . 6
⊢
(∀𝑧 ∈
(0...(#‘{𝑝 ∈
ℙ ∣ 𝑝 ∥
𝑁}))∀𝑥 ∈ {𝑠 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁} ∣ (#‘𝑠) = 𝑧} (#‘𝑥) = 𝑧 → Disj 𝑧 ∈ (0...(#‘{𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁})){𝑠 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁} ∣ (#‘𝑠) = 𝑧}) |
85 | 83, 84 | syl 17 |
. . . . 5
⊢ (𝑁 ∈ ℕ →
Disj 𝑧 ∈
(0...(#‘{𝑝 ∈
ℙ ∣ 𝑝 ∥
𝑁})){𝑠 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁} ∣ (#‘𝑠) = 𝑧}) |
86 | 61 | adantr 481 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ (𝑧 ∈ (0...(#‘{𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁})) ∧ 𝑥 ∈ {𝑠 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁} ∣ (#‘𝑠) = 𝑧})) → {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁} ∈ Fin) |
87 | 74, 77 | sseldi 3601 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ (𝑧 ∈ (0...(#‘{𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁})) ∧ 𝑥 ∈ {𝑠 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁} ∣ (#‘𝑠) = 𝑧})) → 𝑥 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}) |
88 | 87, 62 | syl 17 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ (𝑧 ∈ (0...(#‘{𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁})) ∧ 𝑥 ∈ {𝑠 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁} ∣ (#‘𝑠) = 𝑧})) → 𝑥 ⊆ {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}) |
89 | 86, 88, 63 | syl2anc 693 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ (𝑧 ∈ (0...(#‘{𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁})) ∧ 𝑥 ∈ {𝑠 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁} ∣ (#‘𝑠) = 𝑧})) → 𝑥 ∈ Fin) |
90 | 89, 65 | syl 17 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ (𝑧 ∈ (0...(#‘{𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁})) ∧ 𝑥 ∈ {𝑠 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁} ∣ (#‘𝑠) = 𝑧})) → (#‘𝑥) ∈
ℕ0) |
91 | 60, 90, 67 | sylancr 695 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ (𝑧 ∈ (0...(#‘{𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁})) ∧ 𝑥 ∈ {𝑠 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁} ∣ (#‘𝑠) = 𝑧})) → (-1↑(#‘𝑥)) ∈
ℂ) |
92 | 70, 76, 85, 91 | fsumiun 14553 |
. . . 4
⊢ (𝑁 ∈ ℕ →
Σ𝑥 ∈ ∪ 𝑧 ∈ (0...(#‘{𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁})){𝑠 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁} ∣ (#‘𝑠) = 𝑧} (-1↑(#‘𝑥)) = Σ𝑧 ∈ (0...(#‘{𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}))Σ𝑥 ∈ {𝑠 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁} ∣ (#‘𝑠) = 𝑧} (-1↑(#‘𝑥))) |
93 | 61 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ ∧ 𝑠 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}) → {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁} ∈ Fin) |
94 | | elpwi 4168 |
. . . . . . . . . . . . 13
⊢ (𝑠 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁} → 𝑠 ⊆ {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}) |
95 | 94 | adantl 482 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ ∧ 𝑠 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}) → 𝑠 ⊆ {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}) |
96 | | ssdomg 8001 |
. . . . . . . . . . . 12
⊢ ({𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁} ∈ Fin → (𝑠 ⊆ {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁} → 𝑠 ≼ {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁})) |
97 | 93, 95, 96 | sylc 65 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ 𝑠 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}) → 𝑠 ≼ {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}) |
98 | | ssfi 8180 |
. . . . . . . . . . . . 13
⊢ (({𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁} ∈ Fin ∧ 𝑠 ⊆ {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}) → 𝑠 ∈ Fin) |
99 | 61, 94, 98 | syl2an 494 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ ∧ 𝑠 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}) → 𝑠 ∈ Fin) |
100 | | hashdom 13168 |
. . . . . . . . . . . 12
⊢ ((𝑠 ∈ Fin ∧ {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁} ∈ Fin) → ((#‘𝑠) ≤ (#‘{𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}) ↔ 𝑠 ≼ {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁})) |
101 | 99, 93, 100 | syl2anc 693 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ 𝑠 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}) → ((#‘𝑠) ≤ (#‘{𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}) ↔ 𝑠 ≼ {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁})) |
102 | 97, 101 | mpbird 247 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ 𝑠 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}) → (#‘𝑠) ≤ (#‘{𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁})) |
103 | | hashcl 13147 |
. . . . . . . . . . . . 13
⊢ (𝑠 ∈ Fin →
(#‘𝑠) ∈
ℕ0) |
104 | 99, 103 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ ∧ 𝑠 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}) → (#‘𝑠) ∈
ℕ0) |
105 | | nn0uz 11722 |
. . . . . . . . . . . 12
⊢
ℕ0 = (ℤ≥‘0) |
106 | 104, 105 | syl6eleq 2711 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ 𝑠 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}) → (#‘𝑠) ∈
(ℤ≥‘0)) |
107 | | hashcl 13147 |
. . . . . . . . . . . . . 14
⊢ ({𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁} ∈ Fin → (#‘{𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}) ∈
ℕ0) |
108 | 61, 107 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℕ →
(#‘{𝑝 ∈ ℙ
∣ 𝑝 ∥ 𝑁}) ∈
ℕ0) |
109 | 108 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ ∧ 𝑠 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}) → (#‘{𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}) ∈
ℕ0) |
110 | 109 | nn0zd 11480 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ 𝑠 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}) → (#‘{𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}) ∈ ℤ) |
111 | | elfz5 12334 |
. . . . . . . . . . 11
⊢
(((#‘𝑠) ∈
(ℤ≥‘0) ∧ (#‘{𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}) ∈ ℤ) → ((#‘𝑠) ∈ (0...(#‘{𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁})) ↔ (#‘𝑠) ≤ (#‘{𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}))) |
112 | 106, 110,
111 | syl2anc 693 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ 𝑠 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}) → ((#‘𝑠) ∈ (0...(#‘{𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁})) ↔ (#‘𝑠) ≤ (#‘{𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}))) |
113 | 102, 112 | mpbird 247 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ 𝑠 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}) → (#‘𝑠) ∈ (0...(#‘{𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}))) |
114 | | eqidd 2623 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ 𝑠 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}) → (#‘𝑠) = (#‘𝑠)) |
115 | | eqeq2 2633 |
. . . . . . . . . 10
⊢ (𝑧 = (#‘𝑠) → ((#‘𝑠) = 𝑧 ↔ (#‘𝑠) = (#‘𝑠))) |
116 | 115 | rspcev 3309 |
. . . . . . . . 9
⊢
(((#‘𝑠) ∈
(0...(#‘{𝑝 ∈
ℙ ∣ 𝑝 ∥
𝑁})) ∧ (#‘𝑠) = (#‘𝑠)) → ∃𝑧 ∈ (0...(#‘{𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}))(#‘𝑠) = 𝑧) |
117 | 113, 114,
116 | syl2anc 693 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝑠 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}) → ∃𝑧 ∈ (0...(#‘{𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}))(#‘𝑠) = 𝑧) |
118 | 117 | ralrimiva 2966 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ →
∀𝑠 ∈ 𝒫
{𝑝 ∈ ℙ ∣
𝑝 ∥ 𝑁}∃𝑧 ∈ (0...(#‘{𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}))(#‘𝑠) = 𝑧) |
119 | | rabid2 3118 |
. . . . . . 7
⊢
(𝒫 {𝑝 ∈
ℙ ∣ 𝑝 ∥
𝑁} = {𝑠 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁} ∣ ∃𝑧 ∈ (0...(#‘{𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}))(#‘𝑠) = 𝑧} ↔ ∀𝑠 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}∃𝑧 ∈ (0...(#‘{𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}))(#‘𝑠) = 𝑧) |
120 | 118, 119 | sylibr 224 |
. . . . . 6
⊢ (𝑁 ∈ ℕ → 𝒫
{𝑝 ∈ ℙ ∣
𝑝 ∥ 𝑁} = {𝑠 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁} ∣ ∃𝑧 ∈ (0...(#‘{𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}))(#‘𝑠) = 𝑧}) |
121 | | iunrab 4567 |
. . . . . 6
⊢ ∪ 𝑧 ∈ (0...(#‘{𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁})){𝑠 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁} ∣ (#‘𝑠) = 𝑧} = {𝑠 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁} ∣ ∃𝑧 ∈ (0...(#‘{𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}))(#‘𝑠) = 𝑧} |
122 | 120, 121 | syl6reqr 2675 |
. . . . 5
⊢ (𝑁 ∈ ℕ → ∪ 𝑧 ∈ (0...(#‘{𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁})){𝑠 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁} ∣ (#‘𝑠) = 𝑧} = 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}) |
123 | 122 | sumeq1d 14431 |
. . . 4
⊢ (𝑁 ∈ ℕ →
Σ𝑥 ∈ ∪ 𝑧 ∈ (0...(#‘{𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁})){𝑠 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁} ∣ (#‘𝑠) = 𝑧} (-1↑(#‘𝑥)) = Σ𝑥 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁} (-1↑(#‘𝑥))) |
124 | | elfznn0 12433 |
. . . . . . . . . 10
⊢ (𝑧 ∈ (0...(#‘{𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁})) → 𝑧 ∈ ℕ0) |
125 | 124 | adantl 482 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ 𝑧 ∈ (0...(#‘{𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}))) → 𝑧 ∈ ℕ0) |
126 | | expcl 12878 |
. . . . . . . . 9
⊢ ((-1
∈ ℂ ∧ 𝑧
∈ ℕ0) → (-1↑𝑧) ∈ ℂ) |
127 | 60, 125, 126 | sylancr 695 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝑧 ∈ (0...(#‘{𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}))) → (-1↑𝑧) ∈ ℂ) |
128 | | fsumconst 14522 |
. . . . . . . 8
⊢ (({𝑠 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁} ∣ (#‘𝑠) = 𝑧} ∈ Fin ∧ (-1↑𝑧) ∈ ℂ) →
Σ𝑥 ∈ {𝑠 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁} ∣ (#‘𝑠) = 𝑧} (-1↑𝑧) = ((#‘{𝑠 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁} ∣ (#‘𝑠) = 𝑧}) · (-1↑𝑧))) |
129 | 76, 127, 128 | syl2anc 693 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ 𝑧 ∈ (0...(#‘{𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}))) → Σ𝑥 ∈ {𝑠 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁} ∣ (#‘𝑠) = 𝑧} (-1↑𝑧) = ((#‘{𝑠 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁} ∣ (#‘𝑠) = 𝑧}) · (-1↑𝑧))) |
130 | 81 | adantl 482 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ ∧ 𝑧 ∈ (0...(#‘{𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}))) ∧ 𝑥 ∈ {𝑠 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁} ∣ (#‘𝑠) = 𝑧}) → (#‘𝑥) = 𝑧) |
131 | 130 | oveq2d 6666 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ ∧ 𝑧 ∈ (0...(#‘{𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}))) ∧ 𝑥 ∈ {𝑠 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁} ∣ (#‘𝑠) = 𝑧}) → (-1↑(#‘𝑥)) = (-1↑𝑧)) |
132 | 131 | sumeq2dv 14433 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ 𝑧 ∈ (0...(#‘{𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}))) → Σ𝑥 ∈ {𝑠 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁} ∣ (#‘𝑠) = 𝑧} (-1↑(#‘𝑥)) = Σ𝑥 ∈ {𝑠 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁} ∣ (#‘𝑠) = 𝑧} (-1↑𝑧)) |
133 | | elfzelz 12342 |
. . . . . . . . 9
⊢ (𝑧 ∈ (0...(#‘{𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁})) → 𝑧 ∈ ℤ) |
134 | | hashbc 13237 |
. . . . . . . . 9
⊢ (({𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁} ∈ Fin ∧ 𝑧 ∈ ℤ) → ((#‘{𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁})C𝑧) = (#‘{𝑠 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁} ∣ (#‘𝑠) = 𝑧})) |
135 | 61, 133, 134 | syl2an 494 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝑧 ∈ (0...(#‘{𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}))) → ((#‘{𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁})C𝑧) = (#‘{𝑠 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁} ∣ (#‘𝑠) = 𝑧})) |
136 | 135 | oveq1d 6665 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ 𝑧 ∈ (0...(#‘{𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}))) → (((#‘{𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁})C𝑧) · (-1↑𝑧)) = ((#‘{𝑠 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁} ∣ (#‘𝑠) = 𝑧}) · (-1↑𝑧))) |
137 | 129, 132,
136 | 3eqtr4d 2666 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ 𝑧 ∈ (0...(#‘{𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}))) → Σ𝑥 ∈ {𝑠 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁} ∣ (#‘𝑠) = 𝑧} (-1↑(#‘𝑥)) = (((#‘{𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁})C𝑧) · (-1↑𝑧))) |
138 | 137 | sumeq2dv 14433 |
. . . . 5
⊢ (𝑁 ∈ ℕ →
Σ𝑧 ∈
(0...(#‘{𝑝 ∈
ℙ ∣ 𝑝 ∥
𝑁}))Σ𝑥 ∈ {𝑠 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁} ∣ (#‘𝑠) = 𝑧} (-1↑(#‘𝑥)) = Σ𝑧 ∈ (0...(#‘{𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}))(((#‘{𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁})C𝑧) · (-1↑𝑧))) |
139 | | 1pneg1e0 11129 |
. . . . . . 7
⊢ (1 + -1)
= 0 |
140 | 139 | oveq1i 6660 |
. . . . . 6
⊢ ((1 +
-1)↑(#‘{𝑝 ∈
ℙ ∣ 𝑝 ∥
𝑁})) =
(0↑(#‘{𝑝 ∈
ℙ ∣ 𝑝 ∥
𝑁})) |
141 | | binom1p 14563 |
. . . . . . 7
⊢ ((-1
∈ ℂ ∧ (#‘{𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}) ∈ ℕ0) → ((1 +
-1)↑(#‘{𝑝 ∈
ℙ ∣ 𝑝 ∥
𝑁})) = Σ𝑧 ∈ (0...(#‘{𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}))(((#‘{𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁})C𝑧) · (-1↑𝑧))) |
142 | 60, 108, 141 | sylancr 695 |
. . . . . 6
⊢ (𝑁 ∈ ℕ → ((1 +
-1)↑(#‘{𝑝 ∈
ℙ ∣ 𝑝 ∥
𝑁})) = Σ𝑧 ∈ (0...(#‘{𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}))(((#‘{𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁})C𝑧) · (-1↑𝑧))) |
143 | 140, 142 | syl5eqr 2670 |
. . . . 5
⊢ (𝑁 ∈ ℕ →
(0↑(#‘{𝑝 ∈
ℙ ∣ 𝑝 ∥
𝑁})) = Σ𝑧 ∈ (0...(#‘{𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}))(((#‘{𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁})C𝑧) · (-1↑𝑧))) |
144 | | eqeq2 2633 |
. . . . . 6
⊢ (1 =
if(𝑁 = 1, 1, 0) →
((0↑(#‘{𝑝 ∈
ℙ ∣ 𝑝 ∥
𝑁})) = 1 ↔
(0↑(#‘{𝑝 ∈
ℙ ∣ 𝑝 ∥
𝑁})) = if(𝑁 = 1, 1, 0))) |
145 | | eqeq2 2633 |
. . . . . 6
⊢ (0 =
if(𝑁 = 1, 1, 0) →
((0↑(#‘{𝑝 ∈
ℙ ∣ 𝑝 ∥
𝑁})) = 0 ↔
(0↑(#‘{𝑝 ∈
ℙ ∣ 𝑝 ∥
𝑁})) = if(𝑁 = 1, 1, 0))) |
146 | | nprmdvds1 15418 |
. . . . . . . . . . . . 13
⊢ (𝑝 ∈ ℙ → ¬
𝑝 ∥
1) |
147 | | simpr 477 |
. . . . . . . . . . . . . . 15
⊢ ((𝑁 ∈ ℕ ∧ 𝑁 = 1) → 𝑁 = 1) |
148 | 147 | breq2d 4665 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℕ ∧ 𝑁 = 1) → (𝑝 ∥ 𝑁 ↔ 𝑝 ∥ 1)) |
149 | 148 | notbid 308 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℕ ∧ 𝑁 = 1) → (¬ 𝑝 ∥ 𝑁 ↔ ¬ 𝑝 ∥ 1)) |
150 | 146, 149 | syl5ibr 236 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ ∧ 𝑁 = 1) → (𝑝 ∈ ℙ → ¬ 𝑝 ∥ 𝑁)) |
151 | 150 | ralrimiv 2965 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ 𝑁 = 1) → ∀𝑝 ∈ ℙ ¬ 𝑝 ∥ 𝑁) |
152 | | rabeq0 3957 |
. . . . . . . . . . 11
⊢ ({𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁} = ∅ ↔ ∀𝑝 ∈ ℙ ¬ 𝑝 ∥ 𝑁) |
153 | 151, 152 | sylibr 224 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ 𝑁 = 1) → {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁} = ∅) |
154 | 153 | fveq2d 6195 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ 𝑁 = 1) → (#‘{𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}) = (#‘∅)) |
155 | | hash0 13158 |
. . . . . . . . 9
⊢
(#‘∅) = 0 |
156 | 154, 155 | syl6eq 2672 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝑁 = 1) → (#‘{𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}) = 0) |
157 | 156 | oveq2d 6666 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ 𝑁 = 1) →
(0↑(#‘{𝑝 ∈
ℙ ∣ 𝑝 ∥
𝑁})) =
(0↑0)) |
158 | | 0exp0e1 12865 |
. . . . . . 7
⊢
(0↑0) = 1 |
159 | 157, 158 | syl6eq 2672 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ 𝑁 = 1) →
(0↑(#‘{𝑝 ∈
ℙ ∣ 𝑝 ∥
𝑁})) = 1) |
160 | | df-ne 2795 |
. . . . . . . . . . 11
⊢ (𝑁 ≠ 1 ↔ ¬ 𝑁 = 1) |
161 | | eluz2b3 11762 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈
(ℤ≥‘2) ↔ (𝑁 ∈ ℕ ∧ 𝑁 ≠ 1)) |
162 | 161 | biimpri 218 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ 𝑁 ≠ 1) → 𝑁 ∈
(ℤ≥‘2)) |
163 | 160, 162 | sylan2br 493 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ ¬
𝑁 = 1) → 𝑁 ∈
(ℤ≥‘2)) |
164 | | exprmfct 15416 |
. . . . . . . . . 10
⊢ (𝑁 ∈
(ℤ≥‘2) → ∃𝑝 ∈ ℙ 𝑝 ∥ 𝑁) |
165 | 163, 164 | syl 17 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ ¬
𝑁 = 1) → ∃𝑝 ∈ ℙ 𝑝 ∥ 𝑁) |
166 | | rabn0 3958 |
. . . . . . . . 9
⊢ ({𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁} ≠ ∅ ↔ ∃𝑝 ∈ ℙ 𝑝 ∥ 𝑁) |
167 | 165, 166 | sylibr 224 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ ¬
𝑁 = 1) → {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁} ≠ ∅) |
168 | 61 | adantr 481 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ ¬
𝑁 = 1) → {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁} ∈ Fin) |
169 | | hashnncl 13157 |
. . . . . . . . 9
⊢ ({𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁} ∈ Fin → ((#‘{𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁}) ∈ ℕ ↔ {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁} ≠ ∅)) |
170 | 168, 169 | syl 17 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ ¬
𝑁 = 1) →
((#‘{𝑝 ∈ ℙ
∣ 𝑝 ∥ 𝑁}) ∈ ℕ ↔ {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁} ≠ ∅)) |
171 | 167, 170 | mpbird 247 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ ¬
𝑁 = 1) →
(#‘{𝑝 ∈ ℙ
∣ 𝑝 ∥ 𝑁}) ∈
ℕ) |
172 | 171 | 0expd 13024 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ ¬
𝑁 = 1) →
(0↑(#‘{𝑝 ∈
ℙ ∣ 𝑝 ∥
𝑁})) = 0) |
173 | 144, 145,
159, 172 | ifbothda 4123 |
. . . . 5
⊢ (𝑁 ∈ ℕ →
(0↑(#‘{𝑝 ∈
ℙ ∣ 𝑝 ∥
𝑁})) = if(𝑁 = 1, 1, 0)) |
174 | 138, 143,
173 | 3eqtr2d 2662 |
. . . 4
⊢ (𝑁 ∈ ℕ →
Σ𝑧 ∈
(0...(#‘{𝑝 ∈
ℙ ∣ 𝑝 ∥
𝑁}))Σ𝑥 ∈ {𝑠 ∈ 𝒫 {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑁} ∣ (#‘𝑠) = 𝑧} (-1↑(#‘𝑥)) = if(𝑁 = 1, 1, 0)) |
175 | 92, 123, 174 | 3eqtr3d 2664 |
. . 3
⊢ (𝑁 ∈ ℕ →
Σ𝑥 ∈ 𝒫
{𝑝 ∈ ℙ ∣
𝑝 ∥ 𝑁} (-1↑(#‘𝑥)) = if(𝑁 = 1, 1, 0)) |
176 | 69, 175 | eqtr3d 2658 |
. 2
⊢ (𝑁 ∈ ℕ →
Σ𝑘 ∈ {𝑛 ∈ ℕ ∣
((μ‘𝑛) ≠ 0
∧ 𝑛 ∥ 𝑁)} (-1↑(#‘{𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑘})) = if(𝑁 = 1, 1, 0)) |
177 | 10, 37, 176 | 3eqtr3d 2664 |
1
⊢ (𝑁 ∈ ℕ →
Σ𝑘 ∈ {𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑁} (μ‘𝑘) = if(𝑁 = 1, 1, 0)) |