Proof of Theorem eulerpartlemsv2
Step | Hyp | Ref
| Expression |
1 | | eulerpartlems.r |
. . 3
⊢ 𝑅 = {𝑓 ∣ (◡𝑓 “ ℕ) ∈
Fin} |
2 | | eulerpartlems.s |
. . 3
⊢ 𝑆 = (𝑓 ∈ ((ℕ0
↑𝑚 ℕ) ∩ 𝑅) ↦ Σ𝑘 ∈ ℕ ((𝑓‘𝑘) · 𝑘)) |
3 | 1, 2 | eulerpartlemsv1 29745 |
. 2
⊢ (𝐴 ∈ ((ℕ0
↑𝑚 ℕ) ∩ 𝑅) → (𝑆‘𝐴) = Σ𝑘 ∈ ℕ ((𝐴‘𝑘) · 𝑘)) |
4 | | cnvimass 5404 |
. . . 4
⊢ (◡𝐴 “ ℕ) ⊆ dom 𝐴 |
5 | 1, 2 | eulerpartlemelr 29746 |
. . . . . 6
⊢ (𝐴 ∈ ((ℕ0
↑𝑚 ℕ) ∩ 𝑅) → (𝐴:ℕ⟶ℕ0 ∧
(◡𝐴 “ ℕ) ∈
Fin)) |
6 | 5 | simpld 474 |
. . . . 5
⊢ (𝐴 ∈ ((ℕ0
↑𝑚 ℕ) ∩ 𝑅) → 𝐴:ℕ⟶ℕ0) |
7 | | fdm 5964 |
. . . . 5
⊢ (𝐴:ℕ⟶ℕ0 →
dom 𝐴 =
ℕ) |
8 | 6, 7 | syl 17 |
. . . 4
⊢ (𝐴 ∈ ((ℕ0
↑𝑚 ℕ) ∩ 𝑅) → dom 𝐴 = ℕ) |
9 | 4, 8 | syl5sseq 3616 |
. . 3
⊢ (𝐴 ∈ ((ℕ0
↑𝑚 ℕ) ∩ 𝑅) → (◡𝐴 “ ℕ) ⊆
ℕ) |
10 | 6 | adantr 480 |
. . . . . 6
⊢ ((𝐴 ∈ ((ℕ0
↑𝑚 ℕ) ∩ 𝑅) ∧ 𝑘 ∈ (◡𝐴 “ ℕ)) → 𝐴:ℕ⟶ℕ0) |
11 | 9 | sselda 3568 |
. . . . . 6
⊢ ((𝐴 ∈ ((ℕ0
↑𝑚 ℕ) ∩ 𝑅) ∧ 𝑘 ∈ (◡𝐴 “ ℕ)) → 𝑘 ∈ ℕ) |
12 | 10, 11 | ffvelrnd 6268 |
. . . . 5
⊢ ((𝐴 ∈ ((ℕ0
↑𝑚 ℕ) ∩ 𝑅) ∧ 𝑘 ∈ (◡𝐴 “ ℕ)) → (𝐴‘𝑘) ∈
ℕ0) |
13 | 11 | nnnn0d 11228 |
. . . . 5
⊢ ((𝐴 ∈ ((ℕ0
↑𝑚 ℕ) ∩ 𝑅) ∧ 𝑘 ∈ (◡𝐴 “ ℕ)) → 𝑘 ∈ ℕ0) |
14 | 12, 13 | nn0mulcld 11233 |
. . . 4
⊢ ((𝐴 ∈ ((ℕ0
↑𝑚 ℕ) ∩ 𝑅) ∧ 𝑘 ∈ (◡𝐴 “ ℕ)) → ((𝐴‘𝑘) · 𝑘) ∈
ℕ0) |
15 | 14 | nn0cnd 11230 |
. . 3
⊢ ((𝐴 ∈ ((ℕ0
↑𝑚 ℕ) ∩ 𝑅) ∧ 𝑘 ∈ (◡𝐴 “ ℕ)) → ((𝐴‘𝑘) · 𝑘) ∈ ℂ) |
16 | | simpr 476 |
. . . . . . . 8
⊢ ((𝐴 ∈ ((ℕ0
↑𝑚 ℕ) ∩ 𝑅) ∧ 𝑘 ∈ (ℕ ∖ (◡𝐴 “ ℕ))) → 𝑘 ∈ (ℕ ∖ (◡𝐴 “ ℕ))) |
17 | 16 | eldifad 3552 |
. . . . . . 7
⊢ ((𝐴 ∈ ((ℕ0
↑𝑚 ℕ) ∩ 𝑅) ∧ 𝑘 ∈ (ℕ ∖ (◡𝐴 “ ℕ))) → 𝑘 ∈
ℕ) |
18 | 16 | eldifbd 3553 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ((ℕ0
↑𝑚 ℕ) ∩ 𝑅) ∧ 𝑘 ∈ (ℕ ∖ (◡𝐴 “ ℕ))) → ¬ 𝑘 ∈ (◡𝐴 “ ℕ)) |
19 | 6 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ((ℕ0
↑𝑚 ℕ) ∩ 𝑅) ∧ 𝑘 ∈ (ℕ ∖ (◡𝐴 “ ℕ))) → 𝐴:ℕ⟶ℕ0) |
20 | | ffn 5958 |
. . . . . . . . . 10
⊢ (𝐴:ℕ⟶ℕ0 →
𝐴 Fn
ℕ) |
21 | | elpreima 6245 |
. . . . . . . . . 10
⊢ (𝐴 Fn ℕ → (𝑘 ∈ (◡𝐴 “ ℕ) ↔ (𝑘 ∈ ℕ ∧ (𝐴‘𝑘) ∈ ℕ))) |
22 | 19, 20, 21 | 3syl 18 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ((ℕ0
↑𝑚 ℕ) ∩ 𝑅) ∧ 𝑘 ∈ (ℕ ∖ (◡𝐴 “ ℕ))) → (𝑘 ∈ (◡𝐴 “ ℕ) ↔ (𝑘 ∈ ℕ ∧ (𝐴‘𝑘) ∈ ℕ))) |
23 | 18, 22 | mtbid 313 |
. . . . . . . 8
⊢ ((𝐴 ∈ ((ℕ0
↑𝑚 ℕ) ∩ 𝑅) ∧ 𝑘 ∈ (ℕ ∖ (◡𝐴 “ ℕ))) → ¬ (𝑘 ∈ ℕ ∧ (𝐴‘𝑘) ∈ ℕ)) |
24 | | imnan 437 |
. . . . . . . 8
⊢ ((𝑘 ∈ ℕ → ¬
(𝐴‘𝑘) ∈ ℕ) ↔ ¬ (𝑘 ∈ ℕ ∧ (𝐴‘𝑘) ∈ ℕ)) |
25 | 23, 24 | sylibr 223 |
. . . . . . 7
⊢ ((𝐴 ∈ ((ℕ0
↑𝑚 ℕ) ∩ 𝑅) ∧ 𝑘 ∈ (ℕ ∖ (◡𝐴 “ ℕ))) → (𝑘 ∈ ℕ → ¬
(𝐴‘𝑘) ∈ ℕ)) |
26 | 17, 25 | mpd 15 |
. . . . . 6
⊢ ((𝐴 ∈ ((ℕ0
↑𝑚 ℕ) ∩ 𝑅) ∧ 𝑘 ∈ (ℕ ∖ (◡𝐴 “ ℕ))) → ¬ (𝐴‘𝑘) ∈ ℕ) |
27 | 19, 17 | ffvelrnd 6268 |
. . . . . . 7
⊢ ((𝐴 ∈ ((ℕ0
↑𝑚 ℕ) ∩ 𝑅) ∧ 𝑘 ∈ (ℕ ∖ (◡𝐴 “ ℕ))) → (𝐴‘𝑘) ∈
ℕ0) |
28 | | elnn0 11171 |
. . . . . . 7
⊢ ((𝐴‘𝑘) ∈ ℕ0 ↔ ((𝐴‘𝑘) ∈ ℕ ∨ (𝐴‘𝑘) = 0)) |
29 | 27, 28 | sylib 207 |
. . . . . 6
⊢ ((𝐴 ∈ ((ℕ0
↑𝑚 ℕ) ∩ 𝑅) ∧ 𝑘 ∈ (ℕ ∖ (◡𝐴 “ ℕ))) → ((𝐴‘𝑘) ∈ ℕ ∨ (𝐴‘𝑘) = 0)) |
30 | | orel1 396 |
. . . . . 6
⊢ (¬
(𝐴‘𝑘) ∈ ℕ → (((𝐴‘𝑘) ∈ ℕ ∨ (𝐴‘𝑘) = 0) → (𝐴‘𝑘) = 0)) |
31 | 26, 29, 30 | sylc 63 |
. . . . 5
⊢ ((𝐴 ∈ ((ℕ0
↑𝑚 ℕ) ∩ 𝑅) ∧ 𝑘 ∈ (ℕ ∖ (◡𝐴 “ ℕ))) → (𝐴‘𝑘) = 0) |
32 | 31 | oveq1d 6564 |
. . . 4
⊢ ((𝐴 ∈ ((ℕ0
↑𝑚 ℕ) ∩ 𝑅) ∧ 𝑘 ∈ (ℕ ∖ (◡𝐴 “ ℕ))) → ((𝐴‘𝑘) · 𝑘) = (0 · 𝑘)) |
33 | 17 | nncnd 10913 |
. . . . 5
⊢ ((𝐴 ∈ ((ℕ0
↑𝑚 ℕ) ∩ 𝑅) ∧ 𝑘 ∈ (ℕ ∖ (◡𝐴 “ ℕ))) → 𝑘 ∈
ℂ) |
34 | 33 | mul02d 10113 |
. . . 4
⊢ ((𝐴 ∈ ((ℕ0
↑𝑚 ℕ) ∩ 𝑅) ∧ 𝑘 ∈ (ℕ ∖ (◡𝐴 “ ℕ))) → (0 · 𝑘) = 0) |
35 | 32, 34 | eqtrd 2644 |
. . 3
⊢ ((𝐴 ∈ ((ℕ0
↑𝑚 ℕ) ∩ 𝑅) ∧ 𝑘 ∈ (ℕ ∖ (◡𝐴 “ ℕ))) → ((𝐴‘𝑘) · 𝑘) = 0) |
36 | | nnuz 11599 |
. . . . 5
⊢ ℕ =
(ℤ≥‘1) |
37 | 36 | eqimssi 3622 |
. . . 4
⊢ ℕ
⊆ (ℤ≥‘1) |
38 | 37 | a1i 11 |
. . 3
⊢ (𝐴 ∈ ((ℕ0
↑𝑚 ℕ) ∩ 𝑅) → ℕ ⊆
(ℤ≥‘1)) |
39 | 9, 15, 35, 38 | sumss 14302 |
. 2
⊢ (𝐴 ∈ ((ℕ0
↑𝑚 ℕ) ∩ 𝑅) → Σ𝑘 ∈ (◡𝐴 “ ℕ)((𝐴‘𝑘) · 𝑘) = Σ𝑘 ∈ ℕ ((𝐴‘𝑘) · 𝑘)) |
40 | 3, 39 | eqtr4d 2647 |
1
⊢ (𝐴 ∈ ((ℕ0
↑𝑚 ℕ) ∩ 𝑅) → (𝑆‘𝐴) = Σ𝑘 ∈ (◡𝐴 “ ℕ)((𝐴‘𝑘) · 𝑘)) |