Proof of Theorem arisum2
| Step | Hyp | Ref
| Expression |
| 1 | | elnn0 12528 |
. 2
⊢ (𝑁 ∈ ℕ0
↔ (𝑁 ∈ ℕ
∨ 𝑁 =
0)) |
| 2 | | nnm1nn0 12567 |
. . . . . 6
⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈
ℕ0) |
| 3 | | nn0uz 12920 |
. . . . . 6
⊢
ℕ0 = (ℤ≥‘0) |
| 4 | 2, 3 | eleqtrdi 2851 |
. . . . 5
⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈
(ℤ≥‘0)) |
| 5 | | elfznn0 13660 |
. . . . . . 7
⊢ (𝑘 ∈ (0...(𝑁 − 1)) → 𝑘 ∈ ℕ0) |
| 6 | 5 | adantl 481 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (0...(𝑁 − 1))) → 𝑘 ∈ ℕ0) |
| 7 | 6 | nn0cnd 12589 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (0...(𝑁 − 1))) → 𝑘 ∈ ℂ) |
| 8 | | id 22 |
. . . . 5
⊢ (𝑘 = 0 → 𝑘 = 0) |
| 9 | 4, 7, 8 | fsum1p 15789 |
. . . 4
⊢ (𝑁 ∈ ℕ →
Σ𝑘 ∈ (0...(𝑁 − 1))𝑘 = (0 + Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))𝑘)) |
| 10 | | 1e0p1 12775 |
. . . . . . . . 9
⊢ 1 = (0 +
1) |
| 11 | 10 | oveq1i 7441 |
. . . . . . . 8
⊢
(1...(𝑁 − 1))
= ((0 + 1)...(𝑁 −
1)) |
| 12 | 11 | sumeq1i 15733 |
. . . . . . 7
⊢
Σ𝑘 ∈
(1...(𝑁 − 1))𝑘 = Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))𝑘 |
| 13 | 12 | oveq2i 7442 |
. . . . . 6
⊢ (0 +
Σ𝑘 ∈ (1...(𝑁 − 1))𝑘) = (0 + Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))𝑘) |
| 14 | | fzfid 14014 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ →
(1...(𝑁 − 1)) ∈
Fin) |
| 15 | | elfznn 13593 |
. . . . . . . . . 10
⊢ (𝑘 ∈ (1...(𝑁 − 1)) → 𝑘 ∈ ℕ) |
| 16 | 15 | adantl 481 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (1...(𝑁 − 1))) → 𝑘 ∈ ℕ) |
| 17 | 16 | nncnd 12282 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (1...(𝑁 − 1))) → 𝑘 ∈ ℂ) |
| 18 | 14, 17 | fsumcl 15769 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ →
Σ𝑘 ∈ (1...(𝑁 − 1))𝑘 ∈ ℂ) |
| 19 | 18 | addlidd 11462 |
. . . . . 6
⊢ (𝑁 ∈ ℕ → (0 +
Σ𝑘 ∈ (1...(𝑁 − 1))𝑘) = Σ𝑘 ∈ (1...(𝑁 − 1))𝑘) |
| 20 | 13, 19 | eqtr3id 2791 |
. . . . 5
⊢ (𝑁 ∈ ℕ → (0 +
Σ𝑘 ∈ ((0 +
1)...(𝑁 − 1))𝑘) = Σ𝑘 ∈ (1...(𝑁 − 1))𝑘) |
| 21 | | arisum 15896 |
. . . . . . 7
⊢ ((𝑁 − 1) ∈
ℕ0 → Σ𝑘 ∈ (1...(𝑁 − 1))𝑘 = ((((𝑁 − 1)↑2) + (𝑁 − 1)) / 2)) |
| 22 | 2, 21 | syl 17 |
. . . . . 6
⊢ (𝑁 ∈ ℕ →
Σ𝑘 ∈ (1...(𝑁 − 1))𝑘 = ((((𝑁 − 1)↑2) + (𝑁 − 1)) / 2)) |
| 23 | | nncn 12274 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℂ) |
| 24 | 23 | 2timesd 12509 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℕ → (2
· 𝑁) = (𝑁 + 𝑁)) |
| 25 | 24 | oveq2d 7447 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℕ → ((𝑁↑2) − (2 ·
𝑁)) = ((𝑁↑2) − (𝑁 + 𝑁))) |
| 26 | 23 | sqcld 14184 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℕ → (𝑁↑2) ∈
ℂ) |
| 27 | 26, 23, 23 | subsub4d 11651 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℕ → (((𝑁↑2) − 𝑁) − 𝑁) = ((𝑁↑2) − (𝑁 + 𝑁))) |
| 28 | 25, 27 | eqtr4d 2780 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ → ((𝑁↑2) − (2 ·
𝑁)) = (((𝑁↑2) − 𝑁) − 𝑁)) |
| 29 | 28 | oveq1d 7446 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ → (((𝑁↑2) − (2 ·
𝑁)) + 1) = ((((𝑁↑2) − 𝑁) − 𝑁) + 1)) |
| 30 | | binom2sub1 14260 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℂ → ((𝑁 − 1)↑2) = (((𝑁↑2) − (2 ·
𝑁)) + 1)) |
| 31 | 23, 30 | syl 17 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ → ((𝑁 − 1)↑2) = (((𝑁↑2) − (2 ·
𝑁)) + 1)) |
| 32 | 26, 23 | subcld 11620 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ → ((𝑁↑2) − 𝑁) ∈
ℂ) |
| 33 | | 1cnd 11256 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ → 1 ∈
ℂ) |
| 34 | 32, 23, 33 | subsubd 11648 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ → (((𝑁↑2) − 𝑁) − (𝑁 − 1)) = ((((𝑁↑2) − 𝑁) − 𝑁) + 1)) |
| 35 | 29, 31, 34 | 3eqtr4d 2787 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ → ((𝑁 − 1)↑2) = (((𝑁↑2) − 𝑁) − (𝑁 − 1))) |
| 36 | 35 | oveq1d 7446 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ → (((𝑁 − 1)↑2) + (𝑁 − 1)) = ((((𝑁↑2) − 𝑁) − (𝑁 − 1)) + (𝑁 − 1))) |
| 37 | | ax-1cn 11213 |
. . . . . . . . . 10
⊢ 1 ∈
ℂ |
| 38 | | subcl 11507 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℂ ∧ 1 ∈
ℂ) → (𝑁 −
1) ∈ ℂ) |
| 39 | 23, 37, 38 | sylancl 586 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈
ℂ) |
| 40 | 32, 39 | npcand 11624 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ → ((((𝑁↑2) − 𝑁) − (𝑁 − 1)) + (𝑁 − 1)) = ((𝑁↑2) − 𝑁)) |
| 41 | 36, 40 | eqtrd 2777 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ → (((𝑁 − 1)↑2) + (𝑁 − 1)) = ((𝑁↑2) − 𝑁)) |
| 42 | 41 | oveq1d 7446 |
. . . . . 6
⊢ (𝑁 ∈ ℕ → ((((𝑁 − 1)↑2) + (𝑁 − 1)) / 2) = (((𝑁↑2) − 𝑁) / 2)) |
| 43 | 22, 42 | eqtrd 2777 |
. . . . 5
⊢ (𝑁 ∈ ℕ →
Σ𝑘 ∈ (1...(𝑁 − 1))𝑘 = (((𝑁↑2) − 𝑁) / 2)) |
| 44 | 20, 43 | eqtrd 2777 |
. . . 4
⊢ (𝑁 ∈ ℕ → (0 +
Σ𝑘 ∈ ((0 +
1)...(𝑁 − 1))𝑘) = (((𝑁↑2) − 𝑁) / 2)) |
| 45 | 9, 44 | eqtrd 2777 |
. . 3
⊢ (𝑁 ∈ ℕ →
Σ𝑘 ∈ (0...(𝑁 − 1))𝑘 = (((𝑁↑2) − 𝑁) / 2)) |
| 46 | | oveq1 7438 |
. . . . . . . 8
⊢ (𝑁 = 0 → (𝑁 − 1) = (0 −
1)) |
| 47 | 46 | oveq2d 7447 |
. . . . . . 7
⊢ (𝑁 = 0 → (0...(𝑁 − 1)) = (0...(0 −
1))) |
| 48 | | 0re 11263 |
. . . . . . . . 9
⊢ 0 ∈
ℝ |
| 49 | | ltm1 12109 |
. . . . . . . . 9
⊢ (0 ∈
ℝ → (0 − 1) < 0) |
| 50 | 48, 49 | ax-mp 5 |
. . . . . . . 8
⊢ (0
− 1) < 0 |
| 51 | | 0z 12624 |
. . . . . . . . 9
⊢ 0 ∈
ℤ |
| 52 | | peano2zm 12660 |
. . . . . . . . . 10
⊢ (0 ∈
ℤ → (0 − 1) ∈ ℤ) |
| 53 | 51, 52 | ax-mp 5 |
. . . . . . . . 9
⊢ (0
− 1) ∈ ℤ |
| 54 | | fzn 13580 |
. . . . . . . . 9
⊢ ((0
∈ ℤ ∧ (0 − 1) ∈ ℤ) → ((0 − 1) < 0
↔ (0...(0 − 1)) = ∅)) |
| 55 | 51, 53, 54 | mp2an 692 |
. . . . . . . 8
⊢ ((0
− 1) < 0 ↔ (0...(0 − 1)) = ∅) |
| 56 | 50, 55 | mpbi 230 |
. . . . . . 7
⊢ (0...(0
− 1)) = ∅ |
| 57 | 47, 56 | eqtrdi 2793 |
. . . . . 6
⊢ (𝑁 = 0 → (0...(𝑁 − 1)) =
∅) |
| 58 | 57 | sumeq1d 15736 |
. . . . 5
⊢ (𝑁 = 0 → Σ𝑘 ∈ (0...(𝑁 − 1))𝑘 = Σ𝑘 ∈ ∅ 𝑘) |
| 59 | | sum0 15757 |
. . . . 5
⊢
Σ𝑘 ∈
∅ 𝑘 =
0 |
| 60 | 58, 59 | eqtrdi 2793 |
. . . 4
⊢ (𝑁 = 0 → Σ𝑘 ∈ (0...(𝑁 − 1))𝑘 = 0) |
| 61 | | sq0i 14232 |
. . . . . . . 8
⊢ (𝑁 = 0 → (𝑁↑2) = 0) |
| 62 | | id 22 |
. . . . . . . 8
⊢ (𝑁 = 0 → 𝑁 = 0) |
| 63 | 61, 62 | oveq12d 7449 |
. . . . . . 7
⊢ (𝑁 = 0 → ((𝑁↑2) − 𝑁) = (0 − 0)) |
| 64 | | 0m0e0 12386 |
. . . . . . 7
⊢ (0
− 0) = 0 |
| 65 | 63, 64 | eqtrdi 2793 |
. . . . . 6
⊢ (𝑁 = 0 → ((𝑁↑2) − 𝑁) = 0) |
| 66 | 65 | oveq1d 7446 |
. . . . 5
⊢ (𝑁 = 0 → (((𝑁↑2) − 𝑁) / 2) = (0 / 2)) |
| 67 | | 2cn 12341 |
. . . . . 6
⊢ 2 ∈
ℂ |
| 68 | | 2ne0 12370 |
. . . . . 6
⊢ 2 ≠
0 |
| 69 | 67, 68 | div0i 12001 |
. . . . 5
⊢ (0 / 2) =
0 |
| 70 | 66, 69 | eqtrdi 2793 |
. . . 4
⊢ (𝑁 = 0 → (((𝑁↑2) − 𝑁) / 2) = 0) |
| 71 | 60, 70 | eqtr4d 2780 |
. . 3
⊢ (𝑁 = 0 → Σ𝑘 ∈ (0...(𝑁 − 1))𝑘 = (((𝑁↑2) − 𝑁) / 2)) |
| 72 | 45, 71 | jaoi 858 |
. 2
⊢ ((𝑁 ∈ ℕ ∨ 𝑁 = 0) → Σ𝑘 ∈ (0...(𝑁 − 1))𝑘 = (((𝑁↑2) − 𝑁) / 2)) |
| 73 | 1, 72 | sylbi 217 |
1
⊢ (𝑁 ∈ ℕ0
→ Σ𝑘 ∈
(0...(𝑁 − 1))𝑘 = (((𝑁↑2) − 𝑁) / 2)) |