Proof of Theorem eulerpartlemgu
Step | Hyp | Ref
| Expression |
1 | | eulerpartlemgh.1 |
. 2
⊢ 𝑈 = ∪ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡))) |
2 | | eqid 2610 |
. . . 4
⊢ ∪ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × ((bits ∘ 𝐴)‘𝑡)) = ∪
𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × ((bits ∘ 𝐴)‘𝑡)) |
3 | 2 | marypha2lem2 8225 |
. . 3
⊢ ∪ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × ((bits ∘ 𝐴)‘𝑡)) = {〈𝑡, 𝑛〉 ∣ (𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽) ∧ 𝑛 ∈ ((bits ∘ 𝐴)‘𝑡))} |
4 | | eulerpart.p |
. . . . . . . . . . 11
⊢ 𝑃 = {𝑓 ∈ (ℕ0
↑𝑚 ℕ) ∣ ((◡𝑓 “ ℕ) ∈ Fin ∧
Σ𝑘 ∈ ℕ
((𝑓‘𝑘) · 𝑘) = 𝑁)} |
5 | | eulerpart.o |
. . . . . . . . . . 11
⊢ 𝑂 = {𝑔 ∈ 𝑃 ∣ ∀𝑛 ∈ (◡𝑔 “ ℕ) ¬ 2 ∥ 𝑛} |
6 | | eulerpart.d |
. . . . . . . . . . 11
⊢ 𝐷 = {𝑔 ∈ 𝑃 ∣ ∀𝑛 ∈ ℕ (𝑔‘𝑛) ≤ 1} |
7 | | eulerpart.j |
. . . . . . . . . . 11
⊢ 𝐽 = {𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧} |
8 | | eulerpart.f |
. . . . . . . . . . 11
⊢ 𝐹 = (𝑥 ∈ 𝐽, 𝑦 ∈ ℕ0 ↦
((2↑𝑦) · 𝑥)) |
9 | | eulerpart.h |
. . . . . . . . . . 11
⊢ 𝐻 = {𝑟 ∈ ((𝒫 ℕ0 ∩
Fin) ↑𝑚 𝐽) ∣ (𝑟 supp ∅) ∈ Fin} |
10 | | eulerpart.m |
. . . . . . . . . . 11
⊢ 𝑀 = (𝑟 ∈ 𝐻 ↦ {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ (𝑟‘𝑥))}) |
11 | | eulerpart.r |
. . . . . . . . . . 11
⊢ 𝑅 = {𝑓 ∣ (◡𝑓 “ ℕ) ∈
Fin} |
12 | | eulerpart.t |
. . . . . . . . . . 11
⊢ 𝑇 = {𝑓 ∈ (ℕ0
↑𝑚 ℕ) ∣ (◡𝑓 “ ℕ) ⊆ 𝐽} |
13 | 4, 5, 6, 7, 8, 9, 10, 11, 12 | eulerpartlemt0 29758 |
. . . . . . . . . 10
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) ↔ (𝐴 ∈ (ℕ0
↑𝑚 ℕ) ∧ (◡𝐴 “ ℕ) ∈ Fin ∧ (◡𝐴 “ ℕ) ⊆ 𝐽)) |
14 | 13 | simp1bi 1069 |
. . . . . . . . 9
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → 𝐴 ∈ (ℕ0
↑𝑚 ℕ)) |
15 | | elmapi 7765 |
. . . . . . . . 9
⊢ (𝐴 ∈ (ℕ0
↑𝑚 ℕ) → 𝐴:ℕ⟶ℕ0) |
16 | 14, 15 | syl 17 |
. . . . . . . 8
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → 𝐴:ℕ⟶ℕ0) |
17 | 16 | adantr 480 |
. . . . . . 7
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)) → 𝐴:ℕ⟶ℕ0) |
18 | | ffun 5961 |
. . . . . . 7
⊢ (𝐴:ℕ⟶ℕ0 →
Fun 𝐴) |
19 | 17, 18 | syl 17 |
. . . . . 6
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)) → Fun 𝐴) |
20 | | inss1 3795 |
. . . . . . . . 9
⊢ ((◡𝐴 “ ℕ) ∩ 𝐽) ⊆ (◡𝐴 “ ℕ) |
21 | | cnvimass 5404 |
. . . . . . . . . 10
⊢ (◡𝐴 “ ℕ) ⊆ dom 𝐴 |
22 | | fdm 5964 |
. . . . . . . . . . 11
⊢ (𝐴:ℕ⟶ℕ0 →
dom 𝐴 =
ℕ) |
23 | 16, 22 | syl 17 |
. . . . . . . . . 10
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → dom 𝐴 = ℕ) |
24 | 21, 23 | syl5sseq 3616 |
. . . . . . . . 9
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → (◡𝐴 “ ℕ) ⊆
ℕ) |
25 | 20, 24 | syl5ss 3579 |
. . . . . . . 8
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → ((◡𝐴 “ ℕ) ∩ 𝐽) ⊆ ℕ) |
26 | 25 | sselda 3568 |
. . . . . . 7
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)) → 𝑡 ∈ ℕ) |
27 | 23 | eleq2d 2673 |
. . . . . . . 8
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → (𝑡 ∈ dom 𝐴 ↔ 𝑡 ∈ ℕ)) |
28 | 27 | adantr 480 |
. . . . . . 7
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)) → (𝑡 ∈ dom 𝐴 ↔ 𝑡 ∈ ℕ)) |
29 | 26, 28 | mpbird 246 |
. . . . . 6
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)) → 𝑡 ∈ dom 𝐴) |
30 | | fvco 6184 |
. . . . . 6
⊢ ((Fun
𝐴 ∧ 𝑡 ∈ dom 𝐴) → ((bits ∘ 𝐴)‘𝑡) = (bits‘(𝐴‘𝑡))) |
31 | 19, 29, 30 | syl2anc 691 |
. . . . 5
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)) → ((bits ∘ 𝐴)‘𝑡) = (bits‘(𝐴‘𝑡))) |
32 | 31 | xpeq2d 5063 |
. . . 4
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)) → ({𝑡} × ((bits ∘ 𝐴)‘𝑡)) = ({𝑡} × (bits‘(𝐴‘𝑡)))) |
33 | 32 | iuneq2dv 4478 |
. . 3
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → ∪
𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × ((bits ∘ 𝐴)‘𝑡)) = ∪
𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡)))) |
34 | 3, 33 | syl5reqr 2659 |
. 2
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → ∪
𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡))) = {〈𝑡, 𝑛〉 ∣ (𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽) ∧ 𝑛 ∈ ((bits ∘ 𝐴)‘𝑡))}) |
35 | 1, 34 | syl5eq 2656 |
1
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → 𝑈 = {〈𝑡, 𝑛〉 ∣ (𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽) ∧ 𝑛 ∈ ((bits ∘ 𝐴)‘𝑡))}) |