Proof of Theorem stirlinglem6
| Step | Hyp | Ref
| Expression |
| 1 | | eqid 2737 |
. . 3
⊢ (𝑗 ∈ ℕ ↦
((-1↑(𝑗 − 1))
· (((1 / ((2 · 𝑁) + 1))↑𝑗) / 𝑗))) = (𝑗 ∈ ℕ ↦ ((-1↑(𝑗 − 1)) · (((1 / ((2
· 𝑁) +
1))↑𝑗) / 𝑗))) |
| 2 | | eqid 2737 |
. . 3
⊢ (𝑗 ∈ ℕ ↦ (((1 /
((2 · 𝑁) +
1))↑𝑗) / 𝑗)) = (𝑗 ∈ ℕ ↦ (((1 / ((2 ·
𝑁) + 1))↑𝑗) / 𝑗)) |
| 3 | | eqid 2737 |
. . 3
⊢ (𝑗 ∈ ℕ ↦
(((-1↑(𝑗 − 1))
· (((1 / ((2 · 𝑁) + 1))↑𝑗) / 𝑗)) + (((1 / ((2 · 𝑁) + 1))↑𝑗) / 𝑗))) = (𝑗 ∈ ℕ ↦ (((-1↑(𝑗 − 1)) · (((1 / ((2
· 𝑁) +
1))↑𝑗) / 𝑗)) + (((1 / ((2 · 𝑁) + 1))↑𝑗) / 𝑗))) |
| 4 | | stirlinglem6.1 |
. . 3
⊢ 𝐻 = (𝑗 ∈ ℕ0 ↦ (2
· ((1 / ((2 · 𝑗) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑗) + 1))))) |
| 5 | | eqid 2737 |
. . 3
⊢ (𝑗 ∈ ℕ0
↦ ((2 · 𝑗) +
1)) = (𝑗 ∈
ℕ0 ↦ ((2 · 𝑗) + 1)) |
| 6 | | 2re 12340 |
. . . . . . 7
⊢ 2 ∈
ℝ |
| 7 | 6 | a1i 11 |
. . . . . 6
⊢ (𝑁 ∈ ℕ → 2 ∈
ℝ) |
| 8 | | nnre 12273 |
. . . . . 6
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℝ) |
| 9 | 7, 8 | remulcld 11291 |
. . . . 5
⊢ (𝑁 ∈ ℕ → (2
· 𝑁) ∈
ℝ) |
| 10 | | 0le2 12368 |
. . . . . . 7
⊢ 0 ≤
2 |
| 11 | 10 | a1i 11 |
. . . . . 6
⊢ (𝑁 ∈ ℕ → 0 ≤
2) |
| 12 | | 0red 11264 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ → 0 ∈
ℝ) |
| 13 | | nngt0 12297 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ → 0 <
𝑁) |
| 14 | 12, 8, 13 | ltled 11409 |
. . . . . 6
⊢ (𝑁 ∈ ℕ → 0 ≤
𝑁) |
| 15 | 7, 8, 11, 14 | mulge0d 11840 |
. . . . 5
⊢ (𝑁 ∈ ℕ → 0 ≤ (2
· 𝑁)) |
| 16 | 9, 15 | ge0p1rpd 13107 |
. . . 4
⊢ (𝑁 ∈ ℕ → ((2
· 𝑁) + 1) ∈
ℝ+) |
| 17 | 16 | rpreccld 13087 |
. . 3
⊢ (𝑁 ∈ ℕ → (1 / ((2
· 𝑁) + 1)) ∈
ℝ+) |
| 18 | | 1red 11262 |
. . . . . 6
⊢ (𝑁 ∈ ℕ → 1 ∈
ℝ) |
| 19 | 18 | renegcld 11690 |
. . . . 5
⊢ (𝑁 ∈ ℕ → -1 ∈
ℝ) |
| 20 | 17 | rpred 13077 |
. . . . 5
⊢ (𝑁 ∈ ℕ → (1 / ((2
· 𝑁) + 1)) ∈
ℝ) |
| 21 | | neg1lt0 12383 |
. . . . . 6
⊢ -1 <
0 |
| 22 | 21 | a1i 11 |
. . . . 5
⊢ (𝑁 ∈ ℕ → -1 <
0) |
| 23 | 17 | rpgt0d 13080 |
. . . . 5
⊢ (𝑁 ∈ ℕ → 0 < (1
/ ((2 · 𝑁) +
1))) |
| 24 | 19, 12, 20, 22, 23 | lttrd 11422 |
. . . 4
⊢ (𝑁 ∈ ℕ → -1 <
(1 / ((2 · 𝑁) +
1))) |
| 25 | | 1rp 13038 |
. . . . . 6
⊢ 1 ∈
ℝ+ |
| 26 | 25 | a1i 11 |
. . . . 5
⊢ (𝑁 ∈ ℕ → 1 ∈
ℝ+) |
| 27 | | 1cnd 11256 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ → 1 ∈
ℂ) |
| 28 | 27 | div1d 12035 |
. . . . . 6
⊢ (𝑁 ∈ ℕ → (1 / 1) =
1) |
| 29 | | 2rp 13039 |
. . . . . . . . 9
⊢ 2 ∈
ℝ+ |
| 30 | 29 | a1i 11 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ → 2 ∈
ℝ+) |
| 31 | | nnrp 13046 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℝ+) |
| 32 | 30, 31 | rpmulcld 13093 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ → (2
· 𝑁) ∈
ℝ+) |
| 33 | 18, 32 | ltaddrp2d 13111 |
. . . . . 6
⊢ (𝑁 ∈ ℕ → 1 <
((2 · 𝑁) +
1)) |
| 34 | 28, 33 | eqbrtrd 5165 |
. . . . 5
⊢ (𝑁 ∈ ℕ → (1 / 1)
< ((2 · 𝑁) +
1)) |
| 35 | 26, 16, 34 | ltrec1d 13097 |
. . . 4
⊢ (𝑁 ∈ ℕ → (1 / ((2
· 𝑁) + 1)) <
1) |
| 36 | 20, 18 | absltd 15468 |
. . . 4
⊢ (𝑁 ∈ ℕ →
((abs‘(1 / ((2 · 𝑁) + 1))) < 1 ↔ (-1 < (1 / ((2
· 𝑁) + 1)) ∧ (1
/ ((2 · 𝑁) + 1))
< 1))) |
| 37 | 24, 35, 36 | mpbir2and 713 |
. . 3
⊢ (𝑁 ∈ ℕ →
(abs‘(1 / ((2 · 𝑁) + 1))) < 1) |
| 38 | 1, 2, 3, 4, 5, 17,
37 | stirlinglem5 46093 |
. 2
⊢ (𝑁 ∈ ℕ → seq0( + ,
𝐻) ⇝ (log‘((1 +
(1 / ((2 · 𝑁) + 1)))
/ (1 − (1 / ((2 · 𝑁) + 1)))))) |
| 39 | | 2cnd 12344 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ → 2 ∈
ℂ) |
| 40 | | nncn 12274 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℂ) |
| 41 | 39, 40 | mulcld 11281 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ → (2
· 𝑁) ∈
ℂ) |
| 42 | 41, 27 | addcld 11280 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ → ((2
· 𝑁) + 1) ∈
ℂ) |
| 43 | 9, 18 | readdcld 11290 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ → ((2
· 𝑁) + 1) ∈
ℝ) |
| 44 | | 2pos 12369 |
. . . . . . . . . . . 12
⊢ 0 <
2 |
| 45 | 44 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ → 0 <
2) |
| 46 | 7, 8, 45, 13 | mulgt0d 11416 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ → 0 < (2
· 𝑁)) |
| 47 | 9 | ltp1d 12198 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ → (2
· 𝑁) < ((2
· 𝑁) +
1)) |
| 48 | 12, 9, 43, 46, 47 | lttrd 11422 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ → 0 <
((2 · 𝑁) +
1)) |
| 49 | 48 | gt0ne0d 11827 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ → ((2
· 𝑁) + 1) ≠
0) |
| 50 | 42, 49 | dividd 12041 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ → (((2
· 𝑁) + 1) / ((2
· 𝑁) + 1)) =
1) |
| 51 | 50 | eqcomd 2743 |
. . . . . 6
⊢ (𝑁 ∈ ℕ → 1 = (((2
· 𝑁) + 1) / ((2
· 𝑁) +
1))) |
| 52 | 51 | oveq1d 7446 |
. . . . 5
⊢ (𝑁 ∈ ℕ → (1 + (1 /
((2 · 𝑁) + 1))) =
((((2 · 𝑁) + 1) /
((2 · 𝑁) + 1)) + (1
/ ((2 · 𝑁) +
1)))) |
| 53 | 51 | oveq1d 7446 |
. . . . 5
⊢ (𝑁 ∈ ℕ → (1
− (1 / ((2 · 𝑁) + 1))) = ((((2 · 𝑁) + 1) / ((2 · 𝑁) + 1)) − (1 / ((2 · 𝑁) + 1)))) |
| 54 | 52, 53 | oveq12d 7449 |
. . . 4
⊢ (𝑁 ∈ ℕ → ((1 + (1
/ ((2 · 𝑁) + 1))) /
(1 − (1 / ((2 · 𝑁) + 1)))) = (((((2 · 𝑁) + 1) / ((2 · 𝑁) + 1)) + (1 / ((2 ·
𝑁) + 1))) / ((((2 ·
𝑁) + 1) / ((2 ·
𝑁) + 1)) − (1 / ((2
· 𝑁) +
1))))) |
| 55 | 42, 27, 42, 49 | divdird 12081 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ → ((((2
· 𝑁) + 1) + 1) / ((2
· 𝑁) + 1)) = ((((2
· 𝑁) + 1) / ((2
· 𝑁) + 1)) + (1 /
((2 · 𝑁) +
1)))) |
| 56 | 55 | eqcomd 2743 |
. . . . . 6
⊢ (𝑁 ∈ ℕ → ((((2
· 𝑁) + 1) / ((2
· 𝑁) + 1)) + (1 /
((2 · 𝑁) + 1))) =
((((2 · 𝑁) + 1) + 1)
/ ((2 · 𝑁) +
1))) |
| 57 | 42, 27, 42, 49 | divsubdird 12082 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ → ((((2
· 𝑁) + 1) − 1)
/ ((2 · 𝑁) + 1)) =
((((2 · 𝑁) + 1) /
((2 · 𝑁) + 1))
− (1 / ((2 · 𝑁) + 1)))) |
| 58 | 57 | eqcomd 2743 |
. . . . . 6
⊢ (𝑁 ∈ ℕ → ((((2
· 𝑁) + 1) / ((2
· 𝑁) + 1)) −
(1 / ((2 · 𝑁) + 1)))
= ((((2 · 𝑁) + 1)
− 1) / ((2 · 𝑁) + 1))) |
| 59 | 56, 58 | oveq12d 7449 |
. . . . 5
⊢ (𝑁 ∈ ℕ → (((((2
· 𝑁) + 1) / ((2
· 𝑁) + 1)) + (1 /
((2 · 𝑁) + 1))) /
((((2 · 𝑁) + 1) /
((2 · 𝑁) + 1))
− (1 / ((2 · 𝑁) + 1)))) = (((((2 · 𝑁) + 1) + 1) / ((2 · 𝑁) + 1)) / ((((2 · 𝑁) + 1) − 1) / ((2 ·
𝑁) + 1)))) |
| 60 | 41, 27, 27 | addassd 11283 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ → (((2
· 𝑁) + 1) + 1) = ((2
· 𝑁) + (1 +
1))) |
| 61 | | 1p1e2 12391 |
. . . . . . . . . 10
⊢ (1 + 1) =
2 |
| 62 | 61 | a1i 11 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ → (1 + 1) =
2) |
| 63 | 62 | oveq2d 7447 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ → ((2
· 𝑁) + (1 + 1)) =
((2 · 𝑁) +
2)) |
| 64 | 39 | mulridd 11278 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ → (2
· 1) = 2) |
| 65 | 64 | eqcomd 2743 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ → 2 = (2
· 1)) |
| 66 | 65 | oveq2d 7447 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ → ((2
· 𝑁) + 2) = ((2
· 𝑁) + (2 ·
1))) |
| 67 | 39, 40, 27 | adddid 11285 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ → (2
· (𝑁 + 1)) = ((2
· 𝑁) + (2 ·
1))) |
| 68 | 66, 67 | eqtr4d 2780 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ → ((2
· 𝑁) + 2) = (2
· (𝑁 +
1))) |
| 69 | 60, 63, 68 | 3eqtrd 2781 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ → (((2
· 𝑁) + 1) + 1) = (2
· (𝑁 +
1))) |
| 70 | 69 | oveq1d 7446 |
. . . . . 6
⊢ (𝑁 ∈ ℕ → ((((2
· 𝑁) + 1) + 1) / ((2
· 𝑁) + 1)) = ((2
· (𝑁 + 1)) / ((2
· 𝑁) +
1))) |
| 71 | 41, 27 | pncand 11621 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ → (((2
· 𝑁) + 1) − 1)
= (2 · 𝑁)) |
| 72 | 71 | oveq1d 7446 |
. . . . . 6
⊢ (𝑁 ∈ ℕ → ((((2
· 𝑁) + 1) − 1)
/ ((2 · 𝑁) + 1)) =
((2 · 𝑁) / ((2
· 𝑁) +
1))) |
| 73 | 70, 72 | oveq12d 7449 |
. . . . 5
⊢ (𝑁 ∈ ℕ → (((((2
· 𝑁) + 1) + 1) / ((2
· 𝑁) + 1)) / ((((2
· 𝑁) + 1) − 1)
/ ((2 · 𝑁) + 1))) =
(((2 · (𝑁 + 1)) /
((2 · 𝑁) + 1)) / ((2
· 𝑁) / ((2 ·
𝑁) + 1)))) |
| 74 | 59, 73 | eqtrd 2777 |
. . . 4
⊢ (𝑁 ∈ ℕ → (((((2
· 𝑁) + 1) / ((2
· 𝑁) + 1)) + (1 /
((2 · 𝑁) + 1))) /
((((2 · 𝑁) + 1) /
((2 · 𝑁) + 1))
− (1 / ((2 · 𝑁) + 1)))) = (((2 · (𝑁 + 1)) / ((2 · 𝑁) + 1)) / ((2 · 𝑁) / ((2 · 𝑁) + 1)))) |
| 75 | 40, 27 | addcld 11280 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ → (𝑁 + 1) ∈
ℂ) |
| 76 | 39, 75 | mulcld 11281 |
. . . . . 6
⊢ (𝑁 ∈ ℕ → (2
· (𝑁 + 1)) ∈
ℂ) |
| 77 | 46 | gt0ne0d 11827 |
. . . . . 6
⊢ (𝑁 ∈ ℕ → (2
· 𝑁) ≠
0) |
| 78 | 76, 41, 42, 77, 49 | divcan7d 12071 |
. . . . 5
⊢ (𝑁 ∈ ℕ → (((2
· (𝑁 + 1)) / ((2
· 𝑁) + 1)) / ((2
· 𝑁) / ((2 ·
𝑁) + 1))) = ((2 ·
(𝑁 + 1)) / (2 ·
𝑁))) |
| 79 | 45 | gt0ne0d 11827 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ → 2 ≠
0) |
| 80 | 13 | gt0ne0d 11827 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ → 𝑁 ≠ 0) |
| 81 | 39, 39, 75, 40, 79, 80 | divmuldivd 12084 |
. . . . . 6
⊢ (𝑁 ∈ ℕ → ((2 / 2)
· ((𝑁 + 1) / 𝑁)) = ((2 · (𝑁 + 1)) / (2 · 𝑁))) |
| 82 | 81 | eqcomd 2743 |
. . . . 5
⊢ (𝑁 ∈ ℕ → ((2
· (𝑁 + 1)) / (2
· 𝑁)) = ((2 / 2)
· ((𝑁 + 1) / 𝑁))) |
| 83 | 39, 79 | dividd 12041 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ → (2 / 2) =
1) |
| 84 | 83 | oveq1d 7446 |
. . . . . 6
⊢ (𝑁 ∈ ℕ → ((2 / 2)
· ((𝑁 + 1) / 𝑁)) = (1 · ((𝑁 + 1) / 𝑁))) |
| 85 | 75, 40, 80 | divcld 12043 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ → ((𝑁 + 1) / 𝑁) ∈ ℂ) |
| 86 | 85 | mullidd 11279 |
. . . . . 6
⊢ (𝑁 ∈ ℕ → (1
· ((𝑁 + 1) / 𝑁)) = ((𝑁 + 1) / 𝑁)) |
| 87 | 84, 86 | eqtrd 2777 |
. . . . 5
⊢ (𝑁 ∈ ℕ → ((2 / 2)
· ((𝑁 + 1) / 𝑁)) = ((𝑁 + 1) / 𝑁)) |
| 88 | 78, 82, 87 | 3eqtrd 2781 |
. . . 4
⊢ (𝑁 ∈ ℕ → (((2
· (𝑁 + 1)) / ((2
· 𝑁) + 1)) / ((2
· 𝑁) / ((2 ·
𝑁) + 1))) = ((𝑁 + 1) / 𝑁)) |
| 89 | 54, 74, 88 | 3eqtrd 2781 |
. . 3
⊢ (𝑁 ∈ ℕ → ((1 + (1
/ ((2 · 𝑁) + 1))) /
(1 − (1 / ((2 · 𝑁) + 1)))) = ((𝑁 + 1) / 𝑁)) |
| 90 | 89 | fveq2d 6910 |
. 2
⊢ (𝑁 ∈ ℕ →
(log‘((1 + (1 / ((2 · 𝑁) + 1))) / (1 − (1 / ((2 ·
𝑁) + 1))))) =
(log‘((𝑁 + 1) / 𝑁))) |
| 91 | 38, 90 | breqtrd 5169 |
1
⊢ (𝑁 ∈ ℕ → seq0( + ,
𝐻) ⇝
(log‘((𝑁 + 1) / 𝑁))) |