Step | Hyp | Ref
| Expression |
1 | | nnuz 12502 |
. . . 4
⊢ ℕ =
(ℤ≥‘1) |
2 | | 1zzd 12233 |
. . . 4
⊢ (⊤
→ 1 ∈ ℤ) |
3 | | 1cnd 10853 |
. . . . 5
⊢ (⊤
→ 1 ∈ ℂ) |
4 | | nnex 11861 |
. . . . . . 7
⊢ ℕ
∈ V |
5 | 4 | mptex 7058 |
. . . . . 6
⊢ (𝑛 ∈ ℕ ↦ (1 /
(𝑛 + 1))) ∈
V |
6 | 5 | a1i 11 |
. . . . 5
⊢ (⊤
→ (𝑛 ∈ ℕ
↦ (1 / (𝑛 + 1)))
∈ V) |
7 | | oveq1 7239 |
. . . . . . . 8
⊢ (𝑛 = 𝑘 → (𝑛 + 1) = (𝑘 + 1)) |
8 | 7 | oveq2d 7248 |
. . . . . . 7
⊢ (𝑛 = 𝑘 → (1 / (𝑛 + 1)) = (1 / (𝑘 + 1))) |
9 | | eqid 2738 |
. . . . . . 7
⊢ (𝑛 ∈ ℕ ↦ (1 /
(𝑛 + 1))) = (𝑛 ∈ ℕ ↦ (1 /
(𝑛 + 1))) |
10 | | ovex 7265 |
. . . . . . 7
⊢ (1 /
(𝑘 + 1)) ∈
V |
11 | 8, 9, 10 | fvmpt 6837 |
. . . . . 6
⊢ (𝑘 ∈ ℕ → ((𝑛 ∈ ℕ ↦ (1 /
(𝑛 + 1)))‘𝑘) = (1 / (𝑘 + 1))) |
12 | 11 | adantl 485 |
. . . . 5
⊢
((⊤ ∧ 𝑘
∈ ℕ) → ((𝑛
∈ ℕ ↦ (1 / (𝑛 + 1)))‘𝑘) = (1 / (𝑘 + 1))) |
13 | 1, 2, 3, 2, 6, 12 | divcnvshft 15447 |
. . . 4
⊢ (⊤
→ (𝑛 ∈ ℕ
↦ (1 / (𝑛 + 1)))
⇝ 0) |
14 | | seqex 13603 |
. . . . 5
⊢ seq1( + ,
𝐹) ∈
V |
15 | 14 | a1i 11 |
. . . 4
⊢ (⊤
→ seq1( + , 𝐹) ∈
V) |
16 | | peano2nn 11867 |
. . . . . . . 8
⊢ (𝑘 ∈ ℕ → (𝑘 + 1) ∈
ℕ) |
17 | 16 | adantl 485 |
. . . . . . 7
⊢
((⊤ ∧ 𝑘
∈ ℕ) → (𝑘 +
1) ∈ ℕ) |
18 | 17 | nnrecred 11906 |
. . . . . 6
⊢
((⊤ ∧ 𝑘
∈ ℕ) → (1 / (𝑘 + 1)) ∈ ℝ) |
19 | 18 | recnd 10886 |
. . . . 5
⊢
((⊤ ∧ 𝑘
∈ ℕ) → (1 / (𝑘 + 1)) ∈ ℂ) |
20 | 12, 19 | eqeltrd 2839 |
. . . 4
⊢
((⊤ ∧ 𝑘
∈ ℕ) → ((𝑛
∈ ℕ ↦ (1 / (𝑛 + 1)))‘𝑘) ∈ ℂ) |
21 | 12 | oveq2d 7248 |
. . . . 5
⊢
((⊤ ∧ 𝑘
∈ ℕ) → (1 − ((𝑛 ∈ ℕ ↦ (1 / (𝑛 + 1)))‘𝑘)) = (1 − (1 / (𝑘 + 1)))) |
22 | | elfznn 13166 |
. . . . . . . . . . . 12
⊢ (𝑗 ∈ (1...𝑘) → 𝑗 ∈ ℕ) |
23 | 22 | adantl 485 |
. . . . . . . . . . 11
⊢
(((⊤ ∧ 𝑘
∈ ℕ) ∧ 𝑗
∈ (1...𝑘)) →
𝑗 ∈
ℕ) |
24 | 23 | nncnd 11871 |
. . . . . . . . . 10
⊢
(((⊤ ∧ 𝑘
∈ ℕ) ∧ 𝑗
∈ (1...𝑘)) →
𝑗 ∈
ℂ) |
25 | | peano2cn 11029 |
. . . . . . . . . 10
⊢ (𝑗 ∈ ℂ → (𝑗 + 1) ∈
ℂ) |
26 | 24, 25 | syl 17 |
. . . . . . . . 9
⊢
(((⊤ ∧ 𝑘
∈ ℕ) ∧ 𝑗
∈ (1...𝑘)) →
(𝑗 + 1) ∈
ℂ) |
27 | | peano2nn 11867 |
. . . . . . . . . . . 12
⊢ (𝑗 ∈ ℕ → (𝑗 + 1) ∈
ℕ) |
28 | 23, 27 | syl 17 |
. . . . . . . . . . 11
⊢
(((⊤ ∧ 𝑘
∈ ℕ) ∧ 𝑗
∈ (1...𝑘)) →
(𝑗 + 1) ∈
ℕ) |
29 | 23, 28 | nnmulcld 11908 |
. . . . . . . . . 10
⊢
(((⊤ ∧ 𝑘
∈ ℕ) ∧ 𝑗
∈ (1...𝑘)) →
(𝑗 · (𝑗 + 1)) ∈
ℕ) |
30 | 29 | nncnd 11871 |
. . . . . . . . 9
⊢
(((⊤ ∧ 𝑘
∈ ℕ) ∧ 𝑗
∈ (1...𝑘)) →
(𝑗 · (𝑗 + 1)) ∈
ℂ) |
31 | 29 | nnne0d 11905 |
. . . . . . . . 9
⊢
(((⊤ ∧ 𝑘
∈ ℕ) ∧ 𝑗
∈ (1...𝑘)) →
(𝑗 · (𝑗 + 1)) ≠ 0) |
32 | 26, 24, 30, 31 | divsubdird 11672 |
. . . . . . . 8
⊢
(((⊤ ∧ 𝑘
∈ ℕ) ∧ 𝑗
∈ (1...𝑘)) →
(((𝑗 + 1) − 𝑗) / (𝑗 · (𝑗 + 1))) = (((𝑗 + 1) / (𝑗 · (𝑗 + 1))) − (𝑗 / (𝑗 · (𝑗 + 1))))) |
33 | | ax-1cn 10812 |
. . . . . . . . . 10
⊢ 1 ∈
ℂ |
34 | | pncan2 11110 |
. . . . . . . . . 10
⊢ ((𝑗 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝑗 + 1)
− 𝑗) =
1) |
35 | 24, 33, 34 | sylancl 589 |
. . . . . . . . 9
⊢
(((⊤ ∧ 𝑘
∈ ℕ) ∧ 𝑗
∈ (1...𝑘)) →
((𝑗 + 1) − 𝑗) = 1) |
36 | 35 | oveq1d 7247 |
. . . . . . . 8
⊢
(((⊤ ∧ 𝑘
∈ ℕ) ∧ 𝑗
∈ (1...𝑘)) →
(((𝑗 + 1) − 𝑗) / (𝑗 · (𝑗 + 1))) = (1 / (𝑗 · (𝑗 + 1)))) |
37 | 26 | mulid1d 10875 |
. . . . . . . . . . 11
⊢
(((⊤ ∧ 𝑘
∈ ℕ) ∧ 𝑗
∈ (1...𝑘)) →
((𝑗 + 1) · 1) =
(𝑗 + 1)) |
38 | 26, 24 | mulcomd 10879 |
. . . . . . . . . . 11
⊢
(((⊤ ∧ 𝑘
∈ ℕ) ∧ 𝑗
∈ (1...𝑘)) →
((𝑗 + 1) · 𝑗) = (𝑗 · (𝑗 + 1))) |
39 | 37, 38 | oveq12d 7250 |
. . . . . . . . . 10
⊢
(((⊤ ∧ 𝑘
∈ ℕ) ∧ 𝑗
∈ (1...𝑘)) →
(((𝑗 + 1) · 1) /
((𝑗 + 1) · 𝑗)) = ((𝑗 + 1) / (𝑗 · (𝑗 + 1)))) |
40 | | 1cnd 10853 |
. . . . . . . . . . 11
⊢
(((⊤ ∧ 𝑘
∈ ℕ) ∧ 𝑗
∈ (1...𝑘)) → 1
∈ ℂ) |
41 | 23 | nnne0d 11905 |
. . . . . . . . . . 11
⊢
(((⊤ ∧ 𝑘
∈ ℕ) ∧ 𝑗
∈ (1...𝑘)) →
𝑗 ≠ 0) |
42 | 28 | nnne0d 11905 |
. . . . . . . . . . 11
⊢
(((⊤ ∧ 𝑘
∈ ℕ) ∧ 𝑗
∈ (1...𝑘)) →
(𝑗 + 1) ≠
0) |
43 | 40, 24, 26, 41, 42 | divcan5d 11659 |
. . . . . . . . . 10
⊢
(((⊤ ∧ 𝑘
∈ ℕ) ∧ 𝑗
∈ (1...𝑘)) →
(((𝑗 + 1) · 1) /
((𝑗 + 1) · 𝑗)) = (1 / 𝑗)) |
44 | 39, 43 | eqtr3d 2780 |
. . . . . . . . 9
⊢
(((⊤ ∧ 𝑘
∈ ℕ) ∧ 𝑗
∈ (1...𝑘)) →
((𝑗 + 1) / (𝑗 · (𝑗 + 1))) = (1 / 𝑗)) |
45 | 24 | mulid1d 10875 |
. . . . . . . . . . 11
⊢
(((⊤ ∧ 𝑘
∈ ℕ) ∧ 𝑗
∈ (1...𝑘)) →
(𝑗 · 1) = 𝑗) |
46 | 45 | oveq1d 7247 |
. . . . . . . . . 10
⊢
(((⊤ ∧ 𝑘
∈ ℕ) ∧ 𝑗
∈ (1...𝑘)) →
((𝑗 · 1) / (𝑗 · (𝑗 + 1))) = (𝑗 / (𝑗 · (𝑗 + 1)))) |
47 | 40, 26, 24, 42, 41 | divcan5d 11659 |
. . . . . . . . . 10
⊢
(((⊤ ∧ 𝑘
∈ ℕ) ∧ 𝑗
∈ (1...𝑘)) →
((𝑗 · 1) / (𝑗 · (𝑗 + 1))) = (1 / (𝑗 + 1))) |
48 | 46, 47 | eqtr3d 2780 |
. . . . . . . . 9
⊢
(((⊤ ∧ 𝑘
∈ ℕ) ∧ 𝑗
∈ (1...𝑘)) →
(𝑗 / (𝑗 · (𝑗 + 1))) = (1 / (𝑗 + 1))) |
49 | 44, 48 | oveq12d 7250 |
. . . . . . . 8
⊢
(((⊤ ∧ 𝑘
∈ ℕ) ∧ 𝑗
∈ (1...𝑘)) →
(((𝑗 + 1) / (𝑗 · (𝑗 + 1))) − (𝑗 / (𝑗 · (𝑗 + 1)))) = ((1 / 𝑗) − (1 / (𝑗 + 1)))) |
50 | 32, 36, 49 | 3eqtr3d 2786 |
. . . . . . 7
⊢
(((⊤ ∧ 𝑘
∈ ℕ) ∧ 𝑗
∈ (1...𝑘)) → (1 /
(𝑗 · (𝑗 + 1))) = ((1 / 𝑗) − (1 / (𝑗 + 1)))) |
51 | 50 | sumeq2dv 15295 |
. . . . . 6
⊢
((⊤ ∧ 𝑘
∈ ℕ) → Σ𝑗 ∈ (1...𝑘)(1 / (𝑗 · (𝑗 + 1))) = Σ𝑗 ∈ (1...𝑘)((1 / 𝑗) − (1 / (𝑗 + 1)))) |
52 | | oveq2 7240 |
. . . . . . 7
⊢ (𝑛 = 𝑗 → (1 / 𝑛) = (1 / 𝑗)) |
53 | | oveq2 7240 |
. . . . . . 7
⊢ (𝑛 = (𝑗 + 1) → (1 / 𝑛) = (1 / (𝑗 + 1))) |
54 | | oveq2 7240 |
. . . . . . . 8
⊢ (𝑛 = 1 → (1 / 𝑛) = (1 / 1)) |
55 | | 1div1e1 11547 |
. . . . . . . 8
⊢ (1 / 1) =
1 |
56 | 54, 55 | eqtrdi 2795 |
. . . . . . 7
⊢ (𝑛 = 1 → (1 / 𝑛) = 1) |
57 | | oveq2 7240 |
. . . . . . 7
⊢ (𝑛 = (𝑘 + 1) → (1 / 𝑛) = (1 / (𝑘 + 1))) |
58 | | nnz 12224 |
. . . . . . . 8
⊢ (𝑘 ∈ ℕ → 𝑘 ∈
ℤ) |
59 | 58 | adantl 485 |
. . . . . . 7
⊢
((⊤ ∧ 𝑘
∈ ℕ) → 𝑘
∈ ℤ) |
60 | 17, 1 | eleqtrdi 2849 |
. . . . . . 7
⊢
((⊤ ∧ 𝑘
∈ ℕ) → (𝑘 +
1) ∈ (ℤ≥‘1)) |
61 | | elfznn 13166 |
. . . . . . . . . 10
⊢ (𝑛 ∈ (1...(𝑘 + 1)) → 𝑛 ∈ ℕ) |
62 | 61 | adantl 485 |
. . . . . . . . 9
⊢
(((⊤ ∧ 𝑘
∈ ℕ) ∧ 𝑛
∈ (1...(𝑘 + 1)))
→ 𝑛 ∈
ℕ) |
63 | 62 | nnrecred 11906 |
. . . . . . . 8
⊢
(((⊤ ∧ 𝑘
∈ ℕ) ∧ 𝑛
∈ (1...(𝑘 + 1)))
→ (1 / 𝑛) ∈
ℝ) |
64 | 63 | recnd 10886 |
. . . . . . 7
⊢
(((⊤ ∧ 𝑘
∈ ℕ) ∧ 𝑛
∈ (1...(𝑘 + 1)))
→ (1 / 𝑛) ∈
ℂ) |
65 | 52, 53, 56, 57, 59, 60, 64 | telfsum 15396 |
. . . . . 6
⊢
((⊤ ∧ 𝑘
∈ ℕ) → Σ𝑗 ∈ (1...𝑘)((1 / 𝑗) − (1 / (𝑗 + 1))) = (1 − (1 / (𝑘 + 1)))) |
66 | 51, 65 | eqtrd 2778 |
. . . . 5
⊢
((⊤ ∧ 𝑘
∈ ℕ) → Σ𝑗 ∈ (1...𝑘)(1 / (𝑗 · (𝑗 + 1))) = (1 − (1 / (𝑘 + 1)))) |
67 | | id 22 |
. . . . . . . . . 10
⊢ (𝑛 = 𝑗 → 𝑛 = 𝑗) |
68 | | oveq1 7239 |
. . . . . . . . . 10
⊢ (𝑛 = 𝑗 → (𝑛 + 1) = (𝑗 + 1)) |
69 | 67, 68 | oveq12d 7250 |
. . . . . . . . 9
⊢ (𝑛 = 𝑗 → (𝑛 · (𝑛 + 1)) = (𝑗 · (𝑗 + 1))) |
70 | 69 | oveq2d 7248 |
. . . . . . . 8
⊢ (𝑛 = 𝑗 → (1 / (𝑛 · (𝑛 + 1))) = (1 / (𝑗 · (𝑗 + 1)))) |
71 | | trireciplem.1 |
. . . . . . . 8
⊢ 𝐹 = (𝑛 ∈ ℕ ↦ (1 / (𝑛 · (𝑛 + 1)))) |
72 | | ovex 7265 |
. . . . . . . 8
⊢ (1 /
(𝑗 · (𝑗 + 1))) ∈
V |
73 | 70, 71, 72 | fvmpt 6837 |
. . . . . . 7
⊢ (𝑗 ∈ ℕ → (𝐹‘𝑗) = (1 / (𝑗 · (𝑗 + 1)))) |
74 | 23, 73 | syl 17 |
. . . . . 6
⊢
(((⊤ ∧ 𝑘
∈ ℕ) ∧ 𝑗
∈ (1...𝑘)) →
(𝐹‘𝑗) = (1 / (𝑗 · (𝑗 + 1)))) |
75 | | simpr 488 |
. . . . . . 7
⊢
((⊤ ∧ 𝑘
∈ ℕ) → 𝑘
∈ ℕ) |
76 | 75, 1 | eleqtrdi 2849 |
. . . . . 6
⊢
((⊤ ∧ 𝑘
∈ ℕ) → 𝑘
∈ (ℤ≥‘1)) |
77 | 29 | nnrecred 11906 |
. . . . . . 7
⊢
(((⊤ ∧ 𝑘
∈ ℕ) ∧ 𝑗
∈ (1...𝑘)) → (1 /
(𝑗 · (𝑗 + 1))) ∈
ℝ) |
78 | 77 | recnd 10886 |
. . . . . 6
⊢
(((⊤ ∧ 𝑘
∈ ℕ) ∧ 𝑗
∈ (1...𝑘)) → (1 /
(𝑗 · (𝑗 + 1))) ∈
ℂ) |
79 | 74, 76, 78 | fsumser 15322 |
. . . . 5
⊢
((⊤ ∧ 𝑘
∈ ℕ) → Σ𝑗 ∈ (1...𝑘)(1 / (𝑗 · (𝑗 + 1))) = (seq1( + , 𝐹)‘𝑘)) |
80 | 21, 66, 79 | 3eqtr2rd 2785 |
. . . 4
⊢
((⊤ ∧ 𝑘
∈ ℕ) → (seq1( + , 𝐹)‘𝑘) = (1 − ((𝑛 ∈ ℕ ↦ (1 / (𝑛 + 1)))‘𝑘))) |
81 | 1, 2, 13, 3, 15, 20, 80 | climsubc2 15228 |
. . 3
⊢ (⊤
→ seq1( + , 𝐹) ⇝
(1 − 0)) |
82 | 81 | mptru 1550 |
. 2
⊢ seq1( + ,
𝐹) ⇝ (1 −
0) |
83 | | 1m0e1 11976 |
. 2
⊢ (1
− 0) = 1 |
84 | 82, 83 | breqtri 5093 |
1
⊢ seq1( + ,
𝐹) ⇝
1 |