Metamath Proof Explorer

Theorem stirlinglem11

Description: B is decreasing. (Contributed by Glauco Siliprandi, 29-Jun-2017)

Ref Expression
Hypotheses stirlinglem11.1 
|- A = ( n e. NN |-> ( ( ! ` n ) / ( ( sqrt ` ( 2 x. n ) ) x. ( ( n / _e ) ^ n ) ) ) )
stirlinglem11.2 
|- B = ( n e. NN |-> ( log ` ( A ` n ) ) )
stirlinglem11.3 
|- K = ( k e. NN |-> ( ( 1 / ( ( 2 x. k ) + 1 ) ) x. ( ( 1 / ( ( 2 x. N ) + 1 ) ) ^ ( 2 x. k ) ) ) )
Assertion stirlinglem11 
|- ( N e. NN -> ( B ` ( N + 1 ) ) < ( B ` N ) )

Proof

Step Hyp Ref Expression
1 stirlinglem11.1 
 |-  A = ( n e. NN |-> ( ( ! ` n ) / ( ( sqrt ` ( 2 x. n ) ) x. ( ( n / _e ) ^ n ) ) ) )
2 stirlinglem11.2 
 |-  B = ( n e. NN |-> ( log ` ( A ` n ) ) )
3 stirlinglem11.3 
 |-  K = ( k e. NN |-> ( ( 1 / ( ( 2 x. k ) + 1 ) ) x. ( ( 1 / ( ( 2 x. N ) + 1 ) ) ^ ( 2 x. k ) ) ) )
4 0red 
 |-  ( N e. NN -> 0 e. RR )
5 3 a1i 
 |-  ( N e. NN -> K = ( k e. NN |-> ( ( 1 / ( ( 2 x. k ) + 1 ) ) x. ( ( 1 / ( ( 2 x. N ) + 1 ) ) ^ ( 2 x. k ) ) ) ) )
6 simpr 
 |-  ( ( N e. NN /\ k = 1 ) -> k = 1 )
7 6 oveq2d 
 |-  ( ( N e. NN /\ k = 1 ) -> ( 2 x. k ) = ( 2 x. 1 ) )
8 7 oveq1d 
 |-  ( ( N e. NN /\ k = 1 ) -> ( ( 2 x. k ) + 1 ) = ( ( 2 x. 1 ) + 1 ) )
9 8 oveq2d 
 |-  ( ( N e. NN /\ k = 1 ) -> ( 1 / ( ( 2 x. k ) + 1 ) ) = ( 1 / ( ( 2 x. 1 ) + 1 ) ) )
10 7 oveq2d 
 |-  ( ( N e. NN /\ k = 1 ) -> ( ( 1 / ( ( 2 x. N ) + 1 ) ) ^ ( 2 x. k ) ) = ( ( 1 / ( ( 2 x. N ) + 1 ) ) ^ ( 2 x. 1 ) ) )
11 9 10 oveq12d 
 |-  ( ( N e. NN /\ k = 1 ) -> ( ( 1 / ( ( 2 x. k ) + 1 ) ) x. ( ( 1 / ( ( 2 x. N ) + 1 ) ) ^ ( 2 x. k ) ) ) = ( ( 1 / ( ( 2 x. 1 ) + 1 ) ) x. ( ( 1 / ( ( 2 x. N ) + 1 ) ) ^ ( 2 x. 1 ) ) ) )
12 1nn 
 |-  1 e. NN
13 12 a1i 
 |-  ( N e. NN -> 1 e. NN )
14 2cnd 
 |-  ( N e. NN -> 2 e. CC )
15 1cnd 
 |-  ( N e. NN -> 1 e. CC )
16 14 15 mulcld 
 |-  ( N e. NN -> ( 2 x. 1 ) e. CC )
17 16 15 addcld 
 |-  ( N e. NN -> ( ( 2 x. 1 ) + 1 ) e. CC )
18 2t1e2 
 |-  ( 2 x. 1 ) = 2
19 18 oveq1i 
 |-  ( ( 2 x. 1 ) + 1 ) = ( 2 + 1 )
20 2p1e3 
 |-  ( 2 + 1 ) = 3
21 19 20 eqtri 
 |-  ( ( 2 x. 1 ) + 1 ) = 3
22 3ne0 
 |-  3 =/= 0
23 21 22 eqnetri 
 |-  ( ( 2 x. 1 ) + 1 ) =/= 0
24 23 a1i 
 |-  ( N e. NN -> ( ( 2 x. 1 ) + 1 ) =/= 0 )
25 17 24 reccld 
 |-  ( N e. NN -> ( 1 / ( ( 2 x. 1 ) + 1 ) ) e. CC )
26 nncn 
 |-  ( N e. NN -> N e. CC )
27 14 26 mulcld 
 |-  ( N e. NN -> ( 2 x. N ) e. CC )
28 27 15 addcld 
 |-  ( N e. NN -> ( ( 2 x. N ) + 1 ) e. CC )
29 1red 
 |-  ( N e. NN -> 1 e. RR )
30 2re 
 |-  2 e. RR
31 30 a1i 
 |-  ( N e. NN -> 2 e. RR )
32 nnre 
 |-  ( N e. NN -> N e. RR )
33 31 32 remulcld 
 |-  ( N e. NN -> ( 2 x. N ) e. RR )
34 33 29 readdcld 
 |-  ( N e. NN -> ( ( 2 x. N ) + 1 ) e. RR )
35 0lt1 
 |-  0 < 1
36 35 a1i 
 |-  ( N e. NN -> 0 < 1 )
37 2rp 
 |-  2 e. RR+
38 37 a1i 
 |-  ( N e. NN -> 2 e. RR+ )
39 nnrp 
 |-  ( N e. NN -> N e. RR+ )
40 38 39 rpmulcld 
 |-  ( N e. NN -> ( 2 x. N ) e. RR+ )
41 29 40 ltaddrp2d 
 |-  ( N e. NN -> 1 < ( ( 2 x. N ) + 1 ) )
42 4 29 34 36 41 lttrd 
 |-  ( N e. NN -> 0 < ( ( 2 x. N ) + 1 ) )
43 42 gt0ne0d 
 |-  ( N e. NN -> ( ( 2 x. N ) + 1 ) =/= 0 )
44 28 43 reccld 
 |-  ( N e. NN -> ( 1 / ( ( 2 x. N ) + 1 ) ) e. CC )
45 2nn0 
 |-  2 e. NN0
46 45 a1i 
 |-  ( N e. NN -> 2 e. NN0 )
47 1nn0 
 |-  1 e. NN0
48 47 a1i 
 |-  ( N e. NN -> 1 e. NN0 )
49 46 48 nn0mulcld 
 |-  ( N e. NN -> ( 2 x. 1 ) e. NN0 )
50 44 49 expcld 
 |-  ( N e. NN -> ( ( 1 / ( ( 2 x. N ) + 1 ) ) ^ ( 2 x. 1 ) ) e. CC )
51 25 50 mulcld 
 |-  ( N e. NN -> ( ( 1 / ( ( 2 x. 1 ) + 1 ) ) x. ( ( 1 / ( ( 2 x. N ) + 1 ) ) ^ ( 2 x. 1 ) ) ) e. CC )
52 5 11 13 51 fvmptd 
 |-  ( N e. NN -> ( K ` 1 ) = ( ( 1 / ( ( 2 x. 1 ) + 1 ) ) x. ( ( 1 / ( ( 2 x. N ) + 1 ) ) ^ ( 2 x. 1 ) ) ) )
53 1re 
 |-  1 e. RR
54 30 53 remulcli 
 |-  ( 2 x. 1 ) e. RR
55 54 53 readdcli 
 |-  ( ( 2 x. 1 ) + 1 ) e. RR
56 55 23 rereccli 
 |-  ( 1 / ( ( 2 x. 1 ) + 1 ) ) e. RR
57 56 a1i 
 |-  ( N e. NN -> ( 1 / ( ( 2 x. 1 ) + 1 ) ) e. RR )
58 34 43 rereccld 
 |-  ( N e. NN -> ( 1 / ( ( 2 x. N ) + 1 ) ) e. RR )
59 58 49 reexpcld 
 |-  ( N e. NN -> ( ( 1 / ( ( 2 x. N ) + 1 ) ) ^ ( 2 x. 1 ) ) e. RR )
60 57 59 remulcld 
 |-  ( N e. NN -> ( ( 1 / ( ( 2 x. 1 ) + 1 ) ) x. ( ( 1 / ( ( 2 x. N ) + 1 ) ) ^ ( 2 x. 1 ) ) ) e. RR )
61 52 60 eqeltrd 
 |-  ( N e. NN -> ( K ` 1 ) e. RR )
62 1 stirlinglem2 
 |-  ( N e. NN -> ( A ` N ) e. RR+ )
63 62 relogcld 
 |-  ( N e. NN -> ( log ` ( A ` N ) ) e. RR )
64 nfcv 
 |-  F/_ n N
65 nfcv 
 |-  F/_ n log
66 nfmpt1 
 |-  F/_ n ( n e. NN |-> ( ( ! ` n ) / ( ( sqrt ` ( 2 x. n ) ) x. ( ( n / _e ) ^ n ) ) ) )
67 1 66 nfcxfr 
 |-  F/_ n A
68 67 64 nffv 
 |-  F/_ n ( A ` N )
69 65 68 nffv 
 |-  F/_ n ( log ` ( A ` N ) )
70 2fveq3 
 |-  ( n = N -> ( log ` ( A ` n ) ) = ( log ` ( A ` N ) ) )
71 64 69 70 2 fvmptf 
 |-  ( ( N e. NN /\ ( log ` ( A ` N ) ) e. RR ) -> ( B ` N ) = ( log ` ( A ` N ) ) )
72 63 71 mpdan 
 |-  ( N e. NN -> ( B ` N ) = ( log ` ( A ` N ) ) )
73 72 63 eqeltrd 
 |-  ( N e. NN -> ( B ` N ) e. RR )
74 peano2nn 
 |-  ( N e. NN -> ( N + 1 ) e. NN )
75 1 stirlinglem2 
 |-  ( ( N + 1 ) e. NN -> ( A ` ( N + 1 ) ) e. RR+ )
76 74 75 syl 
 |-  ( N e. NN -> ( A ` ( N + 1 ) ) e. RR+ )
77 76 relogcld 
 |-  ( N e. NN -> ( log ` ( A ` ( N + 1 ) ) ) e. RR )
78 nfcv 
 |-  F/_ n ( N + 1 )
79 67 78 nffv 
 |-  F/_ n ( A ` ( N + 1 ) )
80 65 79 nffv 
 |-  F/_ n ( log ` ( A ` ( N + 1 ) ) )
81 2fveq3 
 |-  ( n = ( N + 1 ) -> ( log ` ( A ` n ) ) = ( log ` ( A ` ( N + 1 ) ) ) )
82 78 80 81 2 fvmptf 
 |-  ( ( ( N + 1 ) e. NN /\ ( log ` ( A ` ( N + 1 ) ) ) e. RR ) -> ( B ` ( N + 1 ) ) = ( log ` ( A ` ( N + 1 ) ) ) )
83 74 77 82 syl2anc 
 |-  ( N e. NN -> ( B ` ( N + 1 ) ) = ( log ` ( A ` ( N + 1 ) ) ) )
84 83 77 eqeltrd 
 |-  ( N e. NN -> ( B ` ( N + 1 ) ) e. RR )
85 73 84 resubcld 
 |-  ( N e. NN -> ( ( B ` N ) - ( B ` ( N + 1 ) ) ) e. RR )
86 31 29 remulcld 
 |-  ( N e. NN -> ( 2 x. 1 ) e. RR )
87 0le2 
 |-  0 <_ 2
88 87 a1i 
 |-  ( N e. NN -> 0 <_ 2 )
89 0le1 
 |-  0 <_ 1
90 89 a1i 
 |-  ( N e. NN -> 0 <_ 1 )
91 31 29 88 90 mulge0d 
 |-  ( N e. NN -> 0 <_ ( 2 x. 1 ) )
92 86 91 ge0p1rpd 
 |-  ( N e. NN -> ( ( 2 x. 1 ) + 1 ) e. RR+ )
93 92 rpreccld 
 |-  ( N e. NN -> ( 1 / ( ( 2 x. 1 ) + 1 ) ) e. RR+ )
94 39 rpge0d 
 |-  ( N e. NN -> 0 <_ N )
95 31 32 88 94 mulge0d 
 |-  ( N e. NN -> 0 <_ ( 2 x. N ) )
96 33 95 ge0p1rpd 
 |-  ( N e. NN -> ( ( 2 x. N ) + 1 ) e. RR+ )
97 96 rpreccld 
 |-  ( N e. NN -> ( 1 / ( ( 2 x. N ) + 1 ) ) e. RR+ )
98 2z 
 |-  2 e. ZZ
99 98 a1i 
 |-  ( N e. NN -> 2 e. ZZ )
100 1z 
 |-  1 e. ZZ
101 100 a1i 
 |-  ( N e. NN -> 1 e. ZZ )
102 99 101 zmulcld 
 |-  ( N e. NN -> ( 2 x. 1 ) e. ZZ )
103 97 102 rpexpcld 
 |-  ( N e. NN -> ( ( 1 / ( ( 2 x. N ) + 1 ) ) ^ ( 2 x. 1 ) ) e. RR+ )
104 93 103 rpmulcld 
 |-  ( N e. NN -> ( ( 1 / ( ( 2 x. 1 ) + 1 ) ) x. ( ( 1 / ( ( 2 x. N ) + 1 ) ) ^ ( 2 x. 1 ) ) ) e. RR+ )
105 52 104 eqeltrd 
 |-  ( N e. NN -> ( K ` 1 ) e. RR+ )
106 105 rpgt0d 
 |-  ( N e. NN -> 0 < ( K ` 1 ) )
107 85 61 resubcld 
 |-  ( N e. NN -> ( ( ( B ` N ) - ( B ` ( N + 1 ) ) ) - ( K ` 1 ) ) e. RR )
108 eqid 
 |-  ( ZZ>= ` ( 1 + 1 ) ) = ( ZZ>= ` ( 1 + 1 ) )
109 101 peano2zd 
 |-  ( N e. NN -> ( 1 + 1 ) e. ZZ )
110 nnuz 
 |-  NN = ( ZZ>= ` 1 )
111 3 a1i 
 |-  ( ( N e. NN /\ j e. NN ) -> K = ( k e. NN |-> ( ( 1 / ( ( 2 x. k ) + 1 ) ) x. ( ( 1 / ( ( 2 x. N ) + 1 ) ) ^ ( 2 x. k ) ) ) ) )
112 oveq2 
 |-  ( k = j -> ( 2 x. k ) = ( 2 x. j ) )
113 112 oveq1d 
 |-  ( k = j -> ( ( 2 x. k ) + 1 ) = ( ( 2 x. j ) + 1 ) )
114 113 oveq2d 
 |-  ( k = j -> ( 1 / ( ( 2 x. k ) + 1 ) ) = ( 1 / ( ( 2 x. j ) + 1 ) ) )
115 112 oveq2d 
 |-  ( k = j -> ( ( 1 / ( ( 2 x. N ) + 1 ) ) ^ ( 2 x. k ) ) = ( ( 1 / ( ( 2 x. N ) + 1 ) ) ^ ( 2 x. j ) ) )
116 114 115 oveq12d 
 |-  ( k = j -> ( ( 1 / ( ( 2 x. k ) + 1 ) ) x. ( ( 1 / ( ( 2 x. N ) + 1 ) ) ^ ( 2 x. k ) ) ) = ( ( 1 / ( ( 2 x. j ) + 1 ) ) x. ( ( 1 / ( ( 2 x. N ) + 1 ) ) ^ ( 2 x. j ) ) ) )
117 116 adantl 
 |-  ( ( ( N e. NN /\ j e. NN ) /\ k = j ) -> ( ( 1 / ( ( 2 x. k ) + 1 ) ) x. ( ( 1 / ( ( 2 x. N ) + 1 ) ) ^ ( 2 x. k ) ) ) = ( ( 1 / ( ( 2 x. j ) + 1 ) ) x. ( ( 1 / ( ( 2 x. N ) + 1 ) ) ^ ( 2 x. j ) ) ) )
118 simpr 
 |-  ( ( N e. NN /\ j e. NN ) -> j e. NN )
119 2cnd 
 |-  ( ( N e. NN /\ j e. NN ) -> 2 e. CC )
120 nncn 
 |-  ( j e. NN -> j e. CC )
121 120 adantl 
 |-  ( ( N e. NN /\ j e. NN ) -> j e. CC )
122 119 121 mulcld 
 |-  ( ( N e. NN /\ j e. NN ) -> ( 2 x. j ) e. CC )
123 1cnd 
 |-  ( ( N e. NN /\ j e. NN ) -> 1 e. CC )
124 122 123 addcld 
 |-  ( ( N e. NN /\ j e. NN ) -> ( ( 2 x. j ) + 1 ) e. CC )
125 0red 
 |-  ( ( N e. NN /\ j e. NN ) -> 0 e. RR )
126 1red 
 |-  ( ( N e. NN /\ j e. NN ) -> 1 e. RR )
127 30 a1i 
 |-  ( ( N e. NN /\ j e. NN ) -> 2 e. RR )
128 nnre 
 |-  ( j e. NN -> j e. RR )
129 128 adantl 
 |-  ( ( N e. NN /\ j e. NN ) -> j e. RR )
130 127 129 remulcld 
 |-  ( ( N e. NN /\ j e. NN ) -> ( 2 x. j ) e. RR )
131 130 126 readdcld 
 |-  ( ( N e. NN /\ j e. NN ) -> ( ( 2 x. j ) + 1 ) e. RR )
132 35 a1i 
 |-  ( ( N e. NN /\ j e. NN ) -> 0 < 1 )
133 37 a1i 
 |-  ( ( N e. NN /\ j e. NN ) -> 2 e. RR+ )
134 nnrp 
 |-  ( j e. NN -> j e. RR+ )
135 134 adantl 
 |-  ( ( N e. NN /\ j e. NN ) -> j e. RR+ )
136 133 135 rpmulcld 
 |-  ( ( N e. NN /\ j e. NN ) -> ( 2 x. j ) e. RR+ )
137 126 136 ltaddrp2d 
 |-  ( ( N e. NN /\ j e. NN ) -> 1 < ( ( 2 x. j ) + 1 ) )
138 125 126 131 132 137 lttrd 
 |-  ( ( N e. NN /\ j e. NN ) -> 0 < ( ( 2 x. j ) + 1 ) )
139 138 gt0ne0d 
 |-  ( ( N e. NN /\ j e. NN ) -> ( ( 2 x. j ) + 1 ) =/= 0 )
140 124 139 reccld 
 |-  ( ( N e. NN /\ j e. NN ) -> ( 1 / ( ( 2 x. j ) + 1 ) ) e. CC )
141 26 adantr 
 |-  ( ( N e. NN /\ j e. NN ) -> N e. CC )
142 119 141 mulcld 
 |-  ( ( N e. NN /\ j e. NN ) -> ( 2 x. N ) e. CC )
143 142 123 addcld 
 |-  ( ( N e. NN /\ j e. NN ) -> ( ( 2 x. N ) + 1 ) e. CC )
144 43 adantr 
 |-  ( ( N e. NN /\ j e. NN ) -> ( ( 2 x. N ) + 1 ) =/= 0 )
145 143 144 reccld 
 |-  ( ( N e. NN /\ j e. NN ) -> ( 1 / ( ( 2 x. N ) + 1 ) ) e. CC )
146 45 a1i 
 |-  ( ( N e. NN /\ j e. NN ) -> 2 e. NN0 )
147 nnnn0 
 |-  ( j e. NN -> j e. NN0 )
148 147 adantl 
 |-  ( ( N e. NN /\ j e. NN ) -> j e. NN0 )
149 146 148 nn0mulcld 
 |-  ( ( N e. NN /\ j e. NN ) -> ( 2 x. j ) e. NN0 )
150 145 149 expcld 
 |-  ( ( N e. NN /\ j e. NN ) -> ( ( 1 / ( ( 2 x. N ) + 1 ) ) ^ ( 2 x. j ) ) e. CC )
151 140 150 mulcld 
 |-  ( ( N e. NN /\ j e. NN ) -> ( ( 1 / ( ( 2 x. j ) + 1 ) ) x. ( ( 1 / ( ( 2 x. N ) + 1 ) ) ^ ( 2 x. j ) ) ) e. CC )
152 111 117 118 151 fvmptd 
 |-  ( ( N e. NN /\ j e. NN ) -> ( K ` j ) = ( ( 1 / ( ( 2 x. j ) + 1 ) ) x. ( ( 1 / ( ( 2 x. N ) + 1 ) ) ^ ( 2 x. j ) ) ) )
153 0red 
 |-  ( j e. NN -> 0 e. RR )
154 1red 
 |-  ( j e. NN -> 1 e. RR )
155 30 a1i 
 |-  ( j e. NN -> 2 e. RR )
156 155 128 remulcld 
 |-  ( j e. NN -> ( 2 x. j ) e. RR )
157 156 154 readdcld 
 |-  ( j e. NN -> ( ( 2 x. j ) + 1 ) e. RR )
158 35 a1i 
 |-  ( j e. NN -> 0 < 1 )
159 37 a1i 
 |-  ( j e. NN -> 2 e. RR+ )
160 159 134 rpmulcld 
 |-  ( j e. NN -> ( 2 x. j ) e. RR+ )
161 154 160 ltaddrp2d 
 |-  ( j e. NN -> 1 < ( ( 2 x. j ) + 1 ) )
162 153 154 157 158 161 lttrd 
 |-  ( j e. NN -> 0 < ( ( 2 x. j ) + 1 ) )
163 162 gt0ne0d 
 |-  ( j e. NN -> ( ( 2 x. j ) + 1 ) =/= 0 )
164 163 adantl 
 |-  ( ( N e. NN /\ j e. NN ) -> ( ( 2 x. j ) + 1 ) =/= 0 )
165 124 164 reccld 
 |-  ( ( N e. NN /\ j e. NN ) -> ( 1 / ( ( 2 x. j ) + 1 ) ) e. CC )
166 165 150 mulcld 
 |-  ( ( N e. NN /\ j e. NN ) -> ( ( 1 / ( ( 2 x. j ) + 1 ) ) x. ( ( 1 / ( ( 2 x. N ) + 1 ) ) ^ ( 2 x. j ) ) ) e. CC )
167 152 166 eqeltrd 
 |-  ( ( N e. NN /\ j e. NN ) -> ( K ` j ) e. CC )
168 eqid 
 |-  ( n e. NN |-> ( ( ( ( 1 + ( 2 x. n ) ) / 2 ) x. ( log ` ( ( n + 1 ) / n ) ) ) - 1 ) ) = ( n e. NN |-> ( ( ( ( 1 + ( 2 x. n ) ) / 2 ) x. ( log ` ( ( n + 1 ) / n ) ) ) - 1 ) )
169 1 2 168 3 stirlinglem9 
 |-  ( N e. NN -> seq 1 ( + , K ) ~~> ( ( B ` N ) - ( B ` ( N + 1 ) ) ) )
170 110 13 167 169 clim2ser 
 |-  ( N e. NN -> seq ( 1 + 1 ) ( + , K ) ~~> ( ( ( B ` N ) - ( B ` ( N + 1 ) ) ) - ( seq 1 ( + , K ) ` 1 ) ) )
171 peano2nn 
 |-  ( 1 e. NN -> ( 1 + 1 ) e. NN )
172 uznnssnn 
 |-  ( ( 1 + 1 ) e. NN -> ( ZZ>= ` ( 1 + 1 ) ) C_ NN )
173 12 171 172 mp2b 
 |-  ( ZZ>= ` ( 1 + 1 ) ) C_ NN
174 173 a1i 
 |-  ( N e. NN -> ( ZZ>= ` ( 1 + 1 ) ) C_ NN )
175 174 sseld 
 |-  ( N e. NN -> ( j e. ( ZZ>= ` ( 1 + 1 ) ) -> j e. NN ) )
176 175 imdistani 
 |-  ( ( N e. NN /\ j e. ( ZZ>= ` ( 1 + 1 ) ) ) -> ( N e. NN /\ j e. NN ) )
177 176 152 syl 
 |-  ( ( N e. NN /\ j e. ( ZZ>= ` ( 1 + 1 ) ) ) -> ( K ` j ) = ( ( 1 / ( ( 2 x. j ) + 1 ) ) x. ( ( 1 / ( ( 2 x. N ) + 1 ) ) ^ ( 2 x. j ) ) ) )
178 30 a1i 
 |-  ( j e. ( ZZ>= ` ( 1 + 1 ) ) -> 2 e. RR )
179 eluzelre 
 |-  ( j e. ( ZZ>= ` ( 1 + 1 ) ) -> j e. RR )
180 178 179 remulcld 
 |-  ( j e. ( ZZ>= ` ( 1 + 1 ) ) -> ( 2 x. j ) e. RR )
181 1red 
 |-  ( j e. ( ZZ>= ` ( 1 + 1 ) ) -> 1 e. RR )
182 180 181 readdcld 
 |-  ( j e. ( ZZ>= ` ( 1 + 1 ) ) -> ( ( 2 x. j ) + 1 ) e. RR )
183 173 sseli 
 |-  ( j e. ( ZZ>= ` ( 1 + 1 ) ) -> j e. NN )
184 183 163 syl 
 |-  ( j e. ( ZZ>= ` ( 1 + 1 ) ) -> ( ( 2 x. j ) + 1 ) =/= 0 )
185 182 184 rereccld 
 |-  ( j e. ( ZZ>= ` ( 1 + 1 ) ) -> ( 1 / ( ( 2 x. j ) + 1 ) ) e. RR )
186 185 adantl 
 |-  ( ( N e. NN /\ j e. ( ZZ>= ` ( 1 + 1 ) ) ) -> ( 1 / ( ( 2 x. j ) + 1 ) ) e. RR )
187 34 adantr 
 |-  ( ( N e. NN /\ j e. ( ZZ>= ` ( 1 + 1 ) ) ) -> ( ( 2 x. N ) + 1 ) e. RR )
188 43 adantr 
 |-  ( ( N e. NN /\ j e. ( ZZ>= ` ( 1 + 1 ) ) ) -> ( ( 2 x. N ) + 1 ) =/= 0 )
189 187 188 rereccld 
 |-  ( ( N e. NN /\ j e. ( ZZ>= ` ( 1 + 1 ) ) ) -> ( 1 / ( ( 2 x. N ) + 1 ) ) e. RR )
190 176 149 syl 
 |-  ( ( N e. NN /\ j e. ( ZZ>= ` ( 1 + 1 ) ) ) -> ( 2 x. j ) e. NN0 )
191 189 190 reexpcld 
 |-  ( ( N e. NN /\ j e. ( ZZ>= ` ( 1 + 1 ) ) ) -> ( ( 1 / ( ( 2 x. N ) + 1 ) ) ^ ( 2 x. j ) ) e. RR )
192 186 191 remulcld 
 |-  ( ( N e. NN /\ j e. ( ZZ>= ` ( 1 + 1 ) ) ) -> ( ( 1 / ( ( 2 x. j ) + 1 ) ) x. ( ( 1 / ( ( 2 x. N ) + 1 ) ) ^ ( 2 x. j ) ) ) e. RR )
193 177 192 eqeltrd 
 |-  ( ( N e. NN /\ j e. ( ZZ>= ` ( 1 + 1 ) ) ) -> ( K ` j ) e. RR )
194 1red 
 |-  ( ( N e. NN /\ j e. ( ZZ>= ` ( 1 + 1 ) ) ) -> 1 e. RR )
195 30 a1i 
 |-  ( ( N e. NN /\ j e. ( ZZ>= ` ( 1 + 1 ) ) ) -> 2 e. RR )
196 176 129 syl 
 |-  ( ( N e. NN /\ j e. ( ZZ>= ` ( 1 + 1 ) ) ) -> j e. RR )
197 195 196 remulcld 
 |-  ( ( N e. NN /\ j e. ( ZZ>= ` ( 1 + 1 ) ) ) -> ( 2 x. j ) e. RR )
198 87 a1i 
 |-  ( ( N e. NN /\ j e. ( ZZ>= ` ( 1 + 1 ) ) ) -> 0 <_ 2 )
199 0red 
 |-  ( j e. ( ZZ>= ` ( 1 + 1 ) ) -> 0 e. RR )
200 87 a1i 
 |-  ( j e. ( ZZ>= ` ( 1 + 1 ) ) -> 0 <_ 2 )
201 1p1e2 
 |-  ( 1 + 1 ) = 2
202 eluzle 
 |-  ( j e. ( ZZ>= ` ( 1 + 1 ) ) -> ( 1 + 1 ) <_ j )
203 201 202 eqbrtrrid 
 |-  ( j e. ( ZZ>= ` ( 1 + 1 ) ) -> 2 <_ j )
204 199 178 179 200 203 letrd 
 |-  ( j e. ( ZZ>= ` ( 1 + 1 ) ) -> 0 <_ j )
205 204 adantl 
 |-  ( ( N e. NN /\ j e. ( ZZ>= ` ( 1 + 1 ) ) ) -> 0 <_ j )
206 195 196 198 205 mulge0d 
 |-  ( ( N e. NN /\ j e. ( ZZ>= ` ( 1 + 1 ) ) ) -> 0 <_ ( 2 x. j ) )
207 197 206 ge0p1rpd 
 |-  ( ( N e. NN /\ j e. ( ZZ>= ` ( 1 + 1 ) ) ) -> ( ( 2 x. j ) + 1 ) e. RR+ )
208 89 a1i 
 |-  ( ( N e. NN /\ j e. ( ZZ>= ` ( 1 + 1 ) ) ) -> 0 <_ 1 )
209 194 207 208 divge0d 
 |-  ( ( N e. NN /\ j e. ( ZZ>= ` ( 1 + 1 ) ) ) -> 0 <_ ( 1 / ( ( 2 x. j ) + 1 ) ) )
210 32 adantr 
 |-  ( ( N e. NN /\ j e. ( ZZ>= ` ( 1 + 1 ) ) ) -> N e. RR )
211 195 210 remulcld 
 |-  ( ( N e. NN /\ j e. ( ZZ>= ` ( 1 + 1 ) ) ) -> ( 2 x. N ) e. RR )
212 94 adantr 
 |-  ( ( N e. NN /\ j e. ( ZZ>= ` ( 1 + 1 ) ) ) -> 0 <_ N )
213 195 210 198 212 mulge0d 
 |-  ( ( N e. NN /\ j e. ( ZZ>= ` ( 1 + 1 ) ) ) -> 0 <_ ( 2 x. N ) )
214 211 213 ge0p1rpd 
 |-  ( ( N e. NN /\ j e. ( ZZ>= ` ( 1 + 1 ) ) ) -> ( ( 2 x. N ) + 1 ) e. RR+ )
215 194 214 208 divge0d 
 |-  ( ( N e. NN /\ j e. ( ZZ>= ` ( 1 + 1 ) ) ) -> 0 <_ ( 1 / ( ( 2 x. N ) + 1 ) ) )
216 189 190 215 expge0d 
 |-  ( ( N e. NN /\ j e. ( ZZ>= ` ( 1 + 1 ) ) ) -> 0 <_ ( ( 1 / ( ( 2 x. N ) + 1 ) ) ^ ( 2 x. j ) ) )
217 186 191 209 216 mulge0d 
 |-  ( ( N e. NN /\ j e. ( ZZ>= ` ( 1 + 1 ) ) ) -> 0 <_ ( ( 1 / ( ( 2 x. j ) + 1 ) ) x. ( ( 1 / ( ( 2 x. N ) + 1 ) ) ^ ( 2 x. j ) ) ) )
218 217 177 breqtrrd 
 |-  ( ( N e. NN /\ j e. ( ZZ>= ` ( 1 + 1 ) ) ) -> 0 <_ ( K ` j ) )
219 108 109 170 193 218 iserge0 
 |-  ( N e. NN -> 0 <_ ( ( ( B ` N ) - ( B ` ( N + 1 ) ) ) - ( seq 1 ( + , K ) ` 1 ) ) )
220 seq1 
 |-  ( 1 e. ZZ -> ( seq 1 ( + , K ) ` 1 ) = ( K ` 1 ) )
221 100 220 mp1i 
 |-  ( N e. NN -> ( seq 1 ( + , K ) ` 1 ) = ( K ` 1 ) )
222 221 oveq2d 
 |-  ( N e. NN -> ( ( ( B ` N ) - ( B ` ( N + 1 ) ) ) - ( seq 1 ( + , K ) ` 1 ) ) = ( ( ( B ` N ) - ( B ` ( N + 1 ) ) ) - ( K ` 1 ) ) )
223 219 222 breqtrd 
 |-  ( N e. NN -> 0 <_ ( ( ( B ` N ) - ( B ` ( N + 1 ) ) ) - ( K ` 1 ) ) )
224 4 107 61 223 leadd1dd 
 |-  ( N e. NN -> ( 0 + ( K ` 1 ) ) <_ ( ( ( ( B ` N ) - ( B ` ( N + 1 ) ) ) - ( K ` 1 ) ) + ( K ` 1 ) ) )
225 52 51 eqeltrd 
 |-  ( N e. NN -> ( K ` 1 ) e. CC )
226 225 addid2d 
 |-  ( N e. NN -> ( 0 + ( K ` 1 ) ) = ( K ` 1 ) )
227 73 recnd 
 |-  ( N e. NN -> ( B ` N ) e. CC )
228 84 recnd 
 |-  ( N e. NN -> ( B ` ( N + 1 ) ) e. CC )
229 227 228 subcld 
 |-  ( N e. NN -> ( ( B ` N ) - ( B ` ( N + 1 ) ) ) e. CC )
230 229 225 npcand 
 |-  ( N e. NN -> ( ( ( ( B ` N ) - ( B ` ( N + 1 ) ) ) - ( K ` 1 ) ) + ( K ` 1 ) ) = ( ( B ` N ) - ( B ` ( N + 1 ) ) ) )
231 224 226 230 3brtr3d 
 |-  ( N e. NN -> ( K ` 1 ) <_ ( ( B ` N ) - ( B ` ( N + 1 ) ) ) )
232 4 61 85 106 231 ltletrd 
 |-  ( N e. NN -> 0 < ( ( B ` N ) - ( B ` ( N + 1 ) ) ) )
233 84 73 posdifd 
 |-  ( N e. NN -> ( ( B ` ( N + 1 ) ) < ( B ` N ) <-> 0 < ( ( B ` N ) - ( B ` ( N + 1 ) ) ) ) )
234 232 233 mpbird 
 |-  ( N e. NN -> ( B ` ( N + 1 ) ) < ( B ` N ) )