Step | Hyp | Ref
| Expression |
1 | | 1nn 11730 |
. . . . 5
⊢ 1 ∈
ℕ |
2 | | stirlinglem12.1 |
. . . . . . 7
⊢ 𝐴 = (𝑛 ∈ ℕ ↦ ((!‘𝑛) / ((√‘(2 ·
𝑛)) · ((𝑛 / e)↑𝑛)))) |
3 | 2 | stirlinglem2 43181 |
. . . . . 6
⊢ (1 ∈
ℕ → (𝐴‘1)
∈ ℝ+) |
4 | | relogcl 25322 |
. . . . . 6
⊢ ((𝐴‘1) ∈
ℝ+ → (log‘(𝐴‘1)) ∈ ℝ) |
5 | 1, 3, 4 | mp2b 10 |
. . . . 5
⊢
(log‘(𝐴‘1)) ∈ ℝ |
6 | | nfcv 2900 |
. . . . . 6
⊢
Ⅎ𝑛1 |
7 | | nfcv 2900 |
. . . . . . 7
⊢
Ⅎ𝑛log |
8 | | nfmpt1 5129 |
. . . . . . . . 9
⊢
Ⅎ𝑛(𝑛 ∈ ℕ ↦ ((!‘𝑛) / ((√‘(2 ·
𝑛)) · ((𝑛 / e)↑𝑛)))) |
9 | 2, 8 | nfcxfr 2898 |
. . . . . . . 8
⊢
Ⅎ𝑛𝐴 |
10 | 9, 6 | nffv 6687 |
. . . . . . 7
⊢
Ⅎ𝑛(𝐴‘1) |
11 | 7, 10 | nffv 6687 |
. . . . . 6
⊢
Ⅎ𝑛(log‘(𝐴‘1)) |
12 | | 2fveq3 6682 |
. . . . . 6
⊢ (𝑛 = 1 → (log‘(𝐴‘𝑛)) = (log‘(𝐴‘1))) |
13 | | stirlinglem12.2 |
. . . . . 6
⊢ 𝐵 = (𝑛 ∈ ℕ ↦ (log‘(𝐴‘𝑛))) |
14 | 6, 11, 12, 13 | fvmptf 6799 |
. . . . 5
⊢ ((1
∈ ℕ ∧ (log‘(𝐴‘1)) ∈ ℝ) → (𝐵‘1) = (log‘(𝐴‘1))) |
15 | 1, 5, 14 | mp2an 692 |
. . . 4
⊢ (𝐵‘1) = (log‘(𝐴‘1)) |
16 | 15, 5 | eqeltri 2830 |
. . 3
⊢ (𝐵‘1) ∈
ℝ |
17 | 16 | a1i 11 |
. 2
⊢ (𝑁 ∈ ℕ → (𝐵‘1) ∈
ℝ) |
18 | 2 | stirlinglem2 43181 |
. . . . 5
⊢ (𝑁 ∈ ℕ → (𝐴‘𝑁) ∈
ℝ+) |
19 | 18 | relogcld 25369 |
. . . 4
⊢ (𝑁 ∈ ℕ →
(log‘(𝐴‘𝑁)) ∈
ℝ) |
20 | | nfcv 2900 |
. . . . 5
⊢
Ⅎ𝑛𝑁 |
21 | 9, 20 | nffv 6687 |
. . . . . 6
⊢
Ⅎ𝑛(𝐴‘𝑁) |
22 | 7, 21 | nffv 6687 |
. . . . 5
⊢
Ⅎ𝑛(log‘(𝐴‘𝑁)) |
23 | | 2fveq3 6682 |
. . . . 5
⊢ (𝑛 = 𝑁 → (log‘(𝐴‘𝑛)) = (log‘(𝐴‘𝑁))) |
24 | 20, 22, 23, 13 | fvmptf 6799 |
. . . 4
⊢ ((𝑁 ∈ ℕ ∧
(log‘(𝐴‘𝑁)) ∈ ℝ) → (𝐵‘𝑁) = (log‘(𝐴‘𝑁))) |
25 | 19, 24 | mpdan 687 |
. . 3
⊢ (𝑁 ∈ ℕ → (𝐵‘𝑁) = (log‘(𝐴‘𝑁))) |
26 | 25, 19 | eqeltrd 2834 |
. 2
⊢ (𝑁 ∈ ℕ → (𝐵‘𝑁) ∈ ℝ) |
27 | | 4re 11803 |
. . . 4
⊢ 4 ∈
ℝ |
28 | | 4ne0 11827 |
. . . 4
⊢ 4 ≠
0 |
29 | 27, 28 | rereccli 11486 |
. . 3
⊢ (1 / 4)
∈ ℝ |
30 | 29 | a1i 11 |
. 2
⊢ (𝑁 ∈ ℕ → (1 / 4)
∈ ℝ) |
31 | | fveq2 6677 |
. . . . 5
⊢ (𝑘 = 𝑗 → (𝐵‘𝑘) = (𝐵‘𝑗)) |
32 | | fveq2 6677 |
. . . . 5
⊢ (𝑘 = (𝑗 + 1) → (𝐵‘𝑘) = (𝐵‘(𝑗 + 1))) |
33 | | fveq2 6677 |
. . . . 5
⊢ (𝑘 = 1 → (𝐵‘𝑘) = (𝐵‘1)) |
34 | | fveq2 6677 |
. . . . 5
⊢ (𝑘 = 𝑁 → (𝐵‘𝑘) = (𝐵‘𝑁)) |
35 | | elnnuz 12367 |
. . . . . 6
⊢ (𝑁 ∈ ℕ ↔ 𝑁 ∈
(ℤ≥‘1)) |
36 | 35 | biimpi 219 |
. . . . 5
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
(ℤ≥‘1)) |
37 | | elfznn 13030 |
. . . . . . . 8
⊢ (𝑘 ∈ (1...𝑁) → 𝑘 ∈ ℕ) |
38 | 2 | stirlinglem2 43181 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ℕ → (𝐴‘𝑘) ∈
ℝ+) |
39 | 37, 38 | syl 17 |
. . . . . . . . 9
⊢ (𝑘 ∈ (1...𝑁) → (𝐴‘𝑘) ∈
ℝ+) |
40 | 39 | relogcld 25369 |
. . . . . . . 8
⊢ (𝑘 ∈ (1...𝑁) → (log‘(𝐴‘𝑘)) ∈ ℝ) |
41 | | nfcv 2900 |
. . . . . . . . 9
⊢
Ⅎ𝑛𝑘 |
42 | 9, 41 | nffv 6687 |
. . . . . . . . . 10
⊢
Ⅎ𝑛(𝐴‘𝑘) |
43 | 7, 42 | nffv 6687 |
. . . . . . . . 9
⊢
Ⅎ𝑛(log‘(𝐴‘𝑘)) |
44 | | 2fveq3 6682 |
. . . . . . . . 9
⊢ (𝑛 = 𝑘 → (log‘(𝐴‘𝑛)) = (log‘(𝐴‘𝑘))) |
45 | 41, 43, 44, 13 | fvmptf 6799 |
. . . . . . . 8
⊢ ((𝑘 ∈ ℕ ∧
(log‘(𝐴‘𝑘)) ∈ ℝ) → (𝐵‘𝑘) = (log‘(𝐴‘𝑘))) |
46 | 37, 40, 45 | syl2anc 587 |
. . . . . . 7
⊢ (𝑘 ∈ (1...𝑁) → (𝐵‘𝑘) = (log‘(𝐴‘𝑘))) |
47 | 46 | adantl 485 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (1...𝑁)) → (𝐵‘𝑘) = (log‘(𝐴‘𝑘))) |
48 | 39 | rpcnd 12519 |
. . . . . . . 8
⊢ (𝑘 ∈ (1...𝑁) → (𝐴‘𝑘) ∈ ℂ) |
49 | 48 | adantl 485 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (1...𝑁)) → (𝐴‘𝑘) ∈ ℂ) |
50 | 38 | rpne0d 12522 |
. . . . . . . . 9
⊢ (𝑘 ∈ ℕ → (𝐴‘𝑘) ≠ 0) |
51 | 37, 50 | syl 17 |
. . . . . . . 8
⊢ (𝑘 ∈ (1...𝑁) → (𝐴‘𝑘) ≠ 0) |
52 | 51 | adantl 485 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (1...𝑁)) → (𝐴‘𝑘) ≠ 0) |
53 | 49, 52 | logcld 25317 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (1...𝑁)) → (log‘(𝐴‘𝑘)) ∈ ℂ) |
54 | 47, 53 | eqeltrd 2834 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (1...𝑁)) → (𝐵‘𝑘) ∈ ℂ) |
55 | 31, 32, 33, 34, 36, 54 | telfsumo 15253 |
. . . 4
⊢ (𝑁 ∈ ℕ →
Σ𝑗 ∈ (1..^𝑁)((𝐵‘𝑗) − (𝐵‘(𝑗 + 1))) = ((𝐵‘1) − (𝐵‘𝑁))) |
56 | | nnz 12088 |
. . . . . 6
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℤ) |
57 | | fzoval 13133 |
. . . . . 6
⊢ (𝑁 ∈ ℤ →
(1..^𝑁) = (1...(𝑁 − 1))) |
58 | 56, 57 | syl 17 |
. . . . 5
⊢ (𝑁 ∈ ℕ →
(1..^𝑁) = (1...(𝑁 − 1))) |
59 | 58 | sumeq1d 15154 |
. . . 4
⊢ (𝑁 ∈ ℕ →
Σ𝑗 ∈ (1..^𝑁)((𝐵‘𝑗) − (𝐵‘(𝑗 + 1))) = Σ𝑗 ∈ (1...(𝑁 − 1))((𝐵‘𝑗) − (𝐵‘(𝑗 + 1)))) |
60 | 55, 59 | eqtr3d 2776 |
. . 3
⊢ (𝑁 ∈ ℕ → ((𝐵‘1) − (𝐵‘𝑁)) = Σ𝑗 ∈ (1...(𝑁 − 1))((𝐵‘𝑗) − (𝐵‘(𝑗 + 1)))) |
61 | | fzfid 13435 |
. . . . 5
⊢ (𝑁 ∈ ℕ →
(1...(𝑁 − 1)) ∈
Fin) |
62 | | elfznn 13030 |
. . . . . . . 8
⊢ (𝑗 ∈ (1...(𝑁 − 1)) → 𝑗 ∈ ℕ) |
63 | 62 | adantl 485 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ (1...(𝑁 − 1))) → 𝑗 ∈ ℕ) |
64 | 2 | stirlinglem2 43181 |
. . . . . . . . . 10
⊢ (𝑗 ∈ ℕ → (𝐴‘𝑗) ∈
ℝ+) |
65 | 64 | relogcld 25369 |
. . . . . . . . 9
⊢ (𝑗 ∈ ℕ →
(log‘(𝐴‘𝑗)) ∈
ℝ) |
66 | | nfcv 2900 |
. . . . . . . . . 10
⊢
Ⅎ𝑛𝑗 |
67 | 9, 66 | nffv 6687 |
. . . . . . . . . . 11
⊢
Ⅎ𝑛(𝐴‘𝑗) |
68 | 7, 67 | nffv 6687 |
. . . . . . . . . 10
⊢
Ⅎ𝑛(log‘(𝐴‘𝑗)) |
69 | | 2fveq3 6682 |
. . . . . . . . . 10
⊢ (𝑛 = 𝑗 → (log‘(𝐴‘𝑛)) = (log‘(𝐴‘𝑗))) |
70 | 66, 68, 69, 13 | fvmptf 6799 |
. . . . . . . . 9
⊢ ((𝑗 ∈ ℕ ∧
(log‘(𝐴‘𝑗)) ∈ ℝ) → (𝐵‘𝑗) = (log‘(𝐴‘𝑗))) |
71 | 65, 70 | mpdan 687 |
. . . . . . . 8
⊢ (𝑗 ∈ ℕ → (𝐵‘𝑗) = (log‘(𝐴‘𝑗))) |
72 | 71, 65 | eqeltrd 2834 |
. . . . . . 7
⊢ (𝑗 ∈ ℕ → (𝐵‘𝑗) ∈ ℝ) |
73 | 63, 72 | syl 17 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ (1...(𝑁 − 1))) → (𝐵‘𝑗) ∈ ℝ) |
74 | | peano2nn 11731 |
. . . . . . . . . 10
⊢ (𝑗 ∈ ℕ → (𝑗 + 1) ∈
ℕ) |
75 | 2 | stirlinglem2 43181 |
. . . . . . . . . . . 12
⊢ ((𝑗 + 1) ∈ ℕ →
(𝐴‘(𝑗 + 1)) ∈
ℝ+) |
76 | 74, 75 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑗 ∈ ℕ → (𝐴‘(𝑗 + 1)) ∈
ℝ+) |
77 | 76 | relogcld 25369 |
. . . . . . . . . 10
⊢ (𝑗 ∈ ℕ →
(log‘(𝐴‘(𝑗 + 1))) ∈
ℝ) |
78 | | nfcv 2900 |
. . . . . . . . . . 11
⊢
Ⅎ𝑛(𝑗 + 1) |
79 | 9, 78 | nffv 6687 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑛(𝐴‘(𝑗 + 1)) |
80 | 7, 79 | nffv 6687 |
. . . . . . . . . . 11
⊢
Ⅎ𝑛(log‘(𝐴‘(𝑗 + 1))) |
81 | | 2fveq3 6682 |
. . . . . . . . . . 11
⊢ (𝑛 = (𝑗 + 1) → (log‘(𝐴‘𝑛)) = (log‘(𝐴‘(𝑗 + 1)))) |
82 | 78, 80, 81, 13 | fvmptf 6799 |
. . . . . . . . . 10
⊢ (((𝑗 + 1) ∈ ℕ ∧
(log‘(𝐴‘(𝑗 + 1))) ∈ ℝ) →
(𝐵‘(𝑗 + 1)) = (log‘(𝐴‘(𝑗 + 1)))) |
83 | 74, 77, 82 | syl2anc 587 |
. . . . . . . . 9
⊢ (𝑗 ∈ ℕ → (𝐵‘(𝑗 + 1)) = (log‘(𝐴‘(𝑗 + 1)))) |
84 | 83, 77 | eqeltrd 2834 |
. . . . . . . 8
⊢ (𝑗 ∈ ℕ → (𝐵‘(𝑗 + 1)) ∈ ℝ) |
85 | 62, 84 | syl 17 |
. . . . . . 7
⊢ (𝑗 ∈ (1...(𝑁 − 1)) → (𝐵‘(𝑗 + 1)) ∈ ℝ) |
86 | 85 | adantl 485 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ (1...(𝑁 − 1))) → (𝐵‘(𝑗 + 1)) ∈ ℝ) |
87 | 73, 86 | resubcld 11149 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ (1...(𝑁 − 1))) → ((𝐵‘𝑗) − (𝐵‘(𝑗 + 1))) ∈ ℝ) |
88 | 61, 87 | fsumrecl 15187 |
. . . 4
⊢ (𝑁 ∈ ℕ →
Σ𝑗 ∈ (1...(𝑁 − 1))((𝐵‘𝑗) − (𝐵‘(𝑗 + 1))) ∈ ℝ) |
89 | 29 | a1i 11 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ (1...(𝑁 − 1))) → (1 / 4) ∈
ℝ) |
90 | 62 | nnred 11734 |
. . . . . . . . 9
⊢ (𝑗 ∈ (1...(𝑁 − 1)) → 𝑗 ∈ ℝ) |
91 | | 1red 10723 |
. . . . . . . . . 10
⊢ (𝑗 ∈ (1...(𝑁 − 1)) → 1 ∈
ℝ) |
92 | 90, 91 | readdcld 10751 |
. . . . . . . . 9
⊢ (𝑗 ∈ (1...(𝑁 − 1)) → (𝑗 + 1) ∈ ℝ) |
93 | 90, 92 | remulcld 10752 |
. . . . . . . 8
⊢ (𝑗 ∈ (1...(𝑁 − 1)) → (𝑗 · (𝑗 + 1)) ∈ ℝ) |
94 | 90 | recnd 10750 |
. . . . . . . . 9
⊢ (𝑗 ∈ (1...(𝑁 − 1)) → 𝑗 ∈ ℂ) |
95 | | 1cnd 10717 |
. . . . . . . . . 10
⊢ (𝑗 ∈ (1...(𝑁 − 1)) → 1 ∈
ℂ) |
96 | 94, 95 | addcld 10741 |
. . . . . . . . 9
⊢ (𝑗 ∈ (1...(𝑁 − 1)) → (𝑗 + 1) ∈ ℂ) |
97 | 62 | nnne0d 11769 |
. . . . . . . . 9
⊢ (𝑗 ∈ (1...(𝑁 − 1)) → 𝑗 ≠ 0) |
98 | 74 | nnne0d 11769 |
. . . . . . . . . 10
⊢ (𝑗 ∈ ℕ → (𝑗 + 1) ≠ 0) |
99 | 62, 98 | syl 17 |
. . . . . . . . 9
⊢ (𝑗 ∈ (1...(𝑁 − 1)) → (𝑗 + 1) ≠ 0) |
100 | 94, 96, 97, 99 | mulne0d 11373 |
. . . . . . . 8
⊢ (𝑗 ∈ (1...(𝑁 − 1)) → (𝑗 · (𝑗 + 1)) ≠ 0) |
101 | 93, 100 | rereccld 11548 |
. . . . . . 7
⊢ (𝑗 ∈ (1...(𝑁 − 1)) → (1 / (𝑗 · (𝑗 + 1))) ∈ ℝ) |
102 | 101 | adantl 485 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ (1...(𝑁 − 1))) → (1 / (𝑗 · (𝑗 + 1))) ∈ ℝ) |
103 | 89, 102 | remulcld 10752 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ (1...(𝑁 − 1))) → ((1 / 4) · (1 /
(𝑗 · (𝑗 + 1)))) ∈
ℝ) |
104 | 61, 103 | fsumrecl 15187 |
. . . 4
⊢ (𝑁 ∈ ℕ →
Σ𝑗 ∈ (1...(𝑁 − 1))((1 / 4) · (1
/ (𝑗 · (𝑗 + 1)))) ∈
ℝ) |
105 | | eqid 2739 |
. . . . . . 7
⊢ (𝑖 ∈ ℕ ↦ ((1 /
((2 · 𝑖) + 1))
· ((1 / ((2 · 𝑗) + 1))↑(2 · 𝑖)))) = (𝑖 ∈ ℕ ↦ ((1 / ((2 ·
𝑖) + 1)) · ((1 / ((2
· 𝑗) + 1))↑(2
· 𝑖)))) |
106 | | eqid 2739 |
. . . . . . 7
⊢ (𝑖 ∈ ℕ ↦ ((1 /
(((2 · 𝑗) +
1)↑2))↑𝑖)) =
(𝑖 ∈ ℕ ↦
((1 / (((2 · 𝑗) +
1)↑2))↑𝑖)) |
107 | 2, 13, 105, 106 | stirlinglem10 43189 |
. . . . . 6
⊢ (𝑗 ∈ ℕ → ((𝐵‘𝑗) − (𝐵‘(𝑗 + 1))) ≤ ((1 / 4) · (1 / (𝑗 · (𝑗 + 1))))) |
108 | 63, 107 | syl 17 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ (1...(𝑁 − 1))) → ((𝐵‘𝑗) − (𝐵‘(𝑗 + 1))) ≤ ((1 / 4) · (1 / (𝑗 · (𝑗 + 1))))) |
109 | 61, 87, 103, 108 | fsumle 15250 |
. . . 4
⊢ (𝑁 ∈ ℕ →
Σ𝑗 ∈ (1...(𝑁 − 1))((𝐵‘𝑗) − (𝐵‘(𝑗 + 1))) ≤ Σ𝑗 ∈ (1...(𝑁 − 1))((1 / 4) · (1 / (𝑗 · (𝑗 + 1))))) |
110 | 61, 102 | fsumrecl 15187 |
. . . . . 6
⊢ (𝑁 ∈ ℕ →
Σ𝑗 ∈ (1...(𝑁 − 1))(1 / (𝑗 · (𝑗 + 1))) ∈ ℝ) |
111 | | 1red 10723 |
. . . . . 6
⊢ (𝑁 ∈ ℕ → 1 ∈
ℝ) |
112 | | 4pos 11826 |
. . . . . . . . 9
⊢ 0 <
4 |
113 | 27, 112 | elrpii 12478 |
. . . . . . . 8
⊢ 4 ∈
ℝ+ |
114 | 113 | a1i 11 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ → 4 ∈
ℝ+) |
115 | | 0red 10725 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ → 0 ∈
ℝ) |
116 | | 0lt1 11243 |
. . . . . . . . 9
⊢ 0 <
1 |
117 | 116 | a1i 11 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ → 0 <
1) |
118 | 115, 111,
117 | ltled 10869 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ → 0 ≤
1) |
119 | 111, 114,
118 | divge0d 12557 |
. . . . . 6
⊢ (𝑁 ∈ ℕ → 0 ≤ (1
/ 4)) |
120 | | eqid 2739 |
. . . . . . . . . 10
⊢
(ℤ≥‘𝑁) = (ℤ≥‘𝑁) |
121 | | eluznn 12403 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈
(ℤ≥‘𝑁)) → 𝑗 ∈ ℕ) |
122 | | stirlinglem12.3 |
. . . . . . . . . . . . 13
⊢ 𝐹 = (𝑛 ∈ ℕ ↦ (1 / (𝑛 · (𝑛 + 1)))) |
123 | 122 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝑗 ∈ ℕ → 𝐹 = (𝑛 ∈ ℕ ↦ (1 / (𝑛 · (𝑛 + 1))))) |
124 | | simpr 488 |
. . . . . . . . . . . . . 14
⊢ ((𝑗 ∈ ℕ ∧ 𝑛 = 𝑗) → 𝑛 = 𝑗) |
125 | 124 | oveq1d 7188 |
. . . . . . . . . . . . . 14
⊢ ((𝑗 ∈ ℕ ∧ 𝑛 = 𝑗) → (𝑛 + 1) = (𝑗 + 1)) |
126 | 124, 125 | oveq12d 7191 |
. . . . . . . . . . . . 13
⊢ ((𝑗 ∈ ℕ ∧ 𝑛 = 𝑗) → (𝑛 · (𝑛 + 1)) = (𝑗 · (𝑗 + 1))) |
127 | 126 | oveq2d 7189 |
. . . . . . . . . . . 12
⊢ ((𝑗 ∈ ℕ ∧ 𝑛 = 𝑗) → (1 / (𝑛 · (𝑛 + 1))) = (1 / (𝑗 · (𝑗 + 1)))) |
128 | | id 22 |
. . . . . . . . . . . 12
⊢ (𝑗 ∈ ℕ → 𝑗 ∈
ℕ) |
129 | | nnre 11726 |
. . . . . . . . . . . . . 14
⊢ (𝑗 ∈ ℕ → 𝑗 ∈
ℝ) |
130 | | 1red 10723 |
. . . . . . . . . . . . . . 15
⊢ (𝑗 ∈ ℕ → 1 ∈
ℝ) |
131 | 129, 130 | readdcld 10751 |
. . . . . . . . . . . . . 14
⊢ (𝑗 ∈ ℕ → (𝑗 + 1) ∈
ℝ) |
132 | 129, 131 | remulcld 10752 |
. . . . . . . . . . . . 13
⊢ (𝑗 ∈ ℕ → (𝑗 · (𝑗 + 1)) ∈ ℝ) |
133 | | nncn 11727 |
. . . . . . . . . . . . . 14
⊢ (𝑗 ∈ ℕ → 𝑗 ∈
ℂ) |
134 | | 1cnd 10717 |
. . . . . . . . . . . . . . 15
⊢ (𝑗 ∈ ℕ → 1 ∈
ℂ) |
135 | 133, 134 | addcld 10741 |
. . . . . . . . . . . . . 14
⊢ (𝑗 ∈ ℕ → (𝑗 + 1) ∈
ℂ) |
136 | | nnne0 11753 |
. . . . . . . . . . . . . 14
⊢ (𝑗 ∈ ℕ → 𝑗 ≠ 0) |
137 | 133, 135,
136, 98 | mulne0d 11373 |
. . . . . . . . . . . . 13
⊢ (𝑗 ∈ ℕ → (𝑗 · (𝑗 + 1)) ≠ 0) |
138 | 132, 137 | rereccld 11548 |
. . . . . . . . . . . 12
⊢ (𝑗 ∈ ℕ → (1 /
(𝑗 · (𝑗 + 1))) ∈
ℝ) |
139 | 123, 127,
128, 138 | fvmptd 6785 |
. . . . . . . . . . 11
⊢ (𝑗 ∈ ℕ → (𝐹‘𝑗) = (1 / (𝑗 · (𝑗 + 1)))) |
140 | 121, 139 | syl 17 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈
(ℤ≥‘𝑁)) → (𝐹‘𝑗) = (1 / (𝑗 · (𝑗 + 1)))) |
141 | 121 | nnred 11734 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈
(ℤ≥‘𝑁)) → 𝑗 ∈ ℝ) |
142 | | 1red 10723 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈
(ℤ≥‘𝑁)) → 1 ∈ ℝ) |
143 | 141, 142 | readdcld 10751 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈
(ℤ≥‘𝑁)) → (𝑗 + 1) ∈ ℝ) |
144 | 141, 143 | remulcld 10752 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈
(ℤ≥‘𝑁)) → (𝑗 · (𝑗 + 1)) ∈ ℝ) |
145 | 141 | recnd 10750 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈
(ℤ≥‘𝑁)) → 𝑗 ∈ ℂ) |
146 | | 1cnd 10717 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈
(ℤ≥‘𝑁)) → 1 ∈ ℂ) |
147 | 145, 146 | addcld 10741 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈
(ℤ≥‘𝑁)) → (𝑗 + 1) ∈ ℂ) |
148 | 121 | nnne0d 11769 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈
(ℤ≥‘𝑁)) → 𝑗 ≠ 0) |
149 | 121, 98 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈
(ℤ≥‘𝑁)) → (𝑗 + 1) ≠ 0) |
150 | 145, 147,
148, 149 | mulne0d 11373 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈
(ℤ≥‘𝑁)) → (𝑗 · (𝑗 + 1)) ≠ 0) |
151 | 144, 150 | rereccld 11548 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈
(ℤ≥‘𝑁)) → (1 / (𝑗 · (𝑗 + 1))) ∈ ℝ) |
152 | | seqeq1 13466 |
. . . . . . . . . . . . 13
⊢ (𝑁 = 1 → seq𝑁( + , 𝐹) = seq1( + , 𝐹)) |
153 | 122 | trireciplem 15313 |
. . . . . . . . . . . . . 14
⊢ seq1( + ,
𝐹) ⇝
1 |
154 | | climrel 14942 |
. . . . . . . . . . . . . . 15
⊢ Rel
⇝ |
155 | 154 | releldmi 5792 |
. . . . . . . . . . . . . 14
⊢ (seq1( +
, 𝐹) ⇝ 1 → seq1(
+ , 𝐹) ∈ dom ⇝
) |
156 | 153, 155 | mp1i 13 |
. . . . . . . . . . . . 13
⊢ (𝑁 = 1 → seq1( + , 𝐹) ∈ dom ⇝
) |
157 | 152, 156 | eqeltrd 2834 |
. . . . . . . . . . . 12
⊢ (𝑁 = 1 → seq𝑁( + , 𝐹) ∈ dom ⇝ ) |
158 | 157 | adantl 485 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ 𝑁 = 1) → seq𝑁( + , 𝐹) ∈ dom ⇝ ) |
159 | | simpl 486 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ ∧ ¬
𝑁 = 1) → 𝑁 ∈
ℕ) |
160 | | simpr 488 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℕ ∧ ¬
𝑁 = 1) → ¬ 𝑁 = 1) |
161 | | elnn1uz2 12410 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈ ℕ ↔ (𝑁 = 1 ∨ 𝑁 ∈
(ℤ≥‘2))) |
162 | 159, 161 | sylib 221 |
. . . . . . . . . . . . . . 15
⊢ ((𝑁 ∈ ℕ ∧ ¬
𝑁 = 1) → (𝑁 = 1 ∨ 𝑁 ∈
(ℤ≥‘2))) |
163 | 162 | ord 863 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℕ ∧ ¬
𝑁 = 1) → (¬ 𝑁 = 1 → 𝑁 ∈
(ℤ≥‘2))) |
164 | 160, 163 | mpd 15 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℕ ∧ ¬
𝑁 = 1) → 𝑁 ∈
(ℤ≥‘2)) |
165 | | uz2m1nn 12408 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈
(ℤ≥‘2) → (𝑁 − 1) ∈ ℕ) |
166 | 164, 165 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ ∧ ¬
𝑁 = 1) → (𝑁 − 1) ∈
ℕ) |
167 | | nncn 11727 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℂ) |
168 | 167 | adantr 484 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑁 ∈ ℕ ∧ (𝑁 − 1) ∈ ℕ)
→ 𝑁 ∈
ℂ) |
169 | | 1cnd 10717 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑁 ∈ ℕ ∧ (𝑁 − 1) ∈ ℕ)
→ 1 ∈ ℂ) |
170 | 168, 169 | npcand 11082 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑁 ∈ ℕ ∧ (𝑁 − 1) ∈ ℕ)
→ ((𝑁 − 1) + 1)
= 𝑁) |
171 | 170 | eqcomd 2745 |
. . . . . . . . . . . . . . 15
⊢ ((𝑁 ∈ ℕ ∧ (𝑁 − 1) ∈ ℕ)
→ 𝑁 = ((𝑁 − 1) +
1)) |
172 | 171 | seqeq1d 13469 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℕ ∧ (𝑁 − 1) ∈ ℕ)
→ seq𝑁( + , 𝐹) = seq((𝑁 − 1) + 1)( + , 𝐹)) |
173 | | nnuz 12366 |
. . . . . . . . . . . . . . . 16
⊢ ℕ =
(ℤ≥‘1) |
174 | | id 22 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑁 − 1) ∈ ℕ
→ (𝑁 − 1) ∈
ℕ) |
175 | 138 | recnd 10750 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑗 ∈ ℕ → (1 /
(𝑗 · (𝑗 + 1))) ∈
ℂ) |
176 | 139, 175 | eqeltrd 2834 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑗 ∈ ℕ → (𝐹‘𝑗) ∈ ℂ) |
177 | 176 | adantl 485 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑁 − 1) ∈ ℕ ∧
𝑗 ∈ ℕ) →
(𝐹‘𝑗) ∈ ℂ) |
178 | 153 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑁 − 1) ∈ ℕ
→ seq1( + , 𝐹) ⇝
1) |
179 | 173, 174,
177, 178 | clim2ser 15107 |
. . . . . . . . . . . . . . 15
⊢ ((𝑁 − 1) ∈ ℕ
→ seq((𝑁 − 1) +
1)( + , 𝐹) ⇝ (1
− (seq1( + , 𝐹)‘(𝑁 − 1)))) |
180 | 179 | adantl 485 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℕ ∧ (𝑁 − 1) ∈ ℕ)
→ seq((𝑁 − 1) +
1)( + , 𝐹) ⇝ (1
− (seq1( + , 𝐹)‘(𝑁 − 1)))) |
181 | 172, 180 | eqbrtrd 5053 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℕ ∧ (𝑁 − 1) ∈ ℕ)
→ seq𝑁( + , 𝐹) ⇝ (1 − (seq1( + ,
𝐹)‘(𝑁 − 1)))) |
182 | 154 | releldmi 5792 |
. . . . . . . . . . . . 13
⊢ (seq𝑁( + , 𝐹) ⇝ (1 − (seq1( + , 𝐹)‘(𝑁 − 1))) → seq𝑁( + , 𝐹) ∈ dom ⇝ ) |
183 | 181, 182 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ ∧ (𝑁 − 1) ∈ ℕ)
→ seq𝑁( + , 𝐹) ∈ dom ⇝
) |
184 | 159, 166,
183 | syl2anc 587 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ ¬
𝑁 = 1) → seq𝑁( + , 𝐹) ∈ dom ⇝ ) |
185 | 158, 184 | pm2.61dan 813 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ → seq𝑁( + , 𝐹) ∈ dom ⇝ ) |
186 | 120, 56, 140, 151, 185 | isumrecl 15216 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ →
Σ𝑗 ∈
(ℤ≥‘𝑁)(1 / (𝑗 · (𝑗 + 1))) ∈ ℝ) |
187 | 121 | nnrpd 12515 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈
(ℤ≥‘𝑁)) → 𝑗 ∈ ℝ+) |
188 | 187 | rpge0d 12521 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈
(ℤ≥‘𝑁)) → 0 ≤ 𝑗) |
189 | 141, 188 | ge0p1rpd 12547 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈
(ℤ≥‘𝑁)) → (𝑗 + 1) ∈
ℝ+) |
190 | 187, 189 | rpmulcld 12533 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈
(ℤ≥‘𝑁)) → (𝑗 · (𝑗 + 1)) ∈
ℝ+) |
191 | 118 | adantr 484 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈
(ℤ≥‘𝑁)) → 0 ≤ 1) |
192 | 142, 190,
191 | divge0d 12557 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈
(ℤ≥‘𝑁)) → 0 ≤ (1 / (𝑗 · (𝑗 + 1)))) |
193 | 120, 56, 140, 151, 185, 192 | isumge0 15217 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ → 0 ≤
Σ𝑗 ∈
(ℤ≥‘𝑁)(1 / (𝑗 · (𝑗 + 1)))) |
194 | 115, 186,
110, 193 | leadd2dd 11336 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ →
(Σ𝑗 ∈
(1...(𝑁 − 1))(1 /
(𝑗 · (𝑗 + 1))) + 0) ≤ (Σ𝑗 ∈ (1...(𝑁 − 1))(1 / (𝑗 · (𝑗 + 1))) + Σ𝑗 ∈ (ℤ≥‘𝑁)(1 / (𝑗 · (𝑗 + 1))))) |
195 | 110 | recnd 10750 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ →
Σ𝑗 ∈ (1...(𝑁 − 1))(1 / (𝑗 · (𝑗 + 1))) ∈ ℂ) |
196 | 195 | addid1d 10921 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ →
(Σ𝑗 ∈
(1...(𝑁 − 1))(1 /
(𝑗 · (𝑗 + 1))) + 0) = Σ𝑗 ∈ (1...(𝑁 − 1))(1 / (𝑗 · (𝑗 + 1)))) |
197 | 196 | eqcomd 2745 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ →
Σ𝑗 ∈ (1...(𝑁 − 1))(1 / (𝑗 · (𝑗 + 1))) = (Σ𝑗 ∈ (1...(𝑁 − 1))(1 / (𝑗 · (𝑗 + 1))) + 0)) |
198 | | id 22 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℕ) |
199 | 139 | adantl 485 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) → (𝐹‘𝑗) = (1 / (𝑗 · (𝑗 + 1)))) |
200 | 133 | adantl 485 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) → 𝑗 ∈
ℂ) |
201 | | 1cnd 10717 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) → 1 ∈
ℂ) |
202 | 200, 201 | addcld 10741 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) → (𝑗 + 1) ∈
ℂ) |
203 | 200, 202 | mulcld 10742 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) → (𝑗 · (𝑗 + 1)) ∈ ℂ) |
204 | 136 | adantl 485 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) → 𝑗 ≠ 0) |
205 | 98 | adantl 485 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) → (𝑗 + 1) ≠ 0) |
206 | 200, 202,
204, 205 | mulne0d 11373 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) → (𝑗 · (𝑗 + 1)) ≠ 0) |
207 | 203, 206 | reccld 11490 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) → (1 /
(𝑗 · (𝑗 + 1))) ∈
ℂ) |
208 | 153, 155 | mp1i 13 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ → seq1( + ,
𝐹) ∈ dom ⇝
) |
209 | 173, 120,
198, 199, 207, 208 | isumsplit 15291 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ →
Σ𝑗 ∈ ℕ (1
/ (𝑗 · (𝑗 + 1))) = (Σ𝑗 ∈ (1...(𝑁 − 1))(1 / (𝑗 · (𝑗 + 1))) + Σ𝑗 ∈ (ℤ≥‘𝑁)(1 / (𝑗 · (𝑗 + 1))))) |
210 | 194, 197,
209 | 3brtr4d 5063 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ →
Σ𝑗 ∈ (1...(𝑁 − 1))(1 / (𝑗 · (𝑗 + 1))) ≤ Σ𝑗 ∈ ℕ (1 / (𝑗 · (𝑗 + 1)))) |
211 | | 1zzd 12097 |
. . . . . . . . 9
⊢ (⊤
→ 1 ∈ ℤ) |
212 | 139 | adantl 485 |
. . . . . . . . 9
⊢
((⊤ ∧ 𝑗
∈ ℕ) → (𝐹‘𝑗) = (1 / (𝑗 · (𝑗 + 1)))) |
213 | 175 | adantl 485 |
. . . . . . . . 9
⊢
((⊤ ∧ 𝑗
∈ ℕ) → (1 / (𝑗 · (𝑗 + 1))) ∈ ℂ) |
214 | 153 | a1i 11 |
. . . . . . . . 9
⊢ (⊤
→ seq1( + , 𝐹) ⇝
1) |
215 | 173, 211,
212, 213, 214 | isumclim 15208 |
. . . . . . . 8
⊢ (⊤
→ Σ𝑗 ∈
ℕ (1 / (𝑗 ·
(𝑗 + 1))) =
1) |
216 | 215 | mptru 1549 |
. . . . . . 7
⊢
Σ𝑗 ∈
ℕ (1 / (𝑗 ·
(𝑗 + 1))) =
1 |
217 | 210, 216 | breqtrdi 5072 |
. . . . . 6
⊢ (𝑁 ∈ ℕ →
Σ𝑗 ∈ (1...(𝑁 − 1))(1 / (𝑗 · (𝑗 + 1))) ≤ 1) |
218 | 110, 111,
30, 119, 217 | lemul2ad 11661 |
. . . . 5
⊢ (𝑁 ∈ ℕ → ((1 / 4)
· Σ𝑗 ∈
(1...(𝑁 − 1))(1 /
(𝑗 · (𝑗 + 1)))) ≤ ((1 / 4) ·
1)) |
219 | | 4cn 11804 |
. . . . . . . 8
⊢ 4 ∈
ℂ |
220 | 219 | a1i 11 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ → 4 ∈
ℂ) |
221 | 112 | a1i 11 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ → 0 <
4) |
222 | 221 | gt0ne0d 11285 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ → 4 ≠
0) |
223 | 220, 222 | reccld 11490 |
. . . . . 6
⊢ (𝑁 ∈ ℕ → (1 / 4)
∈ ℂ) |
224 | 102 | recnd 10750 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ (1...(𝑁 − 1))) → (1 / (𝑗 · (𝑗 + 1))) ∈ ℂ) |
225 | 61, 223, 224 | fsummulc2 15235 |
. . . . 5
⊢ (𝑁 ∈ ℕ → ((1 / 4)
· Σ𝑗 ∈
(1...(𝑁 − 1))(1 /
(𝑗 · (𝑗 + 1)))) = Σ𝑗 ∈ (1...(𝑁 − 1))((1 / 4) · (1 / (𝑗 · (𝑗 + 1))))) |
226 | 223 | mulid1d 10739 |
. . . . 5
⊢ (𝑁 ∈ ℕ → ((1 / 4)
· 1) = (1 / 4)) |
227 | 218, 225,
226 | 3brtr3d 5062 |
. . . 4
⊢ (𝑁 ∈ ℕ →
Σ𝑗 ∈ (1...(𝑁 − 1))((1 / 4) · (1
/ (𝑗 · (𝑗 + 1)))) ≤ (1 /
4)) |
228 | 88, 104, 30, 109, 227 | letrd 10878 |
. . 3
⊢ (𝑁 ∈ ℕ →
Σ𝑗 ∈ (1...(𝑁 − 1))((𝐵‘𝑗) − (𝐵‘(𝑗 + 1))) ≤ (1 / 4)) |
229 | 60, 228 | eqbrtrd 5053 |
. 2
⊢ (𝑁 ∈ ℕ → ((𝐵‘1) − (𝐵‘𝑁)) ≤ (1 / 4)) |
230 | 17, 26, 30, 229 | subled 11324 |
1
⊢ (𝑁 ∈ ℕ → ((𝐵‘1) − (1 / 4)) ≤
(𝐵‘𝑁)) |