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		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	⊢ ( ( 𝐺 ‘ 𝐴 ) ∈ ( ℕ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	⊢ ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) → ( 𝑆 ‘ ( 𝐺 ‘ 𝐴 ) ) = ( 𝑆 ‘ 𝐴 ) )