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

Theorem eulerpartgbij 31704
Description: Lemma for eulerpart 31714: The 𝐺 function is a bijection. (Contributed by Thierry Arnoux, 27-Aug-2017.) (Revised by Thierry Arnoux, 1-Sep-2019.)
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 ∘ (𝑜𝐽))))))
Assertion
Ref Expression
eulerpartgbij 𝐺:(𝑇𝑅)–1-1-onto→(({0, 1} ↑m ℕ) ∩ 𝑅)
Distinct variable groups:   𝑓,𝑔,𝑘,𝑛,𝑜,𝑥,𝑦,𝑧   𝑜,𝐹   𝑓,𝑟,𝐽,𝑜,𝑥,𝑦   𝑜,𝑀,𝑟   𝑓,𝑁,𝑔,𝑥   𝑃,𝑔   𝑅,𝑓,𝑜   𝑜,𝐻,𝑟   𝑇,𝑓,𝑜
Allowed substitution hints:   𝐷(𝑥,𝑦,𝑧,𝑓,𝑔,𝑘,𝑛,𝑜,𝑟)   𝑃(𝑥,𝑦,𝑧,𝑓,𝑘,𝑛,𝑜,𝑟)   𝑅(𝑥,𝑦,𝑧,𝑔,𝑘,𝑛,𝑟)   𝑇(𝑥,𝑦,𝑧,𝑔,𝑘,𝑛,𝑟)   𝐹(𝑥,𝑦,𝑧,𝑓,𝑔,𝑘,𝑛,𝑟)   𝐺(𝑥,𝑦,𝑧,𝑓,𝑔,𝑘,𝑛,𝑜,𝑟)   𝐻(𝑥,𝑦,𝑧,𝑓,𝑔,𝑘,𝑛)   𝐽(𝑧,𝑔,𝑘,𝑛)   𝑀(𝑥,𝑦,𝑧,𝑓,𝑔,𝑘,𝑛)   𝑁(𝑦,𝑧,𝑘,𝑛,𝑜,𝑟)   𝑂(𝑥,𝑦,𝑧,𝑓,𝑔,𝑘,𝑛,𝑜,𝑟)

Proof of Theorem eulerpartgbij
Dummy variables 𝑎 𝑚 𝑏 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 nnex 11631 . . . . 5 ℕ ∈ V
2 indf1ofs 31359 . . . . 5 (ℕ ∈ V → ((𝟭‘ℕ) ↾ Fin):(𝒫 ℕ ∩ Fin)–1-1-onto→{𝑓 ∈ ({0, 1} ↑m ℕ) ∣ (𝑓 “ {1}) ∈ Fin})
31, 2ax-mp 5 . . . 4 ((𝟭‘ℕ) ↾ Fin):(𝒫 ℕ ∩ Fin)–1-1-onto→{𝑓 ∈ ({0, 1} ↑m ℕ) ∣ (𝑓 “ {1}) ∈ Fin}
4 incom 4152 . . . . . . 7 (({0, 1} ↑m ℕ) ∩ {𝑓 ∣ (𝑓 “ ℕ) ∈ Fin}) = ({𝑓 ∣ (𝑓 “ ℕ) ∈ Fin} ∩ ({0, 1} ↑m ℕ))
5 eulerpart.r . . . . . . . 8 𝑅 = {𝑓 ∣ (𝑓 “ ℕ) ∈ Fin}
65ineq2i 4160 . . . . . . 7 (({0, 1} ↑m ℕ) ∩ 𝑅) = (({0, 1} ↑m ℕ) ∩ {𝑓 ∣ (𝑓 “ ℕ) ∈ Fin})
7 dfrab2 4253 . . . . . . 7 {𝑓 ∈ ({0, 1} ↑m ℕ) ∣ (𝑓 “ ℕ) ∈ Fin} = ({𝑓 ∣ (𝑓 “ ℕ) ∈ Fin} ∩ ({0, 1} ↑m ℕ))
84, 6, 73eqtr4i 2855 . . . . . 6 (({0, 1} ↑m ℕ) ∩ 𝑅) = {𝑓 ∈ ({0, 1} ↑m ℕ) ∣ (𝑓 “ ℕ) ∈ Fin}
9 elmapfun 8417 . . . . . . . . 9 (𝑓 ∈ ({0, 1} ↑m ℕ) → Fun 𝑓)
10 elmapi 8415 . . . . . . . . . 10 (𝑓 ∈ ({0, 1} ↑m ℕ) → 𝑓:ℕ⟶{0, 1})
1110frnd 6501 . . . . . . . . 9 (𝑓 ∈ ({0, 1} ↑m ℕ) → ran 𝑓 ⊆ {0, 1})
12 fimacnvinrn2 6823 . . . . . . . . . 10 ((Fun 𝑓 ∧ ran 𝑓 ⊆ {0, 1}) → (𝑓 “ ℕ) = (𝑓 “ (ℕ ∩ {0, 1})))
13 df-pr 4542 . . . . . . . . . . . . . 14 {0, 1} = ({0} ∪ {1})
1413ineq2i 4160 . . . . . . . . . . . . 13 (ℕ ∩ {0, 1}) = (ℕ ∩ ({0} ∪ {1}))
15 indi 4224 . . . . . . . . . . . . 13 (ℕ ∩ ({0} ∪ {1})) = ((ℕ ∩ {0}) ∪ (ℕ ∩ {1}))
16 0nnn 11661 . . . . . . . . . . . . . . 15 ¬ 0 ∈ ℕ
17 disjsn 4621 . . . . . . . . . . . . . . 15 ((ℕ ∩ {0}) = ∅ ↔ ¬ 0 ∈ ℕ)
1816, 17mpbir 234 . . . . . . . . . . . . . 14 (ℕ ∩ {0}) = ∅
19 1nn 11636 . . . . . . . . . . . . . . . . 17 1 ∈ ℕ
20 1ex 10626 . . . . . . . . . . . . . . . . . 18 1 ∈ V
2120snss 4692 . . . . . . . . . . . . . . . . 17 (1 ∈ ℕ ↔ {1} ⊆ ℕ)
2219, 21mpbi 233 . . . . . . . . . . . . . . . 16 {1} ⊆ ℕ
23 dfss 3926 . . . . . . . . . . . . . . . 16 ({1} ⊆ ℕ ↔ {1} = ({1} ∩ ℕ))
2422, 23mpbi 233 . . . . . . . . . . . . . . 15 {1} = ({1} ∩ ℕ)
25 incom 4152 . . . . . . . . . . . . . . 15 ({1} ∩ ℕ) = (ℕ ∩ {1})
2624, 25eqtr2i 2846 . . . . . . . . . . . . . 14 (ℕ ∩ {1}) = {1}
2718, 26uneq12i 4112 . . . . . . . . . . . . 13 ((ℕ ∩ {0}) ∪ (ℕ ∩ {1})) = (∅ ∪ {1})
2814, 15, 273eqtri 2849 . . . . . . . . . . . 12 (ℕ ∩ {0, 1}) = (∅ ∪ {1})
29 uncom 4104 . . . . . . . . . . . 12 (∅ ∪ {1}) = ({1} ∪ ∅)
30 un0 4316 . . . . . . . . . . . 12 ({1} ∪ ∅) = {1}
3128, 29, 303eqtri 2849 . . . . . . . . . . 11 (ℕ ∩ {0, 1}) = {1}
3231imaeq2i 5905 . . . . . . . . . 10 (𝑓 “ (ℕ ∩ {0, 1})) = (𝑓 “ {1})
3312, 32syl6eq 2873 . . . . . . . . 9 ((Fun 𝑓 ∧ ran 𝑓 ⊆ {0, 1}) → (𝑓 “ ℕ) = (𝑓 “ {1}))
349, 11, 33syl2anc 587 . . . . . . . 8 (𝑓 ∈ ({0, 1} ↑m ℕ) → (𝑓 “ ℕ) = (𝑓 “ {1}))
3534eleq1d 2898 . . . . . . 7 (𝑓 ∈ ({0, 1} ↑m ℕ) → ((𝑓 “ ℕ) ∈ Fin ↔ (𝑓 “ {1}) ∈ Fin))
3635rabbiia 3447 . . . . . 6 {𝑓 ∈ ({0, 1} ↑m ℕ) ∣ (𝑓 “ ℕ) ∈ Fin} = {𝑓 ∈ ({0, 1} ↑m ℕ) ∣ (𝑓 “ {1}) ∈ Fin}
378, 36eqtr2i 2846 . . . . 5 {𝑓 ∈ ({0, 1} ↑m ℕ) ∣ (𝑓 “ {1}) ∈ Fin} = (({0, 1} ↑m ℕ) ∩ 𝑅)
38 f1oeq3 6588 . . . . 5 ({𝑓 ∈ ({0, 1} ↑m ℕ) ∣ (𝑓 “ {1}) ∈ Fin} = (({0, 1} ↑m ℕ) ∩ 𝑅) → (((𝟭‘ℕ) ↾ Fin):(𝒫 ℕ ∩ Fin)–1-1-onto→{𝑓 ∈ ({0, 1} ↑m ℕ) ∣ (𝑓 “ {1}) ∈ Fin} ↔ ((𝟭‘ℕ) ↾ Fin):(𝒫 ℕ ∩ Fin)–1-1-onto→(({0, 1} ↑m ℕ) ∩ 𝑅)))
3937, 38ax-mp 5 . . . 4 (((𝟭‘ℕ) ↾ Fin):(𝒫 ℕ ∩ Fin)–1-1-onto→{𝑓 ∈ ({0, 1} ↑m ℕ) ∣ (𝑓 “ {1}) ∈ Fin} ↔ ((𝟭‘ℕ) ↾ Fin):(𝒫 ℕ ∩ Fin)–1-1-onto→(({0, 1} ↑m ℕ) ∩ 𝑅))
403, 39mpbi 233 . . 3 ((𝟭‘ℕ) ↾ Fin):(𝒫 ℕ ∩ Fin)–1-1-onto→(({0, 1} ↑m ℕ) ∩ 𝑅)
41 eulerpart.j . . . . . . 7 𝐽 = {𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧}
42 eulerpart.f . . . . . . 7 𝐹 = (𝑥𝐽, 𝑦 ∈ ℕ0 ↦ ((2↑𝑦) · 𝑥))
4341, 42oddpwdc 31686 . . . . . 6 𝐹:(𝐽 × ℕ0)–1-1-onto→ℕ
44 f1opwfi 8816 . . . . . 6 (𝐹:(𝐽 × ℕ0)–1-1-onto→ℕ → (𝑎 ∈ (𝒫 (𝐽 × ℕ0) ∩ Fin) ↦ (𝐹𝑎)):(𝒫 (𝐽 × ℕ0) ∩ Fin)–1-1-onto→(𝒫 ℕ ∩ Fin))
4543, 44ax-mp 5 . . . . 5 (𝑎 ∈ (𝒫 (𝐽 × ℕ0) ∩ Fin) ↦ (𝐹𝑎)):(𝒫 (𝐽 × ℕ0) ∩ Fin)–1-1-onto→(𝒫 ℕ ∩ Fin)
46 eulerpart.p . . . . . . . 8 𝑃 = {𝑓 ∈ (ℕ0m ℕ) ∣ ((𝑓 “ ℕ) ∈ Fin ∧ Σ𝑘 ∈ ℕ ((𝑓𝑘) · 𝑘) = 𝑁)}
47 eulerpart.o . . . . . . . 8 𝑂 = {𝑔𝑃 ∣ ∀𝑛 ∈ (𝑔 “ ℕ) ¬ 2 ∥ 𝑛}
48 eulerpart.d . . . . . . . 8 𝐷 = {𝑔𝑃 ∣ ∀𝑛 ∈ ℕ (𝑔𝑛) ≤ 1}
49 eulerpart.h . . . . . . . 8 𝐻 = {𝑟 ∈ ((𝒫 ℕ0 ∩ Fin) ↑m 𝐽) ∣ (𝑟 supp ∅) ∈ Fin}
50 eulerpart.m . . . . . . . 8 𝑀 = (𝑟𝐻 ↦ {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐽𝑦 ∈ (𝑟𝑥))})
5146, 47, 48, 41, 42, 49, 50eulerpartlem1 31699 . . . . . . 7 𝑀:𝐻1-1-onto→(𝒫 (𝐽 × ℕ0) ∩ Fin)
52 bitsf1o 15783 . . . . . . . . . . . . . 14 (bits ↾ ℕ0):ℕ01-1-onto→(𝒫 ℕ0 ∩ Fin)
5352a1i 11 . . . . . . . . . . . . 13 (⊤ → (bits ↾ ℕ0):ℕ01-1-onto→(𝒫 ℕ0 ∩ Fin))
5441, 1rabex2 5213 . . . . . . . . . . . . . 14 𝐽 ∈ V
5554a1i 11 . . . . . . . . . . . . 13 (⊤ → 𝐽 ∈ V)
56 nn0ex 11891 . . . . . . . . . . . . . 14 0 ∈ V
5756a1i 11 . . . . . . . . . . . . 13 (⊤ → ℕ0 ∈ V)
5856pwex 5258 . . . . . . . . . . . . . . 15 𝒫 ℕ0 ∈ V
5958inex1 5197 . . . . . . . . . . . . . 14 (𝒫 ℕ0 ∩ Fin) ∈ V
6059a1i 11 . . . . . . . . . . . . 13 (⊤ → (𝒫 ℕ0 ∩ Fin) ∈ V)
61 0nn0 11900 . . . . . . . . . . . . . 14 0 ∈ ℕ0
6261a1i 11 . . . . . . . . . . . . 13 (⊤ → 0 ∈ ℕ0)
63 fvres 6671 . . . . . . . . . . . . . . 15 (0 ∈ ℕ0 → ((bits ↾ ℕ0)‘0) = (bits‘0))
6461, 63ax-mp 5 . . . . . . . . . . . . . 14 ((bits ↾ ℕ0)‘0) = (bits‘0)
65 0bits 15777 . . . . . . . . . . . . . 14 (bits‘0) = ∅
6664, 65eqtr2i 2846 . . . . . . . . . . . . 13 ∅ = ((bits ↾ ℕ0)‘0)
67 elmapi 8415 . . . . . . . . . . . . . . . . 17 (𝑓 ∈ (ℕ0m 𝐽) → 𝑓:𝐽⟶ℕ0)
68 frnnn0supp 11941 . . . . . . . . . . . . . . . . 17 ((𝐽 ∈ V ∧ 𝑓:𝐽⟶ℕ0) → (𝑓 supp 0) = (𝑓 “ ℕ))
6954, 67, 68sylancr 590 . . . . . . . . . . . . . . . 16 (𝑓 ∈ (ℕ0m 𝐽) → (𝑓 supp 0) = (𝑓 “ ℕ))
7069eleq1d 2898 . . . . . . . . . . . . . . 15 (𝑓 ∈ (ℕ0m 𝐽) → ((𝑓 supp 0) ∈ Fin ↔ (𝑓 “ ℕ) ∈ Fin))
7170rabbiia 3447 . . . . . . . . . . . . . 14 {𝑓 ∈ (ℕ0m 𝐽) ∣ (𝑓 supp 0) ∈ Fin} = {𝑓 ∈ (ℕ0m 𝐽) ∣ (𝑓 “ ℕ) ∈ Fin}
72 elmapfun 8417 . . . . . . . . . . . . . . . 16 (𝑓 ∈ (ℕ0m 𝐽) → Fun 𝑓)
73 vex 3472 . . . . . . . . . . . . . . . . 17 𝑓 ∈ V
74 funisfsupp 8826 . . . . . . . . . . . . . . . . 17 ((Fun 𝑓𝑓 ∈ V ∧ 0 ∈ ℕ0) → (𝑓 finSupp 0 ↔ (𝑓 supp 0) ∈ Fin))
7573, 61, 74mp3an23 1450 . . . . . . . . . . . . . . . 16 (Fun 𝑓 → (𝑓 finSupp 0 ↔ (𝑓 supp 0) ∈ Fin))
7672, 75syl 17 . . . . . . . . . . . . . . 15 (𝑓 ∈ (ℕ0m 𝐽) → (𝑓 finSupp 0 ↔ (𝑓 supp 0) ∈ Fin))
7776rabbiia 3447 . . . . . . . . . . . . . 14 {𝑓 ∈ (ℕ0m 𝐽) ∣ 𝑓 finSupp 0} = {𝑓 ∈ (ℕ0m 𝐽) ∣ (𝑓 supp 0) ∈ Fin}
78 incom 4152 . . . . . . . . . . . . . . 15 ({𝑓 ∣ (𝑓 “ ℕ) ∈ Fin} ∩ (ℕ0m 𝐽)) = ((ℕ0m 𝐽) ∩ {𝑓 ∣ (𝑓 “ ℕ) ∈ Fin})
79 dfrab2 4253 . . . . . . . . . . . . . . 15 {𝑓 ∈ (ℕ0m 𝐽) ∣ (𝑓 “ ℕ) ∈ Fin} = ({𝑓 ∣ (𝑓 “ ℕ) ∈ Fin} ∩ (ℕ0m 𝐽))
805ineq2i 4160 . . . . . . . . . . . . . . 15 ((ℕ0m 𝐽) ∩ 𝑅) = ((ℕ0m 𝐽) ∩ {𝑓 ∣ (𝑓 “ ℕ) ∈ Fin})
8178, 79, 803eqtr4ri 2856 . . . . . . . . . . . . . 14 ((ℕ0m 𝐽) ∩ 𝑅) = {𝑓 ∈ (ℕ0m 𝐽) ∣ (𝑓 “ ℕ) ∈ Fin}
8271, 77, 813eqtr4ri 2856 . . . . . . . . . . . . 13 ((ℕ0m 𝐽) ∩ 𝑅) = {𝑓 ∈ (ℕ0m 𝐽) ∣ 𝑓 finSupp 0}
83 elmapfun 8417 . . . . . . . . . . . . . . 15 (𝑟 ∈ ((𝒫 ℕ0 ∩ Fin) ↑m 𝐽) → Fun 𝑟)
84 vex 3472 . . . . . . . . . . . . . . . . 17 𝑟 ∈ V
85 0ex 5187 . . . . . . . . . . . . . . . . 17 ∅ ∈ V
86 funisfsupp 8826 . . . . . . . . . . . . . . . . 17 ((Fun 𝑟𝑟 ∈ V ∧ ∅ ∈ V) → (𝑟 finSupp ∅ ↔ (𝑟 supp ∅) ∈ Fin))
8784, 85, 86mp3an23 1450 . . . . . . . . . . . . . . . 16 (Fun 𝑟 → (𝑟 finSupp ∅ ↔ (𝑟 supp ∅) ∈ Fin))
8887bicomd 226 . . . . . . . . . . . . . . 15 (Fun 𝑟 → ((𝑟 supp ∅) ∈ Fin ↔ 𝑟 finSupp ∅))
8983, 88syl 17 . . . . . . . . . . . . . 14 (𝑟 ∈ ((𝒫 ℕ0 ∩ Fin) ↑m 𝐽) → ((𝑟 supp ∅) ∈ Fin ↔ 𝑟 finSupp ∅))
9089rabbiia 3447 . . . . . . . . . . . . 13 {𝑟 ∈ ((𝒫 ℕ0 ∩ Fin) ↑m 𝐽) ∣ (𝑟 supp ∅) ∈ Fin} = {𝑟 ∈ ((𝒫 ℕ0 ∩ Fin) ↑m 𝐽) ∣ 𝑟 finSupp ∅}
9153, 55, 57, 60, 62, 66, 82, 90fcobijfs 30469 . . . . . . . . . . . 12 (⊤ → (𝑓 ∈ ((ℕ0m 𝐽) ∩ 𝑅) ↦ ((bits ↾ ℕ0) ∘ 𝑓)):((ℕ0m 𝐽) ∩ 𝑅)–1-1-onto→{𝑟 ∈ ((𝒫 ℕ0 ∩ Fin) ↑m 𝐽) ∣ (𝑟 supp ∅) ∈ Fin})
92 elinel1 4146 . . . . . . . . . . . . . . . 16 (𝑓 ∈ ((ℕ0m 𝐽) ∩ 𝑅) → 𝑓 ∈ (ℕ0m 𝐽))
93 frn 6500 . . . . . . . . . . . . . . . . 17 (𝑓:𝐽⟶ℕ0 → ran 𝑓 ⊆ ℕ0)
94 cores 6080 . . . . . . . . . . . . . . . . 17 (ran 𝑓 ⊆ ℕ0 → ((bits ↾ ℕ0) ∘ 𝑓) = (bits ∘ 𝑓))
9567, 93, 943syl 18 . . . . . . . . . . . . . . . 16 (𝑓 ∈ (ℕ0m 𝐽) → ((bits ↾ ℕ0) ∘ 𝑓) = (bits ∘ 𝑓))
9692, 95syl 17 . . . . . . . . . . . . . . 15 (𝑓 ∈ ((ℕ0m 𝐽) ∩ 𝑅) → ((bits ↾ ℕ0) ∘ 𝑓) = (bits ∘ 𝑓))
9796mpteq2ia 5133 . . . . . . . . . . . . . 14 (𝑓 ∈ ((ℕ0m 𝐽) ∩ 𝑅) ↦ ((bits ↾ ℕ0) ∘ 𝑓)) = (𝑓 ∈ ((ℕ0m 𝐽) ∩ 𝑅) ↦ (bits ∘ 𝑓))
9897eqcomi 2831 . . . . . . . . . . . . 13 (𝑓 ∈ ((ℕ0m 𝐽) ∩ 𝑅) ↦ (bits ∘ 𝑓)) = (𝑓 ∈ ((ℕ0m 𝐽) ∩ 𝑅) ↦ ((bits ↾ ℕ0) ∘ 𝑓))
99 f1oeq1 6586 . . . . . . . . . . . . 13 ((𝑓 ∈ ((ℕ0m 𝐽) ∩ 𝑅) ↦ (bits ∘ 𝑓)) = (𝑓 ∈ ((ℕ0m 𝐽) ∩ 𝑅) ↦ ((bits ↾ ℕ0) ∘ 𝑓)) → ((𝑓 ∈ ((ℕ0m 𝐽) ∩ 𝑅) ↦ (bits ∘ 𝑓)):((ℕ0m 𝐽) ∩ 𝑅)–1-1-onto→{𝑟 ∈ ((𝒫 ℕ0 ∩ Fin) ↑m 𝐽) ∣ (𝑟 supp ∅) ∈ Fin} ↔ (𝑓 ∈ ((ℕ0m 𝐽) ∩ 𝑅) ↦ ((bits ↾ ℕ0) ∘ 𝑓)):((ℕ0m 𝐽) ∩ 𝑅)–1-1-onto→{𝑟 ∈ ((𝒫 ℕ0 ∩ Fin) ↑m 𝐽) ∣ (𝑟 supp ∅) ∈ Fin}))
10098, 99mp1i 13 . . . . . . . . . . . 12 (⊤ → ((𝑓 ∈ ((ℕ0m 𝐽) ∩ 𝑅) ↦ (bits ∘ 𝑓)):((ℕ0m 𝐽) ∩ 𝑅)–1-1-onto→{𝑟 ∈ ((𝒫 ℕ0 ∩ Fin) ↑m 𝐽) ∣ (𝑟 supp ∅) ∈ Fin} ↔ (𝑓 ∈ ((ℕ0m 𝐽) ∩ 𝑅) ↦ ((bits ↾ ℕ0) ∘ 𝑓)):((ℕ0m 𝐽) ∩ 𝑅)–1-1-onto→{𝑟 ∈ ((𝒫 ℕ0 ∩ Fin) ↑m 𝐽) ∣ (𝑟 supp ∅) ∈ Fin}))
10191, 100mpbird 260 . . . . . . . . . . 11 (⊤ → (𝑓 ∈ ((ℕ0m 𝐽) ∩ 𝑅) ↦ (bits ∘ 𝑓)):((ℕ0m 𝐽) ∩ 𝑅)–1-1-onto→{𝑟 ∈ ((𝒫 ℕ0 ∩ Fin) ↑m 𝐽) ∣ (𝑟 supp ∅) ∈ Fin})
102101mptru 1545 . . . . . . . . . 10 (𝑓 ∈ ((ℕ0m 𝐽) ∩ 𝑅) ↦ (bits ∘ 𝑓)):((ℕ0m 𝐽) ∩ 𝑅)–1-1-onto→{𝑟 ∈ ((𝒫 ℕ0 ∩ Fin) ↑m 𝐽) ∣ (𝑟 supp ∅) ∈ Fin}
103 ssrab2 4031 . . . . . . . . . . . . . . . 16 {𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧} ⊆ ℕ
10441, 103eqsstri 3976 . . . . . . . . . . . . . . 15 𝐽 ⊆ ℕ
1051, 56, 1043pm3.2i 1336 . . . . . . . . . . . . . 14 (ℕ ∈ V ∧ ℕ0 ∈ V ∧ 𝐽 ⊆ ℕ)
106 eulerpart.t . . . . . . . . . . . . . . . 16 𝑇 = {𝑓 ∈ (ℕ0m ℕ) ∣ (𝑓 “ ℕ) ⊆ 𝐽}
107 cnveq 5721 . . . . . . . . . . . . . . . . . . 19 (𝑓 = 𝑜𝑓 = 𝑜)
108 dfn2 11898 . . . . . . . . . . . . . . . . . . . 20 ℕ = (ℕ0 ∖ {0})
109108a1i 11 . . . . . . . . . . . . . . . . . . 19 (𝑓 = 𝑜 → ℕ = (ℕ0 ∖ {0}))
110107, 109imaeq12d 5908 . . . . . . . . . . . . . . . . . 18 (𝑓 = 𝑜 → (𝑓 “ ℕ) = (𝑜 “ (ℕ0 ∖ {0})))
111110sseq1d 3973 . . . . . . . . . . . . . . . . 17 (𝑓 = 𝑜 → ((𝑓 “ ℕ) ⊆ 𝐽 ↔ (𝑜 “ (ℕ0 ∖ {0})) ⊆ 𝐽))
112111cbvrabv 3467 . . . . . . . . . . . . . . . 16 {𝑓 ∈ (ℕ0m ℕ) ∣ (𝑓 “ ℕ) ⊆ 𝐽} = {𝑜 ∈ (ℕ0m ℕ) ∣ (𝑜 “ (ℕ0 ∖ {0})) ⊆ 𝐽}
113106, 112eqtri 2845 . . . . . . . . . . . . . . 15 𝑇 = {𝑜 ∈ (ℕ0m ℕ) ∣ (𝑜 “ (ℕ0 ∖ {0})) ⊆ 𝐽}
114 eqid 2822 . . . . . . . . . . . . . . 15 (𝑜𝑇 ↦ (𝑜𝐽)) = (𝑜𝑇 ↦ (𝑜𝐽))
115113, 114resf1o 30476 . . . . . . . . . . . . . 14 (((ℕ ∈ V ∧ ℕ0 ∈ V ∧ 𝐽 ⊆ ℕ) ∧ 0 ∈ ℕ0) → (𝑜𝑇 ↦ (𝑜𝐽)):𝑇1-1-onto→(ℕ0m 𝐽))
116105, 61, 115mp2an 691 . . . . . . . . . . . . 13 (𝑜𝑇 ↦ (𝑜𝐽)):𝑇1-1-onto→(ℕ0m 𝐽)
117 f1of1 6596 . . . . . . . . . . . . 13 ((𝑜𝑇 ↦ (𝑜𝐽)):𝑇1-1-onto→(ℕ0m 𝐽) → (𝑜𝑇 ↦ (𝑜𝐽)):𝑇1-1→(ℕ0m 𝐽))
118116, 117ax-mp 5 . . . . . . . . . . . 12 (𝑜𝑇 ↦ (𝑜𝐽)):𝑇1-1→(ℕ0m 𝐽)
119 inss1 4179 . . . . . . . . . . . 12 (𝑇𝑅) ⊆ 𝑇
120 f1ores 6611 . . . . . . . . . . . 12 (((𝑜𝑇 ↦ (𝑜𝐽)):𝑇1-1→(ℕ0m 𝐽) ∧ (𝑇𝑅) ⊆ 𝑇) → ((𝑜𝑇 ↦ (𝑜𝐽)) ↾ (𝑇𝑅)):(𝑇𝑅)–1-1-onto→((𝑜𝑇 ↦ (𝑜𝐽)) “ (𝑇𝑅)))
121118, 119, 120mp2an 691 . . . . . . . . . . 11 ((𝑜𝑇 ↦ (𝑜𝐽)) ↾ (𝑇𝑅)):(𝑇𝑅)–1-1-onto→((𝑜𝑇 ↦ (𝑜𝐽)) “ (𝑇𝑅))
122 vex 3472 . . . . . . . . . . . . . . . . . 18 𝑜 ∈ V
123122resex 5877 . . . . . . . . . . . . . . . . 17 (𝑜𝐽) ∈ V
124123, 114fnmpti 6471 . . . . . . . . . . . . . . . 16 (𝑜𝑇 ↦ (𝑜𝐽)) Fn 𝑇
125 fvelimab 6719 . . . . . . . . . . . . . . . 16 (((𝑜𝑇 ↦ (𝑜𝐽)) Fn 𝑇 ∧ (𝑇𝑅) ⊆ 𝑇) → (𝑓 ∈ ((𝑜𝑇 ↦ (𝑜𝐽)) “ (𝑇𝑅)) ↔ ∃𝑚 ∈ (𝑇𝑅)((𝑜𝑇 ↦ (𝑜𝐽))‘𝑚) = 𝑓))
126124, 119, 125mp2an 691 . . . . . . . . . . . . . . 15 (𝑓 ∈ ((𝑜𝑇 ↦ (𝑜𝐽)) “ (𝑇𝑅)) ↔ ∃𝑚 ∈ (𝑇𝑅)((𝑜𝑇 ↦ (𝑜𝐽))‘𝑚) = 𝑓)
127 eqid 2822 . . . . . . . . . . . . . . . . 17 (𝑚 ∈ (𝑇𝑅) ↦ (𝑚𝐽)) = (𝑚 ∈ (𝑇𝑅) ↦ (𝑚𝐽))
128 vex 3472 . . . . . . . . . . . . . . . . . 18 𝑚 ∈ V
129128resex 5877 . . . . . . . . . . . . . . . . 17 (𝑚𝐽) ∈ V
130127, 129elrnmpti 5809 . . . . . . . . . . . . . . . 16 (𝑓 ∈ ran (𝑚 ∈ (𝑇𝑅) ↦ (𝑚𝐽)) ↔ ∃𝑚 ∈ (𝑇𝑅)𝑓 = (𝑚𝐽))
13146, 47, 48, 41, 42, 49, 50, 5, 106eulerpartlemt 31703 . . . . . . . . . . . . . . . . 17 ((ℕ0m 𝐽) ∩ 𝑅) = ran (𝑚 ∈ (𝑇𝑅) ↦ (𝑚𝐽))
132131eleq2i 2905 . . . . . . . . . . . . . . . 16 (𝑓 ∈ ((ℕ0m 𝐽) ∩ 𝑅) ↔ 𝑓 ∈ ran (𝑚 ∈ (𝑇𝑅) ↦ (𝑚𝐽)))
133 elinel1 4146 . . . . . . . . . . . . . . . . . . 19 (𝑚 ∈ (𝑇𝑅) → 𝑚𝑇)
134114fvtresfn 6752 . . . . . . . . . . . . . . . . . . . 20 (𝑚𝑇 → ((𝑜𝑇 ↦ (𝑜𝐽))‘𝑚) = (𝑚𝐽))
135134eqeq1d 2824 . . . . . . . . . . . . . . . . . . 19 (𝑚𝑇 → (((𝑜𝑇 ↦ (𝑜𝐽))‘𝑚) = 𝑓 ↔ (𝑚𝐽) = 𝑓))
136133, 135syl 17 . . . . . . . . . . . . . . . . . 18 (𝑚 ∈ (𝑇𝑅) → (((𝑜𝑇 ↦ (𝑜𝐽))‘𝑚) = 𝑓 ↔ (𝑚𝐽) = 𝑓))
137 eqcom 2829 . . . . . . . . . . . . . . . . . 18 ((𝑚𝐽) = 𝑓𝑓 = (𝑚𝐽))
138136, 137syl6bb 290 . . . . . . . . . . . . . . . . 17 (𝑚 ∈ (𝑇𝑅) → (((𝑜𝑇 ↦ (𝑜𝐽))‘𝑚) = 𝑓𝑓 = (𝑚𝐽)))
139138rexbiia 3234 . . . . . . . . . . . . . . . 16 (∃𝑚 ∈ (𝑇𝑅)((𝑜𝑇 ↦ (𝑜𝐽))‘𝑚) = 𝑓 ↔ ∃𝑚 ∈ (𝑇𝑅)𝑓 = (𝑚𝐽))
140130, 132, 1393bitr4ri 307 . . . . . . . . . . . . . . 15 (∃𝑚 ∈ (𝑇𝑅)((𝑜𝑇 ↦ (𝑜𝐽))‘𝑚) = 𝑓𝑓 ∈ ((ℕ0m 𝐽) ∩ 𝑅))
141126, 140bitri 278 . . . . . . . . . . . . . 14 (𝑓 ∈ ((𝑜𝑇 ↦ (𝑜𝐽)) “ (𝑇𝑅)) ↔ 𝑓 ∈ ((ℕ0m 𝐽) ∩ 𝑅))
142141eqriv 2819 . . . . . . . . . . . . 13 ((𝑜𝑇 ↦ (𝑜𝐽)) “ (𝑇𝑅)) = ((ℕ0m 𝐽) ∩ 𝑅)
143 f1oeq3 6588 . . . . . . . . . . . . 13 (((𝑜𝑇 ↦ (𝑜𝐽)) “ (𝑇𝑅)) = ((ℕ0m 𝐽) ∩ 𝑅) → (((𝑜𝑇 ↦ (𝑜𝐽)) ↾ (𝑇𝑅)):(𝑇𝑅)–1-1-onto→((𝑜𝑇 ↦ (𝑜𝐽)) “ (𝑇𝑅)) ↔ ((𝑜𝑇 ↦ (𝑜𝐽)) ↾ (𝑇𝑅)):(𝑇𝑅)–1-1-onto→((ℕ0m 𝐽) ∩ 𝑅)))
144142, 143ax-mp 5 . . . . . . . . . . . 12 (((𝑜𝑇 ↦ (𝑜𝐽)) ↾ (𝑇𝑅)):(𝑇𝑅)–1-1-onto→((𝑜𝑇 ↦ (𝑜𝐽)) “ (𝑇𝑅)) ↔ ((𝑜𝑇 ↦ (𝑜𝐽)) ↾ (𝑇𝑅)):(𝑇𝑅)–1-1-onto→((ℕ0m 𝐽) ∩ 𝑅))
145 resmpt 5883 . . . . . . . . . . . . 13 ((𝑇𝑅) ⊆ 𝑇 → ((𝑜𝑇 ↦ (𝑜𝐽)) ↾ (𝑇𝑅)) = (𝑜 ∈ (𝑇𝑅) ↦ (𝑜𝐽)))
146 f1oeq1 6586 . . . . . . . . . . . . 13 (((𝑜𝑇 ↦ (𝑜𝐽)) ↾ (𝑇𝑅)) = (𝑜 ∈ (𝑇𝑅) ↦ (𝑜𝐽)) → (((𝑜𝑇 ↦ (𝑜𝐽)) ↾ (𝑇𝑅)):(𝑇𝑅)–1-1-onto→((ℕ0m 𝐽) ∩ 𝑅) ↔ (𝑜 ∈ (𝑇𝑅) ↦ (𝑜𝐽)):(𝑇𝑅)–1-1-onto→((ℕ0m 𝐽) ∩ 𝑅)))
147119, 145, 146mp2b 10 . . . . . . . . . . . 12 (((𝑜𝑇 ↦ (𝑜𝐽)) ↾ (𝑇𝑅)):(𝑇𝑅)–1-1-onto→((ℕ0m 𝐽) ∩ 𝑅) ↔ (𝑜 ∈ (𝑇𝑅) ↦ (𝑜𝐽)):(𝑇𝑅)–1-1-onto→((ℕ0m 𝐽) ∩ 𝑅))
148144, 147bitri 278 . . . . . . . . . . 11 (((𝑜𝑇 ↦ (𝑜𝐽)) ↾ (𝑇𝑅)):(𝑇𝑅)–1-1-onto→((𝑜𝑇 ↦ (𝑜𝐽)) “ (𝑇𝑅)) ↔ (𝑜 ∈ (𝑇𝑅) ↦ (𝑜𝐽)):(𝑇𝑅)–1-1-onto→((ℕ0m 𝐽) ∩ 𝑅))
149121, 148mpbi 233 . . . . . . . . . 10 (𝑜 ∈ (𝑇𝑅) ↦ (𝑜𝐽)):(𝑇𝑅)–1-1-onto→((ℕ0m 𝐽) ∩ 𝑅)
150 f1oco 6619 . . . . . . . . . 10 (((𝑓 ∈ ((ℕ0m 𝐽) ∩ 𝑅) ↦ (bits ∘ 𝑓)):((ℕ0m 𝐽) ∩ 𝑅)–1-1-onto→{𝑟 ∈ ((𝒫 ℕ0 ∩ Fin) ↑m 𝐽) ∣ (𝑟 supp ∅) ∈ Fin} ∧ (𝑜 ∈ (𝑇𝑅) ↦ (𝑜𝐽)):(𝑇𝑅)–1-1-onto→((ℕ0m 𝐽) ∩ 𝑅)) → ((𝑓 ∈ ((ℕ0m 𝐽) ∩ 𝑅) ↦ (bits ∘ 𝑓)) ∘ (𝑜 ∈ (𝑇𝑅) ↦ (𝑜𝐽))):(𝑇𝑅)–1-1-onto→{𝑟 ∈ ((𝒫 ℕ0 ∩ Fin) ↑m 𝐽) ∣ (𝑟 supp ∅) ∈ Fin})
151102, 149, 150mp2an 691 . . . . . . . . 9 ((𝑓 ∈ ((ℕ0m 𝐽) ∩ 𝑅) ↦ (bits ∘ 𝑓)) ∘ (𝑜 ∈ (𝑇𝑅) ↦ (𝑜𝐽))):(𝑇𝑅)–1-1-onto→{𝑟 ∈ ((𝒫 ℕ0 ∩ Fin) ↑m 𝐽) ∣ (𝑟 supp ∅) ∈ Fin}
152 f1of 6597 . . . . . . . . . . . . . 14 ((𝑜 ∈ (𝑇𝑅) ↦ (𝑜𝐽)):(𝑇𝑅)–1-1-onto→((ℕ0m 𝐽) ∩ 𝑅) → (𝑜 ∈ (𝑇𝑅) ↦ (𝑜𝐽)):(𝑇𝑅)⟶((ℕ0m 𝐽) ∩ 𝑅))
153 eqid 2822 . . . . . . . . . . . . . . . 16 (𝑜 ∈ (𝑇𝑅) ↦ (𝑜𝐽)) = (𝑜 ∈ (𝑇𝑅) ↦ (𝑜𝐽))
154153fmpt 6856 . . . . . . . . . . . . . . 15 (∀𝑜 ∈ (𝑇𝑅)(𝑜𝐽) ∈ ((ℕ0m 𝐽) ∩ 𝑅) ↔ (𝑜 ∈ (𝑇𝑅) ↦ (𝑜𝐽)):(𝑇𝑅)⟶((ℕ0m 𝐽) ∩ 𝑅))
155154biimpri 231 . . . . . . . . . . . . . 14 ((𝑜 ∈ (𝑇𝑅) ↦ (𝑜𝐽)):(𝑇𝑅)⟶((ℕ0m 𝐽) ∩ 𝑅) → ∀𝑜 ∈ (𝑇𝑅)(𝑜𝐽) ∈ ((ℕ0m 𝐽) ∩ 𝑅))
156149, 152, 155mp2b 10 . . . . . . . . . . . . 13 𝑜 ∈ (𝑇𝑅)(𝑜𝐽) ∈ ((ℕ0m 𝐽) ∩ 𝑅)
157156a1i 11 . . . . . . . . . . . 12 (⊤ → ∀𝑜 ∈ (𝑇𝑅)(𝑜𝐽) ∈ ((ℕ0m 𝐽) ∩ 𝑅))
158 eqidd 2823 . . . . . . . . . . . 12 (⊤ → (𝑜 ∈ (𝑇𝑅) ↦ (𝑜𝐽)) = (𝑜 ∈ (𝑇𝑅) ↦ (𝑜𝐽)))
159 eqidd 2823 . . . . . . . . . . . 12 (⊤ → (𝑓 ∈ ((ℕ0m 𝐽) ∩ 𝑅) ↦ (bits ∘ 𝑓)) = (𝑓 ∈ ((ℕ0m 𝐽) ∩ 𝑅) ↦ (bits ∘ 𝑓)))
160 coeq2 5706 . . . . . . . . . . . 12 (𝑓 = (𝑜𝐽) → (bits ∘ 𝑓) = (bits ∘ (𝑜𝐽)))
161157, 158, 159, 160fmptcof 6874 . . . . . . . . . . 11 (⊤ → ((𝑓 ∈ ((ℕ0m 𝐽) ∩ 𝑅) ↦ (bits ∘ 𝑓)) ∘ (𝑜 ∈ (𝑇𝑅) ↦ (𝑜𝐽))) = (𝑜 ∈ (𝑇𝑅) ↦ (bits ∘ (𝑜𝐽))))
162161eqcomd 2828 . . . . . . . . . 10 (⊤ → (𝑜 ∈ (𝑇𝑅) ↦ (bits ∘ (𝑜𝐽))) = ((𝑓 ∈ ((ℕ0m 𝐽) ∩ 𝑅) ↦ (bits ∘ 𝑓)) ∘ (𝑜 ∈ (𝑇𝑅) ↦ (𝑜𝐽))))
163 eqidd 2823 . . . . . . . . . 10 (⊤ → (𝑇𝑅) = (𝑇𝑅))
16449a1i 11 . . . . . . . . . 10 (⊤ → 𝐻 = {𝑟 ∈ ((𝒫 ℕ0 ∩ Fin) ↑m 𝐽) ∣ (𝑟 supp ∅) ∈ Fin})
165162, 163, 164f1oeq123d 6592 . . . . . . . . 9 (⊤ → ((𝑜 ∈ (𝑇𝑅) ↦ (bits ∘ (𝑜𝐽))):(𝑇𝑅)–1-1-onto𝐻 ↔ ((𝑓 ∈ ((ℕ0m 𝐽) ∩ 𝑅) ↦ (bits ∘ 𝑓)) ∘ (𝑜 ∈ (𝑇𝑅) ↦ (𝑜𝐽))):(𝑇𝑅)–1-1-onto→{𝑟 ∈ ((𝒫 ℕ0 ∩ Fin) ↑m 𝐽) ∣ (𝑟 supp ∅) ∈ Fin}))
166151, 165mpbiri 261 . . . . . . . 8 (⊤ → (𝑜 ∈ (𝑇𝑅) ↦ (bits ∘ (𝑜𝐽))):(𝑇𝑅)–1-1-onto𝐻)
167166mptru 1545 . . . . . . 7 (𝑜 ∈ (𝑇𝑅) ↦ (bits ∘ (𝑜𝐽))):(𝑇𝑅)–1-1-onto𝐻
168 f1oco 6619 . . . . . . 7 ((𝑀:𝐻1-1-onto→(𝒫 (𝐽 × ℕ0) ∩ Fin) ∧ (𝑜 ∈ (𝑇𝑅) ↦ (bits ∘ (𝑜𝐽))):(𝑇𝑅)–1-1-onto𝐻) → (𝑀 ∘ (𝑜 ∈ (𝑇𝑅) ↦ (bits ∘ (𝑜𝐽)))):(𝑇𝑅)–1-1-onto→(𝒫 (𝐽 × ℕ0) ∩ Fin))
16951, 167, 168mp2an 691 . . . . . 6 (𝑀 ∘ (𝑜 ∈ (𝑇𝑅) ↦ (bits ∘ (𝑜𝐽)))):(𝑇𝑅)–1-1-onto→(𝒫 (𝐽 × ℕ0) ∩ Fin)
170 eqidd 2823 . . . . . . . . . . 11 (⊤ → (𝑜 ∈ (𝑇𝑅) ↦ (bits ∘ (𝑜𝐽))) = (𝑜 ∈ (𝑇𝑅) ↦ (bits ∘ (𝑜𝐽))))
171 bitsf 15765 . . . . . . . . . . . . . 14 bits:ℤ⟶𝒫 ℕ0
172 zex 11978 . . . . . . . . . . . . . 14 ℤ ∈ V
173 fex 6971 . . . . . . . . . . . . . 14 ((bits:ℤ⟶𝒫 ℕ0 ∧ ℤ ∈ V) → bits ∈ V)
174171, 172, 173mp2an 691 . . . . . . . . . . . . 13 bits ∈ V
175174, 123coex 7621 . . . . . . . . . . . 12 (bits ∘ (𝑜𝐽)) ∈ V
176175a1i 11 . . . . . . . . . . 11 ((⊤ ∧ 𝑜 ∈ (𝑇𝑅)) → (bits ∘ (𝑜𝐽)) ∈ V)
177170, 176fvmpt2d 6763 . . . . . . . . . 10 ((⊤ ∧ 𝑜 ∈ (𝑇𝑅)) → ((𝑜 ∈ (𝑇𝑅) ↦ (bits ∘ (𝑜𝐽)))‘𝑜) = (bits ∘ (𝑜𝐽)))
178 f1of 6597 . . . . . . . . . . . 12 ((𝑜 ∈ (𝑇𝑅) ↦ (bits ∘ (𝑜𝐽))):(𝑇𝑅)–1-1-onto𝐻 → (𝑜 ∈ (𝑇𝑅) ↦ (bits ∘ (𝑜𝐽))):(𝑇𝑅)⟶𝐻)
179166, 178syl 17 . . . . . . . . . . 11 (⊤ → (𝑜 ∈ (𝑇𝑅) ↦ (bits ∘ (𝑜𝐽))):(𝑇𝑅)⟶𝐻)
180179ffvelrnda 6833 . . . . . . . . . 10 ((⊤ ∧ 𝑜 ∈ (𝑇𝑅)) → ((𝑜 ∈ (𝑇𝑅) ↦ (bits ∘ (𝑜𝐽)))‘𝑜) ∈ 𝐻)
181177, 180eqeltrrd 2915 . . . . . . . . 9 ((⊤ ∧ 𝑜 ∈ (𝑇𝑅)) → (bits ∘ (𝑜𝐽)) ∈ 𝐻)
182 f1ofn 6598 . . . . . . . . . . . 12 (𝑀:𝐻1-1-onto→(𝒫 (𝐽 × ℕ0) ∩ Fin) → 𝑀 Fn 𝐻)
18351, 182ax-mp 5 . . . . . . . . . . 11 𝑀 Fn 𝐻
184 dffn5 6706 . . . . . . . . . . 11 (𝑀 Fn 𝐻𝑀 = (𝑟𝐻 ↦ (𝑀𝑟)))
185183, 184mpbi 233 . . . . . . . . . 10 𝑀 = (𝑟𝐻 ↦ (𝑀𝑟))
186185a1i 11 . . . . . . . . 9 (⊤ → 𝑀 = (𝑟𝐻 ↦ (𝑀𝑟)))
187 fveq2 6652 . . . . . . . . 9 (𝑟 = (bits ∘ (𝑜𝐽)) → (𝑀𝑟) = (𝑀‘(bits ∘ (𝑜𝐽))))
188181, 170, 186, 187fmptco 6873 . . . . . . . 8 (⊤ → (𝑀 ∘ (𝑜 ∈ (𝑇𝑅) ↦ (bits ∘ (𝑜𝐽)))) = (𝑜 ∈ (𝑇𝑅) ↦ (𝑀‘(bits ∘ (𝑜𝐽)))))
189188mptru 1545 . . . . . . 7 (𝑀 ∘ (𝑜 ∈ (𝑇𝑅) ↦ (bits ∘ (𝑜𝐽)))) = (𝑜 ∈ (𝑇𝑅) ↦ (𝑀‘(bits ∘ (𝑜𝐽))))
190 f1oeq1 6586 . . . . . . 7 ((𝑀 ∘ (𝑜 ∈ (𝑇𝑅) ↦ (bits ∘ (𝑜𝐽)))) = (𝑜 ∈ (𝑇𝑅) ↦ (𝑀‘(bits ∘ (𝑜𝐽)))) → ((𝑀 ∘ (𝑜 ∈ (𝑇𝑅) ↦ (bits ∘ (𝑜𝐽)))):(𝑇𝑅)–1-1-onto→(𝒫 (𝐽 × ℕ0) ∩ Fin) ↔ (𝑜 ∈ (𝑇𝑅) ↦ (𝑀‘(bits ∘ (𝑜𝐽)))):(𝑇𝑅)–1-1-onto→(𝒫 (𝐽 × ℕ0) ∩ Fin)))
191189, 190ax-mp 5 . . . . . 6 ((𝑀 ∘ (𝑜 ∈ (𝑇𝑅) ↦ (bits ∘ (𝑜𝐽)))):(𝑇𝑅)–1-1-onto→(𝒫 (𝐽 × ℕ0) ∩ Fin) ↔ (𝑜 ∈ (𝑇𝑅) ↦ (𝑀‘(bits ∘ (𝑜𝐽)))):(𝑇𝑅)–1-1-onto→(𝒫 (𝐽 × ℕ0) ∩ Fin))
192169, 191mpbi 233 . . . . 5 (𝑜 ∈ (𝑇𝑅) ↦ (𝑀‘(bits ∘ (𝑜𝐽)))):(𝑇𝑅)–1-1-onto→(𝒫 (𝐽 × ℕ0) ∩ Fin)
193 f1oco 6619 . . . . 5 (((𝑎 ∈ (𝒫 (𝐽 × ℕ0) ∩ Fin) ↦ (𝐹𝑎)):(𝒫 (𝐽 × ℕ0) ∩ Fin)–1-1-onto→(𝒫 ℕ ∩ Fin) ∧ (𝑜 ∈ (𝑇𝑅) ↦ (𝑀‘(bits ∘ (𝑜𝐽)))):(𝑇𝑅)–1-1-onto→(𝒫 (𝐽 × ℕ0) ∩ Fin)) → ((𝑎 ∈ (𝒫 (𝐽 × ℕ0) ∩ Fin) ↦ (𝐹𝑎)) ∘ (𝑜 ∈ (𝑇𝑅) ↦ (𝑀‘(bits ∘ (𝑜𝐽))))):(𝑇𝑅)–1-1-onto→(𝒫 ℕ ∩ Fin))
19445, 192, 193mp2an 691 . . . 4 ((𝑎 ∈ (𝒫 (𝐽 × ℕ0) ∩ Fin) ↦ (𝐹𝑎)) ∘ (𝑜 ∈ (𝑇𝑅) ↦ (𝑀‘(bits ∘ (𝑜𝐽))))):(𝑇𝑅)–1-1-onto→(𝒫 ℕ ∩ Fin)
195 simpr 488 . . . . . . . . 9 ((⊤ ∧ 𝑜 ∈ (𝑇𝑅)) → 𝑜 ∈ (𝑇𝑅))
196 fvex 6665 . . . . . . . . 9 (𝑀‘(bits ∘ (𝑜𝐽))) ∈ V
197 eqid 2822 . . . . . . . . . 10 (𝑜 ∈ (𝑇𝑅) ↦ (𝑀‘(bits ∘ (𝑜𝐽)))) = (𝑜 ∈ (𝑇𝑅) ↦ (𝑀‘(bits ∘ (𝑜𝐽))))
198197fvmpt2 6761 . . . . . . . . 9 ((𝑜 ∈ (𝑇𝑅) ∧ (𝑀‘(bits ∘ (𝑜𝐽))) ∈ V) → ((𝑜 ∈ (𝑇𝑅) ↦ (𝑀‘(bits ∘ (𝑜𝐽))))‘𝑜) = (𝑀‘(bits ∘ (𝑜𝐽))))
199195, 196, 198sylancl 589 . . . . . . . 8 ((⊤ ∧ 𝑜 ∈ (𝑇𝑅)) → ((𝑜 ∈ (𝑇𝑅) ↦ (𝑀‘(bits ∘ (𝑜𝐽))))‘𝑜) = (𝑀‘(bits ∘ (𝑜𝐽))))
200 f1of 6597 . . . . . . . . . 10 ((𝑜 ∈ (𝑇𝑅) ↦ (𝑀‘(bits ∘ (𝑜𝐽)))):(𝑇𝑅)–1-1-onto→(𝒫 (𝐽 × ℕ0) ∩ Fin) → (𝑜 ∈ (𝑇𝑅) ↦ (𝑀‘(bits ∘ (𝑜𝐽)))):(𝑇𝑅)⟶(𝒫 (𝐽 × ℕ0) ∩ Fin))
201192, 200mp1i 13 . . . . . . . . 9 (⊤ → (𝑜 ∈ (𝑇𝑅) ↦ (𝑀‘(bits ∘ (𝑜𝐽)))):(𝑇𝑅)⟶(𝒫 (𝐽 × ℕ0) ∩ Fin))
202201ffvelrnda 6833 . . . . . . . 8 ((⊤ ∧ 𝑜 ∈ (𝑇𝑅)) → ((𝑜 ∈ (𝑇𝑅) ↦ (𝑀‘(bits ∘ (𝑜𝐽))))‘𝑜) ∈ (𝒫 (𝐽 × ℕ0) ∩ Fin))
203199, 202eqeltrrd 2915 . . . . . . 7 ((⊤ ∧ 𝑜 ∈ (𝑇𝑅)) → (𝑀‘(bits ∘ (𝑜𝐽))) ∈ (𝒫 (𝐽 × ℕ0) ∩ Fin))
204 eqidd 2823 . . . . . . 7 (⊤ → (𝑜 ∈ (𝑇𝑅) ↦ (𝑀‘(bits ∘ (𝑜𝐽)))) = (𝑜 ∈ (𝑇𝑅) ↦ (𝑀‘(bits ∘ (𝑜𝐽)))))
205 eqidd 2823 . . . . . . 7 (⊤ → (𝑎 ∈ (𝒫 (𝐽 × ℕ0) ∩ Fin) ↦ (𝐹𝑎)) = (𝑎 ∈ (𝒫 (𝐽 × ℕ0) ∩ Fin) ↦ (𝐹𝑎)))
206 imaeq2 5903 . . . . . . 7 (𝑎 = (𝑀‘(bits ∘ (𝑜𝐽))) → (𝐹𝑎) = (𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽)))))
207203, 204, 205, 206fmptco 6873 . . . . . 6 (⊤ → ((𝑎 ∈ (𝒫 (𝐽 × ℕ0) ∩ Fin) ↦ (𝐹𝑎)) ∘ (𝑜 ∈ (𝑇𝑅) ↦ (𝑀‘(bits ∘ (𝑜𝐽))))) = (𝑜 ∈ (𝑇𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽))))))
208207mptru 1545 . . . . 5 ((𝑎 ∈ (𝒫 (𝐽 × ℕ0) ∩ Fin) ↦ (𝐹𝑎)) ∘ (𝑜 ∈ (𝑇𝑅) ↦ (𝑀‘(bits ∘ (𝑜𝐽))))) = (𝑜 ∈ (𝑇𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽)))))
209 f1oeq1 6586 . . . . 5 (((𝑎 ∈ (𝒫 (𝐽 × ℕ0) ∩ Fin) ↦ (𝐹𝑎)) ∘ (𝑜 ∈ (𝑇𝑅) ↦ (𝑀‘(bits ∘ (𝑜𝐽))))) = (𝑜 ∈ (𝑇𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽))))) → (((𝑎 ∈ (𝒫 (𝐽 × ℕ0) ∩ Fin) ↦ (𝐹𝑎)) ∘ (𝑜 ∈ (𝑇𝑅) ↦ (𝑀‘(bits ∘ (𝑜𝐽))))):(𝑇𝑅)–1-1-onto→(𝒫 ℕ ∩ Fin) ↔ (𝑜 ∈ (𝑇𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽))))):(𝑇𝑅)–1-1-onto→(𝒫 ℕ ∩ Fin)))
210208, 209ax-mp 5 . . . 4 (((𝑎 ∈ (𝒫 (𝐽 × ℕ0) ∩ Fin) ↦ (𝐹𝑎)) ∘ (𝑜 ∈ (𝑇𝑅) ↦ (𝑀‘(bits ∘ (𝑜𝐽))))):(𝑇𝑅)–1-1-onto→(𝒫 ℕ ∩ Fin) ↔ (𝑜 ∈ (𝑇𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽))))):(𝑇𝑅)–1-1-onto→(𝒫 ℕ ∩ Fin))
211194, 210mpbi 233 . . 3 (𝑜 ∈ (𝑇𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽))))):(𝑇𝑅)–1-1-onto→(𝒫 ℕ ∩ Fin)
212 f1oco 6619 . . 3 ((((𝟭‘ℕ) ↾ Fin):(𝒫 ℕ ∩ Fin)–1-1-onto→(({0, 1} ↑m ℕ) ∩ 𝑅) ∧ (𝑜 ∈ (𝑇𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽))))):(𝑇𝑅)–1-1-onto→(𝒫 ℕ ∩ Fin)) → (((𝟭‘ℕ) ↾ Fin) ∘ (𝑜 ∈ (𝑇𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽)))))):(𝑇𝑅)–1-1-onto→(({0, 1} ↑m ℕ) ∩ 𝑅))
21340, 211, 212mp2an 691 . 2 (((𝟭‘ℕ) ↾ Fin) ∘ (𝑜 ∈ (𝑇𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽)))))):(𝑇𝑅)–1-1-onto→(({0, 1} ↑m ℕ) ∩ 𝑅)
214 eulerpart.g . . . 4 𝐺 = (𝑜 ∈ (𝑇𝑅) ↦ ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽))))))
21542mpoexg 7761 . . . . . . . . . 10 ((𝐽 ∈ V ∧ ℕ0 ∈ V) → 𝐹 ∈ V)
21654, 56, 215mp2an 691 . . . . . . . . 9 𝐹 ∈ V
217 imaexg 7606 . . . . . . . . 9 (𝐹 ∈ V → (𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽)))) ∈ V)
218216, 217ax-mp 5 . . . . . . . 8 (𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽)))) ∈ V
219 eqid 2822 . . . . . . . . 9 (𝑜 ∈ (𝑇𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽))))) = (𝑜 ∈ (𝑇𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽)))))
220219fvmpt2 6761 . . . . . . . 8 ((𝑜 ∈ (𝑇𝑅) ∧ (𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽)))) ∈ V) → ((𝑜 ∈ (𝑇𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽)))))‘𝑜) = (𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽)))))
221195, 218, 220sylancl 589 . . . . . . 7 ((⊤ ∧ 𝑜 ∈ (𝑇𝑅)) → ((𝑜 ∈ (𝑇𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽)))))‘𝑜) = (𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽)))))
222 f1of 6597 . . . . . . . . 9 ((𝑜 ∈ (𝑇𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽))))):(𝑇𝑅)–1-1-onto→(𝒫 ℕ ∩ Fin) → (𝑜 ∈ (𝑇𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽))))):(𝑇𝑅)⟶(𝒫 ℕ ∩ Fin))
223211, 222mp1i 13 . . . . . . . 8 (⊤ → (𝑜 ∈ (𝑇𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽))))):(𝑇𝑅)⟶(𝒫 ℕ ∩ Fin))
224223ffvelrnda 6833 . . . . . . 7 ((⊤ ∧ 𝑜 ∈ (𝑇𝑅)) → ((𝑜 ∈ (𝑇𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽)))))‘𝑜) ∈ (𝒫 ℕ ∩ Fin))
225221, 224eqeltrrd 2915 . . . . . 6 ((⊤ ∧ 𝑜 ∈ (𝑇𝑅)) → (𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽)))) ∈ (𝒫 ℕ ∩ Fin))
226 eqidd 2823 . . . . . 6 (⊤ → (𝑜 ∈ (𝑇𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽))))) = (𝑜 ∈ (𝑇𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽))))))
227 indf1o 31357 . . . . . . . . . . 11 (ℕ ∈ V → (𝟭‘ℕ):𝒫 ℕ–1-1-onto→({0, 1} ↑m ℕ))
228 f1ofn 6598 . . . . . . . . . . 11 ((𝟭‘ℕ):𝒫 ℕ–1-1-onto→({0, 1} ↑m ℕ) → (𝟭‘ℕ) Fn 𝒫 ℕ)
2291, 227, 228mp2b 10 . . . . . . . . . 10 (𝟭‘ℕ) Fn 𝒫 ℕ
230 dffn5 6706 . . . . . . . . . 10 ((𝟭‘ℕ) Fn 𝒫 ℕ ↔ (𝟭‘ℕ) = (𝑏 ∈ 𝒫 ℕ ↦ ((𝟭‘ℕ)‘𝑏)))
231229, 230mpbi 233 . . . . . . . . 9 (𝟭‘ℕ) = (𝑏 ∈ 𝒫 ℕ ↦ ((𝟭‘ℕ)‘𝑏))
232231reseq1i 5827 . . . . . . . 8 ((𝟭‘ℕ) ↾ Fin) = ((𝑏 ∈ 𝒫 ℕ ↦ ((𝟭‘ℕ)‘𝑏)) ↾ Fin)
233 resmpt3 5884 . . . . . . . 8 ((𝑏 ∈ 𝒫 ℕ ↦ ((𝟭‘ℕ)‘𝑏)) ↾ Fin) = (𝑏 ∈ (𝒫 ℕ ∩ Fin) ↦ ((𝟭‘ℕ)‘𝑏))
234232, 233eqtri 2845 . . . . . . 7 ((𝟭‘ℕ) ↾ Fin) = (𝑏 ∈ (𝒫 ℕ ∩ Fin) ↦ ((𝟭‘ℕ)‘𝑏))
235234a1i 11 . . . . . 6 (⊤ → ((𝟭‘ℕ) ↾ Fin) = (𝑏 ∈ (𝒫 ℕ ∩ Fin) ↦ ((𝟭‘ℕ)‘𝑏)))
236 fveq2 6652 . . . . . 6 (𝑏 = (𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽)))) → ((𝟭‘ℕ)‘𝑏) = ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽))))))
237225, 226, 235, 236fmptco 6873 . . . . 5 (⊤ → (((𝟭‘ℕ) ↾ Fin) ∘ (𝑜 ∈ (𝑇𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽)))))) = (𝑜 ∈ (𝑇𝑅) ↦ ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽)))))))
238237mptru 1545 . . . 4 (((𝟭‘ℕ) ↾ Fin) ∘ (𝑜 ∈ (𝑇𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽)))))) = (𝑜 ∈ (𝑇𝑅) ↦ ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽))))))
239214, 238eqtr4i 2848 . . 3 𝐺 = (((𝟭‘ℕ) ↾ Fin) ∘ (𝑜 ∈ (𝑇𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽))))))
240 f1oeq1 6586 . . 3 (𝐺 = (((𝟭‘ℕ) ↾ Fin) ∘ (𝑜 ∈ (𝑇𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽)))))) → (𝐺:(𝑇𝑅)–1-1-onto→(({0, 1} ↑m ℕ) ∩ 𝑅) ↔ (((𝟭‘ℕ) ↾ Fin) ∘ (𝑜 ∈ (𝑇𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽)))))):(𝑇𝑅)–1-1-onto→(({0, 1} ↑m ℕ) ∩ 𝑅)))
241239, 240ax-mp 5 . 2 (𝐺:(𝑇𝑅)–1-1-onto→(({0, 1} ↑m ℕ) ∩ 𝑅) ↔ (((𝟭‘ℕ) ↾ Fin) ∘ (𝑜 ∈ (𝑇𝑅) ↦ (𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽)))))):(𝑇𝑅)–1-1-onto→(({0, 1} ↑m ℕ) ∩ 𝑅))
242213, 241mpbir 234 1 𝐺:(𝑇𝑅)–1-1-onto→(({0, 1} ↑m ℕ) ∩ 𝑅)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 209  wa 399  w3a 1084   = wceq 1538  wtru 1539  wcel 2114  {cab 2800  wral 3130  wrex 3131  {crab 3134  Vcvv 3469  cdif 3905  cun 3906  cin 3907  wss 3908  c0 4265  𝒫 cpw 4511  {csn 4539  {cpr 4541   class class class wbr 5042  {copab 5104  cmpt 5122   × cxp 5530  ccnv 5531  ran crn 5533  cres 5534  cima 5535  ccom 5536  Fun wfun 6328   Fn wfn 6329  wf 6330  1-1wf1 6331  1-1-ontowf1o 6333  cfv 6334  (class class class)co 7140  cmpo 7142   supp csupp 7817  m cmap 8393  Fincfn 8496   finSupp cfsupp 8821  0cc0 10526  1c1 10527   · cmul 10531  cle 10665  cn 11625  2c2 11680  0cn0 11885  cz 11969  cexp 13425  Σcsu 15033  cdvds 15598  bitscbits 15757  𝟭cind 31343
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2178  ax-ext 2794  ax-rep 5166  ax-sep 5179  ax-nul 5186  ax-pow 5243  ax-pr 5307  ax-un 7446  ax-inf2 9092  ax-ac2 9874  ax-cnex 10582  ax-resscn 10583  ax-1cn 10584  ax-icn 10585  ax-addcl 10586  ax-addrcl 10587  ax-mulcl 10588  ax-mulrcl 10589  ax-mulcom 10590  ax-addass 10591  ax-mulass 10592  ax-distr 10593  ax-i2m1 10594  ax-1ne0 10595  ax-1rid 10596  ax-rnegex 10597  ax-rrecex 10598  ax-cnre 10599  ax-pre-lttri 10600  ax-pre-lttrn 10601  ax-pre-ltadd 10602  ax-pre-mulgt0 10603  ax-pre-sup 10604
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2622  df-eu 2653  df-clab 2801  df-cleq 2815  df-clel 2894  df-nfc 2962  df-ne 3012  df-nel 3116  df-ral 3135  df-rex 3136  df-reu 3137  df-rmo 3138  df-rab 3139  df-v 3471  df-sbc 3748  df-csb 3856  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-pss 3927  df-nul 4266  df-if 4440  df-pw 4513  df-sn 4540  df-pr 4542  df-tp 4544  df-op 4546  df-uni 4814  df-int 4852  df-iun 4896  df-disj 5008  df-br 5043  df-opab 5105  df-mpt 5123  df-tr 5149  df-id 5437  df-eprel 5442  df-po 5451  df-so 5452  df-fr 5491  df-se 5492  df-we 5493  df-xp 5538  df-rel 5539  df-cnv 5540  df-co 5541  df-dm 5542  df-rn 5543  df-res 5544  df-ima 5545  df-pred 6126  df-ord 6172  df-on 6173  df-lim 6174  df-suc 6175  df-iota 6293  df-fun 6336  df-fn 6337  df-f 6338  df-f1 6339  df-fo 6340  df-f1o 6341  df-fv 6342  df-isom 6343  df-riota 7098  df-ov 7143  df-oprab 7144  df-mpo 7145  df-om 7566  df-1st 7675  df-2nd 7676  df-supp 7818  df-wrecs 7934  df-recs 7995  df-rdg 8033  df-1o 8089  df-2o 8090  df-oadd 8093  df-er 8276  df-map 8395  df-pm 8396  df-en 8497  df-dom 8498  df-sdom 8499  df-fin 8500  df-fsupp 8822  df-sup 8894  df-inf 8895  df-oi 8962  df-dju 9318  df-card 9356  df-acn 9359  df-ac 9531  df-pnf 10666  df-mnf 10667  df-xr 10668  df-ltxr 10669  df-le 10670  df-sub 10861  df-neg 10862  df-div 11287  df-nn 11626  df-2 11688  df-3 11689  df-n0 11886  df-xnn0 11956  df-z 11970  df-uz 12232  df-rp 12378  df-fz 12886  df-fzo 13029  df-fl 13157  df-mod 13233  df-seq 13365  df-exp 13426  df-hash 13687  df-cj 14449  df-re 14450  df-im 14451  df-sqrt 14585  df-abs 14586  df-clim 14836  df-sum 15034  df-dvds 15599  df-bits 15760  df-ind 31344
This theorem is referenced by:  eulerpartlemgf  31711  eulerpartlemgs2  31712  eulerpartlemn  31713
  Copyright terms: Public domain W3C validator