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 34383
Description: Lemma for eulerpart 34384. (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 7446 . . . . . . . . . . 11 ((𝑜 = 𝑞𝑘 ∈ ℕ) → ((𝑜𝑘) · 𝑘) = ((𝑞𝑘) · 𝑘))
43sumeq2dv 15738 . . . . . . . . . 10 (𝑜 = 𝑞 → Σ𝑘 ∈ ℕ ((𝑜𝑘) · 𝑘) = Σ𝑘 ∈ ℕ ((𝑞𝑘) · 𝑘))
54eqeq1d 2739 . . . . . . . . 9 (𝑜 = 𝑞 → (Σ𝑘 ∈ ℕ ((𝑜𝑘) · 𝑘) = 𝑁 ↔ Σ𝑘 ∈ ℕ ((𝑞𝑘) · 𝑘) = 𝑁))
65cbvrabv 3447 . . . . . . . 8 {𝑜 ∈ (𝑇𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑜𝑘) · 𝑘) = 𝑁} = {𝑞 ∈ (𝑇𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑞𝑘) · 𝑘) = 𝑁}
76a1i 11 . . . . . . 7 (𝑜 = 𝑞 → {𝑜 ∈ (𝑇𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑜𝑘) · 𝑘) = 𝑁} = {𝑞 ∈ (𝑇𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑞𝑘) · 𝑘) = 𝑁})
87reseq2d 5997 . . . . . 6 (𝑜 = 𝑞 → (𝐺 ↾ {𝑜 ∈ (𝑇𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑜𝑘) · 𝑘) = 𝑁}) = (𝐺 ↾ {𝑞 ∈ (𝑇𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑞𝑘) · 𝑘) = 𝑁}))
9 eqidd 2738 . . . . . 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 34374 . . . . . 6 𝐺:(𝑇𝑅)–1-1-onto→(({0, 1} ↑m ℕ) ∩ 𝑅)
2322a1i 11 . . . . 5 (⊤ → 𝐺:(𝑇𝑅)–1-1-onto→(({0, 1} ↑m ℕ) ∩ 𝑅))
24 fveq2 6906 . . . . . . . . . . . . . 14 (𝑞 = 𝑜 → (𝐺𝑞) = (𝐺𝑜))
25 reseq1 5991 . . . . . . . . . . . . . . . . . 18 (𝑞 = 𝑜 → (𝑞𝐽) = (𝑜𝐽))
2625coeq2d 5873 . . . . . . . . . . . . . . . . 17 (𝑞 = 𝑜 → (bits ∘ (𝑞𝐽)) = (bits ∘ (𝑜𝐽)))
2726fveq2d 6910 . . . . . . . . . . . . . . . 16 (𝑞 = 𝑜 → (𝑀‘(bits ∘ (𝑞𝐽))) = (𝑀‘(bits ∘ (𝑜𝐽))))
2827imaeq2d 6078 . . . . . . . . . . . . . . 15 (𝑞 = 𝑜 → (𝐹 “ (𝑀‘(bits ∘ (𝑞𝐽)))) = (𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽)))))
2928fveq2d 6910 . . . . . . . . . . . . . 14 (𝑞 = 𝑜 → ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑞𝐽))))) = ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽))))))
3024, 29eqeq12d 2753 . . . . . . . . . . . . 13 (𝑞 = 𝑜 → ((𝐺𝑞) = ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑞𝐽))))) ↔ (𝐺𝑜) = ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽)))))))
3113, 14, 15, 16, 17, 18, 19, 20, 21, 12eulerpartlemgv 34375 . . . . . . . . . . . . 13 (𝑞 ∈ (𝑇𝑅) → (𝐺𝑞) = ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑞𝐽))))))
3230, 31vtoclga 3577 . . . . . . . . . . . 12 (𝑜 ∈ (𝑇𝑅) → (𝐺𝑜) = ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽))))))
33323ad2ant2 1135 . . . . . . . . . . 11 ((⊤ ∧ 𝑜 ∈ (𝑇𝑅) ∧ 𝑑 = ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽)))))) → (𝐺𝑜) = ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽))))))
34 simp3 1139 . . . . . . . . . . 11 ((⊤ ∧ 𝑜 ∈ (𝑇𝑅) ∧ 𝑑 = ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽)))))) → 𝑑 = ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽))))))
3533, 34eqtr4d 2780 . . . . . . . . . 10 ((⊤ ∧ 𝑜 ∈ (𝑇𝑅) ∧ 𝑑 = ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽)))))) → (𝐺𝑜) = 𝑑)
3635fveq1d 6908 . . . . . . . . 9 ((⊤ ∧ 𝑜 ∈ (𝑇𝑅) ∧ 𝑑 = ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽)))))) → ((𝐺𝑜)‘𝑘) = (𝑑𝑘))
3736oveq1d 7446 . . . . . . . 8 ((⊤ ∧ 𝑜 ∈ (𝑇𝑅) ∧ 𝑑 = ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽)))))) → (((𝐺𝑜)‘𝑘) · 𝑘) = ((𝑑𝑘) · 𝑘))
3837sumeq2sdv 15739 . . . . . . 7 ((⊤ ∧ 𝑜 ∈ (𝑇𝑅) ∧ 𝑑 = ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽)))))) → Σ𝑘 ∈ ℕ (((𝐺𝑜)‘𝑘) · 𝑘) = Σ𝑘 ∈ ℕ ((𝑑𝑘) · 𝑘))
3924fveq2d 6910 . . . . . . . . . . 11 (𝑞 = 𝑜 → (𝑆‘(𝐺𝑞)) = (𝑆‘(𝐺𝑜)))
40 fveq2 6906 . . . . . . . . . . 11 (𝑞 = 𝑜 → (𝑆𝑞) = (𝑆𝑜))
4139, 40eqeq12d 2753 . . . . . . . . . 10 (𝑞 = 𝑜 → ((𝑆‘(𝐺𝑞)) = (𝑆𝑞) ↔ (𝑆‘(𝐺𝑜)) = (𝑆𝑜)))
42 eulerpart.s . . . . . . . . . . 11 𝑆 = (𝑓 ∈ ((ℕ0m ℕ) ∩ 𝑅) ↦ Σ𝑘 ∈ ℕ ((𝑓𝑘) · 𝑘))
4313, 14, 15, 16, 17, 18, 19, 20, 21, 12, 42eulerpartlemgs2 34382 . . . . . . . . . 10 (𝑞 ∈ (𝑇𝑅) → (𝑆‘(𝐺𝑞)) = (𝑆𝑞))
4441, 43vtoclga 3577 . . . . . . . . 9 (𝑜 ∈ (𝑇𝑅) → (𝑆‘(𝐺𝑜)) = (𝑆𝑜))
45 nn0ex 12532 . . . . . . . . . . . . 13 0 ∈ V
46 0nn0 12541 . . . . . . . . . . . . . 14 0 ∈ ℕ0
47 1nn0 12542 . . . . . . . . . . . . . 14 1 ∈ ℕ0
48 prssi 4821 . . . . . . . . . . . . . 14 ((0 ∈ ℕ0 ∧ 1 ∈ ℕ0) → {0, 1} ⊆ ℕ0)
4946, 47, 48mp2an 692 . . . . . . . . . . . . 13 {0, 1} ⊆ ℕ0
50 mapss 8929 . . . . . . . . . . . . 13 ((ℕ0 ∈ V ∧ {0, 1} ⊆ ℕ0) → ({0, 1} ↑m ℕ) ⊆ (ℕ0m ℕ))
5145, 49, 50mp2an 692 . . . . . . . . . . . 12 ({0, 1} ↑m ℕ) ⊆ (ℕ0m ℕ)
52 ssrin 4242 . . . . . . . . . . . 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 7103 . . . . . . . . . . 11 (𝑜 ∈ (𝑇𝑅) → (𝐺𝑜) ∈ (({0, 1} ↑m ℕ) ∩ 𝑅))
5753, 56sselid 3981 . . . . . . . . . 10 (𝑜 ∈ (𝑇𝑅) → (𝐺𝑜) ∈ ((ℕ0m ℕ) ∩ 𝑅))
5820, 42eulerpartlemsv1 34358 . . . . . . . . . 10 ((𝐺𝑜) ∈ ((ℕ0m ℕ) ∩ 𝑅) → (𝑆‘(𝐺𝑜)) = Σ𝑘 ∈ ℕ (((𝐺𝑜)‘𝑘) · 𝑘))
5957, 58syl 17 . . . . . . . . 9 (𝑜 ∈ (𝑇𝑅) → (𝑆‘(𝐺𝑜)) = Σ𝑘 ∈ ℕ (((𝐺𝑜)‘𝑘) · 𝑘))
6013, 14, 15, 16, 17, 18, 19, 20, 21eulerpartlemt0 34371 . . . . . . . . . . . 12 (𝑜 ∈ (𝑇𝑅) ↔ (𝑜 ∈ (ℕ0m ℕ) ∧ (𝑜 “ ℕ) ∈ Fin ∧ (𝑜 “ ℕ) ⊆ 𝐽))
6160simp1bi 1146 . . . . . . . . . . 11 (𝑜 ∈ (𝑇𝑅) → 𝑜 ∈ (ℕ0m ℕ))
62 inss2 4238 . . . . . . . . . . . 12 (𝑇𝑅) ⊆ 𝑅
6362sseli 3979 . . . . . . . . . . 11 (𝑜 ∈ (𝑇𝑅) → 𝑜𝑅)
6461, 63elind 4200 . . . . . . . . . 10 (𝑜 ∈ (𝑇𝑅) → 𝑜 ∈ ((ℕ0m ℕ) ∩ 𝑅))
6520, 42eulerpartlemsv1 34358 . . . . . . . . . 10 (𝑜 ∈ ((ℕ0m ℕ) ∩ 𝑅) → (𝑆𝑜) = Σ𝑘 ∈ ℕ ((𝑜𝑘) · 𝑘))
6664, 65syl 17 . . . . . . . . 9 (𝑜 ∈ (𝑇𝑅) → (𝑆𝑜) = Σ𝑘 ∈ ℕ ((𝑜𝑘) · 𝑘))
6744, 59, 663eqtr3d 2785 . . . . . . . 8 (𝑜 ∈ (𝑇𝑅) → Σ𝑘 ∈ ℕ (((𝐺𝑜)‘𝑘) · 𝑘) = Σ𝑘 ∈ ℕ ((𝑜𝑘) · 𝑘))
68673ad2ant2 1135 . . . . . . 7 ((⊤ ∧ 𝑜 ∈ (𝑇𝑅) ∧ 𝑑 = ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽)))))) → Σ𝑘 ∈ ℕ (((𝐺𝑜)‘𝑘) · 𝑘) = Σ𝑘 ∈ ℕ ((𝑜𝑘) · 𝑘))
6938, 68eqtr3d 2779 . . . . . 6 ((⊤ ∧ 𝑜 ∈ (𝑇𝑅) ∧ 𝑑 = ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽)))))) → Σ𝑘 ∈ ℕ ((𝑑𝑘) · 𝑘) = Σ𝑘 ∈ ℕ ((𝑜𝑘) · 𝑘))
7069eqeq1d 2739 . . . . 5 ((⊤ ∧ 𝑜 ∈ (𝑇𝑅) ∧ 𝑑 = ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽)))))) → (Σ𝑘 ∈ ℕ ((𝑑𝑘) · 𝑘) = 𝑁 ↔ Σ𝑘 ∈ ℕ ((𝑜𝑘) · 𝑘) = 𝑁))
7112, 23, 70f1oresrab 7147 . . . 4 (⊤ → (𝐺 ↾ {𝑜 ∈ (𝑇𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑜𝑘) · 𝑘) = 𝑁}):{𝑜 ∈ (𝑇𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑜𝑘) · 𝑘) = 𝑁}–1-1-onto→{𝑑 ∈ (({0, 1} ↑m ℕ) ∩ 𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑑𝑘) · 𝑘) = 𝑁})
7211, 71chvarvv 1998 . . 3 (⊤ → (𝐺 ↾ {𝑞 ∈ (𝑇𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑞𝑘) · 𝑘) = 𝑁}):{𝑞 ∈ (𝑇𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑞𝑘) · 𝑘) = 𝑁}–1-1-onto→{𝑑 ∈ (({0, 1} ↑m ℕ) ∩ 𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑑𝑘) · 𝑘) = 𝑁})
73 cnveq 5884 . . . . . . . . . 10 (𝑔 = 𝑞𝑔 = 𝑞)
7473imaeq1d 6077 . . . . . . . . 9 (𝑔 = 𝑞 → (𝑔 “ ℕ) = (𝑞 “ ℕ))
7574raleqdv 3326 . . . . . . . 8 (𝑔 = 𝑞 → (∀𝑛 ∈ (𝑔 “ ℕ) ¬ 2 ∥ 𝑛 ↔ ∀𝑛 ∈ (𝑞 “ ℕ) ¬ 2 ∥ 𝑛))
7675cbvrabv 3447 . . . . . . 7 {𝑔𝑃 ∣ ∀𝑛 ∈ (𝑔 “ ℕ) ¬ 2 ∥ 𝑛} = {𝑞𝑃 ∣ ∀𝑛 ∈ (𝑞 “ ℕ) ¬ 2 ∥ 𝑛}
77 nfrab1 3457 . . . . . . . 8 𝑞{𝑞𝑃 ∣ ∀𝑛 ∈ (𝑞 “ ℕ) ¬ 2 ∥ 𝑛}
78 nfrab1 3457 . . . . . . . 8 𝑞{𝑞 ∈ (𝑇𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑞𝑘) · 𝑘) = 𝑁}
79 df-3an 1089 . . . . . . . . . . . 12 ((𝑞:ℕ⟶ℕ0 ∧ (𝑞 “ ℕ) ∈ Fin ∧ Σ𝑘 ∈ ℕ ((𝑞𝑘) · 𝑘) = 𝑁) ↔ ((𝑞:ℕ⟶ℕ0 ∧ (𝑞 “ ℕ) ∈ Fin) ∧ Σ𝑘 ∈ ℕ ((𝑞𝑘) · 𝑘) = 𝑁))
8079anbi1i 624 . . . . . . . . . . 11 (((𝑞:ℕ⟶ℕ0 ∧ (𝑞 “ ℕ) ∈ Fin ∧ Σ𝑘 ∈ ℕ ((𝑞𝑘) · 𝑘) = 𝑁) ∧ ∀𝑛 ∈ (𝑞 “ ℕ) ¬ 2 ∥ 𝑛) ↔ (((𝑞:ℕ⟶ℕ0 ∧ (𝑞 “ ℕ) ∈ Fin) ∧ Σ𝑘 ∈ ℕ ((𝑞𝑘) · 𝑘) = 𝑁) ∧ ∀𝑛 ∈ (𝑞 “ ℕ) ¬ 2 ∥ 𝑛))
8113eulerpartleme 34365 . . . . . . . . . . . 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 34371 . . . . . . . . . . . . 13 (𝑞 ∈ (𝑇𝑅) ↔ (𝑞 ∈ (ℕ0m ℕ) ∧ (𝑞 “ ℕ) ∈ Fin ∧ (𝑞 “ ℕ) ⊆ 𝐽))
86 nnex 12272 . . . . . . . . . . . . . . 15 ℕ ∈ V
8745, 86elmap 8911 . . . . . . . . . . . . . 14 (𝑞 ∈ (ℕ0m ℕ) ↔ 𝑞:ℕ⟶ℕ0)
88873anbi1i 1158 . . . . . . . . . . . . 13 ((𝑞 ∈ (ℕ0m ℕ) ∧ (𝑞 “ ℕ) ∈ Fin ∧ (𝑞 “ ℕ) ⊆ 𝐽) ↔ (𝑞:ℕ⟶ℕ0 ∧ (𝑞 “ ℕ) ∈ Fin ∧ (𝑞 “ ℕ) ⊆ 𝐽))
8985, 88bitri 275 . . . . . . . . . . . 12 (𝑞 ∈ (𝑇𝑅) ↔ (𝑞:ℕ⟶ℕ0 ∧ (𝑞 “ ℕ) ∈ Fin ∧ (𝑞 “ ℕ) ⊆ 𝐽))
90 df-3an 1089 . . . . . . . . . . . 12 ((𝑞:ℕ⟶ℕ0 ∧ (𝑞 “ ℕ) ∈ Fin ∧ (𝑞 “ ℕ) ⊆ 𝐽) ↔ ((𝑞:ℕ⟶ℕ0 ∧ (𝑞 “ ℕ) ∈ Fin) ∧ (𝑞 “ ℕ) ⊆ 𝐽))
91 dfss3 3972 . . . . . . . . . . . . . . . 16 ((𝑞 “ ℕ) ⊆ 𝐽 ↔ ∀𝑛 ∈ (𝑞 “ ℕ)𝑛𝐽)
92 breq2 5147 . . . . . . . . . . . . . . . . . . 19 (𝑧 = 𝑛 → (2 ∥ 𝑧 ↔ 2 ∥ 𝑛))
9392notbid 318 . . . . . . . . . . . . . . . . . 18 (𝑧 = 𝑛 → (¬ 2 ∥ 𝑧 ↔ ¬ 2 ∥ 𝑛))
9493, 16elrab2 3695 . . . . . . . . . . . . . . . . 17 (𝑛𝐽 ↔ (𝑛 ∈ ℕ ∧ ¬ 2 ∥ 𝑛))
9594ralbii 3093 . . . . . . . . . . . . . . . 16 (∀𝑛 ∈ (𝑞 “ ℕ)𝑛𝐽 ↔ ∀𝑛 ∈ (𝑞 “ ℕ)(𝑛 ∈ ℕ ∧ ¬ 2 ∥ 𝑛))
96 r19.26 3111 . . . . . . . . . . . . . . . 16 (∀𝑛 ∈ (𝑞 “ ℕ)(𝑛 ∈ ℕ ∧ ¬ 2 ∥ 𝑛) ↔ (∀𝑛 ∈ (𝑞 “ ℕ)𝑛 ∈ ℕ ∧ ∀𝑛 ∈ (𝑞 “ ℕ) ¬ 2 ∥ 𝑛))
9791, 95, 963bitri 297 . . . . . . . . . . . . . . 15 ((𝑞 “ ℕ) ⊆ 𝐽 ↔ (∀𝑛 ∈ (𝑞 “ ℕ)𝑛 ∈ ℕ ∧ ∀𝑛 ∈ (𝑞 “ ℕ) ¬ 2 ∥ 𝑛))
98 cnvimass 6100 . . . . . . . . . . . . . . . . . 18 (𝑞 “ ℕ) ⊆ dom 𝑞
99 fdm 6745 . . . . . . . . . . . . . . . . . 18 (𝑞:ℕ⟶ℕ0 → dom 𝑞 = ℕ)
10098, 99sseqtrid 4026 . . . . . . . . . . . . . . . . 17 (𝑞:ℕ⟶ℕ0 → (𝑞 “ ℕ) ⊆ ℕ)
101 dfss3 3972 . . . . . . . . . . . . . . . . 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 3458 . . . . . . . . 9 (𝑞 ∈ {𝑞𝑃 ∣ ∀𝑛 ∈ (𝑞 “ ℕ) ¬ 2 ∥ 𝑛} ↔ (𝑞𝑃 ∧ ∀𝑛 ∈ (𝑞 “ ℕ) ¬ 2 ∥ 𝑛))
111 rabid 3458 . . . . . . . . 9 (𝑞 ∈ {𝑞 ∈ (𝑇𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑞𝑘) · 𝑘) = 𝑁} ↔ (𝑞 ∈ (𝑇𝑅) ∧ Σ𝑘 ∈ ℕ ((𝑞𝑘) · 𝑘) = 𝑁))
112109, 110, 1113bitr4i 303 . . . . . . . 8 (𝑞 ∈ {𝑞𝑃 ∣ ∀𝑛 ∈ (𝑞 “ ℕ) ¬ 2 ∥ 𝑛} ↔ 𝑞 ∈ {𝑞 ∈ (𝑇𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑞𝑘) · 𝑘) = 𝑁})
11377, 78, 112eqri 4004 . . . . . . 7 {𝑞𝑃 ∣ ∀𝑛 ∈ (𝑞 “ ℕ) ¬ 2 ∥ 𝑛} = {𝑞 ∈ (𝑇𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑞𝑘) · 𝑘) = 𝑁}
11414, 76, 1133eqtri 2769 . . . . . 6 𝑂 = {𝑞 ∈ (𝑇𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑞𝑘) · 𝑘) = 𝑁}
115114reseq2i 5994 . . . . 5 (𝐺𝑂) = (𝐺 ↾ {𝑞 ∈ (𝑇𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑞𝑘) · 𝑘) = 𝑁})
116115a1i 11 . . . 4 (⊤ → (𝐺𝑂) = (𝐺 ↾ {𝑞 ∈ (𝑇𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑞𝑘) · 𝑘) = 𝑁}))
117114a1i 11 . . . 4 (⊤ → 𝑂 = {𝑞 ∈ (𝑇𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑞𝑘) · 𝑘) = 𝑁})
118 nfcv 2905 . . . . . 6 𝑑𝐷
119 nfrab1 3457 . . . . . 6 𝑑{𝑑 ∈ (({0, 1} ↑m ℕ) ∩ 𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑑𝑘) · 𝑘) = 𝑁}
120 fnima 6698 . . . . . . . . . . . . . . . . 17 (𝑑 Fn ℕ → (𝑑 “ ℕ) = ran 𝑑)
121120sseq1d 4015 . . . . . . . . . . . . . . . 16 (𝑑 Fn ℕ → ((𝑑 “ ℕ) ⊆ {0, 1} ↔ ran 𝑑 ⊆ {0, 1}))
122121anbi2d 630 . . . . . . . . . . . . . . 15 (𝑑 Fn ℕ → ((ran 𝑑 ⊆ ℕ0 ∧ (𝑑 “ ℕ) ⊆ {0, 1}) ↔ (ran 𝑑 ⊆ ℕ0 ∧ ran 𝑑 ⊆ {0, 1})))
123 sstr 3992 . . . . . . . . . . . . . . . . 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 6565 . . . . . . . . . . . . 13 (𝑑:ℕ⟶{0, 1} ↔ (𝑑 Fn ℕ ∧ ran 𝑑 ⊆ {0, 1}))
130127, 128, 1293bitr4ri 304 . . . . . . . . . . . 12 (𝑑:ℕ⟶{0, 1} ↔ ((𝑑 Fn ℕ ∧ ran 𝑑 ⊆ ℕ0) ∧ (𝑑 “ ℕ) ⊆ {0, 1}))
131 prex 5437 . . . . . . . . . . . . 13 {0, 1} ∈ V
132131, 86elmap 8911 . . . . . . . . . . . 12 (𝑑 ∈ ({0, 1} ↑m ℕ) ↔ 𝑑:ℕ⟶{0, 1})
133 df-f 6565 . . . . . . . . . . . . 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 3484 . . . . . . . . . . . 12 𝑑 ∈ V
137 cnveq 5884 . . . . . . . . . . . . . 14 (𝑓 = 𝑑𝑓 = 𝑑)
138137imaeq1d 6077 . . . . . . . . . . . . 13 (𝑓 = 𝑑 → (𝑓 “ ℕ) = (𝑑 “ ℕ))
139138eleq1d 2826 . . . . . . . . . . . 12 (𝑓 = 𝑑 → ((𝑓 “ ℕ) ∈ Fin ↔ (𝑑 “ ℕ) ∈ Fin))
140136, 139, 20elab2 3682 . . . . . . . . . . 11 (𝑑𝑅 ↔ (𝑑 “ ℕ) ∈ Fin)
141135, 140anbi12i 628 . . . . . . . . . 10 ((𝑑 ∈ ({0, 1} ↑m ℕ) ∧ 𝑑𝑅) ↔ ((𝑑:ℕ⟶ℕ0 ∧ (𝑑 “ ℕ) ⊆ {0, 1}) ∧ (𝑑 “ ℕ) ∈ Fin))
142 elin 3967 . . . . . . . . . 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 34365 . . . . . . . . . 10 (𝑑𝑃 ↔ (𝑑:ℕ⟶ℕ0 ∧ (𝑑 “ ℕ) ∈ Fin ∧ Σ𝑘 ∈ ℕ ((𝑑𝑘) · 𝑘) = 𝑁))
147146anbi1i 624 . . . . . . . . 9 ((𝑑𝑃 ∧ (𝑑 “ ℕ) ⊆ {0, 1}) ↔ ((𝑑:ℕ⟶ℕ0 ∧ (𝑑 “ ℕ) ∈ Fin ∧ Σ𝑘 ∈ ℕ ((𝑑𝑘) · 𝑘) = 𝑁) ∧ (𝑑 “ ℕ) ⊆ {0, 1}))
148 df-3an 1089 . . . . . . . . . 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 3458 . . . . . . 7 (𝑑 ∈ {𝑑 ∈ (({0, 1} ↑m ℕ) ∩ 𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑑𝑘) · 𝑘) = 𝑁} ↔ (𝑑 ∈ (({0, 1} ↑m ℕ) ∩ 𝑅) ∧ Σ𝑘 ∈ ℕ ((𝑑𝑘) · 𝑘) = 𝑁))
15413, 14, 15eulerpartlemd 34368 . . . . . . 7 (𝑑𝐷 ↔ (𝑑𝑃 ∧ (𝑑 “ ℕ) ⊆ {0, 1}))
155152, 153, 1543bitr4ri 304 . . . . . 6 (𝑑𝐷𝑑 ∈ {𝑑 ∈ (({0, 1} ↑m ℕ) ∩ 𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑑𝑘) · 𝑘) = 𝑁})
156118, 119, 155eqri 4004 . . . . 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 1547 1 (𝐺𝑂):𝑂1-1-onto𝐷
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wa 395  w3a 1087   = wceq 1540  wtru 1541  wcel 2108  {cab 2714  wral 3061  {crab 3436  Vcvv 3480  cin 3950  wss 3951  c0 4333  𝒫 cpw 4600  {cpr 4628   class class class wbr 5143  {copab 5205  cmpt 5225  ccnv 5684  dom cdm 5685  ran crn 5686  cres 5687  cima 5688  ccom 5689   Fn wfn 6556  wf 6557  1-1-ontowf1o 6560  cfv 6561  (class class class)co 7431  cmpo 7433   supp csupp 8185  m cmap 8866  Fincfn 8985  0cc0 11155  1c1 11156   · cmul 11160  cle 11296  cn 12266  2c2 12321  0cn0 12526  cexp 14102  Σcsu 15722  cdvds 16290  bitscbits 16456  𝟭cind 32835
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-rep 5279  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755  ax-inf2 9681  ax-ac2 10503  ax-cnex 11211  ax-resscn 11212  ax-1cn 11213  ax-icn 11214  ax-addcl 11215  ax-addrcl 11216  ax-mulcl 11217  ax-mulrcl 11218  ax-mulcom 11219  ax-addass 11220  ax-mulass 11221  ax-distr 11222  ax-i2m1 11223  ax-1ne0 11224  ax-1rid 11225  ax-rnegex 11226  ax-rrecex 11227  ax-cnre 11228  ax-pre-lttri 11229  ax-pre-lttrn 11230  ax-pre-ltadd 11231  ax-pre-mulgt0 11232  ax-pre-sup 11233
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3380  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-pss 3971  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-int 4947  df-iun 4993  df-disj 5111  df-br 5144  df-opab 5206  df-mpt 5226  df-tr 5260  df-id 5578  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-se 5638  df-we 5639  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-pred 6321  df-ord 6387  df-on 6388  df-lim 6389  df-suc 6390  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-isom 6570  df-riota 7388  df-ov 7434  df-oprab 7435  df-mpo 7436  df-om 7888  df-1st 8014  df-2nd 8015  df-supp 8186  df-frecs 8306  df-wrecs 8337  df-recs 8411  df-rdg 8450  df-1o 8506  df-2o 8507  df-oadd 8510  df-er 8745  df-map 8868  df-pm 8869  df-en 8986  df-dom 8987  df-sdom 8988  df-fin 8989  df-fsupp 9402  df-sup 9482  df-inf 9483  df-oi 9550  df-dju 9941  df-card 9979  df-acn 9982  df-ac 10156  df-pnf 11297  df-mnf 11298  df-xr 11299  df-ltxr 11300  df-le 11301  df-sub 11494  df-neg 11495  df-div 11921  df-nn 12267  df-2 12329  df-3 12330  df-n0 12527  df-xnn0 12600  df-z 12614  df-uz 12879  df-rp 13035  df-fz 13548  df-fzo 13695  df-fl 13832  df-mod 13910  df-seq 14043  df-exp 14103  df-hash 14370  df-cj 15138  df-re 15139  df-im 15140  df-sqrt 15274  df-abs 15275  df-clim 15524  df-sum 15723  df-dvds 16291  df-bits 16459  df-ind 32836
This theorem is referenced by:  eulerpart  34384
  Copyright terms: Public domain W3C validator