| Step | Hyp | Ref
| Expression |
| 1 | | 0red 11264 |
. . 3
⊢ (𝑁 ∈ ℕ → 0 ∈
ℝ) |
| 2 | | stirlinglem11.3 |
. . . . . 6
⊢ 𝐾 = (𝑘 ∈ ℕ ↦ ((1 / ((2 ·
𝑘) + 1)) · ((1 / ((2
· 𝑁) + 1))↑(2
· 𝑘)))) |
| 3 | 2 | a1i 11 |
. . . . 5
⊢ (𝑁 ∈ ℕ → 𝐾 = (𝑘 ∈ ℕ ↦ ((1 / ((2 ·
𝑘) + 1)) · ((1 / ((2
· 𝑁) + 1))↑(2
· 𝑘))))) |
| 4 | | simpr 484 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ 𝑘 = 1) → 𝑘 = 1) |
| 5 | 4 | oveq2d 7447 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝑘 = 1) → (2 · 𝑘) = (2 ·
1)) |
| 6 | 5 | oveq1d 7446 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ 𝑘 = 1) → ((2 · 𝑘) + 1) = ((2 · 1) +
1)) |
| 7 | 6 | oveq2d 7447 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ 𝑘 = 1) → (1 / ((2 ·
𝑘) + 1)) = (1 / ((2
· 1) + 1))) |
| 8 | 5 | oveq2d 7447 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ 𝑘 = 1) → ((1 / ((2 ·
𝑁) + 1))↑(2 ·
𝑘)) = ((1 / ((2 ·
𝑁) + 1))↑(2 ·
1))) |
| 9 | 7, 8 | oveq12d 7449 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ 𝑘 = 1) → ((1 / ((2 ·
𝑘) + 1)) · ((1 / ((2
· 𝑁) + 1))↑(2
· 𝑘))) = ((1 / ((2
· 1) + 1)) · ((1 / ((2 · 𝑁) + 1))↑(2 ·
1)))) |
| 10 | | 1nn 12277 |
. . . . . 6
⊢ 1 ∈
ℕ |
| 11 | 10 | a1i 11 |
. . . . 5
⊢ (𝑁 ∈ ℕ → 1 ∈
ℕ) |
| 12 | | 2cnd 12344 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ → 2 ∈
ℂ) |
| 13 | | 1cnd 11256 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ → 1 ∈
ℂ) |
| 14 | 12, 13 | mulcld 11281 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ → (2
· 1) ∈ ℂ) |
| 15 | 14, 13 | addcld 11280 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ → ((2
· 1) + 1) ∈ ℂ) |
| 16 | | 2t1e2 12429 |
. . . . . . . . . . 11
⊢ (2
· 1) = 2 |
| 17 | 16 | oveq1i 7441 |
. . . . . . . . . 10
⊢ ((2
· 1) + 1) = (2 + 1) |
| 18 | | 2p1e3 12408 |
. . . . . . . . . 10
⊢ (2 + 1) =
3 |
| 19 | 17, 18 | eqtri 2765 |
. . . . . . . . 9
⊢ ((2
· 1) + 1) = 3 |
| 20 | | 3ne0 12372 |
. . . . . . . . 9
⊢ 3 ≠
0 |
| 21 | 19, 20 | eqnetri 3011 |
. . . . . . . 8
⊢ ((2
· 1) + 1) ≠ 0 |
| 22 | 21 | a1i 11 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ → ((2
· 1) + 1) ≠ 0) |
| 23 | 15, 22 | reccld 12036 |
. . . . . 6
⊢ (𝑁 ∈ ℕ → (1 / ((2
· 1) + 1)) ∈ ℂ) |
| 24 | | nncn 12274 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℂ) |
| 25 | 12, 24 | mulcld 11281 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ → (2
· 𝑁) ∈
ℂ) |
| 26 | 25, 13 | addcld 11280 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ → ((2
· 𝑁) + 1) ∈
ℂ) |
| 27 | | 1red 11262 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ → 1 ∈
ℝ) |
| 28 | | 2re 12340 |
. . . . . . . . . . . . 13
⊢ 2 ∈
ℝ |
| 29 | 28 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℕ → 2 ∈
ℝ) |
| 30 | | nnre 12273 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℝ) |
| 31 | 29, 30 | remulcld 11291 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ → (2
· 𝑁) ∈
ℝ) |
| 32 | 31, 27 | readdcld 11290 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ → ((2
· 𝑁) + 1) ∈
ℝ) |
| 33 | | 0lt1 11785 |
. . . . . . . . . . 11
⊢ 0 <
1 |
| 34 | 33 | a1i 11 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ → 0 <
1) |
| 35 | | 2rp 13039 |
. . . . . . . . . . . . 13
⊢ 2 ∈
ℝ+ |
| 36 | 35 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℕ → 2 ∈
ℝ+) |
| 37 | | nnrp 13046 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℝ+) |
| 38 | 36, 37 | rpmulcld 13093 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ → (2
· 𝑁) ∈
ℝ+) |
| 39 | 27, 38 | ltaddrp2d 13111 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ → 1 <
((2 · 𝑁) +
1)) |
| 40 | 1, 27, 32, 34, 39 | lttrd 11422 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ → 0 <
((2 · 𝑁) +
1)) |
| 41 | 40 | gt0ne0d 11827 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ → ((2
· 𝑁) + 1) ≠
0) |
| 42 | 26, 41 | reccld 12036 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ → (1 / ((2
· 𝑁) + 1)) ∈
ℂ) |
| 43 | | 2nn0 12543 |
. . . . . . . . 9
⊢ 2 ∈
ℕ0 |
| 44 | 43 | a1i 11 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ → 2 ∈
ℕ0) |
| 45 | | 1nn0 12542 |
. . . . . . . . 9
⊢ 1 ∈
ℕ0 |
| 46 | 45 | a1i 11 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ → 1 ∈
ℕ0) |
| 47 | 44, 46 | nn0mulcld 12592 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ → (2
· 1) ∈ ℕ0) |
| 48 | 42, 47 | expcld 14186 |
. . . . . 6
⊢ (𝑁 ∈ ℕ → ((1 / ((2
· 𝑁) + 1))↑(2
· 1)) ∈ ℂ) |
| 49 | 23, 48 | mulcld 11281 |
. . . . 5
⊢ (𝑁 ∈ ℕ → ((1 / ((2
· 1) + 1)) · ((1 / ((2 · 𝑁) + 1))↑(2 · 1))) ∈
ℂ) |
| 50 | 3, 9, 11, 49 | fvmptd 7023 |
. . . 4
⊢ (𝑁 ∈ ℕ → (𝐾‘1) = ((1 / ((2 ·
1) + 1)) · ((1 / ((2 · 𝑁) + 1))↑(2 ·
1)))) |
| 51 | | 1re 11261 |
. . . . . . . . 9
⊢ 1 ∈
ℝ |
| 52 | 28, 51 | remulcli 11277 |
. . . . . . . 8
⊢ (2
· 1) ∈ ℝ |
| 53 | 52, 51 | readdcli 11276 |
. . . . . . 7
⊢ ((2
· 1) + 1) ∈ ℝ |
| 54 | 53, 21 | rereccli 12032 |
. . . . . 6
⊢ (1 / ((2
· 1) + 1)) ∈ ℝ |
| 55 | 54 | a1i 11 |
. . . . 5
⊢ (𝑁 ∈ ℕ → (1 / ((2
· 1) + 1)) ∈ ℝ) |
| 56 | 32, 41 | rereccld 12094 |
. . . . . 6
⊢ (𝑁 ∈ ℕ → (1 / ((2
· 𝑁) + 1)) ∈
ℝ) |
| 57 | 56, 47 | reexpcld 14203 |
. . . . 5
⊢ (𝑁 ∈ ℕ → ((1 / ((2
· 𝑁) + 1))↑(2
· 1)) ∈ ℝ) |
| 58 | 55, 57 | remulcld 11291 |
. . . 4
⊢ (𝑁 ∈ ℕ → ((1 / ((2
· 1) + 1)) · ((1 / ((2 · 𝑁) + 1))↑(2 · 1))) ∈
ℝ) |
| 59 | 50, 58 | eqeltrd 2841 |
. . 3
⊢ (𝑁 ∈ ℕ → (𝐾‘1) ∈
ℝ) |
| 60 | | stirlinglem11.1 |
. . . . . . . 8
⊢ 𝐴 = (𝑛 ∈ ℕ ↦ ((!‘𝑛) / ((√‘(2 ·
𝑛)) · ((𝑛 / e)↑𝑛)))) |
| 61 | 60 | stirlinglem2 46090 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ → (𝐴‘𝑁) ∈
ℝ+) |
| 62 | 61 | relogcld 26665 |
. . . . . 6
⊢ (𝑁 ∈ ℕ →
(log‘(𝐴‘𝑁)) ∈
ℝ) |
| 63 | | nfcv 2905 |
. . . . . . 7
⊢
Ⅎ𝑛𝑁 |
| 64 | | nfcv 2905 |
. . . . . . . 8
⊢
Ⅎ𝑛log |
| 65 | | nfmpt1 5250 |
. . . . . . . . . 10
⊢
Ⅎ𝑛(𝑛 ∈ ℕ ↦ ((!‘𝑛) / ((√‘(2 ·
𝑛)) · ((𝑛 / e)↑𝑛)))) |
| 66 | 60, 65 | nfcxfr 2903 |
. . . . . . . . 9
⊢
Ⅎ𝑛𝐴 |
| 67 | 66, 63 | nffv 6916 |
. . . . . . . 8
⊢
Ⅎ𝑛(𝐴‘𝑁) |
| 68 | 64, 67 | nffv 6916 |
. . . . . . 7
⊢
Ⅎ𝑛(log‘(𝐴‘𝑁)) |
| 69 | | 2fveq3 6911 |
. . . . . . 7
⊢ (𝑛 = 𝑁 → (log‘(𝐴‘𝑛)) = (log‘(𝐴‘𝑁))) |
| 70 | | stirlinglem11.2 |
. . . . . . 7
⊢ 𝐵 = (𝑛 ∈ ℕ ↦ (log‘(𝐴‘𝑛))) |
| 71 | 63, 68, 69, 70 | fvmptf 7037 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧
(log‘(𝐴‘𝑁)) ∈ ℝ) → (𝐵‘𝑁) = (log‘(𝐴‘𝑁))) |
| 72 | 62, 71 | mpdan 687 |
. . . . 5
⊢ (𝑁 ∈ ℕ → (𝐵‘𝑁) = (log‘(𝐴‘𝑁))) |
| 73 | 72, 62 | eqeltrd 2841 |
. . . 4
⊢ (𝑁 ∈ ℕ → (𝐵‘𝑁) ∈ ℝ) |
| 74 | | peano2nn 12278 |
. . . . . 6
⊢ (𝑁 ∈ ℕ → (𝑁 + 1) ∈
ℕ) |
| 75 | 60 | stirlinglem2 46090 |
. . . . . . . 8
⊢ ((𝑁 + 1) ∈ ℕ →
(𝐴‘(𝑁 + 1)) ∈
ℝ+) |
| 76 | 74, 75 | syl 17 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ → (𝐴‘(𝑁 + 1)) ∈
ℝ+) |
| 77 | 76 | relogcld 26665 |
. . . . . 6
⊢ (𝑁 ∈ ℕ →
(log‘(𝐴‘(𝑁 + 1))) ∈
ℝ) |
| 78 | | nfcv 2905 |
. . . . . . 7
⊢
Ⅎ𝑛(𝑁 + 1) |
| 79 | 66, 78 | nffv 6916 |
. . . . . . . 8
⊢
Ⅎ𝑛(𝐴‘(𝑁 + 1)) |
| 80 | 64, 79 | nffv 6916 |
. . . . . . 7
⊢
Ⅎ𝑛(log‘(𝐴‘(𝑁 + 1))) |
| 81 | | 2fveq3 6911 |
. . . . . . 7
⊢ (𝑛 = (𝑁 + 1) → (log‘(𝐴‘𝑛)) = (log‘(𝐴‘(𝑁 + 1)))) |
| 82 | 78, 80, 81, 70 | fvmptf 7037 |
. . . . . 6
⊢ (((𝑁 + 1) ∈ ℕ ∧
(log‘(𝐴‘(𝑁 + 1))) ∈ ℝ) →
(𝐵‘(𝑁 + 1)) = (log‘(𝐴‘(𝑁 + 1)))) |
| 83 | 74, 77, 82 | syl2anc 584 |
. . . . 5
⊢ (𝑁 ∈ ℕ → (𝐵‘(𝑁 + 1)) = (log‘(𝐴‘(𝑁 + 1)))) |
| 84 | 83, 77 | eqeltrd 2841 |
. . . 4
⊢ (𝑁 ∈ ℕ → (𝐵‘(𝑁 + 1)) ∈ ℝ) |
| 85 | 73, 84 | resubcld 11691 |
. . 3
⊢ (𝑁 ∈ ℕ → ((𝐵‘𝑁) − (𝐵‘(𝑁 + 1))) ∈ ℝ) |
| 86 | 29, 27 | remulcld 11291 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ → (2
· 1) ∈ ℝ) |
| 87 | | 0le2 12368 |
. . . . . . . . . 10
⊢ 0 ≤
2 |
| 88 | 87 | a1i 11 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ → 0 ≤
2) |
| 89 | | 0le1 11786 |
. . . . . . . . . 10
⊢ 0 ≤
1 |
| 90 | 89 | a1i 11 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ → 0 ≤
1) |
| 91 | 29, 27, 88, 90 | mulge0d 11840 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ → 0 ≤ (2
· 1)) |
| 92 | 86, 91 | ge0p1rpd 13107 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ → ((2
· 1) + 1) ∈ ℝ+) |
| 93 | 92 | rpreccld 13087 |
. . . . . 6
⊢ (𝑁 ∈ ℕ → (1 / ((2
· 1) + 1)) ∈ ℝ+) |
| 94 | 37 | rpge0d 13081 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ → 0 ≤
𝑁) |
| 95 | 29, 30, 88, 94 | mulge0d 11840 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ → 0 ≤ (2
· 𝑁)) |
| 96 | 31, 95 | ge0p1rpd 13107 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ → ((2
· 𝑁) + 1) ∈
ℝ+) |
| 97 | 96 | rpreccld 13087 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ → (1 / ((2
· 𝑁) + 1)) ∈
ℝ+) |
| 98 | | 2z 12649 |
. . . . . . . . 9
⊢ 2 ∈
ℤ |
| 99 | 98 | a1i 11 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ → 2 ∈
ℤ) |
| 100 | | 1z 12647 |
. . . . . . . . 9
⊢ 1 ∈
ℤ |
| 101 | 100 | a1i 11 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ → 1 ∈
ℤ) |
| 102 | 99, 101 | zmulcld 12728 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ → (2
· 1) ∈ ℤ) |
| 103 | 97, 102 | rpexpcld 14286 |
. . . . . 6
⊢ (𝑁 ∈ ℕ → ((1 / ((2
· 𝑁) + 1))↑(2
· 1)) ∈ ℝ+) |
| 104 | 93, 103 | rpmulcld 13093 |
. . . . 5
⊢ (𝑁 ∈ ℕ → ((1 / ((2
· 1) + 1)) · ((1 / ((2 · 𝑁) + 1))↑(2 · 1))) ∈
ℝ+) |
| 105 | 50, 104 | eqeltrd 2841 |
. . . 4
⊢ (𝑁 ∈ ℕ → (𝐾‘1) ∈
ℝ+) |
| 106 | 105 | rpgt0d 13080 |
. . 3
⊢ (𝑁 ∈ ℕ → 0 <
(𝐾‘1)) |
| 107 | 85, 59 | resubcld 11691 |
. . . . 5
⊢ (𝑁 ∈ ℕ → (((𝐵‘𝑁) − (𝐵‘(𝑁 + 1))) − (𝐾‘1)) ∈ ℝ) |
| 108 | | eqid 2737 |
. . . . . . 7
⊢
(ℤ≥‘(1 + 1)) =
(ℤ≥‘(1 + 1)) |
| 109 | 101 | peano2zd 12725 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ → (1 + 1)
∈ ℤ) |
| 110 | | nnuz 12921 |
. . . . . . . 8
⊢ ℕ =
(ℤ≥‘1) |
| 111 | 2 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) → 𝐾 = (𝑘 ∈ ℕ ↦ ((1 / ((2 ·
𝑘) + 1)) · ((1 / ((2
· 𝑁) + 1))↑(2
· 𝑘))))) |
| 112 | | oveq2 7439 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = 𝑗 → (2 · 𝑘) = (2 · 𝑗)) |
| 113 | 112 | oveq1d 7446 |
. . . . . . . . . . . . 13
⊢ (𝑘 = 𝑗 → ((2 · 𝑘) + 1) = ((2 · 𝑗) + 1)) |
| 114 | 113 | oveq2d 7447 |
. . . . . . . . . . . 12
⊢ (𝑘 = 𝑗 → (1 / ((2 · 𝑘) + 1)) = (1 / ((2 · 𝑗) + 1))) |
| 115 | 112 | oveq2d 7447 |
. . . . . . . . . . . 12
⊢ (𝑘 = 𝑗 → ((1 / ((2 · 𝑁) + 1))↑(2 · 𝑘)) = ((1 / ((2 · 𝑁) + 1))↑(2 · 𝑗))) |
| 116 | 114, 115 | oveq12d 7449 |
. . . . . . . . . . 11
⊢ (𝑘 = 𝑗 → ((1 / ((2 · 𝑘) + 1)) · ((1 / ((2 · 𝑁) + 1))↑(2 · 𝑘))) = ((1 / ((2 · 𝑗) + 1)) · ((1 / ((2
· 𝑁) + 1))↑(2
· 𝑗)))) |
| 117 | 116 | adantl 481 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑘 = 𝑗) → ((1 / ((2 · 𝑘) + 1)) · ((1 / ((2
· 𝑁) + 1))↑(2
· 𝑘))) = ((1 / ((2
· 𝑗) + 1)) ·
((1 / ((2 · 𝑁) +
1))↑(2 · 𝑗)))) |
| 118 | | simpr 484 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) → 𝑗 ∈
ℕ) |
| 119 | | 2cnd 12344 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) → 2 ∈
ℂ) |
| 120 | | nncn 12274 |
. . . . . . . . . . . . . . 15
⊢ (𝑗 ∈ ℕ → 𝑗 ∈
ℂ) |
| 121 | 120 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) → 𝑗 ∈
ℂ) |
| 122 | 119, 121 | mulcld 11281 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) → (2
· 𝑗) ∈
ℂ) |
| 123 | | 1cnd 11256 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) → 1 ∈
ℂ) |
| 124 | 122, 123 | addcld 11280 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) → ((2
· 𝑗) + 1) ∈
ℂ) |
| 125 | | 0red 11264 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) → 0 ∈
ℝ) |
| 126 | | 1red 11262 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) → 1 ∈
ℝ) |
| 127 | 28 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) → 2 ∈
ℝ) |
| 128 | | nnre 12273 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑗 ∈ ℕ → 𝑗 ∈
ℝ) |
| 129 | 128 | adantl 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) → 𝑗 ∈
ℝ) |
| 130 | 127, 129 | remulcld 11291 |
. . . . . . . . . . . . . . 15
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) → (2
· 𝑗) ∈
ℝ) |
| 131 | 130, 126 | readdcld 11290 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) → ((2
· 𝑗) + 1) ∈
ℝ) |
| 132 | 33 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) → 0 <
1) |
| 133 | 35 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) → 2 ∈
ℝ+) |
| 134 | | nnrp 13046 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑗 ∈ ℕ → 𝑗 ∈
ℝ+) |
| 135 | 134 | adantl 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) → 𝑗 ∈
ℝ+) |
| 136 | 133, 135 | rpmulcld 13093 |
. . . . . . . . . . . . . . 15
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) → (2
· 𝑗) ∈
ℝ+) |
| 137 | 126, 136 | ltaddrp2d 13111 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) → 1 <
((2 · 𝑗) +
1)) |
| 138 | 125, 126,
131, 132, 137 | lttrd 11422 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) → 0 <
((2 · 𝑗) +
1)) |
| 139 | 138 | gt0ne0d 11827 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) → ((2
· 𝑗) + 1) ≠
0) |
| 140 | 124, 139 | reccld 12036 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) → (1 / ((2
· 𝑗) + 1)) ∈
ℂ) |
| 141 | 24 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) → 𝑁 ∈
ℂ) |
| 142 | 119, 141 | mulcld 11281 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) → (2
· 𝑁) ∈
ℂ) |
| 143 | 142, 123 | addcld 11280 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) → ((2
· 𝑁) + 1) ∈
ℂ) |
| 144 | 41 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) → ((2
· 𝑁) + 1) ≠
0) |
| 145 | 143, 144 | reccld 12036 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) → (1 / ((2
· 𝑁) + 1)) ∈
ℂ) |
| 146 | 43 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) → 2 ∈
ℕ0) |
| 147 | | nnnn0 12533 |
. . . . . . . . . . . . . 14
⊢ (𝑗 ∈ ℕ → 𝑗 ∈
ℕ0) |
| 148 | 147 | adantl 481 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) → 𝑗 ∈
ℕ0) |
| 149 | 146, 148 | nn0mulcld 12592 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) → (2
· 𝑗) ∈
ℕ0) |
| 150 | 145, 149 | expcld 14186 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) → ((1 /
((2 · 𝑁) +
1))↑(2 · 𝑗))
∈ ℂ) |
| 151 | 140, 150 | mulcld 11281 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) → ((1 /
((2 · 𝑗) + 1))
· ((1 / ((2 · 𝑁) + 1))↑(2 · 𝑗))) ∈ ℂ) |
| 152 | 111, 117,
118, 151 | fvmptd 7023 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) → (𝐾‘𝑗) = ((1 / ((2 · 𝑗) + 1)) · ((1 / ((2 · 𝑁) + 1))↑(2 · 𝑗)))) |
| 153 | | 0red 11264 |
. . . . . . . . . . . . . 14
⊢ (𝑗 ∈ ℕ → 0 ∈
ℝ) |
| 154 | | 1red 11262 |
. . . . . . . . . . . . . 14
⊢ (𝑗 ∈ ℕ → 1 ∈
ℝ) |
| 155 | 28 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (𝑗 ∈ ℕ → 2 ∈
ℝ) |
| 156 | 155, 128 | remulcld 11291 |
. . . . . . . . . . . . . . 15
⊢ (𝑗 ∈ ℕ → (2
· 𝑗) ∈
ℝ) |
| 157 | 156, 154 | readdcld 11290 |
. . . . . . . . . . . . . 14
⊢ (𝑗 ∈ ℕ → ((2
· 𝑗) + 1) ∈
ℝ) |
| 158 | 33 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝑗 ∈ ℕ → 0 <
1) |
| 159 | 35 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (𝑗 ∈ ℕ → 2 ∈
ℝ+) |
| 160 | 159, 134 | rpmulcld 13093 |
. . . . . . . . . . . . . . 15
⊢ (𝑗 ∈ ℕ → (2
· 𝑗) ∈
ℝ+) |
| 161 | 154, 160 | ltaddrp2d 13111 |
. . . . . . . . . . . . . 14
⊢ (𝑗 ∈ ℕ → 1 <
((2 · 𝑗) +
1)) |
| 162 | 153, 154,
157, 158, 161 | lttrd 11422 |
. . . . . . . . . . . . 13
⊢ (𝑗 ∈ ℕ → 0 <
((2 · 𝑗) +
1)) |
| 163 | 162 | gt0ne0d 11827 |
. . . . . . . . . . . 12
⊢ (𝑗 ∈ ℕ → ((2
· 𝑗) + 1) ≠
0) |
| 164 | 163 | adantl 481 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) → ((2
· 𝑗) + 1) ≠
0) |
| 165 | 124, 164 | reccld 12036 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) → (1 / ((2
· 𝑗) + 1)) ∈
ℂ) |
| 166 | 165, 150 | mulcld 11281 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) → ((1 /
((2 · 𝑗) + 1))
· ((1 / ((2 · 𝑁) + 1))↑(2 · 𝑗))) ∈ ℂ) |
| 167 | 152, 166 | eqeltrd 2841 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) → (𝐾‘𝑗) ∈ ℂ) |
| 168 | | eqid 2737 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ ↦ ((((1 +
(2 · 𝑛)) / 2)
· (log‘((𝑛 +
1) / 𝑛))) − 1)) =
(𝑛 ∈ ℕ ↦
((((1 + (2 · 𝑛)) /
2) · (log‘((𝑛
+ 1) / 𝑛))) −
1)) |
| 169 | 60, 70, 168, 2 | stirlinglem9 46097 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ → seq1( + ,
𝐾) ⇝ ((𝐵‘𝑁) − (𝐵‘(𝑁 + 1)))) |
| 170 | 110, 11, 167, 169 | clim2ser 15691 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ → seq(1 +
1)( + , 𝐾) ⇝ (((𝐵‘𝑁) − (𝐵‘(𝑁 + 1))) − (seq1( + , 𝐾)‘1))) |
| 171 | | peano2nn 12278 |
. . . . . . . . . . . . 13
⊢ (1 ∈
ℕ → (1 + 1) ∈ ℕ) |
| 172 | | uznnssnn 12937 |
. . . . . . . . . . . . 13
⊢ ((1 + 1)
∈ ℕ → (ℤ≥‘(1 + 1)) ⊆
ℕ) |
| 173 | 10, 171, 172 | mp2b 10 |
. . . . . . . . . . . 12
⊢
(ℤ≥‘(1 + 1)) ⊆ ℕ |
| 174 | 173 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ →
(ℤ≥‘(1 + 1)) ⊆ ℕ) |
| 175 | 174 | sseld 3982 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ → (𝑗 ∈
(ℤ≥‘(1 + 1)) → 𝑗 ∈ ℕ)) |
| 176 | 175 | imdistani 568 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈
(ℤ≥‘(1 + 1))) → (𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ)) |
| 177 | 176, 152 | syl 17 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈
(ℤ≥‘(1 + 1))) → (𝐾‘𝑗) = ((1 / ((2 · 𝑗) + 1)) · ((1 / ((2 · 𝑁) + 1))↑(2 · 𝑗)))) |
| 178 | 28 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝑗 ∈
(ℤ≥‘(1 + 1)) → 2 ∈
ℝ) |
| 179 | | eluzelre 12889 |
. . . . . . . . . . . . 13
⊢ (𝑗 ∈
(ℤ≥‘(1 + 1)) → 𝑗 ∈ ℝ) |
| 180 | 178, 179 | remulcld 11291 |
. . . . . . . . . . . 12
⊢ (𝑗 ∈
(ℤ≥‘(1 + 1)) → (2 · 𝑗) ∈ ℝ) |
| 181 | | 1red 11262 |
. . . . . . . . . . . 12
⊢ (𝑗 ∈
(ℤ≥‘(1 + 1)) → 1 ∈
ℝ) |
| 182 | 180, 181 | readdcld 11290 |
. . . . . . . . . . 11
⊢ (𝑗 ∈
(ℤ≥‘(1 + 1)) → ((2 · 𝑗) + 1) ∈ ℝ) |
| 183 | 173 | sseli 3979 |
. . . . . . . . . . . 12
⊢ (𝑗 ∈
(ℤ≥‘(1 + 1)) → 𝑗 ∈ ℕ) |
| 184 | 183, 163 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑗 ∈
(ℤ≥‘(1 + 1)) → ((2 · 𝑗) + 1) ≠ 0) |
| 185 | 182, 184 | rereccld 12094 |
. . . . . . . . . 10
⊢ (𝑗 ∈
(ℤ≥‘(1 + 1)) → (1 / ((2 · 𝑗) + 1)) ∈
ℝ) |
| 186 | 185 | adantl 481 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈
(ℤ≥‘(1 + 1))) → (1 / ((2 · 𝑗) + 1)) ∈
ℝ) |
| 187 | 32 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈
(ℤ≥‘(1 + 1))) → ((2 · 𝑁) + 1) ∈ ℝ) |
| 188 | 41 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈
(ℤ≥‘(1 + 1))) → ((2 · 𝑁) + 1) ≠ 0) |
| 189 | 187, 188 | rereccld 12094 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈
(ℤ≥‘(1 + 1))) → (1 / ((2 · 𝑁) + 1)) ∈
ℝ) |
| 190 | 176, 149 | syl 17 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈
(ℤ≥‘(1 + 1))) → (2 · 𝑗) ∈
ℕ0) |
| 191 | 189, 190 | reexpcld 14203 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈
(ℤ≥‘(1 + 1))) → ((1 / ((2 · 𝑁) + 1))↑(2 · 𝑗)) ∈
ℝ) |
| 192 | 186, 191 | remulcld 11291 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈
(ℤ≥‘(1 + 1))) → ((1 / ((2 · 𝑗) + 1)) · ((1 / ((2
· 𝑁) + 1))↑(2
· 𝑗))) ∈
ℝ) |
| 193 | 177, 192 | eqeltrd 2841 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈
(ℤ≥‘(1 + 1))) → (𝐾‘𝑗) ∈ ℝ) |
| 194 | | 1red 11262 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈
(ℤ≥‘(1 + 1))) → 1 ∈
ℝ) |
| 195 | 28 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈
(ℤ≥‘(1 + 1))) → 2 ∈
ℝ) |
| 196 | 176, 129 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈
(ℤ≥‘(1 + 1))) → 𝑗 ∈ ℝ) |
| 197 | 195, 196 | remulcld 11291 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈
(ℤ≥‘(1 + 1))) → (2 · 𝑗) ∈ ℝ) |
| 198 | 87 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈
(ℤ≥‘(1 + 1))) → 0 ≤ 2) |
| 199 | | 0red 11264 |
. . . . . . . . . . . . . 14
⊢ (𝑗 ∈
(ℤ≥‘(1 + 1)) → 0 ∈
ℝ) |
| 200 | 87 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝑗 ∈
(ℤ≥‘(1 + 1)) → 0 ≤ 2) |
| 201 | | 1p1e2 12391 |
. . . . . . . . . . . . . . 15
⊢ (1 + 1) =
2 |
| 202 | | eluzle 12891 |
. . . . . . . . . . . . . . 15
⊢ (𝑗 ∈
(ℤ≥‘(1 + 1)) → (1 + 1) ≤ 𝑗) |
| 203 | 201, 202 | eqbrtrrid 5179 |
. . . . . . . . . . . . . 14
⊢ (𝑗 ∈
(ℤ≥‘(1 + 1)) → 2 ≤ 𝑗) |
| 204 | 199, 178,
179, 200, 203 | letrd 11418 |
. . . . . . . . . . . . 13
⊢ (𝑗 ∈
(ℤ≥‘(1 + 1)) → 0 ≤ 𝑗) |
| 205 | 204 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈
(ℤ≥‘(1 + 1))) → 0 ≤ 𝑗) |
| 206 | 195, 196,
198, 205 | mulge0d 11840 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈
(ℤ≥‘(1 + 1))) → 0 ≤ (2 · 𝑗)) |
| 207 | 197, 206 | ge0p1rpd 13107 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈
(ℤ≥‘(1 + 1))) → ((2 · 𝑗) + 1) ∈
ℝ+) |
| 208 | 89 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈
(ℤ≥‘(1 + 1))) → 0 ≤ 1) |
| 209 | 194, 207,
208 | divge0d 13117 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈
(ℤ≥‘(1 + 1))) → 0 ≤ (1 / ((2 · 𝑗) + 1))) |
| 210 | 30 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈
(ℤ≥‘(1 + 1))) → 𝑁 ∈ ℝ) |
| 211 | 195, 210 | remulcld 11291 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈
(ℤ≥‘(1 + 1))) → (2 · 𝑁) ∈ ℝ) |
| 212 | 94 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈
(ℤ≥‘(1 + 1))) → 0 ≤ 𝑁) |
| 213 | 195, 210,
198, 212 | mulge0d 11840 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈
(ℤ≥‘(1 + 1))) → 0 ≤ (2 · 𝑁)) |
| 214 | 211, 213 | ge0p1rpd 13107 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈
(ℤ≥‘(1 + 1))) → ((2 · 𝑁) + 1) ∈
ℝ+) |
| 215 | 194, 214,
208 | divge0d 13117 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈
(ℤ≥‘(1 + 1))) → 0 ≤ (1 / ((2 · 𝑁) + 1))) |
| 216 | 189, 190,
215 | expge0d 14204 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈
(ℤ≥‘(1 + 1))) → 0 ≤ ((1 / ((2 · 𝑁) + 1))↑(2 · 𝑗))) |
| 217 | 186, 191,
209, 216 | mulge0d 11840 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈
(ℤ≥‘(1 + 1))) → 0 ≤ ((1 / ((2 · 𝑗) + 1)) · ((1 / ((2
· 𝑁) + 1))↑(2
· 𝑗)))) |
| 218 | 217, 177 | breqtrrd 5171 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈
(ℤ≥‘(1 + 1))) → 0 ≤ (𝐾‘𝑗)) |
| 219 | 108, 109,
170, 193, 218 | iserge0 15697 |
. . . . . 6
⊢ (𝑁 ∈ ℕ → 0 ≤
(((𝐵‘𝑁) − (𝐵‘(𝑁 + 1))) − (seq1( + , 𝐾)‘1))) |
| 220 | | seq1 14055 |
. . . . . . . 8
⊢ (1 ∈
ℤ → (seq1( + , 𝐾)‘1) = (𝐾‘1)) |
| 221 | 100, 220 | mp1i 13 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ → (seq1( +
, 𝐾)‘1) = (𝐾‘1)) |
| 222 | 221 | oveq2d 7447 |
. . . . . 6
⊢ (𝑁 ∈ ℕ → (((𝐵‘𝑁) − (𝐵‘(𝑁 + 1))) − (seq1( + , 𝐾)‘1)) = (((𝐵‘𝑁) − (𝐵‘(𝑁 + 1))) − (𝐾‘1))) |
| 223 | 219, 222 | breqtrd 5169 |
. . . . 5
⊢ (𝑁 ∈ ℕ → 0 ≤
(((𝐵‘𝑁) − (𝐵‘(𝑁 + 1))) − (𝐾‘1))) |
| 224 | 1, 107, 59, 223 | leadd1dd 11877 |
. . . 4
⊢ (𝑁 ∈ ℕ → (0 +
(𝐾‘1)) ≤ ((((𝐵‘𝑁) − (𝐵‘(𝑁 + 1))) − (𝐾‘1)) + (𝐾‘1))) |
| 225 | 50, 49 | eqeltrd 2841 |
. . . . 5
⊢ (𝑁 ∈ ℕ → (𝐾‘1) ∈
ℂ) |
| 226 | 225 | addlidd 11462 |
. . . 4
⊢ (𝑁 ∈ ℕ → (0 +
(𝐾‘1)) = (𝐾‘1)) |
| 227 | 73 | recnd 11289 |
. . . . . 6
⊢ (𝑁 ∈ ℕ → (𝐵‘𝑁) ∈ ℂ) |
| 228 | 84 | recnd 11289 |
. . . . . 6
⊢ (𝑁 ∈ ℕ → (𝐵‘(𝑁 + 1)) ∈ ℂ) |
| 229 | 227, 228 | subcld 11620 |
. . . . 5
⊢ (𝑁 ∈ ℕ → ((𝐵‘𝑁) − (𝐵‘(𝑁 + 1))) ∈ ℂ) |
| 230 | 229, 225 | npcand 11624 |
. . . 4
⊢ (𝑁 ∈ ℕ → ((((𝐵‘𝑁) − (𝐵‘(𝑁 + 1))) − (𝐾‘1)) + (𝐾‘1)) = ((𝐵‘𝑁) − (𝐵‘(𝑁 + 1)))) |
| 231 | 224, 226,
230 | 3brtr3d 5174 |
. . 3
⊢ (𝑁 ∈ ℕ → (𝐾‘1) ≤ ((𝐵‘𝑁) − (𝐵‘(𝑁 + 1)))) |
| 232 | 1, 59, 85, 106, 231 | ltletrd 11421 |
. 2
⊢ (𝑁 ∈ ℕ → 0 <
((𝐵‘𝑁) − (𝐵‘(𝑁 + 1)))) |
| 233 | 84, 73 | posdifd 11850 |
. 2
⊢ (𝑁 ∈ ℕ → ((𝐵‘(𝑁 + 1)) < (𝐵‘𝑁) ↔ 0 < ((𝐵‘𝑁) − (𝐵‘(𝑁 + 1))))) |
| 234 | 232, 233 | mpbird 257 |
1
⊢ (𝑁 ∈ ℕ → (𝐵‘(𝑁 + 1)) < (𝐵‘𝑁)) |