Step | Hyp | Ref
| Expression |
1 | | nnuz 9522 |
. . . 4
⊢ ℕ =
(ℤ≥‘1) |
2 | | 1zzd 9239 |
. . . 4
⊢ (⊤
→ 1 ∈ ℤ) |
3 | | 1cnd 7936 |
. . . . . 6
⊢ (⊤
→ 1 ∈ ℂ) |
4 | | divcnv 11460 |
. . . . . 6
⊢ (1 ∈
ℂ → (𝑛 ∈
ℕ ↦ (1 / 𝑛))
⇝ 0) |
5 | 3, 4 | syl 14 |
. . . . 5
⊢ (⊤
→ (𝑛 ∈ ℕ
↦ (1 / 𝑛)) ⇝
0) |
6 | | nnex 8884 |
. . . . . . . 8
⊢ ℕ
∈ V |
7 | 6 | mptex 5722 |
. . . . . . 7
⊢ (𝑛 ∈ ℕ ↦ (1 /
(𝑛 + 1))) ∈
V |
8 | 7 | a1i 9 |
. . . . . 6
⊢ (⊤
→ (𝑛 ∈ ℕ
↦ (1 / (𝑛 + 1)))
∈ V) |
9 | 6 | mptex 5722 |
. . . . . . 7
⊢ (𝑛 ∈ ℕ ↦ (1 /
𝑛)) ∈
V |
10 | 9 | a1i 9 |
. . . . . 6
⊢ (⊤
→ (𝑛 ∈ ℕ
↦ (1 / 𝑛)) ∈
V) |
11 | | peano2nn 8890 |
. . . . . . . . 9
⊢ (𝑘 ∈ ℕ → (𝑘 + 1) ∈
ℕ) |
12 | 11 | adantl 275 |
. . . . . . . 8
⊢
((⊤ ∧ 𝑘
∈ ℕ) → (𝑘 +
1) ∈ ℕ) |
13 | 12 | nnrecred 8925 |
. . . . . . . 8
⊢
((⊤ ∧ 𝑘
∈ ℕ) → (1 / (𝑘 + 1)) ∈ ℝ) |
14 | | oveq2 5861 |
. . . . . . . . 9
⊢ (𝑛 = (𝑘 + 1) → (1 / 𝑛) = (1 / (𝑘 + 1))) |
15 | | eqid 2170 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ ↦ (1 /
𝑛)) = (𝑛 ∈ ℕ ↦ (1 / 𝑛)) |
16 | 14, 15 | fvmptg 5572 |
. . . . . . . 8
⊢ (((𝑘 + 1) ∈ ℕ ∧ (1 /
(𝑘 + 1)) ∈ ℝ)
→ ((𝑛 ∈ ℕ
↦ (1 / 𝑛))‘(𝑘 + 1)) = (1 / (𝑘 + 1))) |
17 | 12, 13, 16 | syl2anc 409 |
. . . . . . 7
⊢
((⊤ ∧ 𝑘
∈ ℕ) → ((𝑛
∈ ℕ ↦ (1 / 𝑛))‘(𝑘 + 1)) = (1 / (𝑘 + 1))) |
18 | | simpr 109 |
. . . . . . . 8
⊢
((⊤ ∧ 𝑘
∈ ℕ) → 𝑘
∈ ℕ) |
19 | | oveq1 5860 |
. . . . . . . . . 10
⊢ (𝑛 = 𝑘 → (𝑛 + 1) = (𝑘 + 1)) |
20 | 19 | oveq2d 5869 |
. . . . . . . . 9
⊢ (𝑛 = 𝑘 → (1 / (𝑛 + 1)) = (1 / (𝑘 + 1))) |
21 | | eqid 2170 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ ↦ (1 /
(𝑛 + 1))) = (𝑛 ∈ ℕ ↦ (1 /
(𝑛 + 1))) |
22 | 20, 21 | fvmptg 5572 |
. . . . . . . 8
⊢ ((𝑘 ∈ ℕ ∧ (1 /
(𝑘 + 1)) ∈ ℝ)
→ ((𝑛 ∈ ℕ
↦ (1 / (𝑛 +
1)))‘𝑘) = (1 / (𝑘 + 1))) |
23 | 18, 13, 22 | syl2anc 409 |
. . . . . . 7
⊢
((⊤ ∧ 𝑘
∈ ℕ) → ((𝑛
∈ ℕ ↦ (1 / (𝑛 + 1)))‘𝑘) = (1 / (𝑘 + 1))) |
24 | 17, 23 | eqtr4d 2206 |
. . . . . 6
⊢
((⊤ ∧ 𝑘
∈ ℕ) → ((𝑛
∈ ℕ ↦ (1 / 𝑛))‘(𝑘 + 1)) = ((𝑛 ∈ ℕ ↦ (1 / (𝑛 + 1)))‘𝑘)) |
25 | 1, 2, 2, 8, 10, 24 | climshft2 11269 |
. . . . 5
⊢ (⊤
→ ((𝑛 ∈ ℕ
↦ (1 / (𝑛 + 1)))
⇝ 0 ↔ (𝑛 ∈
ℕ ↦ (1 / 𝑛))
⇝ 0)) |
26 | 5, 25 | mpbird 166 |
. . . 4
⊢ (⊤
→ (𝑛 ∈ ℕ
↦ (1 / (𝑛 + 1)))
⇝ 0) |
27 | | seqex 10403 |
. . . . 5
⊢ seq1( + ,
𝐹) ∈
V |
28 | 27 | a1i 9 |
. . . 4
⊢ (⊤
→ seq1( + , 𝐹) ∈
V) |
29 | 13 | recnd 7948 |
. . . . 5
⊢
((⊤ ∧ 𝑘
∈ ℕ) → (1 / (𝑘 + 1)) ∈ ℂ) |
30 | 23, 29 | eqeltrd 2247 |
. . . 4
⊢
((⊤ ∧ 𝑘
∈ ℕ) → ((𝑛
∈ ℕ ↦ (1 / (𝑛 + 1)))‘𝑘) ∈ ℂ) |
31 | 23 | oveq2d 5869 |
. . . . 5
⊢
((⊤ ∧ 𝑘
∈ ℕ) → (1 − ((𝑛 ∈ ℕ ↦ (1 / (𝑛 + 1)))‘𝑘)) = (1 − (1 / (𝑘 + 1)))) |
32 | | elfznn 10010 |
. . . . . . . . . . . 12
⊢ (𝑗 ∈ (1...𝑘) → 𝑗 ∈ ℕ) |
33 | 32 | adantl 275 |
. . . . . . . . . . 11
⊢
(((⊤ ∧ 𝑘
∈ ℕ) ∧ 𝑗
∈ (1...𝑘)) →
𝑗 ∈
ℕ) |
34 | 33 | nncnd 8892 |
. . . . . . . . . 10
⊢
(((⊤ ∧ 𝑘
∈ ℕ) ∧ 𝑗
∈ (1...𝑘)) →
𝑗 ∈
ℂ) |
35 | | peano2cn 8054 |
. . . . . . . . . 10
⊢ (𝑗 ∈ ℂ → (𝑗 + 1) ∈
ℂ) |
36 | 34, 35 | syl 14 |
. . . . . . . . 9
⊢
(((⊤ ∧ 𝑘
∈ ℕ) ∧ 𝑗
∈ (1...𝑘)) →
(𝑗 + 1) ∈
ℂ) |
37 | | peano2nn 8890 |
. . . . . . . . . . . 12
⊢ (𝑗 ∈ ℕ → (𝑗 + 1) ∈
ℕ) |
38 | 33, 37 | syl 14 |
. . . . . . . . . . 11
⊢
(((⊤ ∧ 𝑘
∈ ℕ) ∧ 𝑗
∈ (1...𝑘)) →
(𝑗 + 1) ∈
ℕ) |
39 | 33, 38 | nnmulcld 8927 |
. . . . . . . . . 10
⊢
(((⊤ ∧ 𝑘
∈ ℕ) ∧ 𝑗
∈ (1...𝑘)) →
(𝑗 · (𝑗 + 1)) ∈
ℕ) |
40 | 39 | nncnd 8892 |
. . . . . . . . 9
⊢
(((⊤ ∧ 𝑘
∈ ℕ) ∧ 𝑗
∈ (1...𝑘)) →
(𝑗 · (𝑗 + 1)) ∈
ℂ) |
41 | 39 | nnap0d 8924 |
. . . . . . . . 9
⊢
(((⊤ ∧ 𝑘
∈ ℕ) ∧ 𝑗
∈ (1...𝑘)) →
(𝑗 · (𝑗 + 1)) # 0) |
42 | 36, 34, 40, 41 | divsubdirapd 8747 |
. . . . . . . 8
⊢
(((⊤ ∧ 𝑘
∈ ℕ) ∧ 𝑗
∈ (1...𝑘)) →
(((𝑗 + 1) − 𝑗) / (𝑗 · (𝑗 + 1))) = (((𝑗 + 1) / (𝑗 · (𝑗 + 1))) − (𝑗 / (𝑗 · (𝑗 + 1))))) |
43 | | ax-1cn 7867 |
. . . . . . . . . 10
⊢ 1 ∈
ℂ |
44 | | pncan2 8126 |
. . . . . . . . . 10
⊢ ((𝑗 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝑗 + 1)
− 𝑗) =
1) |
45 | 34, 43, 44 | sylancl 411 |
. . . . . . . . 9
⊢
(((⊤ ∧ 𝑘
∈ ℕ) ∧ 𝑗
∈ (1...𝑘)) →
((𝑗 + 1) − 𝑗) = 1) |
46 | 45 | oveq1d 5868 |
. . . . . . . 8
⊢
(((⊤ ∧ 𝑘
∈ ℕ) ∧ 𝑗
∈ (1...𝑘)) →
(((𝑗 + 1) − 𝑗) / (𝑗 · (𝑗 + 1))) = (1 / (𝑗 · (𝑗 + 1)))) |
47 | 36 | mulid1d 7937 |
. . . . . . . . . . 11
⊢
(((⊤ ∧ 𝑘
∈ ℕ) ∧ 𝑗
∈ (1...𝑘)) →
((𝑗 + 1) · 1) =
(𝑗 + 1)) |
48 | 36, 34 | mulcomd 7941 |
. . . . . . . . . . 11
⊢
(((⊤ ∧ 𝑘
∈ ℕ) ∧ 𝑗
∈ (1...𝑘)) →
((𝑗 + 1) · 𝑗) = (𝑗 · (𝑗 + 1))) |
49 | 47, 48 | oveq12d 5871 |
. . . . . . . . . 10
⊢
(((⊤ ∧ 𝑘
∈ ℕ) ∧ 𝑗
∈ (1...𝑘)) →
(((𝑗 + 1) · 1) /
((𝑗 + 1) · 𝑗)) = ((𝑗 + 1) / (𝑗 · (𝑗 + 1)))) |
50 | | 1cnd 7936 |
. . . . . . . . . . 11
⊢
(((⊤ ∧ 𝑘
∈ ℕ) ∧ 𝑗
∈ (1...𝑘)) → 1
∈ ℂ) |
51 | 33 | nnap0d 8924 |
. . . . . . . . . . 11
⊢
(((⊤ ∧ 𝑘
∈ ℕ) ∧ 𝑗
∈ (1...𝑘)) →
𝑗 # 0) |
52 | 38 | nnap0d 8924 |
. . . . . . . . . . 11
⊢
(((⊤ ∧ 𝑘
∈ ℕ) ∧ 𝑗
∈ (1...𝑘)) →
(𝑗 + 1) #
0) |
53 | 50, 34, 36, 51, 52 | divcanap5d 8734 |
. . . . . . . . . 10
⊢
(((⊤ ∧ 𝑘
∈ ℕ) ∧ 𝑗
∈ (1...𝑘)) →
(((𝑗 + 1) · 1) /
((𝑗 + 1) · 𝑗)) = (1 / 𝑗)) |
54 | 49, 53 | eqtr3d 2205 |
. . . . . . . . 9
⊢
(((⊤ ∧ 𝑘
∈ ℕ) ∧ 𝑗
∈ (1...𝑘)) →
((𝑗 + 1) / (𝑗 · (𝑗 + 1))) = (1 / 𝑗)) |
55 | 34 | mulid1d 7937 |
. . . . . . . . . . 11
⊢
(((⊤ ∧ 𝑘
∈ ℕ) ∧ 𝑗
∈ (1...𝑘)) →
(𝑗 · 1) = 𝑗) |
56 | 55 | oveq1d 5868 |
. . . . . . . . . 10
⊢
(((⊤ ∧ 𝑘
∈ ℕ) ∧ 𝑗
∈ (1...𝑘)) →
((𝑗 · 1) / (𝑗 · (𝑗 + 1))) = (𝑗 / (𝑗 · (𝑗 + 1)))) |
57 | 50, 36, 34, 52, 51 | divcanap5d 8734 |
. . . . . . . . . 10
⊢
(((⊤ ∧ 𝑘
∈ ℕ) ∧ 𝑗
∈ (1...𝑘)) →
((𝑗 · 1) / (𝑗 · (𝑗 + 1))) = (1 / (𝑗 + 1))) |
58 | 56, 57 | eqtr3d 2205 |
. . . . . . . . 9
⊢
(((⊤ ∧ 𝑘
∈ ℕ) ∧ 𝑗
∈ (1...𝑘)) →
(𝑗 / (𝑗 · (𝑗 + 1))) = (1 / (𝑗 + 1))) |
59 | 54, 58 | oveq12d 5871 |
. . . . . . . 8
⊢
(((⊤ ∧ 𝑘
∈ ℕ) ∧ 𝑗
∈ (1...𝑘)) →
(((𝑗 + 1) / (𝑗 · (𝑗 + 1))) − (𝑗 / (𝑗 · (𝑗 + 1)))) = ((1 / 𝑗) − (1 / (𝑗 + 1)))) |
60 | 42, 46, 59 | 3eqtr3d 2211 |
. . . . . . 7
⊢
(((⊤ ∧ 𝑘
∈ ℕ) ∧ 𝑗
∈ (1...𝑘)) → (1 /
(𝑗 · (𝑗 + 1))) = ((1 / 𝑗) − (1 / (𝑗 + 1)))) |
61 | 60 | sumeq2dv 11331 |
. . . . . 6
⊢
((⊤ ∧ 𝑘
∈ ℕ) → Σ𝑗 ∈ (1...𝑘)(1 / (𝑗 · (𝑗 + 1))) = Σ𝑗 ∈ (1...𝑘)((1 / 𝑗) − (1 / (𝑗 + 1)))) |
62 | | oveq2 5861 |
. . . . . . 7
⊢ (𝑛 = 𝑗 → (1 / 𝑛) = (1 / 𝑗)) |
63 | | oveq2 5861 |
. . . . . . 7
⊢ (𝑛 = (𝑗 + 1) → (1 / 𝑛) = (1 / (𝑗 + 1))) |
64 | | oveq2 5861 |
. . . . . . . 8
⊢ (𝑛 = 1 → (1 / 𝑛) = (1 / 1)) |
65 | | 1div1e1 8621 |
. . . . . . . 8
⊢ (1 / 1) =
1 |
66 | 64, 65 | eqtrdi 2219 |
. . . . . . 7
⊢ (𝑛 = 1 → (1 / 𝑛) = 1) |
67 | | nnz 9231 |
. . . . . . . 8
⊢ (𝑘 ∈ ℕ → 𝑘 ∈
ℤ) |
68 | 67 | adantl 275 |
. . . . . . 7
⊢
((⊤ ∧ 𝑘
∈ ℕ) → 𝑘
∈ ℤ) |
69 | 12, 1 | eleqtrdi 2263 |
. . . . . . 7
⊢
((⊤ ∧ 𝑘
∈ ℕ) → (𝑘 +
1) ∈ (ℤ≥‘1)) |
70 | | elfznn 10010 |
. . . . . . . . . 10
⊢ (𝑛 ∈ (1...(𝑘 + 1)) → 𝑛 ∈ ℕ) |
71 | 70 | adantl 275 |
. . . . . . . . 9
⊢
(((⊤ ∧ 𝑘
∈ ℕ) ∧ 𝑛
∈ (1...(𝑘 + 1)))
→ 𝑛 ∈
ℕ) |
72 | 71 | nnrecred 8925 |
. . . . . . . 8
⊢
(((⊤ ∧ 𝑘
∈ ℕ) ∧ 𝑛
∈ (1...(𝑘 + 1)))
→ (1 / 𝑛) ∈
ℝ) |
73 | 72 | recnd 7948 |
. . . . . . 7
⊢
(((⊤ ∧ 𝑘
∈ ℕ) ∧ 𝑛
∈ (1...(𝑘 + 1)))
→ (1 / 𝑛) ∈
ℂ) |
74 | 62, 63, 66, 14, 68, 69, 73 | telfsum 11431 |
. . . . . 6
⊢
((⊤ ∧ 𝑘
∈ ℕ) → Σ𝑗 ∈ (1...𝑘)((1 / 𝑗) − (1 / (𝑗 + 1))) = (1 − (1 / (𝑘 + 1)))) |
75 | 61, 74 | eqtrd 2203 |
. . . . 5
⊢
((⊤ ∧ 𝑘
∈ ℕ) → Σ𝑗 ∈ (1...𝑘)(1 / (𝑗 · (𝑗 + 1))) = (1 − (1 / (𝑘 + 1)))) |
76 | | elnnuz 9523 |
. . . . . . . . 9
⊢ (𝑗 ∈ ℕ ↔ 𝑗 ∈
(ℤ≥‘1)) |
77 | 76 | biimpri 132 |
. . . . . . . 8
⊢ (𝑗 ∈
(ℤ≥‘1) → 𝑗 ∈ ℕ) |
78 | 77 | adantl 275 |
. . . . . . 7
⊢
(((⊤ ∧ 𝑘
∈ ℕ) ∧ 𝑗
∈ (ℤ≥‘1)) → 𝑗 ∈ ℕ) |
79 | | eluzelz 9496 |
. . . . . . . . . . 11
⊢ (𝑗 ∈
(ℤ≥‘1) → 𝑗 ∈ ℤ) |
80 | 79 | adantl 275 |
. . . . . . . . . 10
⊢
(((⊤ ∧ 𝑘
∈ ℕ) ∧ 𝑗
∈ (ℤ≥‘1)) → 𝑗 ∈ ℤ) |
81 | 80 | zcnd 9335 |
. . . . . . . . 9
⊢
(((⊤ ∧ 𝑘
∈ ℕ) ∧ 𝑗
∈ (ℤ≥‘1)) → 𝑗 ∈ ℂ) |
82 | 81, 35 | syl 14 |
. . . . . . . . 9
⊢
(((⊤ ∧ 𝑘
∈ ℕ) ∧ 𝑗
∈ (ℤ≥‘1)) → (𝑗 + 1) ∈ ℂ) |
83 | 81, 82 | mulcld 7940 |
. . . . . . . 8
⊢
(((⊤ ∧ 𝑘
∈ ℕ) ∧ 𝑗
∈ (ℤ≥‘1)) → (𝑗 · (𝑗 + 1)) ∈ ℂ) |
84 | 78 | nnap0d 8924 |
. . . . . . . . 9
⊢
(((⊤ ∧ 𝑘
∈ ℕ) ∧ 𝑗
∈ (ℤ≥‘1)) → 𝑗 # 0) |
85 | 78, 37 | syl 14 |
. . . . . . . . . 10
⊢
(((⊤ ∧ 𝑘
∈ ℕ) ∧ 𝑗
∈ (ℤ≥‘1)) → (𝑗 + 1) ∈ ℕ) |
86 | 85 | nnap0d 8924 |
. . . . . . . . 9
⊢
(((⊤ ∧ 𝑘
∈ ℕ) ∧ 𝑗
∈ (ℤ≥‘1)) → (𝑗 + 1) # 0) |
87 | 81, 82, 84, 86 | mulap0d 8576 |
. . . . . . . 8
⊢
(((⊤ ∧ 𝑘
∈ ℕ) ∧ 𝑗
∈ (ℤ≥‘1)) → (𝑗 · (𝑗 + 1)) # 0) |
88 | 83, 87 | recclapd 8698 |
. . . . . . 7
⊢
(((⊤ ∧ 𝑘
∈ ℕ) ∧ 𝑗
∈ (ℤ≥‘1)) → (1 / (𝑗 · (𝑗 + 1))) ∈ ℂ) |
89 | | id 19 |
. . . . . . . . . 10
⊢ (𝑛 = 𝑗 → 𝑛 = 𝑗) |
90 | | oveq1 5860 |
. . . . . . . . . 10
⊢ (𝑛 = 𝑗 → (𝑛 + 1) = (𝑗 + 1)) |
91 | 89, 90 | oveq12d 5871 |
. . . . . . . . 9
⊢ (𝑛 = 𝑗 → (𝑛 · (𝑛 + 1)) = (𝑗 · (𝑗 + 1))) |
92 | 91 | oveq2d 5869 |
. . . . . . . 8
⊢ (𝑛 = 𝑗 → (1 / (𝑛 · (𝑛 + 1))) = (1 / (𝑗 · (𝑗 + 1)))) |
93 | | trireciplem.1 |
. . . . . . . 8
⊢ 𝐹 = (𝑛 ∈ ℕ ↦ (1 / (𝑛 · (𝑛 + 1)))) |
94 | 92, 93 | fvmptg 5572 |
. . . . . . 7
⊢ ((𝑗 ∈ ℕ ∧ (1 /
(𝑗 · (𝑗 + 1))) ∈ ℂ) →
(𝐹‘𝑗) = (1 / (𝑗 · (𝑗 + 1)))) |
95 | 78, 88, 94 | syl2anc 409 |
. . . . . 6
⊢
(((⊤ ∧ 𝑘
∈ ℕ) ∧ 𝑗
∈ (ℤ≥‘1)) → (𝐹‘𝑗) = (1 / (𝑗 · (𝑗 + 1)))) |
96 | 18, 1 | eleqtrdi 2263 |
. . . . . 6
⊢
((⊤ ∧ 𝑘
∈ ℕ) → 𝑘
∈ (ℤ≥‘1)) |
97 | 95, 96, 88 | fsum3ser 11360 |
. . . . 5
⊢
((⊤ ∧ 𝑘
∈ ℕ) → Σ𝑗 ∈ (1...𝑘)(1 / (𝑗 · (𝑗 + 1))) = (seq1( + , 𝐹)‘𝑘)) |
98 | 31, 75, 97 | 3eqtr2rd 2210 |
. . . 4
⊢
((⊤ ∧ 𝑘
∈ ℕ) → (seq1( + , 𝐹)‘𝑘) = (1 − ((𝑛 ∈ ℕ ↦ (1 / (𝑛 + 1)))‘𝑘))) |
99 | 1, 2, 26, 3, 28, 30, 98 | climsubc2 11296 |
. . 3
⊢ (⊤
→ seq1( + , 𝐹) ⇝
(1 − 0)) |
100 | 99 | mptru 1357 |
. 2
⊢ seq1( + ,
𝐹) ⇝ (1 −
0) |
101 | | 1m0e1 8991 |
. 2
⊢ (1
− 0) = 1 |
102 | 100, 101 | breqtri 4014 |
1
⊢ seq1( + ,
𝐹) ⇝
1 |