Step | Hyp | Ref
| Expression |
1 | | 1nn 11031 |
. . . . 5
⊢ 1 ∈
ℕ |
2 | | stirlinglem12.1 |
. . . . . . 7
⊢ 𝐴 = (𝑛 ∈ ℕ ↦ ((!‘𝑛) / ((√‘(2 ·
𝑛)) · ((𝑛 / e)↑𝑛)))) |
3 | 2 | stirlinglem2 40292 |
. . . . . 6
⊢ (1 ∈
ℕ → (𝐴‘1)
∈ ℝ+) |
4 | | relogcl 24322 |
. . . . . 6
⊢ ((𝐴‘1) ∈
ℝ+ → (log‘(𝐴‘1)) ∈ ℝ) |
5 | 1, 3, 4 | mp2b 10 |
. . . . 5
⊢
(log‘(𝐴‘1)) ∈ ℝ |
6 | | nfcv 2764 |
. . . . . 6
⊢
Ⅎ𝑛1 |
7 | | nfcv 2764 |
. . . . . . 7
⊢
Ⅎ𝑛log |
8 | | nfmpt1 4747 |
. . . . . . . . 9
⊢
Ⅎ𝑛(𝑛 ∈ ℕ ↦ ((!‘𝑛) / ((√‘(2 ·
𝑛)) · ((𝑛 / e)↑𝑛)))) |
9 | 2, 8 | nfcxfr 2762 |
. . . . . . . 8
⊢
Ⅎ𝑛𝐴 |
10 | 9, 6 | nffv 6198 |
. . . . . . 7
⊢
Ⅎ𝑛(𝐴‘1) |
11 | 7, 10 | nffv 6198 |
. . . . . 6
⊢
Ⅎ𝑛(log‘(𝐴‘1)) |
12 | | fveq2 6191 |
. . . . . . 7
⊢ (𝑛 = 1 → (𝐴‘𝑛) = (𝐴‘1)) |
13 | 12 | fveq2d 6195 |
. . . . . 6
⊢ (𝑛 = 1 → (log‘(𝐴‘𝑛)) = (log‘(𝐴‘1))) |
14 | | stirlinglem12.2 |
. . . . . 6
⊢ 𝐵 = (𝑛 ∈ ℕ ↦ (log‘(𝐴‘𝑛))) |
15 | 6, 11, 13, 14 | fvmptf 6301 |
. . . . 5
⊢ ((1
∈ ℕ ∧ (log‘(𝐴‘1)) ∈ ℝ) → (𝐵‘1) = (log‘(𝐴‘1))) |
16 | 1, 5, 15 | mp2an 708 |
. . . 4
⊢ (𝐵‘1) = (log‘(𝐴‘1)) |
17 | 16, 5 | eqeltri 2697 |
. . 3
⊢ (𝐵‘1) ∈
ℝ |
18 | 17 | a1i 11 |
. 2
⊢ (𝑁 ∈ ℕ → (𝐵‘1) ∈
ℝ) |
19 | 2 | stirlinglem2 40292 |
. . . . 5
⊢ (𝑁 ∈ ℕ → (𝐴‘𝑁) ∈
ℝ+) |
20 | 19 | relogcld 24369 |
. . . 4
⊢ (𝑁 ∈ ℕ →
(log‘(𝐴‘𝑁)) ∈
ℝ) |
21 | | nfcv 2764 |
. . . . 5
⊢
Ⅎ𝑛𝑁 |
22 | 9, 21 | nffv 6198 |
. . . . . 6
⊢
Ⅎ𝑛(𝐴‘𝑁) |
23 | 7, 22 | nffv 6198 |
. . . . 5
⊢
Ⅎ𝑛(log‘(𝐴‘𝑁)) |
24 | | fveq2 6191 |
. . . . . 6
⊢ (𝑛 = 𝑁 → (𝐴‘𝑛) = (𝐴‘𝑁)) |
25 | 24 | fveq2d 6195 |
. . . . 5
⊢ (𝑛 = 𝑁 → (log‘(𝐴‘𝑛)) = (log‘(𝐴‘𝑁))) |
26 | 21, 23, 25, 14 | fvmptf 6301 |
. . . 4
⊢ ((𝑁 ∈ ℕ ∧
(log‘(𝐴‘𝑁)) ∈ ℝ) → (𝐵‘𝑁) = (log‘(𝐴‘𝑁))) |
27 | 20, 26 | mpdan 702 |
. . 3
⊢ (𝑁 ∈ ℕ → (𝐵‘𝑁) = (log‘(𝐴‘𝑁))) |
28 | 27, 20 | eqeltrd 2701 |
. 2
⊢ (𝑁 ∈ ℕ → (𝐵‘𝑁) ∈ ℝ) |
29 | | 4re 11097 |
. . . 4
⊢ 4 ∈
ℝ |
30 | | 4ne0 11117 |
. . . 4
⊢ 4 ≠
0 |
31 | 29, 30 | rereccli 10790 |
. . 3
⊢ (1 / 4)
∈ ℝ |
32 | 31 | a1i 11 |
. 2
⊢ (𝑁 ∈ ℕ → (1 / 4)
∈ ℝ) |
33 | | fveq2 6191 |
. . . . 5
⊢ (𝑘 = 𝑗 → (𝐵‘𝑘) = (𝐵‘𝑗)) |
34 | | fveq2 6191 |
. . . . 5
⊢ (𝑘 = (𝑗 + 1) → (𝐵‘𝑘) = (𝐵‘(𝑗 + 1))) |
35 | | fveq2 6191 |
. . . . 5
⊢ (𝑘 = 1 → (𝐵‘𝑘) = (𝐵‘1)) |
36 | | fveq2 6191 |
. . . . 5
⊢ (𝑘 = 𝑁 → (𝐵‘𝑘) = (𝐵‘𝑁)) |
37 | | elnnuz 11724 |
. . . . . 6
⊢ (𝑁 ∈ ℕ ↔ 𝑁 ∈
(ℤ≥‘1)) |
38 | 37 | biimpi 206 |
. . . . 5
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
(ℤ≥‘1)) |
39 | | elfznn 12370 |
. . . . . . . 8
⊢ (𝑘 ∈ (1...𝑁) → 𝑘 ∈ ℕ) |
40 | 2 | stirlinglem2 40292 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ℕ → (𝐴‘𝑘) ∈
ℝ+) |
41 | 39, 40 | syl 17 |
. . . . . . . . 9
⊢ (𝑘 ∈ (1...𝑁) → (𝐴‘𝑘) ∈
ℝ+) |
42 | 41 | relogcld 24369 |
. . . . . . . 8
⊢ (𝑘 ∈ (1...𝑁) → (log‘(𝐴‘𝑘)) ∈ ℝ) |
43 | | nfcv 2764 |
. . . . . . . . 9
⊢
Ⅎ𝑛𝑘 |
44 | 9, 43 | nffv 6198 |
. . . . . . . . . 10
⊢
Ⅎ𝑛(𝐴‘𝑘) |
45 | 7, 44 | nffv 6198 |
. . . . . . . . 9
⊢
Ⅎ𝑛(log‘(𝐴‘𝑘)) |
46 | | fveq2 6191 |
. . . . . . . . . 10
⊢ (𝑛 = 𝑘 → (𝐴‘𝑛) = (𝐴‘𝑘)) |
47 | 46 | fveq2d 6195 |
. . . . . . . . 9
⊢ (𝑛 = 𝑘 → (log‘(𝐴‘𝑛)) = (log‘(𝐴‘𝑘))) |
48 | 43, 45, 47, 14 | fvmptf 6301 |
. . . . . . . 8
⊢ ((𝑘 ∈ ℕ ∧
(log‘(𝐴‘𝑘)) ∈ ℝ) → (𝐵‘𝑘) = (log‘(𝐴‘𝑘))) |
49 | 39, 42, 48 | syl2anc 693 |
. . . . . . 7
⊢ (𝑘 ∈ (1...𝑁) → (𝐵‘𝑘) = (log‘(𝐴‘𝑘))) |
50 | 49 | adantl 482 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (1...𝑁)) → (𝐵‘𝑘) = (log‘(𝐴‘𝑘))) |
51 | 41 | rpcnd 11874 |
. . . . . . . 8
⊢ (𝑘 ∈ (1...𝑁) → (𝐴‘𝑘) ∈ ℂ) |
52 | 51 | adantl 482 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (1...𝑁)) → (𝐴‘𝑘) ∈ ℂ) |
53 | 40 | rpne0d 11877 |
. . . . . . . . 9
⊢ (𝑘 ∈ ℕ → (𝐴‘𝑘) ≠ 0) |
54 | 39, 53 | syl 17 |
. . . . . . . 8
⊢ (𝑘 ∈ (1...𝑁) → (𝐴‘𝑘) ≠ 0) |
55 | 54 | adantl 482 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (1...𝑁)) → (𝐴‘𝑘) ≠ 0) |
56 | 52, 55 | logcld 24317 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (1...𝑁)) → (log‘(𝐴‘𝑘)) ∈ ℂ) |
57 | 50, 56 | eqeltrd 2701 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (1...𝑁)) → (𝐵‘𝑘) ∈ ℂ) |
58 | 33, 34, 35, 36, 38, 57 | telfsumo 14534 |
. . . 4
⊢ (𝑁 ∈ ℕ →
Σ𝑗 ∈ (1..^𝑁)((𝐵‘𝑗) − (𝐵‘(𝑗 + 1))) = ((𝐵‘1) − (𝐵‘𝑁))) |
59 | | nnz 11399 |
. . . . . 6
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℤ) |
60 | | fzoval 12471 |
. . . . . 6
⊢ (𝑁 ∈ ℤ →
(1..^𝑁) = (1...(𝑁 − 1))) |
61 | 59, 60 | syl 17 |
. . . . 5
⊢ (𝑁 ∈ ℕ →
(1..^𝑁) = (1...(𝑁 − 1))) |
62 | 61 | sumeq1d 14431 |
. . . 4
⊢ (𝑁 ∈ ℕ →
Σ𝑗 ∈ (1..^𝑁)((𝐵‘𝑗) − (𝐵‘(𝑗 + 1))) = Σ𝑗 ∈ (1...(𝑁 − 1))((𝐵‘𝑗) − (𝐵‘(𝑗 + 1)))) |
63 | 58, 62 | eqtr3d 2658 |
. . 3
⊢ (𝑁 ∈ ℕ → ((𝐵‘1) − (𝐵‘𝑁)) = Σ𝑗 ∈ (1...(𝑁 − 1))((𝐵‘𝑗) − (𝐵‘(𝑗 + 1)))) |
64 | | fzfid 12772 |
. . . . 5
⊢ (𝑁 ∈ ℕ →
(1...(𝑁 − 1)) ∈
Fin) |
65 | | elfznn 12370 |
. . . . . . . 8
⊢ (𝑗 ∈ (1...(𝑁 − 1)) → 𝑗 ∈ ℕ) |
66 | 65 | adantl 482 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ (1...(𝑁 − 1))) → 𝑗 ∈ ℕ) |
67 | 2 | stirlinglem2 40292 |
. . . . . . . . . 10
⊢ (𝑗 ∈ ℕ → (𝐴‘𝑗) ∈
ℝ+) |
68 | 67 | relogcld 24369 |
. . . . . . . . 9
⊢ (𝑗 ∈ ℕ →
(log‘(𝐴‘𝑗)) ∈
ℝ) |
69 | | nfcv 2764 |
. . . . . . . . . 10
⊢
Ⅎ𝑛𝑗 |
70 | 9, 69 | nffv 6198 |
. . . . . . . . . . 11
⊢
Ⅎ𝑛(𝐴‘𝑗) |
71 | 7, 70 | nffv 6198 |
. . . . . . . . . 10
⊢
Ⅎ𝑛(log‘(𝐴‘𝑗)) |
72 | | fveq2 6191 |
. . . . . . . . . . 11
⊢ (𝑛 = 𝑗 → (𝐴‘𝑛) = (𝐴‘𝑗)) |
73 | 72 | fveq2d 6195 |
. . . . . . . . . 10
⊢ (𝑛 = 𝑗 → (log‘(𝐴‘𝑛)) = (log‘(𝐴‘𝑗))) |
74 | 69, 71, 73, 14 | fvmptf 6301 |
. . . . . . . . 9
⊢ ((𝑗 ∈ ℕ ∧
(log‘(𝐴‘𝑗)) ∈ ℝ) → (𝐵‘𝑗) = (log‘(𝐴‘𝑗))) |
75 | 68, 74 | mpdan 702 |
. . . . . . . 8
⊢ (𝑗 ∈ ℕ → (𝐵‘𝑗) = (log‘(𝐴‘𝑗))) |
76 | 75, 68 | eqeltrd 2701 |
. . . . . . 7
⊢ (𝑗 ∈ ℕ → (𝐵‘𝑗) ∈ ℝ) |
77 | 66, 76 | syl 17 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ (1...(𝑁 − 1))) → (𝐵‘𝑗) ∈ ℝ) |
78 | | peano2nn 11032 |
. . . . . . . . . 10
⊢ (𝑗 ∈ ℕ → (𝑗 + 1) ∈
ℕ) |
79 | 2 | stirlinglem2 40292 |
. . . . . . . . . . . 12
⊢ ((𝑗 + 1) ∈ ℕ →
(𝐴‘(𝑗 + 1)) ∈
ℝ+) |
80 | 78, 79 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑗 ∈ ℕ → (𝐴‘(𝑗 + 1)) ∈
ℝ+) |
81 | 80 | relogcld 24369 |
. . . . . . . . . 10
⊢ (𝑗 ∈ ℕ →
(log‘(𝐴‘(𝑗 + 1))) ∈
ℝ) |
82 | | nfcv 2764 |
. . . . . . . . . . 11
⊢
Ⅎ𝑛(𝑗 + 1) |
83 | 9, 82 | nffv 6198 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑛(𝐴‘(𝑗 + 1)) |
84 | 7, 83 | nffv 6198 |
. . . . . . . . . . 11
⊢
Ⅎ𝑛(log‘(𝐴‘(𝑗 + 1))) |
85 | | fveq2 6191 |
. . . . . . . . . . . 12
⊢ (𝑛 = (𝑗 + 1) → (𝐴‘𝑛) = (𝐴‘(𝑗 + 1))) |
86 | 85 | fveq2d 6195 |
. . . . . . . . . . 11
⊢ (𝑛 = (𝑗 + 1) → (log‘(𝐴‘𝑛)) = (log‘(𝐴‘(𝑗 + 1)))) |
87 | 82, 84, 86, 14 | fvmptf 6301 |
. . . . . . . . . 10
⊢ (((𝑗 + 1) ∈ ℕ ∧
(log‘(𝐴‘(𝑗 + 1))) ∈ ℝ) →
(𝐵‘(𝑗 + 1)) = (log‘(𝐴‘(𝑗 + 1)))) |
88 | 78, 81, 87 | syl2anc 693 |
. . . . . . . . 9
⊢ (𝑗 ∈ ℕ → (𝐵‘(𝑗 + 1)) = (log‘(𝐴‘(𝑗 + 1)))) |
89 | 88, 81 | eqeltrd 2701 |
. . . . . . . 8
⊢ (𝑗 ∈ ℕ → (𝐵‘(𝑗 + 1)) ∈ ℝ) |
90 | 65, 89 | syl 17 |
. . . . . . 7
⊢ (𝑗 ∈ (1...(𝑁 − 1)) → (𝐵‘(𝑗 + 1)) ∈ ℝ) |
91 | 90 | adantl 482 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ (1...(𝑁 − 1))) → (𝐵‘(𝑗 + 1)) ∈ ℝ) |
92 | 77, 91 | resubcld 10458 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ (1...(𝑁 − 1))) → ((𝐵‘𝑗) − (𝐵‘(𝑗 + 1))) ∈ ℝ) |
93 | 64, 92 | fsumrecl 14465 |
. . . 4
⊢ (𝑁 ∈ ℕ →
Σ𝑗 ∈ (1...(𝑁 − 1))((𝐵‘𝑗) − (𝐵‘(𝑗 + 1))) ∈ ℝ) |
94 | 31 | a1i 11 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ (1...(𝑁 − 1))) → (1 / 4) ∈
ℝ) |
95 | 65 | nnred 11035 |
. . . . . . . . 9
⊢ (𝑗 ∈ (1...(𝑁 − 1)) → 𝑗 ∈ ℝ) |
96 | | 1red 10055 |
. . . . . . . . . 10
⊢ (𝑗 ∈ (1...(𝑁 − 1)) → 1 ∈
ℝ) |
97 | 95, 96 | readdcld 10069 |
. . . . . . . . 9
⊢ (𝑗 ∈ (1...(𝑁 − 1)) → (𝑗 + 1) ∈ ℝ) |
98 | 95, 97 | remulcld 10070 |
. . . . . . . 8
⊢ (𝑗 ∈ (1...(𝑁 − 1)) → (𝑗 · (𝑗 + 1)) ∈ ℝ) |
99 | 95 | recnd 10068 |
. . . . . . . . 9
⊢ (𝑗 ∈ (1...(𝑁 − 1)) → 𝑗 ∈ ℂ) |
100 | | 1cnd 10056 |
. . . . . . . . . 10
⊢ (𝑗 ∈ (1...(𝑁 − 1)) → 1 ∈
ℂ) |
101 | 99, 100 | addcld 10059 |
. . . . . . . . 9
⊢ (𝑗 ∈ (1...(𝑁 − 1)) → (𝑗 + 1) ∈ ℂ) |
102 | 65 | nnne0d 11065 |
. . . . . . . . 9
⊢ (𝑗 ∈ (1...(𝑁 − 1)) → 𝑗 ≠ 0) |
103 | 78 | nnne0d 11065 |
. . . . . . . . . 10
⊢ (𝑗 ∈ ℕ → (𝑗 + 1) ≠ 0) |
104 | 65, 103 | syl 17 |
. . . . . . . . 9
⊢ (𝑗 ∈ (1...(𝑁 − 1)) → (𝑗 + 1) ≠ 0) |
105 | 99, 101, 102, 104 | mulne0d 10679 |
. . . . . . . 8
⊢ (𝑗 ∈ (1...(𝑁 − 1)) → (𝑗 · (𝑗 + 1)) ≠ 0) |
106 | 98, 105 | rereccld 10852 |
. . . . . . 7
⊢ (𝑗 ∈ (1...(𝑁 − 1)) → (1 / (𝑗 · (𝑗 + 1))) ∈ ℝ) |
107 | 106 | adantl 482 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ (1...(𝑁 − 1))) → (1 / (𝑗 · (𝑗 + 1))) ∈ ℝ) |
108 | 94, 107 | remulcld 10070 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ (1...(𝑁 − 1))) → ((1 / 4) · (1 /
(𝑗 · (𝑗 + 1)))) ∈
ℝ) |
109 | 64, 108 | fsumrecl 14465 |
. . . 4
⊢ (𝑁 ∈ ℕ →
Σ𝑗 ∈ (1...(𝑁 − 1))((1 / 4) · (1
/ (𝑗 · (𝑗 + 1)))) ∈
ℝ) |
110 | | eqid 2622 |
. . . . . . 7
⊢ (𝑖 ∈ ℕ ↦ ((1 /
((2 · 𝑖) + 1))
· ((1 / ((2 · 𝑗) + 1))↑(2 · 𝑖)))) = (𝑖 ∈ ℕ ↦ ((1 / ((2 ·
𝑖) + 1)) · ((1 / ((2
· 𝑗) + 1))↑(2
· 𝑖)))) |
111 | | eqid 2622 |
. . . . . . 7
⊢ (𝑖 ∈ ℕ ↦ ((1 /
(((2 · 𝑗) +
1)↑2))↑𝑖)) =
(𝑖 ∈ ℕ ↦
((1 / (((2 · 𝑗) +
1)↑2))↑𝑖)) |
112 | 2, 14, 110, 111 | stirlinglem10 40300 |
. . . . . 6
⊢ (𝑗 ∈ ℕ → ((𝐵‘𝑗) − (𝐵‘(𝑗 + 1))) ≤ ((1 / 4) · (1 / (𝑗 · (𝑗 + 1))))) |
113 | 66, 112 | syl 17 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ (1...(𝑁 − 1))) → ((𝐵‘𝑗) − (𝐵‘(𝑗 + 1))) ≤ ((1 / 4) · (1 / (𝑗 · (𝑗 + 1))))) |
114 | 64, 92, 108, 113 | fsumle 14531 |
. . . 4
⊢ (𝑁 ∈ ℕ →
Σ𝑗 ∈ (1...(𝑁 − 1))((𝐵‘𝑗) − (𝐵‘(𝑗 + 1))) ≤ Σ𝑗 ∈ (1...(𝑁 − 1))((1 / 4) · (1 / (𝑗 · (𝑗 + 1))))) |
115 | 64, 107 | fsumrecl 14465 |
. . . . . 6
⊢ (𝑁 ∈ ℕ →
Σ𝑗 ∈ (1...(𝑁 − 1))(1 / (𝑗 · (𝑗 + 1))) ∈ ℝ) |
116 | | 1red 10055 |
. . . . . 6
⊢ (𝑁 ∈ ℕ → 1 ∈
ℝ) |
117 | | 4pos 11116 |
. . . . . . . . 9
⊢ 0 <
4 |
118 | 29, 117 | elrpii 11835 |
. . . . . . . 8
⊢ 4 ∈
ℝ+ |
119 | 118 | a1i 11 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ → 4 ∈
ℝ+) |
120 | | 0red 10041 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ → 0 ∈
ℝ) |
121 | | 0lt1 10550 |
. . . . . . . . 9
⊢ 0 <
1 |
122 | 121 | a1i 11 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ → 0 <
1) |
123 | 120, 116,
122 | ltled 10185 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ → 0 ≤
1) |
124 | 116, 119,
123 | divge0d 11912 |
. . . . . 6
⊢ (𝑁 ∈ ℕ → 0 ≤ (1
/ 4)) |
125 | | eqid 2622 |
. . . . . . . . . 10
⊢
(ℤ≥‘𝑁) = (ℤ≥‘𝑁) |
126 | | eluznn 11758 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈
(ℤ≥‘𝑁)) → 𝑗 ∈ ℕ) |
127 | | stirlinglem12.3 |
. . . . . . . . . . . . 13
⊢ 𝐹 = (𝑛 ∈ ℕ ↦ (1 / (𝑛 · (𝑛 + 1)))) |
128 | 127 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝑗 ∈ ℕ → 𝐹 = (𝑛 ∈ ℕ ↦ (1 / (𝑛 · (𝑛 + 1))))) |
129 | | simpr 477 |
. . . . . . . . . . . . . 14
⊢ ((𝑗 ∈ ℕ ∧ 𝑛 = 𝑗) → 𝑛 = 𝑗) |
130 | 129 | oveq1d 6665 |
. . . . . . . . . . . . . 14
⊢ ((𝑗 ∈ ℕ ∧ 𝑛 = 𝑗) → (𝑛 + 1) = (𝑗 + 1)) |
131 | 129, 130 | oveq12d 6668 |
. . . . . . . . . . . . 13
⊢ ((𝑗 ∈ ℕ ∧ 𝑛 = 𝑗) → (𝑛 · (𝑛 + 1)) = (𝑗 · (𝑗 + 1))) |
132 | 131 | oveq2d 6666 |
. . . . . . . . . . . 12
⊢ ((𝑗 ∈ ℕ ∧ 𝑛 = 𝑗) → (1 / (𝑛 · (𝑛 + 1))) = (1 / (𝑗 · (𝑗 + 1)))) |
133 | | id 22 |
. . . . . . . . . . . 12
⊢ (𝑗 ∈ ℕ → 𝑗 ∈
ℕ) |
134 | | nnre 11027 |
. . . . . . . . . . . . . 14
⊢ (𝑗 ∈ ℕ → 𝑗 ∈
ℝ) |
135 | | 1red 10055 |
. . . . . . . . . . . . . . 15
⊢ (𝑗 ∈ ℕ → 1 ∈
ℝ) |
136 | 134, 135 | readdcld 10069 |
. . . . . . . . . . . . . 14
⊢ (𝑗 ∈ ℕ → (𝑗 + 1) ∈
ℝ) |
137 | 134, 136 | remulcld 10070 |
. . . . . . . . . . . . 13
⊢ (𝑗 ∈ ℕ → (𝑗 · (𝑗 + 1)) ∈ ℝ) |
138 | | nncn 11028 |
. . . . . . . . . . . . . 14
⊢ (𝑗 ∈ ℕ → 𝑗 ∈
ℂ) |
139 | | 1cnd 10056 |
. . . . . . . . . . . . . . 15
⊢ (𝑗 ∈ ℕ → 1 ∈
ℂ) |
140 | 138, 139 | addcld 10059 |
. . . . . . . . . . . . . 14
⊢ (𝑗 ∈ ℕ → (𝑗 + 1) ∈
ℂ) |
141 | | nnne0 11053 |
. . . . . . . . . . . . . 14
⊢ (𝑗 ∈ ℕ → 𝑗 ≠ 0) |
142 | 138, 140,
141, 103 | mulne0d 10679 |
. . . . . . . . . . . . 13
⊢ (𝑗 ∈ ℕ → (𝑗 · (𝑗 + 1)) ≠ 0) |
143 | 137, 142 | rereccld 10852 |
. . . . . . . . . . . 12
⊢ (𝑗 ∈ ℕ → (1 /
(𝑗 · (𝑗 + 1))) ∈
ℝ) |
144 | 128, 132,
133, 143 | fvmptd 6288 |
. . . . . . . . . . 11
⊢ (𝑗 ∈ ℕ → (𝐹‘𝑗) = (1 / (𝑗 · (𝑗 + 1)))) |
145 | 126, 144 | syl 17 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈
(ℤ≥‘𝑁)) → (𝐹‘𝑗) = (1 / (𝑗 · (𝑗 + 1)))) |
146 | 126 | nnred 11035 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈
(ℤ≥‘𝑁)) → 𝑗 ∈ ℝ) |
147 | | 1red 10055 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈
(ℤ≥‘𝑁)) → 1 ∈ ℝ) |
148 | 146, 147 | readdcld 10069 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈
(ℤ≥‘𝑁)) → (𝑗 + 1) ∈ ℝ) |
149 | 146, 148 | remulcld 10070 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈
(ℤ≥‘𝑁)) → (𝑗 · (𝑗 + 1)) ∈ ℝ) |
150 | 146 | recnd 10068 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈
(ℤ≥‘𝑁)) → 𝑗 ∈ ℂ) |
151 | | 1cnd 10056 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈
(ℤ≥‘𝑁)) → 1 ∈ ℂ) |
152 | 150, 151 | addcld 10059 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈
(ℤ≥‘𝑁)) → (𝑗 + 1) ∈ ℂ) |
153 | 126 | nnne0d 11065 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈
(ℤ≥‘𝑁)) → 𝑗 ≠ 0) |
154 | 126, 103 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈
(ℤ≥‘𝑁)) → (𝑗 + 1) ≠ 0) |
155 | 150, 152,
153, 154 | mulne0d 10679 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈
(ℤ≥‘𝑁)) → (𝑗 · (𝑗 + 1)) ≠ 0) |
156 | 149, 155 | rereccld 10852 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈
(ℤ≥‘𝑁)) → (1 / (𝑗 · (𝑗 + 1))) ∈ ℝ) |
157 | | seqeq1 12804 |
. . . . . . . . . . . . 13
⊢ (𝑁 = 1 → seq𝑁( + , 𝐹) = seq1( + , 𝐹)) |
158 | 127 | trireciplem 14594 |
. . . . . . . . . . . . . 14
⊢ seq1( + ,
𝐹) ⇝
1 |
159 | | climrel 14223 |
. . . . . . . . . . . . . . 15
⊢ Rel
⇝ |
160 | 159 | releldmi 5362 |
. . . . . . . . . . . . . 14
⊢ (seq1( +
, 𝐹) ⇝ 1 → seq1(
+ , 𝐹) ∈ dom ⇝
) |
161 | 158, 160 | mp1i 13 |
. . . . . . . . . . . . 13
⊢ (𝑁 = 1 → seq1( + , 𝐹) ∈ dom ⇝
) |
162 | 157, 161 | eqeltrd 2701 |
. . . . . . . . . . . 12
⊢ (𝑁 = 1 → seq𝑁( + , 𝐹) ∈ dom ⇝ ) |
163 | 162 | adantl 482 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ 𝑁 = 1) → seq𝑁( + , 𝐹) ∈ dom ⇝ ) |
164 | | simpl 473 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ ∧ ¬
𝑁 = 1) → 𝑁 ∈
ℕ) |
165 | | simpr 477 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℕ ∧ ¬
𝑁 = 1) → ¬ 𝑁 = 1) |
166 | | elnn1uz2 11765 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈ ℕ ↔ (𝑁 = 1 ∨ 𝑁 ∈
(ℤ≥‘2))) |
167 | 164, 166 | sylib 208 |
. . . . . . . . . . . . . . 15
⊢ ((𝑁 ∈ ℕ ∧ ¬
𝑁 = 1) → (𝑁 = 1 ∨ 𝑁 ∈
(ℤ≥‘2))) |
168 | 167 | ord 392 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℕ ∧ ¬
𝑁 = 1) → (¬ 𝑁 = 1 → 𝑁 ∈
(ℤ≥‘2))) |
169 | 165, 168 | mpd 15 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℕ ∧ ¬
𝑁 = 1) → 𝑁 ∈
(ℤ≥‘2)) |
170 | | uz2m1nn 11763 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈
(ℤ≥‘2) → (𝑁 − 1) ∈ ℕ) |
171 | 169, 170 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ ∧ ¬
𝑁 = 1) → (𝑁 − 1) ∈
ℕ) |
172 | | nncn 11028 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℂ) |
173 | 172 | adantr 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑁 ∈ ℕ ∧ (𝑁 − 1) ∈ ℕ)
→ 𝑁 ∈
ℂ) |
174 | | 1cnd 10056 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑁 ∈ ℕ ∧ (𝑁 − 1) ∈ ℕ)
→ 1 ∈ ℂ) |
175 | 173, 174 | npcand 10396 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑁 ∈ ℕ ∧ (𝑁 − 1) ∈ ℕ)
→ ((𝑁 − 1) + 1)
= 𝑁) |
176 | 175 | eqcomd 2628 |
. . . . . . . . . . . . . . 15
⊢ ((𝑁 ∈ ℕ ∧ (𝑁 − 1) ∈ ℕ)
→ 𝑁 = ((𝑁 − 1) +
1)) |
177 | 176 | seqeq1d 12807 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℕ ∧ (𝑁 − 1) ∈ ℕ)
→ seq𝑁( + , 𝐹) = seq((𝑁 − 1) + 1)( + , 𝐹)) |
178 | | nnuz 11723 |
. . . . . . . . . . . . . . . 16
⊢ ℕ =
(ℤ≥‘1) |
179 | | id 22 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑁 − 1) ∈ ℕ
→ (𝑁 − 1) ∈
ℕ) |
180 | 143 | recnd 10068 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑗 ∈ ℕ → (1 /
(𝑗 · (𝑗 + 1))) ∈
ℂ) |
181 | 144, 180 | eqeltrd 2701 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑗 ∈ ℕ → (𝐹‘𝑗) ∈ ℂ) |
182 | 181 | adantl 482 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑁 − 1) ∈ ℕ ∧
𝑗 ∈ ℕ) →
(𝐹‘𝑗) ∈ ℂ) |
183 | 158 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑁 − 1) ∈ ℕ
→ seq1( + , 𝐹) ⇝
1) |
184 | 178, 179,
182, 183 | clim2ser 14385 |
. . . . . . . . . . . . . . 15
⊢ ((𝑁 − 1) ∈ ℕ
→ seq((𝑁 − 1) +
1)( + , 𝐹) ⇝ (1
− (seq1( + , 𝐹)‘(𝑁 − 1)))) |
185 | 184 | adantl 482 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℕ ∧ (𝑁 − 1) ∈ ℕ)
→ seq((𝑁 − 1) +
1)( + , 𝐹) ⇝ (1
− (seq1( + , 𝐹)‘(𝑁 − 1)))) |
186 | 177, 185 | eqbrtrd 4675 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℕ ∧ (𝑁 − 1) ∈ ℕ)
→ seq𝑁( + , 𝐹) ⇝ (1 − (seq1( + ,
𝐹)‘(𝑁 − 1)))) |
187 | 159 | releldmi 5362 |
. . . . . . . . . . . . 13
⊢ (seq𝑁( + , 𝐹) ⇝ (1 − (seq1( + , 𝐹)‘(𝑁 − 1))) → seq𝑁( + , 𝐹) ∈ dom ⇝ ) |
188 | 186, 187 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ ∧ (𝑁 − 1) ∈ ℕ)
→ seq𝑁( + , 𝐹) ∈ dom ⇝
) |
189 | 164, 171,
188 | syl2anc 693 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ ¬
𝑁 = 1) → seq𝑁( + , 𝐹) ∈ dom ⇝ ) |
190 | 163, 189 | pm2.61dan 832 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ → seq𝑁( + , 𝐹) ∈ dom ⇝ ) |
191 | 125, 59, 145, 156, 190 | isumrecl 14496 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ →
Σ𝑗 ∈
(ℤ≥‘𝑁)(1 / (𝑗 · (𝑗 + 1))) ∈ ℝ) |
192 | 126 | nnrpd 11870 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈
(ℤ≥‘𝑁)) → 𝑗 ∈ ℝ+) |
193 | 192 | rpge0d 11876 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈
(ℤ≥‘𝑁)) → 0 ≤ 𝑗) |
194 | 146, 193 | ge0p1rpd 11902 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈
(ℤ≥‘𝑁)) → (𝑗 + 1) ∈
ℝ+) |
195 | 192, 194 | rpmulcld 11888 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈
(ℤ≥‘𝑁)) → (𝑗 · (𝑗 + 1)) ∈
ℝ+) |
196 | 123 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈
(ℤ≥‘𝑁)) → 0 ≤ 1) |
197 | 147, 195,
196 | divge0d 11912 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈
(ℤ≥‘𝑁)) → 0 ≤ (1 / (𝑗 · (𝑗 + 1)))) |
198 | 125, 59, 145, 156, 190, 197 | isumge0 14497 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ → 0 ≤
Σ𝑗 ∈
(ℤ≥‘𝑁)(1 / (𝑗 · (𝑗 + 1)))) |
199 | 120, 191,
115, 198 | leadd2dd 10642 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ →
(Σ𝑗 ∈
(1...(𝑁 − 1))(1 /
(𝑗 · (𝑗 + 1))) + 0) ≤ (Σ𝑗 ∈ (1...(𝑁 − 1))(1 / (𝑗 · (𝑗 + 1))) + Σ𝑗 ∈ (ℤ≥‘𝑁)(1 / (𝑗 · (𝑗 + 1))))) |
200 | 115 | recnd 10068 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ →
Σ𝑗 ∈ (1...(𝑁 − 1))(1 / (𝑗 · (𝑗 + 1))) ∈ ℂ) |
201 | 200 | addid1d 10236 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ →
(Σ𝑗 ∈
(1...(𝑁 − 1))(1 /
(𝑗 · (𝑗 + 1))) + 0) = Σ𝑗 ∈ (1...(𝑁 − 1))(1 / (𝑗 · (𝑗 + 1)))) |
202 | 201 | eqcomd 2628 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ →
Σ𝑗 ∈ (1...(𝑁 − 1))(1 / (𝑗 · (𝑗 + 1))) = (Σ𝑗 ∈ (1...(𝑁 − 1))(1 / (𝑗 · (𝑗 + 1))) + 0)) |
203 | | id 22 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℕ) |
204 | 144 | adantl 482 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) → (𝐹‘𝑗) = (1 / (𝑗 · (𝑗 + 1)))) |
205 | 138 | adantl 482 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) → 𝑗 ∈
ℂ) |
206 | | 1cnd 10056 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) → 1 ∈
ℂ) |
207 | 205, 206 | addcld 10059 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) → (𝑗 + 1) ∈
ℂ) |
208 | 205, 207 | mulcld 10060 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) → (𝑗 · (𝑗 + 1)) ∈ ℂ) |
209 | 141 | adantl 482 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) → 𝑗 ≠ 0) |
210 | 103 | adantl 482 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) → (𝑗 + 1) ≠ 0) |
211 | 205, 207,
209, 210 | mulne0d 10679 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) → (𝑗 · (𝑗 + 1)) ≠ 0) |
212 | 208, 211 | reccld 10794 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) → (1 /
(𝑗 · (𝑗 + 1))) ∈
ℂ) |
213 | 158, 160 | mp1i 13 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ → seq1( + ,
𝐹) ∈ dom ⇝
) |
214 | 178, 125,
203, 204, 212, 213 | isumsplit 14572 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ →
Σ𝑗 ∈ ℕ (1
/ (𝑗 · (𝑗 + 1))) = (Σ𝑗 ∈ (1...(𝑁 − 1))(1 / (𝑗 · (𝑗 + 1))) + Σ𝑗 ∈ (ℤ≥‘𝑁)(1 / (𝑗 · (𝑗 + 1))))) |
215 | 199, 202,
214 | 3brtr4d 4685 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ →
Σ𝑗 ∈ (1...(𝑁 − 1))(1 / (𝑗 · (𝑗 + 1))) ≤ Σ𝑗 ∈ ℕ (1 / (𝑗 · (𝑗 + 1)))) |
216 | | 1zzd 11408 |
. . . . . . . . 9
⊢ (⊤
→ 1 ∈ ℤ) |
217 | 144 | adantl 482 |
. . . . . . . . 9
⊢
((⊤ ∧ 𝑗
∈ ℕ) → (𝐹‘𝑗) = (1 / (𝑗 · (𝑗 + 1)))) |
218 | 180 | adantl 482 |
. . . . . . . . 9
⊢
((⊤ ∧ 𝑗
∈ ℕ) → (1 / (𝑗 · (𝑗 + 1))) ∈ ℂ) |
219 | 158 | a1i 11 |
. . . . . . . . 9
⊢ (⊤
→ seq1( + , 𝐹) ⇝
1) |
220 | 178, 216,
217, 218, 219 | isumclim 14488 |
. . . . . . . 8
⊢ (⊤
→ Σ𝑗 ∈
ℕ (1 / (𝑗 ·
(𝑗 + 1))) =
1) |
221 | 220 | trud 1493 |
. . . . . . 7
⊢
Σ𝑗 ∈
ℕ (1 / (𝑗 ·
(𝑗 + 1))) =
1 |
222 | 215, 221 | syl6breq 4694 |
. . . . . 6
⊢ (𝑁 ∈ ℕ →
Σ𝑗 ∈ (1...(𝑁 − 1))(1 / (𝑗 · (𝑗 + 1))) ≤ 1) |
223 | 115, 116,
32, 124, 222 | lemul2ad 10964 |
. . . . 5
⊢ (𝑁 ∈ ℕ → ((1 / 4)
· Σ𝑗 ∈
(1...(𝑁 − 1))(1 /
(𝑗 · (𝑗 + 1)))) ≤ ((1 / 4) ·
1)) |
224 | | 4cn 11098 |
. . . . . . . 8
⊢ 4 ∈
ℂ |
225 | 224 | a1i 11 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ → 4 ∈
ℂ) |
226 | 117 | a1i 11 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ → 0 <
4) |
227 | 226 | gt0ne0d 10592 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ → 4 ≠
0) |
228 | 225, 227 | reccld 10794 |
. . . . . 6
⊢ (𝑁 ∈ ℕ → (1 / 4)
∈ ℂ) |
229 | 107 | recnd 10068 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ (1...(𝑁 − 1))) → (1 / (𝑗 · (𝑗 + 1))) ∈ ℂ) |
230 | 64, 228, 229 | fsummulc2 14516 |
. . . . 5
⊢ (𝑁 ∈ ℕ → ((1 / 4)
· Σ𝑗 ∈
(1...(𝑁 − 1))(1 /
(𝑗 · (𝑗 + 1)))) = Σ𝑗 ∈ (1...(𝑁 − 1))((1 / 4) · (1 / (𝑗 · (𝑗 + 1))))) |
231 | 228 | mulid1d 10057 |
. . . . 5
⊢ (𝑁 ∈ ℕ → ((1 / 4)
· 1) = (1 / 4)) |
232 | 223, 230,
231 | 3brtr3d 4684 |
. . . 4
⊢ (𝑁 ∈ ℕ →
Σ𝑗 ∈ (1...(𝑁 − 1))((1 / 4) · (1
/ (𝑗 · (𝑗 + 1)))) ≤ (1 /
4)) |
233 | 93, 109, 32, 114, 232 | letrd 10194 |
. . 3
⊢ (𝑁 ∈ ℕ →
Σ𝑗 ∈ (1...(𝑁 − 1))((𝐵‘𝑗) − (𝐵‘(𝑗 + 1))) ≤ (1 / 4)) |
234 | 63, 233 | eqbrtrd 4675 |
. 2
⊢ (𝑁 ∈ ℕ → ((𝐵‘1) − (𝐵‘𝑁)) ≤ (1 / 4)) |
235 | 18, 28, 32, 234 | subled 10630 |
1
⊢ (𝑁 ∈ ℕ → ((𝐵‘1) − (1 / 4)) ≤
(𝐵‘𝑁)) |