Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  eulerpartlemn Structured version   Visualization version   GIF version

Theorem eulerpartlemn 34362
Description: Lemma for eulerpart 34363. (Contributed by Thierry Arnoux, 30-Aug-2018.)
Hypotheses
Ref Expression
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
Ref Expression
eulerpartlemn (𝐺𝑂):𝑂1-1-onto𝐷
Distinct variable groups:   𝑓,𝑔,𝑘,𝑛,𝑜,𝑟,𝑥,𝑦,𝑧   𝑘,𝐹,𝑛,𝑜,𝑥,𝑦   𝑓,𝐺,𝑘,𝑜   𝑜,𝐻,𝑟   𝑓,𝐽,𝑘,𝑛,𝑜,𝑟,𝑥,𝑦   𝑘,𝑀,𝑛,𝑜,𝑟,𝑥,𝑦   𝑓,𝑁,𝑔,𝑘,𝑛,𝑜,𝑥   𝑛,𝑂,𝑟,𝑥,𝑦   𝑃,𝑔,𝑘,𝑛   𝑅,𝑓,𝑘,𝑛,𝑜,𝑟,𝑥,𝑦   𝑇,𝑓,𝑘,𝑛,𝑜,𝑟,𝑥,𝑦
Allowed substitution hints:   𝐷(𝑥,𝑦,𝑧,𝑓,𝑔,𝑘,𝑛,𝑜,𝑟)   𝑃(𝑥,𝑦,𝑧,𝑓,𝑜,𝑟)   𝑅(𝑧,𝑔)   𝑆(𝑥,𝑦,𝑧,𝑓,𝑔,𝑘,𝑛,𝑜,𝑟)   𝑇(𝑧,𝑔)   𝐹(𝑧,𝑓,𝑔,𝑟)   𝐺(𝑥,𝑦,𝑧,𝑔,𝑛,𝑟)   𝐻(𝑥,𝑦,𝑧,𝑓,𝑔,𝑘,𝑛)   𝐽(𝑧,𝑔)   𝑀(𝑧,𝑓,𝑔)   𝑁(𝑦,𝑧,𝑟)   𝑂(𝑧,𝑓,𝑔,𝑘,𝑜)

Proof of Theorem eulerpartlemn
Dummy variables 𝑑 𝑞 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simpl 482 . . . . . . . . . . . . 13 ((𝑜 = 𝑞𝑘 ∈ ℕ) → 𝑜 = 𝑞)
21fveq1d 6908 . . . . . . . . . . . 12 ((𝑜 = 𝑞𝑘 ∈ ℕ) → (𝑜𝑘) = (𝑞𝑘))
32oveq1d 7445 . . . . . . . . . . 11 ((𝑜 = 𝑞𝑘 ∈ ℕ) → ((𝑜𝑘) · 𝑘) = ((𝑞𝑘) · 𝑘))
43sumeq2dv 15734 . . . . . . . . . 10 (𝑜 = 𝑞 → Σ𝑘 ∈ ℕ ((𝑜𝑘) · 𝑘) = Σ𝑘 ∈ ℕ ((𝑞𝑘) · 𝑘))
54eqeq1d 2736 . . . . . . . . 9 (𝑜 = 𝑞 → (Σ𝑘 ∈ ℕ ((𝑜𝑘) · 𝑘) = 𝑁 ↔ Σ𝑘 ∈ ℕ ((𝑞𝑘) · 𝑘) = 𝑁))
65cbvrabv 3443 . . . . . . . 8 {𝑜 ∈ (𝑇𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑜𝑘) · 𝑘) = 𝑁} = {𝑞 ∈ (𝑇𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑞𝑘) · 𝑘) = 𝑁}
76a1i 11 . . . . . . 7 (𝑜 = 𝑞 → {𝑜 ∈ (𝑇𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑜𝑘) · 𝑘) = 𝑁} = {𝑞 ∈ (𝑇𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑞𝑘) · 𝑘) = 𝑁})
87reseq2d 5999 . . . . . 6 (𝑜 = 𝑞 → (𝐺 ↾ {𝑜 ∈ (𝑇𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑜𝑘) · 𝑘) = 𝑁}) = (𝐺 ↾ {𝑞 ∈ (𝑇𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑞𝑘) · 𝑘) = 𝑁}))
9 eqidd 2735 . . . . . 6 (𝑜 = 𝑞 → {𝑑 ∈ (({0, 1} ↑m ℕ) ∩ 𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑑𝑘) · 𝑘) = 𝑁} = {𝑑 ∈ (({0, 1} ↑m ℕ) ∩ 𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑑𝑘) · 𝑘) = 𝑁})
108, 7, 9f1oeq123d 6842 . . . . 5 (𝑜 = 𝑞 → ((𝐺 ↾ {𝑜 ∈ (𝑇𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑜𝑘) · 𝑘) = 𝑁}):{𝑜 ∈ (𝑇𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑜𝑘) · 𝑘) = 𝑁}–1-1-onto→{𝑑 ∈ (({0, 1} ↑m ℕ) ∩ 𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑑𝑘) · 𝑘) = 𝑁} ↔ (𝐺 ↾ {𝑞 ∈ (𝑇𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑞𝑘) · 𝑘) = 𝑁}):{𝑞 ∈ (𝑇𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑞𝑘) · 𝑘) = 𝑁}–1-1-onto→{𝑑 ∈ (({0, 1} ↑m ℕ) ∩ 𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑑𝑘) · 𝑘) = 𝑁}))
1110imbi2d 340 . . . 4 (𝑜 = 𝑞 → ((⊤ → (𝐺 ↾ {𝑜 ∈ (𝑇𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑜𝑘) · 𝑘) = 𝑁}):{𝑜 ∈ (𝑇𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑜𝑘) · 𝑘) = 𝑁}–1-1-onto→{𝑑 ∈ (({0, 1} ↑m ℕ) ∩ 𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑑𝑘) · 𝑘) = 𝑁}) ↔ (⊤ → (𝐺 ↾ {𝑞 ∈ (𝑇𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑞𝑘) · 𝑘) = 𝑁}):{𝑞 ∈ (𝑇𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑞𝑘) · 𝑘) = 𝑁}–1-1-onto→{𝑑 ∈ (({0, 1} ↑m ℕ) ∩ 𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑑𝑘) · 𝑘) = 𝑁})))
12 eulerpart.g . . . . 5 𝐺 = (𝑜 ∈ (𝑇𝑅) ↦ ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽))))))
13 eulerpart.p . . . . . . 7 𝑃 = {𝑓 ∈ (ℕ0m ℕ) ∣ ((𝑓 “ ℕ) ∈ Fin ∧ Σ𝑘 ∈ ℕ ((𝑓𝑘) · 𝑘) = 𝑁)}
14 eulerpart.o . . . . . . 7 𝑂 = {𝑔𝑃 ∣ ∀𝑛 ∈ (𝑔 “ ℕ) ¬ 2 ∥ 𝑛}
15 eulerpart.d . . . . . . 7 𝐷 = {𝑔𝑃 ∣ ∀𝑛 ∈ ℕ (𝑔𝑛) ≤ 1}
16 eulerpart.j . . . . . . 7 𝐽 = {𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧}
17 eulerpart.f . . . . . . 7 𝐹 = (𝑥𝐽, 𝑦 ∈ ℕ0 ↦ ((2↑𝑦) · 𝑥))
18 eulerpart.h . . . . . . 7 𝐻 = {𝑟 ∈ ((𝒫 ℕ0 ∩ Fin) ↑m 𝐽) ∣ (𝑟 supp ∅) ∈ Fin}
19 eulerpart.m . . . . . . 7 𝑀 = (𝑟𝐻 ↦ {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐽𝑦 ∈ (𝑟𝑥))})
20 eulerpart.r . . . . . . 7 𝑅 = {𝑓 ∣ (𝑓 “ ℕ) ∈ Fin}
21 eulerpart.t . . . . . . 7 𝑇 = {𝑓 ∈ (ℕ0m ℕ) ∣ (𝑓 “ ℕ) ⊆ 𝐽}
2213, 14, 15, 16, 17, 18, 19, 20, 21, 12eulerpartgbij 34353 . . . . . 6 𝐺:(𝑇𝑅)–1-1-onto→(({0, 1} ↑m ℕ) ∩ 𝑅)
2322a1i 11 . . . . 5 (⊤ → 𝐺:(𝑇𝑅)–1-1-onto→(({0, 1} ↑m ℕ) ∩ 𝑅))
24 fveq2 6906 . . . . . . . . . . . . . 14 (𝑞 = 𝑜 → (𝐺𝑞) = (𝐺𝑜))
25 reseq1 5993 . . . . . . . . . . . . . . . . . 18 (𝑞 = 𝑜 → (𝑞𝐽) = (𝑜𝐽))
2625coeq2d 5875 . . . . . . . . . . . . . . . . 17 (𝑞 = 𝑜 → (bits ∘ (𝑞𝐽)) = (bits ∘ (𝑜𝐽)))
2726fveq2d 6910 . . . . . . . . . . . . . . . 16 (𝑞 = 𝑜 → (𝑀‘(bits ∘ (𝑞𝐽))) = (𝑀‘(bits ∘ (𝑜𝐽))))
2827imaeq2d 6079 . . . . . . . . . . . . . . 15 (𝑞 = 𝑜 → (𝐹 “ (𝑀‘(bits ∘ (𝑞𝐽)))) = (𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽)))))
2928fveq2d 6910 . . . . . . . . . . . . . 14 (𝑞 = 𝑜 → ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑞𝐽))))) = ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽))))))
3024, 29eqeq12d 2750 . . . . . . . . . . . . 13 (𝑞 = 𝑜 → ((𝐺𝑞) = ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑞𝐽))))) ↔ (𝐺𝑜) = ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽)))))))
3113, 14, 15, 16, 17, 18, 19, 20, 21, 12eulerpartlemgv 34354 . . . . . . . . . . . . 13 (𝑞 ∈ (𝑇𝑅) → (𝐺𝑞) = ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑞𝐽))))))
3230, 31vtoclga 3576 . . . . . . . . . . . 12 (𝑜 ∈ (𝑇𝑅) → (𝐺𝑜) = ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽))))))
33323ad2ant2 1133 . . . . . . . . . . 11 ((⊤ ∧ 𝑜 ∈ (𝑇𝑅) ∧ 𝑑 = ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽)))))) → (𝐺𝑜) = ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽))))))
34 simp3 1137 . . . . . . . . . . 11 ((⊤ ∧ 𝑜 ∈ (𝑇𝑅) ∧ 𝑑 = ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽)))))) → 𝑑 = ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽))))))
3533, 34eqtr4d 2777 . . . . . . . . . 10 ((⊤ ∧ 𝑜 ∈ (𝑇𝑅) ∧ 𝑑 = ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽)))))) → (𝐺𝑜) = 𝑑)
3635fveq1d 6908 . . . . . . . . 9 ((⊤ ∧ 𝑜 ∈ (𝑇𝑅) ∧ 𝑑 = ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽)))))) → ((𝐺𝑜)‘𝑘) = (𝑑𝑘))
3736oveq1d 7445 . . . . . . . 8 ((⊤ ∧ 𝑜 ∈ (𝑇𝑅) ∧ 𝑑 = ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽)))))) → (((𝐺𝑜)‘𝑘) · 𝑘) = ((𝑑𝑘) · 𝑘))
3837sumeq2sdv 15735 . . . . . . 7 ((⊤ ∧ 𝑜 ∈ (𝑇𝑅) ∧ 𝑑 = ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽)))))) → Σ𝑘 ∈ ℕ (((𝐺𝑜)‘𝑘) · 𝑘) = Σ𝑘 ∈ ℕ ((𝑑𝑘) · 𝑘))
3924fveq2d 6910 . . . . . . . . . . 11 (𝑞 = 𝑜 → (𝑆‘(𝐺𝑞)) = (𝑆‘(𝐺𝑜)))
40 fveq2 6906 . . . . . . . . . . 11 (𝑞 = 𝑜 → (𝑆𝑞) = (𝑆𝑜))
4139, 40eqeq12d 2750 . . . . . . . . . 10 (𝑞 = 𝑜 → ((𝑆‘(𝐺𝑞)) = (𝑆𝑞) ↔ (𝑆‘(𝐺𝑜)) = (𝑆𝑜)))
42 eulerpart.s . . . . . . . . . . 11 𝑆 = (𝑓 ∈ ((ℕ0m ℕ) ∩ 𝑅) ↦ Σ𝑘 ∈ ℕ ((𝑓𝑘) · 𝑘))
4313, 14, 15, 16, 17, 18, 19, 20, 21, 12, 42eulerpartlemgs2 34361 . . . . . . . . . 10 (𝑞 ∈ (𝑇𝑅) → (𝑆‘(𝐺𝑞)) = (𝑆𝑞))
4441, 43vtoclga 3576 . . . . . . . . 9 (𝑜 ∈ (𝑇𝑅) → (𝑆‘(𝐺𝑜)) = (𝑆𝑜))
45 nn0ex 12529 . . . . . . . . . . . . 13 0 ∈ V
46 0nn0 12538 . . . . . . . . . . . . . 14 0 ∈ ℕ0
47 1nn0 12539 . . . . . . . . . . . . . 14 1 ∈ ℕ0
48 prssi 4825 . . . . . . . . . . . . . 14 ((0 ∈ ℕ0 ∧ 1 ∈ ℕ0) → {0, 1} ⊆ ℕ0)
4946, 47, 48mp2an 692 . . . . . . . . . . . . 13 {0, 1} ⊆ ℕ0
50 mapss 8927 . . . . . . . . . . . . 13 ((ℕ0 ∈ V ∧ {0, 1} ⊆ ℕ0) → ({0, 1} ↑m ℕ) ⊆ (ℕ0m ℕ))
5145, 49, 50mp2an 692 . . . . . . . . . . . 12 ({0, 1} ↑m ℕ) ⊆ (ℕ0m ℕ)
52 ssrin 4249 . . . . . . . . . . . 12 (({0, 1} ↑m ℕ) ⊆ (ℕ0m ℕ) → (({0, 1} ↑m ℕ) ∩ 𝑅) ⊆ ((ℕ0m ℕ) ∩ 𝑅))
5351, 52ax-mp 5 . . . . . . . . . . 11 (({0, 1} ↑m ℕ) ∩ 𝑅) ⊆ ((ℕ0m ℕ) ∩ 𝑅)
54 f1of 6848 . . . . . . . . . . . . 13 (𝐺:(𝑇𝑅)–1-1-onto→(({0, 1} ↑m ℕ) ∩ 𝑅) → 𝐺:(𝑇𝑅)⟶(({0, 1} ↑m ℕ) ∩ 𝑅))
5522, 54ax-mp 5 . . . . . . . . . . . 12 𝐺:(𝑇𝑅)⟶(({0, 1} ↑m ℕ) ∩ 𝑅)
5655ffvelcdmi 7102 . . . . . . . . . . 11 (𝑜 ∈ (𝑇𝑅) → (𝐺𝑜) ∈ (({0, 1} ↑m ℕ) ∩ 𝑅))
5753, 56sselid 3992 . . . . . . . . . 10 (𝑜 ∈ (𝑇𝑅) → (𝐺𝑜) ∈ ((ℕ0m ℕ) ∩ 𝑅))
5820, 42eulerpartlemsv1 34337 . . . . . . . . . 10 ((𝐺𝑜) ∈ ((ℕ0m ℕ) ∩ 𝑅) → (𝑆‘(𝐺𝑜)) = Σ𝑘 ∈ ℕ (((𝐺𝑜)‘𝑘) · 𝑘))
5957, 58syl 17 . . . . . . . . 9 (𝑜 ∈ (𝑇𝑅) → (𝑆‘(𝐺𝑜)) = Σ𝑘 ∈ ℕ (((𝐺𝑜)‘𝑘) · 𝑘))
6013, 14, 15, 16, 17, 18, 19, 20, 21eulerpartlemt0 34350 . . . . . . . . . . . 12 (𝑜 ∈ (𝑇𝑅) ↔ (𝑜 ∈ (ℕ0m ℕ) ∧ (𝑜 “ ℕ) ∈ Fin ∧ (𝑜 “ ℕ) ⊆ 𝐽))
6160simp1bi 1144 . . . . . . . . . . 11 (𝑜 ∈ (𝑇𝑅) → 𝑜 ∈ (ℕ0m ℕ))
62 inss2 4245 . . . . . . . . . . . 12 (𝑇𝑅) ⊆ 𝑅
6362sseli 3990 . . . . . . . . . . 11 (𝑜 ∈ (𝑇𝑅) → 𝑜𝑅)
6461, 63elind 4209 . . . . . . . . . 10 (𝑜 ∈ (𝑇𝑅) → 𝑜 ∈ ((ℕ0m ℕ) ∩ 𝑅))
6520, 42eulerpartlemsv1 34337 . . . . . . . . . 10 (𝑜 ∈ ((ℕ0m ℕ) ∩ 𝑅) → (𝑆𝑜) = Σ𝑘 ∈ ℕ ((𝑜𝑘) · 𝑘))
6664, 65syl 17 . . . . . . . . 9 (𝑜 ∈ (𝑇𝑅) → (𝑆𝑜) = Σ𝑘 ∈ ℕ ((𝑜𝑘) · 𝑘))
6744, 59, 663eqtr3d 2782 . . . . . . . 8 (𝑜 ∈ (𝑇𝑅) → Σ𝑘 ∈ ℕ (((𝐺𝑜)‘𝑘) · 𝑘) = Σ𝑘 ∈ ℕ ((𝑜𝑘) · 𝑘))
68673ad2ant2 1133 . . . . . . 7 ((⊤ ∧ 𝑜 ∈ (𝑇𝑅) ∧ 𝑑 = ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽)))))) → Σ𝑘 ∈ ℕ (((𝐺𝑜)‘𝑘) · 𝑘) = Σ𝑘 ∈ ℕ ((𝑜𝑘) · 𝑘))
6938, 68eqtr3d 2776 . . . . . 6 ((⊤ ∧ 𝑜 ∈ (𝑇𝑅) ∧ 𝑑 = ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽)))))) → Σ𝑘 ∈ ℕ ((𝑑𝑘) · 𝑘) = Σ𝑘 ∈ ℕ ((𝑜𝑘) · 𝑘))
7069eqeq1d 2736 . . . . 5 ((⊤ ∧ 𝑜 ∈ (𝑇𝑅) ∧ 𝑑 = ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽)))))) → (Σ𝑘 ∈ ℕ ((𝑑𝑘) · 𝑘) = 𝑁 ↔ Σ𝑘 ∈ ℕ ((𝑜𝑘) · 𝑘) = 𝑁))
7112, 23, 70f1oresrab 7146 . . . 4 (⊤ → (𝐺 ↾ {𝑜 ∈ (𝑇𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑜𝑘) · 𝑘) = 𝑁}):{𝑜 ∈ (𝑇𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑜𝑘) · 𝑘) = 𝑁}–1-1-onto→{𝑑 ∈ (({0, 1} ↑m ℕ) ∩ 𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑑𝑘) · 𝑘) = 𝑁})
7211, 71chvarvv 1995 . . 3 (⊤ → (𝐺 ↾ {𝑞 ∈ (𝑇𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑞𝑘) · 𝑘) = 𝑁}):{𝑞 ∈ (𝑇𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑞𝑘) · 𝑘) = 𝑁}–1-1-onto→{𝑑 ∈ (({0, 1} ↑m ℕ) ∩ 𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑑𝑘) · 𝑘) = 𝑁})
73 cnveq 5886 . . . . . . . . . 10 (𝑔 = 𝑞𝑔 = 𝑞)
7473imaeq1d 6078 . . . . . . . . 9 (𝑔 = 𝑞 → (𝑔 “ ℕ) = (𝑞 “ ℕ))
7574raleqdv 3323 . . . . . . . 8 (𝑔 = 𝑞 → (∀𝑛 ∈ (𝑔 “ ℕ) ¬ 2 ∥ 𝑛 ↔ ∀𝑛 ∈ (𝑞 “ ℕ) ¬ 2 ∥ 𝑛))
7675cbvrabv 3443 . . . . . . 7 {𝑔𝑃 ∣ ∀𝑛 ∈ (𝑔 “ ℕ) ¬ 2 ∥ 𝑛} = {𝑞𝑃 ∣ ∀𝑛 ∈ (𝑞 “ ℕ) ¬ 2 ∥ 𝑛}
77 nfrab1 3453 . . . . . . . 8 𝑞{𝑞𝑃 ∣ ∀𝑛 ∈ (𝑞 “ ℕ) ¬ 2 ∥ 𝑛}
78 nfrab1 3453 . . . . . . . 8 𝑞{𝑞 ∈ (𝑇𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑞𝑘) · 𝑘) = 𝑁}
79 df-3an 1088 . . . . . . . . . . . 12 ((𝑞:ℕ⟶ℕ0 ∧ (𝑞 “ ℕ) ∈ Fin ∧ Σ𝑘 ∈ ℕ ((𝑞𝑘) · 𝑘) = 𝑁) ↔ ((𝑞:ℕ⟶ℕ0 ∧ (𝑞 “ ℕ) ∈ Fin) ∧ Σ𝑘 ∈ ℕ ((𝑞𝑘) · 𝑘) = 𝑁))
8079anbi1i 624 . . . . . . . . . . 11 (((𝑞:ℕ⟶ℕ0 ∧ (𝑞 “ ℕ) ∈ Fin ∧ Σ𝑘 ∈ ℕ ((𝑞𝑘) · 𝑘) = 𝑁) ∧ ∀𝑛 ∈ (𝑞 “ ℕ) ¬ 2 ∥ 𝑛) ↔ (((𝑞:ℕ⟶ℕ0 ∧ (𝑞 “ ℕ) ∈ Fin) ∧ Σ𝑘 ∈ ℕ ((𝑞𝑘) · 𝑘) = 𝑁) ∧ ∀𝑛 ∈ (𝑞 “ ℕ) ¬ 2 ∥ 𝑛))
8113eulerpartleme 34344 . . . . . . . . . . . 12 (𝑞𝑃 ↔ (𝑞:ℕ⟶ℕ0 ∧ (𝑞 “ ℕ) ∈ Fin ∧ Σ𝑘 ∈ ℕ ((𝑞𝑘) · 𝑘) = 𝑁))
8281anbi1i 624 . . . . . . . . . . 11 ((𝑞𝑃 ∧ ∀𝑛 ∈ (𝑞 “ ℕ) ¬ 2 ∥ 𝑛) ↔ ((𝑞:ℕ⟶ℕ0 ∧ (𝑞 “ ℕ) ∈ Fin ∧ Σ𝑘 ∈ ℕ ((𝑞𝑘) · 𝑘) = 𝑁) ∧ ∀𝑛 ∈ (𝑞 “ ℕ) ¬ 2 ∥ 𝑛))
83 an32 646 . . . . . . . . . . 11 ((((𝑞:ℕ⟶ℕ0 ∧ (𝑞 “ ℕ) ∈ Fin) ∧ ∀𝑛 ∈ (𝑞 “ ℕ) ¬ 2 ∥ 𝑛) ∧ Σ𝑘 ∈ ℕ ((𝑞𝑘) · 𝑘) = 𝑁) ↔ (((𝑞:ℕ⟶ℕ0 ∧ (𝑞 “ ℕ) ∈ Fin) ∧ Σ𝑘 ∈ ℕ ((𝑞𝑘) · 𝑘) = 𝑁) ∧ ∀𝑛 ∈ (𝑞 “ ℕ) ¬ 2 ∥ 𝑛))
8480, 82, 833bitr4i 303 . . . . . . . . . 10 ((𝑞𝑃 ∧ ∀𝑛 ∈ (𝑞 “ ℕ) ¬ 2 ∥ 𝑛) ↔ (((𝑞:ℕ⟶ℕ0 ∧ (𝑞 “ ℕ) ∈ Fin) ∧ ∀𝑛 ∈ (𝑞 “ ℕ) ¬ 2 ∥ 𝑛) ∧ Σ𝑘 ∈ ℕ ((𝑞𝑘) · 𝑘) = 𝑁))
8513, 14, 15, 16, 17, 18, 19, 20, 21eulerpartlemt0 34350 . . . . . . . . . . . . 13 (𝑞 ∈ (𝑇𝑅) ↔ (𝑞 ∈ (ℕ0m ℕ) ∧ (𝑞 “ ℕ) ∈ Fin ∧ (𝑞 “ ℕ) ⊆ 𝐽))
86 nnex 12269 . . . . . . . . . . . . . . 15 ℕ ∈ V
8745, 86elmap 8909 . . . . . . . . . . . . . 14 (𝑞 ∈ (ℕ0m ℕ) ↔ 𝑞:ℕ⟶ℕ0)
88873anbi1i 1156 . . . . . . . . . . . . 13 ((𝑞 ∈ (ℕ0m ℕ) ∧ (𝑞 “ ℕ) ∈ Fin ∧ (𝑞 “ ℕ) ⊆ 𝐽) ↔ (𝑞:ℕ⟶ℕ0 ∧ (𝑞 “ ℕ) ∈ Fin ∧ (𝑞 “ ℕ) ⊆ 𝐽))
8985, 88bitri 275 . . . . . . . . . . . 12 (𝑞 ∈ (𝑇𝑅) ↔ (𝑞:ℕ⟶ℕ0 ∧ (𝑞 “ ℕ) ∈ Fin ∧ (𝑞 “ ℕ) ⊆ 𝐽))
90 df-3an 1088 . . . . . . . . . . . 12 ((𝑞:ℕ⟶ℕ0 ∧ (𝑞 “ ℕ) ∈ Fin ∧ (𝑞 “ ℕ) ⊆ 𝐽) ↔ ((𝑞:ℕ⟶ℕ0 ∧ (𝑞 “ ℕ) ∈ Fin) ∧ (𝑞 “ ℕ) ⊆ 𝐽))
91 dfss3 3983 . . . . . . . . . . . . . . . 16 ((𝑞 “ ℕ) ⊆ 𝐽 ↔ ∀𝑛 ∈ (𝑞 “ ℕ)𝑛𝐽)
92 breq2 5151 . . . . . . . . . . . . . . . . . . 19 (𝑧 = 𝑛 → (2 ∥ 𝑧 ↔ 2 ∥ 𝑛))
9392notbid 318 . . . . . . . . . . . . . . . . . 18 (𝑧 = 𝑛 → (¬ 2 ∥ 𝑧 ↔ ¬ 2 ∥ 𝑛))
9493, 16elrab2 3697 . . . . . . . . . . . . . . . . 17 (𝑛𝐽 ↔ (𝑛 ∈ ℕ ∧ ¬ 2 ∥ 𝑛))
9594ralbii 3090 . . . . . . . . . . . . . . . 16 (∀𝑛 ∈ (𝑞 “ ℕ)𝑛𝐽 ↔ ∀𝑛 ∈ (𝑞 “ ℕ)(𝑛 ∈ ℕ ∧ ¬ 2 ∥ 𝑛))
96 r19.26 3108 . . . . . . . . . . . . . . . 16 (∀𝑛 ∈ (𝑞 “ ℕ)(𝑛 ∈ ℕ ∧ ¬ 2 ∥ 𝑛) ↔ (∀𝑛 ∈ (𝑞 “ ℕ)𝑛 ∈ ℕ ∧ ∀𝑛 ∈ (𝑞 “ ℕ) ¬ 2 ∥ 𝑛))
9791, 95, 963bitri 297 . . . . . . . . . . . . . . 15 ((𝑞 “ ℕ) ⊆ 𝐽 ↔ (∀𝑛 ∈ (𝑞 “ ℕ)𝑛 ∈ ℕ ∧ ∀𝑛 ∈ (𝑞 “ ℕ) ¬ 2 ∥ 𝑛))
98 cnvimass 6101 . . . . . . . . . . . . . . . . . 18 (𝑞 “ ℕ) ⊆ dom 𝑞
99 fdm 6745 . . . . . . . . . . . . . . . . . 18 (𝑞:ℕ⟶ℕ0 → dom 𝑞 = ℕ)
10098, 99sseqtrid 4047 . . . . . . . . . . . . . . . . 17 (𝑞:ℕ⟶ℕ0 → (𝑞 “ ℕ) ⊆ ℕ)
101 dfss3 3983 . . . . . . . . . . . . . . . . 17 ((𝑞 “ ℕ) ⊆ ℕ ↔ ∀𝑛 ∈ (𝑞 “ ℕ)𝑛 ∈ ℕ)
102100, 101sylib 218 . . . . . . . . . . . . . . . 16 (𝑞:ℕ⟶ℕ0 → ∀𝑛 ∈ (𝑞 “ ℕ)𝑛 ∈ ℕ)
103102biantrurd 532 . . . . . . . . . . . . . . 15 (𝑞:ℕ⟶ℕ0 → (∀𝑛 ∈ (𝑞 “ ℕ) ¬ 2 ∥ 𝑛 ↔ (∀𝑛 ∈ (𝑞 “ ℕ)𝑛 ∈ ℕ ∧ ∀𝑛 ∈ (𝑞 “ ℕ) ¬ 2 ∥ 𝑛)))
10497, 103bitr4id 290 . . . . . . . . . . . . . 14 (𝑞:ℕ⟶ℕ0 → ((𝑞 “ ℕ) ⊆ 𝐽 ↔ ∀𝑛 ∈ (𝑞 “ ℕ) ¬ 2 ∥ 𝑛))
105104adantr 480 . . . . . . . . . . . . 13 ((𝑞:ℕ⟶ℕ0 ∧ (𝑞 “ ℕ) ∈ Fin) → ((𝑞 “ ℕ) ⊆ 𝐽 ↔ ∀𝑛 ∈ (𝑞 “ ℕ) ¬ 2 ∥ 𝑛))
106105pm5.32i 574 . . . . . . . . . . . 12 (((𝑞:ℕ⟶ℕ0 ∧ (𝑞 “ ℕ) ∈ Fin) ∧ (𝑞 “ ℕ) ⊆ 𝐽) ↔ ((𝑞:ℕ⟶ℕ0 ∧ (𝑞 “ ℕ) ∈ Fin) ∧ ∀𝑛 ∈ (𝑞 “ ℕ) ¬ 2 ∥ 𝑛))
10789, 90, 1063bitri 297 . . . . . . . . . . 11 (𝑞 ∈ (𝑇𝑅) ↔ ((𝑞:ℕ⟶ℕ0 ∧ (𝑞 “ ℕ) ∈ Fin) ∧ ∀𝑛 ∈ (𝑞 “ ℕ) ¬ 2 ∥ 𝑛))
108107anbi1i 624 . . . . . . . . . 10 ((𝑞 ∈ (𝑇𝑅) ∧ Σ𝑘 ∈ ℕ ((𝑞𝑘) · 𝑘) = 𝑁) ↔ (((𝑞:ℕ⟶ℕ0 ∧ (𝑞 “ ℕ) ∈ Fin) ∧ ∀𝑛 ∈ (𝑞 “ ℕ) ¬ 2 ∥ 𝑛) ∧ Σ𝑘 ∈ ℕ ((𝑞𝑘) · 𝑘) = 𝑁))
10984, 108bitr4i 278 . . . . . . . . 9 ((𝑞𝑃 ∧ ∀𝑛 ∈ (𝑞 “ ℕ) ¬ 2 ∥ 𝑛) ↔ (𝑞 ∈ (𝑇𝑅) ∧ Σ𝑘 ∈ ℕ ((𝑞𝑘) · 𝑘) = 𝑁))
110 rabid 3454 . . . . . . . . 9 (𝑞 ∈ {𝑞𝑃 ∣ ∀𝑛 ∈ (𝑞 “ ℕ) ¬ 2 ∥ 𝑛} ↔ (𝑞𝑃 ∧ ∀𝑛 ∈ (𝑞 “ ℕ) ¬ 2 ∥ 𝑛))
111 rabid 3454 . . . . . . . . 9 (𝑞 ∈ {𝑞 ∈ (𝑇𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑞𝑘) · 𝑘) = 𝑁} ↔ (𝑞 ∈ (𝑇𝑅) ∧ Σ𝑘 ∈ ℕ ((𝑞𝑘) · 𝑘) = 𝑁))
112109, 110, 1113bitr4i 303 . . . . . . . 8 (𝑞 ∈ {𝑞𝑃 ∣ ∀𝑛 ∈ (𝑞 “ ℕ) ¬ 2 ∥ 𝑛} ↔ 𝑞 ∈ {𝑞 ∈ (𝑇𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑞𝑘) · 𝑘) = 𝑁})
11377, 78, 112eqri 4015 . . . . . . 7 {𝑞𝑃 ∣ ∀𝑛 ∈ (𝑞 “ ℕ) ¬ 2 ∥ 𝑛} = {𝑞 ∈ (𝑇𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑞𝑘) · 𝑘) = 𝑁}
11414, 76, 1133eqtri 2766 . . . . . 6 𝑂 = {𝑞 ∈ (𝑇𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑞𝑘) · 𝑘) = 𝑁}
115114reseq2i 5996 . . . . 5 (𝐺𝑂) = (𝐺 ↾ {𝑞 ∈ (𝑇𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑞𝑘) · 𝑘) = 𝑁})
116115a1i 11 . . . 4 (⊤ → (𝐺𝑂) = (𝐺 ↾ {𝑞 ∈ (𝑇𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑞𝑘) · 𝑘) = 𝑁}))
117114a1i 11 . . . 4 (⊤ → 𝑂 = {𝑞 ∈ (𝑇𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑞𝑘) · 𝑘) = 𝑁})
118 nfcv 2902 . . . . . 6 𝑑𝐷
119 nfrab1 3453 . . . . . 6 𝑑{𝑑 ∈ (({0, 1} ↑m ℕ) ∩ 𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑑𝑘) · 𝑘) = 𝑁}
120 fnima 6698 . . . . . . . . . . . . . . . . 17 (𝑑 Fn ℕ → (𝑑 “ ℕ) = ran 𝑑)
121120sseq1d 4026 . . . . . . . . . . . . . . . 16 (𝑑 Fn ℕ → ((𝑑 “ ℕ) ⊆ {0, 1} ↔ ran 𝑑 ⊆ {0, 1}))
122121anbi2d 630 . . . . . . . . . . . . . . 15 (𝑑 Fn ℕ → ((ran 𝑑 ⊆ ℕ0 ∧ (𝑑 “ ℕ) ⊆ {0, 1}) ↔ (ran 𝑑 ⊆ ℕ0 ∧ ran 𝑑 ⊆ {0, 1})))
123 sstr 4003 . . . . . . . . . . . . . . . . 17 ((ran 𝑑 ⊆ {0, 1} ∧ {0, 1} ⊆ ℕ0) → ran 𝑑 ⊆ ℕ0)
12449, 123mpan2 691 . . . . . . . . . . . . . . . 16 (ran 𝑑 ⊆ {0, 1} → ran 𝑑 ⊆ ℕ0)
125124pm4.71ri 560 . . . . . . . . . . . . . . 15 (ran 𝑑 ⊆ {0, 1} ↔ (ran 𝑑 ⊆ ℕ0 ∧ ran 𝑑 ⊆ {0, 1}))
126122, 125bitr4di 289 . . . . . . . . . . . . . 14 (𝑑 Fn ℕ → ((ran 𝑑 ⊆ ℕ0 ∧ (𝑑 “ ℕ) ⊆ {0, 1}) ↔ ran 𝑑 ⊆ {0, 1}))
127126pm5.32i 574 . . . . . . . . . . . . 13 ((𝑑 Fn ℕ ∧ (ran 𝑑 ⊆ ℕ0 ∧ (𝑑 “ ℕ) ⊆ {0, 1})) ↔ (𝑑 Fn ℕ ∧ ran 𝑑 ⊆ {0, 1}))
128 anass 468 . . . . . . . . . . . . 13 (((𝑑 Fn ℕ ∧ ran 𝑑 ⊆ ℕ0) ∧ (𝑑 “ ℕ) ⊆ {0, 1}) ↔ (𝑑 Fn ℕ ∧ (ran 𝑑 ⊆ ℕ0 ∧ (𝑑 “ ℕ) ⊆ {0, 1})))
129 df-f 6566 . . . . . . . . . . . . 13 (𝑑:ℕ⟶{0, 1} ↔ (𝑑 Fn ℕ ∧ ran 𝑑 ⊆ {0, 1}))
130127, 128, 1293bitr4ri 304 . . . . . . . . . . . 12 (𝑑:ℕ⟶{0, 1} ↔ ((𝑑 Fn ℕ ∧ ran 𝑑 ⊆ ℕ0) ∧ (𝑑 “ ℕ) ⊆ {0, 1}))
131 prex 5442 . . . . . . . . . . . . 13 {0, 1} ∈ V
132131, 86elmap 8909 . . . . . . . . . . . 12 (𝑑 ∈ ({0, 1} ↑m ℕ) ↔ 𝑑:ℕ⟶{0, 1})
133 df-f 6566 . . . . . . . . . . . . 13 (𝑑:ℕ⟶ℕ0 ↔ (𝑑 Fn ℕ ∧ ran 𝑑 ⊆ ℕ0))
134133anbi1i 624 . . . . . . . . . . . 12 ((𝑑:ℕ⟶ℕ0 ∧ (𝑑 “ ℕ) ⊆ {0, 1}) ↔ ((𝑑 Fn ℕ ∧ ran 𝑑 ⊆ ℕ0) ∧ (𝑑 “ ℕ) ⊆ {0, 1}))
135130, 132, 1343bitr4i 303 . . . . . . . . . . 11 (𝑑 ∈ ({0, 1} ↑m ℕ) ↔ (𝑑:ℕ⟶ℕ0 ∧ (𝑑 “ ℕ) ⊆ {0, 1}))
136 vex 3481 . . . . . . . . . . . 12 𝑑 ∈ V
137 cnveq 5886 . . . . . . . . . . . . . 14 (𝑓 = 𝑑𝑓 = 𝑑)
138137imaeq1d 6078 . . . . . . . . . . . . 13 (𝑓 = 𝑑 → (𝑓 “ ℕ) = (𝑑 “ ℕ))
139138eleq1d 2823 . . . . . . . . . . . 12 (𝑓 = 𝑑 → ((𝑓 “ ℕ) ∈ Fin ↔ (𝑑 “ ℕ) ∈ Fin))
140136, 139, 20elab2 3684 . . . . . . . . . . 11 (𝑑𝑅 ↔ (𝑑 “ ℕ) ∈ Fin)
141135, 140anbi12i 628 . . . . . . . . . 10 ((𝑑 ∈ ({0, 1} ↑m ℕ) ∧ 𝑑𝑅) ↔ ((𝑑:ℕ⟶ℕ0 ∧ (𝑑 “ ℕ) ⊆ {0, 1}) ∧ (𝑑 “ ℕ) ∈ Fin))
142 elin 3978 . . . . . . . . . 10 (𝑑 ∈ (({0, 1} ↑m ℕ) ∩ 𝑅) ↔ (𝑑 ∈ ({0, 1} ↑m ℕ) ∧ 𝑑𝑅))
143 an32 646 . . . . . . . . . 10 (((𝑑:ℕ⟶ℕ0 ∧ (𝑑 “ ℕ) ∈ Fin) ∧ (𝑑 “ ℕ) ⊆ {0, 1}) ↔ ((𝑑:ℕ⟶ℕ0 ∧ (𝑑 “ ℕ) ⊆ {0, 1}) ∧ (𝑑 “ ℕ) ∈ Fin))
144141, 142, 1433bitr4i 303 . . . . . . . . 9 (𝑑 ∈ (({0, 1} ↑m ℕ) ∩ 𝑅) ↔ ((𝑑:ℕ⟶ℕ0 ∧ (𝑑 “ ℕ) ∈ Fin) ∧ (𝑑 “ ℕ) ⊆ {0, 1}))
145144anbi1i 624 . . . . . . . 8 ((𝑑 ∈ (({0, 1} ↑m ℕ) ∩ 𝑅) ∧ Σ𝑘 ∈ ℕ ((𝑑𝑘) · 𝑘) = 𝑁) ↔ (((𝑑:ℕ⟶ℕ0 ∧ (𝑑 “ ℕ) ∈ Fin) ∧ (𝑑 “ ℕ) ⊆ {0, 1}) ∧ Σ𝑘 ∈ ℕ ((𝑑𝑘) · 𝑘) = 𝑁))
14613eulerpartleme 34344 . . . . . . . . . 10 (𝑑𝑃 ↔ (𝑑:ℕ⟶ℕ0 ∧ (𝑑 “ ℕ) ∈ Fin ∧ Σ𝑘 ∈ ℕ ((𝑑𝑘) · 𝑘) = 𝑁))
147146anbi1i 624 . . . . . . . . 9 ((𝑑𝑃 ∧ (𝑑 “ ℕ) ⊆ {0, 1}) ↔ ((𝑑:ℕ⟶ℕ0 ∧ (𝑑 “ ℕ) ∈ Fin ∧ Σ𝑘 ∈ ℕ ((𝑑𝑘) · 𝑘) = 𝑁) ∧ (𝑑 “ ℕ) ⊆ {0, 1}))
148 df-3an 1088 . . . . . . . . . 10 ((𝑑:ℕ⟶ℕ0 ∧ (𝑑 “ ℕ) ∈ Fin ∧ Σ𝑘 ∈ ℕ ((𝑑𝑘) · 𝑘) = 𝑁) ↔ ((𝑑:ℕ⟶ℕ0 ∧ (𝑑 “ ℕ) ∈ Fin) ∧ Σ𝑘 ∈ ℕ ((𝑑𝑘) · 𝑘) = 𝑁))
149148anbi1i 624 . . . . . . . . 9 (((𝑑:ℕ⟶ℕ0 ∧ (𝑑 “ ℕ) ∈ Fin ∧ Σ𝑘 ∈ ℕ ((𝑑𝑘) · 𝑘) = 𝑁) ∧ (𝑑 “ ℕ) ⊆ {0, 1}) ↔ (((𝑑:ℕ⟶ℕ0 ∧ (𝑑 “ ℕ) ∈ Fin) ∧ Σ𝑘 ∈ ℕ ((𝑑𝑘) · 𝑘) = 𝑁) ∧ (𝑑 “ ℕ) ⊆ {0, 1}))
150 an32 646 . . . . . . . . 9 ((((𝑑:ℕ⟶ℕ0 ∧ (𝑑 “ ℕ) ∈ Fin) ∧ Σ𝑘 ∈ ℕ ((𝑑𝑘) · 𝑘) = 𝑁) ∧ (𝑑 “ ℕ) ⊆ {0, 1}) ↔ (((𝑑:ℕ⟶ℕ0 ∧ (𝑑 “ ℕ) ∈ Fin) ∧ (𝑑 “ ℕ) ⊆ {0, 1}) ∧ Σ𝑘 ∈ ℕ ((𝑑𝑘) · 𝑘) = 𝑁))
151147, 149, 1503bitri 297 . . . . . . . 8 ((𝑑𝑃 ∧ (𝑑 “ ℕ) ⊆ {0, 1}) ↔ (((𝑑:ℕ⟶ℕ0 ∧ (𝑑 “ ℕ) ∈ Fin) ∧ (𝑑 “ ℕ) ⊆ {0, 1}) ∧ Σ𝑘 ∈ ℕ ((𝑑𝑘) · 𝑘) = 𝑁))
152145, 151bitr4i 278 . . . . . . 7 ((𝑑 ∈ (({0, 1} ↑m ℕ) ∩ 𝑅) ∧ Σ𝑘 ∈ ℕ ((𝑑𝑘) · 𝑘) = 𝑁) ↔ (𝑑𝑃 ∧ (𝑑 “ ℕ) ⊆ {0, 1}))
153 rabid 3454 . . . . . . 7 (𝑑 ∈ {𝑑 ∈ (({0, 1} ↑m ℕ) ∩ 𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑑𝑘) · 𝑘) = 𝑁} ↔ (𝑑 ∈ (({0, 1} ↑m ℕ) ∩ 𝑅) ∧ Σ𝑘 ∈ ℕ ((𝑑𝑘) · 𝑘) = 𝑁))
15413, 14, 15eulerpartlemd 34347 . . . . . . 7 (𝑑𝐷 ↔ (𝑑𝑃 ∧ (𝑑 “ ℕ) ⊆ {0, 1}))
155152, 153, 1543bitr4ri 304 . . . . . 6 (𝑑𝐷𝑑 ∈ {𝑑 ∈ (({0, 1} ↑m ℕ) ∩ 𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑑𝑘) · 𝑘) = 𝑁})
156118, 119, 155eqri 4015 . . . . 5 𝐷 = {𝑑 ∈ (({0, 1} ↑m ℕ) ∩ 𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑑𝑘) · 𝑘) = 𝑁}
157156a1i 11 . . . 4 (⊤ → 𝐷 = {𝑑 ∈ (({0, 1} ↑m ℕ) ∩ 𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑑𝑘) · 𝑘) = 𝑁})
158116, 117, 157f1oeq123d 6842 . . 3 (⊤ → ((𝐺𝑂):𝑂1-1-onto𝐷 ↔ (𝐺 ↾ {𝑞 ∈ (𝑇𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑞𝑘) · 𝑘) = 𝑁}):{𝑞 ∈ (𝑇𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑞𝑘) · 𝑘) = 𝑁}–1-1-onto→{𝑑 ∈ (({0, 1} ↑m ℕ) ∩ 𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑑𝑘) · 𝑘) = 𝑁}))
15972, 158mpbird 257 . 2 (⊤ → (𝐺𝑂):𝑂1-1-onto𝐷)
160159mptru 1543 1 (𝐺𝑂):𝑂1-1-onto𝐷
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wa 395  w3a 1086   = wceq 1536  wtru 1537  wcel 2105  {cab 2711  wral 3058  {crab 3432  Vcvv 3477  cin 3961  wss 3962  c0 4338  𝒫 cpw 4604  {cpr 4632   class class class wbr 5147  {copab 5209  cmpt 5230  ccnv 5687  dom cdm 5688  ran crn 5689  cres 5690  cima 5691  ccom 5692   Fn wfn 6557  wf 6558  1-1-ontowf1o 6561  cfv 6562  (class class class)co 7430  cmpo 7432   supp csupp 8183  m cmap 8864  Fincfn 8983  0cc0 11152  1c1 11153   · cmul 11157  cle 11293  cn 12263  2c2 12318  0cn0 12523  cexp 14098  Σcsu 15718  cdvds 16286  bitscbits 16452  𝟭cind 33990
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-rep 5284  ax-sep 5301  ax-nul 5311  ax-pow 5370  ax-pr 5437  ax-un 7753  ax-inf2 9678  ax-ac2 10500  ax-cnex 11208  ax-resscn 11209  ax-1cn 11210  ax-icn 11211  ax-addcl 11212  ax-addrcl 11213  ax-mulcl 11214  ax-mulrcl 11215  ax-mulcom 11216  ax-addass 11217  ax-mulass 11218  ax-distr 11219  ax-i2m1 11220  ax-1ne0 11221  ax-1rid 11222  ax-rnegex 11223  ax-rrecex 11224  ax-cnre 11225  ax-pre-lttri 11226  ax-pre-lttrn 11227  ax-pre-ltadd 11228  ax-pre-mulgt0 11229  ax-pre-sup 11230
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ne 2938  df-nel 3044  df-ral 3059  df-rex 3068  df-rmo 3377  df-reu 3378  df-rab 3433  df-v 3479  df-sbc 3791  df-csb 3908  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-pss 3982  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-int 4951  df-iun 4997  df-disj 5115  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5582  df-eprel 5588  df-po 5596  df-so 5597  df-fr 5640  df-se 5641  df-we 5642  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-pred 6322  df-ord 6388  df-on 6389  df-lim 6390  df-suc 6391  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-f1 6567  df-fo 6568  df-f1o 6569  df-fv 6570  df-isom 6571  df-riota 7387  df-ov 7433  df-oprab 7434  df-mpo 7435  df-om 7887  df-1st 8012  df-2nd 8013  df-supp 8184  df-frecs 8304  df-wrecs 8335  df-recs 8409  df-rdg 8448  df-1o 8504  df-2o 8505  df-oadd 8508  df-er 8743  df-map 8866  df-pm 8867  df-en 8984  df-dom 8985  df-sdom 8986  df-fin 8987  df-fsupp 9399  df-sup 9479  df-inf 9480  df-oi 9547  df-dju 9938  df-card 9976  df-acn 9979  df-ac 10153  df-pnf 11294  df-mnf 11295  df-xr 11296  df-ltxr 11297  df-le 11298  df-sub 11491  df-neg 11492  df-div 11918  df-nn 12264  df-2 12326  df-3 12327  df-n0 12524  df-xnn0 12597  df-z 12611  df-uz 12876  df-rp 13032  df-fz 13544  df-fzo 13691  df-fl 13828  df-mod 13906  df-seq 14039  df-exp 14099  df-hash 14366  df-cj 15134  df-re 15135  df-im 15136  df-sqrt 15270  df-abs 15271  df-clim 15520  df-sum 15719  df-dvds 16287  df-bits 16455  df-ind 33991
This theorem is referenced by:  eulerpart  34363
  Copyright terms: Public domain W3C validator