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 29564
Description: Lemma for eulerpart 29565. (Contributed by Thierry Arnoux, 30-Aug-2018.)
Hypotheses
Ref Expression
eulerpart.p 𝑃 = {𝑓 ∈ (ℕ0𝑚 ℕ) ∣ ((𝑓 “ ℕ) ∈ Fin ∧ Σ𝑘 ∈ ℕ ((𝑓𝑘) · 𝑘) = 𝑁)}
eulerpart.o 𝑂 = {𝑔𝑃 ∣ ∀𝑛 ∈ (𝑔 “ ℕ) ¬ 2 ∥ 𝑛}
eulerpart.d 𝐷 = {𝑔𝑃 ∣ ∀𝑛 ∈ ℕ (𝑔𝑛) ≤ 1}
eulerpart.j 𝐽 = {𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧}
eulerpart.f 𝐹 = (𝑥𝐽, 𝑦 ∈ ℕ0 ↦ ((2↑𝑦) · 𝑥))
eulerpart.h 𝐻 = {𝑟 ∈ ((𝒫 ℕ0 ∩ Fin) ↑𝑚 𝐽) ∣ (𝑟 supp ∅) ∈ Fin}
eulerpart.m 𝑀 = (𝑟𝐻 ↦ {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐽𝑦 ∈ (𝑟𝑥))})
eulerpart.r 𝑅 = {𝑓 ∣ (𝑓 “ ℕ) ∈ Fin}
eulerpart.t 𝑇 = {𝑓 ∈ (ℕ0𝑚 ℕ) ∣ (𝑓 “ ℕ) ⊆ 𝐽}
eulerpart.g 𝐺 = (𝑜 ∈ (𝑇𝑅) ↦ ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽))))))
eulerpart.s 𝑆 = (𝑓 ∈ ((ℕ0𝑚 ℕ) ∩ 𝑅) ↦ Σ𝑘 ∈ ℕ ((𝑓𝑘) · 𝑘))
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 472 . . . . . . . . . . . . 13 ((𝑜 = 𝑞𝑘 ∈ ℕ) → 𝑜 = 𝑞)
21fveq1d 6090 . . . . . . . . . . . 12 ((𝑜 = 𝑞𝑘 ∈ ℕ) → (𝑜𝑘) = (𝑞𝑘))
32oveq1d 6542 . . . . . . . . . . 11 ((𝑜 = 𝑞𝑘 ∈ ℕ) → ((𝑜𝑘) · 𝑘) = ((𝑞𝑘) · 𝑘))
43sumeq2dv 14230 . . . . . . . . . 10 (𝑜 = 𝑞 → Σ𝑘 ∈ ℕ ((𝑜𝑘) · 𝑘) = Σ𝑘 ∈ ℕ ((𝑞𝑘) · 𝑘))
54eqeq1d 2612 . . . . . . . . 9 (𝑜 = 𝑞 → (Σ𝑘 ∈ ℕ ((𝑜𝑘) · 𝑘) = 𝑁 ↔ Σ𝑘 ∈ ℕ ((𝑞𝑘) · 𝑘) = 𝑁))
65cbvrabv 3172 . . . . . . . 8 {𝑜 ∈ (𝑇𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑜𝑘) · 𝑘) = 𝑁} = {𝑞 ∈ (𝑇𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑞𝑘) · 𝑘) = 𝑁}
76a1i 11 . . . . . . 7 (𝑜 = 𝑞 → {𝑜 ∈ (𝑇𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑜𝑘) · 𝑘) = 𝑁} = {𝑞 ∈ (𝑇𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑞𝑘) · 𝑘) = 𝑁})
87reseq2d 5304 . . . . . 6 (𝑜 = 𝑞 → (𝐺 ↾ {𝑜 ∈ (𝑇𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑜𝑘) · 𝑘) = 𝑁}) = (𝐺 ↾ {𝑞 ∈ (𝑇𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑞𝑘) · 𝑘) = 𝑁}))
9 eqidd 2611 . . . . . 6 (𝑜 = 𝑞 → {𝑑 ∈ (({0, 1} ↑𝑚 ℕ) ∩ 𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑑𝑘) · 𝑘) = 𝑁} = {𝑑 ∈ (({0, 1} ↑𝑚 ℕ) ∩ 𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑑𝑘) · 𝑘) = 𝑁})
108, 7, 9f1oeq123d 6031 . . . . 5 (𝑜 = 𝑞 → ((𝐺 ↾ {𝑜 ∈ (𝑇𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑜𝑘) · 𝑘) = 𝑁}):{𝑜 ∈ (𝑇𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑜𝑘) · 𝑘) = 𝑁}–1-1-onto→{𝑑 ∈ (({0, 1} ↑𝑚 ℕ) ∩ 𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑑𝑘) · 𝑘) = 𝑁} ↔ (𝐺 ↾ {𝑞 ∈ (𝑇𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑞𝑘) · 𝑘) = 𝑁}):{𝑞 ∈ (𝑇𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑞𝑘) · 𝑘) = 𝑁}–1-1-onto→{𝑑 ∈ (({0, 1} ↑𝑚 ℕ) ∩ 𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑑𝑘) · 𝑘) = 𝑁}))
1110imbi2d 329 . . . 4 (𝑜 = 𝑞 → ((⊤ → (𝐺 ↾ {𝑜 ∈ (𝑇𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑜𝑘) · 𝑘) = 𝑁}):{𝑜 ∈ (𝑇𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑜𝑘) · 𝑘) = 𝑁}–1-1-onto→{𝑑 ∈ (({0, 1} ↑𝑚 ℕ) ∩ 𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑑𝑘) · 𝑘) = 𝑁}) ↔ (⊤ → (𝐺 ↾ {𝑞 ∈ (𝑇𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑞𝑘) · 𝑘) = 𝑁}):{𝑞 ∈ (𝑇𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑞𝑘) · 𝑘) = 𝑁}–1-1-onto→{𝑑 ∈ (({0, 1} ↑𝑚 ℕ) ∩ 𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑑𝑘) · 𝑘) = 𝑁})))
12 eulerpart.g . . . . 5 𝐺 = (𝑜 ∈ (𝑇𝑅) ↦ ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽))))))
13 eulerpart.p . . . . . . 7 𝑃 = {𝑓 ∈ (ℕ0𝑚 ℕ) ∣ ((𝑓 “ ℕ) ∈ 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) ↑𝑚 𝐽) ∣ (𝑟 supp ∅) ∈ Fin}
19 eulerpart.m . . . . . . 7 𝑀 = (𝑟𝐻 ↦ {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐽𝑦 ∈ (𝑟𝑥))})
20 eulerpart.r . . . . . . 7 𝑅 = {𝑓 ∣ (𝑓 “ ℕ) ∈ Fin}
21 eulerpart.t . . . . . . 7 𝑇 = {𝑓 ∈ (ℕ0𝑚 ℕ) ∣ (𝑓 “ ℕ) ⊆ 𝐽}
2213, 14, 15, 16, 17, 18, 19, 20, 21, 12eulerpartgbij 29555 . . . . . 6 𝐺:(𝑇𝑅)–1-1-onto→(({0, 1} ↑𝑚 ℕ) ∩ 𝑅)
2322a1i 11 . . . . 5 (⊤ → 𝐺:(𝑇𝑅)–1-1-onto→(({0, 1} ↑𝑚 ℕ) ∩ 𝑅))
24 fveq2 6088 . . . . . . . . . . . . . 14 (𝑞 = 𝑜 → (𝐺𝑞) = (𝐺𝑜))
25 reseq1 5298 . . . . . . . . . . . . . . . . . 18 (𝑞 = 𝑜 → (𝑞𝐽) = (𝑜𝐽))
2625coeq2d 5194 . . . . . . . . . . . . . . . . 17 (𝑞 = 𝑜 → (bits ∘ (𝑞𝐽)) = (bits ∘ (𝑜𝐽)))
2726fveq2d 6092 . . . . . . . . . . . . . . . 16 (𝑞 = 𝑜 → (𝑀‘(bits ∘ (𝑞𝐽))) = (𝑀‘(bits ∘ (𝑜𝐽))))
2827imaeq2d 5372 . . . . . . . . . . . . . . 15 (𝑞 = 𝑜 → (𝐹 “ (𝑀‘(bits ∘ (𝑞𝐽)))) = (𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽)))))
2928fveq2d 6092 . . . . . . . . . . . . . 14 (𝑞 = 𝑜 → ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑞𝐽))))) = ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽))))))
3024, 29eqeq12d 2625 . . . . . . . . . . . . 13 (𝑞 = 𝑜 → ((𝐺𝑞) = ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑞𝐽))))) ↔ (𝐺𝑜) = ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽)))))))
3113, 14, 15, 16, 17, 18, 19, 20, 21, 12eulerpartlemgv 29556 . . . . . . . . . . . . 13 (𝑞 ∈ (𝑇𝑅) → (𝐺𝑞) = ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑞𝐽))))))
3230, 31vtoclga 3245 . . . . . . . . . . . 12 (𝑜 ∈ (𝑇𝑅) → (𝐺𝑜) = ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽))))))
33323ad2ant2 1076 . . . . . . . . . . 11 ((⊤ ∧ 𝑜 ∈ (𝑇𝑅) ∧ 𝑑 = ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽)))))) → (𝐺𝑜) = ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽))))))
34 simp3 1056 . . . . . . . . . . 11 ((⊤ ∧ 𝑜 ∈ (𝑇𝑅) ∧ 𝑑 = ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽)))))) → 𝑑 = ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽))))))
3533, 34eqtr4d 2647 . . . . . . . . . 10 ((⊤ ∧ 𝑜 ∈ (𝑇𝑅) ∧ 𝑑 = ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽)))))) → (𝐺𝑜) = 𝑑)
3635fveq1d 6090 . . . . . . . . 9 ((⊤ ∧ 𝑜 ∈ (𝑇𝑅) ∧ 𝑑 = ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽)))))) → ((𝐺𝑜)‘𝑘) = (𝑑𝑘))
3736oveq1d 6542 . . . . . . . 8 ((⊤ ∧ 𝑜 ∈ (𝑇𝑅) ∧ 𝑑 = ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽)))))) → (((𝐺𝑜)‘𝑘) · 𝑘) = ((𝑑𝑘) · 𝑘))
3837sumeq2sdv 14231 . . . . . . 7 ((⊤ ∧ 𝑜 ∈ (𝑇𝑅) ∧ 𝑑 = ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽)))))) → Σ𝑘 ∈ ℕ (((𝐺𝑜)‘𝑘) · 𝑘) = Σ𝑘 ∈ ℕ ((𝑑𝑘) · 𝑘))
3924fveq2d 6092 . . . . . . . . . . 11 (𝑞 = 𝑜 → (𝑆‘(𝐺𝑞)) = (𝑆‘(𝐺𝑜)))
40 fveq2 6088 . . . . . . . . . . 11 (𝑞 = 𝑜 → (𝑆𝑞) = (𝑆𝑜))
4139, 40eqeq12d 2625 . . . . . . . . . 10 (𝑞 = 𝑜 → ((𝑆‘(𝐺𝑞)) = (𝑆𝑞) ↔ (𝑆‘(𝐺𝑜)) = (𝑆𝑜)))
42 eulerpart.s . . . . . . . . . . 11 𝑆 = (𝑓 ∈ ((ℕ0𝑚 ℕ) ∩ 𝑅) ↦ Σ𝑘 ∈ ℕ ((𝑓𝑘) · 𝑘))
4313, 14, 15, 16, 17, 18, 19, 20, 21, 12, 42eulerpartlemgs2 29563 . . . . . . . . . 10 (𝑞 ∈ (𝑇𝑅) → (𝑆‘(𝐺𝑞)) = (𝑆𝑞))
4441, 43vtoclga 3245 . . . . . . . . 9 (𝑜 ∈ (𝑇𝑅) → (𝑆‘(𝐺𝑜)) = (𝑆𝑜))
45 nn0ex 11148 . . . . . . . . . . . . 13 0 ∈ V
46 0nn0 11157 . . . . . . . . . . . . . 14 0 ∈ ℕ0
47 1nn0 11158 . . . . . . . . . . . . . 14 1 ∈ ℕ0
48 prssi 4293 . . . . . . . . . . . . . 14 ((0 ∈ ℕ0 ∧ 1 ∈ ℕ0) → {0, 1} ⊆ ℕ0)
4946, 47, 48mp2an 704 . . . . . . . . . . . . 13 {0, 1} ⊆ ℕ0
50 mapss 7764 . . . . . . . . . . . . 13 ((ℕ0 ∈ V ∧ {0, 1} ⊆ ℕ0) → ({0, 1} ↑𝑚 ℕ) ⊆ (ℕ0𝑚 ℕ))
5145, 49, 50mp2an 704 . . . . . . . . . . . 12 ({0, 1} ↑𝑚 ℕ) ⊆ (ℕ0𝑚 ℕ)
52 ssrin 3800 . . . . . . . . . . . 12 (({0, 1} ↑𝑚 ℕ) ⊆ (ℕ0𝑚 ℕ) → (({0, 1} ↑𝑚 ℕ) ∩ 𝑅) ⊆ ((ℕ0𝑚 ℕ) ∩ 𝑅))
5351, 52ax-mp 5 . . . . . . . . . . 11 (({0, 1} ↑𝑚 ℕ) ∩ 𝑅) ⊆ ((ℕ0𝑚 ℕ) ∩ 𝑅)
54 f1of 6035 . . . . . . . . . . . . 13 (𝐺:(𝑇𝑅)–1-1-onto→(({0, 1} ↑𝑚 ℕ) ∩ 𝑅) → 𝐺:(𝑇𝑅)⟶(({0, 1} ↑𝑚 ℕ) ∩ 𝑅))
5522, 54ax-mp 5 . . . . . . . . . . . 12 𝐺:(𝑇𝑅)⟶(({0, 1} ↑𝑚 ℕ) ∩ 𝑅)
5655ffvelrni 6251 . . . . . . . . . . 11 (𝑜 ∈ (𝑇𝑅) → (𝐺𝑜) ∈ (({0, 1} ↑𝑚 ℕ) ∩ 𝑅))
5753, 56sseldi 3566 . . . . . . . . . 10 (𝑜 ∈ (𝑇𝑅) → (𝐺𝑜) ∈ ((ℕ0𝑚 ℕ) ∩ 𝑅))
5820, 42eulerpartlemsv1 29539 . . . . . . . . . 10 ((𝐺𝑜) ∈ ((ℕ0𝑚 ℕ) ∩ 𝑅) → (𝑆‘(𝐺𝑜)) = Σ𝑘 ∈ ℕ (((𝐺𝑜)‘𝑘) · 𝑘))
5957, 58syl 17 . . . . . . . . 9 (𝑜 ∈ (𝑇𝑅) → (𝑆‘(𝐺𝑜)) = Σ𝑘 ∈ ℕ (((𝐺𝑜)‘𝑘) · 𝑘))
6013, 14, 15, 16, 17, 18, 19, 20, 21eulerpartlemt0 29552 . . . . . . . . . . . 12 (𝑜 ∈ (𝑇𝑅) ↔ (𝑜 ∈ (ℕ0𝑚 ℕ) ∧ (𝑜 “ ℕ) ∈ Fin ∧ (𝑜 “ ℕ) ⊆ 𝐽))
6160simp1bi 1069 . . . . . . . . . . 11 (𝑜 ∈ (𝑇𝑅) → 𝑜 ∈ (ℕ0𝑚 ℕ))
62 inss2 3796 . . . . . . . . . . . 12 (𝑇𝑅) ⊆ 𝑅
6362sseli 3564 . . . . . . . . . . 11 (𝑜 ∈ (𝑇𝑅) → 𝑜𝑅)
6461, 63elind 3760 . . . . . . . . . 10 (𝑜 ∈ (𝑇𝑅) → 𝑜 ∈ ((ℕ0𝑚 ℕ) ∩ 𝑅))
6520, 42eulerpartlemsv1 29539 . . . . . . . . . 10 (𝑜 ∈ ((ℕ0𝑚 ℕ) ∩ 𝑅) → (𝑆𝑜) = Σ𝑘 ∈ ℕ ((𝑜𝑘) · 𝑘))
6664, 65syl 17 . . . . . . . . 9 (𝑜 ∈ (𝑇𝑅) → (𝑆𝑜) = Σ𝑘 ∈ ℕ ((𝑜𝑘) · 𝑘))
6744, 59, 663eqtr3d 2652 . . . . . . . 8 (𝑜 ∈ (𝑇𝑅) → Σ𝑘 ∈ ℕ (((𝐺𝑜)‘𝑘) · 𝑘) = Σ𝑘 ∈ ℕ ((𝑜𝑘) · 𝑘))
68673ad2ant2 1076 . . . . . . 7 ((⊤ ∧ 𝑜 ∈ (𝑇𝑅) ∧ 𝑑 = ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽)))))) → Σ𝑘 ∈ ℕ (((𝐺𝑜)‘𝑘) · 𝑘) = Σ𝑘 ∈ ℕ ((𝑜𝑘) · 𝑘))
6938, 68eqtr3d 2646 . . . . . 6 ((⊤ ∧ 𝑜 ∈ (𝑇𝑅) ∧ 𝑑 = ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽)))))) → Σ𝑘 ∈ ℕ ((𝑑𝑘) · 𝑘) = Σ𝑘 ∈ ℕ ((𝑜𝑘) · 𝑘))
7069eqeq1d 2612 . . . . 5 ((⊤ ∧ 𝑜 ∈ (𝑇𝑅) ∧ 𝑑 = ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽)))))) → (Σ𝑘 ∈ ℕ ((𝑑𝑘) · 𝑘) = 𝑁 ↔ Σ𝑘 ∈ ℕ ((𝑜𝑘) · 𝑘) = 𝑁))
7112, 23, 70f1oresrab 6287 . . . 4 (⊤ → (𝐺 ↾ {𝑜 ∈ (𝑇𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑜𝑘) · 𝑘) = 𝑁}):{𝑜 ∈ (𝑇𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑜𝑘) · 𝑘) = 𝑁}–1-1-onto→{𝑑 ∈ (({0, 1} ↑𝑚 ℕ) ∩ 𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑑𝑘) · 𝑘) = 𝑁})
7211, 71chvarv 2251 . . 3 (⊤ → (𝐺 ↾ {𝑞 ∈ (𝑇𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑞𝑘) · 𝑘) = 𝑁}):{𝑞 ∈ (𝑇𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑞𝑘) · 𝑘) = 𝑁}–1-1-onto→{𝑑 ∈ (({0, 1} ↑𝑚 ℕ) ∩ 𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑑𝑘) · 𝑘) = 𝑁})
73 cnveq 5206 . . . . . . . . . 10 (𝑔 = 𝑞𝑔 = 𝑞)
7473imaeq1d 5371 . . . . . . . . 9 (𝑔 = 𝑞 → (𝑔 “ ℕ) = (𝑞 “ ℕ))
7574raleqdv 3121 . . . . . . . 8 (𝑔 = 𝑞 → (∀𝑛 ∈ (𝑔 “ ℕ) ¬ 2 ∥ 𝑛 ↔ ∀𝑛 ∈ (𝑞 “ ℕ) ¬ 2 ∥ 𝑛))
7675cbvrabv 3172 . . . . . . 7 {𝑔𝑃 ∣ ∀𝑛 ∈ (𝑔 “ ℕ) ¬ 2 ∥ 𝑛} = {𝑞𝑃 ∣ ∀𝑛 ∈ (𝑞 “ ℕ) ¬ 2 ∥ 𝑛}
77 nfrab1 3099 . . . . . . . 8 𝑞{𝑞𝑃 ∣ ∀𝑛 ∈ (𝑞 “ ℕ) ¬ 2 ∥ 𝑛}
78 nfrab1 3099 . . . . . . . 8 𝑞{𝑞 ∈ (𝑇𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑞𝑘) · 𝑘) = 𝑁}
79 df-3an 1033 . . . . . . . . . . . 12 ((𝑞:ℕ⟶ℕ0 ∧ (𝑞 “ ℕ) ∈ Fin ∧ Σ𝑘 ∈ ℕ ((𝑞𝑘) · 𝑘) = 𝑁) ↔ ((𝑞:ℕ⟶ℕ0 ∧ (𝑞 “ ℕ) ∈ Fin) ∧ Σ𝑘 ∈ ℕ ((𝑞𝑘) · 𝑘) = 𝑁))
8079anbi1i 727 . . . . . . . . . . 11 (((𝑞:ℕ⟶ℕ0 ∧ (𝑞 “ ℕ) ∈ Fin ∧ Σ𝑘 ∈ ℕ ((𝑞𝑘) · 𝑘) = 𝑁) ∧ ∀𝑛 ∈ (𝑞 “ ℕ) ¬ 2 ∥ 𝑛) ↔ (((𝑞:ℕ⟶ℕ0 ∧ (𝑞 “ ℕ) ∈ Fin) ∧ Σ𝑘 ∈ ℕ ((𝑞𝑘) · 𝑘) = 𝑁) ∧ ∀𝑛 ∈ (𝑞 “ ℕ) ¬ 2 ∥ 𝑛))
8113eulerpartleme 29546 . . . . . . . . . . . 12 (𝑞𝑃 ↔ (𝑞:ℕ⟶ℕ0 ∧ (𝑞 “ ℕ) ∈ Fin ∧ Σ𝑘 ∈ ℕ ((𝑞𝑘) · 𝑘) = 𝑁))
8281anbi1i 727 . . . . . . . . . . 11 ((𝑞𝑃 ∧ ∀𝑛 ∈ (𝑞 “ ℕ) ¬ 2 ∥ 𝑛) ↔ ((𝑞:ℕ⟶ℕ0 ∧ (𝑞 “ ℕ) ∈ Fin ∧ Σ𝑘 ∈ ℕ ((𝑞𝑘) · 𝑘) = 𝑁) ∧ ∀𝑛 ∈ (𝑞 “ ℕ) ¬ 2 ∥ 𝑛))
83 an32 835 . . . . . . . . . . 11 ((((𝑞:ℕ⟶ℕ0 ∧ (𝑞 “ ℕ) ∈ Fin) ∧ ∀𝑛 ∈ (𝑞 “ ℕ) ¬ 2 ∥ 𝑛) ∧ Σ𝑘 ∈ ℕ ((𝑞𝑘) · 𝑘) = 𝑁) ↔ (((𝑞:ℕ⟶ℕ0 ∧ (𝑞 “ ℕ) ∈ Fin) ∧ Σ𝑘 ∈ ℕ ((𝑞𝑘) · 𝑘) = 𝑁) ∧ ∀𝑛 ∈ (𝑞 “ ℕ) ¬ 2 ∥ 𝑛))
8480, 82, 833bitr4i 291 . . . . . . . . . 10 ((𝑞𝑃 ∧ ∀𝑛 ∈ (𝑞 “ ℕ) ¬ 2 ∥ 𝑛) ↔ (((𝑞:ℕ⟶ℕ0 ∧ (𝑞 “ ℕ) ∈ Fin) ∧ ∀𝑛 ∈ (𝑞 “ ℕ) ¬ 2 ∥ 𝑛) ∧ Σ𝑘 ∈ ℕ ((𝑞𝑘) · 𝑘) = 𝑁))
8513, 14, 15, 16, 17, 18, 19, 20, 21eulerpartlemt0 29552 . . . . . . . . . . . . 13 (𝑞 ∈ (𝑇𝑅) ↔ (𝑞 ∈ (ℕ0𝑚 ℕ) ∧ (𝑞 “ ℕ) ∈ Fin ∧ (𝑞 “ ℕ) ⊆ 𝐽))
86 nnex 10876 . . . . . . . . . . . . . . 15 ℕ ∈ V
8745, 86elmap 7750 . . . . . . . . . . . . . 14 (𝑞 ∈ (ℕ0𝑚 ℕ) ↔ 𝑞:ℕ⟶ℕ0)
88873anbi1i 1246 . . . . . . . . . . . . 13 ((𝑞 ∈ (ℕ0𝑚 ℕ) ∧ (𝑞 “ ℕ) ∈ Fin ∧ (𝑞 “ ℕ) ⊆ 𝐽) ↔ (𝑞:ℕ⟶ℕ0 ∧ (𝑞 “ ℕ) ∈ Fin ∧ (𝑞 “ ℕ) ⊆ 𝐽))
8985, 88bitri 263 . . . . . . . . . . . 12 (𝑞 ∈ (𝑇𝑅) ↔ (𝑞:ℕ⟶ℕ0 ∧ (𝑞 “ ℕ) ∈ Fin ∧ (𝑞 “ ℕ) ⊆ 𝐽))
90 df-3an 1033 . . . . . . . . . . . 12 ((𝑞:ℕ⟶ℕ0 ∧ (𝑞 “ ℕ) ∈ Fin ∧ (𝑞 “ ℕ) ⊆ 𝐽) ↔ ((𝑞:ℕ⟶ℕ0 ∧ (𝑞 “ ℕ) ∈ Fin) ∧ (𝑞 “ ℕ) ⊆ 𝐽))
91 cnvimass 5391 . . . . . . . . . . . . . . . . . 18 (𝑞 “ ℕ) ⊆ dom 𝑞
92 fdm 5950 . . . . . . . . . . . . . . . . . 18 (𝑞:ℕ⟶ℕ0 → dom 𝑞 = ℕ)
9391, 92syl5sseq 3616 . . . . . . . . . . . . . . . . 17 (𝑞:ℕ⟶ℕ0 → (𝑞 “ ℕ) ⊆ ℕ)
94 dfss3 3558 . . . . . . . . . . . . . . . . 17 ((𝑞 “ ℕ) ⊆ ℕ ↔ ∀𝑛 ∈ (𝑞 “ ℕ)𝑛 ∈ ℕ)
9593, 94sylib 207 . . . . . . . . . . . . . . . 16 (𝑞:ℕ⟶ℕ0 → ∀𝑛 ∈ (𝑞 “ ℕ)𝑛 ∈ ℕ)
9695biantrurd 528 . . . . . . . . . . . . . . 15 (𝑞:ℕ⟶ℕ0 → (∀𝑛 ∈ (𝑞 “ ℕ) ¬ 2 ∥ 𝑛 ↔ (∀𝑛 ∈ (𝑞 “ ℕ)𝑛 ∈ ℕ ∧ ∀𝑛 ∈ (𝑞 “ ℕ) ¬ 2 ∥ 𝑛)))
97 dfss3 3558 . . . . . . . . . . . . . . . 16 ((𝑞 “ ℕ) ⊆ 𝐽 ↔ ∀𝑛 ∈ (𝑞 “ ℕ)𝑛𝐽)
98 breq2 4582 . . . . . . . . . . . . . . . . . . 19 (𝑧 = 𝑛 → (2 ∥ 𝑧 ↔ 2 ∥ 𝑛))
9998notbid 307 . . . . . . . . . . . . . . . . . 18 (𝑧 = 𝑛 → (¬ 2 ∥ 𝑧 ↔ ¬ 2 ∥ 𝑛))
10099, 16elrab2 3333 . . . . . . . . . . . . . . . . 17 (𝑛𝐽 ↔ (𝑛 ∈ ℕ ∧ ¬ 2 ∥ 𝑛))
101100ralbii 2963 . . . . . . . . . . . . . . . 16 (∀𝑛 ∈ (𝑞 “ ℕ)𝑛𝐽 ↔ ∀𝑛 ∈ (𝑞 “ ℕ)(𝑛 ∈ ℕ ∧ ¬ 2 ∥ 𝑛))
102 r19.26 3046 . . . . . . . . . . . . . . . 16 (∀𝑛 ∈ (𝑞 “ ℕ)(𝑛 ∈ ℕ ∧ ¬ 2 ∥ 𝑛) ↔ (∀𝑛 ∈ (𝑞 “ ℕ)𝑛 ∈ ℕ ∧ ∀𝑛 ∈ (𝑞 “ ℕ) ¬ 2 ∥ 𝑛))
10397, 101, 1023bitri 285 . . . . . . . . . . . . . . 15 ((𝑞 “ ℕ) ⊆ 𝐽 ↔ (∀𝑛 ∈ (𝑞 “ ℕ)𝑛 ∈ ℕ ∧ ∀𝑛 ∈ (𝑞 “ ℕ) ¬ 2 ∥ 𝑛))
10496, 103syl6rbbr 278 . . . . . . . . . . . . . 14 (𝑞:ℕ⟶ℕ0 → ((𝑞 “ ℕ) ⊆ 𝐽 ↔ ∀𝑛 ∈ (𝑞 “ ℕ) ¬ 2 ∥ 𝑛))
105104adantr 480 . . . . . . . . . . . . 13 ((𝑞:ℕ⟶ℕ0 ∧ (𝑞 “ ℕ) ∈ Fin) → ((𝑞 “ ℕ) ⊆ 𝐽 ↔ ∀𝑛 ∈ (𝑞 “ ℕ) ¬ 2 ∥ 𝑛))
106105pm5.32i 667 . . . . . . . . . . . 12 (((𝑞:ℕ⟶ℕ0 ∧ (𝑞 “ ℕ) ∈ Fin) ∧ (𝑞 “ ℕ) ⊆ 𝐽) ↔ ((𝑞:ℕ⟶ℕ0 ∧ (𝑞 “ ℕ) ∈ Fin) ∧ ∀𝑛 ∈ (𝑞 “ ℕ) ¬ 2 ∥ 𝑛))
10789, 90, 1063bitri 285 . . . . . . . . . . 11 (𝑞 ∈ (𝑇𝑅) ↔ ((𝑞:ℕ⟶ℕ0 ∧ (𝑞 “ ℕ) ∈ Fin) ∧ ∀𝑛 ∈ (𝑞 “ ℕ) ¬ 2 ∥ 𝑛))
108107anbi1i 727 . . . . . . . . . 10 ((𝑞 ∈ (𝑇𝑅) ∧ Σ𝑘 ∈ ℕ ((𝑞𝑘) · 𝑘) = 𝑁) ↔ (((𝑞:ℕ⟶ℕ0 ∧ (𝑞 “ ℕ) ∈ Fin) ∧ ∀𝑛 ∈ (𝑞 “ ℕ) ¬ 2 ∥ 𝑛) ∧ Σ𝑘 ∈ ℕ ((𝑞𝑘) · 𝑘) = 𝑁))
10984, 108bitr4i 266 . . . . . . . . 9 ((𝑞𝑃 ∧ ∀𝑛 ∈ (𝑞 “ ℕ) ¬ 2 ∥ 𝑛) ↔ (𝑞 ∈ (𝑇𝑅) ∧ Σ𝑘 ∈ ℕ ((𝑞𝑘) · 𝑘) = 𝑁))
110 rabid 3095 . . . . . . . . 9 (𝑞 ∈ {𝑞𝑃 ∣ ∀𝑛 ∈ (𝑞 “ ℕ) ¬ 2 ∥ 𝑛} ↔ (𝑞𝑃 ∧ ∀𝑛 ∈ (𝑞 “ ℕ) ¬ 2 ∥ 𝑛))
111 rabid 3095 . . . . . . . . 9 (𝑞 ∈ {𝑞 ∈ (𝑇𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑞𝑘) · 𝑘) = 𝑁} ↔ (𝑞 ∈ (𝑇𝑅) ∧ Σ𝑘 ∈ ℕ ((𝑞𝑘) · 𝑘) = 𝑁))
112109, 110, 1113bitr4i 291 . . . . . . . 8 (𝑞 ∈ {𝑞𝑃 ∣ ∀𝑛 ∈ (𝑞 “ ℕ) ¬ 2 ∥ 𝑛} ↔ 𝑞 ∈ {𝑞 ∈ (𝑇𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑞𝑘) · 𝑘) = 𝑁})
11377, 78, 112eqri 28529 . . . . . . 7 {𝑞𝑃 ∣ ∀𝑛 ∈ (𝑞 “ ℕ) ¬ 2 ∥ 𝑛} = {𝑞 ∈ (𝑇𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑞𝑘) · 𝑘) = 𝑁}
11414, 76, 1133eqtri 2636 . . . . . 6 𝑂 = {𝑞 ∈ (𝑇𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑞𝑘) · 𝑘) = 𝑁}
115114reseq2i 5301 . . . . 5 (𝐺𝑂) = (𝐺 ↾ {𝑞 ∈ (𝑇𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑞𝑘) · 𝑘) = 𝑁})
116115a1i 11 . . . 4 (⊤ → (𝐺𝑂) = (𝐺 ↾ {𝑞 ∈ (𝑇𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑞𝑘) · 𝑘) = 𝑁}))
117114a1i 11 . . . 4 (⊤ → 𝑂 = {𝑞 ∈ (𝑇𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑞𝑘) · 𝑘) = 𝑁})
118 nfcv 2751 . . . . . 6 𝑑𝐷
119 nfrab1 3099 . . . . . 6 𝑑{𝑑 ∈ (({0, 1} ↑𝑚 ℕ) ∩ 𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑑𝑘) · 𝑘) = 𝑁}
120 fnima 5909 . . . . . . . . . . . . . . . . 17 (𝑑 Fn ℕ → (𝑑 “ ℕ) = ran 𝑑)
121120sseq1d 3595 . . . . . . . . . . . . . . . 16 (𝑑 Fn ℕ → ((𝑑 “ ℕ) ⊆ {0, 1} ↔ ran 𝑑 ⊆ {0, 1}))
122121anbi2d 736 . . . . . . . . . . . . . . 15 (𝑑 Fn ℕ → ((ran 𝑑 ⊆ ℕ0 ∧ (𝑑 “ ℕ) ⊆ {0, 1}) ↔ (ran 𝑑 ⊆ ℕ0 ∧ ran 𝑑 ⊆ {0, 1})))
123 sstr 3576 . . . . . . . . . . . . . . . . 17 ((ran 𝑑 ⊆ {0, 1} ∧ {0, 1} ⊆ ℕ0) → ran 𝑑 ⊆ ℕ0)
12449, 123mpan2 703 . . . . . . . . . . . . . . . 16 (ran 𝑑 ⊆ {0, 1} → ran 𝑑 ⊆ ℕ0)
125124pm4.71ri 663 . . . . . . . . . . . . . . 15 (ran 𝑑 ⊆ {0, 1} ↔ (ran 𝑑 ⊆ ℕ0 ∧ ran 𝑑 ⊆ {0, 1}))
126122, 125syl6bbr 277 . . . . . . . . . . . . . 14 (𝑑 Fn ℕ → ((ran 𝑑 ⊆ ℕ0 ∧ (𝑑 “ ℕ) ⊆ {0, 1}) ↔ ran 𝑑 ⊆ {0, 1}))
127126pm5.32i 667 . . . . . . . . . . . . 13 ((𝑑 Fn ℕ ∧ (ran 𝑑 ⊆ ℕ0 ∧ (𝑑 “ ℕ) ⊆ {0, 1})) ↔ (𝑑 Fn ℕ ∧ ran 𝑑 ⊆ {0, 1}))
128 anass 679 . . . . . . . . . . . . 13 (((𝑑 Fn ℕ ∧ ran 𝑑 ⊆ ℕ0) ∧ (𝑑 “ ℕ) ⊆ {0, 1}) ↔ (𝑑 Fn ℕ ∧ (ran 𝑑 ⊆ ℕ0 ∧ (𝑑 “ ℕ) ⊆ {0, 1})))
129 df-f 5794 . . . . . . . . . . . . 13 (𝑑:ℕ⟶{0, 1} ↔ (𝑑 Fn ℕ ∧ ran 𝑑 ⊆ {0, 1}))
130127, 128, 1293bitr4ri 292 . . . . . . . . . . . 12 (𝑑:ℕ⟶{0, 1} ↔ ((𝑑 Fn ℕ ∧ ran 𝑑 ⊆ ℕ0) ∧ (𝑑 “ ℕ) ⊆ {0, 1}))
131 prex 4831 . . . . . . . . . . . . 13 {0, 1} ∈ V
132131, 86elmap 7750 . . . . . . . . . . . 12 (𝑑 ∈ ({0, 1} ↑𝑚 ℕ) ↔ 𝑑:ℕ⟶{0, 1})
133 df-f 5794 . . . . . . . . . . . . 13 (𝑑:ℕ⟶ℕ0 ↔ (𝑑 Fn ℕ ∧ ran 𝑑 ⊆ ℕ0))
134133anbi1i 727 . . . . . . . . . . . 12 ((𝑑:ℕ⟶ℕ0 ∧ (𝑑 “ ℕ) ⊆ {0, 1}) ↔ ((𝑑 Fn ℕ ∧ ran 𝑑 ⊆ ℕ0) ∧ (𝑑 “ ℕ) ⊆ {0, 1}))
135130, 132, 1343bitr4i 291 . . . . . . . . . . 11 (𝑑 ∈ ({0, 1} ↑𝑚 ℕ) ↔ (𝑑:ℕ⟶ℕ0 ∧ (𝑑 “ ℕ) ⊆ {0, 1}))
136 vex 3176 . . . . . . . . . . . 12 𝑑 ∈ V
137 cnveq 5206 . . . . . . . . . . . . . 14 (𝑓 = 𝑑𝑓 = 𝑑)
138137imaeq1d 5371 . . . . . . . . . . . . 13 (𝑓 = 𝑑 → (𝑓 “ ℕ) = (𝑑 “ ℕ))
139138eleq1d 2672 . . . . . . . . . . . 12 (𝑓 = 𝑑 → ((𝑓 “ ℕ) ∈ Fin ↔ (𝑑 “ ℕ) ∈ Fin))
140136, 139, 20elab2 3323 . . . . . . . . . . 11 (𝑑𝑅 ↔ (𝑑 “ ℕ) ∈ Fin)
141135, 140anbi12i 729 . . . . . . . . . 10 ((𝑑 ∈ ({0, 1} ↑𝑚 ℕ) ∧ 𝑑𝑅) ↔ ((𝑑:ℕ⟶ℕ0 ∧ (𝑑 “ ℕ) ⊆ {0, 1}) ∧ (𝑑 “ ℕ) ∈ Fin))
142 elin 3758 . . . . . . . . . 10 (𝑑 ∈ (({0, 1} ↑𝑚 ℕ) ∩ 𝑅) ↔ (𝑑 ∈ ({0, 1} ↑𝑚 ℕ) ∧ 𝑑𝑅))
143 an32 835 . . . . . . . . . 10 (((𝑑:ℕ⟶ℕ0 ∧ (𝑑 “ ℕ) ∈ Fin) ∧ (𝑑 “ ℕ) ⊆ {0, 1}) ↔ ((𝑑:ℕ⟶ℕ0 ∧ (𝑑 “ ℕ) ⊆ {0, 1}) ∧ (𝑑 “ ℕ) ∈ Fin))
144141, 142, 1433bitr4i 291 . . . . . . . . 9 (𝑑 ∈ (({0, 1} ↑𝑚 ℕ) ∩ 𝑅) ↔ ((𝑑:ℕ⟶ℕ0 ∧ (𝑑 “ ℕ) ∈ Fin) ∧ (𝑑 “ ℕ) ⊆ {0, 1}))
145144anbi1i 727 . . . . . . . 8 ((𝑑 ∈ (({0, 1} ↑𝑚 ℕ) ∩ 𝑅) ∧ Σ𝑘 ∈ ℕ ((𝑑𝑘) · 𝑘) = 𝑁) ↔ (((𝑑:ℕ⟶ℕ0 ∧ (𝑑 “ ℕ) ∈ Fin) ∧ (𝑑 “ ℕ) ⊆ {0, 1}) ∧ Σ𝑘 ∈ ℕ ((𝑑𝑘) · 𝑘) = 𝑁))
14613eulerpartleme 29546 . . . . . . . . . 10 (𝑑𝑃 ↔ (𝑑:ℕ⟶ℕ0 ∧ (𝑑 “ ℕ) ∈ Fin ∧ Σ𝑘 ∈ ℕ ((𝑑𝑘) · 𝑘) = 𝑁))
147146anbi1i 727 . . . . . . . . 9 ((𝑑𝑃 ∧ (𝑑 “ ℕ) ⊆ {0, 1}) ↔ ((𝑑:ℕ⟶ℕ0 ∧ (𝑑 “ ℕ) ∈ Fin ∧ Σ𝑘 ∈ ℕ ((𝑑𝑘) · 𝑘) = 𝑁) ∧ (𝑑 “ ℕ) ⊆ {0, 1}))
148 df-3an 1033 . . . . . . . . . 10 ((𝑑:ℕ⟶ℕ0 ∧ (𝑑 “ ℕ) ∈ Fin ∧ Σ𝑘 ∈ ℕ ((𝑑𝑘) · 𝑘) = 𝑁) ↔ ((𝑑:ℕ⟶ℕ0 ∧ (𝑑 “ ℕ) ∈ Fin) ∧ Σ𝑘 ∈ ℕ ((𝑑𝑘) · 𝑘) = 𝑁))
149148anbi1i 727 . . . . . . . . 9 (((𝑑:ℕ⟶ℕ0 ∧ (𝑑 “ ℕ) ∈ Fin ∧ Σ𝑘 ∈ ℕ ((𝑑𝑘) · 𝑘) = 𝑁) ∧ (𝑑 “ ℕ) ⊆ {0, 1}) ↔ (((𝑑:ℕ⟶ℕ0 ∧ (𝑑 “ ℕ) ∈ Fin) ∧ Σ𝑘 ∈ ℕ ((𝑑𝑘) · 𝑘) = 𝑁) ∧ (𝑑 “ ℕ) ⊆ {0, 1}))
150 an32 835 . . . . . . . . 9 ((((𝑑:ℕ⟶ℕ0 ∧ (𝑑 “ ℕ) ∈ Fin) ∧ Σ𝑘 ∈ ℕ ((𝑑𝑘) · 𝑘) = 𝑁) ∧ (𝑑 “ ℕ) ⊆ {0, 1}) ↔ (((𝑑:ℕ⟶ℕ0 ∧ (𝑑 “ ℕ) ∈ Fin) ∧ (𝑑 “ ℕ) ⊆ {0, 1}) ∧ Σ𝑘 ∈ ℕ ((𝑑𝑘) · 𝑘) = 𝑁))
151147, 149, 1503bitri 285 . . . . . . . 8 ((𝑑𝑃 ∧ (𝑑 “ ℕ) ⊆ {0, 1}) ↔ (((𝑑:ℕ⟶ℕ0 ∧ (𝑑 “ ℕ) ∈ Fin) ∧ (𝑑 “ ℕ) ⊆ {0, 1}) ∧ Σ𝑘 ∈ ℕ ((𝑑𝑘) · 𝑘) = 𝑁))
152145, 151bitr4i 266 . . . . . . 7 ((𝑑 ∈ (({0, 1} ↑𝑚 ℕ) ∩ 𝑅) ∧ Σ𝑘 ∈ ℕ ((𝑑𝑘) · 𝑘) = 𝑁) ↔ (𝑑𝑃 ∧ (𝑑 “ ℕ) ⊆ {0, 1}))
153 rabid 3095 . . . . . . 7 (𝑑 ∈ {𝑑 ∈ (({0, 1} ↑𝑚 ℕ) ∩ 𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑑𝑘) · 𝑘) = 𝑁} ↔ (𝑑 ∈ (({0, 1} ↑𝑚 ℕ) ∩ 𝑅) ∧ Σ𝑘 ∈ ℕ ((𝑑𝑘) · 𝑘) = 𝑁))
15413, 14, 15eulerpartlemd 29549 . . . . . . 7 (𝑑𝐷 ↔ (𝑑𝑃 ∧ (𝑑 “ ℕ) ⊆ {0, 1}))
155152, 153, 1543bitr4ri 292 . . . . . 6 (𝑑𝐷𝑑 ∈ {𝑑 ∈ (({0, 1} ↑𝑚 ℕ) ∩ 𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑑𝑘) · 𝑘) = 𝑁})
156118, 119, 155eqri 28529 . . . . 5 𝐷 = {𝑑 ∈ (({0, 1} ↑𝑚 ℕ) ∩ 𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑑𝑘) · 𝑘) = 𝑁}
157156a1i 11 . . . 4 (⊤ → 𝐷 = {𝑑 ∈ (({0, 1} ↑𝑚 ℕ) ∩ 𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑑𝑘) · 𝑘) = 𝑁})
158116, 117, 157f1oeq123d 6031 . . 3 (⊤ → ((𝐺𝑂):𝑂1-1-onto𝐷 ↔ (𝐺 ↾ {𝑞 ∈ (𝑇𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑞𝑘) · 𝑘) = 𝑁}):{𝑞 ∈ (𝑇𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑞𝑘) · 𝑘) = 𝑁}–1-1-onto→{𝑑 ∈ (({0, 1} ↑𝑚 ℕ) ∩ 𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑑𝑘) · 𝑘) = 𝑁}))
15972, 158mpbird 246 . 2 (⊤ → (𝐺𝑂):𝑂1-1-onto𝐷)
160159trud 1484 1 (𝐺𝑂):𝑂1-1-onto𝐷
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 195  wa 383  w3a 1031   = wceq 1475  wtru 1476  wcel 1977  {cab 2596  wral 2896  {crab 2900  Vcvv 3173  cin 3539  wss 3540  c0 3874  𝒫 cpw 4108  {cpr 4127   class class class wbr 4578  {copab 4637  cmpt 4638  ccnv 5027  dom cdm 5028  ran crn 5029  cres 5030  cima 5031  ccom 5032   Fn wfn 5785  wf 5786  1-1-ontowf1o 5789  cfv 5790  (class class class)co 6527  cmpt2 6529   supp csupp 7160  𝑚 cmap 7722  Fincfn 7819  0cc0 9793  1c1 9794   · cmul 9798  cle 9932  cn 10870  2c2 10920  0cn0 11142  cexp 12680  Σcsu 14213  cdvds 14770  bitscbits 14928  𝟭cind 29194
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4694  ax-sep 4704  ax-nul 4712  ax-pow 4764  ax-pr 4828  ax-un 6825  ax-inf2 8399  ax-ac2 9146  ax-cnex 9849  ax-resscn 9850  ax-1cn 9851  ax-icn 9852  ax-addcl 9853  ax-addrcl 9854  ax-mulcl 9855  ax-mulrcl 9856  ax-mulcom 9857  ax-addass 9858  ax-mulass 9859  ax-distr 9860  ax-i2m1 9861  ax-1ne0 9862  ax-1rid 9863  ax-rnegex 9864  ax-rrecex 9865  ax-cnre 9866  ax-pre-lttri 9867  ax-pre-lttrn 9868  ax-pre-ltadd 9869  ax-pre-mulgt0 9870  ax-pre-sup 9871
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-fal 1481  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-reu 2903  df-rmo 2904  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4368  df-int 4406  df-iun 4452  df-disj 4549  df-br 4579  df-opab 4639  df-mpt 4640  df-tr 4676  df-eprel 4939  df-id 4943  df-po 4949  df-so 4950  df-fr 4987  df-se 4988  df-we 4989  df-xp 5034  df-rel 5035  df-cnv 5036  df-co 5037  df-dm 5038  df-rn 5039  df-res 5040  df-ima 5041  df-pred 5583  df-ord 5629  df-on 5630  df-lim 5631  df-suc 5632  df-iota 5754  df-fun 5792  df-fn 5793  df-f 5794  df-f1 5795  df-fo 5796  df-f1o 5797  df-fv 5798  df-isom 5799  df-riota 6489  df-ov 6530  df-oprab 6531  df-mpt2 6532  df-om 6936  df-1st 7037  df-2nd 7038  df-supp 7161  df-wrecs 7272  df-recs 7333  df-rdg 7371  df-1o 7425  df-2o 7426  df-oadd 7429  df-er 7607  df-map 7724  df-pm 7725  df-en 7820  df-dom 7821  df-sdom 7822  df-fin 7823  df-fsupp 8137  df-sup 8209  df-inf 8210  df-oi 8276  df-card 8626  df-acn 8629  df-ac 8800  df-cda 8851  df-pnf 9933  df-mnf 9934  df-xr 9935  df-ltxr 9936  df-le 9937  df-sub 10120  df-neg 10121  df-div 10537  df-nn 10871  df-2 10929  df-3 10930  df-n0 11143  df-z 11214  df-uz 11523  df-rp 11668  df-fz 12156  df-fzo 12293  df-fl 12413  df-mod 12489  df-seq 12622  df-exp 12681  df-hash 12938  df-cj 13636  df-re 13637  df-im 13638  df-sqrt 13772  df-abs 13773  df-clim 14016  df-sum 14214  df-dvds 14771  df-bits 14931  df-ind 29195
This theorem is referenced by:  eulerpart  29565
  Copyright terms: Public domain W3C validator