Proof of Theorem eulerpartlemv
Step | Hyp | Ref
| Expression |
1 | | eulerpart.p |
. . 3
⊢ 𝑃 = {𝑓 ∈ (ℕ0
↑𝑚 ℕ) ∣ ((◡𝑓 “ ℕ) ∈ Fin ∧
Σ𝑘 ∈ ℕ
((𝑓‘𝑘) · 𝑘) = 𝑁)} |
2 | 1 | eulerpartleme 29752 |
. 2
⊢ (𝐴 ∈ 𝑃 ↔ (𝐴:ℕ⟶ℕ0 ∧
(◡𝐴 “ ℕ) ∈ Fin ∧
Σ𝑘 ∈ ℕ
((𝐴‘𝑘) · 𝑘) = 𝑁)) |
3 | | cnvimass 5404 |
. . . . . . . . 9
⊢ (◡𝐴 “ ℕ) ⊆ dom 𝐴 |
4 | | fdm 5964 |
. . . . . . . . 9
⊢ (𝐴:ℕ⟶ℕ0 →
dom 𝐴 =
ℕ) |
5 | 3, 4 | syl5sseq 3616 |
. . . . . . . 8
⊢ (𝐴:ℕ⟶ℕ0 →
(◡𝐴 “ ℕ) ⊆
ℕ) |
6 | | simpl 472 |
. . . . . . . . . . 11
⊢ ((𝐴:ℕ⟶ℕ0 ∧
𝑘 ∈ (◡𝐴 “ ℕ)) → 𝐴:ℕ⟶ℕ0) |
7 | 5 | sselda 3568 |
. . . . . . . . . . 11
⊢ ((𝐴:ℕ⟶ℕ0 ∧
𝑘 ∈ (◡𝐴 “ ℕ)) → 𝑘 ∈ ℕ) |
8 | 6, 7 | ffvelrnd 6268 |
. . . . . . . . . 10
⊢ ((𝐴:ℕ⟶ℕ0 ∧
𝑘 ∈ (◡𝐴 “ ℕ)) → (𝐴‘𝑘) ∈
ℕ0) |
9 | 7 | nnnn0d 11228 |
. . . . . . . . . 10
⊢ ((𝐴:ℕ⟶ℕ0 ∧
𝑘 ∈ (◡𝐴 “ ℕ)) → 𝑘 ∈ ℕ0) |
10 | 8, 9 | nn0mulcld 11233 |
. . . . . . . . 9
⊢ ((𝐴:ℕ⟶ℕ0 ∧
𝑘 ∈ (◡𝐴 “ ℕ)) → ((𝐴‘𝑘) · 𝑘) ∈
ℕ0) |
11 | 10 | nn0cnd 11230 |
. . . . . . . 8
⊢ ((𝐴:ℕ⟶ℕ0 ∧
𝑘 ∈ (◡𝐴 “ ℕ)) → ((𝐴‘𝑘) · 𝑘) ∈ ℂ) |
12 | | simpr 476 |
. . . . . . . . . . . . 13
⊢ ((𝐴:ℕ⟶ℕ0 ∧
𝑘 ∈ (ℕ ∖
(◡𝐴 “ ℕ))) → 𝑘 ∈ (ℕ ∖ (◡𝐴 “ ℕ))) |
13 | 12 | eldifad 3552 |
. . . . . . . . . . . 12
⊢ ((𝐴:ℕ⟶ℕ0 ∧
𝑘 ∈ (ℕ ∖
(◡𝐴 “ ℕ))) → 𝑘 ∈
ℕ) |
14 | 12 | eldifbd 3553 |
. . . . . . . . . . . . . 14
⊢ ((𝐴:ℕ⟶ℕ0 ∧
𝑘 ∈ (ℕ ∖
(◡𝐴 “ ℕ))) → ¬ 𝑘 ∈ (◡𝐴 “ ℕ)) |
15 | | simpl 472 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴:ℕ⟶ℕ0 ∧
𝑘 ∈ (ℕ ∖
(◡𝐴 “ ℕ))) → 𝐴:ℕ⟶ℕ0) |
16 | | ffn 5958 |
. . . . . . . . . . . . . . 15
⊢ (𝐴:ℕ⟶ℕ0 →
𝐴 Fn
ℕ) |
17 | | elpreima 6245 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 Fn ℕ → (𝑘 ∈ (◡𝐴 “ ℕ) ↔ (𝑘 ∈ ℕ ∧ (𝐴‘𝑘) ∈ ℕ))) |
18 | 15, 16, 17 | 3syl 18 |
. . . . . . . . . . . . . 14
⊢ ((𝐴:ℕ⟶ℕ0 ∧
𝑘 ∈ (ℕ ∖
(◡𝐴 “ ℕ))) → (𝑘 ∈ (◡𝐴 “ ℕ) ↔ (𝑘 ∈ ℕ ∧ (𝐴‘𝑘) ∈ ℕ))) |
19 | 14, 18 | mtbid 313 |
. . . . . . . . . . . . 13
⊢ ((𝐴:ℕ⟶ℕ0 ∧
𝑘 ∈ (ℕ ∖
(◡𝐴 “ ℕ))) → ¬ (𝑘 ∈ ℕ ∧ (𝐴‘𝑘) ∈ ℕ)) |
20 | | imnan 437 |
. . . . . . . . . . . . 13
⊢ ((𝑘 ∈ ℕ → ¬
(𝐴‘𝑘) ∈ ℕ) ↔ ¬ (𝑘 ∈ ℕ ∧ (𝐴‘𝑘) ∈ ℕ)) |
21 | 19, 20 | sylibr 223 |
. . . . . . . . . . . 12
⊢ ((𝐴:ℕ⟶ℕ0 ∧
𝑘 ∈ (ℕ ∖
(◡𝐴 “ ℕ))) → (𝑘 ∈ ℕ → ¬
(𝐴‘𝑘) ∈ ℕ)) |
22 | 13, 21 | mpd 15 |
. . . . . . . . . . 11
⊢ ((𝐴:ℕ⟶ℕ0 ∧
𝑘 ∈ (ℕ ∖
(◡𝐴 “ ℕ))) → ¬ (𝐴‘𝑘) ∈ ℕ) |
23 | 15, 13 | ffvelrnd 6268 |
. . . . . . . . . . . 12
⊢ ((𝐴:ℕ⟶ℕ0 ∧
𝑘 ∈ (ℕ ∖
(◡𝐴 “ ℕ))) → (𝐴‘𝑘) ∈
ℕ0) |
24 | | elnn0 11171 |
. . . . . . . . . . . 12
⊢ ((𝐴‘𝑘) ∈ ℕ0 ↔ ((𝐴‘𝑘) ∈ ℕ ∨ (𝐴‘𝑘) = 0)) |
25 | 23, 24 | sylib 207 |
. . . . . . . . . . 11
⊢ ((𝐴:ℕ⟶ℕ0 ∧
𝑘 ∈ (ℕ ∖
(◡𝐴 “ ℕ))) → ((𝐴‘𝑘) ∈ ℕ ∨ (𝐴‘𝑘) = 0)) |
26 | | orel1 396 |
. . . . . . . . . . 11
⊢ (¬
(𝐴‘𝑘) ∈ ℕ → (((𝐴‘𝑘) ∈ ℕ ∨ (𝐴‘𝑘) = 0) → (𝐴‘𝑘) = 0)) |
27 | 22, 25, 26 | sylc 63 |
. . . . . . . . . 10
⊢ ((𝐴:ℕ⟶ℕ0 ∧
𝑘 ∈ (ℕ ∖
(◡𝐴 “ ℕ))) → (𝐴‘𝑘) = 0) |
28 | 27 | oveq1d 6564 |
. . . . . . . . 9
⊢ ((𝐴:ℕ⟶ℕ0 ∧
𝑘 ∈ (ℕ ∖
(◡𝐴 “ ℕ))) → ((𝐴‘𝑘) · 𝑘) = (0 · 𝑘)) |
29 | 13 | nncnd 10913 |
. . . . . . . . . 10
⊢ ((𝐴:ℕ⟶ℕ0 ∧
𝑘 ∈ (ℕ ∖
(◡𝐴 “ ℕ))) → 𝑘 ∈
ℂ) |
30 | 29 | mul02d 10113 |
. . . . . . . . 9
⊢ ((𝐴:ℕ⟶ℕ0 ∧
𝑘 ∈ (ℕ ∖
(◡𝐴 “ ℕ))) → (0 · 𝑘) = 0) |
31 | 28, 30 | eqtrd 2644 |
. . . . . . . 8
⊢ ((𝐴:ℕ⟶ℕ0 ∧
𝑘 ∈ (ℕ ∖
(◡𝐴 “ ℕ))) → ((𝐴‘𝑘) · 𝑘) = 0) |
32 | | nnuz 11599 |
. . . . . . . . . 10
⊢ ℕ =
(ℤ≥‘1) |
33 | 32 | eqimssi 3622 |
. . . . . . . . 9
⊢ ℕ
⊆ (ℤ≥‘1) |
34 | 33 | a1i 11 |
. . . . . . . 8
⊢ (𝐴:ℕ⟶ℕ0 →
ℕ ⊆ (ℤ≥‘1)) |
35 | 5, 11, 31, 34 | sumss 14302 |
. . . . . . 7
⊢ (𝐴:ℕ⟶ℕ0 →
Σ𝑘 ∈ (◡𝐴 “ ℕ)((𝐴‘𝑘) · 𝑘) = Σ𝑘 ∈ ℕ ((𝐴‘𝑘) · 𝑘)) |
36 | 35 | eqcomd 2616 |
. . . . . 6
⊢ (𝐴:ℕ⟶ℕ0 →
Σ𝑘 ∈ ℕ
((𝐴‘𝑘) · 𝑘) = Σ𝑘 ∈ (◡𝐴 “ ℕ)((𝐴‘𝑘) · 𝑘)) |
37 | 36 | adantr 480 |
. . . . 5
⊢ ((𝐴:ℕ⟶ℕ0 ∧
(◡𝐴 “ ℕ) ∈ Fin) →
Σ𝑘 ∈ ℕ
((𝐴‘𝑘) · 𝑘) = Σ𝑘 ∈ (◡𝐴 “ ℕ)((𝐴‘𝑘) · 𝑘)) |
38 | 37 | eqeq1d 2612 |
. . . 4
⊢ ((𝐴:ℕ⟶ℕ0 ∧
(◡𝐴 “ ℕ) ∈ Fin) →
(Σ𝑘 ∈ ℕ
((𝐴‘𝑘) · 𝑘) = 𝑁 ↔ Σ𝑘 ∈ (◡𝐴 “ ℕ)((𝐴‘𝑘) · 𝑘) = 𝑁)) |
39 | 38 | pm5.32i 667 |
. . 3
⊢ (((𝐴:ℕ⟶ℕ0 ∧
(◡𝐴 “ ℕ) ∈ Fin) ∧
Σ𝑘 ∈ ℕ
((𝐴‘𝑘) · 𝑘) = 𝑁) ↔ ((𝐴:ℕ⟶ℕ0 ∧
(◡𝐴 “ ℕ) ∈ Fin) ∧
Σ𝑘 ∈ (◡𝐴 “ ℕ)((𝐴‘𝑘) · 𝑘) = 𝑁)) |
40 | | df-3an 1033 |
. . 3
⊢ ((𝐴:ℕ⟶ℕ0 ∧
(◡𝐴 “ ℕ) ∈ Fin ∧
Σ𝑘 ∈ ℕ
((𝐴‘𝑘) · 𝑘) = 𝑁) ↔ ((𝐴:ℕ⟶ℕ0 ∧
(◡𝐴 “ ℕ) ∈ Fin) ∧
Σ𝑘 ∈ ℕ
((𝐴‘𝑘) · 𝑘) = 𝑁)) |
41 | | df-3an 1033 |
. . 3
⊢ ((𝐴:ℕ⟶ℕ0 ∧
(◡𝐴 “ ℕ) ∈ Fin ∧
Σ𝑘 ∈ (◡𝐴 “ ℕ)((𝐴‘𝑘) · 𝑘) = 𝑁) ↔ ((𝐴:ℕ⟶ℕ0 ∧
(◡𝐴 “ ℕ) ∈ Fin) ∧
Σ𝑘 ∈ (◡𝐴 “ ℕ)((𝐴‘𝑘) · 𝑘) = 𝑁)) |
42 | 39, 40, 41 | 3bitr4i 291 |
. 2
⊢ ((𝐴:ℕ⟶ℕ0 ∧
(◡𝐴 “ ℕ) ∈ Fin ∧
Σ𝑘 ∈ ℕ
((𝐴‘𝑘) · 𝑘) = 𝑁) ↔ (𝐴:ℕ⟶ℕ0 ∧
(◡𝐴 “ ℕ) ∈ Fin ∧
Σ𝑘 ∈ (◡𝐴 “ ℕ)((𝐴‘𝑘) · 𝑘) = 𝑁)) |
43 | 2, 42 | bitri 263 |
1
⊢ (𝐴 ∈ 𝑃 ↔ (𝐴:ℕ⟶ℕ0 ∧
(◡𝐴 “ ℕ) ∈ Fin ∧
Σ𝑘 ∈ (◡𝐴 “ ℕ)((𝐴‘𝑘) · 𝑘) = 𝑁)) |