Proof of Theorem arisum2
Step | Hyp | Ref
| Expression |
1 | | elnn0 9137 |
. 2
⊢ (𝑁 ∈ ℕ0
↔ (𝑁 ∈ ℕ
∨ 𝑁 =
0)) |
2 | | nnm1nn0 9176 |
. . . . . 6
⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈
ℕ0) |
3 | | nn0uz 9521 |
. . . . . 6
⊢
ℕ0 = (ℤ≥‘0) |
4 | 2, 3 | eleqtrdi 2263 |
. . . . 5
⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈
(ℤ≥‘0)) |
5 | | elfznn0 10070 |
. . . . . . 7
⊢ (𝑘 ∈ (0...(𝑁 − 1)) → 𝑘 ∈ ℕ0) |
6 | 5 | adantl 275 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (0...(𝑁 − 1))) → 𝑘 ∈ ℕ0) |
7 | 6 | nn0cnd 9190 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (0...(𝑁 − 1))) → 𝑘 ∈ ℂ) |
8 | | id 19 |
. . . . 5
⊢ (𝑘 = 0 → 𝑘 = 0) |
9 | 4, 7, 8 | fsum1p 11381 |
. . . 4
⊢ (𝑁 ∈ ℕ →
Σ𝑘 ∈ (0...(𝑁 − 1))𝑘 = (0 + Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))𝑘)) |
10 | | 1e0p1 9384 |
. . . . . . . . 9
⊢ 1 = (0 +
1) |
11 | 10 | oveq1i 5863 |
. . . . . . . 8
⊢
(1...(𝑁 − 1))
= ((0 + 1)...(𝑁 −
1)) |
12 | 11 | sumeq1i 11326 |
. . . . . . 7
⊢
Σ𝑘 ∈
(1...(𝑁 − 1))𝑘 = Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))𝑘 |
13 | 12 | oveq2i 5864 |
. . . . . 6
⊢ (0 +
Σ𝑘 ∈ (1...(𝑁 − 1))𝑘) = (0 + Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))𝑘) |
14 | | 1zzd 9239 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ → 1 ∈
ℤ) |
15 | 2 | nn0zd 9332 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈
ℤ) |
16 | 14, 15 | fzfigd 10387 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ →
(1...(𝑁 − 1)) ∈
Fin) |
17 | | elfznn 10010 |
. . . . . . . . . 10
⊢ (𝑘 ∈ (1...(𝑁 − 1)) → 𝑘 ∈ ℕ) |
18 | 17 | adantl 275 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (1...(𝑁 − 1))) → 𝑘 ∈ ℕ) |
19 | 18 | nncnd 8892 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (1...(𝑁 − 1))) → 𝑘 ∈ ℂ) |
20 | 16, 19 | fsumcl 11363 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ →
Σ𝑘 ∈ (1...(𝑁 − 1))𝑘 ∈ ℂ) |
21 | 20 | addid2d 8069 |
. . . . . 6
⊢ (𝑁 ∈ ℕ → (0 +
Σ𝑘 ∈ (1...(𝑁 − 1))𝑘) = Σ𝑘 ∈ (1...(𝑁 − 1))𝑘) |
22 | 13, 21 | eqtr3id 2217 |
. . . . 5
⊢ (𝑁 ∈ ℕ → (0 +
Σ𝑘 ∈ ((0 +
1)...(𝑁 − 1))𝑘) = Σ𝑘 ∈ (1...(𝑁 − 1))𝑘) |
23 | | arisum 11461 |
. . . . . . 7
⊢ ((𝑁 − 1) ∈
ℕ0 → Σ𝑘 ∈ (1...(𝑁 − 1))𝑘 = ((((𝑁 − 1)↑2) + (𝑁 − 1)) / 2)) |
24 | 2, 23 | syl 14 |
. . . . . 6
⊢ (𝑁 ∈ ℕ →
Σ𝑘 ∈ (1...(𝑁 − 1))𝑘 = ((((𝑁 − 1)↑2) + (𝑁 − 1)) / 2)) |
25 | | nncn 8886 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℂ) |
26 | 25 | 2timesd 9120 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℕ → (2
· 𝑁) = (𝑁 + 𝑁)) |
27 | 26 | oveq2d 5869 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℕ → ((𝑁↑2) − (2 ·
𝑁)) = ((𝑁↑2) − (𝑁 + 𝑁))) |
28 | 25 | sqcld 10607 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℕ → (𝑁↑2) ∈
ℂ) |
29 | 28, 25, 25 | subsub4d 8261 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℕ → (((𝑁↑2) − 𝑁) − 𝑁) = ((𝑁↑2) − (𝑁 + 𝑁))) |
30 | 27, 29 | eqtr4d 2206 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ → ((𝑁↑2) − (2 ·
𝑁)) = (((𝑁↑2) − 𝑁) − 𝑁)) |
31 | 30 | oveq1d 5868 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ → (((𝑁↑2) − (2 ·
𝑁)) + 1) = ((((𝑁↑2) − 𝑁) − 𝑁) + 1)) |
32 | | binom2sub1 10590 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℂ → ((𝑁 − 1)↑2) = (((𝑁↑2) − (2 ·
𝑁)) + 1)) |
33 | 25, 32 | syl 14 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ → ((𝑁 − 1)↑2) = (((𝑁↑2) − (2 ·
𝑁)) + 1)) |
34 | 28, 25 | subcld 8230 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ → ((𝑁↑2) − 𝑁) ∈
ℂ) |
35 | | 1cnd 7936 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ → 1 ∈
ℂ) |
36 | 34, 25, 35 | subsubd 8258 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ → (((𝑁↑2) − 𝑁) − (𝑁 − 1)) = ((((𝑁↑2) − 𝑁) − 𝑁) + 1)) |
37 | 31, 33, 36 | 3eqtr4d 2213 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ → ((𝑁 − 1)↑2) = (((𝑁↑2) − 𝑁) − (𝑁 − 1))) |
38 | 37 | oveq1d 5868 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ → (((𝑁 − 1)↑2) + (𝑁 − 1)) = ((((𝑁↑2) − 𝑁) − (𝑁 − 1)) + (𝑁 − 1))) |
39 | | ax-1cn 7867 |
. . . . . . . . . 10
⊢ 1 ∈
ℂ |
40 | | subcl 8118 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℂ ∧ 1 ∈
ℂ) → (𝑁 −
1) ∈ ℂ) |
41 | 25, 39, 40 | sylancl 411 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈
ℂ) |
42 | 34, 41 | npcand 8234 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ → ((((𝑁↑2) − 𝑁) − (𝑁 − 1)) + (𝑁 − 1)) = ((𝑁↑2) − 𝑁)) |
43 | 38, 42 | eqtrd 2203 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ → (((𝑁 − 1)↑2) + (𝑁 − 1)) = ((𝑁↑2) − 𝑁)) |
44 | 43 | oveq1d 5868 |
. . . . . 6
⊢ (𝑁 ∈ ℕ → ((((𝑁 − 1)↑2) + (𝑁 − 1)) / 2) = (((𝑁↑2) − 𝑁) / 2)) |
45 | 24, 44 | eqtrd 2203 |
. . . . 5
⊢ (𝑁 ∈ ℕ →
Σ𝑘 ∈ (1...(𝑁 − 1))𝑘 = (((𝑁↑2) − 𝑁) / 2)) |
46 | 22, 45 | eqtrd 2203 |
. . . 4
⊢ (𝑁 ∈ ℕ → (0 +
Σ𝑘 ∈ ((0 +
1)...(𝑁 − 1))𝑘) = (((𝑁↑2) − 𝑁) / 2)) |
47 | 9, 46 | eqtrd 2203 |
. . 3
⊢ (𝑁 ∈ ℕ →
Σ𝑘 ∈ (0...(𝑁 − 1))𝑘 = (((𝑁↑2) − 𝑁) / 2)) |
48 | | oveq1 5860 |
. . . . . . . 8
⊢ (𝑁 = 0 → (𝑁 − 1) = (0 −
1)) |
49 | 48 | oveq2d 5869 |
. . . . . . 7
⊢ (𝑁 = 0 → (0...(𝑁 − 1)) = (0...(0 −
1))) |
50 | | 0re 7920 |
. . . . . . . . 9
⊢ 0 ∈
ℝ |
51 | | ltm1 8762 |
. . . . . . . . 9
⊢ (0 ∈
ℝ → (0 − 1) < 0) |
52 | 50, 51 | ax-mp 5 |
. . . . . . . 8
⊢ (0
− 1) < 0 |
53 | | 0z 9223 |
. . . . . . . . 9
⊢ 0 ∈
ℤ |
54 | | peano2zm 9250 |
. . . . . . . . . 10
⊢ (0 ∈
ℤ → (0 − 1) ∈ ℤ) |
55 | 53, 54 | ax-mp 5 |
. . . . . . . . 9
⊢ (0
− 1) ∈ ℤ |
56 | | fzn 9998 |
. . . . . . . . 9
⊢ ((0
∈ ℤ ∧ (0 − 1) ∈ ℤ) → ((0 − 1) < 0
↔ (0...(0 − 1)) = ∅)) |
57 | 53, 55, 56 | mp2an 424 |
. . . . . . . 8
⊢ ((0
− 1) < 0 ↔ (0...(0 − 1)) = ∅) |
58 | 52, 57 | mpbi 144 |
. . . . . . 7
⊢ (0...(0
− 1)) = ∅ |
59 | 49, 58 | eqtrdi 2219 |
. . . . . 6
⊢ (𝑁 = 0 → (0...(𝑁 − 1)) =
∅) |
60 | 59 | sumeq1d 11329 |
. . . . 5
⊢ (𝑁 = 0 → Σ𝑘 ∈ (0...(𝑁 − 1))𝑘 = Σ𝑘 ∈ ∅ 𝑘) |
61 | | sum0 11351 |
. . . . 5
⊢
Σ𝑘 ∈
∅ 𝑘 =
0 |
62 | 60, 61 | eqtrdi 2219 |
. . . 4
⊢ (𝑁 = 0 → Σ𝑘 ∈ (0...(𝑁 − 1))𝑘 = 0) |
63 | | sq0i 10567 |
. . . . . . . 8
⊢ (𝑁 = 0 → (𝑁↑2) = 0) |
64 | | id 19 |
. . . . . . . 8
⊢ (𝑁 = 0 → 𝑁 = 0) |
65 | 63, 64 | oveq12d 5871 |
. . . . . . 7
⊢ (𝑁 = 0 → ((𝑁↑2) − 𝑁) = (0 − 0)) |
66 | | 0m0e0 8990 |
. . . . . . 7
⊢ (0
− 0) = 0 |
67 | 65, 66 | eqtrdi 2219 |
. . . . . 6
⊢ (𝑁 = 0 → ((𝑁↑2) − 𝑁) = 0) |
68 | 67 | oveq1d 5868 |
. . . . 5
⊢ (𝑁 = 0 → (((𝑁↑2) − 𝑁) / 2) = (0 / 2)) |
69 | | 2cn 8949 |
. . . . . 6
⊢ 2 ∈
ℂ |
70 | | 2ap0 8971 |
. . . . . 6
⊢ 2 #
0 |
71 | 69, 70 | div0api 8663 |
. . . . 5
⊢ (0 / 2) =
0 |
72 | 68, 71 | eqtrdi 2219 |
. . . 4
⊢ (𝑁 = 0 → (((𝑁↑2) − 𝑁) / 2) = 0) |
73 | 62, 72 | eqtr4d 2206 |
. . 3
⊢ (𝑁 = 0 → Σ𝑘 ∈ (0...(𝑁 − 1))𝑘 = (((𝑁↑2) − 𝑁) / 2)) |
74 | 47, 73 | jaoi 711 |
. 2
⊢ ((𝑁 ∈ ℕ ∨ 𝑁 = 0) → Σ𝑘 ∈ (0...(𝑁 − 1))𝑘 = (((𝑁↑2) − 𝑁) / 2)) |
75 | 1, 74 | sylbi 120 |
1
⊢ (𝑁 ∈ ℕ0
→ Σ𝑘 ∈
(0...(𝑁 − 1))𝑘 = (((𝑁↑2) − 𝑁) / 2)) |