Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  eulerpartlemgs2 Structured version   Visualization version   GIF version

Theorem eulerpartlemgs2 34133
Description: Lemma for eulerpart 34135: The 𝐺 function also preserves partition sums. (Contributed by Thierry Arnoux, 10-Sep-2017.)
Hypotheses
Ref Expression
eulerpart.p 𝑃 = {𝑓 ∈ (ℕ0m ℕ) ∣ ((𝑓 “ ℕ) ∈ Fin ∧ Σ𝑘 ∈ ℕ ((𝑓𝑘) · 𝑘) = 𝑁)}
eulerpart.o 𝑂 = {𝑔𝑃 ∣ ∀𝑛 ∈ (𝑔 “ ℕ) ¬ 2 ∥ 𝑛}
eulerpart.d 𝐷 = {𝑔𝑃 ∣ ∀𝑛 ∈ ℕ (𝑔𝑛) ≤ 1}
eulerpart.j 𝐽 = {𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧}
eulerpart.f 𝐹 = (𝑥𝐽, 𝑦 ∈ ℕ0 ↦ ((2↑𝑦) · 𝑥))
eulerpart.h 𝐻 = {𝑟 ∈ ((𝒫 ℕ0 ∩ Fin) ↑m 𝐽) ∣ (𝑟 supp ∅) ∈ Fin}
eulerpart.m 𝑀 = (𝑟𝐻 ↦ {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐽𝑦 ∈ (𝑟𝑥))})
eulerpart.r 𝑅 = {𝑓 ∣ (𝑓 “ ℕ) ∈ Fin}
eulerpart.t 𝑇 = {𝑓 ∈ (ℕ0m ℕ) ∣ (𝑓 “ ℕ) ⊆ 𝐽}
eulerpart.g 𝐺 = (𝑜 ∈ (𝑇𝑅) ↦ ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽))))))
eulerpart.s 𝑆 = (𝑓 ∈ ((ℕ0m ℕ) ∩ 𝑅) ↦ Σ𝑘 ∈ ℕ ((𝑓𝑘) · 𝑘))
Assertion
Ref Expression
eulerpartlemgs2 (𝐴 ∈ (𝑇𝑅) → (𝑆‘(𝐺𝐴)) = (𝑆𝐴))
Distinct variable groups:   𝑓,𝑔,𝑘,𝑛,𝑜,𝑥,𝑦,𝑧   𝑓,𝑟,𝐴,𝑔,𝑘,𝑛,𝑜,𝑥,𝑦   𝑓,𝐺,𝑘   𝑛,𝐹,𝑜,𝑥,𝑦   𝑜,𝐻,𝑟   𝑓,𝐽,𝑛,𝑜,𝑟,𝑥,𝑦   𝑛,𝑀,𝑜,𝑟,𝑥,𝑦   𝑓,𝑁,𝑔,𝑘,𝑛,𝑥   𝑛,𝑂,𝑟,𝑥,𝑦   𝑃,𝑔,𝑘,𝑛   𝑅,𝑓,𝑘,𝑛,𝑜,𝑟,𝑥,𝑦   𝑇,𝑓,𝑘,𝑛,𝑜,𝑟,𝑥,𝑦
Allowed substitution hints:   𝐴(𝑧)   𝐷(𝑥,𝑦,𝑧,𝑓,𝑔,𝑘,𝑛,𝑜,𝑟)   𝑃(𝑥,𝑦,𝑧,𝑓,𝑜,𝑟)   𝑅(𝑧,𝑔)   𝑆(𝑥,𝑦,𝑧,𝑓,𝑔,𝑘,𝑛,𝑜,𝑟)   𝑇(𝑧,𝑔)   𝐹(𝑧,𝑓,𝑔,𝑘,𝑟)   𝐺(𝑥,𝑦,𝑧,𝑔,𝑛,𝑜,𝑟)   𝐻(𝑥,𝑦,𝑧,𝑓,𝑔,𝑘,𝑛)   𝐽(𝑧,𝑔,𝑘)   𝑀(𝑧,𝑓,𝑔,𝑘)   𝑁(𝑦,𝑧,𝑜,𝑟)   𝑂(𝑧,𝑓,𝑔,𝑘,𝑜)

Proof of Theorem eulerpartlemgs2
Dummy variables 𝑡 𝑚 𝑤 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 cnvimass 6086 . . . . . . . 8 ((𝐺𝐴) “ ℕ) ⊆ dom (𝐺𝐴)
2 eulerpart.p . . . . . . . . . . . . . 14 𝑃 = {𝑓 ∈ (ℕ0m ℕ) ∣ ((𝑓 “ ℕ) ∈ 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 𝑇 = {𝑓 ∈ (ℕ0m ℕ) ∣ (𝑓 “ ℕ) ⊆ 𝐽}
11 eulerpart.g . . . . . . . . . . . . . 14 𝐺 = (𝑜 ∈ (𝑇𝑅) ↦ ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽))))))
122, 3, 4, 5, 6, 7, 8, 9, 10, 11eulerpartgbij 34125 . . . . . . . . . . . . 13 𝐺:(𝑇𝑅)–1-1-onto→(({0, 1} ↑m ℕ) ∩ 𝑅)
13 f1of 6838 . . . . . . . . . . . . 13 (𝐺:(𝑇𝑅)–1-1-onto→(({0, 1} ↑m ℕ) ∩ 𝑅) → 𝐺:(𝑇𝑅)⟶(({0, 1} ↑m ℕ) ∩ 𝑅))
1412, 13ax-mp 5 . . . . . . . . . . . 12 𝐺:(𝑇𝑅)⟶(({0, 1} ↑m ℕ) ∩ 𝑅)
1514ffvelcdmi 7092 . . . . . . . . . . 11 (𝐴 ∈ (𝑇𝑅) → (𝐺𝐴) ∈ (({0, 1} ↑m ℕ) ∩ 𝑅))
16 elin 3960 . . . . . . . . . . 11 ((𝐺𝐴) ∈ (({0, 1} ↑m ℕ) ∩ 𝑅) ↔ ((𝐺𝐴) ∈ ({0, 1} ↑m ℕ) ∧ (𝐺𝐴) ∈ 𝑅))
1715, 16sylib 217 . . . . . . . . . 10 (𝐴 ∈ (𝑇𝑅) → ((𝐺𝐴) ∈ ({0, 1} ↑m ℕ) ∧ (𝐺𝐴) ∈ 𝑅))
1817simpld 493 . . . . . . . . 9 (𝐴 ∈ (𝑇𝑅) → (𝐺𝐴) ∈ ({0, 1} ↑m ℕ))
19 elmapi 8868 . . . . . . . . 9 ((𝐺𝐴) ∈ ({0, 1} ↑m ℕ) → (𝐺𝐴):ℕ⟶{0, 1})
20 fdm 6732 . . . . . . . . 9 ((𝐺𝐴):ℕ⟶{0, 1} → dom (𝐺𝐴) = ℕ)
2118, 19, 203syl 18 . . . . . . . 8 (𝐴 ∈ (𝑇𝑅) → dom (𝐺𝐴) = ℕ)
221, 21sseqtrid 4029 . . . . . . 7 (𝐴 ∈ (𝑇𝑅) → ((𝐺𝐴) “ ℕ) ⊆ ℕ)
2322sselda 3976 . . . . . 6 ((𝐴 ∈ (𝑇𝑅) ∧ 𝑘 ∈ ((𝐺𝐴) “ ℕ)) → 𝑘 ∈ ℕ)
242, 3, 4, 5, 6, 7, 8, 9, 10, 11eulerpartlemgvv 34129 . . . . . . 7 ((𝐴 ∈ (𝑇𝑅) ∧ 𝑘 ∈ ℕ) → ((𝐺𝐴)‘𝑘) = if(∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴𝑡))((2↑𝑛) · 𝑡) = 𝑘, 1, 0))
2524oveq1d 7434 . . . . . 6 ((𝐴 ∈ (𝑇𝑅) ∧ 𝑘 ∈ ℕ) → (((𝐺𝐴)‘𝑘) · 𝑘) = (if(∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴𝑡))((2↑𝑛) · 𝑡) = 𝑘, 1, 0) · 𝑘))
2623, 25syldan 589 . . . . 5 ((𝐴 ∈ (𝑇𝑅) ∧ 𝑘 ∈ ((𝐺𝐴) “ ℕ)) → (((𝐺𝐴)‘𝑘) · 𝑘) = (if(∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴𝑡))((2↑𝑛) · 𝑡) = 𝑘, 1, 0) · 𝑘))
2726sumeq2dv 15690 . . . 4 (𝐴 ∈ (𝑇𝑅) → Σ𝑘 ∈ ((𝐺𝐴) “ ℕ)(((𝐺𝐴)‘𝑘) · 𝑘) = Σ𝑘 ∈ ((𝐺𝐴) “ ℕ)(if(∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴𝑡))((2↑𝑛) · 𝑡) = 𝑘, 1, 0) · 𝑘))
28 eqeq2 2737 . . . . . . . . . . . . 13 (𝑚 = 𝑘 → (((2↑𝑛) · 𝑡) = 𝑚 ↔ ((2↑𝑛) · 𝑡) = 𝑘))
29282rexbidv 3209 . . . . . . . . . . . 12 (𝑚 = 𝑘 → (∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴𝑡))((2↑𝑛) · 𝑡) = 𝑚 ↔ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴𝑡))((2↑𝑛) · 𝑡) = 𝑘))
3029elrab 3679 . . . . . . . . . . 11 (𝑘 ∈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴𝑡))((2↑𝑛) · 𝑡) = 𝑚} ↔ (𝑘 ∈ ℕ ∧ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴𝑡))((2↑𝑛) · 𝑡) = 𝑘))
3130simprbi 495 . . . . . . . . . 10 (𝑘 ∈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴𝑡))((2↑𝑛) · 𝑡) = 𝑚} → ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴𝑡))((2↑𝑛) · 𝑡) = 𝑘)
3231iftrued 4538 . . . . . . . . 9 (𝑘 ∈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴𝑡))((2↑𝑛) · 𝑡) = 𝑚} → if(∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴𝑡))((2↑𝑛) · 𝑡) = 𝑘, 1, 0) = 1)
3332oveq1d 7434 . . . . . . . 8 (𝑘 ∈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴𝑡))((2↑𝑛) · 𝑡) = 𝑚} → (if(∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴𝑡))((2↑𝑛) · 𝑡) = 𝑘, 1, 0) · 𝑘) = (1 · 𝑘))
34 elrabi 3673 . . . . . . . . . 10 (𝑘 ∈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴𝑡))((2↑𝑛) · 𝑡) = 𝑚} → 𝑘 ∈ ℕ)
3534nncnd 12266 . . . . . . . . 9 (𝑘 ∈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴𝑡))((2↑𝑛) · 𝑡) = 𝑚} → 𝑘 ∈ ℂ)
3635mullidd 11269 . . . . . . . 8 (𝑘 ∈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴𝑡))((2↑𝑛) · 𝑡) = 𝑚} → (1 · 𝑘) = 𝑘)
3733, 36eqtrd 2765 . . . . . . 7 (𝑘 ∈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴𝑡))((2↑𝑛) · 𝑡) = 𝑚} → (if(∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴𝑡))((2↑𝑛) · 𝑡) = 𝑘, 1, 0) · 𝑘) = 𝑘)
3837sumeq2i 15686 . . . . . 6 Σ𝑘 ∈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴𝑡))((2↑𝑛) · 𝑡) = 𝑚} (if(∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴𝑡))((2↑𝑛) · 𝑡) = 𝑘, 1, 0) · 𝑘) = Σ𝑘 ∈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴𝑡))((2↑𝑛) · 𝑡) = 𝑚}𝑘
39 id 22 . . . . . . 7 (𝑘 = ((2↑(2nd𝑤)) · (1st𝑤)) → 𝑘 = ((2↑(2nd𝑤)) · (1st𝑤)))
402, 3, 4, 5, 6, 7, 8, 9, 10, 11eulerpartlemgf 34132 . . . . . . . . 9 (𝐴 ∈ (𝑇𝑅) → ((𝐺𝐴) “ ℕ) ∈ Fin)
4134adantl 480 . . . . . . . . . . . 12 ((𝐴 ∈ (𝑇𝑅) ∧ 𝑘 ∈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴𝑡))((2↑𝑛) · 𝑡) = 𝑚}) → 𝑘 ∈ ℕ)
4241, 24syldan 589 . . . . . . . . . . . . . 14 ((𝐴 ∈ (𝑇𝑅) ∧ 𝑘 ∈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴𝑡))((2↑𝑛) · 𝑡) = 𝑚}) → ((𝐺𝐴)‘𝑘) = if(∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴𝑡))((2↑𝑛) · 𝑡) = 𝑘, 1, 0))
4331adantl 480 . . . . . . . . . . . . . . 15 ((𝐴 ∈ (𝑇𝑅) ∧ 𝑘 ∈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴𝑡))((2↑𝑛) · 𝑡) = 𝑚}) → ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴𝑡))((2↑𝑛) · 𝑡) = 𝑘)
4443iftrued 4538 . . . . . . . . . . . . . 14 ((𝐴 ∈ (𝑇𝑅) ∧ 𝑘 ∈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴𝑡))((2↑𝑛) · 𝑡) = 𝑚}) → if(∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴𝑡))((2↑𝑛) · 𝑡) = 𝑘, 1, 0) = 1)
4542, 44eqtrd 2765 . . . . . . . . . . . . 13 ((𝐴 ∈ (𝑇𝑅) ∧ 𝑘 ∈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴𝑡))((2↑𝑛) · 𝑡) = 𝑚}) → ((𝐺𝐴)‘𝑘) = 1)
46 1nn 12261 . . . . . . . . . . . . 13 1 ∈ ℕ
4745, 46eqeltrdi 2833 . . . . . . . . . . . 12 ((𝐴 ∈ (𝑇𝑅) ∧ 𝑘 ∈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴𝑡))((2↑𝑛) · 𝑡) = 𝑚}) → ((𝐺𝐴)‘𝑘) ∈ ℕ)
48 ffn 6723 . . . . . . . . . . . . . 14 ((𝐺𝐴):ℕ⟶{0, 1} → (𝐺𝐴) Fn ℕ)
49 elpreima 7066 . . . . . . . . . . . . . 14 ((𝐺𝐴) Fn ℕ → (𝑘 ∈ ((𝐺𝐴) “ ℕ) ↔ (𝑘 ∈ ℕ ∧ ((𝐺𝐴)‘𝑘) ∈ ℕ)))
5018, 19, 48, 494syl 19 . . . . . . . . . . . . 13 (𝐴 ∈ (𝑇𝑅) → (𝑘 ∈ ((𝐺𝐴) “ ℕ) ↔ (𝑘 ∈ ℕ ∧ ((𝐺𝐴)‘𝑘) ∈ ℕ)))
5150adantr 479 . . . . . . . . . . . 12 ((𝐴 ∈ (𝑇𝑅) ∧ 𝑘 ∈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴𝑡))((2↑𝑛) · 𝑡) = 𝑚}) → (𝑘 ∈ ((𝐺𝐴) “ ℕ) ↔ (𝑘 ∈ ℕ ∧ ((𝐺𝐴)‘𝑘) ∈ ℕ)))
5241, 47, 51mpbir2and 711 . . . . . . . . . . 11 ((𝐴 ∈ (𝑇𝑅) ∧ 𝑘 ∈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴𝑡))((2↑𝑛) · 𝑡) = 𝑚}) → 𝑘 ∈ ((𝐺𝐴) “ ℕ))
5352ex 411 . . . . . . . . . 10 (𝐴 ∈ (𝑇𝑅) → (𝑘 ∈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴𝑡))((2↑𝑛) · 𝑡) = 𝑚} → 𝑘 ∈ ((𝐺𝐴) “ ℕ)))
5453ssrdv 3982 . . . . . . . . 9 (𝐴 ∈ (𝑇𝑅) → {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴𝑡))((2↑𝑛) · 𝑡) = 𝑚} ⊆ ((𝐺𝐴) “ ℕ))
55 ssfi 9201 . . . . . . . . 9 ((((𝐺𝐴) “ ℕ) ∈ Fin ∧ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴𝑡))((2↑𝑛) · 𝑡) = 𝑚} ⊆ ((𝐺𝐴) “ ℕ)) → {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴𝑡))((2↑𝑛) · 𝑡) = 𝑚} ∈ Fin)
5640, 54, 55syl2anc 582 . . . . . . . 8 (𝐴 ∈ (𝑇𝑅) → {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴𝑡))((2↑𝑛) · 𝑡) = 𝑚} ∈ Fin)
57 cnvexg 7932 . . . . . . . . . . 11 (𝐴 ∈ (𝑇𝑅) → 𝐴 ∈ V)
58 imaexg 7921 . . . . . . . . . . 11 (𝐴 ∈ V → (𝐴 “ ℕ) ∈ V)
59 inex1g 5320 . . . . . . . . . . 11 ((𝐴 “ ℕ) ∈ V → ((𝐴 “ ℕ) ∩ 𝐽) ∈ V)
6057, 58, 593syl 18 . . . . . . . . . 10 (𝐴 ∈ (𝑇𝑅) → ((𝐴 “ ℕ) ∩ 𝐽) ∈ V)
61 vsnex 5431 . . . . . . . . . . . 12 {𝑡} ∈ V
62 fvex 6909 . . . . . . . . . . . 12 (bits‘(𝐴𝑡)) ∈ V
6361, 62xpex 7756 . . . . . . . . . . 11 ({𝑡} × (bits‘(𝐴𝑡))) ∈ V
6463rgenw 3054 . . . . . . . . . 10 𝑡 ∈ ((𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴𝑡))) ∈ V
65 iunexg 7968 . . . . . . . . . 10 ((((𝐴 “ ℕ) ∩ 𝐽) ∈ V ∧ ∀𝑡 ∈ ((𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴𝑡))) ∈ V) → 𝑡 ∈ ((𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴𝑡))) ∈ V)
6660, 64, 65sylancl 584 . . . . . . . . 9 (𝐴 ∈ (𝑇𝑅) → 𝑡 ∈ ((𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴𝑡))) ∈ V)
67 eqid 2725 . . . . . . . . . 10 𝑡 ∈ ((𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴𝑡))) = 𝑡 ∈ ((𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴𝑡)))
682, 3, 4, 5, 6, 7, 8, 9, 10, 11, 67eulerpartlemgh 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↑𝑛) · 𝑡) = 𝑚})
7066, 68, 69syl2anc 582 . . . . . . . 8 (𝐴 ∈ (𝑇𝑅) → 𝑡 ∈ ((𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴𝑡))) ≈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴𝑡))((2↑𝑛) · 𝑡) = 𝑚})
71 enfii 9217 . . . . . . . 8 (({𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴𝑡))((2↑𝑛) · 𝑡) = 𝑚} ∈ Fin ∧ 𝑡 ∈ ((𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴𝑡))) ≈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴𝑡))((2↑𝑛) · 𝑡) = 𝑚}) → 𝑡 ∈ ((𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴𝑡))) ∈ Fin)
7256, 70, 71syl2anc 582 . . . . . . 7 (𝐴 ∈ (𝑇𝑅) → 𝑡 ∈ ((𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴𝑡))) ∈ Fin)
73 fvres 6915 . . . . . . . . 9 (𝑤 𝑡 ∈ ((𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴𝑡))) → ((𝐹 𝑡 ∈ ((𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴𝑡))))‘𝑤) = (𝐹𝑤))
7473adantl 480 . . . . . . . 8 ((𝐴 ∈ (𝑇𝑅) ∧ 𝑤 𝑡 ∈ ((𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴𝑡)))) → ((𝐹 𝑡 ∈ ((𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴𝑡))))‘𝑤) = (𝐹𝑤))
75 inss2 4228 . . . . . . . . . . . . . . 15 ((𝐴 “ ℕ) ∩ 𝐽) ⊆ 𝐽
76 simpr 483 . . . . . . . . . . . . . . 15 ((𝐴 ∈ (𝑇𝑅) ∧ 𝑡 ∈ ((𝐴 “ ℕ) ∩ 𝐽)) → 𝑡 ∈ ((𝐴 “ ℕ) ∩ 𝐽))
7775, 76sselid 3974 . . . . . . . . . . . . . 14 ((𝐴 ∈ (𝑇𝑅) ∧ 𝑡 ∈ ((𝐴 “ ℕ) ∩ 𝐽)) → 𝑡𝐽)
7877snssd 4814 . . . . . . . . . . . . 13 ((𝐴 ∈ (𝑇𝑅) ∧ 𝑡 ∈ ((𝐴 “ ℕ) ∩ 𝐽)) → {𝑡} ⊆ 𝐽)
79 bitsss 16409 . . . . . . . . . . . . 13 (bits‘(𝐴𝑡)) ⊆ ℕ0
80 xpss12 5693 . . . . . . . . . . . . 13 (({𝑡} ⊆ 𝐽 ∧ (bits‘(𝐴𝑡)) ⊆ ℕ0) → ({𝑡} × (bits‘(𝐴𝑡))) ⊆ (𝐽 × ℕ0))
8178, 79, 80sylancl 584 . . . . . . . . . . . 12 ((𝐴 ∈ (𝑇𝑅) ∧ 𝑡 ∈ ((𝐴 “ ℕ) ∩ 𝐽)) → ({𝑡} × (bits‘(𝐴𝑡))) ⊆ (𝐽 × ℕ0))
8281ralrimiva 3135 . . . . . . . . . . 11 (𝐴 ∈ (𝑇𝑅) → ∀𝑡 ∈ ((𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴𝑡))) ⊆ (𝐽 × ℕ0))
83 iunss 5049 . . . . . . . . . . 11 ( 𝑡 ∈ ((𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴𝑡))) ⊆ (𝐽 × ℕ0) ↔ ∀𝑡 ∈ ((𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴𝑡))) ⊆ (𝐽 × ℕ0))
8482, 83sylibr 233 . . . . . . . . . 10 (𝐴 ∈ (𝑇𝑅) → 𝑡 ∈ ((𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴𝑡))) ⊆ (𝐽 × ℕ0))
8584sselda 3976 . . . . . . . . 9 ((𝐴 ∈ (𝑇𝑅) ∧ 𝑤 𝑡 ∈ ((𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴𝑡)))) → 𝑤 ∈ (𝐽 × ℕ0))
865, 6oddpwdcv 34108 . . . . . . . . 9 (𝑤 ∈ (𝐽 × ℕ0) → (𝐹𝑤) = ((2↑(2nd𝑤)) · (1st𝑤)))
8785, 86syl 17 . . . . . . . 8 ((𝐴 ∈ (𝑇𝑅) ∧ 𝑤 𝑡 ∈ ((𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴𝑡)))) → (𝐹𝑤) = ((2↑(2nd𝑤)) · (1st𝑤)))
8874, 87eqtrd 2765 . . . . . . 7 ((𝐴 ∈ (𝑇𝑅) ∧ 𝑤 𝑡 ∈ ((𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴𝑡)))) → ((𝐹 𝑡 ∈ ((𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴𝑡))))‘𝑤) = ((2↑(2nd𝑤)) · (1st𝑤)))
8941nncnd 12266 . . . . . . 7 ((𝐴 ∈ (𝑇𝑅) ∧ 𝑘 ∈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴𝑡))((2↑𝑛) · 𝑡) = 𝑚}) → 𝑘 ∈ ℂ)
9039, 72, 68, 88, 89fsumf1o 15710 . . . . . 6 (𝐴 ∈ (𝑇𝑅) → Σ𝑘 ∈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴𝑡))((2↑𝑛) · 𝑡) = 𝑚}𝑘 = Σ𝑤 𝑡 ∈ ((𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴𝑡)))((2↑(2nd𝑤)) · (1st𝑤)))
9138, 90eqtrid 2777 . . . . 5 (𝐴 ∈ (𝑇𝑅) → Σ𝑘 ∈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴𝑡))((2↑𝑛) · 𝑡) = 𝑚} (if(∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴𝑡))((2↑𝑛) · 𝑡) = 𝑘, 1, 0) · 𝑘) = Σ𝑤 𝑡 ∈ ((𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴𝑡)))((2↑(2nd𝑤)) · (1st𝑤)))
92 ax-1cn 11203 . . . . . . . . 9 1 ∈ ℂ
93 0cn 11243 . . . . . . . . 9 0 ∈ ℂ
9492, 93ifcli 4577 . . . . . . . 8 if(∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴𝑡))((2↑𝑛) · 𝑡) = 𝑘, 1, 0) ∈ ℂ
9594a1i 11 . . . . . . 7 ((𝐴 ∈ (𝑇𝑅) ∧ 𝑘 ∈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴𝑡))((2↑𝑛) · 𝑡) = 𝑚}) → if(∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴𝑡))((2↑𝑛) · 𝑡) = 𝑘, 1, 0) ∈ ℂ)
96 ssrab2 4073 . . . . . . . . 9 {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴𝑡))((2↑𝑛) · 𝑡) = 𝑚} ⊆ ℕ
97 simpr 483 . . . . . . . . 9 ((𝐴 ∈ (𝑇𝑅) ∧ 𝑘 ∈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴𝑡))((2↑𝑛) · 𝑡) = 𝑚}) → 𝑘 ∈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴𝑡))((2↑𝑛) · 𝑡) = 𝑚})
9896, 97sselid 3974 . . . . . . . 8 ((𝐴 ∈ (𝑇𝑅) ∧ 𝑘 ∈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴𝑡))((2↑𝑛) · 𝑡) = 𝑚}) → 𝑘 ∈ ℕ)
9998nncnd 12266 . . . . . . 7 ((𝐴 ∈ (𝑇𝑅) ∧ 𝑘 ∈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴𝑡))((2↑𝑛) · 𝑡) = 𝑚}) → 𝑘 ∈ ℂ)
10095, 99mulcld 11271 . . . . . 6 ((𝐴 ∈ (𝑇𝑅) ∧ 𝑘 ∈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴𝑡))((2↑𝑛) · 𝑡) = 𝑚}) → (if(∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴𝑡))((2↑𝑛) · 𝑡) = 𝑘, 1, 0) · 𝑘) ∈ ℂ)
101 simpr 483 . . . . . . . . . . 11 ((𝐴 ∈ (𝑇𝑅) ∧ 𝑘 ∈ (((𝐺𝐴) “ ℕ) ∖ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴𝑡))((2↑𝑛) · 𝑡) = 𝑚})) → 𝑘 ∈ (((𝐺𝐴) “ ℕ) ∖ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴𝑡))((2↑𝑛) · 𝑡) = 𝑚}))
102101eldifbd 3957 . . . . . . . . . 10 ((𝐴 ∈ (𝑇𝑅) ∧ 𝑘 ∈ (((𝐺𝐴) “ ℕ) ∖ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴𝑡))((2↑𝑛) · 𝑡) = 𝑚})) → ¬ 𝑘 ∈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴𝑡))((2↑𝑛) · 𝑡) = 𝑚})
10322ssdifssd 4139 . . . . . . . . . . 11 (𝐴 ∈ (𝑇𝑅) → (((𝐺𝐴) “ ℕ) ∖ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴𝑡))((2↑𝑛) · 𝑡) = 𝑚}) ⊆ ℕ)
104103sselda 3976 . . . . . . . . . 10 ((𝐴 ∈ (𝑇𝑅) ∧ 𝑘 ∈ (((𝐺𝐴) “ ℕ) ∖ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴𝑡))((2↑𝑛) · 𝑡) = 𝑚})) → 𝑘 ∈ ℕ)
10530notbii 319 . . . . . . . . . . 11 𝑘 ∈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴𝑡))((2↑𝑛) · 𝑡) = 𝑚} ↔ ¬ (𝑘 ∈ ℕ ∧ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴𝑡))((2↑𝑛) · 𝑡) = 𝑘))
106 imnan 398 . . . . . . . . . . 11 ((𝑘 ∈ ℕ → ¬ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴𝑡))((2↑𝑛) · 𝑡) = 𝑘) ↔ ¬ (𝑘 ∈ ℕ ∧ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴𝑡))((2↑𝑛) · 𝑡) = 𝑘))
107105, 106sylbb2 237 . . . . . . . . . 10 𝑘 ∈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴𝑡))((2↑𝑛) · 𝑡) = 𝑚} → (𝑘 ∈ ℕ → ¬ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴𝑡))((2↑𝑛) · 𝑡) = 𝑘))
108102, 104, 107sylc 65 . . . . . . . . 9 ((𝐴 ∈ (𝑇𝑅) ∧ 𝑘 ∈ (((𝐺𝐴) “ ℕ) ∖ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴𝑡))((2↑𝑛) · 𝑡) = 𝑚})) → ¬ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴𝑡))((2↑𝑛) · 𝑡) = 𝑘)
109108iffalsed 4541 . . . . . . . 8 ((𝐴 ∈ (𝑇𝑅) ∧ 𝑘 ∈ (((𝐺𝐴) “ ℕ) ∖ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴𝑡))((2↑𝑛) · 𝑡) = 𝑚})) → if(∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴𝑡))((2↑𝑛) · 𝑡) = 𝑘, 1, 0) = 0)
110109oveq1d 7434 . . . . . . 7 ((𝐴 ∈ (𝑇𝑅) ∧ 𝑘 ∈ (((𝐺𝐴) “ ℕ) ∖ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴𝑡))((2↑𝑛) · 𝑡) = 𝑚})) → (if(∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴𝑡))((2↑𝑛) · 𝑡) = 𝑘, 1, 0) · 𝑘) = (0 · 𝑘))
111 nnsscn 12255 . . . . . . . . . 10 ℕ ⊆ ℂ
112103, 111sstrdi 3989 . . . . . . . . 9 (𝐴 ∈ (𝑇𝑅) → (((𝐺𝐴) “ ℕ) ∖ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴𝑡))((2↑𝑛) · 𝑡) = 𝑚}) ⊆ ℂ)
113112sselda 3976 . . . . . . . 8 ((𝐴 ∈ (𝑇𝑅) ∧ 𝑘 ∈ (((𝐺𝐴) “ ℕ) ∖ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴𝑡))((2↑𝑛) · 𝑡) = 𝑚})) → 𝑘 ∈ ℂ)
114113mul02d 11449 . . . . . . 7 ((𝐴 ∈ (𝑇𝑅) ∧ 𝑘 ∈ (((𝐺𝐴) “ ℕ) ∖ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴𝑡))((2↑𝑛) · 𝑡) = 𝑚})) → (0 · 𝑘) = 0)
115110, 114eqtrd 2765 . . . . . 6 ((𝐴 ∈ (𝑇𝑅) ∧ 𝑘 ∈ (((𝐺𝐴) “ ℕ) ∖ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴𝑡))((2↑𝑛) · 𝑡) = 𝑚})) → (if(∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴𝑡))((2↑𝑛) · 𝑡) = 𝑘, 1, 0) · 𝑘) = 0)
11654, 100, 115, 40fsumss 15712 . . . . 5 (𝐴 ∈ (𝑇𝑅) → Σ𝑘 ∈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴𝑡))((2↑𝑛) · 𝑡) = 𝑚} (if(∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴𝑡))((2↑𝑛) · 𝑡) = 𝑘, 1, 0) · 𝑘) = Σ𝑘 ∈ ((𝐺𝐴) “ ℕ)(if(∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴𝑡))((2↑𝑛) · 𝑡) = 𝑘, 1, 0) · 𝑘))
11791, 116eqtr3d 2767 . . . 4 (𝐴 ∈ (𝑇𝑅) → Σ𝑤 𝑡 ∈ ((𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴𝑡)))((2↑(2nd𝑤)) · (1st𝑤)) = Σ𝑘 ∈ ((𝐺𝐴) “ ℕ)(if(∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴𝑡))((2↑𝑛) · 𝑡) = 𝑘, 1, 0) · 𝑘))
1182, 3, 4, 5, 6, 7, 8, 9, 10eulerpartlemt0 34122 . . . . . . . . . . . . 13 (𝐴 ∈ (𝑇𝑅) ↔ (𝐴 ∈ (ℕ0m ℕ) ∧ (𝐴 “ ℕ) ∈ Fin ∧ (𝐴 “ ℕ) ⊆ 𝐽))
119118simp1bi 1142 . . . . . . . . . . . 12 (𝐴 ∈ (𝑇𝑅) → 𝐴 ∈ (ℕ0m ℕ))
120 elmapi 8868 . . . . . . . . . . . 12 (𝐴 ∈ (ℕ0m ℕ) → 𝐴:ℕ⟶ℕ0)
121119, 120syl 17 . . . . . . . . . . 11 (𝐴 ∈ (𝑇𝑅) → 𝐴:ℕ⟶ℕ0)
122121adantr 479 . . . . . . . . . 10 ((𝐴 ∈ (𝑇𝑅) ∧ 𝑡 ∈ ((𝐴 “ ℕ) ∩ 𝐽)) → 𝐴:ℕ⟶ℕ0)
123 cnvimass 6086 . . . . . . . . . . . . 13 (𝐴 “ ℕ) ⊆ dom 𝐴
124123, 121fssdm 6742 . . . . . . . . . . . 12 (𝐴 ∈ (𝑇𝑅) → (𝐴 “ ℕ) ⊆ ℕ)
125124adantr 479 . . . . . . . . . . 11 ((𝐴 ∈ (𝑇𝑅) ∧ 𝑡 ∈ ((𝐴 “ ℕ) ∩ 𝐽)) → (𝐴 “ ℕ) ⊆ ℕ)
126 inss1 4227 . . . . . . . . . . . 12 ((𝐴 “ ℕ) ∩ 𝐽) ⊆ (𝐴 “ ℕ)
127126, 76sselid 3974 . . . . . . . . . . 11 ((𝐴 ∈ (𝑇𝑅) ∧ 𝑡 ∈ ((𝐴 “ ℕ) ∩ 𝐽)) → 𝑡 ∈ (𝐴 “ ℕ))
128125, 127sseldd 3977 . . . . . . . . . 10 ((𝐴 ∈ (𝑇𝑅) ∧ 𝑡 ∈ ((𝐴 “ ℕ) ∩ 𝐽)) → 𝑡 ∈ ℕ)
129122, 128ffvelcdmd 7094 . . . . . . . . 9 ((𝐴 ∈ (𝑇𝑅) ∧ 𝑡 ∈ ((𝐴 “ ℕ) ∩ 𝐽)) → (𝐴𝑡) ∈ ℕ0)
130 bitsfi 16420 . . . . . . . . 9 ((𝐴𝑡) ∈ ℕ0 → (bits‘(𝐴𝑡)) ∈ Fin)
131129, 130syl 17 . . . . . . . 8 ((𝐴 ∈ (𝑇𝑅) ∧ 𝑡 ∈ ((𝐴 “ ℕ) ∩ 𝐽)) → (bits‘(𝐴𝑡)) ∈ Fin)
132128nncnd 12266 . . . . . . . 8 ((𝐴 ∈ (𝑇𝑅) ∧ 𝑡 ∈ ((𝐴 “ ℕ) ∩ 𝐽)) → 𝑡 ∈ ℂ)
133 2cnd 12328 . . . . . . . . . 10 ((𝐴 ∈ (𝑇𝑅) ∧ (𝑡 ∈ ((𝐴 “ ℕ) ∩ 𝐽) ∧ 𝑛 ∈ (bits‘(𝐴𝑡)))) → 2 ∈ ℂ)
134 simprr 771 . . . . . . . . . . 11 ((𝐴 ∈ (𝑇𝑅) ∧ (𝑡 ∈ ((𝐴 “ ℕ) ∩ 𝐽) ∧ 𝑛 ∈ (bits‘(𝐴𝑡)))) → 𝑛 ∈ (bits‘(𝐴𝑡)))
13579, 134sselid 3974 . . . . . . . . . 10 ((𝐴 ∈ (𝑇𝑅) ∧ (𝑡 ∈ ((𝐴 “ ℕ) ∩ 𝐽) ∧ 𝑛 ∈ (bits‘(𝐴𝑡)))) → 𝑛 ∈ ℕ0)
136133, 135expcld 14151 . . . . . . . . 9 ((𝐴 ∈ (𝑇𝑅) ∧ (𝑡 ∈ ((𝐴 “ ℕ) ∩ 𝐽) ∧ 𝑛 ∈ (bits‘(𝐴𝑡)))) → (2↑𝑛) ∈ ℂ)
137136anassrs 466 . . . . . . . 8 (((𝐴 ∈ (𝑇𝑅) ∧ 𝑡 ∈ ((𝐴 “ ℕ) ∩ 𝐽)) ∧ 𝑛 ∈ (bits‘(𝐴𝑡))) → (2↑𝑛) ∈ ℂ)
138131, 132, 137fsummulc1 15772 . . . . . . 7 ((𝐴 ∈ (𝑇𝑅) ∧ 𝑡 ∈ ((𝐴 “ ℕ) ∩ 𝐽)) → (Σ𝑛 ∈ (bits‘(𝐴𝑡))(2↑𝑛) · 𝑡) = Σ𝑛 ∈ (bits‘(𝐴𝑡))((2↑𝑛) · 𝑡))
139138sumeq2dv 15690 . . . . . 6 (𝐴 ∈ (𝑇𝑅) → Σ𝑡 ∈ ((𝐴 “ ℕ) ∩ 𝐽)(Σ𝑛 ∈ (bits‘(𝐴𝑡))(2↑𝑛) · 𝑡) = Σ𝑡 ∈ ((𝐴 “ ℕ) ∩ 𝐽𝑛 ∈ (bits‘(𝐴𝑡))((2↑𝑛) · 𝑡))
140 bitsinv1 16425 . . . . . . . . 9 ((𝐴𝑡) ∈ ℕ0 → Σ𝑛 ∈ (bits‘(𝐴𝑡))(2↑𝑛) = (𝐴𝑡))
141140oveq1d 7434 . . . . . . . 8 ((𝐴𝑡) ∈ ℕ0 → (Σ𝑛 ∈ (bits‘(𝐴𝑡))(2↑𝑛) · 𝑡) = ((𝐴𝑡) · 𝑡))
142129, 141syl 17 . . . . . . 7 ((𝐴 ∈ (𝑇𝑅) ∧ 𝑡 ∈ ((𝐴 “ ℕ) ∩ 𝐽)) → (Σ𝑛 ∈ (bits‘(𝐴𝑡))(2↑𝑛) · 𝑡) = ((𝐴𝑡) · 𝑡))
143142sumeq2dv 15690 . . . . . 6 (𝐴 ∈ (𝑇𝑅) → Σ𝑡 ∈ ((𝐴 “ ℕ) ∩ 𝐽)(Σ𝑛 ∈ (bits‘(𝐴𝑡))(2↑𝑛) · 𝑡) = Σ𝑡 ∈ ((𝐴 “ ℕ) ∩ 𝐽)((𝐴𝑡) · 𝑡))
144 vex 3465 . . . . . . . . . 10 𝑡 ∈ V
145 vex 3465 . . . . . . . . . 10 𝑛 ∈ V
146144, 145op2ndd 8005 . . . . . . . . 9 (𝑤 = ⟨𝑡, 𝑛⟩ → (2nd𝑤) = 𝑛)
147146oveq2d 7435 . . . . . . . 8 (𝑤 = ⟨𝑡, 𝑛⟩ → (2↑(2nd𝑤)) = (2↑𝑛))
148144, 145op1std 8004 . . . . . . . 8 (𝑤 = ⟨𝑡, 𝑛⟩ → (1st𝑤) = 𝑡)
149147, 148oveq12d 7437 . . . . . . 7 (𝑤 = ⟨𝑡, 𝑛⟩ → ((2↑(2nd𝑤)) · (1st𝑤)) = ((2↑𝑛) · 𝑡))
150 inss2 4228 . . . . . . . . . 10 (𝑇𝑅) ⊆ 𝑅
151150sseli 3972 . . . . . . . . 9 (𝐴 ∈ (𝑇𝑅) → 𝐴𝑅)
152 cnveq 5876 . . . . . . . . . . . 12 (𝑓 = 𝐴𝑓 = 𝐴)
153152imaeq1d 6063 . . . . . . . . . . 11 (𝑓 = 𝐴 → (𝑓 “ ℕ) = (𝐴 “ ℕ))
154153eleq1d 2810 . . . . . . . . . 10 (𝑓 = 𝐴 → ((𝑓 “ ℕ) ∈ Fin ↔ (𝐴 “ ℕ) ∈ Fin))
155154, 9elab2g 3666 . . . . . . . . 9 (𝐴 ∈ (𝑇𝑅) → (𝐴𝑅 ↔ (𝐴 “ ℕ) ∈ Fin))
156151, 155mpbid 231 . . . . . . . 8 (𝐴 ∈ (𝑇𝑅) → (𝐴 “ ℕ) ∈ Fin)
157 ssfi 9201 . . . . . . . 8 (((𝐴 “ ℕ) ∈ Fin ∧ ((𝐴 “ ℕ) ∩ 𝐽) ⊆ (𝐴 “ ℕ)) → ((𝐴 “ ℕ) ∩ 𝐽) ∈ Fin)
158156, 126, 157sylancl 584 . . . . . . 7 (𝐴 ∈ (𝑇𝑅) → ((𝐴 “ ℕ) ∩ 𝐽) ∈ Fin)
159132adantrr 715 . . . . . . . 8 ((𝐴 ∈ (𝑇𝑅) ∧ (𝑡 ∈ ((𝐴 “ ℕ) ∩ 𝐽) ∧ 𝑛 ∈ (bits‘(𝐴𝑡)))) → 𝑡 ∈ ℂ)
160136, 159mulcld 11271 . . . . . . 7 ((𝐴 ∈ (𝑇𝑅) ∧ (𝑡 ∈ ((𝐴 “ ℕ) ∩ 𝐽) ∧ 𝑛 ∈ (bits‘(𝐴𝑡)))) → ((2↑𝑛) · 𝑡) ∈ ℂ)
161149, 158, 131, 160fsum2d 15758 . . . . . 6 (𝐴 ∈ (𝑇𝑅) → Σ𝑡 ∈ ((𝐴 “ ℕ) ∩ 𝐽𝑛 ∈ (bits‘(𝐴𝑡))((2↑𝑛) · 𝑡) = Σ𝑤 𝑡 ∈ ((𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴𝑡)))((2↑(2nd𝑤)) · (1st𝑤)))
162139, 143, 1613eqtr3d 2773 . . . . 5 (𝐴 ∈ (𝑇𝑅) → Σ𝑡 ∈ ((𝐴 “ ℕ) ∩ 𝐽)((𝐴𝑡) · 𝑡) = Σ𝑤 𝑡 ∈ ((𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴𝑡)))((2↑(2nd𝑤)) · (1st𝑤)))
163 inss1 4227 . . . . . . . . 9 (𝑇𝑅) ⊆ 𝑇
164163sseli 3972 . . . . . . . 8 (𝐴 ∈ (𝑇𝑅) → 𝐴𝑇)
165153sseq1d 4008 . . . . . . . . . 10 (𝑓 = 𝐴 → ((𝑓 “ ℕ) ⊆ 𝐽 ↔ (𝐴 “ ℕ) ⊆ 𝐽))
166165, 10elrab2 3682 . . . . . . . . 9 (𝐴𝑇 ↔ (𝐴 ∈ (ℕ0m ℕ) ∧ (𝐴 “ ℕ) ⊆ 𝐽))
167166simprbi 495 . . . . . . . 8 (𝐴𝑇 → (𝐴 “ ℕ) ⊆ 𝐽)
168164, 167syl 17 . . . . . . 7 (𝐴 ∈ (𝑇𝑅) → (𝐴 “ ℕ) ⊆ 𝐽)
169 dfss2 3962 . . . . . . 7 ((𝐴 “ ℕ) ⊆ 𝐽 ↔ ((𝐴 “ ℕ) ∩ 𝐽) = (𝐴 “ ℕ))
170168, 169sylib 217 . . . . . 6 (𝐴 ∈ (𝑇𝑅) → ((𝐴 “ ℕ) ∩ 𝐽) = (𝐴 “ ℕ))
171170sumeq1d 15688 . . . . 5 (𝐴 ∈ (𝑇𝑅) → Σ𝑡 ∈ ((𝐴 “ ℕ) ∩ 𝐽)((𝐴𝑡) · 𝑡) = Σ𝑡 ∈ (𝐴 “ ℕ)((𝐴𝑡) · 𝑡))
172162, 171eqtr3d 2767 . . . 4 (𝐴 ∈ (𝑇𝑅) → Σ𝑤 𝑡 ∈ ((𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴𝑡)))((2↑(2nd𝑤)) · (1st𝑤)) = Σ𝑡 ∈ (𝐴 “ ℕ)((𝐴𝑡) · 𝑡))
17327, 117, 1723eqtr2d 2771 . . 3 (𝐴 ∈ (𝑇𝑅) → Σ𝑘 ∈ ((𝐺𝐴) “ ℕ)(((𝐺𝐴)‘𝑘) · 𝑘) = Σ𝑡 ∈ (𝐴 “ ℕ)((𝐴𝑡) · 𝑡))
174 fveq2 6896 . . . . 5 (𝑘 = 𝑡 → (𝐴𝑘) = (𝐴𝑡))
175 id 22 . . . . 5 (𝑘 = 𝑡𝑘 = 𝑡)
176174, 175oveq12d 7437 . . . 4 (𝑘 = 𝑡 → ((𝐴𝑘) · 𝑘) = ((𝐴𝑡) · 𝑡))
177176cbvsumv 15683 . . 3 Σ𝑘 ∈ (𝐴 “ ℕ)((𝐴𝑘) · 𝑘) = Σ𝑡 ∈ (𝐴 “ ℕ)((𝐴𝑡) · 𝑡)
178173, 177eqtr4di 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)
182179, 180, 181mp2an 690 . . . . . . 7 {0, 1} ⊆ ℕ0
183 fss 6739 . . . . . . 7 (((𝐺𝐴):ℕ⟶{0, 1} ∧ {0, 1} ⊆ ℕ0) → (𝐺𝐴):ℕ⟶ℕ0)
184182, 183mpan2 689 . . . . . 6 ((𝐺𝐴):ℕ⟶{0, 1} → (𝐺𝐴):ℕ⟶ℕ0)
185 nn0ex 12516 . . . . . . . 8 0 ∈ V
186 nnex 12256 . . . . . . . 8 ℕ ∈ V
187185, 186elmap 8890 . . . . . . 7 ((𝐺𝐴) ∈ (ℕ0m ℕ) ↔ (𝐺𝐴):ℕ⟶ℕ0)
188187biimpri 227 . . . . . 6 ((𝐺𝐴):ℕ⟶ℕ0 → (𝐺𝐴) ∈ (ℕ0m ℕ))
18919, 184, 1883syl 18 . . . . 5 ((𝐺𝐴) ∈ ({0, 1} ↑m ℕ) → (𝐺𝐴) ∈ (ℕ0m ℕ))
190189anim1i 613 . . . 4 (((𝐺𝐴) ∈ ({0, 1} ↑m ℕ) ∧ (𝐺𝐴) ∈ 𝑅) → ((𝐺𝐴) ∈ (ℕ0m ℕ) ∧ (𝐺𝐴) ∈ 𝑅))
191 elin 3960 . . . 4 ((𝐺𝐴) ∈ ((ℕ0m ℕ) ∩ 𝑅) ↔ ((𝐺𝐴) ∈ (ℕ0m ℕ) ∧ (𝐺𝐴) ∈ 𝑅))
192190, 16, 1913imtr4i 291 . . 3 ((𝐺𝐴) ∈ (({0, 1} ↑m ℕ) ∩ 𝑅) → (𝐺𝐴) ∈ ((ℕ0m ℕ) ∩ 𝑅))
193 eulerpart.s . . . 4 𝑆 = (𝑓 ∈ ((ℕ0m ℕ) ∩ 𝑅) ↦ Σ𝑘 ∈ ℕ ((𝑓𝑘) · 𝑘))
1949, 193eulerpartlemsv2 34111 . . 3 ((𝐺𝐴) ∈ ((ℕ0m ℕ) ∩ 𝑅) → (𝑆‘(𝐺𝐴)) = Σ𝑘 ∈ ((𝐺𝐴) “ ℕ)(((𝐺𝐴)‘𝑘) · 𝑘))
19515, 192, 1943syl 18 . 2 (𝐴 ∈ (𝑇𝑅) → (𝑆‘(𝐺𝐴)) = Σ𝑘 ∈ ((𝐺𝐴) “ ℕ)(((𝐺𝐴)‘𝑘) · 𝑘))
196119, 151elind 4192 . . 3 (𝐴 ∈ (𝑇𝑅) → 𝐴 ∈ ((ℕ0m ℕ) ∩ 𝑅))
1979, 193eulerpartlemsv2 34111 . . 3 (𝐴 ∈ ((ℕ0m ℕ) ∩ 𝑅) → (𝑆𝐴) = Σ𝑘 ∈ (𝐴 “ ℕ)((𝐴𝑘) · 𝑘))
198196, 197syl 17 . 2 (𝐴 ∈ (𝑇𝑅) → (𝑆𝐴) = Σ𝑘 ∈ (𝐴 “ ℕ)((𝐴𝑘) · 𝑘))
199178, 195, 1983eqtr4d 2775 1 (𝐴 ∈ (𝑇𝑅) → (𝑆‘(𝐺𝐴)) = (𝑆𝐴))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 394   = wceq 1533  wcel 2098  {cab 2702  wral 3050  wrex 3059  {crab 3418  Vcvv 3461  cdif 3941  cin 3943  wss 3944  c0 4322  ifcif 4530  𝒫 cpw 4604  {csn 4630  {cpr 4632  cop 4636   ciun 4997   class class class wbr 5149  {copab 5211  cmpt 5232   × cxp 5676  ccnv 5677  dom cdm 5678  cres 5680  cima 5681  ccom 5682   Fn wfn 6544  wf 6545  1-1-ontowf1o 6548  cfv 6549  (class class class)co 7419  cmpo 7421  1st c1st 7992  2nd c2nd 7993   supp csupp 8165  m cmap 8845  cen 8961  Fincfn 8964  cc 11143  0cc0 11145  1c1 11146   · cmul 11150  cle 11286  cn 12250  2c2 12305  0cn0 12510  cexp 14067  Σcsu 15673  cdvds 16239  bitscbits 16402  𝟭cind 33762
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696  ax-rep 5286  ax-sep 5300  ax-nul 5307  ax-pow 5365  ax-pr 5429  ax-un 7741  ax-inf2 9671  ax-ac2 10493  ax-cnex 11201  ax-resscn 11202  ax-1cn 11203  ax-icn 11204  ax-addcl 11205  ax-addrcl 11206  ax-mulcl 11207  ax-mulrcl 11208  ax-mulcom 11209  ax-addass 11210  ax-mulass 11211  ax-distr 11212  ax-i2m1 11213  ax-1ne0 11214  ax-1rid 11215  ax-rnegex 11216  ax-rrecex 11217  ax-cnre 11218  ax-pre-lttri 11219  ax-pre-lttrn 11220  ax-pre-ltadd 11221  ax-pre-mulgt0 11222  ax-pre-sup 11223
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ne 2930  df-nel 3036  df-ral 3051  df-rex 3060  df-rmo 3363  df-reu 3364  df-rab 3419  df-v 3463  df-sbc 3774  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-pss 3964  df-nul 4323  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4910  df-int 4951  df-iun 4999  df-disj 5115  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5576  df-eprel 5582  df-po 5590  df-so 5591  df-fr 5633  df-se 5634  df-we 5635  df-xp 5684  df-rel 5685  df-cnv 5686  df-co 5687  df-dm 5688  df-rn 5689  df-res 5690  df-ima 5691  df-pred 6307  df-ord 6374  df-on 6375  df-lim 6376  df-suc 6377  df-iota 6501  df-fun 6551  df-fn 6552  df-f 6553  df-f1 6554  df-fo 6555  df-f1o 6556  df-fv 6557  df-isom 6558  df-riota 7375  df-ov 7422  df-oprab 7423  df-mpo 7424  df-om 7872  df-1st 7994  df-2nd 7995  df-supp 8166  df-frecs 8287  df-wrecs 8318  df-recs 8392  df-rdg 8431  df-1o 8487  df-2o 8488  df-oadd 8491  df-er 8725  df-map 8847  df-pm 8848  df-en 8965  df-dom 8966  df-sdom 8967  df-fin 8968  df-fsupp 9393  df-sup 9472  df-inf 9473  df-oi 9540  df-dju 9931  df-card 9969  df-acn 9972  df-ac 10146  df-pnf 11287  df-mnf 11288  df-xr 11289  df-ltxr 11290  df-le 11291  df-sub 11483  df-neg 11484  df-div 11909  df-nn 12251  df-2 12313  df-3 12314  df-n0 12511  df-xnn0 12583  df-z 12597  df-uz 12861  df-rp 13015  df-fz 13525  df-fzo 13668  df-fl 13798  df-mod 13876  df-seq 14008  df-exp 14068  df-hash 14331  df-cj 15087  df-re 15088  df-im 15089  df-sqrt 15223  df-abs 15224  df-clim 15473  df-sum 15674  df-dvds 16240  df-bits 16405  df-ind 33763
This theorem is referenced by:  eulerpartlemn  34134
  Copyright terms: Public domain W3C validator