| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | cnvimass 6100 | . . . . . . . 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 34374 | . . . . . . . . . . . . 13
⊢ 𝐺:(𝑇 ∩ 𝑅)–1-1-onto→(({0,
1} ↑m ℕ) ∩ 𝑅) | 
| 13 |  | f1of 6848 | . . . . . . . . . . . . 13
⊢ (𝐺:(𝑇 ∩ 𝑅)–1-1-onto→(({0,
1} ↑m ℕ) ∩ 𝑅) → 𝐺:(𝑇 ∩ 𝑅)⟶(({0, 1} ↑m
ℕ) ∩ 𝑅)) | 
| 14 | 12, 13 | ax-mp 5 | . . . . . . . . . . . 12
⊢ 𝐺:(𝑇 ∩ 𝑅)⟶(({0, 1} ↑m
ℕ) ∩ 𝑅) | 
| 15 | 14 | ffvelcdmi 7103 | . . . . . . . . . . 11
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → (𝐺‘𝐴) ∈ (({0, 1} ↑m
ℕ) ∩ 𝑅)) | 
| 16 |  | elin 3967 | . . . . . . . . . . 11
⊢ ((𝐺‘𝐴) ∈ (({0, 1} ↑m
ℕ) ∩ 𝑅) ↔
((𝐺‘𝐴) ∈ ({0, 1} ↑m ℕ)
∧ (𝐺‘𝐴) ∈ 𝑅)) | 
| 17 | 15, 16 | sylib 218 | . . . . . . . . . 10
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → ((𝐺‘𝐴) ∈ ({0, 1} ↑m ℕ)
∧ (𝐺‘𝐴) ∈ 𝑅)) | 
| 18 | 17 | simpld 494 | . . . . . . . . 9
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → (𝐺‘𝐴) ∈ ({0, 1} ↑m
ℕ)) | 
| 19 |  | elmapi 8889 | . . . . . . . . 9
⊢ ((𝐺‘𝐴) ∈ ({0, 1} ↑m ℕ)
→ (𝐺‘𝐴):ℕ⟶{0,
1}) | 
| 20 |  | fdm 6745 | . . . . . . . . 9
⊢ ((𝐺‘𝐴):ℕ⟶{0, 1} → dom (𝐺‘𝐴) = ℕ) | 
| 21 | 18, 19, 20 | 3syl 18 | . . . . . . . 8
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → dom (𝐺‘𝐴) = ℕ) | 
| 22 | 1, 21 | sseqtrid 4026 | . . . . . . 7
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → (◡(𝐺‘𝐴) “ ℕ) ⊆
ℕ) | 
| 23 | 22 | sselda 3983 | . . . . . 6
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑘 ∈ (◡(𝐺‘𝐴) “ ℕ)) → 𝑘 ∈
ℕ) | 
| 24 | 2, 3, 4, 5, 6, 7, 8, 9, 10, 11 | eulerpartlemgvv 34378 | . . . . . . 7
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑘 ∈ ℕ) → ((𝐺‘𝐴)‘𝑘) = if(∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑘, 1, 0)) | 
| 25 | 24 | oveq1d 7446 | . . . . . 6
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑘 ∈ ℕ) → (((𝐺‘𝐴)‘𝑘) · 𝑘) = (if(∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑘, 1, 0) · 𝑘)) | 
| 26 | 23, 25 | syldan 591 | . . . . 5
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑘 ∈ (◡(𝐺‘𝐴) “ ℕ)) → (((𝐺‘𝐴)‘𝑘) · 𝑘) = (if(∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑘, 1, 0) · 𝑘)) | 
| 27 | 26 | sumeq2dv 15738 | . . . 4
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → Σ𝑘 ∈ (◡(𝐺‘𝐴) “ ℕ)(((𝐺‘𝐴)‘𝑘) · 𝑘) = Σ𝑘 ∈ (◡(𝐺‘𝐴) “ ℕ)(if(∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑘, 1, 0) · 𝑘)) | 
| 28 |  | eqeq2 2749 | . . . . . . . . . . . . 13
⊢ (𝑚 = 𝑘 → (((2↑𝑛) · 𝑡) = 𝑚 ↔ ((2↑𝑛) · 𝑡) = 𝑘)) | 
| 29 | 28 | 2rexbidv 3222 | . . . . . . . . . . . 12
⊢ (𝑚 = 𝑘 → (∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚 ↔ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑘)) | 
| 30 | 29 | elrab 3692 | . . . . . . . . . . 11
⊢ (𝑘 ∈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚} ↔ (𝑘 ∈ ℕ ∧ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑘)) | 
| 31 | 30 | simprbi 496 | . . . . . . . . . 10
⊢ (𝑘 ∈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚} → ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑘) | 
| 32 | 31 | iftrued 4533 | . . . . . . . . 9
⊢ (𝑘 ∈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚} → if(∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑘, 1, 0) = 1) | 
| 33 | 32 | oveq1d 7446 | . . . . . . . 8
⊢ (𝑘 ∈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚} → (if(∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑘, 1, 0) · 𝑘) = (1 · 𝑘)) | 
| 34 |  | elrabi 3687 | . . . . . . . . . 10
⊢ (𝑘 ∈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚} → 𝑘 ∈ ℕ) | 
| 35 | 34 | nncnd 12282 | . . . . . . . . 9
⊢ (𝑘 ∈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚} → 𝑘 ∈ ℂ) | 
| 36 | 35 | mullidd 11279 | . . . . . . . 8
⊢ (𝑘 ∈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚} → (1 · 𝑘) = 𝑘) | 
| 37 | 33, 36 | eqtrd 2777 | . . . . . . 7
⊢ (𝑘 ∈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚} → (if(∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑘, 1, 0) · 𝑘) = 𝑘) | 
| 38 | 37 | sumeq2i 15734 | . . . . . 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 34381 | . . . . . . . . 9
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → (◡(𝐺‘𝐴) “ ℕ) ∈
Fin) | 
| 41 | 34 | adantl 481 | . . . . . . . . . . . 12
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑘 ∈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚}) → 𝑘 ∈ ℕ) | 
| 42 | 41, 24 | syldan 591 | . . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑘 ∈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚}) → ((𝐺‘𝐴)‘𝑘) = if(∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑘, 1, 0)) | 
| 43 | 31 | adantl 481 | . . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑘 ∈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚}) → ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑘) | 
| 44 | 43 | iftrued 4533 | . . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑘 ∈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚}) → if(∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑘, 1, 0) = 1) | 
| 45 | 42, 44 | eqtrd 2777 | . . . . . . . . . . . . 13
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑘 ∈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚}) → ((𝐺‘𝐴)‘𝑘) = 1) | 
| 46 |  | 1nn 12277 | . . . . . . . . . . . . 13
⊢ 1 ∈
ℕ | 
| 47 | 45, 46 | eqeltrdi 2849 | . . . . . . . . . . . 12
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑘 ∈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚}) → ((𝐺‘𝐴)‘𝑘) ∈ ℕ) | 
| 48 |  | ffn 6736 | . . . . . . . . . . . . . 14
⊢ ((𝐺‘𝐴):ℕ⟶{0, 1} → (𝐺‘𝐴) Fn ℕ) | 
| 49 |  | elpreima 7078 | . . . . . . . . . . . . . 14
⊢ ((𝐺‘𝐴) Fn ℕ → (𝑘 ∈ (◡(𝐺‘𝐴) “ ℕ) ↔ (𝑘 ∈ ℕ ∧ ((𝐺‘𝐴)‘𝑘) ∈ ℕ))) | 
| 50 | 18, 19, 48, 49 | 4syl 19 | . . . . . . . . . . . . 13
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → (𝑘 ∈ (◡(𝐺‘𝐴) “ ℕ) ↔ (𝑘 ∈ ℕ ∧ ((𝐺‘𝐴)‘𝑘) ∈ ℕ))) | 
| 51 | 50 | adantr 480 | . . . . . . . . . . . 12
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑘 ∈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚}) → (𝑘 ∈ (◡(𝐺‘𝐴) “ ℕ) ↔ (𝑘 ∈ ℕ ∧ ((𝐺‘𝐴)‘𝑘) ∈ ℕ))) | 
| 52 | 41, 47, 51 | mpbir2and 713 | . . . . . . . . . . 11
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑘 ∈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚}) → 𝑘 ∈ (◡(𝐺‘𝐴) “ ℕ)) | 
| 53 | 52 | ex 412 | . . . . . . . . . 10
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → (𝑘 ∈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚} → 𝑘 ∈ (◡(𝐺‘𝐴) “ ℕ))) | 
| 54 | 53 | ssrdv 3989 | . . . . . . . . 9
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚} ⊆ (◡(𝐺‘𝐴) “ ℕ)) | 
| 55 |  | ssfi 9213 | . . . . . . . . 9
⊢ (((◡(𝐺‘𝐴) “ ℕ) ∈ Fin ∧ {𝑚 ∈ ℕ ∣
∃𝑡 ∈ ℕ
∃𝑛 ∈
(bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚} ⊆ (◡(𝐺‘𝐴) “ ℕ)) → {𝑚 ∈ ℕ ∣
∃𝑡 ∈ ℕ
∃𝑛 ∈
(bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚} ∈ Fin) | 
| 56 | 40, 54, 55 | syl2anc 584 | . . . . . . . 8
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚} ∈ Fin) | 
| 57 |  | cnvexg 7946 | . . . . . . . . . . 11
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → ◡𝐴 ∈ V) | 
| 58 |  | imaexg 7935 | . . . . . . . . . . 11
⊢ (◡𝐴 ∈ V → (◡𝐴 “ ℕ) ∈ V) | 
| 59 |  | inex1g 5319 | . . . . . . . . . . 11
⊢ ((◡𝐴 “ ℕ) ∈ V → ((◡𝐴 “ ℕ) ∩ 𝐽) ∈ V) | 
| 60 | 57, 58, 59 | 3syl 18 | . . . . . . . . . 10
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → ((◡𝐴 “ ℕ) ∩ 𝐽) ∈ V) | 
| 61 |  | vsnex 5434 | . . . . . . . . . . . 12
⊢ {𝑡} ∈ V | 
| 62 |  | fvex 6919 | . . . . . . . . . . . 12
⊢
(bits‘(𝐴‘𝑡)) ∈ V | 
| 63 | 61, 62 | xpex 7773 | . . . . . . . . . . 11
⊢ ({𝑡} × (bits‘(𝐴‘𝑡))) ∈ V | 
| 64 | 63 | rgenw 3065 | . . . . . . . . . 10
⊢
∀𝑡 ∈
((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡))) ∈ V | 
| 65 |  | iunexg 7988 | . . . . . . . . . 10
⊢ ((((◡𝐴 “ ℕ) ∩ 𝐽) ∈ V ∧ ∀𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡))) ∈ V) → ∪ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡))) ∈ V) | 
| 66 | 60, 64, 65 | sylancl 586 | . . . . . . . . 9
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → ∪
𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡))) ∈ V) | 
| 67 |  | eqid 2737 | . . . . . . . . . 10
⊢ ∪ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡))) = ∪
𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡))) | 
| 68 | 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 67 | eulerpartlemgh 34380 | . . . . . . . . 9
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → (𝐹 ↾ ∪
𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡)))):∪
𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡)))–1-1-onto→{𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚}) | 
| 69 |  | f1oeng 9011 | . . . . . . . . 9
⊢
((∪ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡))) ∈ V ∧ (𝐹 ↾ ∪
𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡)))):∪
𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡)))–1-1-onto→{𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚}) → ∪
𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡))) ≈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚}) | 
| 70 | 66, 68, 69 | syl2anc 584 | . . . . . . . 8
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → ∪
𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡))) ≈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚}) | 
| 71 |  | enfii 9226 | . . . . . . . 8
⊢ (({𝑚 ∈ ℕ ∣
∃𝑡 ∈ ℕ
∃𝑛 ∈
(bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚} ∈ Fin ∧ ∪ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡))) ≈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚}) → ∪
𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡))) ∈ Fin) | 
| 72 | 56, 70, 71 | syl2anc 584 | . . . . . . 7
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → ∪
𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡))) ∈ Fin) | 
| 73 |  | fvres 6925 | . . . . . . . . 9
⊢ (𝑤 ∈ ∪ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡))) → ((𝐹 ↾ ∪
𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡))))‘𝑤) = (𝐹‘𝑤)) | 
| 74 | 73 | adantl 481 | . . . . . . . 8
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑤 ∈ ∪
𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡)))) → ((𝐹 ↾ ∪
𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡))))‘𝑤) = (𝐹‘𝑤)) | 
| 75 |  | inss2 4238 | . . . . . . . . . . . . . . 15
⊢ ((◡𝐴 “ ℕ) ∩ 𝐽) ⊆ 𝐽 | 
| 76 |  | simpr 484 | . . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)) → 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)) | 
| 77 | 75, 76 | sselid 3981 | . . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)) → 𝑡 ∈ 𝐽) | 
| 78 | 77 | snssd 4809 | . . . . . . . . . . . . 13
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)) → {𝑡} ⊆ 𝐽) | 
| 79 |  | bitsss 16463 | . . . . . . . . . . . . 13
⊢
(bits‘(𝐴‘𝑡)) ⊆
ℕ0 | 
| 80 |  | xpss12 5700 | . . . . . . . . . . . . 13
⊢ (({𝑡} ⊆ 𝐽 ∧ (bits‘(𝐴‘𝑡)) ⊆ ℕ0) →
({𝑡} ×
(bits‘(𝐴‘𝑡))) ⊆ (𝐽 ×
ℕ0)) | 
| 81 | 78, 79, 80 | sylancl 586 | . . . . . . . . . . . 12
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)) → ({𝑡} × (bits‘(𝐴‘𝑡))) ⊆ (𝐽 ×
ℕ0)) | 
| 82 | 81 | ralrimiva 3146 | . . . . . . . . . . 11
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → ∀𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡))) ⊆ (𝐽 ×
ℕ0)) | 
| 83 |  | iunss 5045 | . . . . . . . . . . 11
⊢ (∪ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡))) ⊆ (𝐽 × ℕ0) ↔
∀𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡))) ⊆ (𝐽 ×
ℕ0)) | 
| 84 | 82, 83 | sylibr 234 | . . . . . . . . . 10
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → ∪
𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡))) ⊆ (𝐽 ×
ℕ0)) | 
| 85 | 84 | sselda 3983 | . . . . . . . . 9
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑤 ∈ ∪
𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡)))) → 𝑤 ∈ (𝐽 ×
ℕ0)) | 
| 86 | 5, 6 | oddpwdcv 34357 | . . . . . . . . 9
⊢ (𝑤 ∈ (𝐽 × ℕ0) → (𝐹‘𝑤) = ((2↑(2nd ‘𝑤)) · (1st
‘𝑤))) | 
| 87 | 85, 86 | syl 17 | . . . . . . . 8
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑤 ∈ ∪
𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡)))) → (𝐹‘𝑤) = ((2↑(2nd ‘𝑤)) · (1st
‘𝑤))) | 
| 88 | 74, 87 | eqtrd 2777 | . . . . . . 7
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑤 ∈ ∪
𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡)))) → ((𝐹 ↾ ∪
𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡))))‘𝑤) = ((2↑(2nd ‘𝑤)) · (1st
‘𝑤))) | 
| 89 | 41 | nncnd 12282 | . . . . . . 7
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑘 ∈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚}) → 𝑘 ∈ ℂ) | 
| 90 | 39, 72, 68, 88, 89 | fsumf1o 15759 | . . . . . 6
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → Σ𝑘 ∈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚}𝑘 = Σ𝑤 ∈ ∪
𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡)))((2↑(2nd ‘𝑤)) · (1st
‘𝑤))) | 
| 91 | 38, 90 | eqtrid 2789 | . . . . 5
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → Σ𝑘 ∈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚} (if(∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑘, 1, 0) · 𝑘) = Σ𝑤 ∈ ∪
𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡)))((2↑(2nd ‘𝑤)) · (1st
‘𝑤))) | 
| 92 |  | ax-1cn 11213 | . . . . . . . . 9
⊢ 1 ∈
ℂ | 
| 93 |  | 0cn 11253 | . . . . . . . . 9
⊢ 0 ∈
ℂ | 
| 94 | 92, 93 | ifcli 4573 | . . . . . . . 8
⊢
if(∃𝑡 ∈
ℕ ∃𝑛 ∈
(bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑘, 1, 0) ∈ ℂ | 
| 95 | 94 | a1i 11 | . . . . . . 7
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑘 ∈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚}) → if(∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑘, 1, 0) ∈ ℂ) | 
| 96 |  | ssrab2 4080 | . . . . . . . . 9
⊢ {𝑚 ∈ ℕ ∣
∃𝑡 ∈ ℕ
∃𝑛 ∈
(bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚} ⊆ ℕ | 
| 97 |  | simpr 484 | . . . . . . . . 9
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑘 ∈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚}) → 𝑘 ∈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚}) | 
| 98 | 96, 97 | sselid 3981 | . . . . . . . 8
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑘 ∈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚}) → 𝑘 ∈ ℕ) | 
| 99 | 98 | nncnd 12282 | . . . . . . 7
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑘 ∈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚}) → 𝑘 ∈ ℂ) | 
| 100 | 95, 99 | mulcld 11281 | . . . . . 6
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑘 ∈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚}) → (if(∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑘, 1, 0) · 𝑘) ∈ ℂ) | 
| 101 |  | simpr 484 | . . . . . . . . . . 11
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑘 ∈ ((◡(𝐺‘𝐴) “ ℕ) ∖ {𝑚 ∈ ℕ ∣
∃𝑡 ∈ ℕ
∃𝑛 ∈
(bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚})) → 𝑘 ∈ ((◡(𝐺‘𝐴) “ ℕ) ∖ {𝑚 ∈ ℕ ∣
∃𝑡 ∈ ℕ
∃𝑛 ∈
(bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚})) | 
| 102 | 101 | eldifbd 3964 | . . . . . . . . . 10
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑘 ∈ ((◡(𝐺‘𝐴) “ ℕ) ∖ {𝑚 ∈ ℕ ∣
∃𝑡 ∈ ℕ
∃𝑛 ∈
(bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚})) → ¬ 𝑘 ∈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚}) | 
| 103 | 22 | ssdifssd 4147 | . . . . . . . . . . 11
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → ((◡(𝐺‘𝐴) “ ℕ) ∖ {𝑚 ∈ ℕ ∣
∃𝑡 ∈ ℕ
∃𝑛 ∈
(bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚}) ⊆ ℕ) | 
| 104 | 103 | sselda 3983 | . . . . . . . . . 10
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑘 ∈ ((◡(𝐺‘𝐴) “ ℕ) ∖ {𝑚 ∈ ℕ ∣
∃𝑡 ∈ ℕ
∃𝑛 ∈
(bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚})) → 𝑘 ∈ ℕ) | 
| 105 | 30 | notbii 320 | . . . . . . . . . . 11
⊢ (¬
𝑘 ∈ {𝑚 ∈ ℕ ∣
∃𝑡 ∈ ℕ
∃𝑛 ∈
(bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚} ↔ ¬ (𝑘 ∈ ℕ ∧ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑘)) | 
| 106 |  | imnan 399 | . . . . . . . . . . 11
⊢ ((𝑘 ∈ ℕ → ¬
∃𝑡 ∈ ℕ
∃𝑛 ∈
(bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑘) ↔ ¬ (𝑘 ∈ ℕ ∧ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑘)) | 
| 107 | 105, 106 | sylbb2 238 | . . . . . . . . . 10
⊢ (¬
𝑘 ∈ {𝑚 ∈ ℕ ∣
∃𝑡 ∈ ℕ
∃𝑛 ∈
(bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚} → (𝑘 ∈ ℕ → ¬ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑘)) | 
| 108 | 102, 104,
107 | sylc 65 | . . . . . . . . 9
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑘 ∈ ((◡(𝐺‘𝐴) “ ℕ) ∖ {𝑚 ∈ ℕ ∣
∃𝑡 ∈ ℕ
∃𝑛 ∈
(bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚})) → ¬ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑘) | 
| 109 | 108 | iffalsed 4536 | . . . . . . . 8
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑘 ∈ ((◡(𝐺‘𝐴) “ ℕ) ∖ {𝑚 ∈ ℕ ∣
∃𝑡 ∈ ℕ
∃𝑛 ∈
(bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚})) → if(∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑘, 1, 0) = 0) | 
| 110 | 109 | oveq1d 7446 | . . . . . . 7
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑘 ∈ ((◡(𝐺‘𝐴) “ ℕ) ∖ {𝑚 ∈ ℕ ∣
∃𝑡 ∈ ℕ
∃𝑛 ∈
(bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚})) → (if(∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑘, 1, 0) · 𝑘) = (0 · 𝑘)) | 
| 111 |  | nnsscn 12271 | . . . . . . . . . 10
⊢ ℕ
⊆ ℂ | 
| 112 | 103, 111 | sstrdi 3996 | . . . . . . . . 9
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → ((◡(𝐺‘𝐴) “ ℕ) ∖ {𝑚 ∈ ℕ ∣
∃𝑡 ∈ ℕ
∃𝑛 ∈
(bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚}) ⊆ ℂ) | 
| 113 | 112 | sselda 3983 | . . . . . . . 8
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑘 ∈ ((◡(𝐺‘𝐴) “ ℕ) ∖ {𝑚 ∈ ℕ ∣
∃𝑡 ∈ ℕ
∃𝑛 ∈
(bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚})) → 𝑘 ∈ ℂ) | 
| 114 | 113 | mul02d 11459 | . . . . . . 7
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑘 ∈ ((◡(𝐺‘𝐴) “ ℕ) ∖ {𝑚 ∈ ℕ ∣
∃𝑡 ∈ ℕ
∃𝑛 ∈
(bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚})) → (0 · 𝑘) = 0) | 
| 115 | 110, 114 | eqtrd 2777 | . . . . . 6
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑘 ∈ ((◡(𝐺‘𝐴) “ ℕ) ∖ {𝑚 ∈ ℕ ∣
∃𝑡 ∈ ℕ
∃𝑛 ∈
(bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚})) → (if(∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑘, 1, 0) · 𝑘) = 0) | 
| 116 | 54, 100, 115, 40 | fsumss 15761 | . . . . 5
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → Σ𝑘 ∈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚} (if(∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑘, 1, 0) · 𝑘) = Σ𝑘 ∈ (◡(𝐺‘𝐴) “ ℕ)(if(∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑘, 1, 0) · 𝑘)) | 
| 117 | 91, 116 | eqtr3d 2779 | . . . 4
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → Σ𝑤 ∈ ∪
𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡)))((2↑(2nd ‘𝑤)) · (1st
‘𝑤)) = Σ𝑘 ∈ (◡(𝐺‘𝐴) “ ℕ)(if(∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑘, 1, 0) · 𝑘)) | 
| 118 | 2, 3, 4, 5, 6, 7, 8, 9, 10 | eulerpartlemt0 34371 | . . . . . . . . . . . . 13
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) ↔ (𝐴 ∈ (ℕ0
↑m ℕ) ∧ (◡𝐴 “ ℕ) ∈ Fin ∧ (◡𝐴 “ ℕ) ⊆ 𝐽)) | 
| 119 | 118 | simp1bi 1146 | . . . . . . . . . . . 12
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → 𝐴 ∈ (ℕ0
↑m ℕ)) | 
| 120 |  | elmapi 8889 | . . . . . . . . . . . 12
⊢ (𝐴 ∈ (ℕ0
↑m ℕ) → 𝐴:ℕ⟶ℕ0) | 
| 121 | 119, 120 | syl 17 | . . . . . . . . . . 11
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → 𝐴:ℕ⟶ℕ0) | 
| 122 | 121 | adantr 480 | . . . . . . . . . 10
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)) → 𝐴:ℕ⟶ℕ0) | 
| 123 |  | cnvimass 6100 | . . . . . . . . . . . . 13
⊢ (◡𝐴 “ ℕ) ⊆ dom 𝐴 | 
| 124 | 123, 121 | fssdm 6755 | . . . . . . . . . . . 12
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → (◡𝐴 “ ℕ) ⊆
ℕ) | 
| 125 | 124 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)) → (◡𝐴 “ ℕ) ⊆
ℕ) | 
| 126 |  | inss1 4237 | . . . . . . . . . . . 12
⊢ ((◡𝐴 “ ℕ) ∩ 𝐽) ⊆ (◡𝐴 “ ℕ) | 
| 127 | 126, 76 | sselid 3981 | . . . . . . . . . . 11
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)) → 𝑡 ∈ (◡𝐴 “ ℕ)) | 
| 128 | 125, 127 | sseldd 3984 | . . . . . . . . . 10
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)) → 𝑡 ∈ ℕ) | 
| 129 | 122, 128 | ffvelcdmd 7105 | . . . . . . . . 9
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)) → (𝐴‘𝑡) ∈
ℕ0) | 
| 130 |  | bitsfi 16474 | . . . . . . . . 9
⊢ ((𝐴‘𝑡) ∈ ℕ0 →
(bits‘(𝐴‘𝑡)) ∈ Fin) | 
| 131 | 129, 130 | syl 17 | . . . . . . . 8
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)) → (bits‘(𝐴‘𝑡)) ∈ Fin) | 
| 132 | 128 | nncnd 12282 | . . . . . . . 8
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)) → 𝑡 ∈ ℂ) | 
| 133 |  | 2cnd 12344 | . . . . . . . . . 10
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ (𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽) ∧ 𝑛 ∈ (bits‘(𝐴‘𝑡)))) → 2 ∈
ℂ) | 
| 134 |  | simprr 773 | . . . . . . . . . . 11
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ (𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽) ∧ 𝑛 ∈ (bits‘(𝐴‘𝑡)))) → 𝑛 ∈ (bits‘(𝐴‘𝑡))) | 
| 135 | 79, 134 | sselid 3981 | . . . . . . . . . 10
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ (𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽) ∧ 𝑛 ∈ (bits‘(𝐴‘𝑡)))) → 𝑛 ∈ ℕ0) | 
| 136 | 133, 135 | expcld 14186 | . . . . . . . . 9
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ (𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽) ∧ 𝑛 ∈ (bits‘(𝐴‘𝑡)))) → (2↑𝑛) ∈ ℂ) | 
| 137 | 136 | anassrs 467 | . . . . . . . 8
⊢ (((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)) ∧ 𝑛 ∈ (bits‘(𝐴‘𝑡))) → (2↑𝑛) ∈ ℂ) | 
| 138 | 131, 132,
137 | fsummulc1 15821 | . . . . . . 7
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)) → (Σ𝑛 ∈ (bits‘(𝐴‘𝑡))(2↑𝑛) · 𝑡) = Σ𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡)) | 
| 139 | 138 | sumeq2dv 15738 | . . . . . 6
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → Σ𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)(Σ𝑛 ∈ (bits‘(𝐴‘𝑡))(2↑𝑛) · 𝑡) = Σ𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)Σ𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡)) | 
| 140 |  | bitsinv1 16479 | . . . . . . . . 9
⊢ ((𝐴‘𝑡) ∈ ℕ0 →
Σ𝑛 ∈
(bits‘(𝐴‘𝑡))(2↑𝑛) = (𝐴‘𝑡)) | 
| 141 | 140 | oveq1d 7446 | . . . . . . . 8
⊢ ((𝐴‘𝑡) ∈ ℕ0 →
(Σ𝑛 ∈
(bits‘(𝐴‘𝑡))(2↑𝑛) · 𝑡) = ((𝐴‘𝑡) · 𝑡)) | 
| 142 | 129, 141 | syl 17 | . . . . . . 7
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)) → (Σ𝑛 ∈ (bits‘(𝐴‘𝑡))(2↑𝑛) · 𝑡) = ((𝐴‘𝑡) · 𝑡)) | 
| 143 | 142 | sumeq2dv 15738 | . . . . . 6
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → Σ𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)(Σ𝑛 ∈ (bits‘(𝐴‘𝑡))(2↑𝑛) · 𝑡) = Σ𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)((𝐴‘𝑡) · 𝑡)) | 
| 144 |  | vex 3484 | . . . . . . . . . 10
⊢ 𝑡 ∈ V | 
| 145 |  | vex 3484 | . . . . . . . . . 10
⊢ 𝑛 ∈ V | 
| 146 | 144, 145 | op2ndd 8025 | . . . . . . . . 9
⊢ (𝑤 = 〈𝑡, 𝑛〉 → (2nd ‘𝑤) = 𝑛) | 
| 147 | 146 | oveq2d 7447 | . . . . . . . 8
⊢ (𝑤 = 〈𝑡, 𝑛〉 → (2↑(2nd
‘𝑤)) = (2↑𝑛)) | 
| 148 | 144, 145 | op1std 8024 | . . . . . . . 8
⊢ (𝑤 = 〈𝑡, 𝑛〉 → (1st ‘𝑤) = 𝑡) | 
| 149 | 147, 148 | oveq12d 7449 | . . . . . . 7
⊢ (𝑤 = 〈𝑡, 𝑛〉 → ((2↑(2nd
‘𝑤)) ·
(1st ‘𝑤))
= ((2↑𝑛) ·
𝑡)) | 
| 150 |  | inss2 4238 | . . . . . . . . . 10
⊢ (𝑇 ∩ 𝑅) ⊆ 𝑅 | 
| 151 | 150 | sseli 3979 | . . . . . . . . 9
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → 𝐴 ∈ 𝑅) | 
| 152 |  | cnveq 5884 | . . . . . . . . . . . 12
⊢ (𝑓 = 𝐴 → ◡𝑓 = ◡𝐴) | 
| 153 | 152 | imaeq1d 6077 | . . . . . . . . . . 11
⊢ (𝑓 = 𝐴 → (◡𝑓 “ ℕ) = (◡𝐴 “ ℕ)) | 
| 154 | 153 | eleq1d 2826 | . . . . . . . . . 10
⊢ (𝑓 = 𝐴 → ((◡𝑓 “ ℕ) ∈ Fin ↔ (◡𝐴 “ ℕ) ∈
Fin)) | 
| 155 | 154, 9 | elab2g 3680 | . . . . . . . . 9
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → (𝐴 ∈ 𝑅 ↔ (◡𝐴 “ ℕ) ∈
Fin)) | 
| 156 | 151, 155 | mpbid 232 | . . . . . . . 8
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → (◡𝐴 “ ℕ) ∈
Fin) | 
| 157 |  | ssfi 9213 | . . . . . . . 8
⊢ (((◡𝐴 “ ℕ) ∈ Fin ∧ ((◡𝐴 “ ℕ) ∩ 𝐽) ⊆ (◡𝐴 “ ℕ)) → ((◡𝐴 “ ℕ) ∩ 𝐽) ∈ Fin) | 
| 158 | 156, 126,
157 | sylancl 586 | . . . . . . 7
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → ((◡𝐴 “ ℕ) ∩ 𝐽) ∈ Fin) | 
| 159 | 132 | adantrr 717 | . . . . . . . 8
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ (𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽) ∧ 𝑛 ∈ (bits‘(𝐴‘𝑡)))) → 𝑡 ∈ ℂ) | 
| 160 | 136, 159 | mulcld 11281 | . . . . . . 7
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ (𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽) ∧ 𝑛 ∈ (bits‘(𝐴‘𝑡)))) → ((2↑𝑛) · 𝑡) ∈ ℂ) | 
| 161 | 149, 158,
131, 160 | fsum2d 15807 | . . . . . 6
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → Σ𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)Σ𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = Σ𝑤 ∈ ∪
𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡)))((2↑(2nd ‘𝑤)) · (1st
‘𝑤))) | 
| 162 | 139, 143,
161 | 3eqtr3d 2785 | . . . . 5
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → Σ𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)((𝐴‘𝑡) · 𝑡) = Σ𝑤 ∈ ∪
𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡)))((2↑(2nd ‘𝑤)) · (1st
‘𝑤))) | 
| 163 |  | inss1 4237 | . . . . . . . . 9
⊢ (𝑇 ∩ 𝑅) ⊆ 𝑇 | 
| 164 | 163 | sseli 3979 | . . . . . . . 8
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → 𝐴 ∈ 𝑇) | 
| 165 | 153 | sseq1d 4015 | . . . . . . . . . 10
⊢ (𝑓 = 𝐴 → ((◡𝑓 “ ℕ) ⊆ 𝐽 ↔ (◡𝐴 “ ℕ) ⊆ 𝐽)) | 
| 166 | 165, 10 | elrab2 3695 | . . . . . . . . 9
⊢ (𝐴 ∈ 𝑇 ↔ (𝐴 ∈ (ℕ0
↑m ℕ) ∧ (◡𝐴 “ ℕ) ⊆ 𝐽)) | 
| 167 | 166 | simprbi 496 | . . . . . . . 8
⊢ (𝐴 ∈ 𝑇 → (◡𝐴 “ ℕ) ⊆ 𝐽) | 
| 168 | 164, 167 | syl 17 | . . . . . . 7
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → (◡𝐴 “ ℕ) ⊆ 𝐽) | 
| 169 |  | dfss2 3969 | . . . . . . 7
⊢ ((◡𝐴 “ ℕ) ⊆ 𝐽 ↔ ((◡𝐴 “ ℕ) ∩ 𝐽) = (◡𝐴 “ ℕ)) | 
| 170 | 168, 169 | sylib 218 | . . . . . 6
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → ((◡𝐴 “ ℕ) ∩ 𝐽) = (◡𝐴 “ ℕ)) | 
| 171 | 170 | sumeq1d 15736 | . . . . 5
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → Σ𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)((𝐴‘𝑡) · 𝑡) = Σ𝑡 ∈ (◡𝐴 “ ℕ)((𝐴‘𝑡) · 𝑡)) | 
| 172 | 162, 171 | eqtr3d 2779 | . . . 4
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → Σ𝑤 ∈ ∪
𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡)))((2↑(2nd ‘𝑤)) · (1st
‘𝑤)) = Σ𝑡 ∈ (◡𝐴 “ ℕ)((𝐴‘𝑡) · 𝑡)) | 
| 173 | 27, 117, 172 | 3eqtr2d 2783 | . . 3
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → Σ𝑘 ∈ (◡(𝐺‘𝐴) “ ℕ)(((𝐺‘𝐴)‘𝑘) · 𝑘) = Σ𝑡 ∈ (◡𝐴 “ ℕ)((𝐴‘𝑡) · 𝑡)) | 
| 174 |  | fveq2 6906 | . . . . 5
⊢ (𝑘 = 𝑡 → (𝐴‘𝑘) = (𝐴‘𝑡)) | 
| 175 |  | id 22 | . . . . 5
⊢ (𝑘 = 𝑡 → 𝑘 = 𝑡) | 
| 176 | 174, 175 | oveq12d 7449 | . . . 4
⊢ (𝑘 = 𝑡 → ((𝐴‘𝑘) · 𝑘) = ((𝐴‘𝑡) · 𝑡)) | 
| 177 | 176 | cbvsumv 15732 | . . 3
⊢
Σ𝑘 ∈
(◡𝐴 “ ℕ)((𝐴‘𝑘) · 𝑘) = Σ𝑡 ∈ (◡𝐴 “ ℕ)((𝐴‘𝑡) · 𝑡) | 
| 178 | 173, 177 | eqtr4di 2795 | . 2
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → Σ𝑘 ∈ (◡(𝐺‘𝐴) “ ℕ)(((𝐺‘𝐴)‘𝑘) · 𝑘) = Σ𝑘 ∈ (◡𝐴 “ ℕ)((𝐴‘𝑘) · 𝑘)) | 
| 179 |  | 0nn0 12541 | . . . . . . . 8
⊢ 0 ∈
ℕ0 | 
| 180 |  | 1nn0 12542 | . . . . . . . 8
⊢ 1 ∈
ℕ0 | 
| 181 |  | prssi 4821 | . . . . . . . 8
⊢ ((0
∈ ℕ0 ∧ 1 ∈ ℕ0) → {0, 1}
⊆ ℕ0) | 
| 182 | 179, 180,
181 | mp2an 692 | . . . . . . 7
⊢ {0, 1}
⊆ ℕ0 | 
| 183 |  | fss 6752 | . . . . . . 7
⊢ (((𝐺‘𝐴):ℕ⟶{0, 1} ∧ {0, 1} ⊆
ℕ0) → (𝐺‘𝐴):ℕ⟶ℕ0) | 
| 184 | 182, 183 | mpan2 691 | . . . . . 6
⊢ ((𝐺‘𝐴):ℕ⟶{0, 1} → (𝐺‘𝐴):ℕ⟶ℕ0) | 
| 185 |  | nn0ex 12532 | . . . . . . . 8
⊢
ℕ0 ∈ V | 
| 186 |  | nnex 12272 | . . . . . . . 8
⊢ ℕ
∈ V | 
| 187 | 185, 186 | elmap 8911 | . . . . . . 7
⊢ ((𝐺‘𝐴) ∈ (ℕ0
↑m ℕ) ↔ (𝐺‘𝐴):ℕ⟶ℕ0) | 
| 188 | 187 | biimpri 228 | . . . . . 6
⊢ ((𝐺‘𝐴):ℕ⟶ℕ0 →
(𝐺‘𝐴) ∈ (ℕ0
↑m ℕ)) | 
| 189 | 19, 184, 188 | 3syl 18 | . . . . 5
⊢ ((𝐺‘𝐴) ∈ ({0, 1} ↑m ℕ)
→ (𝐺‘𝐴) ∈ (ℕ0
↑m ℕ)) | 
| 190 | 189 | anim1i 615 | . . . 4
⊢ (((𝐺‘𝐴) ∈ ({0, 1} ↑m ℕ)
∧ (𝐺‘𝐴) ∈ 𝑅) → ((𝐺‘𝐴) ∈ (ℕ0
↑m ℕ) ∧ (𝐺‘𝐴) ∈ 𝑅)) | 
| 191 |  | elin 3967 | . . . 4
⊢ ((𝐺‘𝐴) ∈ ((ℕ0
↑m ℕ) ∩ 𝑅) ↔ ((𝐺‘𝐴) ∈ (ℕ0
↑m ℕ) ∧ (𝐺‘𝐴) ∈ 𝑅)) | 
| 192 | 190, 16, 191 | 3imtr4i 292 | . . 3
⊢ ((𝐺‘𝐴) ∈ (({0, 1} ↑m
ℕ) ∩ 𝑅) →
(𝐺‘𝐴) ∈ ((ℕ0
↑m ℕ) ∩ 𝑅)) | 
| 193 |  | eulerpart.s | . . . 4
⊢ 𝑆 = (𝑓 ∈ ((ℕ0
↑m ℕ) ∩ 𝑅) ↦ Σ𝑘 ∈ ℕ ((𝑓‘𝑘) · 𝑘)) | 
| 194 | 9, 193 | eulerpartlemsv2 34360 | . . 3
⊢ ((𝐺‘𝐴) ∈ ((ℕ0
↑m ℕ) ∩ 𝑅) → (𝑆‘(𝐺‘𝐴)) = Σ𝑘 ∈ (◡(𝐺‘𝐴) “ ℕ)(((𝐺‘𝐴)‘𝑘) · 𝑘)) | 
| 195 | 15, 192, 194 | 3syl 18 | . 2
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → (𝑆‘(𝐺‘𝐴)) = Σ𝑘 ∈ (◡(𝐺‘𝐴) “ ℕ)(((𝐺‘𝐴)‘𝑘) · 𝑘)) | 
| 196 | 119, 151 | elind 4200 | . . 3
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → 𝐴 ∈ ((ℕ0
↑m ℕ) ∩ 𝑅)) | 
| 197 | 9, 193 | eulerpartlemsv2 34360 | . . 3
⊢ (𝐴 ∈ ((ℕ0
↑m ℕ) ∩ 𝑅) → (𝑆‘𝐴) = Σ𝑘 ∈ (◡𝐴 “ ℕ)((𝐴‘𝑘) · 𝑘)) | 
| 198 | 196, 197 | syl 17 | . 2
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → (𝑆‘𝐴) = Σ𝑘 ∈ (◡𝐴 “ ℕ)((𝐴‘𝑘) · 𝑘)) | 
| 199 | 178, 195,
198 | 3eqtr4d 2787 | 1
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → (𝑆‘(𝐺‘𝐴)) = (𝑆‘𝐴)) |