Metamath Proof Explorer


Theorem eulerpartlemgs2

Description: Lemma for eulerpart : The G function also preserves partition sums. (Contributed by Thierry Arnoux, 10-Sep-2017)

Ref Expression
Hypotheses 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 eulerpartlemgs2 ( 𝐴 ∈ ( 𝑇𝑅 ) → ( 𝑆 ‘ ( 𝐺𝐴 ) ) = ( 𝑆𝐴 ) )

Proof

Step Hyp Ref Expression
1 eulerpart.p 𝑃 = { 𝑓 ∈ ( ℕ0m ℕ ) ∣ ( ( 𝑓 “ ℕ ) ∈ Fin ∧ Σ 𝑘 ∈ ℕ ( ( 𝑓𝑘 ) · 𝑘 ) = 𝑁 ) }
2 eulerpart.o 𝑂 = { 𝑔𝑃 ∣ ∀ 𝑛 ∈ ( 𝑔 “ ℕ ) ¬ 2 ∥ 𝑛 }
3 eulerpart.d 𝐷 = { 𝑔𝑃 ∣ ∀ 𝑛 ∈ ℕ ( 𝑔𝑛 ) ≤ 1 }
4 eulerpart.j 𝐽 = { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 }
5 eulerpart.f 𝐹 = ( 𝑥𝐽 , 𝑦 ∈ ℕ0 ↦ ( ( 2 ↑ 𝑦 ) · 𝑥 ) )
6 eulerpart.h 𝐻 = { 𝑟 ∈ ( ( 𝒫 ℕ0 ∩ Fin ) ↑m 𝐽 ) ∣ ( 𝑟 supp ∅ ) ∈ Fin }
7 eulerpart.m 𝑀 = ( 𝑟𝐻 ↦ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥𝐽𝑦 ∈ ( 𝑟𝑥 ) ) } )
8 eulerpart.r 𝑅 = { 𝑓 ∣ ( 𝑓 “ ℕ ) ∈ Fin }
9 eulerpart.t 𝑇 = { 𝑓 ∈ ( ℕ0m ℕ ) ∣ ( 𝑓 “ ℕ ) ⊆ 𝐽 }
10 eulerpart.g 𝐺 = ( 𝑜 ∈ ( 𝑇𝑅 ) ↦ ( ( 𝟭 ‘ ℕ ) ‘ ( 𝐹 “ ( 𝑀 ‘ ( bits ∘ ( 𝑜𝐽 ) ) ) ) ) )
11 eulerpart.s 𝑆 = ( 𝑓 ∈ ( ( ℕ0m ℕ ) ∩ 𝑅 ) ↦ Σ 𝑘 ∈ ℕ ( ( 𝑓𝑘 ) · 𝑘 ) )
12 cnvimass ( ( 𝐺𝐴 ) “ ℕ ) ⊆ dom ( 𝐺𝐴 )
13 1 2 3 4 5 6 7 8 9 10 eulerpartgbij 𝐺 : ( 𝑇𝑅 ) –1-1-onto→ ( ( { 0 , 1 } ↑m ℕ ) ∩ 𝑅 )
14 f1of ( 𝐺 : ( 𝑇𝑅 ) –1-1-onto→ ( ( { 0 , 1 } ↑m ℕ ) ∩ 𝑅 ) → 𝐺 : ( 𝑇𝑅 ) ⟶ ( ( { 0 , 1 } ↑m ℕ ) ∩ 𝑅 ) )
15 13 14 ax-mp 𝐺 : ( 𝑇𝑅 ) ⟶ ( ( { 0 , 1 } ↑m ℕ ) ∩ 𝑅 )
16 15 ffvelrni ( 𝐴 ∈ ( 𝑇𝑅 ) → ( 𝐺𝐴 ) ∈ ( ( { 0 , 1 } ↑m ℕ ) ∩ 𝑅 ) )
17 elin ( ( 𝐺𝐴 ) ∈ ( ( { 0 , 1 } ↑m ℕ ) ∩ 𝑅 ) ↔ ( ( 𝐺𝐴 ) ∈ ( { 0 , 1 } ↑m ℕ ) ∧ ( 𝐺𝐴 ) ∈ 𝑅 ) )
18 16 17 sylib ( 𝐴 ∈ ( 𝑇𝑅 ) → ( ( 𝐺𝐴 ) ∈ ( { 0 , 1 } ↑m ℕ ) ∧ ( 𝐺𝐴 ) ∈ 𝑅 ) )
19 18 simpld ( 𝐴 ∈ ( 𝑇𝑅 ) → ( 𝐺𝐴 ) ∈ ( { 0 , 1 } ↑m ℕ ) )
20 elmapi ( ( 𝐺𝐴 ) ∈ ( { 0 , 1 } ↑m ℕ ) → ( 𝐺𝐴 ) : ℕ ⟶ { 0 , 1 } )
21 fdm ( ( 𝐺𝐴 ) : ℕ ⟶ { 0 , 1 } → dom ( 𝐺𝐴 ) = ℕ )
22 19 20 21 3syl ( 𝐴 ∈ ( 𝑇𝑅 ) → dom ( 𝐺𝐴 ) = ℕ )
23 12 22 sseqtrid ( 𝐴 ∈ ( 𝑇𝑅 ) → ( ( 𝐺𝐴 ) “ ℕ ) ⊆ ℕ )
24 23 sselda ( ( 𝐴 ∈ ( 𝑇𝑅 ) ∧ 𝑘 ∈ ( ( 𝐺𝐴 ) “ ℕ ) ) → 𝑘 ∈ ℕ )
25 1 2 3 4 5 6 7 8 9 10 eulerpartlemgvv ( ( 𝐴 ∈ ( 𝑇𝑅 ) ∧ 𝑘 ∈ ℕ ) → ( ( 𝐺𝐴 ) ‘ 𝑘 ) = if ( ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑘 , 1 , 0 ) )
26 25 oveq1d ( ( 𝐴 ∈ ( 𝑇𝑅 ) ∧ 𝑘 ∈ ℕ ) → ( ( ( 𝐺𝐴 ) ‘ 𝑘 ) · 𝑘 ) = ( if ( ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑘 , 1 , 0 ) · 𝑘 ) )
27 24 26 syldan ( ( 𝐴 ∈ ( 𝑇𝑅 ) ∧ 𝑘 ∈ ( ( 𝐺𝐴 ) “ ℕ ) ) → ( ( ( 𝐺𝐴 ) ‘ 𝑘 ) · 𝑘 ) = ( if ( ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑘 , 1 , 0 ) · 𝑘 ) )
28 27 sumeq2dv ( 𝐴 ∈ ( 𝑇𝑅 ) → Σ 𝑘 ∈ ( ( 𝐺𝐴 ) “ ℕ ) ( ( ( 𝐺𝐴 ) ‘ 𝑘 ) · 𝑘 ) = Σ 𝑘 ∈ ( ( 𝐺𝐴 ) “ ℕ ) ( if ( ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑘 , 1 , 0 ) · 𝑘 ) )
29 eqeq2 ( 𝑚 = 𝑘 → ( ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑚 ↔ ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑘 ) )
30 29 2rexbidv ( 𝑚 = 𝑘 → ( ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑚 ↔ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑘 ) )
31 30 elrab ( 𝑘 ∈ { 𝑚 ∈ ℕ ∣ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑚 } ↔ ( 𝑘 ∈ ℕ ∧ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑘 ) )
32 31 simprbi ( 𝑘 ∈ { 𝑚 ∈ ℕ ∣ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑚 } → ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑘 )
33 32 iftrued ( 𝑘 ∈ { 𝑚 ∈ ℕ ∣ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑚 } → if ( ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑘 , 1 , 0 ) = 1 )
34 33 oveq1d ( 𝑘 ∈ { 𝑚 ∈ ℕ ∣ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑚 } → ( if ( ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑘 , 1 , 0 ) · 𝑘 ) = ( 1 · 𝑘 ) )
35 elrabi ( 𝑘 ∈ { 𝑚 ∈ ℕ ∣ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑚 } → 𝑘 ∈ ℕ )
36 35 nncnd ( 𝑘 ∈ { 𝑚 ∈ ℕ ∣ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑚 } → 𝑘 ∈ ℂ )
37 36 mulid2d ( 𝑘 ∈ { 𝑚 ∈ ℕ ∣ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑚 } → ( 1 · 𝑘 ) = 𝑘 )
38 34 37 eqtrd ( 𝑘 ∈ { 𝑚 ∈ ℕ ∣ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑚 } → ( if ( ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑘 , 1 , 0 ) · 𝑘 ) = 𝑘 )
39 38 sumeq2i Σ 𝑘 ∈ { 𝑚 ∈ ℕ ∣ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑚 } ( if ( ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑘 , 1 , 0 ) · 𝑘 ) = Σ 𝑘 ∈ { 𝑚 ∈ ℕ ∣ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑚 } 𝑘
40 id ( 𝑘 = ( ( 2 ↑ ( 2nd𝑤 ) ) · ( 1st𝑤 ) ) → 𝑘 = ( ( 2 ↑ ( 2nd𝑤 ) ) · ( 1st𝑤 ) ) )
41 1 2 3 4 5 6 7 8 9 10 eulerpartlemgf ( 𝐴 ∈ ( 𝑇𝑅 ) → ( ( 𝐺𝐴 ) “ ℕ ) ∈ Fin )
42 35 adantl ( ( 𝐴 ∈ ( 𝑇𝑅 ) ∧ 𝑘 ∈ { 𝑚 ∈ ℕ ∣ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑚 } ) → 𝑘 ∈ ℕ )
43 42 25 syldan ( ( 𝐴 ∈ ( 𝑇𝑅 ) ∧ 𝑘 ∈ { 𝑚 ∈ ℕ ∣ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑚 } ) → ( ( 𝐺𝐴 ) ‘ 𝑘 ) = if ( ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑘 , 1 , 0 ) )
44 32 adantl ( ( 𝐴 ∈ ( 𝑇𝑅 ) ∧ 𝑘 ∈ { 𝑚 ∈ ℕ ∣ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑚 } ) → ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑘 )
45 44 iftrued ( ( 𝐴 ∈ ( 𝑇𝑅 ) ∧ 𝑘 ∈ { 𝑚 ∈ ℕ ∣ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑚 } ) → if ( ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑘 , 1 , 0 ) = 1 )
46 43 45 eqtrd ( ( 𝐴 ∈ ( 𝑇𝑅 ) ∧ 𝑘 ∈ { 𝑚 ∈ ℕ ∣ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑚 } ) → ( ( 𝐺𝐴 ) ‘ 𝑘 ) = 1 )
47 1nn 1 ∈ ℕ
48 46 47 eqeltrdi ( ( 𝐴 ∈ ( 𝑇𝑅 ) ∧ 𝑘 ∈ { 𝑚 ∈ ℕ ∣ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑚 } ) → ( ( 𝐺𝐴 ) ‘ 𝑘 ) ∈ ℕ )
49 19 20 syl ( 𝐴 ∈ ( 𝑇𝑅 ) → ( 𝐺𝐴 ) : ℕ ⟶ { 0 , 1 } )
50 ffn ( ( 𝐺𝐴 ) : ℕ ⟶ { 0 , 1 } → ( 𝐺𝐴 ) Fn ℕ )
51 elpreima ( ( 𝐺𝐴 ) Fn ℕ → ( 𝑘 ∈ ( ( 𝐺𝐴 ) “ ℕ ) ↔ ( 𝑘 ∈ ℕ ∧ ( ( 𝐺𝐴 ) ‘ 𝑘 ) ∈ ℕ ) ) )
52 49 50 51 3syl ( 𝐴 ∈ ( 𝑇𝑅 ) → ( 𝑘 ∈ ( ( 𝐺𝐴 ) “ ℕ ) ↔ ( 𝑘 ∈ ℕ ∧ ( ( 𝐺𝐴 ) ‘ 𝑘 ) ∈ ℕ ) ) )
53 52 adantr ( ( 𝐴 ∈ ( 𝑇𝑅 ) ∧ 𝑘 ∈ { 𝑚 ∈ ℕ ∣ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑚 } ) → ( 𝑘 ∈ ( ( 𝐺𝐴 ) “ ℕ ) ↔ ( 𝑘 ∈ ℕ ∧ ( ( 𝐺𝐴 ) ‘ 𝑘 ) ∈ ℕ ) ) )
54 42 48 53 mpbir2and ( ( 𝐴 ∈ ( 𝑇𝑅 ) ∧ 𝑘 ∈ { 𝑚 ∈ ℕ ∣ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑚 } ) → 𝑘 ∈ ( ( 𝐺𝐴 ) “ ℕ ) )
55 54 ex ( 𝐴 ∈ ( 𝑇𝑅 ) → ( 𝑘 ∈ { 𝑚 ∈ ℕ ∣ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑚 } → 𝑘 ∈ ( ( 𝐺𝐴 ) “ ℕ ) ) )
56 55 ssrdv ( 𝐴 ∈ ( 𝑇𝑅 ) → { 𝑚 ∈ ℕ ∣ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑚 } ⊆ ( ( 𝐺𝐴 ) “ ℕ ) )
57 ssfi ( ( ( ( 𝐺𝐴 ) “ ℕ ) ∈ Fin ∧ { 𝑚 ∈ ℕ ∣ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑚 } ⊆ ( ( 𝐺𝐴 ) “ ℕ ) ) → { 𝑚 ∈ ℕ ∣ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑚 } ∈ Fin )
58 41 56 57 syl2anc ( 𝐴 ∈ ( 𝑇𝑅 ) → { 𝑚 ∈ ℕ ∣ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑚 } ∈ Fin )
59 cnvexg ( 𝐴 ∈ ( 𝑇𝑅 ) → 𝐴 ∈ V )
60 imaexg ( 𝐴 ∈ V → ( 𝐴 “ ℕ ) ∈ V )
61 inex1g ( ( 𝐴 “ ℕ ) ∈ V → ( ( 𝐴 “ ℕ ) ∩ 𝐽 ) ∈ V )
62 59 60 61 3syl ( 𝐴 ∈ ( 𝑇𝑅 ) → ( ( 𝐴 “ ℕ ) ∩ 𝐽 ) ∈ V )
63 snex { 𝑡 } ∈ V
64 fvex ( bits ‘ ( 𝐴𝑡 ) ) ∈ V
65 63 64 xpex ( { 𝑡 } × ( bits ‘ ( 𝐴𝑡 ) ) ) ∈ V
66 65 rgenw 𝑡 ∈ ( ( 𝐴 “ ℕ ) ∩ 𝐽 ) ( { 𝑡 } × ( bits ‘ ( 𝐴𝑡 ) ) ) ∈ V
67 iunexg ( ( ( ( 𝐴 “ ℕ ) ∩ 𝐽 ) ∈ V ∧ ∀ 𝑡 ∈ ( ( 𝐴 “ ℕ ) ∩ 𝐽 ) ( { 𝑡 } × ( bits ‘ ( 𝐴𝑡 ) ) ) ∈ V ) → 𝑡 ∈ ( ( 𝐴 “ ℕ ) ∩ 𝐽 ) ( { 𝑡 } × ( bits ‘ ( 𝐴𝑡 ) ) ) ∈ V )
68 62 66 67 sylancl ( 𝐴 ∈ ( 𝑇𝑅 ) → 𝑡 ∈ ( ( 𝐴 “ ℕ ) ∩ 𝐽 ) ( { 𝑡 } × ( bits ‘ ( 𝐴𝑡 ) ) ) ∈ V )
69 eqid 𝑡 ∈ ( ( 𝐴 “ ℕ ) ∩ 𝐽 ) ( { 𝑡 } × ( bits ‘ ( 𝐴𝑡 ) ) ) = 𝑡 ∈ ( ( 𝐴 “ ℕ ) ∩ 𝐽 ) ( { 𝑡 } × ( bits ‘ ( 𝐴𝑡 ) ) )
70 1 2 3 4 5 6 7 8 9 10 69 eulerpartlemgh ( 𝐴 ∈ ( 𝑇𝑅 ) → ( 𝐹 𝑡 ∈ ( ( 𝐴 “ ℕ ) ∩ 𝐽 ) ( { 𝑡 } × ( bits ‘ ( 𝐴𝑡 ) ) ) ) : 𝑡 ∈ ( ( 𝐴 “ ℕ ) ∩ 𝐽 ) ( { 𝑡 } × ( bits ‘ ( 𝐴𝑡 ) ) ) –1-1-onto→ { 𝑚 ∈ ℕ ∣ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑚 } )
71 f1oeng ( ( 𝑡 ∈ ( ( 𝐴 “ ℕ ) ∩ 𝐽 ) ( { 𝑡 } × ( bits ‘ ( 𝐴𝑡 ) ) ) ∈ V ∧ ( 𝐹 𝑡 ∈ ( ( 𝐴 “ ℕ ) ∩ 𝐽 ) ( { 𝑡 } × ( bits ‘ ( 𝐴𝑡 ) ) ) ) : 𝑡 ∈ ( ( 𝐴 “ ℕ ) ∩ 𝐽 ) ( { 𝑡 } × ( bits ‘ ( 𝐴𝑡 ) ) ) –1-1-onto→ { 𝑚 ∈ ℕ ∣ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑚 } ) → 𝑡 ∈ ( ( 𝐴 “ ℕ ) ∩ 𝐽 ) ( { 𝑡 } × ( bits ‘ ( 𝐴𝑡 ) ) ) ≈ { 𝑚 ∈ ℕ ∣ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑚 } )
72 68 70 71 syl2anc ( 𝐴 ∈ ( 𝑇𝑅 ) → 𝑡 ∈ ( ( 𝐴 “ ℕ ) ∩ 𝐽 ) ( { 𝑡 } × ( bits ‘ ( 𝐴𝑡 ) ) ) ≈ { 𝑚 ∈ ℕ ∣ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑚 } )
73 enfii ( ( { 𝑚 ∈ ℕ ∣ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑚 } ∈ Fin ∧ 𝑡 ∈ ( ( 𝐴 “ ℕ ) ∩ 𝐽 ) ( { 𝑡 } × ( bits ‘ ( 𝐴𝑡 ) ) ) ≈ { 𝑚 ∈ ℕ ∣ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑚 } ) → 𝑡 ∈ ( ( 𝐴 “ ℕ ) ∩ 𝐽 ) ( { 𝑡 } × ( bits ‘ ( 𝐴𝑡 ) ) ) ∈ Fin )
74 58 72 73 syl2anc ( 𝐴 ∈ ( 𝑇𝑅 ) → 𝑡 ∈ ( ( 𝐴 “ ℕ ) ∩ 𝐽 ) ( { 𝑡 } × ( bits ‘ ( 𝐴𝑡 ) ) ) ∈ Fin )
75 fvres ( 𝑤 𝑡 ∈ ( ( 𝐴 “ ℕ ) ∩ 𝐽 ) ( { 𝑡 } × ( bits ‘ ( 𝐴𝑡 ) ) ) → ( ( 𝐹 𝑡 ∈ ( ( 𝐴 “ ℕ ) ∩ 𝐽 ) ( { 𝑡 } × ( bits ‘ ( 𝐴𝑡 ) ) ) ) ‘ 𝑤 ) = ( 𝐹𝑤 ) )
76 75 adantl ( ( 𝐴 ∈ ( 𝑇𝑅 ) ∧ 𝑤 𝑡 ∈ ( ( 𝐴 “ ℕ ) ∩ 𝐽 ) ( { 𝑡 } × ( bits ‘ ( 𝐴𝑡 ) ) ) ) → ( ( 𝐹 𝑡 ∈ ( ( 𝐴 “ ℕ ) ∩ 𝐽 ) ( { 𝑡 } × ( bits ‘ ( 𝐴𝑡 ) ) ) ) ‘ 𝑤 ) = ( 𝐹𝑤 ) )
77 inss2 ( ( 𝐴 “ ℕ ) ∩ 𝐽 ) ⊆ 𝐽
78 simpr ( ( 𝐴 ∈ ( 𝑇𝑅 ) ∧ 𝑡 ∈ ( ( 𝐴 “ ℕ ) ∩ 𝐽 ) ) → 𝑡 ∈ ( ( 𝐴 “ ℕ ) ∩ 𝐽 ) )
79 77 78 sselid ( ( 𝐴 ∈ ( 𝑇𝑅 ) ∧ 𝑡 ∈ ( ( 𝐴 “ ℕ ) ∩ 𝐽 ) ) → 𝑡𝐽 )
80 79 snssd ( ( 𝐴 ∈ ( 𝑇𝑅 ) ∧ 𝑡 ∈ ( ( 𝐴 “ ℕ ) ∩ 𝐽 ) ) → { 𝑡 } ⊆ 𝐽 )
81 bitsss ( bits ‘ ( 𝐴𝑡 ) ) ⊆ ℕ0
82 xpss12 ( ( { 𝑡 } ⊆ 𝐽 ∧ ( bits ‘ ( 𝐴𝑡 ) ) ⊆ ℕ0 ) → ( { 𝑡 } × ( bits ‘ ( 𝐴𝑡 ) ) ) ⊆ ( 𝐽 × ℕ0 ) )
83 80 81 82 sylancl ( ( 𝐴 ∈ ( 𝑇𝑅 ) ∧ 𝑡 ∈ ( ( 𝐴 “ ℕ ) ∩ 𝐽 ) ) → ( { 𝑡 } × ( bits ‘ ( 𝐴𝑡 ) ) ) ⊆ ( 𝐽 × ℕ0 ) )
84 83 ralrimiva ( 𝐴 ∈ ( 𝑇𝑅 ) → ∀ 𝑡 ∈ ( ( 𝐴 “ ℕ ) ∩ 𝐽 ) ( { 𝑡 } × ( bits ‘ ( 𝐴𝑡 ) ) ) ⊆ ( 𝐽 × ℕ0 ) )
85 iunss ( 𝑡 ∈ ( ( 𝐴 “ ℕ ) ∩ 𝐽 ) ( { 𝑡 } × ( bits ‘ ( 𝐴𝑡 ) ) ) ⊆ ( 𝐽 × ℕ0 ) ↔ ∀ 𝑡 ∈ ( ( 𝐴 “ ℕ ) ∩ 𝐽 ) ( { 𝑡 } × ( bits ‘ ( 𝐴𝑡 ) ) ) ⊆ ( 𝐽 × ℕ0 ) )
86 84 85 sylibr ( 𝐴 ∈ ( 𝑇𝑅 ) → 𝑡 ∈ ( ( 𝐴 “ ℕ ) ∩ 𝐽 ) ( { 𝑡 } × ( bits ‘ ( 𝐴𝑡 ) ) ) ⊆ ( 𝐽 × ℕ0 ) )
87 86 sselda ( ( 𝐴 ∈ ( 𝑇𝑅 ) ∧ 𝑤 𝑡 ∈ ( ( 𝐴 “ ℕ ) ∩ 𝐽 ) ( { 𝑡 } × ( bits ‘ ( 𝐴𝑡 ) ) ) ) → 𝑤 ∈ ( 𝐽 × ℕ0 ) )
88 4 5 oddpwdcv ( 𝑤 ∈ ( 𝐽 × ℕ0 ) → ( 𝐹𝑤 ) = ( ( 2 ↑ ( 2nd𝑤 ) ) · ( 1st𝑤 ) ) )
89 87 88 syl ( ( 𝐴 ∈ ( 𝑇𝑅 ) ∧ 𝑤 𝑡 ∈ ( ( 𝐴 “ ℕ ) ∩ 𝐽 ) ( { 𝑡 } × ( bits ‘ ( 𝐴𝑡 ) ) ) ) → ( 𝐹𝑤 ) = ( ( 2 ↑ ( 2nd𝑤 ) ) · ( 1st𝑤 ) ) )
90 76 89 eqtrd ( ( 𝐴 ∈ ( 𝑇𝑅 ) ∧ 𝑤 𝑡 ∈ ( ( 𝐴 “ ℕ ) ∩ 𝐽 ) ( { 𝑡 } × ( bits ‘ ( 𝐴𝑡 ) ) ) ) → ( ( 𝐹 𝑡 ∈ ( ( 𝐴 “ ℕ ) ∩ 𝐽 ) ( { 𝑡 } × ( bits ‘ ( 𝐴𝑡 ) ) ) ) ‘ 𝑤 ) = ( ( 2 ↑ ( 2nd𝑤 ) ) · ( 1st𝑤 ) ) )
91 42 nncnd ( ( 𝐴 ∈ ( 𝑇𝑅 ) ∧ 𝑘 ∈ { 𝑚 ∈ ℕ ∣ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑚 } ) → 𝑘 ∈ ℂ )
92 40 74 70 90 91 fsumf1o ( 𝐴 ∈ ( 𝑇𝑅 ) → Σ 𝑘 ∈ { 𝑚 ∈ ℕ ∣ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑚 } 𝑘 = Σ 𝑤 𝑡 ∈ ( ( 𝐴 “ ℕ ) ∩ 𝐽 ) ( { 𝑡 } × ( bits ‘ ( 𝐴𝑡 ) ) ) ( ( 2 ↑ ( 2nd𝑤 ) ) · ( 1st𝑤 ) ) )
93 39 92 syl5eq ( 𝐴 ∈ ( 𝑇𝑅 ) → Σ 𝑘 ∈ { 𝑚 ∈ ℕ ∣ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑚 } ( if ( ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑘 , 1 , 0 ) · 𝑘 ) = Σ 𝑤 𝑡 ∈ ( ( 𝐴 “ ℕ ) ∩ 𝐽 ) ( { 𝑡 } × ( bits ‘ ( 𝐴𝑡 ) ) ) ( ( 2 ↑ ( 2nd𝑤 ) ) · ( 1st𝑤 ) ) )
94 ax-1cn 1 ∈ ℂ
95 0cn 0 ∈ ℂ
96 94 95 ifcli if ( ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑘 , 1 , 0 ) ∈ ℂ
97 96 a1i ( ( 𝐴 ∈ ( 𝑇𝑅 ) ∧ 𝑘 ∈ { 𝑚 ∈ ℕ ∣ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑚 } ) → if ( ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑘 , 1 , 0 ) ∈ ℂ )
98 ssrab2 { 𝑚 ∈ ℕ ∣ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑚 } ⊆ ℕ
99 simpr ( ( 𝐴 ∈ ( 𝑇𝑅 ) ∧ 𝑘 ∈ { 𝑚 ∈ ℕ ∣ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑚 } ) → 𝑘 ∈ { 𝑚 ∈ ℕ ∣ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑚 } )
100 98 99 sselid ( ( 𝐴 ∈ ( 𝑇𝑅 ) ∧ 𝑘 ∈ { 𝑚 ∈ ℕ ∣ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑚 } ) → 𝑘 ∈ ℕ )
101 100 nncnd ( ( 𝐴 ∈ ( 𝑇𝑅 ) ∧ 𝑘 ∈ { 𝑚 ∈ ℕ ∣ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑚 } ) → 𝑘 ∈ ℂ )
102 97 101 mulcld ( ( 𝐴 ∈ ( 𝑇𝑅 ) ∧ 𝑘 ∈ { 𝑚 ∈ ℕ ∣ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑚 } ) → ( if ( ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑘 , 1 , 0 ) · 𝑘 ) ∈ ℂ )
103 simpr ( ( 𝐴 ∈ ( 𝑇𝑅 ) ∧ 𝑘 ∈ ( ( ( 𝐺𝐴 ) “ ℕ ) ∖ { 𝑚 ∈ ℕ ∣ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑚 } ) ) → 𝑘 ∈ ( ( ( 𝐺𝐴 ) “ ℕ ) ∖ { 𝑚 ∈ ℕ ∣ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑚 } ) )
104 103 eldifbd ( ( 𝐴 ∈ ( 𝑇𝑅 ) ∧ 𝑘 ∈ ( ( ( 𝐺𝐴 ) “ ℕ ) ∖ { 𝑚 ∈ ℕ ∣ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑚 } ) ) → ¬ 𝑘 ∈ { 𝑚 ∈ ℕ ∣ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑚 } )
105 23 ssdifssd ( 𝐴 ∈ ( 𝑇𝑅 ) → ( ( ( 𝐺𝐴 ) “ ℕ ) ∖ { 𝑚 ∈ ℕ ∣ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑚 } ) ⊆ ℕ )
106 105 sselda ( ( 𝐴 ∈ ( 𝑇𝑅 ) ∧ 𝑘 ∈ ( ( ( 𝐺𝐴 ) “ ℕ ) ∖ { 𝑚 ∈ ℕ ∣ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑚 } ) ) → 𝑘 ∈ ℕ )
107 31 notbii ( ¬ 𝑘 ∈ { 𝑚 ∈ ℕ ∣ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑚 } ↔ ¬ ( 𝑘 ∈ ℕ ∧ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑘 ) )
108 imnan ( ( 𝑘 ∈ ℕ → ¬ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑘 ) ↔ ¬ ( 𝑘 ∈ ℕ ∧ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑘 ) )
109 107 108 sylbb2 ( ¬ 𝑘 ∈ { 𝑚 ∈ ℕ ∣ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑚 } → ( 𝑘 ∈ ℕ → ¬ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑘 ) )
110 104 106 109 sylc ( ( 𝐴 ∈ ( 𝑇𝑅 ) ∧ 𝑘 ∈ ( ( ( 𝐺𝐴 ) “ ℕ ) ∖ { 𝑚 ∈ ℕ ∣ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑚 } ) ) → ¬ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑘 )
111 110 iffalsed ( ( 𝐴 ∈ ( 𝑇𝑅 ) ∧ 𝑘 ∈ ( ( ( 𝐺𝐴 ) “ ℕ ) ∖ { 𝑚 ∈ ℕ ∣ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑚 } ) ) → if ( ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑘 , 1 , 0 ) = 0 )
112 111 oveq1d ( ( 𝐴 ∈ ( 𝑇𝑅 ) ∧ 𝑘 ∈ ( ( ( 𝐺𝐴 ) “ ℕ ) ∖ { 𝑚 ∈ ℕ ∣ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑚 } ) ) → ( if ( ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑘 , 1 , 0 ) · 𝑘 ) = ( 0 · 𝑘 ) )
113 nnsscn ℕ ⊆ ℂ
114 105 113 sstrdi ( 𝐴 ∈ ( 𝑇𝑅 ) → ( ( ( 𝐺𝐴 ) “ ℕ ) ∖ { 𝑚 ∈ ℕ ∣ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑚 } ) ⊆ ℂ )
115 114 sselda ( ( 𝐴 ∈ ( 𝑇𝑅 ) ∧ 𝑘 ∈ ( ( ( 𝐺𝐴 ) “ ℕ ) ∖ { 𝑚 ∈ ℕ ∣ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑚 } ) ) → 𝑘 ∈ ℂ )
116 115 mul02d ( ( 𝐴 ∈ ( 𝑇𝑅 ) ∧ 𝑘 ∈ ( ( ( 𝐺𝐴 ) “ ℕ ) ∖ { 𝑚 ∈ ℕ ∣ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑚 } ) ) → ( 0 · 𝑘 ) = 0 )
117 112 116 eqtrd ( ( 𝐴 ∈ ( 𝑇𝑅 ) ∧ 𝑘 ∈ ( ( ( 𝐺𝐴 ) “ ℕ ) ∖ { 𝑚 ∈ ℕ ∣ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑚 } ) ) → ( if ( ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑘 , 1 , 0 ) · 𝑘 ) = 0 )
118 56 102 117 41 fsumss ( 𝐴 ∈ ( 𝑇𝑅 ) → Σ 𝑘 ∈ { 𝑚 ∈ ℕ ∣ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑚 } ( if ( ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑘 , 1 , 0 ) · 𝑘 ) = Σ 𝑘 ∈ ( ( 𝐺𝐴 ) “ ℕ ) ( if ( ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑘 , 1 , 0 ) · 𝑘 ) )
119 93 118 eqtr3d ( 𝐴 ∈ ( 𝑇𝑅 ) → Σ 𝑤 𝑡 ∈ ( ( 𝐴 “ ℕ ) ∩ 𝐽 ) ( { 𝑡 } × ( bits ‘ ( 𝐴𝑡 ) ) ) ( ( 2 ↑ ( 2nd𝑤 ) ) · ( 1st𝑤 ) ) = Σ 𝑘 ∈ ( ( 𝐺𝐴 ) “ ℕ ) ( if ( ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑘 , 1 , 0 ) · 𝑘 ) )
120 1 2 3 4 5 6 7 8 9 eulerpartlemt0 ( 𝐴 ∈ ( 𝑇𝑅 ) ↔ ( 𝐴 ∈ ( ℕ0m ℕ ) ∧ ( 𝐴 “ ℕ ) ∈ Fin ∧ ( 𝐴 “ ℕ ) ⊆ 𝐽 ) )
121 120 simp1bi ( 𝐴 ∈ ( 𝑇𝑅 ) → 𝐴 ∈ ( ℕ0m ℕ ) )
122 elmapi ( 𝐴 ∈ ( ℕ0m ℕ ) → 𝐴 : ℕ ⟶ ℕ0 )
123 121 122 syl ( 𝐴 ∈ ( 𝑇𝑅 ) → 𝐴 : ℕ ⟶ ℕ0 )
124 123 adantr ( ( 𝐴 ∈ ( 𝑇𝑅 ) ∧ 𝑡 ∈ ( ( 𝐴 “ ℕ ) ∩ 𝐽 ) ) → 𝐴 : ℕ ⟶ ℕ0 )
125 cnvimass ( 𝐴 “ ℕ ) ⊆ dom 𝐴
126 125 123 fssdm ( 𝐴 ∈ ( 𝑇𝑅 ) → ( 𝐴 “ ℕ ) ⊆ ℕ )
127 126 adantr ( ( 𝐴 ∈ ( 𝑇𝑅 ) ∧ 𝑡 ∈ ( ( 𝐴 “ ℕ ) ∩ 𝐽 ) ) → ( 𝐴 “ ℕ ) ⊆ ℕ )
128 inss1 ( ( 𝐴 “ ℕ ) ∩ 𝐽 ) ⊆ ( 𝐴 “ ℕ )
129 128 78 sselid ( ( 𝐴 ∈ ( 𝑇𝑅 ) ∧ 𝑡 ∈ ( ( 𝐴 “ ℕ ) ∩ 𝐽 ) ) → 𝑡 ∈ ( 𝐴 “ ℕ ) )
130 127 129 sseldd ( ( 𝐴 ∈ ( 𝑇𝑅 ) ∧ 𝑡 ∈ ( ( 𝐴 “ ℕ ) ∩ 𝐽 ) ) → 𝑡 ∈ ℕ )
131 124 130 ffvelrnd ( ( 𝐴 ∈ ( 𝑇𝑅 ) ∧ 𝑡 ∈ ( ( 𝐴 “ ℕ ) ∩ 𝐽 ) ) → ( 𝐴𝑡 ) ∈ ℕ0 )
132 bitsfi ( ( 𝐴𝑡 ) ∈ ℕ0 → ( bits ‘ ( 𝐴𝑡 ) ) ∈ Fin )
133 131 132 syl ( ( 𝐴 ∈ ( 𝑇𝑅 ) ∧ 𝑡 ∈ ( ( 𝐴 “ ℕ ) ∩ 𝐽 ) ) → ( bits ‘ ( 𝐴𝑡 ) ) ∈ Fin )
134 130 nncnd ( ( 𝐴 ∈ ( 𝑇𝑅 ) ∧ 𝑡 ∈ ( ( 𝐴 “ ℕ ) ∩ 𝐽 ) ) → 𝑡 ∈ ℂ )
135 2cnd ( ( 𝐴 ∈ ( 𝑇𝑅 ) ∧ ( 𝑡 ∈ ( ( 𝐴 “ ℕ ) ∩ 𝐽 ) ∧ 𝑛 ∈ ( bits ‘ ( 𝐴𝑡 ) ) ) ) → 2 ∈ ℂ )
136 simprr ( ( 𝐴 ∈ ( 𝑇𝑅 ) ∧ ( 𝑡 ∈ ( ( 𝐴 “ ℕ ) ∩ 𝐽 ) ∧ 𝑛 ∈ ( bits ‘ ( 𝐴𝑡 ) ) ) ) → 𝑛 ∈ ( bits ‘ ( 𝐴𝑡 ) ) )
137 81 136 sselid ( ( 𝐴 ∈ ( 𝑇𝑅 ) ∧ ( 𝑡 ∈ ( ( 𝐴 “ ℕ ) ∩ 𝐽 ) ∧ 𝑛 ∈ ( bits ‘ ( 𝐴𝑡 ) ) ) ) → 𝑛 ∈ ℕ0 )
138 135 137 expcld ( ( 𝐴 ∈ ( 𝑇𝑅 ) ∧ ( 𝑡 ∈ ( ( 𝐴 “ ℕ ) ∩ 𝐽 ) ∧ 𝑛 ∈ ( bits ‘ ( 𝐴𝑡 ) ) ) ) → ( 2 ↑ 𝑛 ) ∈ ℂ )
139 138 anassrs ( ( ( 𝐴 ∈ ( 𝑇𝑅 ) ∧ 𝑡 ∈ ( ( 𝐴 “ ℕ ) ∩ 𝐽 ) ) ∧ 𝑛 ∈ ( bits ‘ ( 𝐴𝑡 ) ) ) → ( 2 ↑ 𝑛 ) ∈ ℂ )
140 133 134 139 fsummulc1 ( ( 𝐴 ∈ ( 𝑇𝑅 ) ∧ 𝑡 ∈ ( ( 𝐴 “ ℕ ) ∩ 𝐽 ) ) → ( Σ 𝑛 ∈ ( bits ‘ ( 𝐴𝑡 ) ) ( 2 ↑ 𝑛 ) · 𝑡 ) = Σ 𝑛 ∈ ( bits ‘ ( 𝐴𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) )
141 140 sumeq2dv ( 𝐴 ∈ ( 𝑇𝑅 ) → Σ 𝑡 ∈ ( ( 𝐴 “ ℕ ) ∩ 𝐽 ) ( Σ 𝑛 ∈ ( bits ‘ ( 𝐴𝑡 ) ) ( 2 ↑ 𝑛 ) · 𝑡 ) = Σ 𝑡 ∈ ( ( 𝐴 “ ℕ ) ∩ 𝐽 ) Σ 𝑛 ∈ ( bits ‘ ( 𝐴𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) )
142 bitsinv1 ( ( 𝐴𝑡 ) ∈ ℕ0 → Σ 𝑛 ∈ ( bits ‘ ( 𝐴𝑡 ) ) ( 2 ↑ 𝑛 ) = ( 𝐴𝑡 ) )
143 142 oveq1d ( ( 𝐴𝑡 ) ∈ ℕ0 → ( Σ 𝑛 ∈ ( bits ‘ ( 𝐴𝑡 ) ) ( 2 ↑ 𝑛 ) · 𝑡 ) = ( ( 𝐴𝑡 ) · 𝑡 ) )
144 131 143 syl ( ( 𝐴 ∈ ( 𝑇𝑅 ) ∧ 𝑡 ∈ ( ( 𝐴 “ ℕ ) ∩ 𝐽 ) ) → ( Σ 𝑛 ∈ ( bits ‘ ( 𝐴𝑡 ) ) ( 2 ↑ 𝑛 ) · 𝑡 ) = ( ( 𝐴𝑡 ) · 𝑡 ) )
145 144 sumeq2dv ( 𝐴 ∈ ( 𝑇𝑅 ) → Σ 𝑡 ∈ ( ( 𝐴 “ ℕ ) ∩ 𝐽 ) ( Σ 𝑛 ∈ ( bits ‘ ( 𝐴𝑡 ) ) ( 2 ↑ 𝑛 ) · 𝑡 ) = Σ 𝑡 ∈ ( ( 𝐴 “ ℕ ) ∩ 𝐽 ) ( ( 𝐴𝑡 ) · 𝑡 ) )
146 vex 𝑡 ∈ V
147 vex 𝑛 ∈ V
148 146 147 op2ndd ( 𝑤 = ⟨ 𝑡 , 𝑛 ⟩ → ( 2nd𝑤 ) = 𝑛 )
149 148 oveq2d ( 𝑤 = ⟨ 𝑡 , 𝑛 ⟩ → ( 2 ↑ ( 2nd𝑤 ) ) = ( 2 ↑ 𝑛 ) )
150 146 147 op1std ( 𝑤 = ⟨ 𝑡 , 𝑛 ⟩ → ( 1st𝑤 ) = 𝑡 )
151 149 150 oveq12d ( 𝑤 = ⟨ 𝑡 , 𝑛 ⟩ → ( ( 2 ↑ ( 2nd𝑤 ) ) · ( 1st𝑤 ) ) = ( ( 2 ↑ 𝑛 ) · 𝑡 ) )
152 inss2 ( 𝑇𝑅 ) ⊆ 𝑅
153 152 sseli ( 𝐴 ∈ ( 𝑇𝑅 ) → 𝐴𝑅 )
154 cnveq ( 𝑓 = 𝐴 𝑓 = 𝐴 )
155 154 imaeq1d ( 𝑓 = 𝐴 → ( 𝑓 “ ℕ ) = ( 𝐴 “ ℕ ) )
156 155 eleq1d ( 𝑓 = 𝐴 → ( ( 𝑓 “ ℕ ) ∈ Fin ↔ ( 𝐴 “ ℕ ) ∈ Fin ) )
157 156 8 elab2g ( 𝐴 ∈ ( 𝑇𝑅 ) → ( 𝐴𝑅 ↔ ( 𝐴 “ ℕ ) ∈ Fin ) )
158 153 157 mpbid ( 𝐴 ∈ ( 𝑇𝑅 ) → ( 𝐴 “ ℕ ) ∈ Fin )
159 ssfi ( ( ( 𝐴 “ ℕ ) ∈ Fin ∧ ( ( 𝐴 “ ℕ ) ∩ 𝐽 ) ⊆ ( 𝐴 “ ℕ ) ) → ( ( 𝐴 “ ℕ ) ∩ 𝐽 ) ∈ Fin )
160 158 128 159 sylancl ( 𝐴 ∈ ( 𝑇𝑅 ) → ( ( 𝐴 “ ℕ ) ∩ 𝐽 ) ∈ Fin )
161 134 adantrr ( ( 𝐴 ∈ ( 𝑇𝑅 ) ∧ ( 𝑡 ∈ ( ( 𝐴 “ ℕ ) ∩ 𝐽 ) ∧ 𝑛 ∈ ( bits ‘ ( 𝐴𝑡 ) ) ) ) → 𝑡 ∈ ℂ )
162 138 161 mulcld ( ( 𝐴 ∈ ( 𝑇𝑅 ) ∧ ( 𝑡 ∈ ( ( 𝐴 “ ℕ ) ∩ 𝐽 ) ∧ 𝑛 ∈ ( bits ‘ ( 𝐴𝑡 ) ) ) ) → ( ( 2 ↑ 𝑛 ) · 𝑡 ) ∈ ℂ )
163 151 160 133 162 fsum2d ( 𝐴 ∈ ( 𝑇𝑅 ) → Σ 𝑡 ∈ ( ( 𝐴 “ ℕ ) ∩ 𝐽 ) Σ 𝑛 ∈ ( bits ‘ ( 𝐴𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = Σ 𝑤 𝑡 ∈ ( ( 𝐴 “ ℕ ) ∩ 𝐽 ) ( { 𝑡 } × ( bits ‘ ( 𝐴𝑡 ) ) ) ( ( 2 ↑ ( 2nd𝑤 ) ) · ( 1st𝑤 ) ) )
164 141 145 163 3eqtr3d ( 𝐴 ∈ ( 𝑇𝑅 ) → Σ 𝑡 ∈ ( ( 𝐴 “ ℕ ) ∩ 𝐽 ) ( ( 𝐴𝑡 ) · 𝑡 ) = Σ 𝑤 𝑡 ∈ ( ( 𝐴 “ ℕ ) ∩ 𝐽 ) ( { 𝑡 } × ( bits ‘ ( 𝐴𝑡 ) ) ) ( ( 2 ↑ ( 2nd𝑤 ) ) · ( 1st𝑤 ) ) )
165 inss1 ( 𝑇𝑅 ) ⊆ 𝑇
166 165 sseli ( 𝐴 ∈ ( 𝑇𝑅 ) → 𝐴𝑇 )
167 155 sseq1d ( 𝑓 = 𝐴 → ( ( 𝑓 “ ℕ ) ⊆ 𝐽 ↔ ( 𝐴 “ ℕ ) ⊆ 𝐽 ) )
168 167 9 elrab2 ( 𝐴𝑇 ↔ ( 𝐴 ∈ ( ℕ0m ℕ ) ∧ ( 𝐴 “ ℕ ) ⊆ 𝐽 ) )
169 168 simprbi ( 𝐴𝑇 → ( 𝐴 “ ℕ ) ⊆ 𝐽 )
170 166 169 syl ( 𝐴 ∈ ( 𝑇𝑅 ) → ( 𝐴 “ ℕ ) ⊆ 𝐽 )
171 df-ss ( ( 𝐴 “ ℕ ) ⊆ 𝐽 ↔ ( ( 𝐴 “ ℕ ) ∩ 𝐽 ) = ( 𝐴 “ ℕ ) )
172 170 171 sylib ( 𝐴 ∈ ( 𝑇𝑅 ) → ( ( 𝐴 “ ℕ ) ∩ 𝐽 ) = ( 𝐴 “ ℕ ) )
173 172 sumeq1d ( 𝐴 ∈ ( 𝑇𝑅 ) → Σ 𝑡 ∈ ( ( 𝐴 “ ℕ ) ∩ 𝐽 ) ( ( 𝐴𝑡 ) · 𝑡 ) = Σ 𝑡 ∈ ( 𝐴 “ ℕ ) ( ( 𝐴𝑡 ) · 𝑡 ) )
174 164 173 eqtr3d ( 𝐴 ∈ ( 𝑇𝑅 ) → Σ 𝑤 𝑡 ∈ ( ( 𝐴 “ ℕ ) ∩ 𝐽 ) ( { 𝑡 } × ( bits ‘ ( 𝐴𝑡 ) ) ) ( ( 2 ↑ ( 2nd𝑤 ) ) · ( 1st𝑤 ) ) = Σ 𝑡 ∈ ( 𝐴 “ ℕ ) ( ( 𝐴𝑡 ) · 𝑡 ) )
175 28 119 174 3eqtr2d ( 𝐴 ∈ ( 𝑇𝑅 ) → Σ 𝑘 ∈ ( ( 𝐺𝐴 ) “ ℕ ) ( ( ( 𝐺𝐴 ) ‘ 𝑘 ) · 𝑘 ) = Σ 𝑡 ∈ ( 𝐴 “ ℕ ) ( ( 𝐴𝑡 ) · 𝑡 ) )
176 fveq2 ( 𝑘 = 𝑡 → ( 𝐴𝑘 ) = ( 𝐴𝑡 ) )
177 id ( 𝑘 = 𝑡𝑘 = 𝑡 )
178 176 177 oveq12d ( 𝑘 = 𝑡 → ( ( 𝐴𝑘 ) · 𝑘 ) = ( ( 𝐴𝑡 ) · 𝑡 ) )
179 178 cbvsumv Σ 𝑘 ∈ ( 𝐴 “ ℕ ) ( ( 𝐴𝑘 ) · 𝑘 ) = Σ 𝑡 ∈ ( 𝐴 “ ℕ ) ( ( 𝐴𝑡 ) · 𝑡 )
180 175 179 eqtr4di ( 𝐴 ∈ ( 𝑇𝑅 ) → Σ 𝑘 ∈ ( ( 𝐺𝐴 ) “ ℕ ) ( ( ( 𝐺𝐴 ) ‘ 𝑘 ) · 𝑘 ) = Σ 𝑘 ∈ ( 𝐴 “ ℕ ) ( ( 𝐴𝑘 ) · 𝑘 ) )
181 0nn0 0 ∈ ℕ0
182 1nn0 1 ∈ ℕ0
183 prssi ( ( 0 ∈ ℕ0 ∧ 1 ∈ ℕ0 ) → { 0 , 1 } ⊆ ℕ0 )
184 181 182 183 mp2an { 0 , 1 } ⊆ ℕ0
185 fss ( ( ( 𝐺𝐴 ) : ℕ ⟶ { 0 , 1 } ∧ { 0 , 1 } ⊆ ℕ0 ) → ( 𝐺𝐴 ) : ℕ ⟶ ℕ0 )
186 184 185 mpan2 ( ( 𝐺𝐴 ) : ℕ ⟶ { 0 , 1 } → ( 𝐺𝐴 ) : ℕ ⟶ ℕ0 )
187 nn0ex 0 ∈ V
188 nnex ℕ ∈ V
189 187 188 elmap ( ( 𝐺𝐴 ) ∈ ( ℕ0m ℕ ) ↔ ( 𝐺𝐴 ) : ℕ ⟶ ℕ0 )
190 189 biimpri ( ( 𝐺𝐴 ) : ℕ ⟶ ℕ0 → ( 𝐺𝐴 ) ∈ ( ℕ0m ℕ ) )
191 20 186 190 3syl ( ( 𝐺𝐴 ) ∈ ( { 0 , 1 } ↑m ℕ ) → ( 𝐺𝐴 ) ∈ ( ℕ0m ℕ ) )
192 191 anim1i ( ( ( 𝐺𝐴 ) ∈ ( { 0 , 1 } ↑m ℕ ) ∧ ( 𝐺𝐴 ) ∈ 𝑅 ) → ( ( 𝐺𝐴 ) ∈ ( ℕ0m ℕ ) ∧ ( 𝐺𝐴 ) ∈ 𝑅 ) )
193 elin ( ( 𝐺𝐴 ) ∈ ( ( ℕ0m ℕ ) ∩ 𝑅 ) ↔ ( ( 𝐺𝐴 ) ∈ ( ℕ0m ℕ ) ∧ ( 𝐺𝐴 ) ∈ 𝑅 ) )
194 192 17 193 3imtr4i ( ( 𝐺𝐴 ) ∈ ( ( { 0 , 1 } ↑m ℕ ) ∩ 𝑅 ) → ( 𝐺𝐴 ) ∈ ( ( ℕ0m ℕ ) ∩ 𝑅 ) )
195 8 11 eulerpartlemsv2 ( ( 𝐺𝐴 ) ∈ ( ( ℕ0m ℕ ) ∩ 𝑅 ) → ( 𝑆 ‘ ( 𝐺𝐴 ) ) = Σ 𝑘 ∈ ( ( 𝐺𝐴 ) “ ℕ ) ( ( ( 𝐺𝐴 ) ‘ 𝑘 ) · 𝑘 ) )
196 16 194 195 3syl ( 𝐴 ∈ ( 𝑇𝑅 ) → ( 𝑆 ‘ ( 𝐺𝐴 ) ) = Σ 𝑘 ∈ ( ( 𝐺𝐴 ) “ ℕ ) ( ( ( 𝐺𝐴 ) ‘ 𝑘 ) · 𝑘 ) )
197 121 153 elind ( 𝐴 ∈ ( 𝑇𝑅 ) → 𝐴 ∈ ( ( ℕ0m ℕ ) ∩ 𝑅 ) )
198 8 11 eulerpartlemsv2 ( 𝐴 ∈ ( ( ℕ0m ℕ ) ∩ 𝑅 ) → ( 𝑆𝐴 ) = Σ 𝑘 ∈ ( 𝐴 “ ℕ ) ( ( 𝐴𝑘 ) · 𝑘 ) )
199 197 198 syl ( 𝐴 ∈ ( 𝑇𝑅 ) → ( 𝑆𝐴 ) = Σ 𝑘 ∈ ( 𝐴 “ ℕ ) ( ( 𝐴𝑘 ) · 𝑘 ) )
200 180 196 199 3eqtr4d ( 𝐴 ∈ ( 𝑇𝑅 ) → ( 𝑆 ‘ ( 𝐺𝐴 ) ) = ( 𝑆𝐴 ) )