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 30571
Description: Lemma for eulerpart 30572. (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 6231 . . . . . . . . . . . 12 ((𝑜 = 𝑞𝑘 ∈ ℕ) → (𝑜𝑘) = (𝑞𝑘))
32oveq1d 6705 . . . . . . . . . . 11 ((𝑜 = 𝑞𝑘 ∈ ℕ) → ((𝑜𝑘) · 𝑘) = ((𝑞𝑘) · 𝑘))
43sumeq2dv 14477 . . . . . . . . . 10 (𝑜 = 𝑞 → Σ𝑘 ∈ ℕ ((𝑜𝑘) · 𝑘) = Σ𝑘 ∈ ℕ ((𝑞𝑘) · 𝑘))
54eqeq1d 2653 . . . . . . . . 9 (𝑜 = 𝑞 → (Σ𝑘 ∈ ℕ ((𝑜𝑘) · 𝑘) = 𝑁 ↔ Σ𝑘 ∈ ℕ ((𝑞𝑘) · 𝑘) = 𝑁))
65cbvrabv 3230 . . . . . . . 8 {𝑜 ∈ (𝑇𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑜𝑘) · 𝑘) = 𝑁} = {𝑞 ∈ (𝑇𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑞𝑘) · 𝑘) = 𝑁}
76a1i 11 . . . . . . 7 (𝑜 = 𝑞 → {𝑜 ∈ (𝑇𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑜𝑘) · 𝑘) = 𝑁} = {𝑞 ∈ (𝑇𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑞𝑘) · 𝑘) = 𝑁})
87reseq2d 5428 . . . . . 6 (𝑜 = 𝑞 → (𝐺 ↾ {𝑜 ∈ (𝑇𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑜𝑘) · 𝑘) = 𝑁}) = (𝐺 ↾ {𝑞 ∈ (𝑇𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑞𝑘) · 𝑘) = 𝑁}))
9 eqidd 2652 . . . . . 6 (𝑜 = 𝑞 → {𝑑 ∈ (({0, 1} ↑𝑚 ℕ) ∩ 𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑑𝑘) · 𝑘) = 𝑁} = {𝑑 ∈ (({0, 1} ↑𝑚 ℕ) ∩ 𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑑𝑘) · 𝑘) = 𝑁})
108, 7, 9f1oeq123d 6171 . . . . 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 30562 . . . . . 6 𝐺:(𝑇𝑅)–1-1-onto→(({0, 1} ↑𝑚 ℕ) ∩ 𝑅)
2322a1i 11 . . . . 5 (⊤ → 𝐺:(𝑇𝑅)–1-1-onto→(({0, 1} ↑𝑚 ℕ) ∩ 𝑅))
24 fveq2 6229 . . . . . . . . . . . . . 14 (𝑞 = 𝑜 → (𝐺𝑞) = (𝐺𝑜))
25 reseq1 5422 . . . . . . . . . . . . . . . . . 18 (𝑞 = 𝑜 → (𝑞𝐽) = (𝑜𝐽))
2625coeq2d 5317 . . . . . . . . . . . . . . . . 17 (𝑞 = 𝑜 → (bits ∘ (𝑞𝐽)) = (bits ∘ (𝑜𝐽)))
2726fveq2d 6233 . . . . . . . . . . . . . . . 16 (𝑞 = 𝑜 → (𝑀‘(bits ∘ (𝑞𝐽))) = (𝑀‘(bits ∘ (𝑜𝐽))))
2827imaeq2d 5501 . . . . . . . . . . . . . . 15 (𝑞 = 𝑜 → (𝐹 “ (𝑀‘(bits ∘ (𝑞𝐽)))) = (𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽)))))
2928fveq2d 6233 . . . . . . . . . . . . . 14 (𝑞 = 𝑜 → ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑞𝐽))))) = ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽))))))
3024, 29eqeq12d 2666 . . . . . . . . . . . . 13 (𝑞 = 𝑜 → ((𝐺𝑞) = ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑞𝐽))))) ↔ (𝐺𝑜) = ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽)))))))
3113, 14, 15, 16, 17, 18, 19, 20, 21, 12eulerpartlemgv 30563 . . . . . . . . . . . . 13 (𝑞 ∈ (𝑇𝑅) → (𝐺𝑞) = ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑞𝐽))))))
3230, 31vtoclga 3303 . . . . . . . . . . . 12 (𝑜 ∈ (𝑇𝑅) → (𝐺𝑜) = ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽))))))
33323ad2ant2 1103 . . . . . . . . . . 11 ((⊤ ∧ 𝑜 ∈ (𝑇𝑅) ∧ 𝑑 = ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽)))))) → (𝐺𝑜) = ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽))))))
34 simp3 1083 . . . . . . . . . . 11 ((⊤ ∧ 𝑜 ∈ (𝑇𝑅) ∧ 𝑑 = ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽)))))) → 𝑑 = ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽))))))
3533, 34eqtr4d 2688 . . . . . . . . . 10 ((⊤ ∧ 𝑜 ∈ (𝑇𝑅) ∧ 𝑑 = ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽)))))) → (𝐺𝑜) = 𝑑)
3635fveq1d 6231 . . . . . . . . 9 ((⊤ ∧ 𝑜 ∈ (𝑇𝑅) ∧ 𝑑 = ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽)))))) → ((𝐺𝑜)‘𝑘) = (𝑑𝑘))
3736oveq1d 6705 . . . . . . . 8 ((⊤ ∧ 𝑜 ∈ (𝑇𝑅) ∧ 𝑑 = ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽)))))) → (((𝐺𝑜)‘𝑘) · 𝑘) = ((𝑑𝑘) · 𝑘))
3837sumeq2sdv 14479 . . . . . . 7 ((⊤ ∧ 𝑜 ∈ (𝑇𝑅) ∧ 𝑑 = ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽)))))) → Σ𝑘 ∈ ℕ (((𝐺𝑜)‘𝑘) · 𝑘) = Σ𝑘 ∈ ℕ ((𝑑𝑘) · 𝑘))
3924fveq2d 6233 . . . . . . . . . . 11 (𝑞 = 𝑜 → (𝑆‘(𝐺𝑞)) = (𝑆‘(𝐺𝑜)))
40 fveq2 6229 . . . . . . . . . . 11 (𝑞 = 𝑜 → (𝑆𝑞) = (𝑆𝑜))
4139, 40eqeq12d 2666 . . . . . . . . . 10 (𝑞 = 𝑜 → ((𝑆‘(𝐺𝑞)) = (𝑆𝑞) ↔ (𝑆‘(𝐺𝑜)) = (𝑆𝑜)))
42 eulerpart.s . . . . . . . . . . 11 𝑆 = (𝑓 ∈ ((ℕ0𝑚 ℕ) ∩ 𝑅) ↦ Σ𝑘 ∈ ℕ ((𝑓𝑘) · 𝑘))
4313, 14, 15, 16, 17, 18, 19, 20, 21, 12, 42eulerpartlemgs2 30570 . . . . . . . . . 10 (𝑞 ∈ (𝑇𝑅) → (𝑆‘(𝐺𝑞)) = (𝑆𝑞))
4441, 43vtoclga 3303 . . . . . . . . 9 (𝑜 ∈ (𝑇𝑅) → (𝑆‘(𝐺𝑜)) = (𝑆𝑜))
45 nn0ex 11336 . . . . . . . . . . . . 13 0 ∈ V
46 0nn0 11345 . . . . . . . . . . . . . 14 0 ∈ ℕ0
47 1nn0 11346 . . . . . . . . . . . . . 14 1 ∈ ℕ0
48 prssi 4385 . . . . . . . . . . . . . 14 ((0 ∈ ℕ0 ∧ 1 ∈ ℕ0) → {0, 1} ⊆ ℕ0)
4946, 47, 48mp2an 708 . . . . . . . . . . . . 13 {0, 1} ⊆ ℕ0
50 mapss 7942 . . . . . . . . . . . . 13 ((ℕ0 ∈ V ∧ {0, 1} ⊆ ℕ0) → ({0, 1} ↑𝑚 ℕ) ⊆ (ℕ0𝑚 ℕ))
5145, 49, 50mp2an 708 . . . . . . . . . . . 12 ({0, 1} ↑𝑚 ℕ) ⊆ (ℕ0𝑚 ℕ)
52 ssrin 3871 . . . . . . . . . . . 12 (({0, 1} ↑𝑚 ℕ) ⊆ (ℕ0𝑚 ℕ) → (({0, 1} ↑𝑚 ℕ) ∩ 𝑅) ⊆ ((ℕ0𝑚 ℕ) ∩ 𝑅))
5351, 52ax-mp 5 . . . . . . . . . . 11 (({0, 1} ↑𝑚 ℕ) ∩ 𝑅) ⊆ ((ℕ0𝑚 ℕ) ∩ 𝑅)
54 f1of 6175 . . . . . . . . . . . . 13 (𝐺:(𝑇𝑅)–1-1-onto→(({0, 1} ↑𝑚 ℕ) ∩ 𝑅) → 𝐺:(𝑇𝑅)⟶(({0, 1} ↑𝑚 ℕ) ∩ 𝑅))
5522, 54ax-mp 5 . . . . . . . . . . . 12 𝐺:(𝑇𝑅)⟶(({0, 1} ↑𝑚 ℕ) ∩ 𝑅)
5655ffvelrni 6398 . . . . . . . . . . 11 (𝑜 ∈ (𝑇𝑅) → (𝐺𝑜) ∈ (({0, 1} ↑𝑚 ℕ) ∩ 𝑅))
5753, 56sseldi 3634 . . . . . . . . . 10 (𝑜 ∈ (𝑇𝑅) → (𝐺𝑜) ∈ ((ℕ0𝑚 ℕ) ∩ 𝑅))
5820, 42eulerpartlemsv1 30546 . . . . . . . . . 10 ((𝐺𝑜) ∈ ((ℕ0𝑚 ℕ) ∩ 𝑅) → (𝑆‘(𝐺𝑜)) = Σ𝑘 ∈ ℕ (((𝐺𝑜)‘𝑘) · 𝑘))
5957, 58syl 17 . . . . . . . . 9 (𝑜 ∈ (𝑇𝑅) → (𝑆‘(𝐺𝑜)) = Σ𝑘 ∈ ℕ (((𝐺𝑜)‘𝑘) · 𝑘))
6013, 14, 15, 16, 17, 18, 19, 20, 21eulerpartlemt0 30559 . . . . . . . . . . . 12 (𝑜 ∈ (𝑇𝑅) ↔ (𝑜 ∈ (ℕ0𝑚 ℕ) ∧ (𝑜 “ ℕ) ∈ Fin ∧ (𝑜 “ ℕ) ⊆ 𝐽))
6160simp1bi 1096 . . . . . . . . . . 11 (𝑜 ∈ (𝑇𝑅) → 𝑜 ∈ (ℕ0𝑚 ℕ))
62 inss2 3867 . . . . . . . . . . . 12 (𝑇𝑅) ⊆ 𝑅
6362sseli 3632 . . . . . . . . . . 11 (𝑜 ∈ (𝑇𝑅) → 𝑜𝑅)
6461, 63elind 3831 . . . . . . . . . 10 (𝑜 ∈ (𝑇𝑅) → 𝑜 ∈ ((ℕ0𝑚 ℕ) ∩ 𝑅))
6520, 42eulerpartlemsv1 30546 . . . . . . . . . 10 (𝑜 ∈ ((ℕ0𝑚 ℕ) ∩ 𝑅) → (𝑆𝑜) = Σ𝑘 ∈ ℕ ((𝑜𝑘) · 𝑘))
6664, 65syl 17 . . . . . . . . 9 (𝑜 ∈ (𝑇𝑅) → (𝑆𝑜) = Σ𝑘 ∈ ℕ ((𝑜𝑘) · 𝑘))
6744, 59, 663eqtr3d 2693 . . . . . . . 8 (𝑜 ∈ (𝑇𝑅) → Σ𝑘 ∈ ℕ (((𝐺𝑜)‘𝑘) · 𝑘) = Σ𝑘 ∈ ℕ ((𝑜𝑘) · 𝑘))
68673ad2ant2 1103 . . . . . . 7 ((⊤ ∧ 𝑜 ∈ (𝑇𝑅) ∧ 𝑑 = ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽)))))) → Σ𝑘 ∈ ℕ (((𝐺𝑜)‘𝑘) · 𝑘) = Σ𝑘 ∈ ℕ ((𝑜𝑘) · 𝑘))
6938, 68eqtr3d 2687 . . . . . 6 ((⊤ ∧ 𝑜 ∈ (𝑇𝑅) ∧ 𝑑 = ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽)))))) → Σ𝑘 ∈ ℕ ((𝑑𝑘) · 𝑘) = Σ𝑘 ∈ ℕ ((𝑜𝑘) · 𝑘))
7069eqeq1d 2653 . . . . 5 ((⊤ ∧ 𝑜 ∈ (𝑇𝑅) ∧ 𝑑 = ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽)))))) → (Σ𝑘 ∈ ℕ ((𝑑𝑘) · 𝑘) = 𝑁 ↔ Σ𝑘 ∈ ℕ ((𝑜𝑘) · 𝑘) = 𝑁))
7112, 23, 70f1oresrab 6435 . . . 4 (⊤ → (𝐺 ↾ {𝑜 ∈ (𝑇𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑜𝑘) · 𝑘) = 𝑁}):{𝑜 ∈ (𝑇𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑜𝑘) · 𝑘) = 𝑁}–1-1-onto→{𝑑 ∈ (({0, 1} ↑𝑚 ℕ) ∩ 𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑑𝑘) · 𝑘) = 𝑁})
7211, 71chvarv 2299 . . 3 (⊤ → (𝐺 ↾ {𝑞 ∈ (𝑇𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑞𝑘) · 𝑘) = 𝑁}):{𝑞 ∈ (𝑇𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑞𝑘) · 𝑘) = 𝑁}–1-1-onto→{𝑑 ∈ (({0, 1} ↑𝑚 ℕ) ∩ 𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑑𝑘) · 𝑘) = 𝑁})
73 cnveq 5328 . . . . . . . . . 10 (𝑔 = 𝑞𝑔 = 𝑞)
7473imaeq1d 5500 . . . . . . . . 9 (𝑔 = 𝑞 → (𝑔 “ ℕ) = (𝑞 “ ℕ))
7574raleqdv 3174 . . . . . . . 8 (𝑔 = 𝑞 → (∀𝑛 ∈ (𝑔 “ ℕ) ¬ 2 ∥ 𝑛 ↔ ∀𝑛 ∈ (𝑞 “ ℕ) ¬ 2 ∥ 𝑛))
7675cbvrabv 3230 . . . . . . 7 {𝑔𝑃 ∣ ∀𝑛 ∈ (𝑔 “ ℕ) ¬ 2 ∥ 𝑛} = {𝑞𝑃 ∣ ∀𝑛 ∈ (𝑞 “ ℕ) ¬ 2 ∥ 𝑛}
77 nfrab1 3152 . . . . . . . 8 𝑞{𝑞𝑃 ∣ ∀𝑛 ∈ (𝑞 “ ℕ) ¬ 2 ∥ 𝑛}
78 nfrab1 3152 . . . . . . . 8 𝑞{𝑞 ∈ (𝑇𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑞𝑘) · 𝑘) = 𝑁}
79 df-3an 1056 . . . . . . . . . . . 12 ((𝑞:ℕ⟶ℕ0 ∧ (𝑞 “ ℕ) ∈ Fin ∧ Σ𝑘 ∈ ℕ ((𝑞𝑘) · 𝑘) = 𝑁) ↔ ((𝑞:ℕ⟶ℕ0 ∧ (𝑞 “ ℕ) ∈ Fin) ∧ Σ𝑘 ∈ ℕ ((𝑞𝑘) · 𝑘) = 𝑁))
8079anbi1i 731 . . . . . . . . . . 11 (((𝑞:ℕ⟶ℕ0 ∧ (𝑞 “ ℕ) ∈ Fin ∧ Σ𝑘 ∈ ℕ ((𝑞𝑘) · 𝑘) = 𝑁) ∧ ∀𝑛 ∈ (𝑞 “ ℕ) ¬ 2 ∥ 𝑛) ↔ (((𝑞:ℕ⟶ℕ0 ∧ (𝑞 “ ℕ) ∈ Fin) ∧ Σ𝑘 ∈ ℕ ((𝑞𝑘) · 𝑘) = 𝑁) ∧ ∀𝑛 ∈ (𝑞 “ ℕ) ¬ 2 ∥ 𝑛))
8113eulerpartleme 30553 . . . . . . . . . . . 12 (𝑞𝑃 ↔ (𝑞:ℕ⟶ℕ0 ∧ (𝑞 “ ℕ) ∈ Fin ∧ Σ𝑘 ∈ ℕ ((𝑞𝑘) · 𝑘) = 𝑁))
8281anbi1i 731 . . . . . . . . . . 11 ((𝑞𝑃 ∧ ∀𝑛 ∈ (𝑞 “ ℕ) ¬ 2 ∥ 𝑛) ↔ ((𝑞:ℕ⟶ℕ0 ∧ (𝑞 “ ℕ) ∈ Fin ∧ Σ𝑘 ∈ ℕ ((𝑞𝑘) · 𝑘) = 𝑁) ∧ ∀𝑛 ∈ (𝑞 “ ℕ) ¬ 2 ∥ 𝑛))
83 an32 856 . . . . . . . . . . 11 ((((𝑞:ℕ⟶ℕ0 ∧ (𝑞 “ ℕ) ∈ Fin) ∧ ∀𝑛 ∈ (𝑞 “ ℕ) ¬ 2 ∥ 𝑛) ∧ Σ𝑘 ∈ ℕ ((𝑞𝑘) · 𝑘) = 𝑁) ↔ (((𝑞:ℕ⟶ℕ0 ∧ (𝑞 “ ℕ) ∈ Fin) ∧ Σ𝑘 ∈ ℕ ((𝑞𝑘) · 𝑘) = 𝑁) ∧ ∀𝑛 ∈ (𝑞 “ ℕ) ¬ 2 ∥ 𝑛))
8480, 82, 833bitr4i 292 . . . . . . . . . 10 ((𝑞𝑃 ∧ ∀𝑛 ∈ (𝑞 “ ℕ) ¬ 2 ∥ 𝑛) ↔ (((𝑞:ℕ⟶ℕ0 ∧ (𝑞 “ ℕ) ∈ Fin) ∧ ∀𝑛 ∈ (𝑞 “ ℕ) ¬ 2 ∥ 𝑛) ∧ Σ𝑘 ∈ ℕ ((𝑞𝑘) · 𝑘) = 𝑁))
8513, 14, 15, 16, 17, 18, 19, 20, 21eulerpartlemt0 30559 . . . . . . . . . . . . 13 (𝑞 ∈ (𝑇𝑅) ↔ (𝑞 ∈ (ℕ0𝑚 ℕ) ∧ (𝑞 “ ℕ) ∈ Fin ∧ (𝑞 “ ℕ) ⊆ 𝐽))
86 nnex 11064 . . . . . . . . . . . . . . 15 ℕ ∈ V
8745, 86elmap 7928 . . . . . . . . . . . . . 14 (𝑞 ∈ (ℕ0𝑚 ℕ) ↔ 𝑞:ℕ⟶ℕ0)
88873anbi1i 1272 . . . . . . . . . . . . 13 ((𝑞 ∈ (ℕ0𝑚 ℕ) ∧ (𝑞 “ ℕ) ∈ Fin ∧ (𝑞 “ ℕ) ⊆ 𝐽) ↔ (𝑞:ℕ⟶ℕ0 ∧ (𝑞 “ ℕ) ∈ Fin ∧ (𝑞 “ ℕ) ⊆ 𝐽))
8985, 88bitri 264 . . . . . . . . . . . 12 (𝑞 ∈ (𝑇𝑅) ↔ (𝑞:ℕ⟶ℕ0 ∧ (𝑞 “ ℕ) ∈ Fin ∧ (𝑞 “ ℕ) ⊆ 𝐽))
90 df-3an 1056 . . . . . . . . . . . 12 ((𝑞:ℕ⟶ℕ0 ∧ (𝑞 “ ℕ) ∈ Fin ∧ (𝑞 “ ℕ) ⊆ 𝐽) ↔ ((𝑞:ℕ⟶ℕ0 ∧ (𝑞 “ ℕ) ∈ Fin) ∧ (𝑞 “ ℕ) ⊆ 𝐽))
91 cnvimass 5520 . . . . . . . . . . . . . . . . . 18 (𝑞 “ ℕ) ⊆ dom 𝑞
92 fdm 6089 . . . . . . . . . . . . . . . . . 18 (𝑞:ℕ⟶ℕ0 → dom 𝑞 = ℕ)
9391, 92syl5sseq 3686 . . . . . . . . . . . . . . . . 17 (𝑞:ℕ⟶ℕ0 → (𝑞 “ ℕ) ⊆ ℕ)
94 dfss3 3625 . . . . . . . . . . . . . . . . 17 ((𝑞 “ ℕ) ⊆ ℕ ↔ ∀𝑛 ∈ (𝑞 “ ℕ)𝑛 ∈ ℕ)
9593, 94sylib 208 . . . . . . . . . . . . . . . 16 (𝑞:ℕ⟶ℕ0 → ∀𝑛 ∈ (𝑞 “ ℕ)𝑛 ∈ ℕ)
9695biantrurd 528 . . . . . . . . . . . . . . 15 (𝑞:ℕ⟶ℕ0 → (∀𝑛 ∈ (𝑞 “ ℕ) ¬ 2 ∥ 𝑛 ↔ (∀𝑛 ∈ (𝑞 “ ℕ)𝑛 ∈ ℕ ∧ ∀𝑛 ∈ (𝑞 “ ℕ) ¬ 2 ∥ 𝑛)))
97 dfss3 3625 . . . . . . . . . . . . . . . 16 ((𝑞 “ ℕ) ⊆ 𝐽 ↔ ∀𝑛 ∈ (𝑞 “ ℕ)𝑛𝐽)
98 breq2 4689 . . . . . . . . . . . . . . . . . . 19 (𝑧 = 𝑛 → (2 ∥ 𝑧 ↔ 2 ∥ 𝑛))
9998notbid 307 . . . . . . . . . . . . . . . . . 18 (𝑧 = 𝑛 → (¬ 2 ∥ 𝑧 ↔ ¬ 2 ∥ 𝑛))
10099, 16elrab2 3399 . . . . . . . . . . . . . . . . 17 (𝑛𝐽 ↔ (𝑛 ∈ ℕ ∧ ¬ 2 ∥ 𝑛))
101100ralbii 3009 . . . . . . . . . . . . . . . 16 (∀𝑛 ∈ (𝑞 “ ℕ)𝑛𝐽 ↔ ∀𝑛 ∈ (𝑞 “ ℕ)(𝑛 ∈ ℕ ∧ ¬ 2 ∥ 𝑛))
102 r19.26 3093 . . . . . . . . . . . . . . . 16 (∀𝑛 ∈ (𝑞 “ ℕ)(𝑛 ∈ ℕ ∧ ¬ 2 ∥ 𝑛) ↔ (∀𝑛 ∈ (𝑞 “ ℕ)𝑛 ∈ ℕ ∧ ∀𝑛 ∈ (𝑞 “ ℕ) ¬ 2 ∥ 𝑛))
10397, 101, 1023bitri 286 . . . . . . . . . . . . . . 15 ((𝑞 “ ℕ) ⊆ 𝐽 ↔ (∀𝑛 ∈ (𝑞 “ ℕ)𝑛 ∈ ℕ ∧ ∀𝑛 ∈ (𝑞 “ ℕ) ¬ 2 ∥ 𝑛))
10496, 103syl6rbbr 279 . . . . . . . . . . . . . 14 (𝑞:ℕ⟶ℕ0 → ((𝑞 “ ℕ) ⊆ 𝐽 ↔ ∀𝑛 ∈ (𝑞 “ ℕ) ¬ 2 ∥ 𝑛))
105104adantr 480 . . . . . . . . . . . . 13 ((𝑞:ℕ⟶ℕ0 ∧ (𝑞 “ ℕ) ∈ Fin) → ((𝑞 “ ℕ) ⊆ 𝐽 ↔ ∀𝑛 ∈ (𝑞 “ ℕ) ¬ 2 ∥ 𝑛))
106105pm5.32i 670 . . . . . . . . . . . 12 (((𝑞:ℕ⟶ℕ0 ∧ (𝑞 “ ℕ) ∈ Fin) ∧ (𝑞 “ ℕ) ⊆ 𝐽) ↔ ((𝑞:ℕ⟶ℕ0 ∧ (𝑞 “ ℕ) ∈ Fin) ∧ ∀𝑛 ∈ (𝑞 “ ℕ) ¬ 2 ∥ 𝑛))
10789, 90, 1063bitri 286 . . . . . . . . . . 11 (𝑞 ∈ (𝑇𝑅) ↔ ((𝑞:ℕ⟶ℕ0 ∧ (𝑞 “ ℕ) ∈ Fin) ∧ ∀𝑛 ∈ (𝑞 “ ℕ) ¬ 2 ∥ 𝑛))
108107anbi1i 731 . . . . . . . . . 10 ((𝑞 ∈ (𝑇𝑅) ∧ Σ𝑘 ∈ ℕ ((𝑞𝑘) · 𝑘) = 𝑁) ↔ (((𝑞:ℕ⟶ℕ0 ∧ (𝑞 “ ℕ) ∈ Fin) ∧ ∀𝑛 ∈ (𝑞 “ ℕ) ¬ 2 ∥ 𝑛) ∧ Σ𝑘 ∈ ℕ ((𝑞𝑘) · 𝑘) = 𝑁))
10984, 108bitr4i 267 . . . . . . . . 9 ((𝑞𝑃 ∧ ∀𝑛 ∈ (𝑞 “ ℕ) ¬ 2 ∥ 𝑛) ↔ (𝑞 ∈ (𝑇𝑅) ∧ Σ𝑘 ∈ ℕ ((𝑞𝑘) · 𝑘) = 𝑁))
110 rabid 3145 . . . . . . . . 9 (𝑞 ∈ {𝑞𝑃 ∣ ∀𝑛 ∈ (𝑞 “ ℕ) ¬ 2 ∥ 𝑛} ↔ (𝑞𝑃 ∧ ∀𝑛 ∈ (𝑞 “ ℕ) ¬ 2 ∥ 𝑛))
111 rabid 3145 . . . . . . . . 9 (𝑞 ∈ {𝑞 ∈ (𝑇𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑞𝑘) · 𝑘) = 𝑁} ↔ (𝑞 ∈ (𝑇𝑅) ∧ Σ𝑘 ∈ ℕ ((𝑞𝑘) · 𝑘) = 𝑁))
112109, 110, 1113bitr4i 292 . . . . . . . 8 (𝑞 ∈ {𝑞𝑃 ∣ ∀𝑛 ∈ (𝑞 “ ℕ) ¬ 2 ∥ 𝑛} ↔ 𝑞 ∈ {𝑞 ∈ (𝑇𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑞𝑘) · 𝑘) = 𝑁})
11377, 78, 112eqri 29443 . . . . . . 7 {𝑞𝑃 ∣ ∀𝑛 ∈ (𝑞 “ ℕ) ¬ 2 ∥ 𝑛} = {𝑞 ∈ (𝑇𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑞𝑘) · 𝑘) = 𝑁}
11414, 76, 1133eqtri 2677 . . . . . 6 𝑂 = {𝑞 ∈ (𝑇𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑞𝑘) · 𝑘) = 𝑁}
115114reseq2i 5425 . . . . 5 (𝐺𝑂) = (𝐺 ↾ {𝑞 ∈ (𝑇𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑞𝑘) · 𝑘) = 𝑁})
116115a1i 11 . . . 4 (⊤ → (𝐺𝑂) = (𝐺 ↾ {𝑞 ∈ (𝑇𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑞𝑘) · 𝑘) = 𝑁}))
117114a1i 11 . . . 4 (⊤ → 𝑂 = {𝑞 ∈ (𝑇𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑞𝑘) · 𝑘) = 𝑁})
118 nfcv 2793 . . . . . 6 𝑑𝐷
119 nfrab1 3152 . . . . . 6 𝑑{𝑑 ∈ (({0, 1} ↑𝑚 ℕ) ∩ 𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑑𝑘) · 𝑘) = 𝑁}
120 fnima 6048 . . . . . . . . . . . . . . . . 17 (𝑑 Fn ℕ → (𝑑 “ ℕ) = ran 𝑑)
121120sseq1d 3665 . . . . . . . . . . . . . . . 16 (𝑑 Fn ℕ → ((𝑑 “ ℕ) ⊆ {0, 1} ↔ ran 𝑑 ⊆ {0, 1}))
122121anbi2d 740 . . . . . . . . . . . . . . 15 (𝑑 Fn ℕ → ((ran 𝑑 ⊆ ℕ0 ∧ (𝑑 “ ℕ) ⊆ {0, 1}) ↔ (ran 𝑑 ⊆ ℕ0 ∧ ran 𝑑 ⊆ {0, 1})))
123 sstr 3644 . . . . . . . . . . . . . . . . 17 ((ran 𝑑 ⊆ {0, 1} ∧ {0, 1} ⊆ ℕ0) → ran 𝑑 ⊆ ℕ0)
12449, 123mpan2 707 . . . . . . . . . . . . . . . 16 (ran 𝑑 ⊆ {0, 1} → ran 𝑑 ⊆ ℕ0)
125124pm4.71ri 666 . . . . . . . . . . . . . . 15 (ran 𝑑 ⊆ {0, 1} ↔ (ran 𝑑 ⊆ ℕ0 ∧ ran 𝑑 ⊆ {0, 1}))
126122, 125syl6bbr 278 . . . . . . . . . . . . . 14 (𝑑 Fn ℕ → ((ran 𝑑 ⊆ ℕ0 ∧ (𝑑 “ ℕ) ⊆ {0, 1}) ↔ ran 𝑑 ⊆ {0, 1}))
127126pm5.32i 670 . . . . . . . . . . . . 13 ((𝑑 Fn ℕ ∧ (ran 𝑑 ⊆ ℕ0 ∧ (𝑑 “ ℕ) ⊆ {0, 1})) ↔ (𝑑 Fn ℕ ∧ ran 𝑑 ⊆ {0, 1}))
128 anass 682 . . . . . . . . . . . . 13 (((𝑑 Fn ℕ ∧ ran 𝑑 ⊆ ℕ0) ∧ (𝑑 “ ℕ) ⊆ {0, 1}) ↔ (𝑑 Fn ℕ ∧ (ran 𝑑 ⊆ ℕ0 ∧ (𝑑 “ ℕ) ⊆ {0, 1})))
129 df-f 5930 . . . . . . . . . . . . 13 (𝑑:ℕ⟶{0, 1} ↔ (𝑑 Fn ℕ ∧ ran 𝑑 ⊆ {0, 1}))
130127, 128, 1293bitr4ri 293 . . . . . . . . . . . 12 (𝑑:ℕ⟶{0, 1} ↔ ((𝑑 Fn ℕ ∧ ran 𝑑 ⊆ ℕ0) ∧ (𝑑 “ ℕ) ⊆ {0, 1}))
131 prex 4939 . . . . . . . . . . . . 13 {0, 1} ∈ V
132131, 86elmap 7928 . . . . . . . . . . . 12 (𝑑 ∈ ({0, 1} ↑𝑚 ℕ) ↔ 𝑑:ℕ⟶{0, 1})
133 df-f 5930 . . . . . . . . . . . . 13 (𝑑:ℕ⟶ℕ0 ↔ (𝑑 Fn ℕ ∧ ran 𝑑 ⊆ ℕ0))
134133anbi1i 731 . . . . . . . . . . . 12 ((𝑑:ℕ⟶ℕ0 ∧ (𝑑 “ ℕ) ⊆ {0, 1}) ↔ ((𝑑 Fn ℕ ∧ ran 𝑑 ⊆ ℕ0) ∧ (𝑑 “ ℕ) ⊆ {0, 1}))
135130, 132, 1343bitr4i 292 . . . . . . . . . . 11 (𝑑 ∈ ({0, 1} ↑𝑚 ℕ) ↔ (𝑑:ℕ⟶ℕ0 ∧ (𝑑 “ ℕ) ⊆ {0, 1}))
136 vex 3234 . . . . . . . . . . . 12 𝑑 ∈ V
137 cnveq 5328 . . . . . . . . . . . . . 14 (𝑓 = 𝑑𝑓 = 𝑑)
138137imaeq1d 5500 . . . . . . . . . . . . 13 (𝑓 = 𝑑 → (𝑓 “ ℕ) = (𝑑 “ ℕ))
139138eleq1d 2715 . . . . . . . . . . . 12 (𝑓 = 𝑑 → ((𝑓 “ ℕ) ∈ Fin ↔ (𝑑 “ ℕ) ∈ Fin))
140136, 139, 20elab2 3386 . . . . . . . . . . 11 (𝑑𝑅 ↔ (𝑑 “ ℕ) ∈ Fin)
141135, 140anbi12i 733 . . . . . . . . . 10 ((𝑑 ∈ ({0, 1} ↑𝑚 ℕ) ∧ 𝑑𝑅) ↔ ((𝑑:ℕ⟶ℕ0 ∧ (𝑑 “ ℕ) ⊆ {0, 1}) ∧ (𝑑 “ ℕ) ∈ Fin))
142 elin 3829 . . . . . . . . . 10 (𝑑 ∈ (({0, 1} ↑𝑚 ℕ) ∩ 𝑅) ↔ (𝑑 ∈ ({0, 1} ↑𝑚 ℕ) ∧ 𝑑𝑅))
143 an32 856 . . . . . . . . . 10 (((𝑑:ℕ⟶ℕ0 ∧ (𝑑 “ ℕ) ∈ Fin) ∧ (𝑑 “ ℕ) ⊆ {0, 1}) ↔ ((𝑑:ℕ⟶ℕ0 ∧ (𝑑 “ ℕ) ⊆ {0, 1}) ∧ (𝑑 “ ℕ) ∈ Fin))
144141, 142, 1433bitr4i 292 . . . . . . . . 9 (𝑑 ∈ (({0, 1} ↑𝑚 ℕ) ∩ 𝑅) ↔ ((𝑑:ℕ⟶ℕ0 ∧ (𝑑 “ ℕ) ∈ Fin) ∧ (𝑑 “ ℕ) ⊆ {0, 1}))
145144anbi1i 731 . . . . . . . 8 ((𝑑 ∈ (({0, 1} ↑𝑚 ℕ) ∩ 𝑅) ∧ Σ𝑘 ∈ ℕ ((𝑑𝑘) · 𝑘) = 𝑁) ↔ (((𝑑:ℕ⟶ℕ0 ∧ (𝑑 “ ℕ) ∈ Fin) ∧ (𝑑 “ ℕ) ⊆ {0, 1}) ∧ Σ𝑘 ∈ ℕ ((𝑑𝑘) · 𝑘) = 𝑁))
14613eulerpartleme 30553 . . . . . . . . . 10 (𝑑𝑃 ↔ (𝑑:ℕ⟶ℕ0 ∧ (𝑑 “ ℕ) ∈ Fin ∧ Σ𝑘 ∈ ℕ ((𝑑𝑘) · 𝑘) = 𝑁))
147146anbi1i 731 . . . . . . . . 9 ((𝑑𝑃 ∧ (𝑑 “ ℕ) ⊆ {0, 1}) ↔ ((𝑑:ℕ⟶ℕ0 ∧ (𝑑 “ ℕ) ∈ Fin ∧ Σ𝑘 ∈ ℕ ((𝑑𝑘) · 𝑘) = 𝑁) ∧ (𝑑 “ ℕ) ⊆ {0, 1}))
148 df-3an 1056 . . . . . . . . . 10 ((𝑑:ℕ⟶ℕ0 ∧ (𝑑 “ ℕ) ∈ Fin ∧ Σ𝑘 ∈ ℕ ((𝑑𝑘) · 𝑘) = 𝑁) ↔ ((𝑑:ℕ⟶ℕ0 ∧ (𝑑 “ ℕ) ∈ Fin) ∧ Σ𝑘 ∈ ℕ ((𝑑𝑘) · 𝑘) = 𝑁))
149148anbi1i 731 . . . . . . . . 9 (((𝑑:ℕ⟶ℕ0 ∧ (𝑑 “ ℕ) ∈ Fin ∧ Σ𝑘 ∈ ℕ ((𝑑𝑘) · 𝑘) = 𝑁) ∧ (𝑑 “ ℕ) ⊆ {0, 1}) ↔ (((𝑑:ℕ⟶ℕ0 ∧ (𝑑 “ ℕ) ∈ Fin) ∧ Σ𝑘 ∈ ℕ ((𝑑𝑘) · 𝑘) = 𝑁) ∧ (𝑑 “ ℕ) ⊆ {0, 1}))
150 an32 856 . . . . . . . . 9 ((((𝑑:ℕ⟶ℕ0 ∧ (𝑑 “ ℕ) ∈ Fin) ∧ Σ𝑘 ∈ ℕ ((𝑑𝑘) · 𝑘) = 𝑁) ∧ (𝑑 “ ℕ) ⊆ {0, 1}) ↔ (((𝑑:ℕ⟶ℕ0 ∧ (𝑑 “ ℕ) ∈ Fin) ∧ (𝑑 “ ℕ) ⊆ {0, 1}) ∧ Σ𝑘 ∈ ℕ ((𝑑𝑘) · 𝑘) = 𝑁))
151147, 149, 1503bitri 286 . . . . . . . 8 ((𝑑𝑃 ∧ (𝑑 “ ℕ) ⊆ {0, 1}) ↔ (((𝑑:ℕ⟶ℕ0 ∧ (𝑑 “ ℕ) ∈ Fin) ∧ (𝑑 “ ℕ) ⊆ {0, 1}) ∧ Σ𝑘 ∈ ℕ ((𝑑𝑘) · 𝑘) = 𝑁))
152145, 151bitr4i 267 . . . . . . 7 ((𝑑 ∈ (({0, 1} ↑𝑚 ℕ) ∩ 𝑅) ∧ Σ𝑘 ∈ ℕ ((𝑑𝑘) · 𝑘) = 𝑁) ↔ (𝑑𝑃 ∧ (𝑑 “ ℕ) ⊆ {0, 1}))
153 rabid 3145 . . . . . . 7 (𝑑 ∈ {𝑑 ∈ (({0, 1} ↑𝑚 ℕ) ∩ 𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑑𝑘) · 𝑘) = 𝑁} ↔ (𝑑 ∈ (({0, 1} ↑𝑚 ℕ) ∩ 𝑅) ∧ Σ𝑘 ∈ ℕ ((𝑑𝑘) · 𝑘) = 𝑁))
15413, 14, 15eulerpartlemd 30556 . . . . . . 7 (𝑑𝐷 ↔ (𝑑𝑃 ∧ (𝑑 “ ℕ) ⊆ {0, 1}))
155152, 153, 1543bitr4ri 293 . . . . . 6 (𝑑𝐷𝑑 ∈ {𝑑 ∈ (({0, 1} ↑𝑚 ℕ) ∩ 𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑑𝑘) · 𝑘) = 𝑁})
156118, 119, 155eqri 29443 . . . . 5 𝐷 = {𝑑 ∈ (({0, 1} ↑𝑚 ℕ) ∩ 𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑑𝑘) · 𝑘) = 𝑁}
157156a1i 11 . . . 4 (⊤ → 𝐷 = {𝑑 ∈ (({0, 1} ↑𝑚 ℕ) ∩ 𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑑𝑘) · 𝑘) = 𝑁})
158116, 117, 157f1oeq123d 6171 . . 3 (⊤ → ((𝐺𝑂):𝑂1-1-onto𝐷 ↔ (𝐺 ↾ {𝑞 ∈ (𝑇𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑞𝑘) · 𝑘) = 𝑁}):{𝑞 ∈ (𝑇𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑞𝑘) · 𝑘) = 𝑁}–1-1-onto→{𝑑 ∈ (({0, 1} ↑𝑚 ℕ) ∩ 𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑑𝑘) · 𝑘) = 𝑁}))
15972, 158mpbird 247 . 2 (⊤ → (𝐺𝑂):𝑂1-1-onto𝐷)
160159trud 1533 1 (𝐺𝑂):𝑂1-1-onto𝐷
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 383  w3a 1054   = wceq 1523  wtru 1524  wcel 2030  {cab 2637  wral 2941  {crab 2945  Vcvv 3231  cin 3606  wss 3607  c0 3948  𝒫 cpw 4191  {cpr 4212   class class class wbr 4685  {copab 4745  cmpt 4762  ccnv 5142  dom cdm 5143  ran crn 5144  cres 5145  cima 5146  ccom 5147   Fn wfn 5921  wf 5922  1-1-ontowf1o 5925  cfv 5926  (class class class)co 6690  cmpt2 6692   supp csupp 7340  𝑚 cmap 7899  Fincfn 7997  0cc0 9974  1c1 9975   · cmul 9979  cle 10113  cn 11058  2c2 11108  0cn0 11330  cexp 12900  Σcsu 14460  cdvds 15027  bitscbits 15188  𝟭cind 30200
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-rep 4804  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991  ax-inf2 8576  ax-ac2 9323  ax-cnex 10030  ax-resscn 10031  ax-1cn 10032  ax-icn 10033  ax-addcl 10034  ax-addrcl 10035  ax-mulcl 10036  ax-mulrcl 10037  ax-mulcom 10038  ax-addass 10039  ax-mulass 10040  ax-distr 10041  ax-i2m1 10042  ax-1ne0 10043  ax-1rid 10044  ax-rnegex 10045  ax-rrecex 10046  ax-cnre 10047  ax-pre-lttri 10048  ax-pre-lttrn 10049  ax-pre-ltadd 10050  ax-pre-mulgt0 10051  ax-pre-sup 10052
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-fal 1529  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-nel 2927  df-ral 2946  df-rex 2947  df-reu 2948  df-rmo 2949  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-int 4508  df-iun 4554  df-disj 4653  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-se 5103  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-pred 5718  df-ord 5764  df-on 5765  df-lim 5766  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-isom 5935  df-riota 6651  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-om 7108  df-1st 7210  df-2nd 7211  df-supp 7341  df-wrecs 7452  df-recs 7513  df-rdg 7551  df-1o 7605  df-2o 7606  df-oadd 7609  df-er 7787  df-map 7901  df-pm 7902  df-en 7998  df-dom 7999  df-sdom 8000  df-fin 8001  df-fsupp 8317  df-sup 8389  df-inf 8390  df-oi 8456  df-card 8803  df-acn 8806  df-ac 8977  df-cda 9028  df-pnf 10114  df-mnf 10115  df-xr 10116  df-ltxr 10117  df-le 10118  df-sub 10306  df-neg 10307  df-div 10723  df-nn 11059  df-2 11117  df-3 11118  df-n0 11331  df-xnn0 11402  df-z 11416  df-uz 11726  df-rp 11871  df-fz 12365  df-fzo 12505  df-fl 12633  df-mod 12709  df-seq 12842  df-exp 12901  df-hash 13158  df-cj 13883  df-re 13884  df-im 13885  df-sqrt 14019  df-abs 14020  df-clim 14263  df-sum 14461  df-dvds 15028  df-bits 15191  df-ind 30201
This theorem is referenced by:  eulerpart  30572
  Copyright terms: Public domain W3C validator