Proof of Theorem eulerpartlemv
| Step | Hyp | Ref
| Expression |
| 1 | | eulerpart.p |
. . 3
⊢ 𝑃 = {𝑓 ∈ (ℕ0
↑m ℕ) ∣ ((◡𝑓 “ ℕ) ∈ Fin ∧
Σ𝑘 ∈ ℕ
((𝑓‘𝑘) · 𝑘) = 𝑁)} |
| 2 | 1 | eulerpartleme 34365 |
. 2
⊢ (𝐴 ∈ 𝑃 ↔ (𝐴:ℕ⟶ℕ0 ∧
(◡𝐴 “ ℕ) ∈ Fin ∧
Σ𝑘 ∈ ℕ
((𝐴‘𝑘) · 𝑘) = 𝑁)) |
| 3 | | cnvimass 6100 |
. . . . . . . . 9
⊢ (◡𝐴 “ ℕ) ⊆ dom 𝐴 |
| 4 | | fdm 6745 |
. . . . . . . . 9
⊢ (𝐴:ℕ⟶ℕ0 →
dom 𝐴 =
ℕ) |
| 5 | 3, 4 | sseqtrid 4026 |
. . . . . . . 8
⊢ (𝐴:ℕ⟶ℕ0 →
(◡𝐴 “ ℕ) ⊆
ℕ) |
| 6 | | simpl 482 |
. . . . . . . . . . 11
⊢ ((𝐴:ℕ⟶ℕ0 ∧
𝑘 ∈ (◡𝐴 “ ℕ)) → 𝐴:ℕ⟶ℕ0) |
| 7 | 5 | sselda 3983 |
. . . . . . . . . . 11
⊢ ((𝐴:ℕ⟶ℕ0 ∧
𝑘 ∈ (◡𝐴 “ ℕ)) → 𝑘 ∈ ℕ) |
| 8 | 6, 7 | ffvelcdmd 7105 |
. . . . . . . . . 10
⊢ ((𝐴:ℕ⟶ℕ0 ∧
𝑘 ∈ (◡𝐴 “ ℕ)) → (𝐴‘𝑘) ∈
ℕ0) |
| 9 | 7 | nnnn0d 12587 |
. . . . . . . . . 10
⊢ ((𝐴:ℕ⟶ℕ0 ∧
𝑘 ∈ (◡𝐴 “ ℕ)) → 𝑘 ∈ ℕ0) |
| 10 | 8, 9 | nn0mulcld 12592 |
. . . . . . . . 9
⊢ ((𝐴:ℕ⟶ℕ0 ∧
𝑘 ∈ (◡𝐴 “ ℕ)) → ((𝐴‘𝑘) · 𝑘) ∈
ℕ0) |
| 11 | 10 | nn0cnd 12589 |
. . . . . . . 8
⊢ ((𝐴:ℕ⟶ℕ0 ∧
𝑘 ∈ (◡𝐴 “ ℕ)) → ((𝐴‘𝑘) · 𝑘) ∈ ℂ) |
| 12 | | simpr 484 |
. . . . . . . . . . . . 13
⊢ ((𝐴:ℕ⟶ℕ0 ∧
𝑘 ∈ (ℕ ∖
(◡𝐴 “ ℕ))) → 𝑘 ∈ (ℕ ∖ (◡𝐴 “ ℕ))) |
| 13 | 12 | eldifad 3963 |
. . . . . . . . . . . 12
⊢ ((𝐴:ℕ⟶ℕ0 ∧
𝑘 ∈ (ℕ ∖
(◡𝐴 “ ℕ))) → 𝑘 ∈
ℕ) |
| 14 | 12 | eldifbd 3964 |
. . . . . . . . . . . . . 14
⊢ ((𝐴:ℕ⟶ℕ0 ∧
𝑘 ∈ (ℕ ∖
(◡𝐴 “ ℕ))) → ¬ 𝑘 ∈ (◡𝐴 “ ℕ)) |
| 15 | | simpl 482 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴:ℕ⟶ℕ0 ∧
𝑘 ∈ (ℕ ∖
(◡𝐴 “ ℕ))) → 𝐴:ℕ⟶ℕ0) |
| 16 | | ffn 6736 |
. . . . . . . . . . . . . . 15
⊢ (𝐴:ℕ⟶ℕ0 →
𝐴 Fn
ℕ) |
| 17 | | elpreima 7078 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 Fn ℕ → (𝑘 ∈ (◡𝐴 “ ℕ) ↔ (𝑘 ∈ ℕ ∧ (𝐴‘𝑘) ∈ ℕ))) |
| 18 | 15, 16, 17 | 3syl 18 |
. . . . . . . . . . . . . 14
⊢ ((𝐴:ℕ⟶ℕ0 ∧
𝑘 ∈ (ℕ ∖
(◡𝐴 “ ℕ))) → (𝑘 ∈ (◡𝐴 “ ℕ) ↔ (𝑘 ∈ ℕ ∧ (𝐴‘𝑘) ∈ ℕ))) |
| 19 | 14, 18 | mtbid 324 |
. . . . . . . . . . . . 13
⊢ ((𝐴:ℕ⟶ℕ0 ∧
𝑘 ∈ (ℕ ∖
(◡𝐴 “ ℕ))) → ¬ (𝑘 ∈ ℕ ∧ (𝐴‘𝑘) ∈ ℕ)) |
| 20 | | imnan 399 |
. . . . . . . . . . . . 13
⊢ ((𝑘 ∈ ℕ → ¬
(𝐴‘𝑘) ∈ ℕ) ↔ ¬ (𝑘 ∈ ℕ ∧ (𝐴‘𝑘) ∈ ℕ)) |
| 21 | 19, 20 | sylibr 234 |
. . . . . . . . . . . 12
⊢ ((𝐴:ℕ⟶ℕ0 ∧
𝑘 ∈ (ℕ ∖
(◡𝐴 “ ℕ))) → (𝑘 ∈ ℕ → ¬
(𝐴‘𝑘) ∈ ℕ)) |
| 22 | 13, 21 | mpd 15 |
. . . . . . . . . . 11
⊢ ((𝐴:ℕ⟶ℕ0 ∧
𝑘 ∈ (ℕ ∖
(◡𝐴 “ ℕ))) → ¬ (𝐴‘𝑘) ∈ ℕ) |
| 23 | 15, 13 | ffvelcdmd 7105 |
. . . . . . . . . . . 12
⊢ ((𝐴:ℕ⟶ℕ0 ∧
𝑘 ∈ (ℕ ∖
(◡𝐴 “ ℕ))) → (𝐴‘𝑘) ∈
ℕ0) |
| 24 | | elnn0 12528 |
. . . . . . . . . . . 12
⊢ ((𝐴‘𝑘) ∈ ℕ0 ↔ ((𝐴‘𝑘) ∈ ℕ ∨ (𝐴‘𝑘) = 0)) |
| 25 | 23, 24 | sylib 218 |
. . . . . . . . . . 11
⊢ ((𝐴:ℕ⟶ℕ0 ∧
𝑘 ∈ (ℕ ∖
(◡𝐴 “ ℕ))) → ((𝐴‘𝑘) ∈ ℕ ∨ (𝐴‘𝑘) = 0)) |
| 26 | | orel1 889 |
. . . . . . . . . . 11
⊢ (¬
(𝐴‘𝑘) ∈ ℕ → (((𝐴‘𝑘) ∈ ℕ ∨ (𝐴‘𝑘) = 0) → (𝐴‘𝑘) = 0)) |
| 27 | 22, 25, 26 | sylc 65 |
. . . . . . . . . 10
⊢ ((𝐴:ℕ⟶ℕ0 ∧
𝑘 ∈ (ℕ ∖
(◡𝐴 “ ℕ))) → (𝐴‘𝑘) = 0) |
| 28 | 27 | oveq1d 7446 |
. . . . . . . . 9
⊢ ((𝐴:ℕ⟶ℕ0 ∧
𝑘 ∈ (ℕ ∖
(◡𝐴 “ ℕ))) → ((𝐴‘𝑘) · 𝑘) = (0 · 𝑘)) |
| 29 | 13 | nncnd 12282 |
. . . . . . . . . 10
⊢ ((𝐴:ℕ⟶ℕ0 ∧
𝑘 ∈ (ℕ ∖
(◡𝐴 “ ℕ))) → 𝑘 ∈
ℂ) |
| 30 | 29 | mul02d 11459 |
. . . . . . . . 9
⊢ ((𝐴:ℕ⟶ℕ0 ∧
𝑘 ∈ (ℕ ∖
(◡𝐴 “ ℕ))) → (0 · 𝑘) = 0) |
| 31 | 28, 30 | eqtrd 2777 |
. . . . . . . 8
⊢ ((𝐴:ℕ⟶ℕ0 ∧
𝑘 ∈ (ℕ ∖
(◡𝐴 “ ℕ))) → ((𝐴‘𝑘) · 𝑘) = 0) |
| 32 | | nnuz 12921 |
. . . . . . . . . 10
⊢ ℕ =
(ℤ≥‘1) |
| 33 | 32 | eqimssi 4044 |
. . . . . . . . 9
⊢ ℕ
⊆ (ℤ≥‘1) |
| 34 | 33 | a1i 11 |
. . . . . . . 8
⊢ (𝐴:ℕ⟶ℕ0 →
ℕ ⊆ (ℤ≥‘1)) |
| 35 | 5, 11, 31, 34 | sumss 15760 |
. . . . . . 7
⊢ (𝐴:ℕ⟶ℕ0 →
Σ𝑘 ∈ (◡𝐴 “ ℕ)((𝐴‘𝑘) · 𝑘) = Σ𝑘 ∈ ℕ ((𝐴‘𝑘) · 𝑘)) |
| 36 | 35 | eqcomd 2743 |
. . . . . 6
⊢ (𝐴:ℕ⟶ℕ0 →
Σ𝑘 ∈ ℕ
((𝐴‘𝑘) · 𝑘) = Σ𝑘 ∈ (◡𝐴 “ ℕ)((𝐴‘𝑘) · 𝑘)) |
| 37 | 36 | adantr 480 |
. . . . 5
⊢ ((𝐴:ℕ⟶ℕ0 ∧
(◡𝐴 “ ℕ) ∈ Fin) →
Σ𝑘 ∈ ℕ
((𝐴‘𝑘) · 𝑘) = Σ𝑘 ∈ (◡𝐴 “ ℕ)((𝐴‘𝑘) · 𝑘)) |
| 38 | 37 | eqeq1d 2739 |
. . . 4
⊢ ((𝐴:ℕ⟶ℕ0 ∧
(◡𝐴 “ ℕ) ∈ Fin) →
(Σ𝑘 ∈ ℕ
((𝐴‘𝑘) · 𝑘) = 𝑁 ↔ Σ𝑘 ∈ (◡𝐴 “ ℕ)((𝐴‘𝑘) · 𝑘) = 𝑁)) |
| 39 | 38 | pm5.32i 574 |
. . 3
⊢ (((𝐴:ℕ⟶ℕ0 ∧
(◡𝐴 “ ℕ) ∈ Fin) ∧
Σ𝑘 ∈ ℕ
((𝐴‘𝑘) · 𝑘) = 𝑁) ↔ ((𝐴:ℕ⟶ℕ0 ∧
(◡𝐴 “ ℕ) ∈ Fin) ∧
Σ𝑘 ∈ (◡𝐴 “ ℕ)((𝐴‘𝑘) · 𝑘) = 𝑁)) |
| 40 | | df-3an 1089 |
. . 3
⊢ ((𝐴:ℕ⟶ℕ0 ∧
(◡𝐴 “ ℕ) ∈ Fin ∧
Σ𝑘 ∈ ℕ
((𝐴‘𝑘) · 𝑘) = 𝑁) ↔ ((𝐴:ℕ⟶ℕ0 ∧
(◡𝐴 “ ℕ) ∈ Fin) ∧
Σ𝑘 ∈ ℕ
((𝐴‘𝑘) · 𝑘) = 𝑁)) |
| 41 | | df-3an 1089 |
. . 3
⊢ ((𝐴:ℕ⟶ℕ0 ∧
(◡𝐴 “ ℕ) ∈ Fin ∧
Σ𝑘 ∈ (◡𝐴 “ ℕ)((𝐴‘𝑘) · 𝑘) = 𝑁) ↔ ((𝐴:ℕ⟶ℕ0 ∧
(◡𝐴 “ ℕ) ∈ Fin) ∧
Σ𝑘 ∈ (◡𝐴 “ ℕ)((𝐴‘𝑘) · 𝑘) = 𝑁)) |
| 42 | 39, 40, 41 | 3bitr4i 303 |
. 2
⊢ ((𝐴:ℕ⟶ℕ0 ∧
(◡𝐴 “ ℕ) ∈ Fin ∧
Σ𝑘 ∈ ℕ
((𝐴‘𝑘) · 𝑘) = 𝑁) ↔ (𝐴:ℕ⟶ℕ0 ∧
(◡𝐴 “ ℕ) ∈ Fin ∧
Σ𝑘 ∈ (◡𝐴 “ ℕ)((𝐴‘𝑘) · 𝑘) = 𝑁)) |
| 43 | 2, 42 | bitri 275 |
1
⊢ (𝐴 ∈ 𝑃 ↔ (𝐴:ℕ⟶ℕ0 ∧
(◡𝐴 “ ℕ) ∈ Fin ∧
Σ𝑘 ∈ (◡𝐴 “ ℕ)((𝐴‘𝑘) · 𝑘) = 𝑁)) |