Step | Hyp | Ref
| Expression |
1 | | 0red 10041 |
. . 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 477 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ 𝑘 = 1) → 𝑘 = 1) |
5 | 4 | oveq2d 6666 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝑘 = 1) → (2 · 𝑘) = (2 ·
1)) |
6 | 5 | oveq1d 6665 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ 𝑘 = 1) → ((2 · 𝑘) + 1) = ((2 · 1) +
1)) |
7 | 6 | oveq2d 6666 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ 𝑘 = 1) → (1 / ((2 ·
𝑘) + 1)) = (1 / ((2
· 1) + 1))) |
8 | 5 | oveq2d 6666 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ 𝑘 = 1) → ((1 / ((2 ·
𝑁) + 1))↑(2 ·
𝑘)) = ((1 / ((2 ·
𝑁) + 1))↑(2 ·
1))) |
9 | 7, 8 | oveq12d 6668 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ 𝑘 = 1) → ((1 / ((2 ·
𝑘) + 1)) · ((1 / ((2
· 𝑁) + 1))↑(2
· 𝑘))) = ((1 / ((2
· 1) + 1)) · ((1 / ((2 · 𝑁) + 1))↑(2 ·
1)))) |
10 | | 1nn 11031 |
. . . . . 6
⊢ 1 ∈
ℕ |
11 | 10 | a1i 11 |
. . . . 5
⊢ (𝑁 ∈ ℕ → 1 ∈
ℕ) |
12 | | 2cnd 11093 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ → 2 ∈
ℂ) |
13 | | 1cnd 10056 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ → 1 ∈
ℂ) |
14 | 12, 13 | mulcld 10060 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ → (2
· 1) ∈ ℂ) |
15 | 14, 13 | addcld 10059 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ → ((2
· 1) + 1) ∈ ℂ) |
16 | | 2t1e2 11176 |
. . . . . . . . . . 11
⊢ (2
· 1) = 2 |
17 | 16 | oveq1i 6660 |
. . . . . . . . . 10
⊢ ((2
· 1) + 1) = (2 + 1) |
18 | | 2p1e3 11151 |
. . . . . . . . . 10
⊢ (2 + 1) =
3 |
19 | 17, 18 | eqtri 2644 |
. . . . . . . . 9
⊢ ((2
· 1) + 1) = 3 |
20 | | 3ne0 11115 |
. . . . . . . . 9
⊢ 3 ≠
0 |
21 | 19, 20 | eqnetri 2864 |
. . . . . . . 8
⊢ ((2
· 1) + 1) ≠ 0 |
22 | 21 | a1i 11 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ → ((2
· 1) + 1) ≠ 0) |
23 | 15, 22 | reccld 10794 |
. . . . . 6
⊢ (𝑁 ∈ ℕ → (1 / ((2
· 1) + 1)) ∈ ℂ) |
24 | | nncn 11028 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℂ) |
25 | 12, 24 | mulcld 10060 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ → (2
· 𝑁) ∈
ℂ) |
26 | 25, 13 | addcld 10059 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ → ((2
· 𝑁) + 1) ∈
ℂ) |
27 | | 1red 10055 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ → 1 ∈
ℝ) |
28 | | 2re 11090 |
. . . . . . . . . . . . 13
⊢ 2 ∈
ℝ |
29 | 28 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℕ → 2 ∈
ℝ) |
30 | | nnre 11027 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℝ) |
31 | 29, 30 | remulcld 10070 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ → (2
· 𝑁) ∈
ℝ) |
32 | 31, 27 | readdcld 10069 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ → ((2
· 𝑁) + 1) ∈
ℝ) |
33 | | 0lt1 10550 |
. . . . . . . . . . 11
⊢ 0 <
1 |
34 | 33 | a1i 11 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ → 0 <
1) |
35 | | 2rp 11837 |
. . . . . . . . . . . . 13
⊢ 2 ∈
ℝ+ |
36 | 35 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℕ → 2 ∈
ℝ+) |
37 | | nnrp 11842 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℝ+) |
38 | 36, 37 | rpmulcld 11888 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ → (2
· 𝑁) ∈
ℝ+) |
39 | 27, 38 | ltaddrp2d 11906 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ → 1 <
((2 · 𝑁) +
1)) |
40 | 1, 27, 32, 34, 39 | lttrd 10198 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ → 0 <
((2 · 𝑁) +
1)) |
41 | 40 | gt0ne0d 10592 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ → ((2
· 𝑁) + 1) ≠
0) |
42 | 26, 41 | reccld 10794 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ → (1 / ((2
· 𝑁) + 1)) ∈
ℂ) |
43 | | 2nn0 11309 |
. . . . . . . . 9
⊢ 2 ∈
ℕ0 |
44 | 43 | a1i 11 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ → 2 ∈
ℕ0) |
45 | | 1nn0 11308 |
. . . . . . . . 9
⊢ 1 ∈
ℕ0 |
46 | 45 | a1i 11 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ → 1 ∈
ℕ0) |
47 | 44, 46 | nn0mulcld 11356 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ → (2
· 1) ∈ ℕ0) |
48 | 42, 47 | expcld 13008 |
. . . . . 6
⊢ (𝑁 ∈ ℕ → ((1 / ((2
· 𝑁) + 1))↑(2
· 1)) ∈ ℂ) |
49 | 23, 48 | mulcld 10060 |
. . . . 5
⊢ (𝑁 ∈ ℕ → ((1 / ((2
· 1) + 1)) · ((1 / ((2 · 𝑁) + 1))↑(2 · 1))) ∈
ℂ) |
50 | 3, 9, 11, 49 | fvmptd 6288 |
. . . 4
⊢ (𝑁 ∈ ℕ → (𝐾‘1) = ((1 / ((2 ·
1) + 1)) · ((1 / ((2 · 𝑁) + 1))↑(2 ·
1)))) |
51 | | 1re 10039 |
. . . . . . . . 9
⊢ 1 ∈
ℝ |
52 | 28, 51 | remulcli 10054 |
. . . . . . . 8
⊢ (2
· 1) ∈ ℝ |
53 | 52, 51 | readdcli 10053 |
. . . . . . 7
⊢ ((2
· 1) + 1) ∈ ℝ |
54 | 53, 21 | rereccli 10790 |
. . . . . 6
⊢ (1 / ((2
· 1) + 1)) ∈ ℝ |
55 | 54 | a1i 11 |
. . . . 5
⊢ (𝑁 ∈ ℕ → (1 / ((2
· 1) + 1)) ∈ ℝ) |
56 | 32, 41 | rereccld 10852 |
. . . . . 6
⊢ (𝑁 ∈ ℕ → (1 / ((2
· 𝑁) + 1)) ∈
ℝ) |
57 | 56, 47 | reexpcld 13025 |
. . . . 5
⊢ (𝑁 ∈ ℕ → ((1 / ((2
· 𝑁) + 1))↑(2
· 1)) ∈ ℝ) |
58 | 55, 57 | remulcld 10070 |
. . . 4
⊢ (𝑁 ∈ ℕ → ((1 / ((2
· 1) + 1)) · ((1 / ((2 · 𝑁) + 1))↑(2 · 1))) ∈
ℝ) |
59 | 50, 58 | eqeltrd 2701 |
. . 3
⊢ (𝑁 ∈ ℕ → (𝐾‘1) ∈
ℝ) |
60 | | stirlinglem11.1 |
. . . . . . . 8
⊢ 𝐴 = (𝑛 ∈ ℕ ↦ ((!‘𝑛) / ((√‘(2 ·
𝑛)) · ((𝑛 / e)↑𝑛)))) |
61 | 60 | stirlinglem2 40292 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ → (𝐴‘𝑁) ∈
ℝ+) |
62 | 61 | relogcld 24369 |
. . . . . 6
⊢ (𝑁 ∈ ℕ →
(log‘(𝐴‘𝑁)) ∈
ℝ) |
63 | | nfcv 2764 |
. . . . . . 7
⊢
Ⅎ𝑛𝑁 |
64 | | nfcv 2764 |
. . . . . . . 8
⊢
Ⅎ𝑛log |
65 | | nfmpt1 4747 |
. . . . . . . . . 10
⊢
Ⅎ𝑛(𝑛 ∈ ℕ ↦ ((!‘𝑛) / ((√‘(2 ·
𝑛)) · ((𝑛 / e)↑𝑛)))) |
66 | 60, 65 | nfcxfr 2762 |
. . . . . . . . 9
⊢
Ⅎ𝑛𝐴 |
67 | 66, 63 | nffv 6198 |
. . . . . . . 8
⊢
Ⅎ𝑛(𝐴‘𝑁) |
68 | 64, 67 | nffv 6198 |
. . . . . . 7
⊢
Ⅎ𝑛(log‘(𝐴‘𝑁)) |
69 | | fveq2 6191 |
. . . . . . . 8
⊢ (𝑛 = 𝑁 → (𝐴‘𝑛) = (𝐴‘𝑁)) |
70 | 69 | fveq2d 6195 |
. . . . . . 7
⊢ (𝑛 = 𝑁 → (log‘(𝐴‘𝑛)) = (log‘(𝐴‘𝑁))) |
71 | | stirlinglem11.2 |
. . . . . . 7
⊢ 𝐵 = (𝑛 ∈ ℕ ↦ (log‘(𝐴‘𝑛))) |
72 | 63, 68, 70, 71 | fvmptf 6301 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧
(log‘(𝐴‘𝑁)) ∈ ℝ) → (𝐵‘𝑁) = (log‘(𝐴‘𝑁))) |
73 | 62, 72 | mpdan 702 |
. . . . 5
⊢ (𝑁 ∈ ℕ → (𝐵‘𝑁) = (log‘(𝐴‘𝑁))) |
74 | 73, 62 | eqeltrd 2701 |
. . . 4
⊢ (𝑁 ∈ ℕ → (𝐵‘𝑁) ∈ ℝ) |
75 | | peano2nn 11032 |
. . . . . 6
⊢ (𝑁 ∈ ℕ → (𝑁 + 1) ∈
ℕ) |
76 | 60 | stirlinglem2 40292 |
. . . . . . . 8
⊢ ((𝑁 + 1) ∈ ℕ →
(𝐴‘(𝑁 + 1)) ∈
ℝ+) |
77 | 75, 76 | syl 17 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ → (𝐴‘(𝑁 + 1)) ∈
ℝ+) |
78 | 77 | relogcld 24369 |
. . . . . 6
⊢ (𝑁 ∈ ℕ →
(log‘(𝐴‘(𝑁 + 1))) ∈
ℝ) |
79 | | nfcv 2764 |
. . . . . . 7
⊢
Ⅎ𝑛(𝑁 + 1) |
80 | 66, 79 | nffv 6198 |
. . . . . . . 8
⊢
Ⅎ𝑛(𝐴‘(𝑁 + 1)) |
81 | 64, 80 | nffv 6198 |
. . . . . . 7
⊢
Ⅎ𝑛(log‘(𝐴‘(𝑁 + 1))) |
82 | | fveq2 6191 |
. . . . . . . 8
⊢ (𝑛 = (𝑁 + 1) → (𝐴‘𝑛) = (𝐴‘(𝑁 + 1))) |
83 | 82 | fveq2d 6195 |
. . . . . . 7
⊢ (𝑛 = (𝑁 + 1) → (log‘(𝐴‘𝑛)) = (log‘(𝐴‘(𝑁 + 1)))) |
84 | 79, 81, 83, 71 | fvmptf 6301 |
. . . . . 6
⊢ (((𝑁 + 1) ∈ ℕ ∧
(log‘(𝐴‘(𝑁 + 1))) ∈ ℝ) →
(𝐵‘(𝑁 + 1)) = (log‘(𝐴‘(𝑁 + 1)))) |
85 | 75, 78, 84 | syl2anc 693 |
. . . . 5
⊢ (𝑁 ∈ ℕ → (𝐵‘(𝑁 + 1)) = (log‘(𝐴‘(𝑁 + 1)))) |
86 | 85, 78 | eqeltrd 2701 |
. . . 4
⊢ (𝑁 ∈ ℕ → (𝐵‘(𝑁 + 1)) ∈ ℝ) |
87 | 74, 86 | resubcld 10458 |
. . 3
⊢ (𝑁 ∈ ℕ → ((𝐵‘𝑁) − (𝐵‘(𝑁 + 1))) ∈ ℝ) |
88 | 29, 27 | remulcld 10070 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ → (2
· 1) ∈ ℝ) |
89 | | 0le2 11111 |
. . . . . . . . . 10
⊢ 0 ≤
2 |
90 | 89 | a1i 11 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ → 0 ≤
2) |
91 | | 0le1 10551 |
. . . . . . . . . 10
⊢ 0 ≤
1 |
92 | 91 | a1i 11 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ → 0 ≤
1) |
93 | 29, 27, 90, 92 | mulge0d 10604 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ → 0 ≤ (2
· 1)) |
94 | 88, 93 | ge0p1rpd 11902 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ → ((2
· 1) + 1) ∈ ℝ+) |
95 | 94 | rpreccld 11882 |
. . . . . 6
⊢ (𝑁 ∈ ℕ → (1 / ((2
· 1) + 1)) ∈ ℝ+) |
96 | 37 | rpge0d 11876 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ → 0 ≤
𝑁) |
97 | 29, 30, 90, 96 | mulge0d 10604 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ → 0 ≤ (2
· 𝑁)) |
98 | 31, 97 | ge0p1rpd 11902 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ → ((2
· 𝑁) + 1) ∈
ℝ+) |
99 | 98 | rpreccld 11882 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ → (1 / ((2
· 𝑁) + 1)) ∈
ℝ+) |
100 | | 2z 11409 |
. . . . . . . . 9
⊢ 2 ∈
ℤ |
101 | 100 | a1i 11 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ → 2 ∈
ℤ) |
102 | | 1z 11407 |
. . . . . . . . 9
⊢ 1 ∈
ℤ |
103 | 102 | a1i 11 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ → 1 ∈
ℤ) |
104 | 101, 103 | zmulcld 11488 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ → (2
· 1) ∈ ℤ) |
105 | 99, 104 | rpexpcld 13032 |
. . . . . 6
⊢ (𝑁 ∈ ℕ → ((1 / ((2
· 𝑁) + 1))↑(2
· 1)) ∈ ℝ+) |
106 | 95, 105 | rpmulcld 11888 |
. . . . 5
⊢ (𝑁 ∈ ℕ → ((1 / ((2
· 1) + 1)) · ((1 / ((2 · 𝑁) + 1))↑(2 · 1))) ∈
ℝ+) |
107 | 50, 106 | eqeltrd 2701 |
. . . 4
⊢ (𝑁 ∈ ℕ → (𝐾‘1) ∈
ℝ+) |
108 | 107 | rpgt0d 11875 |
. . 3
⊢ (𝑁 ∈ ℕ → 0 <
(𝐾‘1)) |
109 | 87, 59 | resubcld 10458 |
. . . . 5
⊢ (𝑁 ∈ ℕ → (((𝐵‘𝑁) − (𝐵‘(𝑁 + 1))) − (𝐾‘1)) ∈ ℝ) |
110 | | eqid 2622 |
. . . . . . 7
⊢
(ℤ≥‘(1 + 1)) =
(ℤ≥‘(1 + 1)) |
111 | 103 | peano2zd 11485 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ → (1 + 1)
∈ ℤ) |
112 | | nnuz 11723 |
. . . . . . . 8
⊢ ℕ =
(ℤ≥‘1) |
113 | 2 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) → 𝐾 = (𝑘 ∈ ℕ ↦ ((1 / ((2 ·
𝑘) + 1)) · ((1 / ((2
· 𝑁) + 1))↑(2
· 𝑘))))) |
114 | | oveq2 6658 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = 𝑗 → (2 · 𝑘) = (2 · 𝑗)) |
115 | 114 | oveq1d 6665 |
. . . . . . . . . . . . 13
⊢ (𝑘 = 𝑗 → ((2 · 𝑘) + 1) = ((2 · 𝑗) + 1)) |
116 | 115 | oveq2d 6666 |
. . . . . . . . . . . 12
⊢ (𝑘 = 𝑗 → (1 / ((2 · 𝑘) + 1)) = (1 / ((2 · 𝑗) + 1))) |
117 | 114 | oveq2d 6666 |
. . . . . . . . . . . 12
⊢ (𝑘 = 𝑗 → ((1 / ((2 · 𝑁) + 1))↑(2 · 𝑘)) = ((1 / ((2 · 𝑁) + 1))↑(2 · 𝑗))) |
118 | 116, 117 | oveq12d 6668 |
. . . . . . . . . . 11
⊢ (𝑘 = 𝑗 → ((1 / ((2 · 𝑘) + 1)) · ((1 / ((2 · 𝑁) + 1))↑(2 · 𝑘))) = ((1 / ((2 · 𝑗) + 1)) · ((1 / ((2
· 𝑁) + 1))↑(2
· 𝑗)))) |
119 | 118 | adantl 482 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑘 = 𝑗) → ((1 / ((2 · 𝑘) + 1)) · ((1 / ((2
· 𝑁) + 1))↑(2
· 𝑘))) = ((1 / ((2
· 𝑗) + 1)) ·
((1 / ((2 · 𝑁) +
1))↑(2 · 𝑗)))) |
120 | | simpr 477 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) → 𝑗 ∈
ℕ) |
121 | | 2cnd 11093 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) → 2 ∈
ℂ) |
122 | | nncn 11028 |
. . . . . . . . . . . . . . 15
⊢ (𝑗 ∈ ℕ → 𝑗 ∈
ℂ) |
123 | 122 | adantl 482 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) → 𝑗 ∈
ℂ) |
124 | 121, 123 | mulcld 10060 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) → (2
· 𝑗) ∈
ℂ) |
125 | | 1cnd 10056 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) → 1 ∈
ℂ) |
126 | 124, 125 | addcld 10059 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) → ((2
· 𝑗) + 1) ∈
ℂ) |
127 | | 0red 10041 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) → 0 ∈
ℝ) |
128 | | 1red 10055 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) → 1 ∈
ℝ) |
129 | 28 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) → 2 ∈
ℝ) |
130 | | nnre 11027 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑗 ∈ ℕ → 𝑗 ∈
ℝ) |
131 | 130 | adantl 482 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) → 𝑗 ∈
ℝ) |
132 | 129, 131 | remulcld 10070 |
. . . . . . . . . . . . . . 15
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) → (2
· 𝑗) ∈
ℝ) |
133 | 132, 128 | readdcld 10069 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) → ((2
· 𝑗) + 1) ∈
ℝ) |
134 | 33 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) → 0 <
1) |
135 | 35 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) → 2 ∈
ℝ+) |
136 | | nnrp 11842 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑗 ∈ ℕ → 𝑗 ∈
ℝ+) |
137 | 136 | adantl 482 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) → 𝑗 ∈
ℝ+) |
138 | 135, 137 | rpmulcld 11888 |
. . . . . . . . . . . . . . 15
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) → (2
· 𝑗) ∈
ℝ+) |
139 | 128, 138 | ltaddrp2d 11906 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) → 1 <
((2 · 𝑗) +
1)) |
140 | 127, 128,
133, 134, 139 | lttrd 10198 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) → 0 <
((2 · 𝑗) +
1)) |
141 | 140 | gt0ne0d 10592 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) → ((2
· 𝑗) + 1) ≠
0) |
142 | 126, 141 | reccld 10794 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) → (1 / ((2
· 𝑗) + 1)) ∈
ℂ) |
143 | 24 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) → 𝑁 ∈
ℂ) |
144 | 121, 143 | mulcld 10060 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) → (2
· 𝑁) ∈
ℂ) |
145 | 144, 125 | addcld 10059 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) → ((2
· 𝑁) + 1) ∈
ℂ) |
146 | 41 | adantr 481 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) → ((2
· 𝑁) + 1) ≠
0) |
147 | 145, 146 | reccld 10794 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) → (1 / ((2
· 𝑁) + 1)) ∈
ℂ) |
148 | 43 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) → 2 ∈
ℕ0) |
149 | | nnnn0 11299 |
. . . . . . . . . . . . . 14
⊢ (𝑗 ∈ ℕ → 𝑗 ∈
ℕ0) |
150 | 149 | adantl 482 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) → 𝑗 ∈
ℕ0) |
151 | 148, 150 | nn0mulcld 11356 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) → (2
· 𝑗) ∈
ℕ0) |
152 | 147, 151 | expcld 13008 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) → ((1 /
((2 · 𝑁) +
1))↑(2 · 𝑗))
∈ ℂ) |
153 | 142, 152 | mulcld 10060 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) → ((1 /
((2 · 𝑗) + 1))
· ((1 / ((2 · 𝑁) + 1))↑(2 · 𝑗))) ∈ ℂ) |
154 | 113, 119,
120, 153 | fvmptd 6288 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) → (𝐾‘𝑗) = ((1 / ((2 · 𝑗) + 1)) · ((1 / ((2 · 𝑁) + 1))↑(2 · 𝑗)))) |
155 | | 0red 10041 |
. . . . . . . . . . . . . 14
⊢ (𝑗 ∈ ℕ → 0 ∈
ℝ) |
156 | | 1red 10055 |
. . . . . . . . . . . . . 14
⊢ (𝑗 ∈ ℕ → 1 ∈
ℝ) |
157 | 28 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (𝑗 ∈ ℕ → 2 ∈
ℝ) |
158 | 157, 130 | remulcld 10070 |
. . . . . . . . . . . . . . 15
⊢ (𝑗 ∈ ℕ → (2
· 𝑗) ∈
ℝ) |
159 | 158, 156 | readdcld 10069 |
. . . . . . . . . . . . . 14
⊢ (𝑗 ∈ ℕ → ((2
· 𝑗) + 1) ∈
ℝ) |
160 | 33 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝑗 ∈ ℕ → 0 <
1) |
161 | 35 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (𝑗 ∈ ℕ → 2 ∈
ℝ+) |
162 | 161, 136 | rpmulcld 11888 |
. . . . . . . . . . . . . . 15
⊢ (𝑗 ∈ ℕ → (2
· 𝑗) ∈
ℝ+) |
163 | 156, 162 | ltaddrp2d 11906 |
. . . . . . . . . . . . . 14
⊢ (𝑗 ∈ ℕ → 1 <
((2 · 𝑗) +
1)) |
164 | 155, 156,
159, 160, 163 | lttrd 10198 |
. . . . . . . . . . . . 13
⊢ (𝑗 ∈ ℕ → 0 <
((2 · 𝑗) +
1)) |
165 | 164 | gt0ne0d 10592 |
. . . . . . . . . . . 12
⊢ (𝑗 ∈ ℕ → ((2
· 𝑗) + 1) ≠
0) |
166 | 165 | adantl 482 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) → ((2
· 𝑗) + 1) ≠
0) |
167 | 126, 166 | reccld 10794 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) → (1 / ((2
· 𝑗) + 1)) ∈
ℂ) |
168 | 167, 152 | mulcld 10060 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) → ((1 /
((2 · 𝑗) + 1))
· ((1 / ((2 · 𝑁) + 1))↑(2 · 𝑗))) ∈ ℂ) |
169 | 154, 168 | eqeltrd 2701 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) → (𝐾‘𝑗) ∈ ℂ) |
170 | | eqid 2622 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ ↦ ((((1 +
(2 · 𝑛)) / 2)
· (log‘((𝑛 +
1) / 𝑛))) − 1)) =
(𝑛 ∈ ℕ ↦
((((1 + (2 · 𝑛)) /
2) · (log‘((𝑛
+ 1) / 𝑛))) −
1)) |
171 | 60, 71, 170, 2 | stirlinglem9 40299 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ → seq1( + ,
𝐾) ⇝ ((𝐵‘𝑁) − (𝐵‘(𝑁 + 1)))) |
172 | 112, 11, 169, 171 | clim2ser 14385 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ → seq(1 +
1)( + , 𝐾) ⇝ (((𝐵‘𝑁) − (𝐵‘(𝑁 + 1))) − (seq1( + , 𝐾)‘1))) |
173 | | peano2nn 11032 |
. . . . . . . . . . . . 13
⊢ (1 ∈
ℕ → (1 + 1) ∈ ℕ) |
174 | | uznnssnn 11735 |
. . . . . . . . . . . . 13
⊢ ((1 + 1)
∈ ℕ → (ℤ≥‘(1 + 1)) ⊆
ℕ) |
175 | 10, 173, 174 | mp2b 10 |
. . . . . . . . . . . 12
⊢
(ℤ≥‘(1 + 1)) ⊆ ℕ |
176 | 175 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ →
(ℤ≥‘(1 + 1)) ⊆ ℕ) |
177 | 176 | sseld 3602 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ → (𝑗 ∈
(ℤ≥‘(1 + 1)) → 𝑗 ∈ ℕ)) |
178 | 177 | imdistani 726 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈
(ℤ≥‘(1 + 1))) → (𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ)) |
179 | 178, 154 | syl 17 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈
(ℤ≥‘(1 + 1))) → (𝐾‘𝑗) = ((1 / ((2 · 𝑗) + 1)) · ((1 / ((2 · 𝑁) + 1))↑(2 · 𝑗)))) |
180 | 28 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝑗 ∈
(ℤ≥‘(1 + 1)) → 2 ∈
ℝ) |
181 | | eluzelre 11698 |
. . . . . . . . . . . . 13
⊢ (𝑗 ∈
(ℤ≥‘(1 + 1)) → 𝑗 ∈ ℝ) |
182 | 180, 181 | remulcld 10070 |
. . . . . . . . . . . 12
⊢ (𝑗 ∈
(ℤ≥‘(1 + 1)) → (2 · 𝑗) ∈ ℝ) |
183 | | 1red 10055 |
. . . . . . . . . . . 12
⊢ (𝑗 ∈
(ℤ≥‘(1 + 1)) → 1 ∈
ℝ) |
184 | 182, 183 | readdcld 10069 |
. . . . . . . . . . 11
⊢ (𝑗 ∈
(ℤ≥‘(1 + 1)) → ((2 · 𝑗) + 1) ∈ ℝ) |
185 | 175 | sseli 3599 |
. . . . . . . . . . . 12
⊢ (𝑗 ∈
(ℤ≥‘(1 + 1)) → 𝑗 ∈ ℕ) |
186 | 185, 165 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑗 ∈
(ℤ≥‘(1 + 1)) → ((2 · 𝑗) + 1) ≠ 0) |
187 | 184, 186 | rereccld 10852 |
. . . . . . . . . 10
⊢ (𝑗 ∈
(ℤ≥‘(1 + 1)) → (1 / ((2 · 𝑗) + 1)) ∈
ℝ) |
188 | 187 | adantl 482 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈
(ℤ≥‘(1 + 1))) → (1 / ((2 · 𝑗) + 1)) ∈
ℝ) |
189 | 32 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈
(ℤ≥‘(1 + 1))) → ((2 · 𝑁) + 1) ∈ ℝ) |
190 | 41 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈
(ℤ≥‘(1 + 1))) → ((2 · 𝑁) + 1) ≠ 0) |
191 | 189, 190 | rereccld 10852 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈
(ℤ≥‘(1 + 1))) → (1 / ((2 · 𝑁) + 1)) ∈
ℝ) |
192 | 178, 151 | syl 17 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈
(ℤ≥‘(1 + 1))) → (2 · 𝑗) ∈
ℕ0) |
193 | 191, 192 | reexpcld 13025 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈
(ℤ≥‘(1 + 1))) → ((1 / ((2 · 𝑁) + 1))↑(2 · 𝑗)) ∈
ℝ) |
194 | 188, 193 | remulcld 10070 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈
(ℤ≥‘(1 + 1))) → ((1 / ((2 · 𝑗) + 1)) · ((1 / ((2
· 𝑁) + 1))↑(2
· 𝑗))) ∈
ℝ) |
195 | 179, 194 | eqeltrd 2701 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈
(ℤ≥‘(1 + 1))) → (𝐾‘𝑗) ∈ ℝ) |
196 | | 1red 10055 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈
(ℤ≥‘(1 + 1))) → 1 ∈
ℝ) |
197 | 28 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈
(ℤ≥‘(1 + 1))) → 2 ∈
ℝ) |
198 | 178, 131 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈
(ℤ≥‘(1 + 1))) → 𝑗 ∈ ℝ) |
199 | 197, 198 | remulcld 10070 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈
(ℤ≥‘(1 + 1))) → (2 · 𝑗) ∈ ℝ) |
200 | 89 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈
(ℤ≥‘(1 + 1))) → 0 ≤ 2) |
201 | | 0red 10041 |
. . . . . . . . . . . . . 14
⊢ (𝑗 ∈
(ℤ≥‘(1 + 1)) → 0 ∈
ℝ) |
202 | 89 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝑗 ∈
(ℤ≥‘(1 + 1)) → 0 ≤ 2) |
203 | | 1p1e2 11134 |
. . . . . . . . . . . . . . 15
⊢ (1 + 1) =
2 |
204 | | eluzle 11700 |
. . . . . . . . . . . . . . 15
⊢ (𝑗 ∈
(ℤ≥‘(1 + 1)) → (1 + 1) ≤ 𝑗) |
205 | 203, 204 | syl5eqbrr 4689 |
. . . . . . . . . . . . . 14
⊢ (𝑗 ∈
(ℤ≥‘(1 + 1)) → 2 ≤ 𝑗) |
206 | 201, 180,
181, 202, 205 | letrd 10194 |
. . . . . . . . . . . . 13
⊢ (𝑗 ∈
(ℤ≥‘(1 + 1)) → 0 ≤ 𝑗) |
207 | 206 | adantl 482 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈
(ℤ≥‘(1 + 1))) → 0 ≤ 𝑗) |
208 | 197, 198,
200, 207 | mulge0d 10604 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈
(ℤ≥‘(1 + 1))) → 0 ≤ (2 · 𝑗)) |
209 | 199, 208 | ge0p1rpd 11902 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈
(ℤ≥‘(1 + 1))) → ((2 · 𝑗) + 1) ∈
ℝ+) |
210 | 91 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈
(ℤ≥‘(1 + 1))) → 0 ≤ 1) |
211 | 196, 209,
210 | divge0d 11912 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈
(ℤ≥‘(1 + 1))) → 0 ≤ (1 / ((2 · 𝑗) + 1))) |
212 | 30 | adantr 481 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈
(ℤ≥‘(1 + 1))) → 𝑁 ∈ ℝ) |
213 | 197, 212 | remulcld 10070 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈
(ℤ≥‘(1 + 1))) → (2 · 𝑁) ∈ ℝ) |
214 | 96 | adantr 481 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈
(ℤ≥‘(1 + 1))) → 0 ≤ 𝑁) |
215 | 197, 212,
200, 214 | mulge0d 10604 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈
(ℤ≥‘(1 + 1))) → 0 ≤ (2 · 𝑁)) |
216 | 213, 215 | ge0p1rpd 11902 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈
(ℤ≥‘(1 + 1))) → ((2 · 𝑁) + 1) ∈
ℝ+) |
217 | 196, 216,
210 | divge0d 11912 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈
(ℤ≥‘(1 + 1))) → 0 ≤ (1 / ((2 · 𝑁) + 1))) |
218 | 191, 192,
217 | expge0d 13026 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈
(ℤ≥‘(1 + 1))) → 0 ≤ ((1 / ((2 · 𝑁) + 1))↑(2 · 𝑗))) |
219 | 188, 193,
211, 218 | mulge0d 10604 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈
(ℤ≥‘(1 + 1))) → 0 ≤ ((1 / ((2 · 𝑗) + 1)) · ((1 / ((2
· 𝑁) + 1))↑(2
· 𝑗)))) |
220 | 219, 179 | breqtrrd 4681 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈
(ℤ≥‘(1 + 1))) → 0 ≤ (𝐾‘𝑗)) |
221 | 110, 111,
172, 195, 220 | iserge0 14391 |
. . . . . 6
⊢ (𝑁 ∈ ℕ → 0 ≤
(((𝐵‘𝑁) − (𝐵‘(𝑁 + 1))) − (seq1( + , 𝐾)‘1))) |
222 | | seq1 12814 |
. . . . . . . 8
⊢ (1 ∈
ℤ → (seq1( + , 𝐾)‘1) = (𝐾‘1)) |
223 | 102, 222 | mp1i 13 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ → (seq1( +
, 𝐾)‘1) = (𝐾‘1)) |
224 | 223 | oveq2d 6666 |
. . . . . 6
⊢ (𝑁 ∈ ℕ → (((𝐵‘𝑁) − (𝐵‘(𝑁 + 1))) − (seq1( + , 𝐾)‘1)) = (((𝐵‘𝑁) − (𝐵‘(𝑁 + 1))) − (𝐾‘1))) |
225 | 221, 224 | breqtrd 4679 |
. . . . 5
⊢ (𝑁 ∈ ℕ → 0 ≤
(((𝐵‘𝑁) − (𝐵‘(𝑁 + 1))) − (𝐾‘1))) |
226 | 1, 109, 59, 225 | leadd1dd 10641 |
. . . 4
⊢ (𝑁 ∈ ℕ → (0 +
(𝐾‘1)) ≤ ((((𝐵‘𝑁) − (𝐵‘(𝑁 + 1))) − (𝐾‘1)) + (𝐾‘1))) |
227 | 50, 49 | eqeltrd 2701 |
. . . . 5
⊢ (𝑁 ∈ ℕ → (𝐾‘1) ∈
ℂ) |
228 | 227 | addid2d 10237 |
. . . 4
⊢ (𝑁 ∈ ℕ → (0 +
(𝐾‘1)) = (𝐾‘1)) |
229 | 74 | recnd 10068 |
. . . . . 6
⊢ (𝑁 ∈ ℕ → (𝐵‘𝑁) ∈ ℂ) |
230 | 86 | recnd 10068 |
. . . . . 6
⊢ (𝑁 ∈ ℕ → (𝐵‘(𝑁 + 1)) ∈ ℂ) |
231 | 229, 230 | subcld 10392 |
. . . . 5
⊢ (𝑁 ∈ ℕ → ((𝐵‘𝑁) − (𝐵‘(𝑁 + 1))) ∈ ℂ) |
232 | 231, 227 | npcand 10396 |
. . . 4
⊢ (𝑁 ∈ ℕ → ((((𝐵‘𝑁) − (𝐵‘(𝑁 + 1))) − (𝐾‘1)) + (𝐾‘1)) = ((𝐵‘𝑁) − (𝐵‘(𝑁 + 1)))) |
233 | 226, 228,
232 | 3brtr3d 4684 |
. . 3
⊢ (𝑁 ∈ ℕ → (𝐾‘1) ≤ ((𝐵‘𝑁) − (𝐵‘(𝑁 + 1)))) |
234 | 1, 59, 87, 108, 233 | ltletrd 10197 |
. 2
⊢ (𝑁 ∈ ℕ → 0 <
((𝐵‘𝑁) − (𝐵‘(𝑁 + 1)))) |
235 | 86, 74 | posdifd 10614 |
. 2
⊢ (𝑁 ∈ ℕ → ((𝐵‘(𝑁 + 1)) < (𝐵‘𝑁) ↔ 0 < ((𝐵‘𝑁) − (𝐵‘(𝑁 + 1))))) |
236 | 234, 235 | mpbird 247 |
1
⊢ (𝑁 ∈ ℕ → (𝐵‘(𝑁 + 1)) < (𝐵‘𝑁)) |