Step | Hyp | Ref
| Expression |
1 | | cnvimass 6086 |
. . . . . . . 8
⊢ (◡(𝐺‘𝐴) “ ℕ) ⊆ dom (𝐺‘𝐴) |
2 | | eulerpart.p |
. . . . . . . . . . . . . 14
⊢ 𝑃 = {𝑓 ∈ (ℕ0
↑m ℕ) ∣ ((◡𝑓 “ ℕ) ∈ Fin ∧
Σ𝑘 ∈ ℕ
((𝑓‘𝑘) · 𝑘) = 𝑁)} |
3 | | eulerpart.o |
. . . . . . . . . . . . . 14
⊢ 𝑂 = {𝑔 ∈ 𝑃 ∣ ∀𝑛 ∈ (◡𝑔 “ ℕ) ¬ 2 ∥ 𝑛} |
4 | | eulerpart.d |
. . . . . . . . . . . . . 14
⊢ 𝐷 = {𝑔 ∈ 𝑃 ∣ ∀𝑛 ∈ ℕ (𝑔‘𝑛) ≤ 1} |
5 | | eulerpart.j |
. . . . . . . . . . . . . 14
⊢ 𝐽 = {𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧} |
6 | | eulerpart.f |
. . . . . . . . . . . . . 14
⊢ 𝐹 = (𝑥 ∈ 𝐽, 𝑦 ∈ ℕ0 ↦
((2↑𝑦) · 𝑥)) |
7 | | eulerpart.h |
. . . . . . . . . . . . . 14
⊢ 𝐻 = {𝑟 ∈ ((𝒫 ℕ0 ∩
Fin) ↑m 𝐽)
∣ (𝑟 supp ∅)
∈ Fin} |
8 | | eulerpart.m |
. . . . . . . . . . . . . 14
⊢ 𝑀 = (𝑟 ∈ 𝐻 ↦ {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ (𝑟‘𝑥))}) |
9 | | eulerpart.r |
. . . . . . . . . . . . . 14
⊢ 𝑅 = {𝑓 ∣ (◡𝑓 “ ℕ) ∈
Fin} |
10 | | eulerpart.t |
. . . . . . . . . . . . . 14
⊢ 𝑇 = {𝑓 ∈ (ℕ0
↑m ℕ) ∣ (◡𝑓 “ ℕ) ⊆ 𝐽} |
11 | | eulerpart.g |
. . . . . . . . . . . . . 14
⊢ 𝐺 = (𝑜 ∈ (𝑇 ∩ 𝑅) ↦
((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))))) |
12 | 2, 3, 4, 5, 6, 7, 8, 9, 10, 11 | eulerpartgbij 34125 |
. . . . . . . . . . . . 13
⊢ 𝐺:(𝑇 ∩ 𝑅)–1-1-onto→(({0,
1} ↑m ℕ) ∩ 𝑅) |
13 | | f1of 6838 |
. . . . . . . . . . . . 13
⊢ (𝐺:(𝑇 ∩ 𝑅)–1-1-onto→(({0,
1} ↑m ℕ) ∩ 𝑅) → 𝐺:(𝑇 ∩ 𝑅)⟶(({0, 1} ↑m
ℕ) ∩ 𝑅)) |
14 | 12, 13 | ax-mp 5 |
. . . . . . . . . . . 12
⊢ 𝐺:(𝑇 ∩ 𝑅)⟶(({0, 1} ↑m
ℕ) ∩ 𝑅) |
15 | 14 | ffvelcdmi 7092 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → (𝐺‘𝐴) ∈ (({0, 1} ↑m
ℕ) ∩ 𝑅)) |
16 | | elin 3960 |
. . . . . . . . . . 11
⊢ ((𝐺‘𝐴) ∈ (({0, 1} ↑m
ℕ) ∩ 𝑅) ↔
((𝐺‘𝐴) ∈ ({0, 1} ↑m ℕ)
∧ (𝐺‘𝐴) ∈ 𝑅)) |
17 | 15, 16 | sylib 217 |
. . . . . . . . . 10
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → ((𝐺‘𝐴) ∈ ({0, 1} ↑m ℕ)
∧ (𝐺‘𝐴) ∈ 𝑅)) |
18 | 17 | simpld 493 |
. . . . . . . . 9
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → (𝐺‘𝐴) ∈ ({0, 1} ↑m
ℕ)) |
19 | | elmapi 8868 |
. . . . . . . . 9
⊢ ((𝐺‘𝐴) ∈ ({0, 1} ↑m ℕ)
→ (𝐺‘𝐴):ℕ⟶{0,
1}) |
20 | | fdm 6732 |
. . . . . . . . 9
⊢ ((𝐺‘𝐴):ℕ⟶{0, 1} → dom (𝐺‘𝐴) = ℕ) |
21 | 18, 19, 20 | 3syl 18 |
. . . . . . . 8
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → dom (𝐺‘𝐴) = ℕ) |
22 | 1, 21 | sseqtrid 4029 |
. . . . . . 7
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → (◡(𝐺‘𝐴) “ ℕ) ⊆
ℕ) |
23 | 22 | sselda 3976 |
. . . . . 6
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑘 ∈ (◡(𝐺‘𝐴) “ ℕ)) → 𝑘 ∈
ℕ) |
24 | 2, 3, 4, 5, 6, 7, 8, 9, 10, 11 | eulerpartlemgvv 34129 |
. . . . . . 7
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑘 ∈ ℕ) → ((𝐺‘𝐴)‘𝑘) = if(∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑘, 1, 0)) |
25 | 24 | oveq1d 7434 |
. . . . . 6
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑘 ∈ ℕ) → (((𝐺‘𝐴)‘𝑘) · 𝑘) = (if(∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑘, 1, 0) · 𝑘)) |
26 | 23, 25 | syldan 589 |
. . . . 5
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑘 ∈ (◡(𝐺‘𝐴) “ ℕ)) → (((𝐺‘𝐴)‘𝑘) · 𝑘) = (if(∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑘, 1, 0) · 𝑘)) |
27 | 26 | sumeq2dv 15690 |
. . . 4
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → Σ𝑘 ∈ (◡(𝐺‘𝐴) “ ℕ)(((𝐺‘𝐴)‘𝑘) · 𝑘) = Σ𝑘 ∈ (◡(𝐺‘𝐴) “ ℕ)(if(∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑘, 1, 0) · 𝑘)) |
28 | | eqeq2 2737 |
. . . . . . . . . . . . 13
⊢ (𝑚 = 𝑘 → (((2↑𝑛) · 𝑡) = 𝑚 ↔ ((2↑𝑛) · 𝑡) = 𝑘)) |
29 | 28 | 2rexbidv 3209 |
. . . . . . . . . . . 12
⊢ (𝑚 = 𝑘 → (∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚 ↔ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑘)) |
30 | 29 | elrab 3679 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚} ↔ (𝑘 ∈ ℕ ∧ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑘)) |
31 | 30 | simprbi 495 |
. . . . . . . . . 10
⊢ (𝑘 ∈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚} → ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑘) |
32 | 31 | iftrued 4538 |
. . . . . . . . 9
⊢ (𝑘 ∈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚} → if(∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑘, 1, 0) = 1) |
33 | 32 | oveq1d 7434 |
. . . . . . . 8
⊢ (𝑘 ∈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚} → (if(∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑘, 1, 0) · 𝑘) = (1 · 𝑘)) |
34 | | elrabi 3673 |
. . . . . . . . . 10
⊢ (𝑘 ∈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚} → 𝑘 ∈ ℕ) |
35 | 34 | nncnd 12266 |
. . . . . . . . 9
⊢ (𝑘 ∈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚} → 𝑘 ∈ ℂ) |
36 | 35 | mullidd 11269 |
. . . . . . . 8
⊢ (𝑘 ∈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚} → (1 · 𝑘) = 𝑘) |
37 | 33, 36 | eqtrd 2765 |
. . . . . . 7
⊢ (𝑘 ∈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚} → (if(∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑘, 1, 0) · 𝑘) = 𝑘) |
38 | 37 | sumeq2i 15686 |
. . . . . 6
⊢
Σ𝑘 ∈
{𝑚 ∈ ℕ ∣
∃𝑡 ∈ ℕ
∃𝑛 ∈
(bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚} (if(∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑘, 1, 0) · 𝑘) = Σ𝑘 ∈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚}𝑘 |
39 | | id 22 |
. . . . . . 7
⊢ (𝑘 = ((2↑(2nd
‘𝑤)) ·
(1st ‘𝑤))
→ 𝑘 =
((2↑(2nd ‘𝑤)) · (1st ‘𝑤))) |
40 | 2, 3, 4, 5, 6, 7, 8, 9, 10, 11 | eulerpartlemgf 34132 |
. . . . . . . . 9
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → (◡(𝐺‘𝐴) “ ℕ) ∈
Fin) |
41 | 34 | adantl 480 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑘 ∈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚}) → 𝑘 ∈ ℕ) |
42 | 41, 24 | syldan 589 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑘 ∈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚}) → ((𝐺‘𝐴)‘𝑘) = if(∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑘, 1, 0)) |
43 | 31 | adantl 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑘 ∈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚}) → ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑘) |
44 | 43 | iftrued 4538 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑘 ∈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚}) → if(∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑘, 1, 0) = 1) |
45 | 42, 44 | eqtrd 2765 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑘 ∈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚}) → ((𝐺‘𝐴)‘𝑘) = 1) |
46 | | 1nn 12261 |
. . . . . . . . . . . . 13
⊢ 1 ∈
ℕ |
47 | 45, 46 | eqeltrdi 2833 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑘 ∈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚}) → ((𝐺‘𝐴)‘𝑘) ∈ ℕ) |
48 | | ffn 6723 |
. . . . . . . . . . . . . 14
⊢ ((𝐺‘𝐴):ℕ⟶{0, 1} → (𝐺‘𝐴) Fn ℕ) |
49 | | elpreima 7066 |
. . . . . . . . . . . . . 14
⊢ ((𝐺‘𝐴) Fn ℕ → (𝑘 ∈ (◡(𝐺‘𝐴) “ ℕ) ↔ (𝑘 ∈ ℕ ∧ ((𝐺‘𝐴)‘𝑘) ∈ ℕ))) |
50 | 18, 19, 48, 49 | 4syl 19 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → (𝑘 ∈ (◡(𝐺‘𝐴) “ ℕ) ↔ (𝑘 ∈ ℕ ∧ ((𝐺‘𝐴)‘𝑘) ∈ ℕ))) |
51 | 50 | adantr 479 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑘 ∈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚}) → (𝑘 ∈ (◡(𝐺‘𝐴) “ ℕ) ↔ (𝑘 ∈ ℕ ∧ ((𝐺‘𝐴)‘𝑘) ∈ ℕ))) |
52 | 41, 47, 51 | mpbir2and 711 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑘 ∈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚}) → 𝑘 ∈ (◡(𝐺‘𝐴) “ ℕ)) |
53 | 52 | ex 411 |
. . . . . . . . . 10
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → (𝑘 ∈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚} → 𝑘 ∈ (◡(𝐺‘𝐴) “ ℕ))) |
54 | 53 | ssrdv 3982 |
. . . . . . . . 9
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚} ⊆ (◡(𝐺‘𝐴) “ ℕ)) |
55 | | ssfi 9201 |
. . . . . . . . 9
⊢ (((◡(𝐺‘𝐴) “ ℕ) ∈ Fin ∧ {𝑚 ∈ ℕ ∣
∃𝑡 ∈ ℕ
∃𝑛 ∈
(bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚} ⊆ (◡(𝐺‘𝐴) “ ℕ)) → {𝑚 ∈ ℕ ∣
∃𝑡 ∈ ℕ
∃𝑛 ∈
(bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚} ∈ Fin) |
56 | 40, 54, 55 | syl2anc 582 |
. . . . . . . 8
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚} ∈ Fin) |
57 | | cnvexg 7932 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → ◡𝐴 ∈ V) |
58 | | imaexg 7921 |
. . . . . . . . . . 11
⊢ (◡𝐴 ∈ V → (◡𝐴 “ ℕ) ∈ V) |
59 | | inex1g 5320 |
. . . . . . . . . . 11
⊢ ((◡𝐴 “ ℕ) ∈ V → ((◡𝐴 “ ℕ) ∩ 𝐽) ∈ V) |
60 | 57, 58, 59 | 3syl 18 |
. . . . . . . . . 10
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → ((◡𝐴 “ ℕ) ∩ 𝐽) ∈ V) |
61 | | vsnex 5431 |
. . . . . . . . . . . 12
⊢ {𝑡} ∈ V |
62 | | fvex 6909 |
. . . . . . . . . . . 12
⊢
(bits‘(𝐴‘𝑡)) ∈ V |
63 | 61, 62 | xpex 7756 |
. . . . . . . . . . 11
⊢ ({𝑡} × (bits‘(𝐴‘𝑡))) ∈ V |
64 | 63 | rgenw 3054 |
. . . . . . . . . 10
⊢
∀𝑡 ∈
((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡))) ∈ V |
65 | | iunexg 7968 |
. . . . . . . . . 10
⊢ ((((◡𝐴 “ ℕ) ∩ 𝐽) ∈ V ∧ ∀𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡))) ∈ V) → ∪ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡))) ∈ V) |
66 | 60, 64, 65 | sylancl 584 |
. . . . . . . . 9
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → ∪
𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡))) ∈ V) |
67 | | eqid 2725 |
. . . . . . . . . 10
⊢ ∪ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡))) = ∪
𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡))) |
68 | 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 67 | eulerpartlemgh 34131 |
. . . . . . . . 9
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → (𝐹 ↾ ∪
𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡)))):∪
𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡)))–1-1-onto→{𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚}) |
69 | | f1oeng 8992 |
. . . . . . . . 9
⊢
((∪ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡))) ∈ V ∧ (𝐹 ↾ ∪
𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡)))):∪
𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡)))–1-1-onto→{𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚}) → ∪
𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡))) ≈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚}) |
70 | 66, 68, 69 | syl2anc 582 |
. . . . . . . 8
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → ∪
𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡))) ≈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚}) |
71 | | enfii 9217 |
. . . . . . . 8
⊢ (({𝑚 ∈ ℕ ∣
∃𝑡 ∈ ℕ
∃𝑛 ∈
(bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚} ∈ Fin ∧ ∪ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡))) ≈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚}) → ∪
𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡))) ∈ Fin) |
72 | 56, 70, 71 | syl2anc 582 |
. . . . . . 7
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → ∪
𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡))) ∈ Fin) |
73 | | fvres 6915 |
. . . . . . . . 9
⊢ (𝑤 ∈ ∪ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡))) → ((𝐹 ↾ ∪
𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡))))‘𝑤) = (𝐹‘𝑤)) |
74 | 73 | adantl 480 |
. . . . . . . 8
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑤 ∈ ∪
𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡)))) → ((𝐹 ↾ ∪
𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡))))‘𝑤) = (𝐹‘𝑤)) |
75 | | inss2 4228 |
. . . . . . . . . . . . . . 15
⊢ ((◡𝐴 “ ℕ) ∩ 𝐽) ⊆ 𝐽 |
76 | | simpr 483 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)) → 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)) |
77 | 75, 76 | sselid 3974 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)) → 𝑡 ∈ 𝐽) |
78 | 77 | snssd 4814 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)) → {𝑡} ⊆ 𝐽) |
79 | | bitsss 16409 |
. . . . . . . . . . . . 13
⊢
(bits‘(𝐴‘𝑡)) ⊆
ℕ0 |
80 | | xpss12 5693 |
. . . . . . . . . . . . 13
⊢ (({𝑡} ⊆ 𝐽 ∧ (bits‘(𝐴‘𝑡)) ⊆ ℕ0) →
({𝑡} ×
(bits‘(𝐴‘𝑡))) ⊆ (𝐽 ×
ℕ0)) |
81 | 78, 79, 80 | sylancl 584 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)) → ({𝑡} × (bits‘(𝐴‘𝑡))) ⊆ (𝐽 ×
ℕ0)) |
82 | 81 | ralrimiva 3135 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → ∀𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡))) ⊆ (𝐽 ×
ℕ0)) |
83 | | iunss 5049 |
. . . . . . . . . . 11
⊢ (∪ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡))) ⊆ (𝐽 × ℕ0) ↔
∀𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡))) ⊆ (𝐽 ×
ℕ0)) |
84 | 82, 83 | sylibr 233 |
. . . . . . . . . 10
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → ∪
𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡))) ⊆ (𝐽 ×
ℕ0)) |
85 | 84 | sselda 3976 |
. . . . . . . . 9
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑤 ∈ ∪
𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡)))) → 𝑤 ∈ (𝐽 ×
ℕ0)) |
86 | 5, 6 | oddpwdcv 34108 |
. . . . . . . . 9
⊢ (𝑤 ∈ (𝐽 × ℕ0) → (𝐹‘𝑤) = ((2↑(2nd ‘𝑤)) · (1st
‘𝑤))) |
87 | 85, 86 | syl 17 |
. . . . . . . 8
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑤 ∈ ∪
𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡)))) → (𝐹‘𝑤) = ((2↑(2nd ‘𝑤)) · (1st
‘𝑤))) |
88 | 74, 87 | eqtrd 2765 |
. . . . . . 7
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑤 ∈ ∪
𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡)))) → ((𝐹 ↾ ∪
𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡))))‘𝑤) = ((2↑(2nd ‘𝑤)) · (1st
‘𝑤))) |
89 | 41 | nncnd 12266 |
. . . . . . 7
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑘 ∈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚}) → 𝑘 ∈ ℂ) |
90 | 39, 72, 68, 88, 89 | fsumf1o 15710 |
. . . . . 6
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → Σ𝑘 ∈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚}𝑘 = Σ𝑤 ∈ ∪
𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡)))((2↑(2nd ‘𝑤)) · (1st
‘𝑤))) |
91 | 38, 90 | eqtrid 2777 |
. . . . 5
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → Σ𝑘 ∈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚} (if(∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑘, 1, 0) · 𝑘) = Σ𝑤 ∈ ∪
𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡)))((2↑(2nd ‘𝑤)) · (1st
‘𝑤))) |
92 | | ax-1cn 11203 |
. . . . . . . . 9
⊢ 1 ∈
ℂ |
93 | | 0cn 11243 |
. . . . . . . . 9
⊢ 0 ∈
ℂ |
94 | 92, 93 | ifcli 4577 |
. . . . . . . 8
⊢
if(∃𝑡 ∈
ℕ ∃𝑛 ∈
(bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑘, 1, 0) ∈ ℂ |
95 | 94 | a1i 11 |
. . . . . . 7
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑘 ∈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚}) → if(∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑘, 1, 0) ∈ ℂ) |
96 | | ssrab2 4073 |
. . . . . . . . 9
⊢ {𝑚 ∈ ℕ ∣
∃𝑡 ∈ ℕ
∃𝑛 ∈
(bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚} ⊆ ℕ |
97 | | simpr 483 |
. . . . . . . . 9
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑘 ∈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚}) → 𝑘 ∈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚}) |
98 | 96, 97 | sselid 3974 |
. . . . . . . 8
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑘 ∈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚}) → 𝑘 ∈ ℕ) |
99 | 98 | nncnd 12266 |
. . . . . . 7
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑘 ∈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚}) → 𝑘 ∈ ℂ) |
100 | 95, 99 | mulcld 11271 |
. . . . . 6
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑘 ∈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚}) → (if(∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑘, 1, 0) · 𝑘) ∈ ℂ) |
101 | | simpr 483 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑘 ∈ ((◡(𝐺‘𝐴) “ ℕ) ∖ {𝑚 ∈ ℕ ∣
∃𝑡 ∈ ℕ
∃𝑛 ∈
(bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚})) → 𝑘 ∈ ((◡(𝐺‘𝐴) “ ℕ) ∖ {𝑚 ∈ ℕ ∣
∃𝑡 ∈ ℕ
∃𝑛 ∈
(bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚})) |
102 | 101 | eldifbd 3957 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑘 ∈ ((◡(𝐺‘𝐴) “ ℕ) ∖ {𝑚 ∈ ℕ ∣
∃𝑡 ∈ ℕ
∃𝑛 ∈
(bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚})) → ¬ 𝑘 ∈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚}) |
103 | 22 | ssdifssd 4139 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → ((◡(𝐺‘𝐴) “ ℕ) ∖ {𝑚 ∈ ℕ ∣
∃𝑡 ∈ ℕ
∃𝑛 ∈
(bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚}) ⊆ ℕ) |
104 | 103 | sselda 3976 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑘 ∈ ((◡(𝐺‘𝐴) “ ℕ) ∖ {𝑚 ∈ ℕ ∣
∃𝑡 ∈ ℕ
∃𝑛 ∈
(bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚})) → 𝑘 ∈ ℕ) |
105 | 30 | notbii 319 |
. . . . . . . . . . 11
⊢ (¬
𝑘 ∈ {𝑚 ∈ ℕ ∣
∃𝑡 ∈ ℕ
∃𝑛 ∈
(bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚} ↔ ¬ (𝑘 ∈ ℕ ∧ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑘)) |
106 | | imnan 398 |
. . . . . . . . . . 11
⊢ ((𝑘 ∈ ℕ → ¬
∃𝑡 ∈ ℕ
∃𝑛 ∈
(bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑘) ↔ ¬ (𝑘 ∈ ℕ ∧ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑘)) |
107 | 105, 106 | sylbb2 237 |
. . . . . . . . . 10
⊢ (¬
𝑘 ∈ {𝑚 ∈ ℕ ∣
∃𝑡 ∈ ℕ
∃𝑛 ∈
(bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚} → (𝑘 ∈ ℕ → ¬ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑘)) |
108 | 102, 104,
107 | sylc 65 |
. . . . . . . . 9
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑘 ∈ ((◡(𝐺‘𝐴) “ ℕ) ∖ {𝑚 ∈ ℕ ∣
∃𝑡 ∈ ℕ
∃𝑛 ∈
(bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚})) → ¬ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑘) |
109 | 108 | iffalsed 4541 |
. . . . . . . 8
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑘 ∈ ((◡(𝐺‘𝐴) “ ℕ) ∖ {𝑚 ∈ ℕ ∣
∃𝑡 ∈ ℕ
∃𝑛 ∈
(bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚})) → if(∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑘, 1, 0) = 0) |
110 | 109 | oveq1d 7434 |
. . . . . . 7
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑘 ∈ ((◡(𝐺‘𝐴) “ ℕ) ∖ {𝑚 ∈ ℕ ∣
∃𝑡 ∈ ℕ
∃𝑛 ∈
(bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚})) → (if(∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑘, 1, 0) · 𝑘) = (0 · 𝑘)) |
111 | | nnsscn 12255 |
. . . . . . . . . 10
⊢ ℕ
⊆ ℂ |
112 | 103, 111 | sstrdi 3989 |
. . . . . . . . 9
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → ((◡(𝐺‘𝐴) “ ℕ) ∖ {𝑚 ∈ ℕ ∣
∃𝑡 ∈ ℕ
∃𝑛 ∈
(bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚}) ⊆ ℂ) |
113 | 112 | sselda 3976 |
. . . . . . . 8
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑘 ∈ ((◡(𝐺‘𝐴) “ ℕ) ∖ {𝑚 ∈ ℕ ∣
∃𝑡 ∈ ℕ
∃𝑛 ∈
(bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚})) → 𝑘 ∈ ℂ) |
114 | 113 | mul02d 11449 |
. . . . . . 7
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑘 ∈ ((◡(𝐺‘𝐴) “ ℕ) ∖ {𝑚 ∈ ℕ ∣
∃𝑡 ∈ ℕ
∃𝑛 ∈
(bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚})) → (0 · 𝑘) = 0) |
115 | 110, 114 | eqtrd 2765 |
. . . . . 6
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑘 ∈ ((◡(𝐺‘𝐴) “ ℕ) ∖ {𝑚 ∈ ℕ ∣
∃𝑡 ∈ ℕ
∃𝑛 ∈
(bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚})) → (if(∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑘, 1, 0) · 𝑘) = 0) |
116 | 54, 100, 115, 40 | fsumss 15712 |
. . . . 5
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → Σ𝑘 ∈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚} (if(∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑘, 1, 0) · 𝑘) = Σ𝑘 ∈ (◡(𝐺‘𝐴) “ ℕ)(if(∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑘, 1, 0) · 𝑘)) |
117 | 91, 116 | eqtr3d 2767 |
. . . 4
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → Σ𝑤 ∈ ∪
𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡)))((2↑(2nd ‘𝑤)) · (1st
‘𝑤)) = Σ𝑘 ∈ (◡(𝐺‘𝐴) “ ℕ)(if(∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑘, 1, 0) · 𝑘)) |
118 | 2, 3, 4, 5, 6, 7, 8, 9, 10 | eulerpartlemt0 34122 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) ↔ (𝐴 ∈ (ℕ0
↑m ℕ) ∧ (◡𝐴 “ ℕ) ∈ Fin ∧ (◡𝐴 “ ℕ) ⊆ 𝐽)) |
119 | 118 | simp1bi 1142 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → 𝐴 ∈ (ℕ0
↑m ℕ)) |
120 | | elmapi 8868 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ (ℕ0
↑m ℕ) → 𝐴:ℕ⟶ℕ0) |
121 | 119, 120 | syl 17 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → 𝐴:ℕ⟶ℕ0) |
122 | 121 | adantr 479 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)) → 𝐴:ℕ⟶ℕ0) |
123 | | cnvimass 6086 |
. . . . . . . . . . . . 13
⊢ (◡𝐴 “ ℕ) ⊆ dom 𝐴 |
124 | 123, 121 | fssdm 6742 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → (◡𝐴 “ ℕ) ⊆
ℕ) |
125 | 124 | adantr 479 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)) → (◡𝐴 “ ℕ) ⊆
ℕ) |
126 | | inss1 4227 |
. . . . . . . . . . . 12
⊢ ((◡𝐴 “ ℕ) ∩ 𝐽) ⊆ (◡𝐴 “ ℕ) |
127 | 126, 76 | sselid 3974 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)) → 𝑡 ∈ (◡𝐴 “ ℕ)) |
128 | 125, 127 | sseldd 3977 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)) → 𝑡 ∈ ℕ) |
129 | 122, 128 | ffvelcdmd 7094 |
. . . . . . . . 9
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)) → (𝐴‘𝑡) ∈
ℕ0) |
130 | | bitsfi 16420 |
. . . . . . . . 9
⊢ ((𝐴‘𝑡) ∈ ℕ0 →
(bits‘(𝐴‘𝑡)) ∈ Fin) |
131 | 129, 130 | syl 17 |
. . . . . . . 8
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)) → (bits‘(𝐴‘𝑡)) ∈ Fin) |
132 | 128 | nncnd 12266 |
. . . . . . . 8
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)) → 𝑡 ∈ ℂ) |
133 | | 2cnd 12328 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ (𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽) ∧ 𝑛 ∈ (bits‘(𝐴‘𝑡)))) → 2 ∈
ℂ) |
134 | | simprr 771 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ (𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽) ∧ 𝑛 ∈ (bits‘(𝐴‘𝑡)))) → 𝑛 ∈ (bits‘(𝐴‘𝑡))) |
135 | 79, 134 | sselid 3974 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ (𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽) ∧ 𝑛 ∈ (bits‘(𝐴‘𝑡)))) → 𝑛 ∈ ℕ0) |
136 | 133, 135 | expcld 14151 |
. . . . . . . . 9
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ (𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽) ∧ 𝑛 ∈ (bits‘(𝐴‘𝑡)))) → (2↑𝑛) ∈ ℂ) |
137 | 136 | anassrs 466 |
. . . . . . . 8
⊢ (((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)) ∧ 𝑛 ∈ (bits‘(𝐴‘𝑡))) → (2↑𝑛) ∈ ℂ) |
138 | 131, 132,
137 | fsummulc1 15772 |
. . . . . . 7
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)) → (Σ𝑛 ∈ (bits‘(𝐴‘𝑡))(2↑𝑛) · 𝑡) = Σ𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡)) |
139 | 138 | sumeq2dv 15690 |
. . . . . 6
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → Σ𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)(Σ𝑛 ∈ (bits‘(𝐴‘𝑡))(2↑𝑛) · 𝑡) = Σ𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)Σ𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡)) |
140 | | bitsinv1 16425 |
. . . . . . . . 9
⊢ ((𝐴‘𝑡) ∈ ℕ0 →
Σ𝑛 ∈
(bits‘(𝐴‘𝑡))(2↑𝑛) = (𝐴‘𝑡)) |
141 | 140 | oveq1d 7434 |
. . . . . . . 8
⊢ ((𝐴‘𝑡) ∈ ℕ0 →
(Σ𝑛 ∈
(bits‘(𝐴‘𝑡))(2↑𝑛) · 𝑡) = ((𝐴‘𝑡) · 𝑡)) |
142 | 129, 141 | syl 17 |
. . . . . . 7
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)) → (Σ𝑛 ∈ (bits‘(𝐴‘𝑡))(2↑𝑛) · 𝑡) = ((𝐴‘𝑡) · 𝑡)) |
143 | 142 | sumeq2dv 15690 |
. . . . . 6
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → Σ𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)(Σ𝑛 ∈ (bits‘(𝐴‘𝑡))(2↑𝑛) · 𝑡) = Σ𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)((𝐴‘𝑡) · 𝑡)) |
144 | | vex 3465 |
. . . . . . . . . 10
⊢ 𝑡 ∈ V |
145 | | vex 3465 |
. . . . . . . . . 10
⊢ 𝑛 ∈ V |
146 | 144, 145 | op2ndd 8005 |
. . . . . . . . 9
⊢ (𝑤 = 〈𝑡, 𝑛〉 → (2nd ‘𝑤) = 𝑛) |
147 | 146 | oveq2d 7435 |
. . . . . . . 8
⊢ (𝑤 = 〈𝑡, 𝑛〉 → (2↑(2nd
‘𝑤)) = (2↑𝑛)) |
148 | 144, 145 | op1std 8004 |
. . . . . . . 8
⊢ (𝑤 = 〈𝑡, 𝑛〉 → (1st ‘𝑤) = 𝑡) |
149 | 147, 148 | oveq12d 7437 |
. . . . . . 7
⊢ (𝑤 = 〈𝑡, 𝑛〉 → ((2↑(2nd
‘𝑤)) ·
(1st ‘𝑤))
= ((2↑𝑛) ·
𝑡)) |
150 | | inss2 4228 |
. . . . . . . . . 10
⊢ (𝑇 ∩ 𝑅) ⊆ 𝑅 |
151 | 150 | sseli 3972 |
. . . . . . . . 9
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → 𝐴 ∈ 𝑅) |
152 | | cnveq 5876 |
. . . . . . . . . . . 12
⊢ (𝑓 = 𝐴 → ◡𝑓 = ◡𝐴) |
153 | 152 | imaeq1d 6063 |
. . . . . . . . . . 11
⊢ (𝑓 = 𝐴 → (◡𝑓 “ ℕ) = (◡𝐴 “ ℕ)) |
154 | 153 | eleq1d 2810 |
. . . . . . . . . 10
⊢ (𝑓 = 𝐴 → ((◡𝑓 “ ℕ) ∈ Fin ↔ (◡𝐴 “ ℕ) ∈
Fin)) |
155 | 154, 9 | elab2g 3666 |
. . . . . . . . 9
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → (𝐴 ∈ 𝑅 ↔ (◡𝐴 “ ℕ) ∈
Fin)) |
156 | 151, 155 | mpbid 231 |
. . . . . . . 8
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → (◡𝐴 “ ℕ) ∈
Fin) |
157 | | ssfi 9201 |
. . . . . . . 8
⊢ (((◡𝐴 “ ℕ) ∈ Fin ∧ ((◡𝐴 “ ℕ) ∩ 𝐽) ⊆ (◡𝐴 “ ℕ)) → ((◡𝐴 “ ℕ) ∩ 𝐽) ∈ Fin) |
158 | 156, 126,
157 | sylancl 584 |
. . . . . . 7
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → ((◡𝐴 “ ℕ) ∩ 𝐽) ∈ Fin) |
159 | 132 | adantrr 715 |
. . . . . . . 8
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ (𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽) ∧ 𝑛 ∈ (bits‘(𝐴‘𝑡)))) → 𝑡 ∈ ℂ) |
160 | 136, 159 | mulcld 11271 |
. . . . . . 7
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ (𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽) ∧ 𝑛 ∈ (bits‘(𝐴‘𝑡)))) → ((2↑𝑛) · 𝑡) ∈ ℂ) |
161 | 149, 158,
131, 160 | fsum2d 15758 |
. . . . . 6
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → Σ𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)Σ𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = Σ𝑤 ∈ ∪
𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡)))((2↑(2nd ‘𝑤)) · (1st
‘𝑤))) |
162 | 139, 143,
161 | 3eqtr3d 2773 |
. . . . 5
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → Σ𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)((𝐴‘𝑡) · 𝑡) = Σ𝑤 ∈ ∪
𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡)))((2↑(2nd ‘𝑤)) · (1st
‘𝑤))) |
163 | | inss1 4227 |
. . . . . . . . 9
⊢ (𝑇 ∩ 𝑅) ⊆ 𝑇 |
164 | 163 | sseli 3972 |
. . . . . . . 8
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → 𝐴 ∈ 𝑇) |
165 | 153 | sseq1d 4008 |
. . . . . . . . . 10
⊢ (𝑓 = 𝐴 → ((◡𝑓 “ ℕ) ⊆ 𝐽 ↔ (◡𝐴 “ ℕ) ⊆ 𝐽)) |
166 | 165, 10 | elrab2 3682 |
. . . . . . . . 9
⊢ (𝐴 ∈ 𝑇 ↔ (𝐴 ∈ (ℕ0
↑m ℕ) ∧ (◡𝐴 “ ℕ) ⊆ 𝐽)) |
167 | 166 | simprbi 495 |
. . . . . . . 8
⊢ (𝐴 ∈ 𝑇 → (◡𝐴 “ ℕ) ⊆ 𝐽) |
168 | 164, 167 | syl 17 |
. . . . . . 7
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → (◡𝐴 “ ℕ) ⊆ 𝐽) |
169 | | dfss2 3962 |
. . . . . . 7
⊢ ((◡𝐴 “ ℕ) ⊆ 𝐽 ↔ ((◡𝐴 “ ℕ) ∩ 𝐽) = (◡𝐴 “ ℕ)) |
170 | 168, 169 | sylib 217 |
. . . . . 6
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → ((◡𝐴 “ ℕ) ∩ 𝐽) = (◡𝐴 “ ℕ)) |
171 | 170 | sumeq1d 15688 |
. . . . 5
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → Σ𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)((𝐴‘𝑡) · 𝑡) = Σ𝑡 ∈ (◡𝐴 “ ℕ)((𝐴‘𝑡) · 𝑡)) |
172 | 162, 171 | eqtr3d 2767 |
. . . 4
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → Σ𝑤 ∈ ∪
𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡)))((2↑(2nd ‘𝑤)) · (1st
‘𝑤)) = Σ𝑡 ∈ (◡𝐴 “ ℕ)((𝐴‘𝑡) · 𝑡)) |
173 | 27, 117, 172 | 3eqtr2d 2771 |
. . 3
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → Σ𝑘 ∈ (◡(𝐺‘𝐴) “ ℕ)(((𝐺‘𝐴)‘𝑘) · 𝑘) = Σ𝑡 ∈ (◡𝐴 “ ℕ)((𝐴‘𝑡) · 𝑡)) |
174 | | fveq2 6896 |
. . . . 5
⊢ (𝑘 = 𝑡 → (𝐴‘𝑘) = (𝐴‘𝑡)) |
175 | | id 22 |
. . . . 5
⊢ (𝑘 = 𝑡 → 𝑘 = 𝑡) |
176 | 174, 175 | oveq12d 7437 |
. . . 4
⊢ (𝑘 = 𝑡 → ((𝐴‘𝑘) · 𝑘) = ((𝐴‘𝑡) · 𝑡)) |
177 | 176 | cbvsumv 15683 |
. . 3
⊢
Σ𝑘 ∈
(◡𝐴 “ ℕ)((𝐴‘𝑘) · 𝑘) = Σ𝑡 ∈ (◡𝐴 “ ℕ)((𝐴‘𝑡) · 𝑡) |
178 | 173, 177 | eqtr4di 2783 |
. 2
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → Σ𝑘 ∈ (◡(𝐺‘𝐴) “ ℕ)(((𝐺‘𝐴)‘𝑘) · 𝑘) = Σ𝑘 ∈ (◡𝐴 “ ℕ)((𝐴‘𝑘) · 𝑘)) |
179 | | 0nn0 12525 |
. . . . . . . 8
⊢ 0 ∈
ℕ0 |
180 | | 1nn0 12526 |
. . . . . . . 8
⊢ 1 ∈
ℕ0 |
181 | | prssi 4826 |
. . . . . . . 8
⊢ ((0
∈ ℕ0 ∧ 1 ∈ ℕ0) → {0, 1}
⊆ ℕ0) |
182 | 179, 180,
181 | mp2an 690 |
. . . . . . 7
⊢ {0, 1}
⊆ ℕ0 |
183 | | fss 6739 |
. . . . . . 7
⊢ (((𝐺‘𝐴):ℕ⟶{0, 1} ∧ {0, 1} ⊆
ℕ0) → (𝐺‘𝐴):ℕ⟶ℕ0) |
184 | 182, 183 | mpan2 689 |
. . . . . 6
⊢ ((𝐺‘𝐴):ℕ⟶{0, 1} → (𝐺‘𝐴):ℕ⟶ℕ0) |
185 | | nn0ex 12516 |
. . . . . . . 8
⊢
ℕ0 ∈ V |
186 | | nnex 12256 |
. . . . . . . 8
⊢ ℕ
∈ V |
187 | 185, 186 | elmap 8890 |
. . . . . . 7
⊢ ((𝐺‘𝐴) ∈ (ℕ0
↑m ℕ) ↔ (𝐺‘𝐴):ℕ⟶ℕ0) |
188 | 187 | biimpri 227 |
. . . . . 6
⊢ ((𝐺‘𝐴):ℕ⟶ℕ0 →
(𝐺‘𝐴) ∈ (ℕ0
↑m ℕ)) |
189 | 19, 184, 188 | 3syl 18 |
. . . . 5
⊢ ((𝐺‘𝐴) ∈ ({0, 1} ↑m ℕ)
→ (𝐺‘𝐴) ∈ (ℕ0
↑m ℕ)) |
190 | 189 | anim1i 613 |
. . . 4
⊢ (((𝐺‘𝐴) ∈ ({0, 1} ↑m ℕ)
∧ (𝐺‘𝐴) ∈ 𝑅) → ((𝐺‘𝐴) ∈ (ℕ0
↑m ℕ) ∧ (𝐺‘𝐴) ∈ 𝑅)) |
191 | | elin 3960 |
. . . 4
⊢ ((𝐺‘𝐴) ∈ ((ℕ0
↑m ℕ) ∩ 𝑅) ↔ ((𝐺‘𝐴) ∈ (ℕ0
↑m ℕ) ∧ (𝐺‘𝐴) ∈ 𝑅)) |
192 | 190, 16, 191 | 3imtr4i 291 |
. . 3
⊢ ((𝐺‘𝐴) ∈ (({0, 1} ↑m
ℕ) ∩ 𝑅) →
(𝐺‘𝐴) ∈ ((ℕ0
↑m ℕ) ∩ 𝑅)) |
193 | | eulerpart.s |
. . . 4
⊢ 𝑆 = (𝑓 ∈ ((ℕ0
↑m ℕ) ∩ 𝑅) ↦ Σ𝑘 ∈ ℕ ((𝑓‘𝑘) · 𝑘)) |
194 | 9, 193 | eulerpartlemsv2 34111 |
. . 3
⊢ ((𝐺‘𝐴) ∈ ((ℕ0
↑m ℕ) ∩ 𝑅) → (𝑆‘(𝐺‘𝐴)) = Σ𝑘 ∈ (◡(𝐺‘𝐴) “ ℕ)(((𝐺‘𝐴)‘𝑘) · 𝑘)) |
195 | 15, 192, 194 | 3syl 18 |
. 2
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → (𝑆‘(𝐺‘𝐴)) = Σ𝑘 ∈ (◡(𝐺‘𝐴) “ ℕ)(((𝐺‘𝐴)‘𝑘) · 𝑘)) |
196 | 119, 151 | elind 4192 |
. . 3
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → 𝐴 ∈ ((ℕ0
↑m ℕ) ∩ 𝑅)) |
197 | 9, 193 | eulerpartlemsv2 34111 |
. . 3
⊢ (𝐴 ∈ ((ℕ0
↑m ℕ) ∩ 𝑅) → (𝑆‘𝐴) = Σ𝑘 ∈ (◡𝐴 “ ℕ)((𝐴‘𝑘) · 𝑘)) |
198 | 196, 197 | syl 17 |
. 2
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → (𝑆‘𝐴) = Σ𝑘 ∈ (◡𝐴 “ ℕ)((𝐴‘𝑘) · 𝑘)) |
199 | 178, 195,
198 | 3eqtr4d 2775 |
1
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → (𝑆‘(𝐺‘𝐴)) = (𝑆‘𝐴)) |