| Step | Hyp | Ref
| Expression |
| 1 | | simpl 482 |
. . . . . . . . . . . . 13
⊢ ((𝑜 = 𝑞 ∧ 𝑘 ∈ ℕ) → 𝑜 = 𝑞) |
| 2 | 1 | fveq1d 6908 |
. . . . . . . . . . . 12
⊢ ((𝑜 = 𝑞 ∧ 𝑘 ∈ ℕ) → (𝑜‘𝑘) = (𝑞‘𝑘)) |
| 3 | 2 | oveq1d 7446 |
. . . . . . . . . . 11
⊢ ((𝑜 = 𝑞 ∧ 𝑘 ∈ ℕ) → ((𝑜‘𝑘) · 𝑘) = ((𝑞‘𝑘) · 𝑘)) |
| 4 | 3 | sumeq2dv 15738 |
. . . . . . . . . 10
⊢ (𝑜 = 𝑞 → Σ𝑘 ∈ ℕ ((𝑜‘𝑘) · 𝑘) = Σ𝑘 ∈ ℕ ((𝑞‘𝑘) · 𝑘)) |
| 5 | 4 | eqeq1d 2739 |
. . . . . . . . 9
⊢ (𝑜 = 𝑞 → (Σ𝑘 ∈ ℕ ((𝑜‘𝑘) · 𝑘) = 𝑁 ↔ Σ𝑘 ∈ ℕ ((𝑞‘𝑘) · 𝑘) = 𝑁)) |
| 6 | 5 | cbvrabv 3447 |
. . . . . . . 8
⊢ {𝑜 ∈ (𝑇 ∩ 𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑜‘𝑘) · 𝑘) = 𝑁} = {𝑞 ∈ (𝑇 ∩ 𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑞‘𝑘) · 𝑘) = 𝑁} |
| 7 | 6 | a1i 11 |
. . . . . . 7
⊢ (𝑜 = 𝑞 → {𝑜 ∈ (𝑇 ∩ 𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑜‘𝑘) · 𝑘) = 𝑁} = {𝑞 ∈ (𝑇 ∩ 𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑞‘𝑘) · 𝑘) = 𝑁}) |
| 8 | 7 | reseq2d 5997 |
. . . . . 6
⊢ (𝑜 = 𝑞 → (𝐺 ↾ {𝑜 ∈ (𝑇 ∩ 𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑜‘𝑘) · 𝑘) = 𝑁}) = (𝐺 ↾ {𝑞 ∈ (𝑇 ∩ 𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑞‘𝑘) · 𝑘) = 𝑁})) |
| 9 | | eqidd 2738 |
. . . . . 6
⊢ (𝑜 = 𝑞 → {𝑑 ∈ (({0, 1} ↑m ℕ)
∩ 𝑅) ∣
Σ𝑘 ∈ ℕ
((𝑑‘𝑘) · 𝑘) = 𝑁} = {𝑑 ∈ (({0, 1} ↑m ℕ)
∩ 𝑅) ∣
Σ𝑘 ∈ ℕ
((𝑑‘𝑘) · 𝑘) = 𝑁}) |
| 10 | 8, 7, 9 | f1oeq123d 6842 |
. . . . 5
⊢ (𝑜 = 𝑞 → ((𝐺 ↾ {𝑜 ∈ (𝑇 ∩ 𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑜‘𝑘) · 𝑘) = 𝑁}):{𝑜 ∈ (𝑇 ∩ 𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑜‘𝑘) · 𝑘) = 𝑁}–1-1-onto→{𝑑 ∈ (({0, 1} ↑m ℕ)
∩ 𝑅) ∣
Σ𝑘 ∈ ℕ
((𝑑‘𝑘) · 𝑘) = 𝑁} ↔ (𝐺 ↾ {𝑞 ∈ (𝑇 ∩ 𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑞‘𝑘) · 𝑘) = 𝑁}):{𝑞 ∈ (𝑇 ∩ 𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑞‘𝑘) · 𝑘) = 𝑁}–1-1-onto→{𝑑 ∈ (({0, 1} ↑m ℕ)
∩ 𝑅) ∣
Σ𝑘 ∈ ℕ
((𝑑‘𝑘) · 𝑘) = 𝑁})) |
| 11 | 10 | imbi2d 340 |
. . . 4
⊢ (𝑜 = 𝑞 → ((⊤ → (𝐺 ↾ {𝑜 ∈ (𝑇 ∩ 𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑜‘𝑘) · 𝑘) = 𝑁}):{𝑜 ∈ (𝑇 ∩ 𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑜‘𝑘) · 𝑘) = 𝑁}–1-1-onto→{𝑑 ∈ (({0, 1} ↑m ℕ)
∩ 𝑅) ∣
Σ𝑘 ∈ ℕ
((𝑑‘𝑘) · 𝑘) = 𝑁}) ↔ (⊤ → (𝐺 ↾ {𝑞 ∈ (𝑇 ∩ 𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑞‘𝑘) · 𝑘) = 𝑁}):{𝑞 ∈ (𝑇 ∩ 𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑞‘𝑘) · 𝑘) = 𝑁}–1-1-onto→{𝑑 ∈ (({0, 1} ↑m ℕ)
∩ 𝑅) ∣
Σ𝑘 ∈ ℕ
((𝑑‘𝑘) · 𝑘) = 𝑁}))) |
| 12 | | eulerpart.g |
. . . . 5
⊢ 𝐺 = (𝑜 ∈ (𝑇 ∩ 𝑅) ↦
((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))))) |
| 13 | | eulerpart.p |
. . . . . . 7
⊢ 𝑃 = {𝑓 ∈ (ℕ0
↑m ℕ) ∣ ((◡𝑓 “ ℕ) ∈ 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
⊢ 𝑇 = {𝑓 ∈ (ℕ0
↑m ℕ) ∣ (◡𝑓 “ ℕ) ⊆ 𝐽} |
| 22 | 13, 14, 15, 16, 17, 18, 19, 20, 21, 12 | eulerpartgbij 34374 |
. . . . . 6
⊢ 𝐺:(𝑇 ∩ 𝑅)–1-1-onto→(({0,
1} ↑m ℕ) ∩ 𝑅) |
| 23 | 22 | a1i 11 |
. . . . 5
⊢ (⊤
→ 𝐺:(𝑇 ∩ 𝑅)–1-1-onto→(({0,
1} ↑m ℕ) ∩ 𝑅)) |
| 24 | | fveq2 6906 |
. . . . . . . . . . . . . 14
⊢ (𝑞 = 𝑜 → (𝐺‘𝑞) = (𝐺‘𝑜)) |
| 25 | | reseq1 5991 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑞 = 𝑜 → (𝑞 ↾ 𝐽) = (𝑜 ↾ 𝐽)) |
| 26 | 25 | coeq2d 5873 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑞 = 𝑜 → (bits ∘ (𝑞 ↾ 𝐽)) = (bits ∘ (𝑜 ↾ 𝐽))) |
| 27 | 26 | fveq2d 6910 |
. . . . . . . . . . . . . . . 16
⊢ (𝑞 = 𝑜 → (𝑀‘(bits ∘ (𝑞 ↾ 𝐽))) = (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))) |
| 28 | 27 | imaeq2d 6078 |
. . . . . . . . . . . . . . 15
⊢ (𝑞 = 𝑜 → (𝐹 “ (𝑀‘(bits ∘ (𝑞 ↾ 𝐽)))) = (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))) |
| 29 | 28 | fveq2d 6910 |
. . . . . . . . . . . . . 14
⊢ (𝑞 = 𝑜 →
((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑞 ↾ 𝐽))))) =
((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))))) |
| 30 | 24, 29 | eqeq12d 2753 |
. . . . . . . . . . . . 13
⊢ (𝑞 = 𝑜 → ((𝐺‘𝑞) = ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑞 ↾ 𝐽))))) ↔ (𝐺‘𝑜) = ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))))) |
| 31 | 13, 14, 15, 16, 17, 18, 19, 20, 21, 12 | eulerpartlemgv 34375 |
. . . . . . . . . . . . 13
⊢ (𝑞 ∈ (𝑇 ∩ 𝑅) → (𝐺‘𝑞) = ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑞 ↾ 𝐽)))))) |
| 32 | 30, 31 | vtoclga 3577 |
. . . . . . . . . . . 12
⊢ (𝑜 ∈ (𝑇 ∩ 𝑅) → (𝐺‘𝑜) = ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))))) |
| 33 | 32 | 3ad2ant2 1135 |
. . . . . . . . . . 11
⊢
((⊤ ∧ 𝑜
∈ (𝑇 ∩ 𝑅) ∧ 𝑑 = ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))))) → (𝐺‘𝑜) = ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))))) |
| 34 | | simp3 1139 |
. . . . . . . . . . 11
⊢
((⊤ ∧ 𝑜
∈ (𝑇 ∩ 𝑅) ∧ 𝑑 = ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))))) → 𝑑 = ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))))) |
| 35 | 33, 34 | eqtr4d 2780 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑜
∈ (𝑇 ∩ 𝑅) ∧ 𝑑 = ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))))) → (𝐺‘𝑜) = 𝑑) |
| 36 | 35 | fveq1d 6908 |
. . . . . . . . 9
⊢
((⊤ ∧ 𝑜
∈ (𝑇 ∩ 𝑅) ∧ 𝑑 = ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))))) → ((𝐺‘𝑜)‘𝑘) = (𝑑‘𝑘)) |
| 37 | 36 | oveq1d 7446 |
. . . . . . . 8
⊢
((⊤ ∧ 𝑜
∈ (𝑇 ∩ 𝑅) ∧ 𝑑 = ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))))) → (((𝐺‘𝑜)‘𝑘) · 𝑘) = ((𝑑‘𝑘) · 𝑘)) |
| 38 | 37 | sumeq2sdv 15739 |
. . . . . . 7
⊢
((⊤ ∧ 𝑜
∈ (𝑇 ∩ 𝑅) ∧ 𝑑 = ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))))) → Σ𝑘 ∈ ℕ (((𝐺‘𝑜)‘𝑘) · 𝑘) = Σ𝑘 ∈ ℕ ((𝑑‘𝑘) · 𝑘)) |
| 39 | 24 | fveq2d 6910 |
. . . . . . . . . . 11
⊢ (𝑞 = 𝑜 → (𝑆‘(𝐺‘𝑞)) = (𝑆‘(𝐺‘𝑜))) |
| 40 | | fveq2 6906 |
. . . . . . . . . . 11
⊢ (𝑞 = 𝑜 → (𝑆‘𝑞) = (𝑆‘𝑜)) |
| 41 | 39, 40 | eqeq12d 2753 |
. . . . . . . . . 10
⊢ (𝑞 = 𝑜 → ((𝑆‘(𝐺‘𝑞)) = (𝑆‘𝑞) ↔ (𝑆‘(𝐺‘𝑜)) = (𝑆‘𝑜))) |
| 42 | | eulerpart.s |
. . . . . . . . . . 11
⊢ 𝑆 = (𝑓 ∈ ((ℕ0
↑m ℕ) ∩ 𝑅) ↦ Σ𝑘 ∈ ℕ ((𝑓‘𝑘) · 𝑘)) |
| 43 | 13, 14, 15, 16, 17, 18, 19, 20, 21, 12, 42 | eulerpartlemgs2 34382 |
. . . . . . . . . 10
⊢ (𝑞 ∈ (𝑇 ∩ 𝑅) → (𝑆‘(𝐺‘𝑞)) = (𝑆‘𝑞)) |
| 44 | 41, 43 | vtoclga 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) |
| 49 | 46, 47, 48 | mp2an 692 |
. . . . . . . . . . . . 13
⊢ {0, 1}
⊆ ℕ0 |
| 50 | | mapss 8929 |
. . . . . . . . . . . . 13
⊢
((ℕ0 ∈ V ∧ {0, 1} ⊆ ℕ0)
→ ({0, 1} ↑m ℕ) ⊆ (ℕ0
↑m ℕ)) |
| 51 | 45, 49, 50 | mp2an 692 |
. . . . . . . . . . . 12
⊢ ({0, 1}
↑m ℕ) ⊆ (ℕ0 ↑m
ℕ) |
| 52 | | ssrin 4242 |
. . . . . . . . . . . 12
⊢ (({0, 1}
↑m ℕ) ⊆ (ℕ0 ↑m
ℕ) → (({0, 1} ↑m ℕ) ∩ 𝑅) ⊆ ((ℕ0
↑m ℕ) ∩ 𝑅)) |
| 53 | 51, 52 | ax-mp 5 |
. . . . . . . . . . 11
⊢ (({0, 1}
↑m ℕ) ∩ 𝑅) ⊆ ((ℕ0
↑m ℕ) ∩ 𝑅) |
| 54 | | f1of 6848 |
. . . . . . . . . . . . 13
⊢ (𝐺:(𝑇 ∩ 𝑅)–1-1-onto→(({0,
1} ↑m ℕ) ∩ 𝑅) → 𝐺:(𝑇 ∩ 𝑅)⟶(({0, 1} ↑m
ℕ) ∩ 𝑅)) |
| 55 | 22, 54 | ax-mp 5 |
. . . . . . . . . . . 12
⊢ 𝐺:(𝑇 ∩ 𝑅)⟶(({0, 1} ↑m
ℕ) ∩ 𝑅) |
| 56 | 55 | ffvelcdmi 7103 |
. . . . . . . . . . 11
⊢ (𝑜 ∈ (𝑇 ∩ 𝑅) → (𝐺‘𝑜) ∈ (({0, 1} ↑m ℕ)
∩ 𝑅)) |
| 57 | 53, 56 | sselid 3981 |
. . . . . . . . . 10
⊢ (𝑜 ∈ (𝑇 ∩ 𝑅) → (𝐺‘𝑜) ∈ ((ℕ0
↑m ℕ) ∩ 𝑅)) |
| 58 | 20, 42 | eulerpartlemsv1 34358 |
. . . . . . . . . 10
⊢ ((𝐺‘𝑜) ∈ ((ℕ0
↑m ℕ) ∩ 𝑅) → (𝑆‘(𝐺‘𝑜)) = Σ𝑘 ∈ ℕ (((𝐺‘𝑜)‘𝑘) · 𝑘)) |
| 59 | 57, 58 | syl 17 |
. . . . . . . . 9
⊢ (𝑜 ∈ (𝑇 ∩ 𝑅) → (𝑆‘(𝐺‘𝑜)) = Σ𝑘 ∈ ℕ (((𝐺‘𝑜)‘𝑘) · 𝑘)) |
| 60 | 13, 14, 15, 16, 17, 18, 19, 20, 21 | eulerpartlemt0 34371 |
. . . . . . . . . . . 12
⊢ (𝑜 ∈ (𝑇 ∩ 𝑅) ↔ (𝑜 ∈ (ℕ0
↑m ℕ) ∧ (◡𝑜 “ ℕ) ∈ Fin ∧ (◡𝑜 “ ℕ) ⊆ 𝐽)) |
| 61 | 60 | simp1bi 1146 |
. . . . . . . . . . 11
⊢ (𝑜 ∈ (𝑇 ∩ 𝑅) → 𝑜 ∈ (ℕ0
↑m ℕ)) |
| 62 | | inss2 4238 |
. . . . . . . . . . . 12
⊢ (𝑇 ∩ 𝑅) ⊆ 𝑅 |
| 63 | 62 | sseli 3979 |
. . . . . . . . . . 11
⊢ (𝑜 ∈ (𝑇 ∩ 𝑅) → 𝑜 ∈ 𝑅) |
| 64 | 61, 63 | elind 4200 |
. . . . . . . . . 10
⊢ (𝑜 ∈ (𝑇 ∩ 𝑅) → 𝑜 ∈ ((ℕ0
↑m ℕ) ∩ 𝑅)) |
| 65 | 20, 42 | eulerpartlemsv1 34358 |
. . . . . . . . . 10
⊢ (𝑜 ∈ ((ℕ0
↑m ℕ) ∩ 𝑅) → (𝑆‘𝑜) = Σ𝑘 ∈ ℕ ((𝑜‘𝑘) · 𝑘)) |
| 66 | 64, 65 | syl 17 |
. . . . . . . . 9
⊢ (𝑜 ∈ (𝑇 ∩ 𝑅) → (𝑆‘𝑜) = Σ𝑘 ∈ ℕ ((𝑜‘𝑘) · 𝑘)) |
| 67 | 44, 59, 66 | 3eqtr3d 2785 |
. . . . . . . 8
⊢ (𝑜 ∈ (𝑇 ∩ 𝑅) → Σ𝑘 ∈ ℕ (((𝐺‘𝑜)‘𝑘) · 𝑘) = Σ𝑘 ∈ ℕ ((𝑜‘𝑘) · 𝑘)) |
| 68 | 67 | 3ad2ant2 1135 |
. . . . . . 7
⊢
((⊤ ∧ 𝑜
∈ (𝑇 ∩ 𝑅) ∧ 𝑑 = ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))))) → Σ𝑘 ∈ ℕ (((𝐺‘𝑜)‘𝑘) · 𝑘) = Σ𝑘 ∈ ℕ ((𝑜‘𝑘) · 𝑘)) |
| 69 | 38, 68 | eqtr3d 2779 |
. . . . . 6
⊢
((⊤ ∧ 𝑜
∈ (𝑇 ∩ 𝑅) ∧ 𝑑 = ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))))) → Σ𝑘 ∈ ℕ ((𝑑‘𝑘) · 𝑘) = Σ𝑘 ∈ ℕ ((𝑜‘𝑘) · 𝑘)) |
| 70 | 69 | eqeq1d 2739 |
. . . . 5
⊢
((⊤ ∧ 𝑜
∈ (𝑇 ∩ 𝑅) ∧ 𝑑 = ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))))) → (Σ𝑘 ∈ ℕ ((𝑑‘𝑘) · 𝑘) = 𝑁 ↔ Σ𝑘 ∈ ℕ ((𝑜‘𝑘) · 𝑘) = 𝑁)) |
| 71 | 12, 23, 70 | f1oresrab 7147 |
. . . 4
⊢ (⊤
→ (𝐺 ↾ {𝑜 ∈ (𝑇 ∩ 𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑜‘𝑘) · 𝑘) = 𝑁}):{𝑜 ∈ (𝑇 ∩ 𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑜‘𝑘) · 𝑘) = 𝑁}–1-1-onto→{𝑑 ∈ (({0, 1} ↑m ℕ)
∩ 𝑅) ∣
Σ𝑘 ∈ ℕ
((𝑑‘𝑘) · 𝑘) = 𝑁}) |
| 72 | 11, 71 | chvarvv 1998 |
. . 3
⊢ (⊤
→ (𝐺 ↾ {𝑞 ∈ (𝑇 ∩ 𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑞‘𝑘) · 𝑘) = 𝑁}):{𝑞 ∈ (𝑇 ∩ 𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑞‘𝑘) · 𝑘) = 𝑁}–1-1-onto→{𝑑 ∈ (({0, 1} ↑m ℕ)
∩ 𝑅) ∣
Σ𝑘 ∈ ℕ
((𝑑‘𝑘) · 𝑘) = 𝑁}) |
| 73 | | cnveq 5884 |
. . . . . . . . . 10
⊢ (𝑔 = 𝑞 → ◡𝑔 = ◡𝑞) |
| 74 | 73 | imaeq1d 6077 |
. . . . . . . . 9
⊢ (𝑔 = 𝑞 → (◡𝑔 “ ℕ) = (◡𝑞 “ ℕ)) |
| 75 | 74 | raleqdv 3326 |
. . . . . . . 8
⊢ (𝑔 = 𝑞 → (∀𝑛 ∈ (◡𝑔 “ ℕ) ¬ 2 ∥ 𝑛 ↔ ∀𝑛 ∈ (◡𝑞 “ ℕ) ¬ 2 ∥ 𝑛)) |
| 76 | 75 | cbvrabv 3447 |
. . . . . . 7
⊢ {𝑔 ∈ 𝑃 ∣ ∀𝑛 ∈ (◡𝑔 “ ℕ) ¬ 2 ∥ 𝑛} = {𝑞 ∈ 𝑃 ∣ ∀𝑛 ∈ (◡𝑞 “ ℕ) ¬ 2 ∥ 𝑛} |
| 77 | | nfrab1 3457 |
. . . . . . . 8
⊢
Ⅎ𝑞{𝑞 ∈ 𝑃 ∣ ∀𝑛 ∈ (◡𝑞 “ ℕ) ¬ 2 ∥ 𝑛} |
| 78 | | nfrab1 3457 |
. . . . . . . 8
⊢
Ⅎ𝑞{𝑞 ∈ (𝑇 ∩ 𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑞‘𝑘) · 𝑘) = 𝑁} |
| 79 | | df-3an 1089 |
. . . . . . . . . . . 12
⊢ ((𝑞:ℕ⟶ℕ0 ∧
(◡𝑞 “ ℕ) ∈ Fin ∧
Σ𝑘 ∈ ℕ
((𝑞‘𝑘) · 𝑘) = 𝑁) ↔ ((𝑞:ℕ⟶ℕ0 ∧
(◡𝑞 “ ℕ) ∈ Fin) ∧
Σ𝑘 ∈ ℕ
((𝑞‘𝑘) · 𝑘) = 𝑁)) |
| 80 | 79 | anbi1i 624 |
. . . . . . . . . . 11
⊢ (((𝑞:ℕ⟶ℕ0 ∧
(◡𝑞 “ ℕ) ∈ Fin ∧
Σ𝑘 ∈ ℕ
((𝑞‘𝑘) · 𝑘) = 𝑁) ∧ ∀𝑛 ∈ (◡𝑞 “ ℕ) ¬ 2 ∥ 𝑛) ↔ (((𝑞:ℕ⟶ℕ0 ∧
(◡𝑞 “ ℕ) ∈ Fin) ∧
Σ𝑘 ∈ ℕ
((𝑞‘𝑘) · 𝑘) = 𝑁) ∧ ∀𝑛 ∈ (◡𝑞 “ ℕ) ¬ 2 ∥ 𝑛)) |
| 81 | 13 | eulerpartleme 34365 |
. . . . . . . . . . . 12
⊢ (𝑞 ∈ 𝑃 ↔ (𝑞:ℕ⟶ℕ0 ∧
(◡𝑞 “ ℕ) ∈ Fin ∧
Σ𝑘 ∈ ℕ
((𝑞‘𝑘) · 𝑘) = 𝑁)) |
| 82 | 81 | anbi1i 624 |
. . . . . . . . . . 11
⊢ ((𝑞 ∈ 𝑃 ∧ ∀𝑛 ∈ (◡𝑞 “ ℕ) ¬ 2 ∥ 𝑛) ↔ ((𝑞:ℕ⟶ℕ0 ∧
(◡𝑞 “ ℕ) ∈ Fin ∧
Σ𝑘 ∈ ℕ
((𝑞‘𝑘) · 𝑘) = 𝑁) ∧ ∀𝑛 ∈ (◡𝑞 “ ℕ) ¬ 2 ∥ 𝑛)) |
| 83 | | an32 646 |
. . . . . . . . . . 11
⊢ ((((𝑞:ℕ⟶ℕ0 ∧
(◡𝑞 “ ℕ) ∈ Fin) ∧
∀𝑛 ∈ (◡𝑞 “ ℕ) ¬ 2 ∥ 𝑛) ∧ Σ𝑘 ∈ ℕ ((𝑞‘𝑘) · 𝑘) = 𝑁) ↔ (((𝑞:ℕ⟶ℕ0 ∧
(◡𝑞 “ ℕ) ∈ Fin) ∧
Σ𝑘 ∈ ℕ
((𝑞‘𝑘) · 𝑘) = 𝑁) ∧ ∀𝑛 ∈ (◡𝑞 “ ℕ) ¬ 2 ∥ 𝑛)) |
| 84 | 80, 82, 83 | 3bitr4i 303 |
. . . . . . . . . 10
⊢ ((𝑞 ∈ 𝑃 ∧ ∀𝑛 ∈ (◡𝑞 “ ℕ) ¬ 2 ∥ 𝑛) ↔ (((𝑞:ℕ⟶ℕ0 ∧
(◡𝑞 “ ℕ) ∈ Fin) ∧
∀𝑛 ∈ (◡𝑞 “ ℕ) ¬ 2 ∥ 𝑛) ∧ Σ𝑘 ∈ ℕ ((𝑞‘𝑘) · 𝑘) = 𝑁)) |
| 85 | 13, 14, 15, 16, 17, 18, 19, 20, 21 | eulerpartlemt0 34371 |
. . . . . . . . . . . . 13
⊢ (𝑞 ∈ (𝑇 ∩ 𝑅) ↔ (𝑞 ∈ (ℕ0
↑m ℕ) ∧ (◡𝑞 “ ℕ) ∈ Fin ∧ (◡𝑞 “ ℕ) ⊆ 𝐽)) |
| 86 | | nnex 12272 |
. . . . . . . . . . . . . . 15
⊢ ℕ
∈ V |
| 87 | 45, 86 | elmap 8911 |
. . . . . . . . . . . . . 14
⊢ (𝑞 ∈ (ℕ0
↑m ℕ) ↔ 𝑞:ℕ⟶ℕ0) |
| 88 | 87 | 3anbi1i 1158 |
. . . . . . . . . . . . 13
⊢ ((𝑞 ∈ (ℕ0
↑m ℕ) ∧ (◡𝑞 “ ℕ) ∈ Fin ∧ (◡𝑞 “ ℕ) ⊆ 𝐽) ↔ (𝑞:ℕ⟶ℕ0 ∧
(◡𝑞 “ ℕ) ∈ Fin ∧ (◡𝑞 “ ℕ) ⊆ 𝐽)) |
| 89 | 85, 88 | bitri 275 |
. . . . . . . . . . . 12
⊢ (𝑞 ∈ (𝑇 ∩ 𝑅) ↔ (𝑞:ℕ⟶ℕ0 ∧
(◡𝑞 “ ℕ) ∈ Fin ∧ (◡𝑞 “ ℕ) ⊆ 𝐽)) |
| 90 | | df-3an 1089 |
. . . . . . . . . . . 12
⊢ ((𝑞:ℕ⟶ℕ0 ∧
(◡𝑞 “ ℕ) ∈ Fin ∧ (◡𝑞 “ ℕ) ⊆ 𝐽) ↔ ((𝑞:ℕ⟶ℕ0 ∧
(◡𝑞 “ ℕ) ∈ Fin) ∧ (◡𝑞 “ ℕ) ⊆ 𝐽)) |
| 91 | | dfss3 3972 |
. . . . . . . . . . . . . . . 16
⊢ ((◡𝑞 “ ℕ) ⊆ 𝐽 ↔ ∀𝑛 ∈ (◡𝑞 “ ℕ)𝑛 ∈ 𝐽) |
| 92 | | breq2 5147 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑧 = 𝑛 → (2 ∥ 𝑧 ↔ 2 ∥ 𝑛)) |
| 93 | 92 | notbid 318 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑧 = 𝑛 → (¬ 2 ∥ 𝑧 ↔ ¬ 2 ∥ 𝑛)) |
| 94 | 93, 16 | elrab2 3695 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ 𝐽 ↔ (𝑛 ∈ ℕ ∧ ¬ 2 ∥ 𝑛)) |
| 95 | 94 | ralbii 3093 |
. . . . . . . . . . . . . . . 16
⊢
(∀𝑛 ∈
(◡𝑞 “ ℕ)𝑛 ∈ 𝐽 ↔ ∀𝑛 ∈ (◡𝑞 “ ℕ)(𝑛 ∈ ℕ ∧ ¬ 2 ∥ 𝑛)) |
| 96 | | r19.26 3111 |
. . . . . . . . . . . . . . . 16
⊢
(∀𝑛 ∈
(◡𝑞 “ ℕ)(𝑛 ∈ ℕ ∧ ¬ 2 ∥ 𝑛) ↔ (∀𝑛 ∈ (◡𝑞 “ ℕ)𝑛 ∈ ℕ ∧ ∀𝑛 ∈ (◡𝑞 “ ℕ) ¬ 2 ∥ 𝑛)) |
| 97 | 91, 95, 96 | 3bitri 297 |
. . . . . . . . . . . . . . 15
⊢ ((◡𝑞 “ ℕ) ⊆ 𝐽 ↔ (∀𝑛 ∈ (◡𝑞 “ ℕ)𝑛 ∈ ℕ ∧ ∀𝑛 ∈ (◡𝑞 “ ℕ) ¬ 2 ∥ 𝑛)) |
| 98 | | cnvimass 6100 |
. . . . . . . . . . . . . . . . . 18
⊢ (◡𝑞 “ ℕ) ⊆ dom 𝑞 |
| 99 | | fdm 6745 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑞:ℕ⟶ℕ0 →
dom 𝑞 =
ℕ) |
| 100 | 98, 99 | sseqtrid 4026 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑞:ℕ⟶ℕ0 →
(◡𝑞 “ ℕ) ⊆
ℕ) |
| 101 | | dfss3 3972 |
. . . . . . . . . . . . . . . . 17
⊢ ((◡𝑞 “ ℕ) ⊆ ℕ ↔
∀𝑛 ∈ (◡𝑞 “ ℕ)𝑛 ∈ ℕ) |
| 102 | 100, 101 | sylib 218 |
. . . . . . . . . . . . . . . 16
⊢ (𝑞:ℕ⟶ℕ0 →
∀𝑛 ∈ (◡𝑞 “ ℕ)𝑛 ∈ ℕ) |
| 103 | 102 | biantrurd 532 |
. . . . . . . . . . . . . . 15
⊢ (𝑞:ℕ⟶ℕ0 →
(∀𝑛 ∈ (◡𝑞 “ ℕ) ¬ 2 ∥ 𝑛 ↔ (∀𝑛 ∈ (◡𝑞 “ ℕ)𝑛 ∈ ℕ ∧ ∀𝑛 ∈ (◡𝑞 “ ℕ) ¬ 2 ∥ 𝑛))) |
| 104 | 97, 103 | bitr4id 290 |
. . . . . . . . . . . . . 14
⊢ (𝑞:ℕ⟶ℕ0 →
((◡𝑞 “ ℕ) ⊆ 𝐽 ↔ ∀𝑛 ∈ (◡𝑞 “ ℕ) ¬ 2 ∥ 𝑛)) |
| 105 | 104 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝑞:ℕ⟶ℕ0 ∧
(◡𝑞 “ ℕ) ∈ Fin) → ((◡𝑞 “ ℕ) ⊆ 𝐽 ↔ ∀𝑛 ∈ (◡𝑞 “ ℕ) ¬ 2 ∥ 𝑛)) |
| 106 | 105 | pm5.32i 574 |
. . . . . . . . . . . 12
⊢ (((𝑞:ℕ⟶ℕ0 ∧
(◡𝑞 “ ℕ) ∈ Fin) ∧ (◡𝑞 “ ℕ) ⊆ 𝐽) ↔ ((𝑞:ℕ⟶ℕ0 ∧
(◡𝑞 “ ℕ) ∈ Fin) ∧
∀𝑛 ∈ (◡𝑞 “ ℕ) ¬ 2 ∥ 𝑛)) |
| 107 | 89, 90, 106 | 3bitri 297 |
. . . . . . . . . . 11
⊢ (𝑞 ∈ (𝑇 ∩ 𝑅) ↔ ((𝑞:ℕ⟶ℕ0 ∧
(◡𝑞 “ ℕ) ∈ Fin) ∧
∀𝑛 ∈ (◡𝑞 “ ℕ) ¬ 2 ∥ 𝑛)) |
| 108 | 107 | anbi1i 624 |
. . . . . . . . . 10
⊢ ((𝑞 ∈ (𝑇 ∩ 𝑅) ∧ Σ𝑘 ∈ ℕ ((𝑞‘𝑘) · 𝑘) = 𝑁) ↔ (((𝑞:ℕ⟶ℕ0 ∧
(◡𝑞 “ ℕ) ∈ Fin) ∧
∀𝑛 ∈ (◡𝑞 “ ℕ) ¬ 2 ∥ 𝑛) ∧ Σ𝑘 ∈ ℕ ((𝑞‘𝑘) · 𝑘) = 𝑁)) |
| 109 | 84, 108 | bitr4i 278 |
. . . . . . . . 9
⊢ ((𝑞 ∈ 𝑃 ∧ ∀𝑛 ∈ (◡𝑞 “ ℕ) ¬ 2 ∥ 𝑛) ↔ (𝑞 ∈ (𝑇 ∩ 𝑅) ∧ Σ𝑘 ∈ ℕ ((𝑞‘𝑘) · 𝑘) = 𝑁)) |
| 110 | | rabid 3458 |
. . . . . . . . 9
⊢ (𝑞 ∈ {𝑞 ∈ 𝑃 ∣ ∀𝑛 ∈ (◡𝑞 “ ℕ) ¬ 2 ∥ 𝑛} ↔ (𝑞 ∈ 𝑃 ∧ ∀𝑛 ∈ (◡𝑞 “ ℕ) ¬ 2 ∥ 𝑛)) |
| 111 | | rabid 3458 |
. . . . . . . . 9
⊢ (𝑞 ∈ {𝑞 ∈ (𝑇 ∩ 𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑞‘𝑘) · 𝑘) = 𝑁} ↔ (𝑞 ∈ (𝑇 ∩ 𝑅) ∧ Σ𝑘 ∈ ℕ ((𝑞‘𝑘) · 𝑘) = 𝑁)) |
| 112 | 109, 110,
111 | 3bitr4i 303 |
. . . . . . . 8
⊢ (𝑞 ∈ {𝑞 ∈ 𝑃 ∣ ∀𝑛 ∈ (◡𝑞 “ ℕ) ¬ 2 ∥ 𝑛} ↔ 𝑞 ∈ {𝑞 ∈ (𝑇 ∩ 𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑞‘𝑘) · 𝑘) = 𝑁}) |
| 113 | 77, 78, 112 | eqri 4004 |
. . . . . . 7
⊢ {𝑞 ∈ 𝑃 ∣ ∀𝑛 ∈ (◡𝑞 “ ℕ) ¬ 2 ∥ 𝑛} = {𝑞 ∈ (𝑇 ∩ 𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑞‘𝑘) · 𝑘) = 𝑁} |
| 114 | 14, 76, 113 | 3eqtri 2769 |
. . . . . 6
⊢ 𝑂 = {𝑞 ∈ (𝑇 ∩ 𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑞‘𝑘) · 𝑘) = 𝑁} |
| 115 | 114 | reseq2i 5994 |
. . . . 5
⊢ (𝐺 ↾ 𝑂) = (𝐺 ↾ {𝑞 ∈ (𝑇 ∩ 𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑞‘𝑘) · 𝑘) = 𝑁}) |
| 116 | 115 | a1i 11 |
. . . 4
⊢ (⊤
→ (𝐺 ↾ 𝑂) = (𝐺 ↾ {𝑞 ∈ (𝑇 ∩ 𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑞‘𝑘) · 𝑘) = 𝑁})) |
| 117 | 114 | a1i 11 |
. . . 4
⊢ (⊤
→ 𝑂 = {𝑞 ∈ (𝑇 ∩ 𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑞‘𝑘) · 𝑘) = 𝑁}) |
| 118 | | nfcv 2905 |
. . . . . 6
⊢
Ⅎ𝑑𝐷 |
| 119 | | nfrab1 3457 |
. . . . . 6
⊢
Ⅎ𝑑{𝑑 ∈ (({0, 1} ↑m ℕ)
∩ 𝑅) ∣
Σ𝑘 ∈ ℕ
((𝑑‘𝑘) · 𝑘) = 𝑁} |
| 120 | | fnima 6698 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑑 Fn ℕ → (𝑑 “ ℕ) = ran 𝑑) |
| 121 | 120 | sseq1d 4015 |
. . . . . . . . . . . . . . . 16
⊢ (𝑑 Fn ℕ → ((𝑑 “ ℕ) ⊆ {0, 1}
↔ ran 𝑑 ⊆ {0,
1})) |
| 122 | 121 | anbi2d 630 |
. . . . . . . . . . . . . . 15
⊢ (𝑑 Fn ℕ → ((ran 𝑑 ⊆ ℕ0
∧ (𝑑 “ ℕ)
⊆ {0, 1}) ↔ (ran 𝑑 ⊆ ℕ0 ∧ ran 𝑑 ⊆ {0,
1}))) |
| 123 | | sstr 3992 |
. . . . . . . . . . . . . . . . 17
⊢ ((ran
𝑑 ⊆ {0, 1} ∧ {0,
1} ⊆ ℕ0) → ran 𝑑 ⊆
ℕ0) |
| 124 | 49, 123 | mpan2 691 |
. . . . . . . . . . . . . . . 16
⊢ (ran
𝑑 ⊆ {0, 1} → ran
𝑑 ⊆
ℕ0) |
| 125 | 124 | pm4.71ri 560 |
. . . . . . . . . . . . . . 15
⊢ (ran
𝑑 ⊆ {0, 1} ↔
(ran 𝑑 ⊆
ℕ0 ∧ ran 𝑑 ⊆ {0, 1})) |
| 126 | 122, 125 | bitr4di 289 |
. . . . . . . . . . . . . 14
⊢ (𝑑 Fn ℕ → ((ran 𝑑 ⊆ ℕ0
∧ (𝑑 “ ℕ)
⊆ {0, 1}) ↔ ran 𝑑 ⊆ {0, 1})) |
| 127 | 126 | pm5.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})) |
| 130 | 127, 128,
129 | 3bitr4ri 304 |
. . . . . . . . . . . 12
⊢ (𝑑:ℕ⟶{0, 1} ↔
((𝑑 Fn ℕ ∧ ran
𝑑 ⊆
ℕ0) ∧ (𝑑 “ ℕ) ⊆ {0,
1})) |
| 131 | | prex 5437 |
. . . . . . . . . . . . 13
⊢ {0, 1}
∈ V |
| 132 | 131, 86 | elmap 8911 |
. . . . . . . . . . . 12
⊢ (𝑑 ∈ ({0, 1}
↑m ℕ) ↔ 𝑑:ℕ⟶{0, 1}) |
| 133 | | df-f 6565 |
. . . . . . . . . . . . 13
⊢ (𝑑:ℕ⟶ℕ0 ↔
(𝑑 Fn ℕ ∧ ran
𝑑 ⊆
ℕ0)) |
| 134 | 133 | anbi1i 624 |
. . . . . . . . . . . 12
⊢ ((𝑑:ℕ⟶ℕ0 ∧
(𝑑 “ ℕ) ⊆
{0, 1}) ↔ ((𝑑 Fn
ℕ ∧ ran 𝑑 ⊆
ℕ0) ∧ (𝑑 “ ℕ) ⊆ {0,
1})) |
| 135 | 130, 132,
134 | 3bitr4i 303 |
. . . . . . . . . . 11
⊢ (𝑑 ∈ ({0, 1}
↑m ℕ) ↔ (𝑑:ℕ⟶ℕ0 ∧
(𝑑 “ ℕ) ⊆
{0, 1})) |
| 136 | | vex 3484 |
. . . . . . . . . . . 12
⊢ 𝑑 ∈ V |
| 137 | | cnveq 5884 |
. . . . . . . . . . . . . 14
⊢ (𝑓 = 𝑑 → ◡𝑓 = ◡𝑑) |
| 138 | 137 | imaeq1d 6077 |
. . . . . . . . . . . . 13
⊢ (𝑓 = 𝑑 → (◡𝑓 “ ℕ) = (◡𝑑 “ ℕ)) |
| 139 | 138 | eleq1d 2826 |
. . . . . . . . . . . 12
⊢ (𝑓 = 𝑑 → ((◡𝑓 “ ℕ) ∈ Fin ↔ (◡𝑑 “ ℕ) ∈
Fin)) |
| 140 | 136, 139,
20 | elab2 3682 |
. . . . . . . . . . 11
⊢ (𝑑 ∈ 𝑅 ↔ (◡𝑑 “ ℕ) ∈
Fin) |
| 141 | 135, 140 | anbi12i 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)) |
| 144 | 141, 142,
143 | 3bitr4i 303 |
. . . . . . . . 9
⊢ (𝑑 ∈ (({0, 1}
↑m ℕ) ∩ 𝑅) ↔ ((𝑑:ℕ⟶ℕ0 ∧
(◡𝑑 “ ℕ) ∈ Fin) ∧ (𝑑 “ ℕ) ⊆ {0,
1})) |
| 145 | 144 | anbi1i 624 |
. . . . . . . 8
⊢ ((𝑑 ∈ (({0, 1}
↑m ℕ) ∩ 𝑅) ∧ Σ𝑘 ∈ ℕ ((𝑑‘𝑘) · 𝑘) = 𝑁) ↔ (((𝑑:ℕ⟶ℕ0 ∧
(◡𝑑 “ ℕ) ∈ Fin) ∧ (𝑑 “ ℕ) ⊆ {0,
1}) ∧ Σ𝑘 ∈
ℕ ((𝑑‘𝑘) · 𝑘) = 𝑁)) |
| 146 | 13 | eulerpartleme 34365 |
. . . . . . . . . 10
⊢ (𝑑 ∈ 𝑃 ↔ (𝑑:ℕ⟶ℕ0 ∧
(◡𝑑 “ ℕ) ∈ Fin ∧
Σ𝑘 ∈ ℕ
((𝑑‘𝑘) · 𝑘) = 𝑁)) |
| 147 | 146 | anbi1i 624 |
. . . . . . . . 9
⊢ ((𝑑 ∈ 𝑃 ∧ (𝑑 “ ℕ) ⊆ {0, 1}) ↔
((𝑑:ℕ⟶ℕ0 ∧
(◡𝑑 “ ℕ) ∈ Fin ∧
Σ𝑘 ∈ ℕ
((𝑑‘𝑘) · 𝑘) = 𝑁) ∧ (𝑑 “ ℕ) ⊆ {0,
1})) |
| 148 | | df-3an 1089 |
. . . . . . . . . 10
⊢ ((𝑑:ℕ⟶ℕ0 ∧
(◡𝑑 “ ℕ) ∈ Fin ∧
Σ𝑘 ∈ ℕ
((𝑑‘𝑘) · 𝑘) = 𝑁) ↔ ((𝑑:ℕ⟶ℕ0 ∧
(◡𝑑 “ ℕ) ∈ Fin) ∧
Σ𝑘 ∈ ℕ
((𝑑‘𝑘) · 𝑘) = 𝑁)) |
| 149 | 148 | anbi1i 624 |
. . . . . . . . 9
⊢ (((𝑑:ℕ⟶ℕ0 ∧
(◡𝑑 “ ℕ) ∈ Fin ∧
Σ𝑘 ∈ ℕ
((𝑑‘𝑘) · 𝑘) = 𝑁) ∧ (𝑑 “ ℕ) ⊆ {0, 1}) ↔
(((𝑑:ℕ⟶ℕ0 ∧
(◡𝑑 “ ℕ) ∈ Fin) ∧
Σ𝑘 ∈ ℕ
((𝑑‘𝑘) · 𝑘) = 𝑁) ∧ (𝑑 “ ℕ) ⊆ {0,
1})) |
| 150 | | an32 646 |
. . . . . . . . 9
⊢ ((((𝑑:ℕ⟶ℕ0 ∧
(◡𝑑 “ ℕ) ∈ Fin) ∧
Σ𝑘 ∈ ℕ
((𝑑‘𝑘) · 𝑘) = 𝑁) ∧ (𝑑 “ ℕ) ⊆ {0, 1}) ↔
(((𝑑:ℕ⟶ℕ0 ∧
(◡𝑑 “ ℕ) ∈ Fin) ∧ (𝑑 “ ℕ) ⊆ {0,
1}) ∧ Σ𝑘 ∈
ℕ ((𝑑‘𝑘) · 𝑘) = 𝑁)) |
| 151 | 147, 149,
150 | 3bitri 297 |
. . . . . . . 8
⊢ ((𝑑 ∈ 𝑃 ∧ (𝑑 “ ℕ) ⊆ {0, 1}) ↔
(((𝑑:ℕ⟶ℕ0 ∧
(◡𝑑 “ ℕ) ∈ Fin) ∧ (𝑑 “ ℕ) ⊆ {0,
1}) ∧ Σ𝑘 ∈
ℕ ((𝑑‘𝑘) · 𝑘) = 𝑁)) |
| 152 | 145, 151 | bitr4i 278 |
. . . . . . 7
⊢ ((𝑑 ∈ (({0, 1}
↑m ℕ) ∩ 𝑅) ∧ Σ𝑘 ∈ ℕ ((𝑑‘𝑘) · 𝑘) = 𝑁) ↔ (𝑑 ∈ 𝑃 ∧ (𝑑 “ ℕ) ⊆ {0,
1})) |
| 153 | | rabid 3458 |
. . . . . . 7
⊢ (𝑑 ∈ {𝑑 ∈ (({0, 1} ↑m ℕ)
∩ 𝑅) ∣
Σ𝑘 ∈ ℕ
((𝑑‘𝑘) · 𝑘) = 𝑁} ↔ (𝑑 ∈ (({0, 1} ↑m ℕ)
∩ 𝑅) ∧ Σ𝑘 ∈ ℕ ((𝑑‘𝑘) · 𝑘) = 𝑁)) |
| 154 | 13, 14, 15 | eulerpartlemd 34368 |
. . . . . . 7
⊢ (𝑑 ∈ 𝐷 ↔ (𝑑 ∈ 𝑃 ∧ (𝑑 “ ℕ) ⊆ {0,
1})) |
| 155 | 152, 153,
154 | 3bitr4ri 304 |
. . . . . 6
⊢ (𝑑 ∈ 𝐷 ↔ 𝑑 ∈ {𝑑 ∈ (({0, 1} ↑m ℕ)
∩ 𝑅) ∣
Σ𝑘 ∈ ℕ
((𝑑‘𝑘) · 𝑘) = 𝑁}) |
| 156 | 118, 119,
155 | eqri 4004 |
. . . . 5
⊢ 𝐷 = {𝑑 ∈ (({0, 1} ↑m ℕ)
∩ 𝑅) ∣
Σ𝑘 ∈ ℕ
((𝑑‘𝑘) · 𝑘) = 𝑁} |
| 157 | 156 | a1i 11 |
. . . 4
⊢ (⊤
→ 𝐷 = {𝑑 ∈ (({0, 1}
↑m ℕ) ∩ 𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑑‘𝑘) · 𝑘) = 𝑁}) |
| 158 | 116, 117,
157 | f1oeq123d 6842 |
. . 3
⊢ (⊤
→ ((𝐺 ↾ 𝑂):𝑂–1-1-onto→𝐷 ↔ (𝐺 ↾ {𝑞 ∈ (𝑇 ∩ 𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑞‘𝑘) · 𝑘) = 𝑁}):{𝑞 ∈ (𝑇 ∩ 𝑅) ∣ Σ𝑘 ∈ ℕ ((𝑞‘𝑘) · 𝑘) = 𝑁}–1-1-onto→{𝑑 ∈ (({0, 1} ↑m ℕ)
∩ 𝑅) ∣
Σ𝑘 ∈ ℕ
((𝑑‘𝑘) · 𝑘) = 𝑁})) |
| 159 | 72, 158 | mpbird 257 |
. 2
⊢ (⊤
→ (𝐺 ↾ 𝑂):𝑂–1-1-onto→𝐷) |
| 160 | 159 | mptru 1547 |
1
⊢ (𝐺 ↾ 𝑂):𝑂–1-1-onto→𝐷 |