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 ⊢ 𝑃 = { 𝑓 ∈ ( ℕ0 ↑m ℕ ) ∣ ( ( ◡ 𝑓 “ ℕ ) ∈ 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 ⊢ 𝑇 = { 𝑓 ∈ ( ℕ0 ↑m ℕ ) ∣ ( ◡ 𝑓 “ ℕ ) ⊆ 𝐽 }
eulerpart.g ⊢ 𝐺 = ( 𝑜 ∈ ( 𝑇 ∩ 𝑅 ) ↦ ( ( 𝟭 ‘ ℕ ) ‘ ( 𝐹 “ ( 𝑀 ‘ ( bits ∘ ( 𝑜 ↾ 𝐽 ) ) ) ) ) )
eulerpart.s ⊢ 𝑆 = ( 𝑓 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ↦ Σ 𝑘 ∈ ℕ ( ( 𝑓 ‘ 𝑘 ) · 𝑘 ) )
Assertion eulerpartlemgs2 ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) → ( 𝑆 ‘ ( 𝐺 ‘ 𝐴 ) ) = ( 𝑆 ‘ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 eulerpart.p ⊢ 𝑃 = { 𝑓 ∈ ( ℕ0 ↑m ℕ ) ∣ ( ( ◡ 𝑓 “ ℕ ) ∈ 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 ⊢ 𝑇 = { 𝑓 ∈ ( ℕ0 ↑m ℕ ) ∣ ( ◡ 𝑓 “ ℕ ) ⊆ 𝐽 }
10 eulerpart.g ⊢ 𝐺 = ( 𝑜 ∈ ( 𝑇 ∩ 𝑅 ) ↦ ( ( 𝟭 ‘ ℕ ) ‘ ( 𝐹 “ ( 𝑀 ‘ ( bits ∘ ( 𝑜 ↾ 𝐽 ) ) ) ) ) )
11 eulerpart.s ⊢ 𝑆 = ( 𝑓 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ↦ Σ 𝑘 ∈ ℕ ( ( 𝑓 ‘ 𝑘 ) · 𝑘 ) )
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 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 vsnex ⊢ { 𝑡 } ∈ 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 eqtrid ⊢ ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) → Σ 𝑘 ∈ { 𝑚 ∈ ℕ ∣ ∃ 𝑡 ∈ ℕ ∃ 𝑛 ∈ ( 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 ⊢ ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ↔ ( 𝐴 ∈ ( ℕ0 ↑m ℕ ) ∧ ( ◡ 𝐴 “ ℕ ) ∈ Fin ∧ ( ◡ 𝐴 “ ℕ ) ⊆ 𝐽 ) )
121 120 simp1bi ⊢ ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) → 𝐴 ∈ ( ℕ0 ↑m ℕ ) )
122 elmapi ⊢ ( 𝐴 ∈ ( ℕ0 ↑m ℕ ) → 𝐴 : ℕ ⟶ ℕ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 ffvelcdmd ⊢ ( ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝑡 ∈ ( ( ◡ 𝐴 “ ℕ ) ∩ 𝐽 ) ) → ( 𝐴 ‘ 𝑡 ) ∈ ℕ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 ⊢ ( 𝐴 ∈ 𝑇 ↔ ( 𝐴 ∈ ( ℕ0 ↑m ℕ ) ∧ ( ◡ 𝐴 “ ℕ ) ⊆ 𝐽 ) )
169 168 simprbi ⊢ ( 𝐴 ∈ 𝑇 → ( ◡ 𝐴 “ ℕ ) ⊆ 𝐽 )
170 166 169 syl ⊢ ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) → ( ◡ 𝐴 “ ℕ ) ⊆ 𝐽 )
171 dfss2 ⊢ ( ( ◡ 𝐴 “ ℕ ) ⊆ 𝐽 ↔ ( ( ◡ 𝐴 “ ℕ ) ∩ 𝐽 ) = ( ◡ 𝐴 “ ℕ ) )
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 ⊢ ( ( 𝐺 ‘ 𝐴 ) ∈ ( ℕ0 ↑m ℕ ) ↔ ( 𝐺 ‘ 𝐴 ) : ℕ ⟶ ℕ0 )
190 189 biimpri ⊢ ( ( 𝐺 ‘ 𝐴 ) : ℕ ⟶ ℕ0 → ( 𝐺 ‘ 𝐴 ) ∈ ( ℕ0 ↑m ℕ ) )
191 20 186 190 3syl ⊢ ( ( 𝐺 ‘ 𝐴 ) ∈ ( { 0 , 1 } ↑m ℕ ) → ( 𝐺 ‘ 𝐴 ) ∈ ( ℕ0 ↑m ℕ ) )
192 191 anim1i ⊢ ( ( ( 𝐺 ‘ 𝐴 ) ∈ ( { 0 , 1 } ↑m ℕ ) ∧ ( 𝐺 ‘ 𝐴 ) ∈ 𝑅 ) → ( ( 𝐺 ‘ 𝐴 ) ∈ ( ℕ0 ↑m ℕ ) ∧ ( 𝐺 ‘ 𝐴 ) ∈ 𝑅 ) )
193 elin ⊢ ( ( 𝐺 ‘ 𝐴 ) ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ↔ ( ( 𝐺 ‘ 𝐴 ) ∈ ( ℕ0 ↑m ℕ ) ∧ ( 𝐺 ‘ 𝐴 ) ∈ 𝑅 ) )
194 192 17 193 3imtr4i ⊢ ( ( 𝐺 ‘ 𝐴 ) ∈ ( ( { 0 , 1 } ↑m ℕ ) ∩ 𝑅 ) → ( 𝐺 ‘ 𝐴 ) ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) )
195 8 11 eulerpartlemsv2 ⊢ ( ( 𝐺 ‘ 𝐴 ) ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) → ( 𝑆 ‘ ( 𝐺 ‘ 𝐴 ) ) = Σ 𝑘 ∈ ( ◡ ( 𝐺 ‘ 𝐴 ) “ ℕ ) ( ( ( 𝐺 ‘ 𝐴 ) ‘ 𝑘 ) · 𝑘 ) )
196 16 194 195 3syl ⊢ ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) → ( 𝑆 ‘ ( 𝐺 ‘ 𝐴 ) ) = Σ 𝑘 ∈ ( ◡ ( 𝐺 ‘ 𝐴 ) “ ℕ ) ( ( ( 𝐺 ‘ 𝐴 ) ‘ 𝑘 ) · 𝑘 ) )
197 121 153 elind ⊢ ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) → 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) )
198 8 11 eulerpartlemsv2 ⊢ ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) → ( 𝑆 ‘ 𝐴 ) = Σ 𝑘 ∈ ( ◡ 𝐴 “ ℕ ) ( ( 𝐴 ‘ 𝑘 ) · 𝑘 ) )
199 197 198 syl ⊢ ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) → ( 𝑆 ‘ 𝐴 ) = Σ 𝑘 ∈ ( ◡ 𝐴 “ ℕ ) ( ( 𝐴 ‘ 𝑘 ) · 𝑘 ) )
200 180 196 199 3eqtr4d ⊢ ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) → ( 𝑆 ‘ ( 𝐺 ‘ 𝐴 ) ) = ( 𝑆 ‘ 𝐴 ) )