Proof of Theorem eulerpartlemf
| Step | Hyp | Ref
| Expression |
| 1 | | eldif 3961 |
. . . . . 6
⊢ (𝑡 ∈ (ℕ ∖ 𝐽) ↔ (𝑡 ∈ ℕ ∧ ¬ 𝑡 ∈ 𝐽)) |
| 2 | | breq2 5147 |
. . . . . . . . . . 11
⊢ (𝑧 = 𝑡 → (2 ∥ 𝑧 ↔ 2 ∥ 𝑡)) |
| 3 | 2 | notbid 318 |
. . . . . . . . . 10
⊢ (𝑧 = 𝑡 → (¬ 2 ∥ 𝑧 ↔ ¬ 2 ∥ 𝑡)) |
| 4 | | eulerpart.j |
. . . . . . . . . 10
⊢ 𝐽 = {𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧} |
| 5 | 3, 4 | elrab2 3695 |
. . . . . . . . 9
⊢ (𝑡 ∈ 𝐽 ↔ (𝑡 ∈ ℕ ∧ ¬ 2 ∥ 𝑡)) |
| 6 | 5 | simplbi2 500 |
. . . . . . . 8
⊢ (𝑡 ∈ ℕ → (¬ 2
∥ 𝑡 → 𝑡 ∈ 𝐽)) |
| 7 | 6 | con1d 145 |
. . . . . . 7
⊢ (𝑡 ∈ ℕ → (¬
𝑡 ∈ 𝐽 → 2 ∥ 𝑡)) |
| 8 | 7 | imp 406 |
. . . . . 6
⊢ ((𝑡 ∈ ℕ ∧ ¬
𝑡 ∈ 𝐽) → 2 ∥ 𝑡) |
| 9 | 1, 8 | sylbi 217 |
. . . . 5
⊢ (𝑡 ∈ (ℕ ∖ 𝐽) → 2 ∥ 𝑡) |
| 10 | 9 | adantl 481 |
. . . 4
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ (ℕ ∖ 𝐽)) → 2 ∥ 𝑡) |
| 11 | 10 | adantr 480 |
. . 3
⊢ (((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ (ℕ ∖ 𝐽)) ∧ (𝐴‘𝑡) ∈ ℕ) → 2 ∥ 𝑡) |
| 12 | | simpll 767 |
. . . 4
⊢ (((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ (ℕ ∖ 𝐽)) ∧ (𝐴‘𝑡) ∈ ℕ) → 𝐴 ∈ (𝑇 ∩ 𝑅)) |
| 13 | | eldifi 4131 |
. . . . . 6
⊢ (𝑡 ∈ (ℕ ∖ 𝐽) → 𝑡 ∈ ℕ) |
| 14 | | eulerpart.p |
. . . . . . . . . . 11
⊢ 𝑃 = {𝑓 ∈ (ℕ0
↑m ℕ) ∣ ((◡𝑓 “ ℕ) ∈ Fin ∧
Σ𝑘 ∈ ℕ
((𝑓‘𝑘) · 𝑘) = 𝑁)} |
| 15 | | eulerpart.o |
. . . . . . . . . . 11
⊢ 𝑂 = {𝑔 ∈ 𝑃 ∣ ∀𝑛 ∈ (◡𝑔 “ ℕ) ¬ 2 ∥ 𝑛} |
| 16 | | eulerpart.d |
. . . . . . . . . . 11
⊢ 𝐷 = {𝑔 ∈ 𝑃 ∣ ∀𝑛 ∈ ℕ (𝑔‘𝑛) ≤ 1} |
| 17 | | eulerpart.f |
. . . . . . . . . . 11
⊢ 𝐹 = (𝑥 ∈ 𝐽, 𝑦 ∈ ℕ0 ↦
((2↑𝑦) · 𝑥)) |
| 18 | | eulerpart.h |
. . . . . . . . . . 11
⊢ 𝐻 = {𝑟 ∈ ((𝒫 ℕ0 ∩
Fin) ↑m 𝐽)
∣ (𝑟 supp ∅)
∈ Fin} |
| 19 | | eulerpart.m |
. . . . . . . . . . 11
⊢ 𝑀 = (𝑟 ∈ 𝐻 ↦ {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ (𝑟‘𝑥))}) |
| 20 | | eulerpart.r |
. . . . . . . . . . 11
⊢ 𝑅 = {𝑓 ∣ (◡𝑓 “ ℕ) ∈
Fin} |
| 21 | | eulerpart.t |
. . . . . . . . . . 11
⊢ 𝑇 = {𝑓 ∈ (ℕ0
↑m ℕ) ∣ (◡𝑓 “ ℕ) ⊆ 𝐽} |
| 22 | 14, 15, 16, 4, 17, 18, 19, 20, 21 | eulerpartlemt0 34371 |
. . . . . . . . . 10
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) ↔ (𝐴 ∈ (ℕ0
↑m ℕ) ∧ (◡𝐴 “ ℕ) ∈ Fin ∧ (◡𝐴 “ ℕ) ⊆ 𝐽)) |
| 23 | 22 | simp1bi 1146 |
. . . . . . . . 9
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → 𝐴 ∈ (ℕ0
↑m ℕ)) |
| 24 | | elmapi 8889 |
. . . . . . . . 9
⊢ (𝐴 ∈ (ℕ0
↑m ℕ) → 𝐴:ℕ⟶ℕ0) |
| 25 | 23, 24 | syl 17 |
. . . . . . . 8
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → 𝐴:ℕ⟶ℕ0) |
| 26 | | ffn 6736 |
. . . . . . . 8
⊢ (𝐴:ℕ⟶ℕ0 →
𝐴 Fn
ℕ) |
| 27 | | elpreima 7078 |
. . . . . . . 8
⊢ (𝐴 Fn ℕ → (𝑡 ∈ (◡𝐴 “ ℕ) ↔ (𝑡 ∈ ℕ ∧ (𝐴‘𝑡) ∈ ℕ))) |
| 28 | 25, 26, 27 | 3syl 18 |
. . . . . . 7
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → (𝑡 ∈ (◡𝐴 “ ℕ) ↔ (𝑡 ∈ ℕ ∧ (𝐴‘𝑡) ∈ ℕ))) |
| 29 | 28 | baibd 539 |
. . . . . 6
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ ℕ) → (𝑡 ∈ (◡𝐴 “ ℕ) ↔ (𝐴‘𝑡) ∈ ℕ)) |
| 30 | 13, 29 | sylan2 593 |
. . . . 5
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ (ℕ ∖ 𝐽)) → (𝑡 ∈ (◡𝐴 “ ℕ) ↔ (𝐴‘𝑡) ∈ ℕ)) |
| 31 | 30 | biimpar 477 |
. . . 4
⊢ (((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ (ℕ ∖ 𝐽)) ∧ (𝐴‘𝑡) ∈ ℕ) → 𝑡 ∈ (◡𝐴 “ ℕ)) |
| 32 | 22 | simp3bi 1148 |
. . . . . 6
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → (◡𝐴 “ ℕ) ⊆ 𝐽) |
| 33 | 32 | sselda 3983 |
. . . . 5
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ (◡𝐴 “ ℕ)) → 𝑡 ∈ 𝐽) |
| 34 | 5 | simprbi 496 |
. . . . 5
⊢ (𝑡 ∈ 𝐽 → ¬ 2 ∥ 𝑡) |
| 35 | 33, 34 | syl 17 |
. . . 4
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ (◡𝐴 “ ℕ)) → ¬ 2 ∥
𝑡) |
| 36 | 12, 31, 35 | syl2anc 584 |
. . 3
⊢ (((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ (ℕ ∖ 𝐽)) ∧ (𝐴‘𝑡) ∈ ℕ) → ¬ 2 ∥
𝑡) |
| 37 | 11, 36 | pm2.65da 817 |
. 2
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ (ℕ ∖ 𝐽)) → ¬ (𝐴‘𝑡) ∈ ℕ) |
| 38 | 25 | adantr 480 |
. . . 4
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ (ℕ ∖ 𝐽)) → 𝐴:ℕ⟶ℕ0) |
| 39 | 13 | adantl 481 |
. . . 4
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ (ℕ ∖ 𝐽)) → 𝑡 ∈ ℕ) |
| 40 | 38, 39 | ffvelcdmd 7105 |
. . 3
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ (ℕ ∖ 𝐽)) → (𝐴‘𝑡) ∈
ℕ0) |
| 41 | | elnn0 12528 |
. . 3
⊢ ((𝐴‘𝑡) ∈ ℕ0 ↔ ((𝐴‘𝑡) ∈ ℕ ∨ (𝐴‘𝑡) = 0)) |
| 42 | 40, 41 | sylib 218 |
. 2
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ (ℕ ∖ 𝐽)) → ((𝐴‘𝑡) ∈ ℕ ∨ (𝐴‘𝑡) = 0)) |
| 43 | | orel1 889 |
. 2
⊢ (¬
(𝐴‘𝑡) ∈ ℕ → (((𝐴‘𝑡) ∈ ℕ ∨ (𝐴‘𝑡) = 0) → (𝐴‘𝑡) = 0)) |
| 44 | 37, 42, 43 | sylc 65 |
1
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ (ℕ ∖ 𝐽)) → (𝐴‘𝑡) = 0) |