Step | Hyp | Ref
| Expression |
1 | | cnvimass 5988 |
. . . . . . . 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 32335 |
. . . . . . . . . . . . 13
⊢ 𝐺:(𝑇 ∩ 𝑅)–1-1-onto→(({0,
1} ↑m ℕ) ∩ 𝑅) |
13 | | f1of 6714 |
. . . . . . . . . . . . 13
⊢ (𝐺:(𝑇 ∩ 𝑅)–1-1-onto→(({0,
1} ↑m ℕ) ∩ 𝑅) → 𝐺:(𝑇 ∩ 𝑅)⟶(({0, 1} ↑m
ℕ) ∩ 𝑅)) |
14 | 12, 13 | ax-mp 5 |
. . . . . . . . . . . 12
⊢ 𝐺:(𝑇 ∩ 𝑅)⟶(({0, 1} ↑m
ℕ) ∩ 𝑅) |
15 | 14 | ffvelrni 6957 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → (𝐺‘𝐴) ∈ (({0, 1} ↑m
ℕ) ∩ 𝑅)) |
16 | | elin 3908 |
. . . . . . . . . . 11
⊢ ((𝐺‘𝐴) ∈ (({0, 1} ↑m
ℕ) ∩ 𝑅) ↔
((𝐺‘𝐴) ∈ ({0, 1} ↑m ℕ)
∧ (𝐺‘𝐴) ∈ 𝑅)) |
17 | 15, 16 | sylib 217 |
. . . . . . . . . 10
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → ((𝐺‘𝐴) ∈ ({0, 1} ↑m ℕ)
∧ (𝐺‘𝐴) ∈ 𝑅)) |
18 | 17 | simpld 495 |
. . . . . . . . 9
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → (𝐺‘𝐴) ∈ ({0, 1} ↑m
ℕ)) |
19 | | elmapi 8620 |
. . . . . . . . 9
⊢ ((𝐺‘𝐴) ∈ ({0, 1} ↑m ℕ)
→ (𝐺‘𝐴):ℕ⟶{0,
1}) |
20 | | fdm 6607 |
. . . . . . . . 9
⊢ ((𝐺‘𝐴):ℕ⟶{0, 1} → dom (𝐺‘𝐴) = ℕ) |
21 | 18, 19, 20 | 3syl 18 |
. . . . . . . 8
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → dom (𝐺‘𝐴) = ℕ) |
22 | 1, 21 | sseqtrid 3978 |
. . . . . . 7
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → (◡(𝐺‘𝐴) “ ℕ) ⊆
ℕ) |
23 | 22 | sselda 3926 |
. . . . . 6
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑘 ∈ (◡(𝐺‘𝐴) “ ℕ)) → 𝑘 ∈
ℕ) |
24 | 2, 3, 4, 5, 6, 7, 8, 9, 10, 11 | eulerpartlemgvv 32339 |
. . . . . . 7
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑘 ∈ ℕ) → ((𝐺‘𝐴)‘𝑘) = if(∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑘, 1, 0)) |
25 | 24 | oveq1d 7286 |
. . . . . 6
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑘 ∈ ℕ) → (((𝐺‘𝐴)‘𝑘) · 𝑘) = (if(∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑘, 1, 0) · 𝑘)) |
26 | 23, 25 | syldan 591 |
. . . . 5
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑘 ∈ (◡(𝐺‘𝐴) “ ℕ)) → (((𝐺‘𝐴)‘𝑘) · 𝑘) = (if(∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑘, 1, 0) · 𝑘)) |
27 | 26 | sumeq2dv 15413 |
. . . 4
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → Σ𝑘 ∈ (◡(𝐺‘𝐴) “ ℕ)(((𝐺‘𝐴)‘𝑘) · 𝑘) = Σ𝑘 ∈ (◡(𝐺‘𝐴) “ ℕ)(if(∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑘, 1, 0) · 𝑘)) |
28 | | eqeq2 2752 |
. . . . . . . . . . . . 13
⊢ (𝑚 = 𝑘 → (((2↑𝑛) · 𝑡) = 𝑚 ↔ ((2↑𝑛) · 𝑡) = 𝑘)) |
29 | 28 | 2rexbidv 3231 |
. . . . . . . . . . . 12
⊢ (𝑚 = 𝑘 → (∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚 ↔ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑘)) |
30 | 29 | elrab 3626 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚} ↔ (𝑘 ∈ ℕ ∧ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑘)) |
31 | 30 | simprbi 497 |
. . . . . . . . . 10
⊢ (𝑘 ∈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚} → ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑘) |
32 | 31 | iftrued 4473 |
. . . . . . . . 9
⊢ (𝑘 ∈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚} → if(∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑘, 1, 0) = 1) |
33 | 32 | oveq1d 7286 |
. . . . . . . 8
⊢ (𝑘 ∈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚} → (if(∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑘, 1, 0) · 𝑘) = (1 · 𝑘)) |
34 | | elrabi 3620 |
. . . . . . . . . 10
⊢ (𝑘 ∈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚} → 𝑘 ∈ ℕ) |
35 | 34 | nncnd 11989 |
. . . . . . . . 9
⊢ (𝑘 ∈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚} → 𝑘 ∈ ℂ) |
36 | 35 | mulid2d 10994 |
. . . . . . . 8
⊢ (𝑘 ∈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚} → (1 · 𝑘) = 𝑘) |
37 | 33, 36 | eqtrd 2780 |
. . . . . . 7
⊢ (𝑘 ∈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚} → (if(∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑘, 1, 0) · 𝑘) = 𝑘) |
38 | 37 | sumeq2i 15409 |
. . . . . 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 32342 |
. . . . . . . . 9
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → (◡(𝐺‘𝐴) “ ℕ) ∈
Fin) |
41 | 34 | adantl 482 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑘 ∈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚}) → 𝑘 ∈ ℕ) |
42 | 41, 24 | syldan 591 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑘 ∈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚}) → ((𝐺‘𝐴)‘𝑘) = if(∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑘, 1, 0)) |
43 | 31 | adantl 482 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑘 ∈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚}) → ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑘) |
44 | 43 | iftrued 4473 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑘 ∈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚}) → if(∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑘, 1, 0) = 1) |
45 | 42, 44 | eqtrd 2780 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑘 ∈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚}) → ((𝐺‘𝐴)‘𝑘) = 1) |
46 | | 1nn 11984 |
. . . . . . . . . . . . 13
⊢ 1 ∈
ℕ |
47 | 45, 46 | eqeltrdi 2849 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑘 ∈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚}) → ((𝐺‘𝐴)‘𝑘) ∈ ℕ) |
48 | 18, 19 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → (𝐺‘𝐴):ℕ⟶{0, 1}) |
49 | | ffn 6598 |
. . . . . . . . . . . . . 14
⊢ ((𝐺‘𝐴):ℕ⟶{0, 1} → (𝐺‘𝐴) Fn ℕ) |
50 | | elpreima 6932 |
. . . . . . . . . . . . . 14
⊢ ((𝐺‘𝐴) Fn ℕ → (𝑘 ∈ (◡(𝐺‘𝐴) “ ℕ) ↔ (𝑘 ∈ ℕ ∧ ((𝐺‘𝐴)‘𝑘) ∈ ℕ))) |
51 | 48, 49, 50 | 3syl 18 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → (𝑘 ∈ (◡(𝐺‘𝐴) “ ℕ) ↔ (𝑘 ∈ ℕ ∧ ((𝐺‘𝐴)‘𝑘) ∈ ℕ))) |
52 | 51 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑘 ∈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚}) → (𝑘 ∈ (◡(𝐺‘𝐴) “ ℕ) ↔ (𝑘 ∈ ℕ ∧ ((𝐺‘𝐴)‘𝑘) ∈ ℕ))) |
53 | 41, 47, 52 | mpbir2and 710 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑘 ∈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚}) → 𝑘 ∈ (◡(𝐺‘𝐴) “ ℕ)) |
54 | 53 | ex 413 |
. . . . . . . . . 10
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → (𝑘 ∈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚} → 𝑘 ∈ (◡(𝐺‘𝐴) “ ℕ))) |
55 | 54 | ssrdv 3932 |
. . . . . . . . 9
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚} ⊆ (◡(𝐺‘𝐴) “ ℕ)) |
56 | | ssfi 8938 |
. . . . . . . . 9
⊢ (((◡(𝐺‘𝐴) “ ℕ) ∈ Fin ∧ {𝑚 ∈ ℕ ∣
∃𝑡 ∈ ℕ
∃𝑛 ∈
(bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚} ⊆ (◡(𝐺‘𝐴) “ ℕ)) → {𝑚 ∈ ℕ ∣
∃𝑡 ∈ ℕ
∃𝑛 ∈
(bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚} ∈ Fin) |
57 | 40, 55, 56 | syl2anc 584 |
. . . . . . . 8
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚} ∈ Fin) |
58 | | cnvexg 7765 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → ◡𝐴 ∈ V) |
59 | | imaexg 7756 |
. . . . . . . . . . 11
⊢ (◡𝐴 ∈ V → (◡𝐴 “ ℕ) ∈ V) |
60 | | inex1g 5247 |
. . . . . . . . . . 11
⊢ ((◡𝐴 “ ℕ) ∈ V → ((◡𝐴 “ ℕ) ∩ 𝐽) ∈ V) |
61 | 58, 59, 60 | 3syl 18 |
. . . . . . . . . 10
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → ((◡𝐴 “ ℕ) ∩ 𝐽) ∈ V) |
62 | | snex 5358 |
. . . . . . . . . . . 12
⊢ {𝑡} ∈ V |
63 | | fvex 6784 |
. . . . . . . . . . . 12
⊢
(bits‘(𝐴‘𝑡)) ∈ V |
64 | 62, 63 | xpex 7597 |
. . . . . . . . . . 11
⊢ ({𝑡} × (bits‘(𝐴‘𝑡))) ∈ V |
65 | 64 | rgenw 3078 |
. . . . . . . . . 10
⊢
∀𝑡 ∈
((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡))) ∈ V |
66 | | iunexg 7799 |
. . . . . . . . . 10
⊢ ((((◡𝐴 “ ℕ) ∩ 𝐽) ∈ V ∧ ∀𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡))) ∈ V) → ∪ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡))) ∈ V) |
67 | 61, 65, 66 | sylancl 586 |
. . . . . . . . 9
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → ∪
𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡))) ∈ V) |
68 | | eqid 2740 |
. . . . . . . . . 10
⊢ ∪ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡))) = ∪
𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡))) |
69 | 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 68 | eulerpartlemgh 32341 |
. . . . . . . . 9
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → (𝐹 ↾ ∪
𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡)))):∪
𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡)))–1-1-onto→{𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚}) |
70 | | f1oeng 8742 |
. . . . . . . . 9
⊢
((∪ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡))) ∈ V ∧ (𝐹 ↾ ∪
𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡)))):∪
𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡)))–1-1-onto→{𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚}) → ∪
𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡))) ≈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚}) |
71 | 67, 69, 70 | syl2anc 584 |
. . . . . . . 8
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → ∪
𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡))) ≈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚}) |
72 | | enfii 8954 |
. . . . . . . 8
⊢ (({𝑚 ∈ ℕ ∣
∃𝑡 ∈ ℕ
∃𝑛 ∈
(bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚} ∈ Fin ∧ ∪ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡))) ≈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚}) → ∪
𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡))) ∈ Fin) |
73 | 57, 71, 72 | syl2anc 584 |
. . . . . . 7
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → ∪
𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡))) ∈ Fin) |
74 | | fvres 6790 |
. . . . . . . . 9
⊢ (𝑤 ∈ ∪ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡))) → ((𝐹 ↾ ∪
𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡))))‘𝑤) = (𝐹‘𝑤)) |
75 | 74 | adantl 482 |
. . . . . . . 8
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑤 ∈ ∪
𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡)))) → ((𝐹 ↾ ∪
𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡))))‘𝑤) = (𝐹‘𝑤)) |
76 | | inss2 4169 |
. . . . . . . . . . . . . . 15
⊢ ((◡𝐴 “ ℕ) ∩ 𝐽) ⊆ 𝐽 |
77 | | simpr 485 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)) → 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)) |
78 | 76, 77 | sselid 3924 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)) → 𝑡 ∈ 𝐽) |
79 | 78 | snssd 4748 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)) → {𝑡} ⊆ 𝐽) |
80 | | bitsss 16131 |
. . . . . . . . . . . . 13
⊢
(bits‘(𝐴‘𝑡)) ⊆
ℕ0 |
81 | | xpss12 5605 |
. . . . . . . . . . . . 13
⊢ (({𝑡} ⊆ 𝐽 ∧ (bits‘(𝐴‘𝑡)) ⊆ ℕ0) →
({𝑡} ×
(bits‘(𝐴‘𝑡))) ⊆ (𝐽 ×
ℕ0)) |
82 | 79, 80, 81 | sylancl 586 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)) → ({𝑡} × (bits‘(𝐴‘𝑡))) ⊆ (𝐽 ×
ℕ0)) |
83 | 82 | ralrimiva 3110 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → ∀𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡))) ⊆ (𝐽 ×
ℕ0)) |
84 | | iunss 4980 |
. . . . . . . . . . 11
⊢ (∪ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡))) ⊆ (𝐽 × ℕ0) ↔
∀𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡))) ⊆ (𝐽 ×
ℕ0)) |
85 | 83, 84 | sylibr 233 |
. . . . . . . . . 10
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → ∪
𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡))) ⊆ (𝐽 ×
ℕ0)) |
86 | 85 | sselda 3926 |
. . . . . . . . 9
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑤 ∈ ∪
𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡)))) → 𝑤 ∈ (𝐽 ×
ℕ0)) |
87 | 5, 6 | oddpwdcv 32318 |
. . . . . . . . 9
⊢ (𝑤 ∈ (𝐽 × ℕ0) → (𝐹‘𝑤) = ((2↑(2nd ‘𝑤)) · (1st
‘𝑤))) |
88 | 86, 87 | syl 17 |
. . . . . . . 8
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑤 ∈ ∪
𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡)))) → (𝐹‘𝑤) = ((2↑(2nd ‘𝑤)) · (1st
‘𝑤))) |
89 | 75, 88 | eqtrd 2780 |
. . . . . . 7
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑤 ∈ ∪
𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡)))) → ((𝐹 ↾ ∪
𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡))))‘𝑤) = ((2↑(2nd ‘𝑤)) · (1st
‘𝑤))) |
90 | 41 | nncnd 11989 |
. . . . . . 7
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑘 ∈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚}) → 𝑘 ∈ ℂ) |
91 | 39, 73, 69, 89, 90 | fsumf1o 15433 |
. . . . . 6
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → Σ𝑘 ∈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚}𝑘 = Σ𝑤 ∈ ∪
𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡)))((2↑(2nd ‘𝑤)) · (1st
‘𝑤))) |
92 | 38, 91 | eqtrid 2792 |
. . . . 5
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → Σ𝑘 ∈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚} (if(∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑘, 1, 0) · 𝑘) = Σ𝑤 ∈ ∪
𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡)))((2↑(2nd ‘𝑤)) · (1st
‘𝑤))) |
93 | | ax-1cn 10930 |
. . . . . . . . 9
⊢ 1 ∈
ℂ |
94 | | 0cn 10968 |
. . . . . . . . 9
⊢ 0 ∈
ℂ |
95 | 93, 94 | ifcli 4512 |
. . . . . . . 8
⊢
if(∃𝑡 ∈
ℕ ∃𝑛 ∈
(bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑘, 1, 0) ∈ ℂ |
96 | 95 | a1i 11 |
. . . . . . 7
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑘 ∈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚}) → if(∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑘, 1, 0) ∈ ℂ) |
97 | | ssrab2 4018 |
. . . . . . . . 9
⊢ {𝑚 ∈ ℕ ∣
∃𝑡 ∈ ℕ
∃𝑛 ∈
(bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚} ⊆ ℕ |
98 | | simpr 485 |
. . . . . . . . 9
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑘 ∈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚}) → 𝑘 ∈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚}) |
99 | 97, 98 | sselid 3924 |
. . . . . . . 8
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑘 ∈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚}) → 𝑘 ∈ ℕ) |
100 | 99 | nncnd 11989 |
. . . . . . 7
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑘 ∈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚}) → 𝑘 ∈ ℂ) |
101 | 96, 100 | mulcld 10996 |
. . . . . 6
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑘 ∈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚}) → (if(∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑘, 1, 0) · 𝑘) ∈ ℂ) |
102 | | simpr 485 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑘 ∈ ((◡(𝐺‘𝐴) “ ℕ) ∖ {𝑚 ∈ ℕ ∣
∃𝑡 ∈ ℕ
∃𝑛 ∈
(bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚})) → 𝑘 ∈ ((◡(𝐺‘𝐴) “ ℕ) ∖ {𝑚 ∈ ℕ ∣
∃𝑡 ∈ ℕ
∃𝑛 ∈
(bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚})) |
103 | 102 | eldifbd 3905 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑘 ∈ ((◡(𝐺‘𝐴) “ ℕ) ∖ {𝑚 ∈ ℕ ∣
∃𝑡 ∈ ℕ
∃𝑛 ∈
(bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚})) → ¬ 𝑘 ∈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚}) |
104 | 22 | ssdifssd 4082 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → ((◡(𝐺‘𝐴) “ ℕ) ∖ {𝑚 ∈ ℕ ∣
∃𝑡 ∈ ℕ
∃𝑛 ∈
(bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚}) ⊆ ℕ) |
105 | 104 | sselda 3926 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑘 ∈ ((◡(𝐺‘𝐴) “ ℕ) ∖ {𝑚 ∈ ℕ ∣
∃𝑡 ∈ ℕ
∃𝑛 ∈
(bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚})) → 𝑘 ∈ ℕ) |
106 | 30 | notbii 320 |
. . . . . . . . . . 11
⊢ (¬
𝑘 ∈ {𝑚 ∈ ℕ ∣
∃𝑡 ∈ ℕ
∃𝑛 ∈
(bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚} ↔ ¬ (𝑘 ∈ ℕ ∧ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑘)) |
107 | | imnan 400 |
. . . . . . . . . . 11
⊢ ((𝑘 ∈ ℕ → ¬
∃𝑡 ∈ ℕ
∃𝑛 ∈
(bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑘) ↔ ¬ (𝑘 ∈ ℕ ∧ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑘)) |
108 | 106, 107 | sylbb2 237 |
. . . . . . . . . 10
⊢ (¬
𝑘 ∈ {𝑚 ∈ ℕ ∣
∃𝑡 ∈ ℕ
∃𝑛 ∈
(bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚} → (𝑘 ∈ ℕ → ¬ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑘)) |
109 | 103, 105,
108 | sylc 65 |
. . . . . . . . 9
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑘 ∈ ((◡(𝐺‘𝐴) “ ℕ) ∖ {𝑚 ∈ ℕ ∣
∃𝑡 ∈ ℕ
∃𝑛 ∈
(bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚})) → ¬ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑘) |
110 | 109 | iffalsed 4476 |
. . . . . . . 8
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑘 ∈ ((◡(𝐺‘𝐴) “ ℕ) ∖ {𝑚 ∈ ℕ ∣
∃𝑡 ∈ ℕ
∃𝑛 ∈
(bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚})) → if(∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑘, 1, 0) = 0) |
111 | 110 | oveq1d 7286 |
. . . . . . 7
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑘 ∈ ((◡(𝐺‘𝐴) “ ℕ) ∖ {𝑚 ∈ ℕ ∣
∃𝑡 ∈ ℕ
∃𝑛 ∈
(bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚})) → (if(∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑘, 1, 0) · 𝑘) = (0 · 𝑘)) |
112 | | nnsscn 11978 |
. . . . . . . . . 10
⊢ ℕ
⊆ ℂ |
113 | 104, 112 | sstrdi 3938 |
. . . . . . . . 9
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → ((◡(𝐺‘𝐴) “ ℕ) ∖ {𝑚 ∈ ℕ ∣
∃𝑡 ∈ ℕ
∃𝑛 ∈
(bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚}) ⊆ ℂ) |
114 | 113 | sselda 3926 |
. . . . . . . 8
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑘 ∈ ((◡(𝐺‘𝐴) “ ℕ) ∖ {𝑚 ∈ ℕ ∣
∃𝑡 ∈ ℕ
∃𝑛 ∈
(bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚})) → 𝑘 ∈ ℂ) |
115 | 114 | mul02d 11173 |
. . . . . . 7
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑘 ∈ ((◡(𝐺‘𝐴) “ ℕ) ∖ {𝑚 ∈ ℕ ∣
∃𝑡 ∈ ℕ
∃𝑛 ∈
(bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚})) → (0 · 𝑘) = 0) |
116 | 111, 115 | eqtrd 2780 |
. . . . . 6
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑘 ∈ ((◡(𝐺‘𝐴) “ ℕ) ∖ {𝑚 ∈ ℕ ∣
∃𝑡 ∈ ℕ
∃𝑛 ∈
(bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚})) → (if(∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑘, 1, 0) · 𝑘) = 0) |
117 | 55, 101, 116, 40 | fsumss 15435 |
. . . . 5
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → Σ𝑘 ∈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚} (if(∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑘, 1, 0) · 𝑘) = Σ𝑘 ∈ (◡(𝐺‘𝐴) “ ℕ)(if(∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑘, 1, 0) · 𝑘)) |
118 | 92, 117 | eqtr3d 2782 |
. . . 4
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → Σ𝑤 ∈ ∪
𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡)))((2↑(2nd ‘𝑤)) · (1st
‘𝑤)) = Σ𝑘 ∈ (◡(𝐺‘𝐴) “ ℕ)(if(∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑘, 1, 0) · 𝑘)) |
119 | 2, 3, 4, 5, 6, 7, 8, 9, 10 | eulerpartlemt0 32332 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) ↔ (𝐴 ∈ (ℕ0
↑m ℕ) ∧ (◡𝐴 “ ℕ) ∈ Fin ∧ (◡𝐴 “ ℕ) ⊆ 𝐽)) |
120 | 119 | simp1bi 1144 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → 𝐴 ∈ (ℕ0
↑m ℕ)) |
121 | | elmapi 8620 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ (ℕ0
↑m ℕ) → 𝐴:ℕ⟶ℕ0) |
122 | 120, 121 | syl 17 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → 𝐴:ℕ⟶ℕ0) |
123 | 122 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)) → 𝐴:ℕ⟶ℕ0) |
124 | | cnvimass 5988 |
. . . . . . . . . . . . 13
⊢ (◡𝐴 “ ℕ) ⊆ dom 𝐴 |
125 | 124, 122 | fssdm 6618 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → (◡𝐴 “ ℕ) ⊆
ℕ) |
126 | 125 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)) → (◡𝐴 “ ℕ) ⊆
ℕ) |
127 | | inss1 4168 |
. . . . . . . . . . . 12
⊢ ((◡𝐴 “ ℕ) ∩ 𝐽) ⊆ (◡𝐴 “ ℕ) |
128 | 127, 77 | sselid 3924 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)) → 𝑡 ∈ (◡𝐴 “ ℕ)) |
129 | 126, 128 | sseldd 3927 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)) → 𝑡 ∈ ℕ) |
130 | 123, 129 | ffvelrnd 6959 |
. . . . . . . . 9
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)) → (𝐴‘𝑡) ∈
ℕ0) |
131 | | bitsfi 16142 |
. . . . . . . . 9
⊢ ((𝐴‘𝑡) ∈ ℕ0 →
(bits‘(𝐴‘𝑡)) ∈ Fin) |
132 | 130, 131 | syl 17 |
. . . . . . . 8
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)) → (bits‘(𝐴‘𝑡)) ∈ Fin) |
133 | 129 | nncnd 11989 |
. . . . . . . 8
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)) → 𝑡 ∈ ℂ) |
134 | | 2cnd 12051 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ (𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽) ∧ 𝑛 ∈ (bits‘(𝐴‘𝑡)))) → 2 ∈
ℂ) |
135 | | simprr 770 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ (𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽) ∧ 𝑛 ∈ (bits‘(𝐴‘𝑡)))) → 𝑛 ∈ (bits‘(𝐴‘𝑡))) |
136 | 80, 135 | sselid 3924 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ (𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽) ∧ 𝑛 ∈ (bits‘(𝐴‘𝑡)))) → 𝑛 ∈ ℕ0) |
137 | 134, 136 | expcld 13862 |
. . . . . . . . 9
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ (𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽) ∧ 𝑛 ∈ (bits‘(𝐴‘𝑡)))) → (2↑𝑛) ∈ ℂ) |
138 | 137 | anassrs 468 |
. . . . . . . 8
⊢ (((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)) ∧ 𝑛 ∈ (bits‘(𝐴‘𝑡))) → (2↑𝑛) ∈ ℂ) |
139 | 132, 133,
138 | fsummulc1 15495 |
. . . . . . 7
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)) → (Σ𝑛 ∈ (bits‘(𝐴‘𝑡))(2↑𝑛) · 𝑡) = Σ𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡)) |
140 | 139 | sumeq2dv 15413 |
. . . . . 6
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → Σ𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)(Σ𝑛 ∈ (bits‘(𝐴‘𝑡))(2↑𝑛) · 𝑡) = Σ𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)Σ𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡)) |
141 | | bitsinv1 16147 |
. . . . . . . . 9
⊢ ((𝐴‘𝑡) ∈ ℕ0 →
Σ𝑛 ∈
(bits‘(𝐴‘𝑡))(2↑𝑛) = (𝐴‘𝑡)) |
142 | 141 | oveq1d 7286 |
. . . . . . . 8
⊢ ((𝐴‘𝑡) ∈ ℕ0 →
(Σ𝑛 ∈
(bits‘(𝐴‘𝑡))(2↑𝑛) · 𝑡) = ((𝐴‘𝑡) · 𝑡)) |
143 | 130, 142 | syl 17 |
. . . . . . 7
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)) → (Σ𝑛 ∈ (bits‘(𝐴‘𝑡))(2↑𝑛) · 𝑡) = ((𝐴‘𝑡) · 𝑡)) |
144 | 143 | sumeq2dv 15413 |
. . . . . 6
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → Σ𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)(Σ𝑛 ∈ (bits‘(𝐴‘𝑡))(2↑𝑛) · 𝑡) = Σ𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)((𝐴‘𝑡) · 𝑡)) |
145 | | vex 3435 |
. . . . . . . . . 10
⊢ 𝑡 ∈ V |
146 | | vex 3435 |
. . . . . . . . . 10
⊢ 𝑛 ∈ V |
147 | 145, 146 | op2ndd 7835 |
. . . . . . . . 9
⊢ (𝑤 = 〈𝑡, 𝑛〉 → (2nd ‘𝑤) = 𝑛) |
148 | 147 | oveq2d 7287 |
. . . . . . . 8
⊢ (𝑤 = 〈𝑡, 𝑛〉 → (2↑(2nd
‘𝑤)) = (2↑𝑛)) |
149 | 145, 146 | op1std 7834 |
. . . . . . . 8
⊢ (𝑤 = 〈𝑡, 𝑛〉 → (1st ‘𝑤) = 𝑡) |
150 | 148, 149 | oveq12d 7289 |
. . . . . . 7
⊢ (𝑤 = 〈𝑡, 𝑛〉 → ((2↑(2nd
‘𝑤)) ·
(1st ‘𝑤))
= ((2↑𝑛) ·
𝑡)) |
151 | | inss2 4169 |
. . . . . . . . . 10
⊢ (𝑇 ∩ 𝑅) ⊆ 𝑅 |
152 | 151 | sseli 3922 |
. . . . . . . . 9
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → 𝐴 ∈ 𝑅) |
153 | | cnveq 5781 |
. . . . . . . . . . . 12
⊢ (𝑓 = 𝐴 → ◡𝑓 = ◡𝐴) |
154 | 153 | imaeq1d 5967 |
. . . . . . . . . . 11
⊢ (𝑓 = 𝐴 → (◡𝑓 “ ℕ) = (◡𝐴 “ ℕ)) |
155 | 154 | eleq1d 2825 |
. . . . . . . . . 10
⊢ (𝑓 = 𝐴 → ((◡𝑓 “ ℕ) ∈ Fin ↔ (◡𝐴 “ ℕ) ∈
Fin)) |
156 | 155, 9 | elab2g 3613 |
. . . . . . . . 9
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → (𝐴 ∈ 𝑅 ↔ (◡𝐴 “ ℕ) ∈
Fin)) |
157 | 152, 156 | mpbid 231 |
. . . . . . . 8
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → (◡𝐴 “ ℕ) ∈
Fin) |
158 | | ssfi 8938 |
. . . . . . . 8
⊢ (((◡𝐴 “ ℕ) ∈ Fin ∧ ((◡𝐴 “ ℕ) ∩ 𝐽) ⊆ (◡𝐴 “ ℕ)) → ((◡𝐴 “ ℕ) ∩ 𝐽) ∈ Fin) |
159 | 157, 127,
158 | sylancl 586 |
. . . . . . 7
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → ((◡𝐴 “ ℕ) ∩ 𝐽) ∈ Fin) |
160 | 133 | adantrr 714 |
. . . . . . . 8
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ (𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽) ∧ 𝑛 ∈ (bits‘(𝐴‘𝑡)))) → 𝑡 ∈ ℂ) |
161 | 137, 160 | mulcld 10996 |
. . . . . . 7
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ (𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽) ∧ 𝑛 ∈ (bits‘(𝐴‘𝑡)))) → ((2↑𝑛) · 𝑡) ∈ ℂ) |
162 | 150, 159,
132, 161 | fsum2d 15481 |
. . . . . 6
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → Σ𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)Σ𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = Σ𝑤 ∈ ∪
𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡)))((2↑(2nd ‘𝑤)) · (1st
‘𝑤))) |
163 | 140, 144,
162 | 3eqtr3d 2788 |
. . . . 5
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → Σ𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)((𝐴‘𝑡) · 𝑡) = Σ𝑤 ∈ ∪
𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡)))((2↑(2nd ‘𝑤)) · (1st
‘𝑤))) |
164 | | inss1 4168 |
. . . . . . . . 9
⊢ (𝑇 ∩ 𝑅) ⊆ 𝑇 |
165 | 164 | sseli 3922 |
. . . . . . . 8
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → 𝐴 ∈ 𝑇) |
166 | 154 | sseq1d 3957 |
. . . . . . . . . 10
⊢ (𝑓 = 𝐴 → ((◡𝑓 “ ℕ) ⊆ 𝐽 ↔ (◡𝐴 “ ℕ) ⊆ 𝐽)) |
167 | 166, 10 | elrab2 3629 |
. . . . . . . . 9
⊢ (𝐴 ∈ 𝑇 ↔ (𝐴 ∈ (ℕ0
↑m ℕ) ∧ (◡𝐴 “ ℕ) ⊆ 𝐽)) |
168 | 167 | simprbi 497 |
. . . . . . . 8
⊢ (𝐴 ∈ 𝑇 → (◡𝐴 “ ℕ) ⊆ 𝐽) |
169 | 165, 168 | syl 17 |
. . . . . . 7
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → (◡𝐴 “ ℕ) ⊆ 𝐽) |
170 | | df-ss 3909 |
. . . . . . 7
⊢ ((◡𝐴 “ ℕ) ⊆ 𝐽 ↔ ((◡𝐴 “ ℕ) ∩ 𝐽) = (◡𝐴 “ ℕ)) |
171 | 169, 170 | sylib 217 |
. . . . . 6
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → ((◡𝐴 “ ℕ) ∩ 𝐽) = (◡𝐴 “ ℕ)) |
172 | 171 | sumeq1d 15411 |
. . . . 5
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → Σ𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)((𝐴‘𝑡) · 𝑡) = Σ𝑡 ∈ (◡𝐴 “ ℕ)((𝐴‘𝑡) · 𝑡)) |
173 | 163, 172 | eqtr3d 2782 |
. . . 4
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → Σ𝑤 ∈ ∪
𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡)))((2↑(2nd ‘𝑤)) · (1st
‘𝑤)) = Σ𝑡 ∈ (◡𝐴 “ ℕ)((𝐴‘𝑡) · 𝑡)) |
174 | 27, 118, 173 | 3eqtr2d 2786 |
. . 3
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → Σ𝑘 ∈ (◡(𝐺‘𝐴) “ ℕ)(((𝐺‘𝐴)‘𝑘) · 𝑘) = Σ𝑡 ∈ (◡𝐴 “ ℕ)((𝐴‘𝑡) · 𝑡)) |
175 | | fveq2 6771 |
. . . . 5
⊢ (𝑘 = 𝑡 → (𝐴‘𝑘) = (𝐴‘𝑡)) |
176 | | id 22 |
. . . . 5
⊢ (𝑘 = 𝑡 → 𝑘 = 𝑡) |
177 | 175, 176 | oveq12d 7289 |
. . . 4
⊢ (𝑘 = 𝑡 → ((𝐴‘𝑘) · 𝑘) = ((𝐴‘𝑡) · 𝑡)) |
178 | 177 | cbvsumv 15406 |
. . 3
⊢
Σ𝑘 ∈
(◡𝐴 “ ℕ)((𝐴‘𝑘) · 𝑘) = Σ𝑡 ∈ (◡𝐴 “ ℕ)((𝐴‘𝑡) · 𝑡) |
179 | 174, 178 | eqtr4di 2798 |
. 2
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → Σ𝑘 ∈ (◡(𝐺‘𝐴) “ ℕ)(((𝐺‘𝐴)‘𝑘) · 𝑘) = Σ𝑘 ∈ (◡𝐴 “ ℕ)((𝐴‘𝑘) · 𝑘)) |
180 | | 0nn0 12248 |
. . . . . . . 8
⊢ 0 ∈
ℕ0 |
181 | | 1nn0 12249 |
. . . . . . . 8
⊢ 1 ∈
ℕ0 |
182 | | prssi 4760 |
. . . . . . . 8
⊢ ((0
∈ ℕ0 ∧ 1 ∈ ℕ0) → {0, 1}
⊆ ℕ0) |
183 | 180, 181,
182 | mp2an 689 |
. . . . . . 7
⊢ {0, 1}
⊆ ℕ0 |
184 | | fss 6615 |
. . . . . . 7
⊢ (((𝐺‘𝐴):ℕ⟶{0, 1} ∧ {0, 1} ⊆
ℕ0) → (𝐺‘𝐴):ℕ⟶ℕ0) |
185 | 183, 184 | mpan2 688 |
. . . . . 6
⊢ ((𝐺‘𝐴):ℕ⟶{0, 1} → (𝐺‘𝐴):ℕ⟶ℕ0) |
186 | | nn0ex 12239 |
. . . . . . . 8
⊢
ℕ0 ∈ V |
187 | | nnex 11979 |
. . . . . . . 8
⊢ ℕ
∈ V |
188 | 186, 187 | elmap 8642 |
. . . . . . 7
⊢ ((𝐺‘𝐴) ∈ (ℕ0
↑m ℕ) ↔ (𝐺‘𝐴):ℕ⟶ℕ0) |
189 | 188 | biimpri 227 |
. . . . . 6
⊢ ((𝐺‘𝐴):ℕ⟶ℕ0 →
(𝐺‘𝐴) ∈ (ℕ0
↑m ℕ)) |
190 | 19, 185, 189 | 3syl 18 |
. . . . 5
⊢ ((𝐺‘𝐴) ∈ ({0, 1} ↑m ℕ)
→ (𝐺‘𝐴) ∈ (ℕ0
↑m ℕ)) |
191 | 190 | anim1i 615 |
. . . 4
⊢ (((𝐺‘𝐴) ∈ ({0, 1} ↑m ℕ)
∧ (𝐺‘𝐴) ∈ 𝑅) → ((𝐺‘𝐴) ∈ (ℕ0
↑m ℕ) ∧ (𝐺‘𝐴) ∈ 𝑅)) |
192 | | elin 3908 |
. . . 4
⊢ ((𝐺‘𝐴) ∈ ((ℕ0
↑m ℕ) ∩ 𝑅) ↔ ((𝐺‘𝐴) ∈ (ℕ0
↑m ℕ) ∧ (𝐺‘𝐴) ∈ 𝑅)) |
193 | 191, 16, 192 | 3imtr4i 292 |
. . 3
⊢ ((𝐺‘𝐴) ∈ (({0, 1} ↑m
ℕ) ∩ 𝑅) →
(𝐺‘𝐴) ∈ ((ℕ0
↑m ℕ) ∩ 𝑅)) |
194 | | eulerpart.s |
. . . 4
⊢ 𝑆 = (𝑓 ∈ ((ℕ0
↑m ℕ) ∩ 𝑅) ↦ Σ𝑘 ∈ ℕ ((𝑓‘𝑘) · 𝑘)) |
195 | 9, 194 | eulerpartlemsv2 32321 |
. . 3
⊢ ((𝐺‘𝐴) ∈ ((ℕ0
↑m ℕ) ∩ 𝑅) → (𝑆‘(𝐺‘𝐴)) = Σ𝑘 ∈ (◡(𝐺‘𝐴) “ ℕ)(((𝐺‘𝐴)‘𝑘) · 𝑘)) |
196 | 15, 193, 195 | 3syl 18 |
. 2
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → (𝑆‘(𝐺‘𝐴)) = Σ𝑘 ∈ (◡(𝐺‘𝐴) “ ℕ)(((𝐺‘𝐴)‘𝑘) · 𝑘)) |
197 | 120, 152 | elind 4133 |
. . 3
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → 𝐴 ∈ ((ℕ0
↑m ℕ) ∩ 𝑅)) |
198 | 9, 194 | eulerpartlemsv2 32321 |
. . 3
⊢ (𝐴 ∈ ((ℕ0
↑m ℕ) ∩ 𝑅) → (𝑆‘𝐴) = Σ𝑘 ∈ (◡𝐴 “ ℕ)((𝐴‘𝑘) · 𝑘)) |
199 | 197, 198 | syl 17 |
. 2
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → (𝑆‘𝐴) = Σ𝑘 ∈ (◡𝐴 “ ℕ)((𝐴‘𝑘) · 𝑘)) |
200 | 179, 196,
199 | 3eqtr4d 2790 |
1
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → (𝑆‘(𝐺‘𝐴)) = (𝑆‘𝐴)) |