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 ffvelcdmi ( 𝐴 ∈ ( 𝑇𝑅 ) → ( 𝐺𝐴 ) ∈ ( ( { 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 mullidd ( 𝑘 ∈ { 𝑚 ∈ ℕ ∣ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( 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 ffn ( ( 𝐺𝐴 ) : ℕ ⟶ { 0 , 1 } → ( 𝐺𝐴 ) Fn ℕ )
50 elpreima ( ( 𝐺𝐴 ) Fn ℕ → ( 𝑘 ∈ ( ( 𝐺𝐴 ) “ ℕ ) ↔ ( 𝑘 ∈ ℕ ∧ ( ( 𝐺𝐴 ) ‘ 𝑘 ) ∈ ℕ ) ) )
51 19 20 49 50 4syl ( 𝐴 ∈ ( 𝑇𝑅 ) → ( 𝑘 ∈ ( ( 𝐺𝐴 ) “ ℕ ) ↔ ( 𝑘 ∈ ℕ ∧ ( ( 𝐺𝐴 ) ‘ 𝑘 ) ∈ ℕ ) ) )
52 51 adantr ( ( 𝐴 ∈ ( 𝑇𝑅 ) ∧ 𝑘 ∈ { 𝑚 ∈ ℕ ∣ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑚 } ) → ( 𝑘 ∈ ( ( 𝐺𝐴 ) “ ℕ ) ↔ ( 𝑘 ∈ ℕ ∧ ( ( 𝐺𝐴 ) ‘ 𝑘 ) ∈ ℕ ) ) )
53 42 48 52 mpbir2and ( ( 𝐴 ∈ ( 𝑇𝑅 ) ∧ 𝑘 ∈ { 𝑚 ∈ ℕ ∣ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑚 } ) → 𝑘 ∈ ( ( 𝐺𝐴 ) “ ℕ ) )
54 53 ex ( 𝐴 ∈ ( 𝑇𝑅 ) → ( 𝑘 ∈ { 𝑚 ∈ ℕ ∣ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑚 } → 𝑘 ∈ ( ( 𝐺𝐴 ) “ ℕ ) ) )
55 54 ssrdv ( 𝐴 ∈ ( 𝑇𝑅 ) → { 𝑚 ∈ ℕ ∣ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑚 } ⊆ ( ( 𝐺𝐴 ) “ ℕ ) )
56 ssfi ( ( ( ( 𝐺𝐴 ) “ ℕ ) ∈ Fin ∧ { 𝑚 ∈ ℕ ∣ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑚 } ⊆ ( ( 𝐺𝐴 ) “ ℕ ) ) → { 𝑚 ∈ ℕ ∣ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑚 } ∈ Fin )
57 41 55 56 syl2anc ( 𝐴 ∈ ( 𝑇𝑅 ) → { 𝑚 ∈ ℕ ∣ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑚 } ∈ Fin )
58 cnvexg ( 𝐴 ∈ ( 𝑇𝑅 ) → 𝐴 ∈ V )
59 imaexg ( 𝐴 ∈ V → ( 𝐴 “ ℕ ) ∈ V )
60 inex1g ( ( 𝐴 “ ℕ ) ∈ V → ( ( 𝐴 “ ℕ ) ∩ 𝐽 ) ∈ V )
61 58 59 60 3syl ( 𝐴 ∈ ( 𝑇𝑅 ) → ( ( 𝐴 “ ℕ ) ∩ 𝐽 ) ∈ V )
62 vsnex { 𝑡 } ∈ V
63 fvex ( bits ‘ ( 𝐴𝑡 ) ) ∈ V
64 62 63 xpex ( { 𝑡 } × ( bits ‘ ( 𝐴𝑡 ) ) ) ∈ V
65 64 rgenw 𝑡 ∈ ( ( 𝐴 “ ℕ ) ∩ 𝐽 ) ( { 𝑡 } × ( bits ‘ ( 𝐴𝑡 ) ) ) ∈ V
66 iunexg ( ( ( ( 𝐴 “ ℕ ) ∩ 𝐽 ) ∈ V ∧ ∀ 𝑡 ∈ ( ( 𝐴 “ ℕ ) ∩ 𝐽 ) ( { 𝑡 } × ( bits ‘ ( 𝐴𝑡 ) ) ) ∈ V ) → 𝑡 ∈ ( ( 𝐴 “ ℕ ) ∩ 𝐽 ) ( { 𝑡 } × ( bits ‘ ( 𝐴𝑡 ) ) ) ∈ V )
67 61 65 66 sylancl ( 𝐴 ∈ ( 𝑇𝑅 ) → 𝑡 ∈ ( ( 𝐴 “ ℕ ) ∩ 𝐽 ) ( { 𝑡 } × ( bits ‘ ( 𝐴𝑡 ) ) ) ∈ V )
68 eqid 𝑡 ∈ ( ( 𝐴 “ ℕ ) ∩ 𝐽 ) ( { 𝑡 } × ( bits ‘ ( 𝐴𝑡 ) ) ) = 𝑡 ∈ ( ( 𝐴 “ ℕ ) ∩ 𝐽 ) ( { 𝑡 } × ( bits ‘ ( 𝐴𝑡 ) ) )
69 1 2 3 4 5 6 7 8 9 10 68 eulerpartlemgh ( 𝐴 ∈ ( 𝑇𝑅 ) → ( 𝐹 𝑡 ∈ ( ( 𝐴 “ ℕ ) ∩ 𝐽 ) ( { 𝑡 } × ( bits ‘ ( 𝐴𝑡 ) ) ) ) : 𝑡 ∈ ( ( 𝐴 “ ℕ ) ∩ 𝐽 ) ( { 𝑡 } × ( bits ‘ ( 𝐴𝑡 ) ) ) –1-1-onto→ { 𝑚 ∈ ℕ ∣ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑚 } )
70 f1oeng ( ( 𝑡 ∈ ( ( 𝐴 “ ℕ ) ∩ 𝐽 ) ( { 𝑡 } × ( bits ‘ ( 𝐴𝑡 ) ) ) ∈ V ∧ ( 𝐹 𝑡 ∈ ( ( 𝐴 “ ℕ ) ∩ 𝐽 ) ( { 𝑡 } × ( bits ‘ ( 𝐴𝑡 ) ) ) ) : 𝑡 ∈ ( ( 𝐴 “ ℕ ) ∩ 𝐽 ) ( { 𝑡 } × ( bits ‘ ( 𝐴𝑡 ) ) ) –1-1-onto→ { 𝑚 ∈ ℕ ∣ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑚 } ) → 𝑡 ∈ ( ( 𝐴 “ ℕ ) ∩ 𝐽 ) ( { 𝑡 } × ( bits ‘ ( 𝐴𝑡 ) ) ) ≈ { 𝑚 ∈ ℕ ∣ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑚 } )
71 67 69 70 syl2anc ( 𝐴 ∈ ( 𝑇𝑅 ) → 𝑡 ∈ ( ( 𝐴 “ ℕ ) ∩ 𝐽 ) ( { 𝑡 } × ( bits ‘ ( 𝐴𝑡 ) ) ) ≈ { 𝑚 ∈ ℕ ∣ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑚 } )
72 enfii ( ( { 𝑚 ∈ ℕ ∣ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑚 } ∈ Fin ∧ 𝑡 ∈ ( ( 𝐴 “ ℕ ) ∩ 𝐽 ) ( { 𝑡 } × ( bits ‘ ( 𝐴𝑡 ) ) ) ≈ { 𝑚 ∈ ℕ ∣ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑚 } ) → 𝑡 ∈ ( ( 𝐴 “ ℕ ) ∩ 𝐽 ) ( { 𝑡 } × ( bits ‘ ( 𝐴𝑡 ) ) ) ∈ Fin )
73 57 71 72 syl2anc ( 𝐴 ∈ ( 𝑇𝑅 ) → 𝑡 ∈ ( ( 𝐴 “ ℕ ) ∩ 𝐽 ) ( { 𝑡 } × ( bits ‘ ( 𝐴𝑡 ) ) ) ∈ Fin )
74 fvres ( 𝑤 𝑡 ∈ ( ( 𝐴 “ ℕ ) ∩ 𝐽 ) ( { 𝑡 } × ( bits ‘ ( 𝐴𝑡 ) ) ) → ( ( 𝐹 𝑡 ∈ ( ( 𝐴 “ ℕ ) ∩ 𝐽 ) ( { 𝑡 } × ( bits ‘ ( 𝐴𝑡 ) ) ) ) ‘ 𝑤 ) = ( 𝐹𝑤 ) )
75 74 adantl ( ( 𝐴 ∈ ( 𝑇𝑅 ) ∧ 𝑤 𝑡 ∈ ( ( 𝐴 “ ℕ ) ∩ 𝐽 ) ( { 𝑡 } × ( bits ‘ ( 𝐴𝑡 ) ) ) ) → ( ( 𝐹 𝑡 ∈ ( ( 𝐴 “ ℕ ) ∩ 𝐽 ) ( { 𝑡 } × ( bits ‘ ( 𝐴𝑡 ) ) ) ) ‘ 𝑤 ) = ( 𝐹𝑤 ) )
76 inss2 ( ( 𝐴 “ ℕ ) ∩ 𝐽 ) ⊆ 𝐽
77 simpr ( ( 𝐴 ∈ ( 𝑇𝑅 ) ∧ 𝑡 ∈ ( ( 𝐴 “ ℕ ) ∩ 𝐽 ) ) → 𝑡 ∈ ( ( 𝐴 “ ℕ ) ∩ 𝐽 ) )
78 76 77 sselid ( ( 𝐴 ∈ ( 𝑇𝑅 ) ∧ 𝑡 ∈ ( ( 𝐴 “ ℕ ) ∩ 𝐽 ) ) → 𝑡𝐽 )
79 78 snssd ( ( 𝐴 ∈ ( 𝑇𝑅 ) ∧ 𝑡 ∈ ( ( 𝐴 “ ℕ ) ∩ 𝐽 ) ) → { 𝑡 } ⊆ 𝐽 )
80 bitsss ( bits ‘ ( 𝐴𝑡 ) ) ⊆ ℕ0
81 xpss12 ( ( { 𝑡 } ⊆ 𝐽 ∧ ( bits ‘ ( 𝐴𝑡 ) ) ⊆ ℕ0 ) → ( { 𝑡 } × ( bits ‘ ( 𝐴𝑡 ) ) ) ⊆ ( 𝐽 × ℕ0 ) )
82 79 80 81 sylancl ( ( 𝐴 ∈ ( 𝑇𝑅 ) ∧ 𝑡 ∈ ( ( 𝐴 “ ℕ ) ∩ 𝐽 ) ) → ( { 𝑡 } × ( bits ‘ ( 𝐴𝑡 ) ) ) ⊆ ( 𝐽 × ℕ0 ) )
83 82 ralrimiva ( 𝐴 ∈ ( 𝑇𝑅 ) → ∀ 𝑡 ∈ ( ( 𝐴 “ ℕ ) ∩ 𝐽 ) ( { 𝑡 } × ( bits ‘ ( 𝐴𝑡 ) ) ) ⊆ ( 𝐽 × ℕ0 ) )
84 iunss ( 𝑡 ∈ ( ( 𝐴 “ ℕ ) ∩ 𝐽 ) ( { 𝑡 } × ( bits ‘ ( 𝐴𝑡 ) ) ) ⊆ ( 𝐽 × ℕ0 ) ↔ ∀ 𝑡 ∈ ( ( 𝐴 “ ℕ ) ∩ 𝐽 ) ( { 𝑡 } × ( bits ‘ ( 𝐴𝑡 ) ) ) ⊆ ( 𝐽 × ℕ0 ) )
85 83 84 sylibr ( 𝐴 ∈ ( 𝑇𝑅 ) → 𝑡 ∈ ( ( 𝐴 “ ℕ ) ∩ 𝐽 ) ( { 𝑡 } × ( bits ‘ ( 𝐴𝑡 ) ) ) ⊆ ( 𝐽 × ℕ0 ) )
86 85 sselda ( ( 𝐴 ∈ ( 𝑇𝑅 ) ∧ 𝑤 𝑡 ∈ ( ( 𝐴 “ ℕ ) ∩ 𝐽 ) ( { 𝑡 } × ( bits ‘ ( 𝐴𝑡 ) ) ) ) → 𝑤 ∈ ( 𝐽 × ℕ0 ) )
87 4 5 oddpwdcv ( 𝑤 ∈ ( 𝐽 × ℕ0 ) → ( 𝐹𝑤 ) = ( ( 2 ↑ ( 2nd𝑤 ) ) · ( 1st𝑤 ) ) )
88 86 87 syl ( ( 𝐴 ∈ ( 𝑇𝑅 ) ∧ 𝑤 𝑡 ∈ ( ( 𝐴 “ ℕ ) ∩ 𝐽 ) ( { 𝑡 } × ( bits ‘ ( 𝐴𝑡 ) ) ) ) → ( 𝐹𝑤 ) = ( ( 2 ↑ ( 2nd𝑤 ) ) · ( 1st𝑤 ) ) )
89 75 88 eqtrd ( ( 𝐴 ∈ ( 𝑇𝑅 ) ∧ 𝑤 𝑡 ∈ ( ( 𝐴 “ ℕ ) ∩ 𝐽 ) ( { 𝑡 } × ( bits ‘ ( 𝐴𝑡 ) ) ) ) → ( ( 𝐹 𝑡 ∈ ( ( 𝐴 “ ℕ ) ∩ 𝐽 ) ( { 𝑡 } × ( bits ‘ ( 𝐴𝑡 ) ) ) ) ‘ 𝑤 ) = ( ( 2 ↑ ( 2nd𝑤 ) ) · ( 1st𝑤 ) ) )
90 42 nncnd ( ( 𝐴 ∈ ( 𝑇𝑅 ) ∧ 𝑘 ∈ { 𝑚 ∈ ℕ ∣ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑚 } ) → 𝑘 ∈ ℂ )
91 40 73 69 89 90 fsumf1o ( 𝐴 ∈ ( 𝑇𝑅 ) → Σ 𝑘 ∈ { 𝑚 ∈ ℕ ∣ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑚 } 𝑘 = Σ 𝑤 𝑡 ∈ ( ( 𝐴 “ ℕ ) ∩ 𝐽 ) ( { 𝑡 } × ( bits ‘ ( 𝐴𝑡 ) ) ) ( ( 2 ↑ ( 2nd𝑤 ) ) · ( 1st𝑤 ) ) )
92 39 91 eqtrid ( 𝐴 ∈ ( 𝑇𝑅 ) → Σ 𝑘 ∈ { 𝑚 ∈ ℕ ∣ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑚 } ( if ( ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑘 , 1 , 0 ) · 𝑘 ) = Σ 𝑤 𝑡 ∈ ( ( 𝐴 “ ℕ ) ∩ 𝐽 ) ( { 𝑡 } × ( bits ‘ ( 𝐴𝑡 ) ) ) ( ( 2 ↑ ( 2nd𝑤 ) ) · ( 1st𝑤 ) ) )
93 ax-1cn 1 ∈ ℂ
94 0cn 0 ∈ ℂ
95 93 94 ifcli if ( ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑘 , 1 , 0 ) ∈ ℂ
96 95 a1i ( ( 𝐴 ∈ ( 𝑇𝑅 ) ∧ 𝑘 ∈ { 𝑚 ∈ ℕ ∣ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑚 } ) → if ( ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑘 , 1 , 0 ) ∈ ℂ )
97 ssrab2 { 𝑚 ∈ ℕ ∣ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑚 } ⊆ ℕ
98 simpr ( ( 𝐴 ∈ ( 𝑇𝑅 ) ∧ 𝑘 ∈ { 𝑚 ∈ ℕ ∣ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑚 } ) → 𝑘 ∈ { 𝑚 ∈ ℕ ∣ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑚 } )
99 97 98 sselid ( ( 𝐴 ∈ ( 𝑇𝑅 ) ∧ 𝑘 ∈ { 𝑚 ∈ ℕ ∣ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑚 } ) → 𝑘 ∈ ℕ )
100 99 nncnd ( ( 𝐴 ∈ ( 𝑇𝑅 ) ∧ 𝑘 ∈ { 𝑚 ∈ ℕ ∣ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑚 } ) → 𝑘 ∈ ℂ )
101 96 100 mulcld ( ( 𝐴 ∈ ( 𝑇𝑅 ) ∧ 𝑘 ∈ { 𝑚 ∈ ℕ ∣ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑚 } ) → ( if ( ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑘 , 1 , 0 ) · 𝑘 ) ∈ ℂ )
102 simpr ( ( 𝐴 ∈ ( 𝑇𝑅 ) ∧ 𝑘 ∈ ( ( ( 𝐺𝐴 ) “ ℕ ) ∖ { 𝑚 ∈ ℕ ∣ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑚 } ) ) → 𝑘 ∈ ( ( ( 𝐺𝐴 ) “ ℕ ) ∖ { 𝑚 ∈ ℕ ∣ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑚 } ) )
103 102 eldifbd ( ( 𝐴 ∈ ( 𝑇𝑅 ) ∧ 𝑘 ∈ ( ( ( 𝐺𝐴 ) “ ℕ ) ∖ { 𝑚 ∈ ℕ ∣ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑚 } ) ) → ¬ 𝑘 ∈ { 𝑚 ∈ ℕ ∣ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑚 } )
104 23 ssdifssd ( 𝐴 ∈ ( 𝑇𝑅 ) → ( ( ( 𝐺𝐴 ) “ ℕ ) ∖ { 𝑚 ∈ ℕ ∣ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑚 } ) ⊆ ℕ )
105 104 sselda ( ( 𝐴 ∈ ( 𝑇𝑅 ) ∧ 𝑘 ∈ ( ( ( 𝐺𝐴 ) “ ℕ ) ∖ { 𝑚 ∈ ℕ ∣ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑚 } ) ) → 𝑘 ∈ ℕ )
106 31 notbii ( ¬ 𝑘 ∈ { 𝑚 ∈ ℕ ∣ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑚 } ↔ ¬ ( 𝑘 ∈ ℕ ∧ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑘 ) )
107 imnan ( ( 𝑘 ∈ ℕ → ¬ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑘 ) ↔ ¬ ( 𝑘 ∈ ℕ ∧ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑘 ) )
108 106 107 sylbb2 ( ¬ 𝑘 ∈ { 𝑚 ∈ ℕ ∣ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑚 } → ( 𝑘 ∈ ℕ → ¬ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑘 ) )
109 103 105 108 sylc ( ( 𝐴 ∈ ( 𝑇𝑅 ) ∧ 𝑘 ∈ ( ( ( 𝐺𝐴 ) “ ℕ ) ∖ { 𝑚 ∈ ℕ ∣ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑚 } ) ) → ¬ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑘 )
110 109 iffalsed ( ( 𝐴 ∈ ( 𝑇𝑅 ) ∧ 𝑘 ∈ ( ( ( 𝐺𝐴 ) “ ℕ ) ∖ { 𝑚 ∈ ℕ ∣ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑚 } ) ) → if ( ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑘 , 1 , 0 ) = 0 )
111 110 oveq1d ( ( 𝐴 ∈ ( 𝑇𝑅 ) ∧ 𝑘 ∈ ( ( ( 𝐺𝐴 ) “ ℕ ) ∖ { 𝑚 ∈ ℕ ∣ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑚 } ) ) → ( if ( ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑘 , 1 , 0 ) · 𝑘 ) = ( 0 · 𝑘 ) )
112 nnsscn ℕ ⊆ ℂ
113 104 112 sstrdi ( 𝐴 ∈ ( 𝑇𝑅 ) → ( ( ( 𝐺𝐴 ) “ ℕ ) ∖ { 𝑚 ∈ ℕ ∣ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑚 } ) ⊆ ℂ )
114 113 sselda ( ( 𝐴 ∈ ( 𝑇𝑅 ) ∧ 𝑘 ∈ ( ( ( 𝐺𝐴 ) “ ℕ ) ∖ { 𝑚 ∈ ℕ ∣ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑚 } ) ) → 𝑘 ∈ ℂ )
115 114 mul02d ( ( 𝐴 ∈ ( 𝑇𝑅 ) ∧ 𝑘 ∈ ( ( ( 𝐺𝐴 ) “ ℕ ) ∖ { 𝑚 ∈ ℕ ∣ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑚 } ) ) → ( 0 · 𝑘 ) = 0 )
116 111 115 eqtrd ( ( 𝐴 ∈ ( 𝑇𝑅 ) ∧ 𝑘 ∈ ( ( ( 𝐺𝐴 ) “ ℕ ) ∖ { 𝑚 ∈ ℕ ∣ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑚 } ) ) → ( if ( ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑘 , 1 , 0 ) · 𝑘 ) = 0 )
117 55 101 116 41 fsumss ( 𝐴 ∈ ( 𝑇𝑅 ) → Σ 𝑘 ∈ { 𝑚 ∈ ℕ ∣ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑚 } ( if ( ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑘 , 1 , 0 ) · 𝑘 ) = Σ 𝑘 ∈ ( ( 𝐺𝐴 ) “ ℕ ) ( if ( ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑘 , 1 , 0 ) · 𝑘 ) )
118 92 117 eqtr3d ( 𝐴 ∈ ( 𝑇𝑅 ) → Σ 𝑤 𝑡 ∈ ( ( 𝐴 “ ℕ ) ∩ 𝐽 ) ( { 𝑡 } × ( bits ‘ ( 𝐴𝑡 ) ) ) ( ( 2 ↑ ( 2nd𝑤 ) ) · ( 1st𝑤 ) ) = Σ 𝑘 ∈ ( ( 𝐺𝐴 ) “ ℕ ) ( if ( ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( bits ‘ ( 𝐴𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = 𝑘 , 1 , 0 ) · 𝑘 ) )
119 1 2 3 4 5 6 7 8 9 eulerpartlemt0 ( 𝐴 ∈ ( 𝑇𝑅 ) ↔ ( 𝐴 ∈ ( ℕ0m ℕ ) ∧ ( 𝐴 “ ℕ ) ∈ Fin ∧ ( 𝐴 “ ℕ ) ⊆ 𝐽 ) )
120 119 simp1bi ( 𝐴 ∈ ( 𝑇𝑅 ) → 𝐴 ∈ ( ℕ0m ℕ ) )
121 elmapi ( 𝐴 ∈ ( ℕ0m ℕ ) → 𝐴 : ℕ ⟶ ℕ0 )
122 120 121 syl ( 𝐴 ∈ ( 𝑇𝑅 ) → 𝐴 : ℕ ⟶ ℕ0 )
123 122 adantr ( ( 𝐴 ∈ ( 𝑇𝑅 ) ∧ 𝑡 ∈ ( ( 𝐴 “ ℕ ) ∩ 𝐽 ) ) → 𝐴 : ℕ ⟶ ℕ0 )
124 cnvimass ( 𝐴 “ ℕ ) ⊆ dom 𝐴
125 124 122 fssdm ( 𝐴 ∈ ( 𝑇𝑅 ) → ( 𝐴 “ ℕ ) ⊆ ℕ )
126 125 adantr ( ( 𝐴 ∈ ( 𝑇𝑅 ) ∧ 𝑡 ∈ ( ( 𝐴 “ ℕ ) ∩ 𝐽 ) ) → ( 𝐴 “ ℕ ) ⊆ ℕ )
127 inss1 ( ( 𝐴 “ ℕ ) ∩ 𝐽 ) ⊆ ( 𝐴 “ ℕ )
128 127 77 sselid ( ( 𝐴 ∈ ( 𝑇𝑅 ) ∧ 𝑡 ∈ ( ( 𝐴 “ ℕ ) ∩ 𝐽 ) ) → 𝑡 ∈ ( 𝐴 “ ℕ ) )
129 126 128 sseldd ( ( 𝐴 ∈ ( 𝑇𝑅 ) ∧ 𝑡 ∈ ( ( 𝐴 “ ℕ ) ∩ 𝐽 ) ) → 𝑡 ∈ ℕ )
130 123 129 ffvelcdmd ( ( 𝐴 ∈ ( 𝑇𝑅 ) ∧ 𝑡 ∈ ( ( 𝐴 “ ℕ ) ∩ 𝐽 ) ) → ( 𝐴𝑡 ) ∈ ℕ0 )
131 bitsfi ( ( 𝐴𝑡 ) ∈ ℕ0 → ( bits ‘ ( 𝐴𝑡 ) ) ∈ Fin )
132 130 131 syl ( ( 𝐴 ∈ ( 𝑇𝑅 ) ∧ 𝑡 ∈ ( ( 𝐴 “ ℕ ) ∩ 𝐽 ) ) → ( bits ‘ ( 𝐴𝑡 ) ) ∈ Fin )
133 129 nncnd ( ( 𝐴 ∈ ( 𝑇𝑅 ) ∧ 𝑡 ∈ ( ( 𝐴 “ ℕ ) ∩ 𝐽 ) ) → 𝑡 ∈ ℂ )
134 2cnd ( ( 𝐴 ∈ ( 𝑇𝑅 ) ∧ ( 𝑡 ∈ ( ( 𝐴 “ ℕ ) ∩ 𝐽 ) ∧ 𝑛 ∈ ( bits ‘ ( 𝐴𝑡 ) ) ) ) → 2 ∈ ℂ )
135 simprr ( ( 𝐴 ∈ ( 𝑇𝑅 ) ∧ ( 𝑡 ∈ ( ( 𝐴 “ ℕ ) ∩ 𝐽 ) ∧ 𝑛 ∈ ( bits ‘ ( 𝐴𝑡 ) ) ) ) → 𝑛 ∈ ( bits ‘ ( 𝐴𝑡 ) ) )
136 80 135 sselid ( ( 𝐴 ∈ ( 𝑇𝑅 ) ∧ ( 𝑡 ∈ ( ( 𝐴 “ ℕ ) ∩ 𝐽 ) ∧ 𝑛 ∈ ( bits ‘ ( 𝐴𝑡 ) ) ) ) → 𝑛 ∈ ℕ0 )
137 134 136 expcld ( ( 𝐴 ∈ ( 𝑇𝑅 ) ∧ ( 𝑡 ∈ ( ( 𝐴 “ ℕ ) ∩ 𝐽 ) ∧ 𝑛 ∈ ( bits ‘ ( 𝐴𝑡 ) ) ) ) → ( 2 ↑ 𝑛 ) ∈ ℂ )
138 137 anassrs ( ( ( 𝐴 ∈ ( 𝑇𝑅 ) ∧ 𝑡 ∈ ( ( 𝐴 “ ℕ ) ∩ 𝐽 ) ) ∧ 𝑛 ∈ ( bits ‘ ( 𝐴𝑡 ) ) ) → ( 2 ↑ 𝑛 ) ∈ ℂ )
139 132 133 138 fsummulc1 ( ( 𝐴 ∈ ( 𝑇𝑅 ) ∧ 𝑡 ∈ ( ( 𝐴 “ ℕ ) ∩ 𝐽 ) ) → ( Σ 𝑛 ∈ ( bits ‘ ( 𝐴𝑡 ) ) ( 2 ↑ 𝑛 ) · 𝑡 ) = Σ 𝑛 ∈ ( bits ‘ ( 𝐴𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) )
140 139 sumeq2dv ( 𝐴 ∈ ( 𝑇𝑅 ) → Σ 𝑡 ∈ ( ( 𝐴 “ ℕ ) ∩ 𝐽 ) ( Σ 𝑛 ∈ ( bits ‘ ( 𝐴𝑡 ) ) ( 2 ↑ 𝑛 ) · 𝑡 ) = Σ 𝑡 ∈ ( ( 𝐴 “ ℕ ) ∩ 𝐽 ) Σ 𝑛 ∈ ( bits ‘ ( 𝐴𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) )
141 bitsinv1 ( ( 𝐴𝑡 ) ∈ ℕ0 → Σ 𝑛 ∈ ( bits ‘ ( 𝐴𝑡 ) ) ( 2 ↑ 𝑛 ) = ( 𝐴𝑡 ) )
142 141 oveq1d ( ( 𝐴𝑡 ) ∈ ℕ0 → ( Σ 𝑛 ∈ ( bits ‘ ( 𝐴𝑡 ) ) ( 2 ↑ 𝑛 ) · 𝑡 ) = ( ( 𝐴𝑡 ) · 𝑡 ) )
143 130 142 syl ( ( 𝐴 ∈ ( 𝑇𝑅 ) ∧ 𝑡 ∈ ( ( 𝐴 “ ℕ ) ∩ 𝐽 ) ) → ( Σ 𝑛 ∈ ( bits ‘ ( 𝐴𝑡 ) ) ( 2 ↑ 𝑛 ) · 𝑡 ) = ( ( 𝐴𝑡 ) · 𝑡 ) )
144 143 sumeq2dv ( 𝐴 ∈ ( 𝑇𝑅 ) → Σ 𝑡 ∈ ( ( 𝐴 “ ℕ ) ∩ 𝐽 ) ( Σ 𝑛 ∈ ( bits ‘ ( 𝐴𝑡 ) ) ( 2 ↑ 𝑛 ) · 𝑡 ) = Σ 𝑡 ∈ ( ( 𝐴 “ ℕ ) ∩ 𝐽 ) ( ( 𝐴𝑡 ) · 𝑡 ) )
145 vex 𝑡 ∈ V
146 vex 𝑛 ∈ V
147 145 146 op2ndd ( 𝑤 = ⟨ 𝑡 , 𝑛 ⟩ → ( 2nd𝑤 ) = 𝑛 )
148 147 oveq2d ( 𝑤 = ⟨ 𝑡 , 𝑛 ⟩ → ( 2 ↑ ( 2nd𝑤 ) ) = ( 2 ↑ 𝑛 ) )
149 145 146 op1std ( 𝑤 = ⟨ 𝑡 , 𝑛 ⟩ → ( 1st𝑤 ) = 𝑡 )
150 148 149 oveq12d ( 𝑤 = ⟨ 𝑡 , 𝑛 ⟩ → ( ( 2 ↑ ( 2nd𝑤 ) ) · ( 1st𝑤 ) ) = ( ( 2 ↑ 𝑛 ) · 𝑡 ) )
151 inss2 ( 𝑇𝑅 ) ⊆ 𝑅
152 151 sseli ( 𝐴 ∈ ( 𝑇𝑅 ) → 𝐴𝑅 )
153 cnveq ( 𝑓 = 𝐴 𝑓 = 𝐴 )
154 153 imaeq1d ( 𝑓 = 𝐴 → ( 𝑓 “ ℕ ) = ( 𝐴 “ ℕ ) )
155 154 eleq1d ( 𝑓 = 𝐴 → ( ( 𝑓 “ ℕ ) ∈ Fin ↔ ( 𝐴 “ ℕ ) ∈ Fin ) )
156 155 8 elab2g ( 𝐴 ∈ ( 𝑇𝑅 ) → ( 𝐴𝑅 ↔ ( 𝐴 “ ℕ ) ∈ Fin ) )
157 152 156 mpbid ( 𝐴 ∈ ( 𝑇𝑅 ) → ( 𝐴 “ ℕ ) ∈ Fin )
158 ssfi ( ( ( 𝐴 “ ℕ ) ∈ Fin ∧ ( ( 𝐴 “ ℕ ) ∩ 𝐽 ) ⊆ ( 𝐴 “ ℕ ) ) → ( ( 𝐴 “ ℕ ) ∩ 𝐽 ) ∈ Fin )
159 157 127 158 sylancl ( 𝐴 ∈ ( 𝑇𝑅 ) → ( ( 𝐴 “ ℕ ) ∩ 𝐽 ) ∈ Fin )
160 133 adantrr ( ( 𝐴 ∈ ( 𝑇𝑅 ) ∧ ( 𝑡 ∈ ( ( 𝐴 “ ℕ ) ∩ 𝐽 ) ∧ 𝑛 ∈ ( bits ‘ ( 𝐴𝑡 ) ) ) ) → 𝑡 ∈ ℂ )
161 137 160 mulcld ( ( 𝐴 ∈ ( 𝑇𝑅 ) ∧ ( 𝑡 ∈ ( ( 𝐴 “ ℕ ) ∩ 𝐽 ) ∧ 𝑛 ∈ ( bits ‘ ( 𝐴𝑡 ) ) ) ) → ( ( 2 ↑ 𝑛 ) · 𝑡 ) ∈ ℂ )
162 150 159 132 161 fsum2d ( 𝐴 ∈ ( 𝑇𝑅 ) → Σ 𝑡 ∈ ( ( 𝐴 “ ℕ ) ∩ 𝐽 ) Σ 𝑛 ∈ ( bits ‘ ( 𝐴𝑡 ) ) ( ( 2 ↑ 𝑛 ) · 𝑡 ) = Σ 𝑤 𝑡 ∈ ( ( 𝐴 “ ℕ ) ∩ 𝐽 ) ( { 𝑡 } × ( bits ‘ ( 𝐴𝑡 ) ) ) ( ( 2 ↑ ( 2nd𝑤 ) ) · ( 1st𝑤 ) ) )
163 140 144 162 3eqtr3d ( 𝐴 ∈ ( 𝑇𝑅 ) → Σ 𝑡 ∈ ( ( 𝐴 “ ℕ ) ∩ 𝐽 ) ( ( 𝐴𝑡 ) · 𝑡 ) = Σ 𝑤 𝑡 ∈ ( ( 𝐴 “ ℕ ) ∩ 𝐽 ) ( { 𝑡 } × ( bits ‘ ( 𝐴𝑡 ) ) ) ( ( 2 ↑ ( 2nd𝑤 ) ) · ( 1st𝑤 ) ) )
164 inss1 ( 𝑇𝑅 ) ⊆ 𝑇
165 164 sseli ( 𝐴 ∈ ( 𝑇𝑅 ) → 𝐴𝑇 )
166 154 sseq1d ( 𝑓 = 𝐴 → ( ( 𝑓 “ ℕ ) ⊆ 𝐽 ↔ ( 𝐴 “ ℕ ) ⊆ 𝐽 ) )
167 166 9 elrab2 ( 𝐴𝑇 ↔ ( 𝐴 ∈ ( ℕ0m ℕ ) ∧ ( 𝐴 “ ℕ ) ⊆ 𝐽 ) )
168 167 simprbi ( 𝐴𝑇 → ( 𝐴 “ ℕ ) ⊆ 𝐽 )
169 165 168 syl ( 𝐴 ∈ ( 𝑇𝑅 ) → ( 𝐴 “ ℕ ) ⊆ 𝐽 )
170 dfss2 ( ( 𝐴 “ ℕ ) ⊆ 𝐽 ↔ ( ( 𝐴 “ ℕ ) ∩ 𝐽 ) = ( 𝐴 “ ℕ ) )
171 169 170 sylib ( 𝐴 ∈ ( 𝑇𝑅 ) → ( ( 𝐴 “ ℕ ) ∩ 𝐽 ) = ( 𝐴 “ ℕ ) )
172 171 sumeq1d ( 𝐴 ∈ ( 𝑇𝑅 ) → Σ 𝑡 ∈ ( ( 𝐴 “ ℕ ) ∩ 𝐽 ) ( ( 𝐴𝑡 ) · 𝑡 ) = Σ 𝑡 ∈ ( 𝐴 “ ℕ ) ( ( 𝐴𝑡 ) · 𝑡 ) )
173 163 172 eqtr3d ( 𝐴 ∈ ( 𝑇𝑅 ) → Σ 𝑤 𝑡 ∈ ( ( 𝐴 “ ℕ ) ∩ 𝐽 ) ( { 𝑡 } × ( bits ‘ ( 𝐴𝑡 ) ) ) ( ( 2 ↑ ( 2nd𝑤 ) ) · ( 1st𝑤 ) ) = Σ 𝑡 ∈ ( 𝐴 “ ℕ ) ( ( 𝐴𝑡 ) · 𝑡 ) )
174 28 118 173 3eqtr2d ( 𝐴 ∈ ( 𝑇𝑅 ) → Σ 𝑘 ∈ ( ( 𝐺𝐴 ) “ ℕ ) ( ( ( 𝐺𝐴 ) ‘ 𝑘 ) · 𝑘 ) = Σ 𝑡 ∈ ( 𝐴 “ ℕ ) ( ( 𝐴𝑡 ) · 𝑡 ) )
175 fveq2 ( 𝑘 = 𝑡 → ( 𝐴𝑘 ) = ( 𝐴𝑡 ) )
176 id ( 𝑘 = 𝑡𝑘 = 𝑡 )
177 175 176 oveq12d ( 𝑘 = 𝑡 → ( ( 𝐴𝑘 ) · 𝑘 ) = ( ( 𝐴𝑡 ) · 𝑡 ) )
178 177 cbvsumv Σ 𝑘 ∈ ( 𝐴 “ ℕ ) ( ( 𝐴𝑘 ) · 𝑘 ) = Σ 𝑡 ∈ ( 𝐴 “ ℕ ) ( ( 𝐴𝑡 ) · 𝑡 )
179 174 178 eqtr4di ( 𝐴 ∈ ( 𝑇𝑅 ) → Σ 𝑘 ∈ ( ( 𝐺𝐴 ) “ ℕ ) ( ( ( 𝐺𝐴 ) ‘ 𝑘 ) · 𝑘 ) = Σ 𝑘 ∈ ( 𝐴 “ ℕ ) ( ( 𝐴𝑘 ) · 𝑘 ) )
180 0nn0 0 ∈ ℕ0
181 1nn0 1 ∈ ℕ0
182 prssi ( ( 0 ∈ ℕ0 ∧ 1 ∈ ℕ0 ) → { 0 , 1 } ⊆ ℕ0 )
183 180 181 182 mp2an { 0 , 1 } ⊆ ℕ0
184 fss ( ( ( 𝐺𝐴 ) : ℕ ⟶ { 0 , 1 } ∧ { 0 , 1 } ⊆ ℕ0 ) → ( 𝐺𝐴 ) : ℕ ⟶ ℕ0 )
185 183 184 mpan2 ( ( 𝐺𝐴 ) : ℕ ⟶ { 0 , 1 } → ( 𝐺𝐴 ) : ℕ ⟶ ℕ0 )
186 nn0ex 0 ∈ V
187 nnex ℕ ∈ V
188 186 187 elmap ( ( 𝐺𝐴 ) ∈ ( ℕ0m ℕ ) ↔ ( 𝐺𝐴 ) : ℕ ⟶ ℕ0 )
189 188 biimpri ( ( 𝐺𝐴 ) : ℕ ⟶ ℕ0 → ( 𝐺𝐴 ) ∈ ( ℕ0m ℕ ) )
190 20 185 189 3syl ( ( 𝐺𝐴 ) ∈ ( { 0 , 1 } ↑m ℕ ) → ( 𝐺𝐴 ) ∈ ( ℕ0m ℕ ) )
191 190 anim1i ( ( ( 𝐺𝐴 ) ∈ ( { 0 , 1 } ↑m ℕ ) ∧ ( 𝐺𝐴 ) ∈ 𝑅 ) → ( ( 𝐺𝐴 ) ∈ ( ℕ0m ℕ ) ∧ ( 𝐺𝐴 ) ∈ 𝑅 ) )
192 elin ( ( 𝐺𝐴 ) ∈ ( ( ℕ0m ℕ ) ∩ 𝑅 ) ↔ ( ( 𝐺𝐴 ) ∈ ( ℕ0m ℕ ) ∧ ( 𝐺𝐴 ) ∈ 𝑅 ) )
193 191 17 192 3imtr4i ( ( 𝐺𝐴 ) ∈ ( ( { 0 , 1 } ↑m ℕ ) ∩ 𝑅 ) → ( 𝐺𝐴 ) ∈ ( ( ℕ0m ℕ ) ∩ 𝑅 ) )
194 8 11 eulerpartlemsv2 ( ( 𝐺𝐴 ) ∈ ( ( ℕ0m ℕ ) ∩ 𝑅 ) → ( 𝑆 ‘ ( 𝐺𝐴 ) ) = Σ 𝑘 ∈ ( ( 𝐺𝐴 ) “ ℕ ) ( ( ( 𝐺𝐴 ) ‘ 𝑘 ) · 𝑘 ) )
195 16 193 194 3syl ( 𝐴 ∈ ( 𝑇𝑅 ) → ( 𝑆 ‘ ( 𝐺𝐴 ) ) = Σ 𝑘 ∈ ( ( 𝐺𝐴 ) “ ℕ ) ( ( ( 𝐺𝐴 ) ‘ 𝑘 ) · 𝑘 ) )
196 120 152 elind ( 𝐴 ∈ ( 𝑇𝑅 ) → 𝐴 ∈ ( ( ℕ0m ℕ ) ∩ 𝑅 ) )
197 8 11 eulerpartlemsv2 ( 𝐴 ∈ ( ( ℕ0m ℕ ) ∩ 𝑅 ) → ( 𝑆𝐴 ) = Σ 𝑘 ∈ ( 𝐴 “ ℕ ) ( ( 𝐴𝑘 ) · 𝑘 ) )
198 196 197 syl ( 𝐴 ∈ ( 𝑇𝑅 ) → ( 𝑆𝐴 ) = Σ 𝑘 ∈ ( 𝐴 “ ℕ ) ( ( 𝐴𝑘 ) · 𝑘 ) )
199 179 195 198 3eqtr4d ( 𝐴 ∈ ( 𝑇𝑅 ) → ( 𝑆 ‘ ( 𝐺𝐴 ) ) = ( 𝑆𝐴 ) )