Proof of Theorem eulerpartlemsv2
Step | Hyp | Ref
| Expression |
1 | | eulerpartlems.r |
. . 3
⊢ 𝑅 = {𝑓 ∣ (◡𝑓 “ ℕ) ∈
Fin} |
2 | | eulerpartlems.s |
. . 3
⊢ 𝑆 = (𝑓 ∈ ((ℕ0
↑𝑚 ℕ) ∩ 𝑅) ↦ Σ𝑘 ∈ ℕ ((𝑓‘𝑘) · 𝑘)) |
3 | 1, 2 | eulerpartlemsv1 30418 |
. 2
⊢ (𝐴 ∈ ((ℕ0
↑𝑚 ℕ) ∩ 𝑅) → (𝑆‘𝐴) = Σ𝑘 ∈ ℕ ((𝐴‘𝑘) · 𝑘)) |
4 | | cnvimass 5485 |
. . . 4
⊢ (◡𝐴 “ ℕ) ⊆ dom 𝐴 |
5 | 1, 2 | eulerpartlemelr 30419 |
. . . . . 6
⊢ (𝐴 ∈ ((ℕ0
↑𝑚 ℕ) ∩ 𝑅) → (𝐴:ℕ⟶ℕ0 ∧
(◡𝐴 “ ℕ) ∈
Fin)) |
6 | 5 | simpld 475 |
. . . . 5
⊢ (𝐴 ∈ ((ℕ0
↑𝑚 ℕ) ∩ 𝑅) → 𝐴:ℕ⟶ℕ0) |
7 | | fdm 6051 |
. . . . 5
⊢ (𝐴:ℕ⟶ℕ0 →
dom 𝐴 =
ℕ) |
8 | 6, 7 | syl 17 |
. . . 4
⊢ (𝐴 ∈ ((ℕ0
↑𝑚 ℕ) ∩ 𝑅) → dom 𝐴 = ℕ) |
9 | 4, 8 | syl5sseq 3653 |
. . 3
⊢ (𝐴 ∈ ((ℕ0
↑𝑚 ℕ) ∩ 𝑅) → (◡𝐴 “ ℕ) ⊆
ℕ) |
10 | 6 | adantr 481 |
. . . . . 6
⊢ ((𝐴 ∈ ((ℕ0
↑𝑚 ℕ) ∩ 𝑅) ∧ 𝑘 ∈ (◡𝐴 “ ℕ)) → 𝐴:ℕ⟶ℕ0) |
11 | 9 | sselda 3603 |
. . . . . 6
⊢ ((𝐴 ∈ ((ℕ0
↑𝑚 ℕ) ∩ 𝑅) ∧ 𝑘 ∈ (◡𝐴 “ ℕ)) → 𝑘 ∈ ℕ) |
12 | 10, 11 | ffvelrnd 6360 |
. . . . 5
⊢ ((𝐴 ∈ ((ℕ0
↑𝑚 ℕ) ∩ 𝑅) ∧ 𝑘 ∈ (◡𝐴 “ ℕ)) → (𝐴‘𝑘) ∈
ℕ0) |
13 | 11 | nnnn0d 11351 |
. . . . 5
⊢ ((𝐴 ∈ ((ℕ0
↑𝑚 ℕ) ∩ 𝑅) ∧ 𝑘 ∈ (◡𝐴 “ ℕ)) → 𝑘 ∈ ℕ0) |
14 | 12, 13 | nn0mulcld 11356 |
. . . 4
⊢ ((𝐴 ∈ ((ℕ0
↑𝑚 ℕ) ∩ 𝑅) ∧ 𝑘 ∈ (◡𝐴 “ ℕ)) → ((𝐴‘𝑘) · 𝑘) ∈
ℕ0) |
15 | 14 | nn0cnd 11353 |
. . 3
⊢ ((𝐴 ∈ ((ℕ0
↑𝑚 ℕ) ∩ 𝑅) ∧ 𝑘 ∈ (◡𝐴 “ ℕ)) → ((𝐴‘𝑘) · 𝑘) ∈ ℂ) |
16 | | simpr 477 |
. . . . . . . 8
⊢ ((𝐴 ∈ ((ℕ0
↑𝑚 ℕ) ∩ 𝑅) ∧ 𝑘 ∈ (ℕ ∖ (◡𝐴 “ ℕ))) → 𝑘 ∈ (ℕ ∖ (◡𝐴 “ ℕ))) |
17 | 16 | eldifad 3586 |
. . . . . . 7
⊢ ((𝐴 ∈ ((ℕ0
↑𝑚 ℕ) ∩ 𝑅) ∧ 𝑘 ∈ (ℕ ∖ (◡𝐴 “ ℕ))) → 𝑘 ∈
ℕ) |
18 | 16 | eldifbd 3587 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ((ℕ0
↑𝑚 ℕ) ∩ 𝑅) ∧ 𝑘 ∈ (ℕ ∖ (◡𝐴 “ ℕ))) → ¬ 𝑘 ∈ (◡𝐴 “ ℕ)) |
19 | 6 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ((ℕ0
↑𝑚 ℕ) ∩ 𝑅) ∧ 𝑘 ∈ (ℕ ∖ (◡𝐴 “ ℕ))) → 𝐴:ℕ⟶ℕ0) |
20 | | ffn 6045 |
. . . . . . . . . 10
⊢ (𝐴:ℕ⟶ℕ0 →
𝐴 Fn
ℕ) |
21 | | elpreima 6337 |
. . . . . . . . . 10
⊢ (𝐴 Fn ℕ → (𝑘 ∈ (◡𝐴 “ ℕ) ↔ (𝑘 ∈ ℕ ∧ (𝐴‘𝑘) ∈ ℕ))) |
22 | 19, 20, 21 | 3syl 18 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ((ℕ0
↑𝑚 ℕ) ∩ 𝑅) ∧ 𝑘 ∈ (ℕ ∖ (◡𝐴 “ ℕ))) → (𝑘 ∈ (◡𝐴 “ ℕ) ↔ (𝑘 ∈ ℕ ∧ (𝐴‘𝑘) ∈ ℕ))) |
23 | 18, 22 | mtbid 314 |
. . . . . . . 8
⊢ ((𝐴 ∈ ((ℕ0
↑𝑚 ℕ) ∩ 𝑅) ∧ 𝑘 ∈ (ℕ ∖ (◡𝐴 “ ℕ))) → ¬ (𝑘 ∈ ℕ ∧ (𝐴‘𝑘) ∈ ℕ)) |
24 | | imnan 438 |
. . . . . . . 8
⊢ ((𝑘 ∈ ℕ → ¬
(𝐴‘𝑘) ∈ ℕ) ↔ ¬ (𝑘 ∈ ℕ ∧ (𝐴‘𝑘) ∈ ℕ)) |
25 | 23, 24 | sylibr 224 |
. . . . . . 7
⊢ ((𝐴 ∈ ((ℕ0
↑𝑚 ℕ) ∩ 𝑅) ∧ 𝑘 ∈ (ℕ ∖ (◡𝐴 “ ℕ))) → (𝑘 ∈ ℕ → ¬
(𝐴‘𝑘) ∈ ℕ)) |
26 | 17, 25 | mpd 15 |
. . . . . 6
⊢ ((𝐴 ∈ ((ℕ0
↑𝑚 ℕ) ∩ 𝑅) ∧ 𝑘 ∈ (ℕ ∖ (◡𝐴 “ ℕ))) → ¬ (𝐴‘𝑘) ∈ ℕ) |
27 | 19, 17 | ffvelrnd 6360 |
. . . . . . 7
⊢ ((𝐴 ∈ ((ℕ0
↑𝑚 ℕ) ∩ 𝑅) ∧ 𝑘 ∈ (ℕ ∖ (◡𝐴 “ ℕ))) → (𝐴‘𝑘) ∈
ℕ0) |
28 | | elnn0 11294 |
. . . . . . 7
⊢ ((𝐴‘𝑘) ∈ ℕ0 ↔ ((𝐴‘𝑘) ∈ ℕ ∨ (𝐴‘𝑘) = 0)) |
29 | 27, 28 | sylib 208 |
. . . . . 6
⊢ ((𝐴 ∈ ((ℕ0
↑𝑚 ℕ) ∩ 𝑅) ∧ 𝑘 ∈ (ℕ ∖ (◡𝐴 “ ℕ))) → ((𝐴‘𝑘) ∈ ℕ ∨ (𝐴‘𝑘) = 0)) |
30 | | orel1 397 |
. . . . . 6
⊢ (¬
(𝐴‘𝑘) ∈ ℕ → (((𝐴‘𝑘) ∈ ℕ ∨ (𝐴‘𝑘) = 0) → (𝐴‘𝑘) = 0)) |
31 | 26, 29, 30 | sylc 65 |
. . . . 5
⊢ ((𝐴 ∈ ((ℕ0
↑𝑚 ℕ) ∩ 𝑅) ∧ 𝑘 ∈ (ℕ ∖ (◡𝐴 “ ℕ))) → (𝐴‘𝑘) = 0) |
32 | 31 | oveq1d 6665 |
. . . 4
⊢ ((𝐴 ∈ ((ℕ0
↑𝑚 ℕ) ∩ 𝑅) ∧ 𝑘 ∈ (ℕ ∖ (◡𝐴 “ ℕ))) → ((𝐴‘𝑘) · 𝑘) = (0 · 𝑘)) |
33 | 17 | nncnd 11036 |
. . . . 5
⊢ ((𝐴 ∈ ((ℕ0
↑𝑚 ℕ) ∩ 𝑅) ∧ 𝑘 ∈ (ℕ ∖ (◡𝐴 “ ℕ))) → 𝑘 ∈
ℂ) |
34 | 33 | mul02d 10234 |
. . . 4
⊢ ((𝐴 ∈ ((ℕ0
↑𝑚 ℕ) ∩ 𝑅) ∧ 𝑘 ∈ (ℕ ∖ (◡𝐴 “ ℕ))) → (0 · 𝑘) = 0) |
35 | 32, 34 | eqtrd 2656 |
. . 3
⊢ ((𝐴 ∈ ((ℕ0
↑𝑚 ℕ) ∩ 𝑅) ∧ 𝑘 ∈ (ℕ ∖ (◡𝐴 “ ℕ))) → ((𝐴‘𝑘) · 𝑘) = 0) |
36 | | nnuz 11723 |
. . . . 5
⊢ ℕ =
(ℤ≥‘1) |
37 | 36 | eqimssi 3659 |
. . . 4
⊢ ℕ
⊆ (ℤ≥‘1) |
38 | 37 | a1i 11 |
. . 3
⊢ (𝐴 ∈ ((ℕ0
↑𝑚 ℕ) ∩ 𝑅) → ℕ ⊆
(ℤ≥‘1)) |
39 | 9, 15, 35, 38 | sumss 14455 |
. 2
⊢ (𝐴 ∈ ((ℕ0
↑𝑚 ℕ) ∩ 𝑅) → Σ𝑘 ∈ (◡𝐴 “ ℕ)((𝐴‘𝑘) · 𝑘) = Σ𝑘 ∈ ℕ ((𝐴‘𝑘) · 𝑘)) |
40 | 3, 39 | eqtr4d 2659 |
1
⊢ (𝐴 ∈ ((ℕ0
↑𝑚 ℕ) ∩ 𝑅) → (𝑆‘𝐴) = Σ𝑘 ∈ (◡𝐴 “ ℕ)((𝐴‘𝑘) · 𝑘)) |