Proof of Theorem eulerpartlemgu
Step | Hyp | Ref
| Expression |
1 | | eulerpartlemgh.1 |
. 2
⊢ 𝑈 = ∪ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡))) |
2 | | eulerpart.p |
. . . . . . . . . . 11
⊢ 𝑃 = {𝑓 ∈ (ℕ0
↑m ℕ) ∣ ((◡𝑓 “ ℕ) ∈ Fin ∧
Σ𝑘 ∈ ℕ
((𝑓‘𝑘) · 𝑘) = 𝑁)} |
3 | | eulerpart.o |
. . . . . . . . . . 11
⊢ 𝑂 = {𝑔 ∈ 𝑃 ∣ ∀𝑛 ∈ (◡𝑔 “ ℕ) ¬ 2 ∥ 𝑛} |
4 | | eulerpart.d |
. . . . . . . . . . 11
⊢ 𝐷 = {𝑔 ∈ 𝑃 ∣ ∀𝑛 ∈ ℕ (𝑔‘𝑛) ≤ 1} |
5 | | eulerpart.j |
. . . . . . . . . . 11
⊢ 𝐽 = {𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧} |
6 | | eulerpart.f |
. . . . . . . . . . 11
⊢ 𝐹 = (𝑥 ∈ 𝐽, 𝑦 ∈ ℕ0 ↦
((2↑𝑦) · 𝑥)) |
7 | | eulerpart.h |
. . . . . . . . . . 11
⊢ 𝐻 = {𝑟 ∈ ((𝒫 ℕ0 ∩
Fin) ↑m 𝐽)
∣ (𝑟 supp ∅)
∈ Fin} |
8 | | eulerpart.m |
. . . . . . . . . . 11
⊢ 𝑀 = (𝑟 ∈ 𝐻 ↦ {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ (𝑟‘𝑥))}) |
9 | | eulerpart.r |
. . . . . . . . . . 11
⊢ 𝑅 = {𝑓 ∣ (◡𝑓 “ ℕ) ∈
Fin} |
10 | | eulerpart.t |
. . . . . . . . . . 11
⊢ 𝑇 = {𝑓 ∈ (ℕ0
↑m ℕ) ∣ (◡𝑓 “ ℕ) ⊆ 𝐽} |
11 | 2, 3, 4, 5, 6, 7, 8, 9, 10 | eulerpartlemt0 31919 |
. . . . . . . . . 10
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) ↔ (𝐴 ∈ (ℕ0
↑m ℕ) ∧ (◡𝐴 “ ℕ) ∈ Fin ∧ (◡𝐴 “ ℕ) ⊆ 𝐽)) |
12 | 11 | simp1bi 1146 |
. . . . . . . . 9
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → 𝐴 ∈ (ℕ0
↑m ℕ)) |
13 | | elmapi 8472 |
. . . . . . . . 9
⊢ (𝐴 ∈ (ℕ0
↑m ℕ) → 𝐴:ℕ⟶ℕ0) |
14 | 12, 13 | syl 17 |
. . . . . . . 8
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → 𝐴:ℕ⟶ℕ0) |
15 | 14 | adantr 484 |
. . . . . . 7
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)) → 𝐴:ℕ⟶ℕ0) |
16 | 15 | ffund 6519 |
. . . . . 6
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)) → Fun 𝐴) |
17 | | inss1 4129 |
. . . . . . . . 9
⊢ ((◡𝐴 “ ℕ) ∩ 𝐽) ⊆ (◡𝐴 “ ℕ) |
18 | | cnvimass 5933 |
. . . . . . . . . 10
⊢ (◡𝐴 “ ℕ) ⊆ dom 𝐴 |
19 | 18, 14 | fssdm 6535 |
. . . . . . . . 9
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → (◡𝐴 “ ℕ) ⊆
ℕ) |
20 | 17, 19 | sstrid 3898 |
. . . . . . . 8
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → ((◡𝐴 “ ℕ) ∩ 𝐽) ⊆ ℕ) |
21 | 20 | sselda 3887 |
. . . . . . 7
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)) → 𝑡 ∈ ℕ) |
22 | 14 | fdmd 6526 |
. . . . . . . . 9
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → dom 𝐴 = ℕ) |
23 | 22 | eleq2d 2819 |
. . . . . . . 8
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → (𝑡 ∈ dom 𝐴 ↔ 𝑡 ∈ ℕ)) |
24 | 23 | adantr 484 |
. . . . . . 7
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)) → (𝑡 ∈ dom 𝐴 ↔ 𝑡 ∈ ℕ)) |
25 | 21, 24 | mpbird 260 |
. . . . . 6
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)) → 𝑡 ∈ dom 𝐴) |
26 | | fvco 6779 |
. . . . . 6
⊢ ((Fun
𝐴 ∧ 𝑡 ∈ dom 𝐴) → ((bits ∘ 𝐴)‘𝑡) = (bits‘(𝐴‘𝑡))) |
27 | 16, 25, 26 | syl2anc 587 |
. . . . 5
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)) → ((bits ∘ 𝐴)‘𝑡) = (bits‘(𝐴‘𝑡))) |
28 | 27 | xpeq2d 5565 |
. . . 4
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)) → ({𝑡} × ((bits ∘ 𝐴)‘𝑡)) = ({𝑡} × (bits‘(𝐴‘𝑡)))) |
29 | 28 | iuneq2dv 4915 |
. . 3
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → ∪
𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × ((bits ∘ 𝐴)‘𝑡)) = ∪
𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡)))) |
30 | | eqid 2739 |
. . . 4
⊢ ∪ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × ((bits ∘ 𝐴)‘𝑡)) = ∪
𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × ((bits ∘ 𝐴)‘𝑡)) |
31 | 30 | marypha2lem2 8986 |
. . 3
⊢ ∪ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × ((bits ∘ 𝐴)‘𝑡)) = {〈𝑡, 𝑛〉 ∣ (𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽) ∧ 𝑛 ∈ ((bits ∘ 𝐴)‘𝑡))} |
32 | 29, 31 | eqtr3di 2789 |
. 2
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → ∪
𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡))) = {〈𝑡, 𝑛〉 ∣ (𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽) ∧ 𝑛 ∈ ((bits ∘ 𝐴)‘𝑡))}) |
33 | 1, 32 | syl5eq 2786 |
1
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → 𝑈 = {〈𝑡, 𝑛〉 ∣ (𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽) ∧ 𝑛 ∈ ((bits ∘ 𝐴)‘𝑡))}) |