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 30800
Description: Lemma for eulerpart 30801. (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 469 . . . . . . . . . . . . 13 ((𝑜 = 𝑞𝑘 ∈ ℕ) → 𝑜 = 𝑞)
21fveq1d 6350 . . . . . . . . . . . 12 ((𝑜 = 𝑞𝑘 ∈ ℕ) → (𝑜𝑘) = (𝑞𝑘))
32oveq1d 6827 . . . . . . . . . . 11 ((𝑜 = 𝑞𝑘 ∈ ℕ) → ((𝑜𝑘) · 𝑘) = ((𝑞𝑘) · 𝑘))
43sumeq2dv 14663 . . . . . . . . . 10 (𝑜 = 𝑞 → Σ𝑘 ∈ ℕ ((𝑜𝑘) · 𝑘) = Σ𝑘 ∈ ℕ ((𝑞𝑘) · 𝑘))
54eqeq1d 2776 . . . . . . . . 9 (𝑜 = 𝑞 → (Σ𝑘 ∈ ℕ ((𝑜𝑘) · 𝑘) = 𝑁 ↔ Σ𝑘 ∈ ℕ ((𝑞𝑘) · 𝑘) = 𝑁))
65cbvrabv 3353 . . . . . . . 8 {𝑜 ∈ (𝑇𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑜𝑘) · 𝑘) = 𝑁} = {𝑞 ∈ (𝑇𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑞𝑘) · 𝑘) = 𝑁}
76a1i 11 . . . . . . 7 (𝑜 = 𝑞 → {𝑜 ∈ (𝑇𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑜𝑘) · 𝑘) = 𝑁} = {𝑞 ∈ (𝑇𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑞𝑘) · 𝑘) = 𝑁})
87reseq2d 5546 . . . . . 6 (𝑜 = 𝑞 → (𝐺 ↾ {𝑜 ∈ (𝑇𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑜𝑘) · 𝑘) = 𝑁}) = (𝐺 ↾ {𝑞 ∈ (𝑇𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑞𝑘) · 𝑘) = 𝑁}))
9 eqidd 2775 . . . . . 6 (𝑜 = 𝑞 → {𝑑 ∈ (({0, 1} ↑𝑚 ℕ) ∩ 𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑑𝑘) · 𝑘) = 𝑁} = {𝑑 ∈ (({0, 1} ↑𝑚 ℕ) ∩ 𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑑𝑘) · 𝑘) = 𝑁})
108, 7, 9f1oeq123d 6289 . . . . 5 (𝑜 = 𝑞 → ((𝐺 ↾ {𝑜 ∈ (𝑇𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑜𝑘) · 𝑘) = 𝑁}):{𝑜 ∈ (𝑇𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑜𝑘) · 𝑘) = 𝑁}–1-1-onto→{𝑑 ∈ (({0, 1} ↑𝑚 ℕ) ∩ 𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑑𝑘) · 𝑘) = 𝑁} ↔ (𝐺 ↾ {𝑞 ∈ (𝑇𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑞𝑘) · 𝑘) = 𝑁}):{𝑞 ∈ (𝑇𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑞𝑘) · 𝑘) = 𝑁}–1-1-onto→{𝑑 ∈ (({0, 1} ↑𝑚 ℕ) ∩ 𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑑𝑘) · 𝑘) = 𝑁}))
1110imbi2d 330 . . . 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 30791 . . . . . 6 𝐺:(𝑇𝑅)–1-1-onto→(({0, 1} ↑𝑚 ℕ) ∩ 𝑅)
2322a1i 11 . . . . 5 (⊤ → 𝐺:(𝑇𝑅)–1-1-onto→(({0, 1} ↑𝑚 ℕ) ∩ 𝑅))
24 fveq2 6348 . . . . . . . . . . . . . 14 (𝑞 = 𝑜 → (𝐺𝑞) = (𝐺𝑜))
25 reseq1 5540 . . . . . . . . . . . . . . . . . 18 (𝑞 = 𝑜 → (𝑞𝐽) = (𝑜𝐽))
2625coeq2d 5435 . . . . . . . . . . . . . . . . 17 (𝑞 = 𝑜 → (bits ∘ (𝑞𝐽)) = (bits ∘ (𝑜𝐽)))
2726fveq2d 6352 . . . . . . . . . . . . . . . 16 (𝑞 = 𝑜 → (𝑀‘(bits ∘ (𝑞𝐽))) = (𝑀‘(bits ∘ (𝑜𝐽))))
2827imaeq2d 5617 . . . . . . . . . . . . . . 15 (𝑞 = 𝑜 → (𝐹 “ (𝑀‘(bits ∘ (𝑞𝐽)))) = (𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽)))))
2928fveq2d 6352 . . . . . . . . . . . . . 14 (𝑞 = 𝑜 → ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑞𝐽))))) = ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽))))))
3024, 29eqeq12d 2789 . . . . . . . . . . . . 13 (𝑞 = 𝑜 → ((𝐺𝑞) = ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑞𝐽))))) ↔ (𝐺𝑜) = ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽)))))))
3113, 14, 15, 16, 17, 18, 19, 20, 21, 12eulerpartlemgv 30792 . . . . . . . . . . . . 13 (𝑞 ∈ (𝑇𝑅) → (𝐺𝑞) = ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑞𝐽))))))
3230, 31vtoclga 3428 . . . . . . . . . . . 12 (𝑜 ∈ (𝑇𝑅) → (𝐺𝑜) = ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽))))))
33323ad2ant2 1155 . . . . . . . . . . 11 ((⊤ ∧ 𝑜 ∈ (𝑇𝑅) ∧ 𝑑 = ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽)))))) → (𝐺𝑜) = ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽))))))
34 simp3 1159 . . . . . . . . . . 11 ((⊤ ∧ 𝑜 ∈ (𝑇𝑅) ∧ 𝑑 = ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽)))))) → 𝑑 = ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽))))))
3533, 34eqtr4d 2811 . . . . . . . . . 10 ((⊤ ∧ 𝑜 ∈ (𝑇𝑅) ∧ 𝑑 = ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽)))))) → (𝐺𝑜) = 𝑑)
3635fveq1d 6350 . . . . . . . . 9 ((⊤ ∧ 𝑜 ∈ (𝑇𝑅) ∧ 𝑑 = ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽)))))) → ((𝐺𝑜)‘𝑘) = (𝑑𝑘))
3736oveq1d 6827 . . . . . . . 8 ((⊤ ∧ 𝑜 ∈ (𝑇𝑅) ∧ 𝑑 = ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽)))))) → (((𝐺𝑜)‘𝑘) · 𝑘) = ((𝑑𝑘) · 𝑘))
3837sumeq2sdv 14665 . . . . . . 7 ((⊤ ∧ 𝑜 ∈ (𝑇𝑅) ∧ 𝑑 = ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽)))))) → Σ𝑘 ∈ ℕ (((𝐺𝑜)‘𝑘) · 𝑘) = Σ𝑘 ∈ ℕ ((𝑑𝑘) · 𝑘))
3924fveq2d 6352 . . . . . . . . . . 11 (𝑞 = 𝑜 → (𝑆‘(𝐺𝑞)) = (𝑆‘(𝐺𝑜)))
40 fveq2 6348 . . . . . . . . . . 11 (𝑞 = 𝑜 → (𝑆𝑞) = (𝑆𝑜))
4139, 40eqeq12d 2789 . . . . . . . . . 10 (𝑞 = 𝑜 → ((𝑆‘(𝐺𝑞)) = (𝑆𝑞) ↔ (𝑆‘(𝐺𝑜)) = (𝑆𝑜)))
42 eulerpart.s . . . . . . . . . . 11 𝑆 = (𝑓 ∈ ((ℕ0𝑚 ℕ) ∩ 𝑅) ↦ Σ𝑘 ∈ ℕ ((𝑓𝑘) · 𝑘))
4313, 14, 15, 16, 17, 18, 19, 20, 21, 12, 42eulerpartlemgs2 30799 . . . . . . . . . 10 (𝑞 ∈ (𝑇𝑅) → (𝑆‘(𝐺𝑞)) = (𝑆𝑞))
4441, 43vtoclga 3428 . . . . . . . . 9 (𝑜 ∈ (𝑇𝑅) → (𝑆‘(𝐺𝑜)) = (𝑆𝑜))
45 nn0ex 11522 . . . . . . . . . . . . 13 0 ∈ V
46 0nn0 11531 . . . . . . . . . . . . . 14 0 ∈ ℕ0
47 1nn0 11532 . . . . . . . . . . . . . 14 1 ∈ ℕ0
48 prssi 4498 . . . . . . . . . . . . . 14 ((0 ∈ ℕ0 ∧ 1 ∈ ℕ0) → {0, 1} ⊆ ℕ0)
4946, 47, 48mp2an 673 . . . . . . . . . . . . 13 {0, 1} ⊆ ℕ0
50 mapss 8075 . . . . . . . . . . . . 13 ((ℕ0 ∈ V ∧ {0, 1} ⊆ ℕ0) → ({0, 1} ↑𝑚 ℕ) ⊆ (ℕ0𝑚 ℕ))
5145, 49, 50mp2an 673 . . . . . . . . . . . 12 ({0, 1} ↑𝑚 ℕ) ⊆ (ℕ0𝑚 ℕ)
52 ssrin 3993 . . . . . . . . . . . 12 (({0, 1} ↑𝑚 ℕ) ⊆ (ℕ0𝑚 ℕ) → (({0, 1} ↑𝑚 ℕ) ∩ 𝑅) ⊆ ((ℕ0𝑚 ℕ) ∩ 𝑅))
5351, 52ax-mp 5 . . . . . . . . . . 11 (({0, 1} ↑𝑚 ℕ) ∩ 𝑅) ⊆ ((ℕ0𝑚 ℕ) ∩ 𝑅)
54 f1of 6293 . . . . . . . . . . . . 13 (𝐺:(𝑇𝑅)–1-1-onto→(({0, 1} ↑𝑚 ℕ) ∩ 𝑅) → 𝐺:(𝑇𝑅)⟶(({0, 1} ↑𝑚 ℕ) ∩ 𝑅))
5522, 54ax-mp 5 . . . . . . . . . . . 12 𝐺:(𝑇𝑅)⟶(({0, 1} ↑𝑚 ℕ) ∩ 𝑅)
5655ffvelrni 6518 . . . . . . . . . . 11 (𝑜 ∈ (𝑇𝑅) → (𝐺𝑜) ∈ (({0, 1} ↑𝑚 ℕ) ∩ 𝑅))
5753, 56sseldi 3756 . . . . . . . . . 10 (𝑜 ∈ (𝑇𝑅) → (𝐺𝑜) ∈ ((ℕ0𝑚 ℕ) ∩ 𝑅))
5820, 42eulerpartlemsv1 30775 . . . . . . . . . 10 ((𝐺𝑜) ∈ ((ℕ0𝑚 ℕ) ∩ 𝑅) → (𝑆‘(𝐺𝑜)) = Σ𝑘 ∈ ℕ (((𝐺𝑜)‘𝑘) · 𝑘))
5957, 58syl 17 . . . . . . . . 9 (𝑜 ∈ (𝑇𝑅) → (𝑆‘(𝐺𝑜)) = Σ𝑘 ∈ ℕ (((𝐺𝑜)‘𝑘) · 𝑘))
6013, 14, 15, 16, 17, 18, 19, 20, 21eulerpartlemt0 30788 . . . . . . . . . . . 12 (𝑜 ∈ (𝑇𝑅) ↔ (𝑜 ∈ (ℕ0𝑚 ℕ) ∧ (𝑜 “ ℕ) ∈ Fin ∧ (𝑜 “ ℕ) ⊆ 𝐽))
6160simp1bi 1166 . . . . . . . . . . 11 (𝑜 ∈ (𝑇𝑅) → 𝑜 ∈ (ℕ0𝑚 ℕ))
62 inss2 3989 . . . . . . . . . . . 12 (𝑇𝑅) ⊆ 𝑅
6362sseli 3754 . . . . . . . . . . 11 (𝑜 ∈ (𝑇𝑅) → 𝑜𝑅)
6461, 63elind 3956 . . . . . . . . . 10 (𝑜 ∈ (𝑇𝑅) → 𝑜 ∈ ((ℕ0𝑚 ℕ) ∩ 𝑅))
6520, 42eulerpartlemsv1 30775 . . . . . . . . . 10 (𝑜 ∈ ((ℕ0𝑚 ℕ) ∩ 𝑅) → (𝑆𝑜) = Σ𝑘 ∈ ℕ ((𝑜𝑘) · 𝑘))
6664, 65syl 17 . . . . . . . . 9 (𝑜 ∈ (𝑇𝑅) → (𝑆𝑜) = Σ𝑘 ∈ ℕ ((𝑜𝑘) · 𝑘))
6744, 59, 663eqtr3d 2816 . . . . . . . 8 (𝑜 ∈ (𝑇𝑅) → Σ𝑘 ∈ ℕ (((𝐺𝑜)‘𝑘) · 𝑘) = Σ𝑘 ∈ ℕ ((𝑜𝑘) · 𝑘))
68673ad2ant2 1155 . . . . . . 7 ((⊤ ∧ 𝑜 ∈ (𝑇𝑅) ∧ 𝑑 = ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽)))))) → Σ𝑘 ∈ ℕ (((𝐺𝑜)‘𝑘) · 𝑘) = Σ𝑘 ∈ ℕ ((𝑜𝑘) · 𝑘))
6938, 68eqtr3d 2810 . . . . . 6 ((⊤ ∧ 𝑜 ∈ (𝑇𝑅) ∧ 𝑑 = ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽)))))) → Σ𝑘 ∈ ℕ ((𝑑𝑘) · 𝑘) = Σ𝑘 ∈ ℕ ((𝑜𝑘) · 𝑘))
7069eqeq1d 2776 . . . . 5 ((⊤ ∧ 𝑜 ∈ (𝑇𝑅) ∧ 𝑑 = ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽)))))) → (Σ𝑘 ∈ ℕ ((𝑑𝑘) · 𝑘) = 𝑁 ↔ Σ𝑘 ∈ ℕ ((𝑜𝑘) · 𝑘) = 𝑁))
7112, 23, 70f1oresrab 6555 . . . 4 (⊤ → (𝐺 ↾ {𝑜 ∈ (𝑇𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑜𝑘) · 𝑘) = 𝑁}):{𝑜 ∈ (𝑇𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑜𝑘) · 𝑘) = 𝑁}–1-1-onto→{𝑑 ∈ (({0, 1} ↑𝑚 ℕ) ∩ 𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑑𝑘) · 𝑘) = 𝑁})
7211, 71chvarv 2428 . . 3 (⊤ → (𝐺 ↾ {𝑞 ∈ (𝑇𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑞𝑘) · 𝑘) = 𝑁}):{𝑞 ∈ (𝑇𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑞𝑘) · 𝑘) = 𝑁}–1-1-onto→{𝑑 ∈ (({0, 1} ↑𝑚 ℕ) ∩ 𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑑𝑘) · 𝑘) = 𝑁})
73 cnveq 5446 . . . . . . . . . 10 (𝑔 = 𝑞𝑔 = 𝑞)
7473imaeq1d 5616 . . . . . . . . 9 (𝑔 = 𝑞 → (𝑔 “ ℕ) = (𝑞 “ ℕ))
7574raleqdv 3297 . . . . . . . 8 (𝑔 = 𝑞 → (∀𝑛 ∈ (𝑔 “ ℕ) ¬ 2 ∥ 𝑛 ↔ ∀𝑛 ∈ (𝑞 “ ℕ) ¬ 2 ∥ 𝑛))
7675cbvrabv 3353 . . . . . . 7 {𝑔𝑃 ∣ ∀𝑛 ∈ (𝑔 “ ℕ) ¬ 2 ∥ 𝑛} = {𝑞𝑃 ∣ ∀𝑛 ∈ (𝑞 “ ℕ) ¬ 2 ∥ 𝑛}
77 nfrab1 3275 . . . . . . . 8 𝑞{𝑞𝑃 ∣ ∀𝑛 ∈ (𝑞 “ ℕ) ¬ 2 ∥ 𝑛}
78 nfrab1 3275 . . . . . . . 8 𝑞{𝑞 ∈ (𝑇𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑞𝑘) · 𝑘) = 𝑁}
79 df-3an 1100 . . . . . . . . . . . 12 ((𝑞:ℕ⟶ℕ0 ∧ (𝑞 “ ℕ) ∈ Fin ∧ Σ𝑘 ∈ ℕ ((𝑞𝑘) · 𝑘) = 𝑁) ↔ ((𝑞:ℕ⟶ℕ0 ∧ (𝑞 “ ℕ) ∈ Fin) ∧ Σ𝑘 ∈ ℕ ((𝑞𝑘) · 𝑘) = 𝑁))
8079anbi1i 611 . . . . . . . . . . 11 (((𝑞:ℕ⟶ℕ0 ∧ (𝑞 “ ℕ) ∈ Fin ∧ Σ𝑘 ∈ ℕ ((𝑞𝑘) · 𝑘) = 𝑁) ∧ ∀𝑛 ∈ (𝑞 “ ℕ) ¬ 2 ∥ 𝑛) ↔ (((𝑞:ℕ⟶ℕ0 ∧ (𝑞 “ ℕ) ∈ Fin) ∧ Σ𝑘 ∈ ℕ ((𝑞𝑘) · 𝑘) = 𝑁) ∧ ∀𝑛 ∈ (𝑞 “ ℕ) ¬ 2 ∥ 𝑛))
8113eulerpartleme 30782 . . . . . . . . . . . 12 (𝑞𝑃 ↔ (𝑞:ℕ⟶ℕ0 ∧ (𝑞 “ ℕ) ∈ Fin ∧ Σ𝑘 ∈ ℕ ((𝑞𝑘) · 𝑘) = 𝑁))
8281anbi1i 611 . . . . . . . . . . 11 ((𝑞𝑃 ∧ ∀𝑛 ∈ (𝑞 “ ℕ) ¬ 2 ∥ 𝑛) ↔ ((𝑞:ℕ⟶ℕ0 ∧ (𝑞 “ ℕ) ∈ Fin ∧ Σ𝑘 ∈ ℕ ((𝑞𝑘) · 𝑘) = 𝑁) ∧ ∀𝑛 ∈ (𝑞 “ ℕ) ¬ 2 ∥ 𝑛))
83 an32 626 . . . . . . . . . . 11 ((((𝑞:ℕ⟶ℕ0 ∧ (𝑞 “ ℕ) ∈ Fin) ∧ ∀𝑛 ∈ (𝑞 “ ℕ) ¬ 2 ∥ 𝑛) ∧ Σ𝑘 ∈ ℕ ((𝑞𝑘) · 𝑘) = 𝑁) ↔ (((𝑞:ℕ⟶ℕ0 ∧ (𝑞 “ ℕ) ∈ Fin) ∧ Σ𝑘 ∈ ℕ ((𝑞𝑘) · 𝑘) = 𝑁) ∧ ∀𝑛 ∈ (𝑞 “ ℕ) ¬ 2 ∥ 𝑛))
8480, 82, 833bitr4i 293 . . . . . . . . . 10 ((𝑞𝑃 ∧ ∀𝑛 ∈ (𝑞 “ ℕ) ¬ 2 ∥ 𝑛) ↔ (((𝑞:ℕ⟶ℕ0 ∧ (𝑞 “ ℕ) ∈ Fin) ∧ ∀𝑛 ∈ (𝑞 “ ℕ) ¬ 2 ∥ 𝑛) ∧ Σ𝑘 ∈ ℕ ((𝑞𝑘) · 𝑘) = 𝑁))
8513, 14, 15, 16, 17, 18, 19, 20, 21eulerpartlemt0 30788 . . . . . . . . . . . . 13 (𝑞 ∈ (𝑇𝑅) ↔ (𝑞 ∈ (ℕ0𝑚 ℕ) ∧ (𝑞 “ ℕ) ∈ Fin ∧ (𝑞 “ ℕ) ⊆ 𝐽))
86 nnex 11249 . . . . . . . . . . . . . . 15 ℕ ∈ V
8745, 86elmap 8059 . . . . . . . . . . . . . 14 (𝑞 ∈ (ℕ0𝑚 ℕ) ↔ 𝑞:ℕ⟶ℕ0)
88873anbi1i 1187 . . . . . . . . . . . . 13 ((𝑞 ∈ (ℕ0𝑚 ℕ) ∧ (𝑞 “ ℕ) ∈ Fin ∧ (𝑞 “ ℕ) ⊆ 𝐽) ↔ (𝑞:ℕ⟶ℕ0 ∧ (𝑞 “ ℕ) ∈ Fin ∧ (𝑞 “ ℕ) ⊆ 𝐽))
8985, 88bitri 265 . . . . . . . . . . . 12 (𝑞 ∈ (𝑇𝑅) ↔ (𝑞:ℕ⟶ℕ0 ∧ (𝑞 “ ℕ) ∈ Fin ∧ (𝑞 “ ℕ) ⊆ 𝐽))
90 df-3an 1100 . . . . . . . . . . . 12 ((𝑞:ℕ⟶ℕ0 ∧ (𝑞 “ ℕ) ∈ Fin ∧ (𝑞 “ ℕ) ⊆ 𝐽) ↔ ((𝑞:ℕ⟶ℕ0 ∧ (𝑞 “ ℕ) ∈ Fin) ∧ (𝑞 “ ℕ) ⊆ 𝐽))
91 cnvimass 5636 . . . . . . . . . . . . . . . . . 18 (𝑞 “ ℕ) ⊆ dom 𝑞
92 fdm 6204 . . . . . . . . . . . . . . . . . 18 (𝑞:ℕ⟶ℕ0 → dom 𝑞 = ℕ)
9391, 92syl5sseq 3809 . . . . . . . . . . . . . . . . 17 (𝑞:ℕ⟶ℕ0 → (𝑞 “ ℕ) ⊆ ℕ)
94 dfss3 3747 . . . . . . . . . . . . . . . . 17 ((𝑞 “ ℕ) ⊆ ℕ ↔ ∀𝑛 ∈ (𝑞 “ ℕ)𝑛 ∈ ℕ)
9593, 94sylib 209 . . . . . . . . . . . . . . . 16 (𝑞:ℕ⟶ℕ0 → ∀𝑛 ∈ (𝑞 “ ℕ)𝑛 ∈ ℕ)
9695biantrurd 523 . . . . . . . . . . . . . . 15 (𝑞:ℕ⟶ℕ0 → (∀𝑛 ∈ (𝑞 “ ℕ) ¬ 2 ∥ 𝑛 ↔ (∀𝑛 ∈ (𝑞 “ ℕ)𝑛 ∈ ℕ ∧ ∀𝑛 ∈ (𝑞 “ ℕ) ¬ 2 ∥ 𝑛)))
97 dfss3 3747 . . . . . . . . . . . . . . . 16 ((𝑞 “ ℕ) ⊆ 𝐽 ↔ ∀𝑛 ∈ (𝑞 “ ℕ)𝑛𝐽)
98 breq2 4801 . . . . . . . . . . . . . . . . . . 19 (𝑧 = 𝑛 → (2 ∥ 𝑧 ↔ 2 ∥ 𝑛))
9998notbid 308 . . . . . . . . . . . . . . . . . 18 (𝑧 = 𝑛 → (¬ 2 ∥ 𝑧 ↔ ¬ 2 ∥ 𝑛))
10099, 16elrab2 3524 . . . . . . . . . . . . . . . . 17 (𝑛𝐽 ↔ (𝑛 ∈ ℕ ∧ ¬ 2 ∥ 𝑛))
101100ralbii 3132 . . . . . . . . . . . . . . . 16 (∀𝑛 ∈ (𝑞 “ ℕ)𝑛𝐽 ↔ ∀𝑛 ∈ (𝑞 “ ℕ)(𝑛 ∈ ℕ ∧ ¬ 2 ∥ 𝑛))
102 r19.26 3216 . . . . . . . . . . . . . . . 16 (∀𝑛 ∈ (𝑞 “ ℕ)(𝑛 ∈ ℕ ∧ ¬ 2 ∥ 𝑛) ↔ (∀𝑛 ∈ (𝑞 “ ℕ)𝑛 ∈ ℕ ∧ ∀𝑛 ∈ (𝑞 “ ℕ) ¬ 2 ∥ 𝑛))
10397, 101, 1023bitri 287 . . . . . . . . . . . . . . 15 ((𝑞 “ ℕ) ⊆ 𝐽 ↔ (∀𝑛 ∈ (𝑞 “ ℕ)𝑛 ∈ ℕ ∧ ∀𝑛 ∈ (𝑞 “ ℕ) ¬ 2 ∥ 𝑛))
10496, 103syl6rbbr 280 . . . . . . . . . . . . . 14 (𝑞:ℕ⟶ℕ0 → ((𝑞 “ ℕ) ⊆ 𝐽 ↔ ∀𝑛 ∈ (𝑞 “ ℕ) ¬ 2 ∥ 𝑛))
105104adantr 467 . . . . . . . . . . . . 13 ((𝑞:ℕ⟶ℕ0 ∧ (𝑞 “ ℕ) ∈ Fin) → ((𝑞 “ ℕ) ⊆ 𝐽 ↔ ∀𝑛 ∈ (𝑞 “ ℕ) ¬ 2 ∥ 𝑛))
106105pm5.32i 565 . . . . . . . . . . . 12 (((𝑞:ℕ⟶ℕ0 ∧ (𝑞 “ ℕ) ∈ Fin) ∧ (𝑞 “ ℕ) ⊆ 𝐽) ↔ ((𝑞:ℕ⟶ℕ0 ∧ (𝑞 “ ℕ) ∈ Fin) ∧ ∀𝑛 ∈ (𝑞 “ ℕ) ¬ 2 ∥ 𝑛))
10789, 90, 1063bitri 287 . . . . . . . . . . 11 (𝑞 ∈ (𝑇𝑅) ↔ ((𝑞:ℕ⟶ℕ0 ∧ (𝑞 “ ℕ) ∈ Fin) ∧ ∀𝑛 ∈ (𝑞 “ ℕ) ¬ 2 ∥ 𝑛))
108107anbi1i 611 . . . . . . . . . 10 ((𝑞 ∈ (𝑇𝑅) ∧ Σ𝑘 ∈ ℕ ((𝑞𝑘) · 𝑘) = 𝑁) ↔ (((𝑞:ℕ⟶ℕ0 ∧ (𝑞 “ ℕ) ∈ Fin) ∧ ∀𝑛 ∈ (𝑞 “ ℕ) ¬ 2 ∥ 𝑛) ∧ Σ𝑘 ∈ ℕ ((𝑞𝑘) · 𝑘) = 𝑁))
10984, 108bitr4i 268 . . . . . . . . 9 ((𝑞𝑃 ∧ ∀𝑛 ∈ (𝑞 “ ℕ) ¬ 2 ∥ 𝑛) ↔ (𝑞 ∈ (𝑇𝑅) ∧ Σ𝑘 ∈ ℕ ((𝑞𝑘) · 𝑘) = 𝑁))
110 rabid 3268 . . . . . . . . 9 (𝑞 ∈ {𝑞𝑃 ∣ ∀𝑛 ∈ (𝑞 “ ℕ) ¬ 2 ∥ 𝑛} ↔ (𝑞𝑃 ∧ ∀𝑛 ∈ (𝑞 “ ℕ) ¬ 2 ∥ 𝑛))
111 rabid 3268 . . . . . . . . 9 (𝑞 ∈ {𝑞 ∈ (𝑇𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑞𝑘) · 𝑘) = 𝑁} ↔ (𝑞 ∈ (𝑇𝑅) ∧ Σ𝑘 ∈ ℕ ((𝑞𝑘) · 𝑘) = 𝑁))
112109, 110, 1113bitr4i 293 . . . . . . . 8 (𝑞 ∈ {𝑞𝑃 ∣ ∀𝑛 ∈ (𝑞 “ ℕ) ¬ 2 ∥ 𝑛} ↔ 𝑞 ∈ {𝑞 ∈ (𝑇𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑞𝑘) · 𝑘) = 𝑁})
11377, 78, 112eqri 29672 . . . . . . 7 {𝑞𝑃 ∣ ∀𝑛 ∈ (𝑞 “ ℕ) ¬ 2 ∥ 𝑛} = {𝑞 ∈ (𝑇𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑞𝑘) · 𝑘) = 𝑁}
11414, 76, 1133eqtri 2800 . . . . . 6 𝑂 = {𝑞 ∈ (𝑇𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑞𝑘) · 𝑘) = 𝑁}
115114reseq2i 5543 . . . . 5 (𝐺𝑂) = (𝐺 ↾ {𝑞 ∈ (𝑇𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑞𝑘) · 𝑘) = 𝑁})
116115a1i 11 . . . 4 (⊤ → (𝐺𝑂) = (𝐺 ↾ {𝑞 ∈ (𝑇𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑞𝑘) · 𝑘) = 𝑁}))
117114a1i 11 . . . 4 (⊤ → 𝑂 = {𝑞 ∈ (𝑇𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑞𝑘) · 𝑘) = 𝑁})
118 nfcv 2916 . . . . . 6 𝑑𝐷
119 nfrab1 3275 . . . . . 6 𝑑{𝑑 ∈ (({0, 1} ↑𝑚 ℕ) ∩ 𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑑𝑘) · 𝑘) = 𝑁}
120 fnima 6161 . . . . . . . . . . . . . . . . 17 (𝑑 Fn ℕ → (𝑑 “ ℕ) = ran 𝑑)
121120sseq1d 3788 . . . . . . . . . . . . . . . 16 (𝑑 Fn ℕ → ((𝑑 “ ℕ) ⊆ {0, 1} ↔ ran 𝑑 ⊆ {0, 1}))
122121anbi2d 615 . . . . . . . . . . . . . . 15 (𝑑 Fn ℕ → ((ran 𝑑 ⊆ ℕ0 ∧ (𝑑 “ ℕ) ⊆ {0, 1}) ↔ (ran 𝑑 ⊆ ℕ0 ∧ ran 𝑑 ⊆ {0, 1})))
123 sstr 3766 . . . . . . . . . . . . . . . . 17 ((ran 𝑑 ⊆ {0, 1} ∧ {0, 1} ⊆ ℕ0) → ran 𝑑 ⊆ ℕ0)
12449, 123mpan2 672 . . . . . . . . . . . . . . . 16 (ran 𝑑 ⊆ {0, 1} → ran 𝑑 ⊆ ℕ0)
125124pm4.71ri 551 . . . . . . . . . . . . . . 15 (ran 𝑑 ⊆ {0, 1} ↔ (ran 𝑑 ⊆ ℕ0 ∧ ran 𝑑 ⊆ {0, 1}))
126122, 125syl6bbr 279 . . . . . . . . . . . . . 14 (𝑑 Fn ℕ → ((ran 𝑑 ⊆ ℕ0 ∧ (𝑑 “ ℕ) ⊆ {0, 1}) ↔ ran 𝑑 ⊆ {0, 1}))
127126pm5.32i 565 . . . . . . . . . . . . 13 ((𝑑 Fn ℕ ∧ (ran 𝑑 ⊆ ℕ0 ∧ (𝑑 “ ℕ) ⊆ {0, 1})) ↔ (𝑑 Fn ℕ ∧ ran 𝑑 ⊆ {0, 1}))
128 anass 455 . . . . . . . . . . . . 13 (((𝑑 Fn ℕ ∧ ran 𝑑 ⊆ ℕ0) ∧ (𝑑 “ ℕ) ⊆ {0, 1}) ↔ (𝑑 Fn ℕ ∧ (ran 𝑑 ⊆ ℕ0 ∧ (𝑑 “ ℕ) ⊆ {0, 1})))
129 df-f 6046 . . . . . . . . . . . . 13 (𝑑:ℕ⟶{0, 1} ↔ (𝑑 Fn ℕ ∧ ran 𝑑 ⊆ {0, 1}))
130127, 128, 1293bitr4ri 294 . . . . . . . . . . . 12 (𝑑:ℕ⟶{0, 1} ↔ ((𝑑 Fn ℕ ∧ ran 𝑑 ⊆ ℕ0) ∧ (𝑑 “ ℕ) ⊆ {0, 1}))
131 prex 5051 . . . . . . . . . . . . 13 {0, 1} ∈ V
132131, 86elmap 8059 . . . . . . . . . . . 12 (𝑑 ∈ ({0, 1} ↑𝑚 ℕ) ↔ 𝑑:ℕ⟶{0, 1})
133 df-f 6046 . . . . . . . . . . . . 13 (𝑑:ℕ⟶ℕ0 ↔ (𝑑 Fn ℕ ∧ ran 𝑑 ⊆ ℕ0))
134133anbi1i 611 . . . . . . . . . . . 12 ((𝑑:ℕ⟶ℕ0 ∧ (𝑑 “ ℕ) ⊆ {0, 1}) ↔ ((𝑑 Fn ℕ ∧ ran 𝑑 ⊆ ℕ0) ∧ (𝑑 “ ℕ) ⊆ {0, 1}))
135130, 132, 1343bitr4i 293 . . . . . . . . . . 11 (𝑑 ∈ ({0, 1} ↑𝑚 ℕ) ↔ (𝑑:ℕ⟶ℕ0 ∧ (𝑑 “ ℕ) ⊆ {0, 1}))
136 vex 3358 . . . . . . . . . . . 12 𝑑 ∈ V
137 cnveq 5446 . . . . . . . . . . . . . 14 (𝑓 = 𝑑𝑓 = 𝑑)
138137imaeq1d 5616 . . . . . . . . . . . . 13 (𝑓 = 𝑑 → (𝑓 “ ℕ) = (𝑑 “ ℕ))
139138eleq1d 2838 . . . . . . . . . . . 12 (𝑓 = 𝑑 → ((𝑓 “ ℕ) ∈ Fin ↔ (𝑑 “ ℕ) ∈ Fin))
140136, 139, 20elab2 3511 . . . . . . . . . . 11 (𝑑𝑅 ↔ (𝑑 “ ℕ) ∈ Fin)
141135, 140anbi12i 613 . . . . . . . . . 10 ((𝑑 ∈ ({0, 1} ↑𝑚 ℕ) ∧ 𝑑𝑅) ↔ ((𝑑:ℕ⟶ℕ0 ∧ (𝑑 “ ℕ) ⊆ {0, 1}) ∧ (𝑑 “ ℕ) ∈ Fin))
142 elin 3954 . . . . . . . . . 10 (𝑑 ∈ (({0, 1} ↑𝑚 ℕ) ∩ 𝑅) ↔ (𝑑 ∈ ({0, 1} ↑𝑚 ℕ) ∧ 𝑑𝑅))
143 an32 626 . . . . . . . . . 10 (((𝑑:ℕ⟶ℕ0 ∧ (𝑑 “ ℕ) ∈ Fin) ∧ (𝑑 “ ℕ) ⊆ {0, 1}) ↔ ((𝑑:ℕ⟶ℕ0 ∧ (𝑑 “ ℕ) ⊆ {0, 1}) ∧ (𝑑 “ ℕ) ∈ Fin))
144141, 142, 1433bitr4i 293 . . . . . . . . 9 (𝑑 ∈ (({0, 1} ↑𝑚 ℕ) ∩ 𝑅) ↔ ((𝑑:ℕ⟶ℕ0 ∧ (𝑑 “ ℕ) ∈ Fin) ∧ (𝑑 “ ℕ) ⊆ {0, 1}))
145144anbi1i 611 . . . . . . . 8 ((𝑑 ∈ (({0, 1} ↑𝑚 ℕ) ∩ 𝑅) ∧ Σ𝑘 ∈ ℕ ((𝑑𝑘) · 𝑘) = 𝑁) ↔ (((𝑑:ℕ⟶ℕ0 ∧ (𝑑 “ ℕ) ∈ Fin) ∧ (𝑑 “ ℕ) ⊆ {0, 1}) ∧ Σ𝑘 ∈ ℕ ((𝑑𝑘) · 𝑘) = 𝑁))
14613eulerpartleme 30782 . . . . . . . . . 10 (𝑑𝑃 ↔ (𝑑:ℕ⟶ℕ0 ∧ (𝑑 “ ℕ) ∈ Fin ∧ Σ𝑘 ∈ ℕ ((𝑑𝑘) · 𝑘) = 𝑁))
147146anbi1i 611 . . . . . . . . 9 ((𝑑𝑃 ∧ (𝑑 “ ℕ) ⊆ {0, 1}) ↔ ((𝑑:ℕ⟶ℕ0 ∧ (𝑑 “ ℕ) ∈ Fin ∧ Σ𝑘 ∈ ℕ ((𝑑𝑘) · 𝑘) = 𝑁) ∧ (𝑑 “ ℕ) ⊆ {0, 1}))
148 df-3an 1100 . . . . . . . . . 10 ((𝑑:ℕ⟶ℕ0 ∧ (𝑑 “ ℕ) ∈ Fin ∧ Σ𝑘 ∈ ℕ ((𝑑𝑘) · 𝑘) = 𝑁) ↔ ((𝑑:ℕ⟶ℕ0 ∧ (𝑑 “ ℕ) ∈ Fin) ∧ Σ𝑘 ∈ ℕ ((𝑑𝑘) · 𝑘) = 𝑁))
149148anbi1i 611 . . . . . . . . 9 (((𝑑:ℕ⟶ℕ0 ∧ (𝑑 “ ℕ) ∈ Fin ∧ Σ𝑘 ∈ ℕ ((𝑑𝑘) · 𝑘) = 𝑁) ∧ (𝑑 “ ℕ) ⊆ {0, 1}) ↔ (((𝑑:ℕ⟶ℕ0 ∧ (𝑑 “ ℕ) ∈ Fin) ∧ Σ𝑘 ∈ ℕ ((𝑑𝑘) · 𝑘) = 𝑁) ∧ (𝑑 “ ℕ) ⊆ {0, 1}))
150 an32 626 . . . . . . . . 9 ((((𝑑:ℕ⟶ℕ0 ∧ (𝑑 “ ℕ) ∈ Fin) ∧ Σ𝑘 ∈ ℕ ((𝑑𝑘) · 𝑘) = 𝑁) ∧ (𝑑 “ ℕ) ⊆ {0, 1}) ↔ (((𝑑:ℕ⟶ℕ0 ∧ (𝑑 “ ℕ) ∈ Fin) ∧ (𝑑 “ ℕ) ⊆ {0, 1}) ∧ Σ𝑘 ∈ ℕ ((𝑑𝑘) · 𝑘) = 𝑁))
151147, 149, 1503bitri 287 . . . . . . . 8 ((𝑑𝑃 ∧ (𝑑 “ ℕ) ⊆ {0, 1}) ↔ (((𝑑:ℕ⟶ℕ0 ∧ (𝑑 “ ℕ) ∈ Fin) ∧ (𝑑 “ ℕ) ⊆ {0, 1}) ∧ Σ𝑘 ∈ ℕ ((𝑑𝑘) · 𝑘) = 𝑁))
152145, 151bitr4i 268 . . . . . . 7 ((𝑑 ∈ (({0, 1} ↑𝑚 ℕ) ∩ 𝑅) ∧ Σ𝑘 ∈ ℕ ((𝑑𝑘) · 𝑘) = 𝑁) ↔ (𝑑𝑃 ∧ (𝑑 “ ℕ) ⊆ {0, 1}))
153 rabid 3268 . . . . . . 7 (𝑑 ∈ {𝑑 ∈ (({0, 1} ↑𝑚 ℕ) ∩ 𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑑𝑘) · 𝑘) = 𝑁} ↔ (𝑑 ∈ (({0, 1} ↑𝑚 ℕ) ∩ 𝑅) ∧ Σ𝑘 ∈ ℕ ((𝑑𝑘) · 𝑘) = 𝑁))
15413, 14, 15eulerpartlemd 30785 . . . . . . 7 (𝑑𝐷 ↔ (𝑑𝑃 ∧ (𝑑 “ ℕ) ⊆ {0, 1}))
155152, 153, 1543bitr4ri 294 . . . . . 6 (𝑑𝐷𝑑 ∈ {𝑑 ∈ (({0, 1} ↑𝑚 ℕ) ∩ 𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑑𝑘) · 𝑘) = 𝑁})
156118, 119, 155eqri 29672 . . . . 5 𝐷 = {𝑑 ∈ (({0, 1} ↑𝑚 ℕ) ∩ 𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑑𝑘) · 𝑘) = 𝑁}
157156a1i 11 . . . 4 (⊤ → 𝐷 = {𝑑 ∈ (({0, 1} ↑𝑚 ℕ) ∩ 𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑑𝑘) · 𝑘) = 𝑁})
158116, 117, 157f1oeq123d 6289 . . 3 (⊤ → ((𝐺𝑂):𝑂1-1-onto𝐷 ↔ (𝐺 ↾ {𝑞 ∈ (𝑇𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑞𝑘) · 𝑘) = 𝑁}):{𝑞 ∈ (𝑇𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑞𝑘) · 𝑘) = 𝑁}–1-1-onto→{𝑑 ∈ (({0, 1} ↑𝑚 ℕ) ∩ 𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑑𝑘) · 𝑘) = 𝑁}))
15972, 158mpbird 248 . 2 (⊤ → (𝐺𝑂):𝑂1-1-onto𝐷)
160159trud 1644 1 (𝐺𝑂):𝑂1-1-onto𝐷
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 197  wa 383  w3a 1098   = wceq 1634  wtru 1635  wcel 2148  {cab 2760  wral 3064  {crab 3068  Vcvv 3355  cin 3728  wss 3729  c0 4073  𝒫 cpw 4307  {cpr 4328   class class class wbr 4797  {copab 4859  cmpt 4876  ccnv 5262  dom cdm 5263  ran crn 5264  cres 5265  cima 5266  ccom 5267   Fn wfn 6037  wf 6038  1-1-ontowf1o 6041  cfv 6042  (class class class)co 6812  cmpt2 6814   supp csupp 7467  𝑚 cmap 8030  Fincfn 8130  0cc0 10159  1c1 10160   · cmul 10164  cle 10298  cn 11243  2c2 11293  0cn0 11516  cexp 13089  Σcsu 14646  cdvds 15211  bitscbits 15370  𝟭cind 30429
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1873  ax-4 1888  ax-5 1994  ax-6 2060  ax-7 2096  ax-8 2150  ax-9 2157  ax-10 2177  ax-11 2193  ax-12 2206  ax-13 2411  ax-ext 2754  ax-rep 4917  ax-sep 4928  ax-nul 4936  ax-pow 4988  ax-pr 5048  ax-un 7117  ax-inf2 8723  ax-ac2 9508  ax-cnex 10215  ax-resscn 10216  ax-1cn 10217  ax-icn 10218  ax-addcl 10219  ax-addrcl 10220  ax-mulcl 10221  ax-mulrcl 10222  ax-mulcom 10223  ax-addass 10224  ax-mulass 10225  ax-distr 10226  ax-i2m1 10227  ax-1ne0 10228  ax-1rid 10229  ax-rnegex 10230  ax-rrecex 10231  ax-cnre 10232  ax-pre-lttri 10233  ax-pre-lttrn 10234  ax-pre-ltadd 10235  ax-pre-mulgt0 10236  ax-pre-sup 10237
This theorem depends on definitions:  df-bi 198  df-an 384  df-or 864  df-3or 1099  df-3an 1100  df-tru 1637  df-fal 1640  df-ex 1856  df-nf 1861  df-sb 2053  df-eu 2625  df-mo 2626  df-clab 2761  df-cleq 2767  df-clel 2770  df-nfc 2905  df-ne 2947  df-nel 3050  df-ral 3069  df-rex 3070  df-reu 3071  df-rmo 3072  df-rab 3073  df-v 3357  df-sbc 3594  df-csb 3689  df-dif 3732  df-un 3734  df-in 3736  df-ss 3743  df-pss 3745  df-nul 4074  df-if 4236  df-pw 4309  df-sn 4327  df-pr 4329  df-tp 4331  df-op 4333  df-uni 4586  df-int 4623  df-iun 4667  df-disj 4766  df-br 4798  df-opab 4860  df-mpt 4877  df-tr 4900  df-id 5171  df-eprel 5176  df-po 5184  df-so 5185  df-fr 5222  df-se 5223  df-we 5224  df-xp 5269  df-rel 5270  df-cnv 5271  df-co 5272  df-dm 5273  df-rn 5274  df-res 5275  df-ima 5276  df-pred 5834  df-ord 5880  df-on 5881  df-lim 5882  df-suc 5883  df-iota 6005  df-fun 6044  df-fn 6045  df-f 6046  df-f1 6047  df-fo 6048  df-f1o 6049  df-fv 6050  df-isom 6051  df-riota 6773  df-ov 6815  df-oprab 6816  df-mpt2 6817  df-om 7234  df-1st 7336  df-2nd 7337  df-supp 7468  df-wrecs 7580  df-recs 7642  df-rdg 7680  df-1o 7734  df-2o 7735  df-oadd 7738  df-er 7917  df-map 8032  df-pm 8033  df-en 8131  df-dom 8132  df-sdom 8133  df-fin 8134  df-fsupp 8453  df-sup 8525  df-inf 8526  df-oi 8592  df-card 8986  df-acn 8989  df-ac 9160  df-cda 9213  df-pnf 10299  df-mnf 10300  df-xr 10301  df-ltxr 10302  df-le 10303  df-sub 10491  df-neg 10492  df-div 10908  df-nn 11244  df-2 11302  df-3 11303  df-n0 11517  df-xnn0 11588  df-z 11602  df-uz 11911  df-rp 12053  df-fz 12556  df-fzo 12696  df-fl 12823  df-mod 12899  df-seq 13031  df-exp 13090  df-hash 13344  df-cj 14069  df-re 14070  df-im 14071  df-sqrt 14205  df-abs 14206  df-clim 14449  df-sum 14647  df-dvds 15212  df-bits 15373  df-ind 30430
This theorem is referenced by:  eulerpart  30801
  Copyright terms: Public domain W3C validator