Theorem eulerpartlemn

Description: Lemma for eulerpart . (Contributed by Thierry Arnoux, 30-Aug-2018)

	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	eulerpartlemn	⊢ ( 𝐺 ↾ 𝑂 ) : 𝑂 –1-1-onto→ 𝐷

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		simpl	⊢ ( ( 𝑜 = 𝑞 ∧ 𝑘 ∈ ℕ ) → 𝑜 = 𝑞 )
13	12	fveq1d	⊢ ( ( 𝑜 = 𝑞 ∧ 𝑘 ∈ ℕ ) → ( 𝑜 ‘ 𝑘 ) = ( 𝑞 ‘ 𝑘 ) )
14	13	oveq1d	⊢ ( ( 𝑜 = 𝑞 ∧ 𝑘 ∈ ℕ ) → ( ( 𝑜 ‘ 𝑘 ) · 𝑘 ) = ( ( 𝑞 ‘ 𝑘 ) · 𝑘 ) )
15	14	sumeq2dv	⊢ ( 𝑜 = 𝑞 → Σ 𝑘 ∈ ℕ ( ( 𝑜 ‘ 𝑘 ) · 𝑘 ) = Σ 𝑘 ∈ ℕ ( ( 𝑞 ‘ 𝑘 ) · 𝑘 ) )
16	15	eqeq1d	⊢ ( 𝑜 = 𝑞 → ( Σ 𝑘 ∈ ℕ ( ( 𝑜 ‘ 𝑘 ) · 𝑘 ) = 𝑁 ↔ Σ 𝑘 ∈ ℕ ( ( 𝑞 ‘ 𝑘 ) · 𝑘 ) = 𝑁 ) )
17	16	cbvrabv	⊢ { 𝑜 ∈ ( 𝑇 ∩ 𝑅 ) ∣ Σ 𝑘 ∈ ℕ ( ( 𝑜 ‘ 𝑘 ) · 𝑘 ) = 𝑁 } = { 𝑞 ∈ ( 𝑇 ∩ 𝑅 ) ∣ Σ 𝑘 ∈ ℕ ( ( 𝑞 ‘ 𝑘 ) · 𝑘 ) = 𝑁 }
18	17	a1i	⊢ ( 𝑜 = 𝑞 → { 𝑜 ∈ ( 𝑇 ∩ 𝑅 ) ∣ Σ 𝑘 ∈ ℕ ( ( 𝑜 ‘ 𝑘 ) · 𝑘 ) = 𝑁 } = { 𝑞 ∈ ( 𝑇 ∩ 𝑅 ) ∣ Σ 𝑘 ∈ ℕ ( ( 𝑞 ‘ 𝑘 ) · 𝑘 ) = 𝑁 } )
19	18	reseq2d	⊢ ( 𝑜 = 𝑞 → ( 𝐺 ↾ { 𝑜 ∈ ( 𝑇 ∩ 𝑅 ) ∣ Σ 𝑘 ∈ ℕ ( ( 𝑜 ‘ 𝑘 ) · 𝑘 ) = 𝑁 } ) = ( 𝐺 ↾ { 𝑞 ∈ ( 𝑇 ∩ 𝑅 ) ∣ Σ 𝑘 ∈ ℕ ( ( 𝑞 ‘ 𝑘 ) · 𝑘 ) = 𝑁 } ) )
20		eqidd	⊢ ( 𝑜 = 𝑞 → { 𝑑 ∈ ( ( { 0 , 1 } ↑m ℕ ) ∩ 𝑅 ) ∣ Σ 𝑘 ∈ ℕ ( ( 𝑑 ‘ 𝑘 ) · 𝑘 ) = 𝑁 } = { 𝑑 ∈ ( ( { 0 , 1 } ↑m ℕ ) ∩ 𝑅 ) ∣ Σ 𝑘 ∈ ℕ ( ( 𝑑 ‘ 𝑘 ) · 𝑘 ) = 𝑁 } )
21	19 18 20	f1oeq123d	⊢ ( 𝑜 = 𝑞 → ( ( 𝐺 ↾ { 𝑜 ∈ ( 𝑇 ∩ 𝑅 ) ∣ Σ 𝑘 ∈ ℕ ( ( 𝑜 ‘ 𝑘 ) · 𝑘 ) = 𝑁 } ) : { 𝑜 ∈ ( 𝑇 ∩ 𝑅 ) ∣ Σ 𝑘 ∈ ℕ ( ( 𝑜 ‘ 𝑘 ) · 𝑘 ) = 𝑁 } –1-1-onto→ { 𝑑 ∈ ( ( { 0 , 1 } ↑m ℕ ) ∩ 𝑅 ) ∣ Σ 𝑘 ∈ ℕ ( ( 𝑑 ‘ 𝑘 ) · 𝑘 ) = 𝑁 } ↔ ( 𝐺 ↾ { 𝑞 ∈ ( 𝑇 ∩ 𝑅 ) ∣ Σ 𝑘 ∈ ℕ ( ( 𝑞 ‘ 𝑘 ) · 𝑘 ) = 𝑁 } ) : { 𝑞 ∈ ( 𝑇 ∩ 𝑅 ) ∣ Σ 𝑘 ∈ ℕ ( ( 𝑞 ‘ 𝑘 ) · 𝑘 ) = 𝑁 } –1-1-onto→ { 𝑑 ∈ ( ( { 0 , 1 } ↑m ℕ ) ∩ 𝑅 ) ∣ Σ 𝑘 ∈ ℕ ( ( 𝑑 ‘ 𝑘 ) · 𝑘 ) = 𝑁 } ) )
22	21	imbi2d	⊢ ( 𝑜 = 𝑞 → ( ( ⊤ → ( 𝐺 ↾ { 𝑜 ∈ ( 𝑇 ∩ 𝑅 ) ∣ Σ 𝑘 ∈ ℕ ( ( 𝑜 ‘ 𝑘 ) · 𝑘 ) = 𝑁 } ) : { 𝑜 ∈ ( 𝑇 ∩ 𝑅 ) ∣ Σ 𝑘 ∈ ℕ ( ( 𝑜 ‘ 𝑘 ) · 𝑘 ) = 𝑁 } –1-1-onto→ { 𝑑 ∈ ( ( { 0 , 1 } ↑m ℕ ) ∩ 𝑅 ) ∣ Σ 𝑘 ∈ ℕ ( ( 𝑑 ‘ 𝑘 ) · 𝑘 ) = 𝑁 } ) ↔ ( ⊤ → ( 𝐺 ↾ { 𝑞 ∈ ( 𝑇 ∩ 𝑅 ) ∣ Σ 𝑘 ∈ ℕ ( ( 𝑞 ‘ 𝑘 ) · 𝑘 ) = 𝑁 } ) : { 𝑞 ∈ ( 𝑇 ∩ 𝑅 ) ∣ Σ 𝑘 ∈ ℕ ( ( 𝑞 ‘ 𝑘 ) · 𝑘 ) = 𝑁 } –1-1-onto→ { 𝑑 ∈ ( ( { 0 , 1 } ↑m ℕ ) ∩ 𝑅 ) ∣ Σ 𝑘 ∈ ℕ ( ( 𝑑 ‘ 𝑘 ) · 𝑘 ) = 𝑁 } ) ) )
23	1 2 3 4 5 6 7 8 9 10	eulerpartgbij	⊢ 𝐺 : ( 𝑇 ∩ 𝑅 ) –1-1-onto→ ( ( { 0 , 1 } ↑m ℕ ) ∩ 𝑅 )
24	23	a1i	⊢ ( ⊤ → 𝐺 : ( 𝑇 ∩ 𝑅 ) –1-1-onto→ ( ( { 0 , 1 } ↑m ℕ ) ∩ 𝑅 ) )
25		fveq2	⊢ ( 𝑞 = 𝑜 → ( 𝐺 ‘ 𝑞 ) = ( 𝐺 ‘ 𝑜 ) )
26		reseq1	⊢ ( 𝑞 = 𝑜 → ( 𝑞 ↾ 𝐽 ) = ( 𝑜 ↾ 𝐽 ) )
27	26	coeq2d	⊢ ( 𝑞 = 𝑜 → ( bits ∘ ( 𝑞 ↾ 𝐽 ) ) = ( bits ∘ ( 𝑜 ↾ 𝐽 ) ) )
28	27	fveq2d	⊢ ( 𝑞 = 𝑜 → ( 𝑀 ‘ ( bits ∘ ( 𝑞 ↾ 𝐽 ) ) ) = ( 𝑀 ‘ ( bits ∘ ( 𝑜 ↾ 𝐽 ) ) ) )
29	28	imaeq2d	⊢ ( 𝑞 = 𝑜 → ( 𝐹 “ ( 𝑀 ‘ ( bits ∘ ( 𝑞 ↾ 𝐽 ) ) ) ) = ( 𝐹 “ ( 𝑀 ‘ ( bits ∘ ( 𝑜 ↾ 𝐽 ) ) ) ) )
30	29	fveq2d	⊢ ( 𝑞 = 𝑜 → ( ( 𝟭 ‘ ℕ ) ‘ ( 𝐹 “ ( 𝑀 ‘ ( bits ∘ ( 𝑞 ↾ 𝐽 ) ) ) ) ) = ( ( 𝟭 ‘ ℕ ) ‘ ( 𝐹 “ ( 𝑀 ‘ ( bits ∘ ( 𝑜 ↾ 𝐽 ) ) ) ) ) )
31	25 30	eqeq12d	⊢ ( 𝑞 = 𝑜 → ( ( 𝐺 ‘ 𝑞 ) = ( ( 𝟭 ‘ ℕ ) ‘ ( 𝐹 “ ( 𝑀 ‘ ( bits ∘ ( 𝑞 ↾ 𝐽 ) ) ) ) ) ↔ ( 𝐺 ‘ 𝑜 ) = ( ( 𝟭 ‘ ℕ ) ‘ ( 𝐹 “ ( 𝑀 ‘ ( bits ∘ ( 𝑜 ↾ 𝐽 ) ) ) ) ) ) )
32	1 2 3 4 5 6 7 8 9 10	eulerpartlemgv	⊢ ( 𝑞 ∈ ( 𝑇 ∩ 𝑅 ) → ( 𝐺 ‘ 𝑞 ) = ( ( 𝟭 ‘ ℕ ) ‘ ( 𝐹 “ ( 𝑀 ‘ ( bits ∘ ( 𝑞 ↾ 𝐽 ) ) ) ) ) )
33	31 32	vtoclga	⊢ ( 𝑜 ∈ ( 𝑇 ∩ 𝑅 ) → ( 𝐺 ‘ 𝑜 ) = ( ( 𝟭 ‘ ℕ ) ‘ ( 𝐹 “ ( 𝑀 ‘ ( bits ∘ ( 𝑜 ↾ 𝐽 ) ) ) ) ) )
34	33	3ad2ant2	⊢ ( ( ⊤ ∧ 𝑜 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝑑 = ( ( 𝟭 ‘ ℕ ) ‘ ( 𝐹 “ ( 𝑀 ‘ ( bits ∘ ( 𝑜 ↾ 𝐽 ) ) ) ) ) ) → ( 𝐺 ‘ 𝑜 ) = ( ( 𝟭 ‘ ℕ ) ‘ ( 𝐹 “ ( 𝑀 ‘ ( bits ∘ ( 𝑜 ↾ 𝐽 ) ) ) ) ) )
35		simp3	⊢ ( ( ⊤ ∧ 𝑜 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝑑 = ( ( 𝟭 ‘ ℕ ) ‘ ( 𝐹 “ ( 𝑀 ‘ ( bits ∘ ( 𝑜 ↾ 𝐽 ) ) ) ) ) ) → 𝑑 = ( ( 𝟭 ‘ ℕ ) ‘ ( 𝐹 “ ( 𝑀 ‘ ( bits ∘ ( 𝑜 ↾ 𝐽 ) ) ) ) ) )
36	34 35	eqtr4d	⊢ ( ( ⊤ ∧ 𝑜 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝑑 = ( ( 𝟭 ‘ ℕ ) ‘ ( 𝐹 “ ( 𝑀 ‘ ( bits ∘ ( 𝑜 ↾ 𝐽 ) ) ) ) ) ) → ( 𝐺 ‘ 𝑜 ) = 𝑑 )
37	36	fveq1d	⊢ ( ( ⊤ ∧ 𝑜 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝑑 = ( ( 𝟭 ‘ ℕ ) ‘ ( 𝐹 “ ( 𝑀 ‘ ( bits ∘ ( 𝑜 ↾ 𝐽 ) ) ) ) ) ) → ( ( 𝐺 ‘ 𝑜 ) ‘ 𝑘 ) = ( 𝑑 ‘ 𝑘 ) )
38	37	oveq1d	⊢ ( ( ⊤ ∧ 𝑜 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝑑 = ( ( 𝟭 ‘ ℕ ) ‘ ( 𝐹 “ ( 𝑀 ‘ ( bits ∘ ( 𝑜 ↾ 𝐽 ) ) ) ) ) ) → ( ( ( 𝐺 ‘ 𝑜 ) ‘ 𝑘 ) · 𝑘 ) = ( ( 𝑑 ‘ 𝑘 ) · 𝑘 ) )
39	38	sumeq2sdv	⊢ ( ( ⊤ ∧ 𝑜 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝑑 = ( ( 𝟭 ‘ ℕ ) ‘ ( 𝐹 “ ( 𝑀 ‘ ( bits ∘ ( 𝑜 ↾ 𝐽 ) ) ) ) ) ) → Σ 𝑘 ∈ ℕ ( ( ( 𝐺 ‘ 𝑜 ) ‘ 𝑘 ) · 𝑘 ) = Σ 𝑘 ∈ ℕ ( ( 𝑑 ‘ 𝑘 ) · 𝑘 ) )
40	25	fveq2d	⊢ ( 𝑞 = 𝑜 → ( 𝑆 ‘ ( 𝐺 ‘ 𝑞 ) ) = ( 𝑆 ‘ ( 𝐺 ‘ 𝑜 ) ) )
41		fveq2	⊢ ( 𝑞 = 𝑜 → ( 𝑆 ‘ 𝑞 ) = ( 𝑆 ‘ 𝑜 ) )
42	40 41	eqeq12d	⊢ ( 𝑞 = 𝑜 → ( ( 𝑆 ‘ ( 𝐺 ‘ 𝑞 ) ) = ( 𝑆 ‘ 𝑞 ) ↔ ( 𝑆 ‘ ( 𝐺 ‘ 𝑜 ) ) = ( 𝑆 ‘ 𝑜 ) ) )
43	1 2 3 4 5 6 7 8 9 10 11	eulerpartlemgs2	⊢ ( 𝑞 ∈ ( 𝑇 ∩ 𝑅 ) → ( 𝑆 ‘ ( 𝐺 ‘ 𝑞 ) ) = ( 𝑆 ‘ 𝑞 ) )
44	42 43	vtoclga	⊢ ( 𝑜 ∈ ( 𝑇 ∩ 𝑅 ) → ( 𝑆 ‘ ( 𝐺 ‘ 𝑜 ) ) = ( 𝑆 ‘ 𝑜 ) )
45		nn0ex	⊢ ℕ0 ∈ V
46		0nn0	⊢ 0 ∈ ℕ0
47		1nn0	⊢ 1 ∈ ℕ0
48		prssi	⊢ ( ( 0 ∈ ℕ0 ∧ 1 ∈ ℕ0 ) → { 0 , 1 } ⊆ ℕ0 )
49	46 47 48	mp2an	⊢ { 0 , 1 } ⊆ ℕ0
50		mapss	⊢ ( ( ℕ0 ∈ V ∧ { 0 , 1 } ⊆ ℕ0 ) → ( { 0 , 1 } ↑m ℕ ) ⊆ ( ℕ0 ↑m ℕ ) )
51	45 49 50	mp2an	⊢ ( { 0 , 1 } ↑m ℕ ) ⊆ ( ℕ0 ↑m ℕ )
52		ssrin	⊢ ( ( { 0 , 1 } ↑m ℕ ) ⊆ ( ℕ0 ↑m ℕ ) → ( ( { 0 , 1 } ↑m ℕ ) ∩ 𝑅 ) ⊆ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) )
53	51 52	ax-mp	⊢ ( ( { 0 , 1 } ↑m ℕ ) ∩ 𝑅 ) ⊆ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 )
54		f1of	⊢ ( 𝐺 : ( 𝑇 ∩ 𝑅 ) –1-1-onto→ ( ( { 0 , 1 } ↑m ℕ ) ∩ 𝑅 ) → 𝐺 : ( 𝑇 ∩ 𝑅 ) ⟶ ( ( { 0 , 1 } ↑m ℕ ) ∩ 𝑅 ) )
55	23 54	ax-mp	⊢ 𝐺 : ( 𝑇 ∩ 𝑅 ) ⟶ ( ( { 0 , 1 } ↑m ℕ ) ∩ 𝑅 )
56	55	ffvelcdmi	⊢ ( 𝑜 ∈ ( 𝑇 ∩ 𝑅 ) → ( 𝐺 ‘ 𝑜 ) ∈ ( ( { 0 , 1 } ↑m ℕ ) ∩ 𝑅 ) )
57	53 56	sselid	⊢ ( 𝑜 ∈ ( 𝑇 ∩ 𝑅 ) → ( 𝐺 ‘ 𝑜 ) ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) )
58	8 11	eulerpartlemsv1	⊢ ( ( 𝐺 ‘ 𝑜 ) ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) → ( 𝑆 ‘ ( 𝐺 ‘ 𝑜 ) ) = Σ 𝑘 ∈ ℕ ( ( ( 𝐺 ‘ 𝑜 ) ‘ 𝑘 ) · 𝑘 ) )
59	57 58	syl	⊢ ( 𝑜 ∈ ( 𝑇 ∩ 𝑅 ) → ( 𝑆 ‘ ( 𝐺 ‘ 𝑜 ) ) = Σ 𝑘 ∈ ℕ ( ( ( 𝐺 ‘ 𝑜 ) ‘ 𝑘 ) · 𝑘 ) )
60	1 2 3 4 5 6 7 8 9	eulerpartlemt0	⊢ ( 𝑜 ∈ ( 𝑇 ∩ 𝑅 ) ↔ ( 𝑜 ∈ ( ℕ0 ↑m ℕ ) ∧ ( ◡ 𝑜 “ ℕ ) ∈ Fin ∧ ( ◡ 𝑜 “ ℕ ) ⊆ 𝐽 ) )
61	60	simp1bi	⊢ ( 𝑜 ∈ ( 𝑇 ∩ 𝑅 ) → 𝑜 ∈ ( ℕ0 ↑m ℕ ) )
62		inss2	⊢ ( 𝑇 ∩ 𝑅 ) ⊆ 𝑅
63	62	sseli	⊢ ( 𝑜 ∈ ( 𝑇 ∩ 𝑅 ) → 𝑜 ∈ 𝑅 )
64	61 63	elind	⊢ ( 𝑜 ∈ ( 𝑇 ∩ 𝑅 ) → 𝑜 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) )
65	8 11	eulerpartlemsv1	⊢ ( 𝑜 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) → ( 𝑆 ‘ 𝑜 ) = Σ 𝑘 ∈ ℕ ( ( 𝑜 ‘ 𝑘 ) · 𝑘 ) )
66	64 65	syl	⊢ ( 𝑜 ∈ ( 𝑇 ∩ 𝑅 ) → ( 𝑆 ‘ 𝑜 ) = Σ 𝑘 ∈ ℕ ( ( 𝑜 ‘ 𝑘 ) · 𝑘 ) )
67	44 59 66	3eqtr3d	⊢ ( 𝑜 ∈ ( 𝑇 ∩ 𝑅 ) → Σ 𝑘 ∈ ℕ ( ( ( 𝐺 ‘ 𝑜 ) ‘ 𝑘 ) · 𝑘 ) = Σ 𝑘 ∈ ℕ ( ( 𝑜 ‘ 𝑘 ) · 𝑘 ) )
68	67	3ad2ant2	⊢ ( ( ⊤ ∧ 𝑜 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝑑 = ( ( 𝟭 ‘ ℕ ) ‘ ( 𝐹 “ ( 𝑀 ‘ ( bits ∘ ( 𝑜 ↾ 𝐽 ) ) ) ) ) ) → Σ 𝑘 ∈ ℕ ( ( ( 𝐺 ‘ 𝑜 ) ‘ 𝑘 ) · 𝑘 ) = Σ 𝑘 ∈ ℕ ( ( 𝑜 ‘ 𝑘 ) · 𝑘 ) )
69	39 68	eqtr3d	⊢ ( ( ⊤ ∧ 𝑜 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝑑 = ( ( 𝟭 ‘ ℕ ) ‘ ( 𝐹 “ ( 𝑀 ‘ ( bits ∘ ( 𝑜 ↾ 𝐽 ) ) ) ) ) ) → Σ 𝑘 ∈ ℕ ( ( 𝑑 ‘ 𝑘 ) · 𝑘 ) = Σ 𝑘 ∈ ℕ ( ( 𝑜 ‘ 𝑘 ) · 𝑘 ) )
70	69	eqeq1d	⊢ ( ( ⊤ ∧ 𝑜 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝑑 = ( ( 𝟭 ‘ ℕ ) ‘ ( 𝐹 “ ( 𝑀 ‘ ( bits ∘ ( 𝑜 ↾ 𝐽 ) ) ) ) ) ) → ( Σ 𝑘 ∈ ℕ ( ( 𝑑 ‘ 𝑘 ) · 𝑘 ) = 𝑁 ↔ Σ 𝑘 ∈ ℕ ( ( 𝑜 ‘ 𝑘 ) · 𝑘 ) = 𝑁 ) )
71	10 24 70	f1oresrab	⊢ ( ⊤ → ( 𝐺 ↾ { 𝑜 ∈ ( 𝑇 ∩ 𝑅 ) ∣ Σ 𝑘 ∈ ℕ ( ( 𝑜 ‘ 𝑘 ) · 𝑘 ) = 𝑁 } ) : { 𝑜 ∈ ( 𝑇 ∩ 𝑅 ) ∣ Σ 𝑘 ∈ ℕ ( ( 𝑜 ‘ 𝑘 ) · 𝑘 ) = 𝑁 } –1-1-onto→ { 𝑑 ∈ ( ( { 0 , 1 } ↑m ℕ ) ∩ 𝑅 ) ∣ Σ 𝑘 ∈ ℕ ( ( 𝑑 ‘ 𝑘 ) · 𝑘 ) = 𝑁 } )
72	22 71	chvarvv	⊢ ( ⊤ → ( 𝐺 ↾ { 𝑞 ∈ ( 𝑇 ∩ 𝑅 ) ∣ Σ 𝑘 ∈ ℕ ( ( 𝑞 ‘ 𝑘 ) · 𝑘 ) = 𝑁 } ) : { 𝑞 ∈ ( 𝑇 ∩ 𝑅 ) ∣ Σ 𝑘 ∈ ℕ ( ( 𝑞 ‘ 𝑘 ) · 𝑘 ) = 𝑁 } –1-1-onto→ { 𝑑 ∈ ( ( { 0 , 1 } ↑m ℕ ) ∩ 𝑅 ) ∣ Σ 𝑘 ∈ ℕ ( ( 𝑑 ‘ 𝑘 ) · 𝑘 ) = 𝑁 } )
73		cnveq	⊢ ( 𝑔 = 𝑞 → ◡ 𝑔 = ◡ 𝑞 )
74	73	imaeq1d	⊢ ( 𝑔 = 𝑞 → ( ◡ 𝑔 “ ℕ ) = ( ◡ 𝑞 “ ℕ ) )
75	74	raleqdv	⊢ ( 𝑔 = 𝑞 → ( ∀ 𝑛 ∈ ( ◡ 𝑔 “ ℕ ) ¬ 2 ∥ 𝑛 ↔ ∀ 𝑛 ∈ ( ◡ 𝑞 “ ℕ ) ¬ 2 ∥ 𝑛 ) )
76	75	cbvrabv	⊢ { 𝑔 ∈ 𝑃 ∣ ∀ 𝑛 ∈ ( ◡ 𝑔 “ ℕ ) ¬ 2 ∥ 𝑛 } = { 𝑞 ∈ 𝑃 ∣ ∀ 𝑛 ∈ ( ◡ 𝑞 “ ℕ ) ¬ 2 ∥ 𝑛 }
77		nfrab1	⊢ Ⅎ 𝑞 { 𝑞 ∈ 𝑃 ∣ ∀ 𝑛 ∈ ( ◡ 𝑞 “ ℕ ) ¬ 2 ∥ 𝑛 }
78		nfrab1	⊢ Ⅎ 𝑞 { 𝑞 ∈ ( 𝑇 ∩ 𝑅 ) ∣ Σ 𝑘 ∈ ℕ ( ( 𝑞 ‘ 𝑘 ) · 𝑘 ) = 𝑁 }
79		df-3an	⊢ ( ( 𝑞 : ℕ ⟶ ℕ0 ∧ ( ◡ 𝑞 “ ℕ ) ∈ Fin ∧ Σ 𝑘 ∈ ℕ ( ( 𝑞 ‘ 𝑘 ) · 𝑘 ) = 𝑁 ) ↔ ( ( 𝑞 : ℕ ⟶ ℕ0 ∧ ( ◡ 𝑞 “ ℕ ) ∈ Fin ) ∧ Σ 𝑘 ∈ ℕ ( ( 𝑞 ‘ 𝑘 ) · 𝑘 ) = 𝑁 ) )
80	79	anbi1i	⊢ ( ( ( 𝑞 : ℕ ⟶ ℕ0 ∧ ( ◡ 𝑞 “ ℕ ) ∈ Fin ∧ Σ 𝑘 ∈ ℕ ( ( 𝑞 ‘ 𝑘 ) · 𝑘 ) = 𝑁 ) ∧ ∀ 𝑛 ∈ ( ◡ 𝑞 “ ℕ ) ¬ 2 ∥ 𝑛 ) ↔ ( ( ( 𝑞 : ℕ ⟶ ℕ0 ∧ ( ◡ 𝑞 “ ℕ ) ∈ Fin ) ∧ Σ 𝑘 ∈ ℕ ( ( 𝑞 ‘ 𝑘 ) · 𝑘 ) = 𝑁 ) ∧ ∀ 𝑛 ∈ ( ◡ 𝑞 “ ℕ ) ¬ 2 ∥ 𝑛 ) )
81	1	eulerpartleme	⊢ ( 𝑞 ∈ 𝑃 ↔ ( 𝑞 : ℕ ⟶ ℕ0 ∧ ( ◡ 𝑞 “ ℕ ) ∈ Fin ∧ Σ 𝑘 ∈ ℕ ( ( 𝑞 ‘ 𝑘 ) · 𝑘 ) = 𝑁 ) )
82	81	anbi1i	⊢ ( ( 𝑞 ∈ 𝑃 ∧ ∀ 𝑛 ∈ ( ◡ 𝑞 “ ℕ ) ¬ 2 ∥ 𝑛 ) ↔ ( ( 𝑞 : ℕ ⟶ ℕ0 ∧ ( ◡ 𝑞 “ ℕ ) ∈ Fin ∧ Σ 𝑘 ∈ ℕ ( ( 𝑞 ‘ 𝑘 ) · 𝑘 ) = 𝑁 ) ∧ ∀ 𝑛 ∈ ( ◡ 𝑞 “ ℕ ) ¬ 2 ∥ 𝑛 ) )
83		an32	⊢ ( ( ( ( 𝑞 : ℕ ⟶ ℕ0 ∧ ( ◡ 𝑞 “ ℕ ) ∈ Fin ) ∧ ∀ 𝑛 ∈ ( ◡ 𝑞 “ ℕ ) ¬ 2 ∥ 𝑛 ) ∧ Σ 𝑘 ∈ ℕ ( ( 𝑞 ‘ 𝑘 ) · 𝑘 ) = 𝑁 ) ↔ ( ( ( 𝑞 : ℕ ⟶ ℕ0 ∧ ( ◡ 𝑞 “ ℕ ) ∈ Fin ) ∧ Σ 𝑘 ∈ ℕ ( ( 𝑞 ‘ 𝑘 ) · 𝑘 ) = 𝑁 ) ∧ ∀ 𝑛 ∈ ( ◡ 𝑞 “ ℕ ) ¬ 2 ∥ 𝑛 ) )
84	80 82 83	3bitr4i	⊢ ( ( 𝑞 ∈ 𝑃 ∧ ∀ 𝑛 ∈ ( ◡ 𝑞 “ ℕ ) ¬ 2 ∥ 𝑛 ) ↔ ( ( ( 𝑞 : ℕ ⟶ ℕ0 ∧ ( ◡ 𝑞 “ ℕ ) ∈ Fin ) ∧ ∀ 𝑛 ∈ ( ◡ 𝑞 “ ℕ ) ¬ 2 ∥ 𝑛 ) ∧ Σ 𝑘 ∈ ℕ ( ( 𝑞 ‘ 𝑘 ) · 𝑘 ) = 𝑁 ) )
85	1 2 3 4 5 6 7 8 9	eulerpartlemt0	⊢ ( 𝑞 ∈ ( 𝑇 ∩ 𝑅 ) ↔ ( 𝑞 ∈ ( ℕ0 ↑m ℕ ) ∧ ( ◡ 𝑞 “ ℕ ) ∈ Fin ∧ ( ◡ 𝑞 “ ℕ ) ⊆ 𝐽 ) )
86		nnex	⊢ ℕ ∈ V
87	45 86	elmap	⊢ ( 𝑞 ∈ ( ℕ0 ↑m ℕ ) ↔ 𝑞 : ℕ ⟶ ℕ0 )
88	87	3anbi1i	⊢ ( ( 𝑞 ∈ ( ℕ0 ↑m ℕ ) ∧ ( ◡ 𝑞 “ ℕ ) ∈ Fin ∧ ( ◡ 𝑞 “ ℕ ) ⊆ 𝐽 ) ↔ ( 𝑞 : ℕ ⟶ ℕ0 ∧ ( ◡ 𝑞 “ ℕ ) ∈ Fin ∧ ( ◡ 𝑞 “ ℕ ) ⊆ 𝐽 ) )
89	85 88	bitri	⊢ ( 𝑞 ∈ ( 𝑇 ∩ 𝑅 ) ↔ ( 𝑞 : ℕ ⟶ ℕ0 ∧ ( ◡ 𝑞 “ ℕ ) ∈ Fin ∧ ( ◡ 𝑞 “ ℕ ) ⊆ 𝐽 ) )
90		df-3an	⊢ ( ( 𝑞 : ℕ ⟶ ℕ0 ∧ ( ◡ 𝑞 “ ℕ ) ∈ Fin ∧ ( ◡ 𝑞 “ ℕ ) ⊆ 𝐽 ) ↔ ( ( 𝑞 : ℕ ⟶ ℕ0 ∧ ( ◡ 𝑞 “ ℕ ) ∈ Fin ) ∧ ( ◡ 𝑞 “ ℕ ) ⊆ 𝐽 ) )
91		dfss3	⊢ ( ( ◡ 𝑞 “ ℕ ) ⊆ 𝐽 ↔ ∀ 𝑛 ∈ ( ◡ 𝑞 “ ℕ ) 𝑛 ∈ 𝐽 )
92		breq2	⊢ ( 𝑧 = 𝑛 → ( 2 ∥ 𝑧 ↔ 2 ∥ 𝑛 ) )
93	92	notbid	⊢ ( 𝑧 = 𝑛 → ( ¬ 2 ∥ 𝑧 ↔ ¬ 2 ∥ 𝑛 ) )
94	93 4	elrab2	⊢ ( 𝑛 ∈ 𝐽 ↔ ( 𝑛 ∈ ℕ ∧ ¬ 2 ∥ 𝑛 ) )
95	94	ralbii	⊢ ( ∀ 𝑛 ∈ ( ◡ 𝑞 “ ℕ ) 𝑛 ∈ 𝐽 ↔ ∀ 𝑛 ∈ ( ◡ 𝑞 “ ℕ ) ( 𝑛 ∈ ℕ ∧ ¬ 2 ∥ 𝑛 ) )
96		r19.26	⊢ ( ∀ 𝑛 ∈ ( ◡ 𝑞 “ ℕ ) ( 𝑛 ∈ ℕ ∧ ¬ 2 ∥ 𝑛 ) ↔ ( ∀ 𝑛 ∈ ( ◡ 𝑞 “ ℕ ) 𝑛 ∈ ℕ ∧ ∀ 𝑛 ∈ ( ◡ 𝑞 “ ℕ ) ¬ 2 ∥ 𝑛 ) )
97	91 95 96	3bitri	⊢ ( ( ◡ 𝑞 “ ℕ ) ⊆ 𝐽 ↔ ( ∀ 𝑛 ∈ ( ◡ 𝑞 “ ℕ ) 𝑛 ∈ ℕ ∧ ∀ 𝑛 ∈ ( ◡ 𝑞 “ ℕ ) ¬ 2 ∥ 𝑛 ) )
98		cnvimass	⊢ ( ◡ 𝑞 “ ℕ ) ⊆ dom 𝑞
99		fdm	⊢ ( 𝑞 : ℕ ⟶ ℕ0 → dom 𝑞 = ℕ )
100	98 99	sseqtrid	⊢ ( 𝑞 : ℕ ⟶ ℕ0 → ( ◡ 𝑞 “ ℕ ) ⊆ ℕ )
101		dfss3	⊢ ( ( ◡ 𝑞 “ ℕ ) ⊆ ℕ ↔ ∀ 𝑛 ∈ ( ◡ 𝑞 “ ℕ ) 𝑛 ∈ ℕ )
102	100 101	sylib	⊢ ( 𝑞 : ℕ ⟶ ℕ0 → ∀ 𝑛 ∈ ( ◡ 𝑞 “ ℕ ) 𝑛 ∈ ℕ )
103	102	biantrurd	⊢ ( 𝑞 : ℕ ⟶ ℕ0 → ( ∀ 𝑛 ∈ ( ◡ 𝑞 “ ℕ ) ¬ 2 ∥ 𝑛 ↔ ( ∀ 𝑛 ∈ ( ◡ 𝑞 “ ℕ ) 𝑛 ∈ ℕ ∧ ∀ 𝑛 ∈ ( ◡ 𝑞 “ ℕ ) ¬ 2 ∥ 𝑛 ) ) )
104	97 103	bitr4id	⊢ ( 𝑞 : ℕ ⟶ ℕ0 → ( ( ◡ 𝑞 “ ℕ ) ⊆ 𝐽 ↔ ∀ 𝑛 ∈ ( ◡ 𝑞 “ ℕ ) ¬ 2 ∥ 𝑛 ) )
105	104	adantr	⊢ ( ( 𝑞 : ℕ ⟶ ℕ0 ∧ ( ◡ 𝑞 “ ℕ ) ∈ Fin ) → ( ( ◡ 𝑞 “ ℕ ) ⊆ 𝐽 ↔ ∀ 𝑛 ∈ ( ◡ 𝑞 “ ℕ ) ¬ 2 ∥ 𝑛 ) )
106	105	pm5.32i	⊢ ( ( ( 𝑞 : ℕ ⟶ ℕ0 ∧ ( ◡ 𝑞 “ ℕ ) ∈ Fin ) ∧ ( ◡ 𝑞 “ ℕ ) ⊆ 𝐽 ) ↔ ( ( 𝑞 : ℕ ⟶ ℕ0 ∧ ( ◡ 𝑞 “ ℕ ) ∈ Fin ) ∧ ∀ 𝑛 ∈ ( ◡ 𝑞 “ ℕ ) ¬ 2 ∥ 𝑛 ) )
107	89 90 106	3bitri	⊢ ( 𝑞 ∈ ( 𝑇 ∩ 𝑅 ) ↔ ( ( 𝑞 : ℕ ⟶ ℕ0 ∧ ( ◡ 𝑞 “ ℕ ) ∈ Fin ) ∧ ∀ 𝑛 ∈ ( ◡ 𝑞 “ ℕ ) ¬ 2 ∥ 𝑛 ) )
108	107	anbi1i	⊢ ( ( 𝑞 ∈ ( 𝑇 ∩ 𝑅 ) ∧ Σ 𝑘 ∈ ℕ ( ( 𝑞 ‘ 𝑘 ) · 𝑘 ) = 𝑁 ) ↔ ( ( ( 𝑞 : ℕ ⟶ ℕ0 ∧ ( ◡ 𝑞 “ ℕ ) ∈ Fin ) ∧ ∀ 𝑛 ∈ ( ◡ 𝑞 “ ℕ ) ¬ 2 ∥ 𝑛 ) ∧ Σ 𝑘 ∈ ℕ ( ( 𝑞 ‘ 𝑘 ) · 𝑘 ) = 𝑁 ) )
109	84 108	bitr4i	⊢ ( ( 𝑞 ∈ 𝑃 ∧ ∀ 𝑛 ∈ ( ◡ 𝑞 “ ℕ ) ¬ 2 ∥ 𝑛 ) ↔ ( 𝑞 ∈ ( 𝑇 ∩ 𝑅 ) ∧ Σ 𝑘 ∈ ℕ ( ( 𝑞 ‘ 𝑘 ) · 𝑘 ) = 𝑁 ) )
110		rabid	⊢ ( 𝑞 ∈ { 𝑞 ∈ 𝑃 ∣ ∀ 𝑛 ∈ ( ◡ 𝑞 “ ℕ ) ¬ 2 ∥ 𝑛 } ↔ ( 𝑞 ∈ 𝑃 ∧ ∀ 𝑛 ∈ ( ◡ 𝑞 “ ℕ ) ¬ 2 ∥ 𝑛 ) )
111		rabid	⊢ ( 𝑞 ∈ { 𝑞 ∈ ( 𝑇 ∩ 𝑅 ) ∣ Σ 𝑘 ∈ ℕ ( ( 𝑞 ‘ 𝑘 ) · 𝑘 ) = 𝑁 } ↔ ( 𝑞 ∈ ( 𝑇 ∩ 𝑅 ) ∧ Σ 𝑘 ∈ ℕ ( ( 𝑞 ‘ 𝑘 ) · 𝑘 ) = 𝑁 ) )
112	109 110 111	3bitr4i	⊢ ( 𝑞 ∈ { 𝑞 ∈ 𝑃 ∣ ∀ 𝑛 ∈ ( ◡ 𝑞 “ ℕ ) ¬ 2 ∥ 𝑛 } ↔ 𝑞 ∈ { 𝑞 ∈ ( 𝑇 ∩ 𝑅 ) ∣ Σ 𝑘 ∈ ℕ ( ( 𝑞 ‘ 𝑘 ) · 𝑘 ) = 𝑁 } )
113	77 78 112	eqri	⊢ { 𝑞 ∈ 𝑃 ∣ ∀ 𝑛 ∈ ( ◡ 𝑞 “ ℕ ) ¬ 2 ∥ 𝑛 } = { 𝑞 ∈ ( 𝑇 ∩ 𝑅 ) ∣ Σ 𝑘 ∈ ℕ ( ( 𝑞 ‘ 𝑘 ) · 𝑘 ) = 𝑁 }
114	2 76 113	3eqtri	⊢ 𝑂 = { 𝑞 ∈ ( 𝑇 ∩ 𝑅 ) ∣ Σ 𝑘 ∈ ℕ ( ( 𝑞 ‘ 𝑘 ) · 𝑘 ) = 𝑁 }
115	114	reseq2i	⊢ ( 𝐺 ↾ 𝑂 ) = ( 𝐺 ↾ { 𝑞 ∈ ( 𝑇 ∩ 𝑅 ) ∣ Σ 𝑘 ∈ ℕ ( ( 𝑞 ‘ 𝑘 ) · 𝑘 ) = 𝑁 } )
116	115	a1i	⊢ ( ⊤ → ( 𝐺 ↾ 𝑂 ) = ( 𝐺 ↾ { 𝑞 ∈ ( 𝑇 ∩ 𝑅 ) ∣ Σ 𝑘 ∈ ℕ ( ( 𝑞 ‘ 𝑘 ) · 𝑘 ) = 𝑁 } ) )
117	114	a1i	⊢ ( ⊤ → 𝑂 = { 𝑞 ∈ ( 𝑇 ∩ 𝑅 ) ∣ Σ 𝑘 ∈ ℕ ( ( 𝑞 ‘ 𝑘 ) · 𝑘 ) = 𝑁 } )
118		nfcv	⊢ Ⅎ 𝑑 𝐷
119		nfrab1	⊢ Ⅎ 𝑑 { 𝑑 ∈ ( ( { 0 , 1 } ↑m ℕ ) ∩ 𝑅 ) ∣ Σ 𝑘 ∈ ℕ ( ( 𝑑 ‘ 𝑘 ) · 𝑘 ) = 𝑁 }
120		fnima	⊢ ( 𝑑 Fn ℕ → ( 𝑑 “ ℕ ) = ran 𝑑 )
121	120	sseq1d	⊢ ( 𝑑 Fn ℕ → ( ( 𝑑 “ ℕ ) ⊆ { 0 , 1 } ↔ ran 𝑑 ⊆ { 0 , 1 } ) )
122	121	anbi2d	⊢ ( 𝑑 Fn ℕ → ( ( ran 𝑑 ⊆ ℕ0 ∧ ( 𝑑 “ ℕ ) ⊆ { 0 , 1 } ) ↔ ( ran 𝑑 ⊆ ℕ0 ∧ ran 𝑑 ⊆ { 0 , 1 } ) ) )
123		sstr	⊢ ( ( ran 𝑑 ⊆ { 0 , 1 } ∧ { 0 , 1 } ⊆ ℕ0 ) → ran 𝑑 ⊆ ℕ0 )
124	49 123	mpan2	⊢ ( ran 𝑑 ⊆ { 0 , 1 } → ran 𝑑 ⊆ ℕ0 )
125	124	pm4.71ri	⊢ ( ran 𝑑 ⊆ { 0 , 1 } ↔ ( ran 𝑑 ⊆ ℕ0 ∧ ran 𝑑 ⊆ { 0 , 1 } ) )
126	122 125	bitr4di	⊢ ( 𝑑 Fn ℕ → ( ( ran 𝑑 ⊆ ℕ0 ∧ ( 𝑑 “ ℕ ) ⊆ { 0 , 1 } ) ↔ ran 𝑑 ⊆ { 0 , 1 } ) )
127	126	pm5.32i	⊢ ( ( 𝑑 Fn ℕ ∧ ( ran 𝑑 ⊆ ℕ0 ∧ ( 𝑑 “ ℕ ) ⊆ { 0 , 1 } ) ) ↔ ( 𝑑 Fn ℕ ∧ ran 𝑑 ⊆ { 0 , 1 } ) )
128		anass	⊢ ( ( ( 𝑑 Fn ℕ ∧ ran 𝑑 ⊆ ℕ0 ) ∧ ( 𝑑 “ ℕ ) ⊆ { 0 , 1 } ) ↔ ( 𝑑 Fn ℕ ∧ ( ran 𝑑 ⊆ ℕ0 ∧ ( 𝑑 “ ℕ ) ⊆ { 0 , 1 } ) ) )
129		df-f	⊢ ( 𝑑 : ℕ ⟶ { 0 , 1 } ↔ ( 𝑑 Fn ℕ ∧ ran 𝑑 ⊆ { 0 , 1 } ) )
130	127 128 129	3bitr4ri	⊢ ( 𝑑 : ℕ ⟶ { 0 , 1 } ↔ ( ( 𝑑 Fn ℕ ∧ ran 𝑑 ⊆ ℕ0 ) ∧ ( 𝑑 “ ℕ ) ⊆ { 0 , 1 } ) )
131		prex	⊢ { 0 , 1 } ∈ V
132	131 86	elmap	⊢ ( 𝑑 ∈ ( { 0 , 1 } ↑m ℕ ) ↔ 𝑑 : ℕ ⟶ { 0 , 1 } )
133		df-f	⊢ ( 𝑑 : ℕ ⟶ ℕ0 ↔ ( 𝑑 Fn ℕ ∧ ran 𝑑 ⊆ ℕ0 ) )
134	133	anbi1i	⊢ ( ( 𝑑 : ℕ ⟶ ℕ0 ∧ ( 𝑑 “ ℕ ) ⊆ { 0 , 1 } ) ↔ ( ( 𝑑 Fn ℕ ∧ ran 𝑑 ⊆ ℕ0 ) ∧ ( 𝑑 “ ℕ ) ⊆ { 0 , 1 } ) )
135	130 132 134	3bitr4i	⊢ ( 𝑑 ∈ ( { 0 , 1 } ↑m ℕ ) ↔ ( 𝑑 : ℕ ⟶ ℕ0 ∧ ( 𝑑 “ ℕ ) ⊆ { 0 , 1 } ) )
136		vex	⊢ 𝑑 ∈ V
137		cnveq	⊢ ( 𝑓 = 𝑑 → ◡ 𝑓 = ◡ 𝑑 )
138	137	imaeq1d	⊢ ( 𝑓 = 𝑑 → ( ◡ 𝑓 “ ℕ ) = ( ◡ 𝑑 “ ℕ ) )
139	138	eleq1d	⊢ ( 𝑓 = 𝑑 → ( ( ◡ 𝑓 “ ℕ ) ∈ Fin ↔ ( ◡ 𝑑 “ ℕ ) ∈ Fin ) )
140	136 139 8	elab2	⊢ ( 𝑑 ∈ 𝑅 ↔ ( ◡ 𝑑 “ ℕ ) ∈ Fin )
141	135 140	anbi12i	⊢ ( ( 𝑑 ∈ ( { 0 , 1 } ↑m ℕ ) ∧ 𝑑 ∈ 𝑅 ) ↔ ( ( 𝑑 : ℕ ⟶ ℕ0 ∧ ( 𝑑 “ ℕ ) ⊆ { 0 , 1 } ) ∧ ( ◡ 𝑑 “ ℕ ) ∈ Fin ) )
142		elin	⊢ ( 𝑑 ∈ ( ( { 0 , 1 } ↑m ℕ ) ∩ 𝑅 ) ↔ ( 𝑑 ∈ ( { 0 , 1 } ↑m ℕ ) ∧ 𝑑 ∈ 𝑅 ) )
143		an32	⊢ ( ( ( 𝑑 : ℕ ⟶ ℕ0 ∧ ( ◡ 𝑑 “ ℕ ) ∈ Fin ) ∧ ( 𝑑 “ ℕ ) ⊆ { 0 , 1 } ) ↔ ( ( 𝑑 : ℕ ⟶ ℕ0 ∧ ( 𝑑 “ ℕ ) ⊆ { 0 , 1 } ) ∧ ( ◡ 𝑑 “ ℕ ) ∈ Fin ) )
144	141 142 143	3bitr4i	⊢ ( 𝑑 ∈ ( ( { 0 , 1 } ↑m ℕ ) ∩ 𝑅 ) ↔ ( ( 𝑑 : ℕ ⟶ ℕ0 ∧ ( ◡ 𝑑 “ ℕ ) ∈ Fin ) ∧ ( 𝑑 “ ℕ ) ⊆ { 0 , 1 } ) )
145	144	anbi1i	⊢ ( ( 𝑑 ∈ ( ( { 0 , 1 } ↑m ℕ ) ∩ 𝑅 ) ∧ Σ 𝑘 ∈ ℕ ( ( 𝑑 ‘ 𝑘 ) · 𝑘 ) = 𝑁 ) ↔ ( ( ( 𝑑 : ℕ ⟶ ℕ0 ∧ ( ◡ 𝑑 “ ℕ ) ∈ Fin ) ∧ ( 𝑑 “ ℕ ) ⊆ { 0 , 1 } ) ∧ Σ 𝑘 ∈ ℕ ( ( 𝑑 ‘ 𝑘 ) · 𝑘 ) = 𝑁 ) )
146	1	eulerpartleme	⊢ ( 𝑑 ∈ 𝑃 ↔ ( 𝑑 : ℕ ⟶ ℕ0 ∧ ( ◡ 𝑑 “ ℕ ) ∈ Fin ∧ Σ 𝑘 ∈ ℕ ( ( 𝑑 ‘ 𝑘 ) · 𝑘 ) = 𝑁 ) )
147	146	anbi1i	⊢ ( ( 𝑑 ∈ 𝑃 ∧ ( 𝑑 “ ℕ ) ⊆ { 0 , 1 } ) ↔ ( ( 𝑑 : ℕ ⟶ ℕ0 ∧ ( ◡ 𝑑 “ ℕ ) ∈ Fin ∧ Σ 𝑘 ∈ ℕ ( ( 𝑑 ‘ 𝑘 ) · 𝑘 ) = 𝑁 ) ∧ ( 𝑑 “ ℕ ) ⊆ { 0 , 1 } ) )
148		df-3an	⊢ ( ( 𝑑 : ℕ ⟶ ℕ0 ∧ ( ◡ 𝑑 “ ℕ ) ∈ Fin ∧ Σ 𝑘 ∈ ℕ ( ( 𝑑 ‘ 𝑘 ) · 𝑘 ) = 𝑁 ) ↔ ( ( 𝑑 : ℕ ⟶ ℕ0 ∧ ( ◡ 𝑑 “ ℕ ) ∈ Fin ) ∧ Σ 𝑘 ∈ ℕ ( ( 𝑑 ‘ 𝑘 ) · 𝑘 ) = 𝑁 ) )
149	148	anbi1i	⊢ ( ( ( 𝑑 : ℕ ⟶ ℕ0 ∧ ( ◡ 𝑑 “ ℕ ) ∈ Fin ∧ Σ 𝑘 ∈ ℕ ( ( 𝑑 ‘ 𝑘 ) · 𝑘 ) = 𝑁 ) ∧ ( 𝑑 “ ℕ ) ⊆ { 0 , 1 } ) ↔ ( ( ( 𝑑 : ℕ ⟶ ℕ0 ∧ ( ◡ 𝑑 “ ℕ ) ∈ Fin ) ∧ Σ 𝑘 ∈ ℕ ( ( 𝑑 ‘ 𝑘 ) · 𝑘 ) = 𝑁 ) ∧ ( 𝑑 “ ℕ ) ⊆ { 0 , 1 } ) )
150		an32	⊢ ( ( ( ( 𝑑 : ℕ ⟶ ℕ0 ∧ ( ◡ 𝑑 “ ℕ ) ∈ Fin ) ∧ Σ 𝑘 ∈ ℕ ( ( 𝑑 ‘ 𝑘 ) · 𝑘 ) = 𝑁 ) ∧ ( 𝑑 “ ℕ ) ⊆ { 0 , 1 } ) ↔ ( ( ( 𝑑 : ℕ ⟶ ℕ0 ∧ ( ◡ 𝑑 “ ℕ ) ∈ Fin ) ∧ ( 𝑑 “ ℕ ) ⊆ { 0 , 1 } ) ∧ Σ 𝑘 ∈ ℕ ( ( 𝑑 ‘ 𝑘 ) · 𝑘 ) = 𝑁 ) )
151	147 149 150	3bitri	⊢ ( ( 𝑑 ∈ 𝑃 ∧ ( 𝑑 “ ℕ ) ⊆ { 0 , 1 } ) ↔ ( ( ( 𝑑 : ℕ ⟶ ℕ0 ∧ ( ◡ 𝑑 “ ℕ ) ∈ Fin ) ∧ ( 𝑑 “ ℕ ) ⊆ { 0 , 1 } ) ∧ Σ 𝑘 ∈ ℕ ( ( 𝑑 ‘ 𝑘 ) · 𝑘 ) = 𝑁 ) )
152	145 151	bitr4i	⊢ ( ( 𝑑 ∈ ( ( { 0 , 1 } ↑m ℕ ) ∩ 𝑅 ) ∧ Σ 𝑘 ∈ ℕ ( ( 𝑑 ‘ 𝑘 ) · 𝑘 ) = 𝑁 ) ↔ ( 𝑑 ∈ 𝑃 ∧ ( 𝑑 “ ℕ ) ⊆ { 0 , 1 } ) )
153		rabid	⊢ ( 𝑑 ∈ { 𝑑 ∈ ( ( { 0 , 1 } ↑m ℕ ) ∩ 𝑅 ) ∣ Σ 𝑘 ∈ ℕ ( ( 𝑑 ‘ 𝑘 ) · 𝑘 ) = 𝑁 } ↔ ( 𝑑 ∈ ( ( { 0 , 1 } ↑m ℕ ) ∩ 𝑅 ) ∧ Σ 𝑘 ∈ ℕ ( ( 𝑑 ‘ 𝑘 ) · 𝑘 ) = 𝑁 ) )
154	1 2 3	eulerpartlemd	⊢ ( 𝑑 ∈ 𝐷 ↔ ( 𝑑 ∈ 𝑃 ∧ ( 𝑑 “ ℕ ) ⊆ { 0 , 1 } ) )
155	152 153 154	3bitr4ri	⊢ ( 𝑑 ∈ 𝐷 ↔ 𝑑 ∈ { 𝑑 ∈ ( ( { 0 , 1 } ↑m ℕ ) ∩ 𝑅 ) ∣ Σ 𝑘 ∈ ℕ ( ( 𝑑 ‘ 𝑘 ) · 𝑘 ) = 𝑁 } )
156	118 119 155	eqri	⊢ 𝐷 = { 𝑑 ∈ ( ( { 0 , 1 } ↑m ℕ ) ∩ 𝑅 ) ∣ Σ 𝑘 ∈ ℕ ( ( 𝑑 ‘ 𝑘 ) · 𝑘 ) = 𝑁 }
157	156	a1i	⊢ ( ⊤ → 𝐷 = { 𝑑 ∈ ( ( { 0 , 1 } ↑m ℕ ) ∩ 𝑅 ) ∣ Σ 𝑘 ∈ ℕ ( ( 𝑑 ‘ 𝑘 ) · 𝑘 ) = 𝑁 } )
158	116 117 157	f1oeq123d	⊢ ( ⊤ → ( ( 𝐺 ↾ 𝑂 ) : 𝑂 –1-1-onto→ 𝐷 ↔ ( 𝐺 ↾ { 𝑞 ∈ ( 𝑇 ∩ 𝑅 ) ∣ Σ 𝑘 ∈ ℕ ( ( 𝑞 ‘ 𝑘 ) · 𝑘 ) = 𝑁 } ) : { 𝑞 ∈ ( 𝑇 ∩ 𝑅 ) ∣ Σ 𝑘 ∈ ℕ ( ( 𝑞 ‘ 𝑘 ) · 𝑘 ) = 𝑁 } –1-1-onto→ { 𝑑 ∈ ( ( { 0 , 1 } ↑m ℕ ) ∩ 𝑅 ) ∣ Σ 𝑘 ∈ ℕ ( ( 𝑑 ‘ 𝑘 ) · 𝑘 ) = 𝑁 } ) )
159	72 158	mpbird	⊢ ( ⊤ → ( 𝐺 ↾ 𝑂 ) : 𝑂 –1-1-onto→ 𝐷 )
160	159	mptru	⊢ ( 𝐺 ↾ 𝑂 ) : 𝑂 –1-1-onto→ 𝐷