Metamath Proof Explorer

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 ffvelrni ⊢ ( 𝑜 ∈ ( 𝑇 ∩ 𝑅 ) → ( 𝐺 ‘ 𝑜 ) ∈ ( ( { 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→ 𝐷