Metamath Proof Explorer

Theorem stirlinglem12

Description: The sequence B is bounded below. (Contributed by Glauco Siliprandi, 29-Jun-2017)

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

Proof

Step Hyp Ref Expression
1 stirlinglem12.1 
 |-  A = ( n e. NN |-> ( ( ! ` n ) / ( ( sqrt ` ( 2 x. n ) ) x. ( ( n / _e ) ^ n ) ) ) )
2 stirlinglem12.2 
 |-  B = ( n e. NN |-> ( log ` ( A ` n ) ) )
3 stirlinglem12.3 
 |-  F = ( n e. NN |-> ( 1 / ( n x. ( n + 1 ) ) ) )
4 1nn 
 |-  1 e. NN
5 1 stirlinglem2 
 |-  ( 1 e. NN -> ( A ` 1 ) e. RR+ )
6 relogcl 
 |-  ( ( A ` 1 ) e. RR+ -> ( log ` ( A ` 1 ) ) e. RR )
7 4 5 6 mp2b 
 |-  ( log ` ( A ` 1 ) ) e. RR
8 nfcv 
 |-  F/_ n 1
9 nfcv 
 |-  F/_ n log
10 nfmpt1 
 |-  F/_ n ( n e. NN |-> ( ( ! ` n ) / ( ( sqrt ` ( 2 x. n ) ) x. ( ( n / _e ) ^ n ) ) ) )
11 1 10 nfcxfr 
 |-  F/_ n A
12 11 8 nffv 
 |-  F/_ n ( A ` 1 )
13 9 12 nffv 
 |-  F/_ n ( log ` ( A ` 1 ) )
14 2fveq3 
 |-  ( n = 1 -> ( log ` ( A ` n ) ) = ( log ` ( A ` 1 ) ) )
15 8 13 14 2 fvmptf 
 |-  ( ( 1 e. NN /\ ( log ` ( A ` 1 ) ) e. RR ) -> ( B ` 1 ) = ( log ` ( A ` 1 ) ) )
16 4 7 15 mp2an 
 |-  ( B ` 1 ) = ( log ` ( A ` 1 ) )
17 16 7 eqeltri 
 |-  ( B ` 1 ) e. RR
18 17 a1i 
 |-  ( N e. NN -> ( B ` 1 ) e. RR )
19 1 stirlinglem2 
 |-  ( N e. NN -> ( A ` N ) e. RR+ )
20 19 relogcld 
 |-  ( N e. NN -> ( log ` ( A ` N ) ) e. RR )
21 nfcv 
 |-  F/_ n N
22 11 21 nffv 
 |-  F/_ n ( A ` N )
23 9 22 nffv 
 |-  F/_ n ( log ` ( A ` N ) )
24 2fveq3 
 |-  ( n = N -> ( log ` ( A ` n ) ) = ( log ` ( A ` N ) ) )
25 21 23 24 2 fvmptf 
 |-  ( ( N e. NN /\ ( log ` ( A ` N ) ) e. RR ) -> ( B ` N ) = ( log ` ( A ` N ) ) )
26 20 25 mpdan 
 |-  ( N e. NN -> ( B ` N ) = ( log ` ( A ` N ) ) )
27 26 20 eqeltrd 
 |-  ( N e. NN -> ( B ` N ) e. RR )
28 4re 
 |-  4 e. RR
29 4ne0 
 |-  4 =/= 0
30 28 29 rereccli 
 |-  ( 1 / 4 ) e. RR
31 30 a1i 
 |-  ( N e. NN -> ( 1 / 4 ) e. RR )
32 fveq2 
 |-  ( k = j -> ( B ` k ) = ( B ` j ) )
33 fveq2 
 |-  ( k = ( j + 1 ) -> ( B ` k ) = ( B ` ( j + 1 ) ) )
34 fveq2 
 |-  ( k = 1 -> ( B ` k ) = ( B ` 1 ) )
35 fveq2 
 |-  ( k = N -> ( B ` k ) = ( B ` N ) )
36 elnnuz 
 |-  ( N e. NN <-> N e. ( ZZ>= ` 1 ) )
37 36 biimpi 
 |-  ( N e. NN -> N e. ( ZZ>= ` 1 ) )
38 elfznn 
 |-  ( k e. ( 1 ... N ) -> k e. NN )
39 1 stirlinglem2 
 |-  ( k e. NN -> ( A ` k ) e. RR+ )
40 38 39 syl 
 |-  ( k e. ( 1 ... N ) -> ( A ` k ) e. RR+ )
41 40 relogcld 
 |-  ( k e. ( 1 ... N ) -> ( log ` ( A ` k ) ) e. RR )
42 nfcv 
 |-  F/_ n k
43 11 42 nffv 
 |-  F/_ n ( A ` k )
44 9 43 nffv 
 |-  F/_ n ( log ` ( A ` k ) )
45 2fveq3 
 |-  ( n = k -> ( log ` ( A ` n ) ) = ( log ` ( A ` k ) ) )
46 42 44 45 2 fvmptf 
 |-  ( ( k e. NN /\ ( log ` ( A ` k ) ) e. RR ) -> ( B ` k ) = ( log ` ( A ` k ) ) )
47 38 41 46 syl2anc 
 |-  ( k e. ( 1 ... N ) -> ( B ` k ) = ( log ` ( A ` k ) ) )
48 47 adantl 
 |-  ( ( N e. NN /\ k e. ( 1 ... N ) ) -> ( B ` k ) = ( log ` ( A ` k ) ) )
49 40 rpcnd 
 |-  ( k e. ( 1 ... N ) -> ( A ` k ) e. CC )
50 49 adantl 
 |-  ( ( N e. NN /\ k e. ( 1 ... N ) ) -> ( A ` k ) e. CC )
51 39 rpne0d 
 |-  ( k e. NN -> ( A ` k ) =/= 0 )
52 38 51 syl 
 |-  ( k e. ( 1 ... N ) -> ( A ` k ) =/= 0 )
53 52 adantl 
 |-  ( ( N e. NN /\ k e. ( 1 ... N ) ) -> ( A ` k ) =/= 0 )
54 50 53 logcld 
 |-  ( ( N e. NN /\ k e. ( 1 ... N ) ) -> ( log ` ( A ` k ) ) e. CC )
55 48 54 eqeltrd 
 |-  ( ( N e. NN /\ k e. ( 1 ... N ) ) -> ( B ` k ) e. CC )
56 32 33 34 35 37 55 telfsumo 
 |-  ( N e. NN -> sum_ j e. ( 1 ..^ N ) ( ( B ` j ) - ( B ` ( j + 1 ) ) ) = ( ( B ` 1 ) - ( B ` N ) ) )
57 nnz 
 |-  ( N e. NN -> N e. ZZ )
58 fzoval 
 |-  ( N e. ZZ -> ( 1 ..^ N ) = ( 1 ... ( N - 1 ) ) )
59 57 58 syl 
 |-  ( N e. NN -> ( 1 ..^ N ) = ( 1 ... ( N - 1 ) ) )
60 59 sumeq1d 
 |-  ( N e. NN -> sum_ j e. ( 1 ..^ N ) ( ( B ` j ) - ( B ` ( j + 1 ) ) ) = sum_ j e. ( 1 ... ( N - 1 ) ) ( ( B ` j ) - ( B ` ( j + 1 ) ) ) )
61 56 60 eqtr3d 
 |-  ( N e. NN -> ( ( B ` 1 ) - ( B ` N ) ) = sum_ j e. ( 1 ... ( N - 1 ) ) ( ( B ` j ) - ( B ` ( j + 1 ) ) ) )
62 fzfid 
 |-  ( N e. NN -> ( 1 ... ( N - 1 ) ) e. Fin )
63 elfznn 
 |-  ( j e. ( 1 ... ( N - 1 ) ) -> j e. NN )
64 63 adantl 
 |-  ( ( N e. NN /\ j e. ( 1 ... ( N - 1 ) ) ) -> j e. NN )
65 1 stirlinglem2 
 |-  ( j e. NN -> ( A ` j ) e. RR+ )
66 65 relogcld 
 |-  ( j e. NN -> ( log ` ( A ` j ) ) e. RR )
67 nfcv 
 |-  F/_ n j
68 11 67 nffv 
 |-  F/_ n ( A ` j )
69 9 68 nffv 
 |-  F/_ n ( log ` ( A ` j ) )
70 2fveq3 
 |-  ( n = j -> ( log ` ( A ` n ) ) = ( log ` ( A ` j ) ) )
71 67 69 70 2 fvmptf 
 |-  ( ( j e. NN /\ ( log ` ( A ` j ) ) e. RR ) -> ( B ` j ) = ( log ` ( A ` j ) ) )
72 66 71 mpdan 
 |-  ( j e. NN -> ( B ` j ) = ( log ` ( A ` j ) ) )
73 72 66 eqeltrd 
 |-  ( j e. NN -> ( B ` j ) e. RR )
74 64 73 syl 
 |-  ( ( N e. NN /\ j e. ( 1 ... ( N - 1 ) ) ) -> ( B ` j ) e. RR )
75 peano2nn 
 |-  ( j e. NN -> ( j + 1 ) e. NN )
76 1 stirlinglem2 
 |-  ( ( j + 1 ) e. NN -> ( A ` ( j + 1 ) ) e. RR+ )
77 75 76 syl 
 |-  ( j e. NN -> ( A ` ( j + 1 ) ) e. RR+ )
78 77 relogcld 
 |-  ( j e. NN -> ( log ` ( A ` ( j + 1 ) ) ) e. RR )
79 nfcv 
 |-  F/_ n ( j + 1 )
80 11 79 nffv 
 |-  F/_ n ( A ` ( j + 1 ) )
81 9 80 nffv 
 |-  F/_ n ( log ` ( A ` ( j + 1 ) ) )
82 2fveq3 
 |-  ( n = ( j + 1 ) -> ( log ` ( A ` n ) ) = ( log ` ( A ` ( j + 1 ) ) ) )
83 79 81 82 2 fvmptf 
 |-  ( ( ( j + 1 ) e. NN /\ ( log ` ( A ` ( j + 1 ) ) ) e. RR ) -> ( B ` ( j + 1 ) ) = ( log ` ( A ` ( j + 1 ) ) ) )
84 75 78 83 syl2anc 
 |-  ( j e. NN -> ( B ` ( j + 1 ) ) = ( log ` ( A ` ( j + 1 ) ) ) )
85 84 78 eqeltrd 
 |-  ( j e. NN -> ( B ` ( j + 1 ) ) e. RR )
86 63 85 syl 
 |-  ( j e. ( 1 ... ( N - 1 ) ) -> ( B ` ( j + 1 ) ) e. RR )
87 86 adantl 
 |-  ( ( N e. NN /\ j e. ( 1 ... ( N - 1 ) ) ) -> ( B ` ( j + 1 ) ) e. RR )
88 74 87 resubcld 
 |-  ( ( N e. NN /\ j e. ( 1 ... ( N - 1 ) ) ) -> ( ( B ` j ) - ( B ` ( j + 1 ) ) ) e. RR )
89 62 88 fsumrecl 
 |-  ( N e. NN -> sum_ j e. ( 1 ... ( N - 1 ) ) ( ( B ` j ) - ( B ` ( j + 1 ) ) ) e. RR )
90 30 a1i 
 |-  ( ( N e. NN /\ j e. ( 1 ... ( N - 1 ) ) ) -> ( 1 / 4 ) e. RR )
91 63 nnred 
 |-  ( j e. ( 1 ... ( N - 1 ) ) -> j e. RR )
92 1red 
 |-  ( j e. ( 1 ... ( N - 1 ) ) -> 1 e. RR )
93 91 92 readdcld 
 |-  ( j e. ( 1 ... ( N - 1 ) ) -> ( j + 1 ) e. RR )
94 91 93 remulcld 
 |-  ( j e. ( 1 ... ( N - 1 ) ) -> ( j x. ( j + 1 ) ) e. RR )
95 91 recnd 
 |-  ( j e. ( 1 ... ( N - 1 ) ) -> j e. CC )
96 1cnd 
 |-  ( j e. ( 1 ... ( N - 1 ) ) -> 1 e. CC )
97 95 96 addcld 
 |-  ( j e. ( 1 ... ( N - 1 ) ) -> ( j + 1 ) e. CC )
98 63 nnne0d 
 |-  ( j e. ( 1 ... ( N - 1 ) ) -> j =/= 0 )
99 75 nnne0d 
 |-  ( j e. NN -> ( j + 1 ) =/= 0 )
100 63 99 syl 
 |-  ( j e. ( 1 ... ( N - 1 ) ) -> ( j + 1 ) =/= 0 )
101 95 97 98 100 mulne0d 
 |-  ( j e. ( 1 ... ( N - 1 ) ) -> ( j x. ( j + 1 ) ) =/= 0 )
102 94 101 rereccld 
 |-  ( j e. ( 1 ... ( N - 1 ) ) -> ( 1 / ( j x. ( j + 1 ) ) ) e. RR )
103 102 adantl 
 |-  ( ( N e. NN /\ j e. ( 1 ... ( N - 1 ) ) ) -> ( 1 / ( j x. ( j + 1 ) ) ) e. RR )
104 90 103 remulcld 
 |-  ( ( N e. NN /\ j e. ( 1 ... ( N - 1 ) ) ) -> ( ( 1 / 4 ) x. ( 1 / ( j x. ( j + 1 ) ) ) ) e. RR )
105 62 104 fsumrecl 
 |-  ( N e. NN -> sum_ j e. ( 1 ... ( N - 1 ) ) ( ( 1 / 4 ) x. ( 1 / ( j x. ( j + 1 ) ) ) ) e. RR )
106 eqid 
 |-  ( i e. NN |-> ( ( 1 / ( ( 2 x. i ) + 1 ) ) x. ( ( 1 / ( ( 2 x. j ) + 1 ) ) ^ ( 2 x. i ) ) ) ) = ( i e. NN |-> ( ( 1 / ( ( 2 x. i ) + 1 ) ) x. ( ( 1 / ( ( 2 x. j ) + 1 ) ) ^ ( 2 x. i ) ) ) )
107 eqid 
 |-  ( i e. NN |-> ( ( 1 / ( ( ( 2 x. j ) + 1 ) ^ 2 ) ) ^ i ) ) = ( i e. NN |-> ( ( 1 / ( ( ( 2 x. j ) + 1 ) ^ 2 ) ) ^ i ) )
108 1 2 106 107 stirlinglem10 
 |-  ( j e. NN -> ( ( B ` j ) - ( B ` ( j + 1 ) ) ) <_ ( ( 1 / 4 ) x. ( 1 / ( j x. ( j + 1 ) ) ) ) )
109 64 108 syl 
 |-  ( ( N e. NN /\ j e. ( 1 ... ( N - 1 ) ) ) -> ( ( B ` j ) - ( B ` ( j + 1 ) ) ) <_ ( ( 1 / 4 ) x. ( 1 / ( j x. ( j + 1 ) ) ) ) )
110 62 88 104 109 fsumle 
 |-  ( N e. NN -> sum_ j e. ( 1 ... ( N - 1 ) ) ( ( B ` j ) - ( B ` ( j + 1 ) ) ) <_ sum_ j e. ( 1 ... ( N - 1 ) ) ( ( 1 / 4 ) x. ( 1 / ( j x. ( j + 1 ) ) ) ) )
111 62 103 fsumrecl 
 |-  ( N e. NN -> sum_ j e. ( 1 ... ( N - 1 ) ) ( 1 / ( j x. ( j + 1 ) ) ) e. RR )
112 1red 
 |-  ( N e. NN -> 1 e. RR )
113 4pos 
 |-  0 < 4
114 28 113 elrpii 
 |-  4 e. RR+
115 114 a1i 
 |-  ( N e. NN -> 4 e. RR+ )
116 0red 
 |-  ( N e. NN -> 0 e. RR )
117 0lt1 
 |-  0 < 1
118 117 a1i 
 |-  ( N e. NN -> 0 < 1 )
119 116 112 118 ltled 
 |-  ( N e. NN -> 0 <_ 1 )
120 112 115 119 divge0d 
 |-  ( N e. NN -> 0 <_ ( 1 / 4 ) )
121 eqid 
 |-  ( ZZ>= ` N ) = ( ZZ>= ` N )
122 eluznn 
 |-  ( ( N e. NN /\ j e. ( ZZ>= ` N ) ) -> j e. NN )
123 3 a1i 
 |-  ( j e. NN -> F = ( n e. NN |-> ( 1 / ( n x. ( n + 1 ) ) ) ) )
124 simpr 
 |-  ( ( j e. NN /\ n = j ) -> n = j )
125 124 oveq1d 
 |-  ( ( j e. NN /\ n = j ) -> ( n + 1 ) = ( j + 1 ) )
126 124 125 oveq12d 
 |-  ( ( j e. NN /\ n = j ) -> ( n x. ( n + 1 ) ) = ( j x. ( j + 1 ) ) )
127 126 oveq2d 
 |-  ( ( j e. NN /\ n = j ) -> ( 1 / ( n x. ( n + 1 ) ) ) = ( 1 / ( j x. ( j + 1 ) ) ) )
128 id 
 |-  ( j e. NN -> j e. NN )
129 nnre 
 |-  ( j e. NN -> j e. RR )
130 1red 
 |-  ( j e. NN -> 1 e. RR )
131 129 130 readdcld 
 |-  ( j e. NN -> ( j + 1 ) e. RR )
132 129 131 remulcld 
 |-  ( j e. NN -> ( j x. ( j + 1 ) ) e. RR )
133 nncn 
 |-  ( j e. NN -> j e. CC )
134 1cnd 
 |-  ( j e. NN -> 1 e. CC )
135 133 134 addcld 
 |-  ( j e. NN -> ( j + 1 ) e. CC )
136 nnne0 
 |-  ( j e. NN -> j =/= 0 )
137 133 135 136 99 mulne0d 
 |-  ( j e. NN -> ( j x. ( j + 1 ) ) =/= 0 )
138 132 137 rereccld 
 |-  ( j e. NN -> ( 1 / ( j x. ( j + 1 ) ) ) e. RR )
139 123 127 128 138 fvmptd 
 |-  ( j e. NN -> ( F ` j ) = ( 1 / ( j x. ( j + 1 ) ) ) )
140 122 139 syl 
 |-  ( ( N e. NN /\ j e. ( ZZ>= ` N ) ) -> ( F ` j ) = ( 1 / ( j x. ( j + 1 ) ) ) )
141 122 nnred 
 |-  ( ( N e. NN /\ j e. ( ZZ>= ` N ) ) -> j e. RR )
142 1red 
 |-  ( ( N e. NN /\ j e. ( ZZ>= ` N ) ) -> 1 e. RR )
143 141 142 readdcld 
 |-  ( ( N e. NN /\ j e. ( ZZ>= ` N ) ) -> ( j + 1 ) e. RR )
144 141 143 remulcld 
 |-  ( ( N e. NN /\ j e. ( ZZ>= ` N ) ) -> ( j x. ( j + 1 ) ) e. RR )
145 141 recnd 
 |-  ( ( N e. NN /\ j e. ( ZZ>= ` N ) ) -> j e. CC )
146 1cnd 
 |-  ( ( N e. NN /\ j e. ( ZZ>= ` N ) ) -> 1 e. CC )
147 145 146 addcld 
 |-  ( ( N e. NN /\ j e. ( ZZ>= ` N ) ) -> ( j + 1 ) e. CC )
148 122 nnne0d 
 |-  ( ( N e. NN /\ j e. ( ZZ>= ` N ) ) -> j =/= 0 )
149 122 99 syl 
 |-  ( ( N e. NN /\ j e. ( ZZ>= ` N ) ) -> ( j + 1 ) =/= 0 )
150 145 147 148 149 mulne0d 
 |-  ( ( N e. NN /\ j e. ( ZZ>= ` N ) ) -> ( j x. ( j + 1 ) ) =/= 0 )
151 144 150 rereccld 
 |-  ( ( N e. NN /\ j e. ( ZZ>= ` N ) ) -> ( 1 / ( j x. ( j + 1 ) ) ) e. RR )
152 seqeq1 
 |-  ( N = 1 -> seq N ( + , F ) = seq 1 ( + , F ) )
153 3 trireciplem 
 |-  seq 1 ( + , F ) ~~> 1
154 climrel 
 |-  Rel ~~>
155 154 releldmi 
 |-  ( seq 1 ( + , F ) ~~> 1 -> seq 1 ( + , F ) e. dom ~~> )
156 153 155 mp1i 
 |-  ( N = 1 -> seq 1 ( + , F ) e. dom ~~> )
157 152 156 eqeltrd 
 |-  ( N = 1 -> seq N ( + , F ) e. dom ~~> )
158 157 adantl 
 |-  ( ( N e. NN /\ N = 1 ) -> seq N ( + , F ) e. dom ~~> )
159 simpl 
 |-  ( ( N e. NN /\ -. N = 1 ) -> N e. NN )
160 simpr 
 |-  ( ( N e. NN /\ -. N = 1 ) -> -. N = 1 )
161 elnn1uz2 
 |-  ( N e. NN <-> ( N = 1 \/ N e. ( ZZ>= ` 2 ) ) )
162 159 161 sylib 
 |-  ( ( N e. NN /\ -. N = 1 ) -> ( N = 1 \/ N e. ( ZZ>= ` 2 ) ) )
163 162 ord 
 |-  ( ( N e. NN /\ -. N = 1 ) -> ( -. N = 1 -> N e. ( ZZ>= ` 2 ) ) )
164 160 163 mpd 
 |-  ( ( N e. NN /\ -. N = 1 ) -> N e. ( ZZ>= ` 2 ) )
165 uz2m1nn 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( N - 1 ) e. NN )
166 164 165 syl 
 |-  ( ( N e. NN /\ -. N = 1 ) -> ( N - 1 ) e. NN )
167 nncn 
 |-  ( N e. NN -> N e. CC )
168 167 adantr 
 |-  ( ( N e. NN /\ ( N - 1 ) e. NN ) -> N e. CC )
169 1cnd 
 |-  ( ( N e. NN /\ ( N - 1 ) e. NN ) -> 1 e. CC )
170 168 169 npcand 
 |-  ( ( N e. NN /\ ( N - 1 ) e. NN ) -> ( ( N - 1 ) + 1 ) = N )
171 170 eqcomd 
 |-  ( ( N e. NN /\ ( N - 1 ) e. NN ) -> N = ( ( N - 1 ) + 1 ) )
172 171 seqeq1d 
 |-  ( ( N e. NN /\ ( N - 1 ) e. NN ) -> seq N ( + , F ) = seq ( ( N - 1 ) + 1 ) ( + , F ) )
173 nnuz 
 |-  NN = ( ZZ>= ` 1 )
174 id 
 |-  ( ( N - 1 ) e. NN -> ( N - 1 ) e. NN )
175 138 recnd 
 |-  ( j e. NN -> ( 1 / ( j x. ( j + 1 ) ) ) e. CC )
176 139 175 eqeltrd 
 |-  ( j e. NN -> ( F ` j ) e. CC )
177 176 adantl 
 |-  ( ( ( N - 1 ) e. NN /\ j e. NN ) -> ( F ` j ) e. CC )
178 153 a1i 
 |-  ( ( N - 1 ) e. NN -> seq 1 ( + , F ) ~~> 1 )
179 173 174 177 178 clim2ser 
 |-  ( ( N - 1 ) e. NN -> seq ( ( N - 1 ) + 1 ) ( + , F ) ~~> ( 1 - ( seq 1 ( + , F ) ` ( N - 1 ) ) ) )
180 179 adantl 
 |-  ( ( N e. NN /\ ( N - 1 ) e. NN ) -> seq ( ( N - 1 ) + 1 ) ( + , F ) ~~> ( 1 - ( seq 1 ( + , F ) ` ( N - 1 ) ) ) )
181 172 180 eqbrtrd 
 |-  ( ( N e. NN /\ ( N - 1 ) e. NN ) -> seq N ( + , F ) ~~> ( 1 - ( seq 1 ( + , F ) ` ( N - 1 ) ) ) )
182 154 releldmi 
 |-  ( seq N ( + , F ) ~~> ( 1 - ( seq 1 ( + , F ) ` ( N - 1 ) ) ) -> seq N ( + , F ) e. dom ~~> )
183 181 182 syl 
 |-  ( ( N e. NN /\ ( N - 1 ) e. NN ) -> seq N ( + , F ) e. dom ~~> )
184 159 166 183 syl2anc 
 |-  ( ( N e. NN /\ -. N = 1 ) -> seq N ( + , F ) e. dom ~~> )
185 158 184 pm2.61dan 
 |-  ( N e. NN -> seq N ( + , F ) e. dom ~~> )
186 121 57 140 151 185 isumrecl 
 |-  ( N e. NN -> sum_ j e. ( ZZ>= ` N ) ( 1 / ( j x. ( j + 1 ) ) ) e. RR )
187 122 nnrpd 
 |-  ( ( N e. NN /\ j e. ( ZZ>= ` N ) ) -> j e. RR+ )
188 187 rpge0d 
 |-  ( ( N e. NN /\ j e. ( ZZ>= ` N ) ) -> 0 <_ j )
189 141 188 ge0p1rpd 
 |-  ( ( N e. NN /\ j e. ( ZZ>= ` N ) ) -> ( j + 1 ) e. RR+ )
190 187 189 rpmulcld 
 |-  ( ( N e. NN /\ j e. ( ZZ>= ` N ) ) -> ( j x. ( j + 1 ) ) e. RR+ )
191 119 adantr 
 |-  ( ( N e. NN /\ j e. ( ZZ>= ` N ) ) -> 0 <_ 1 )
192 142 190 191 divge0d 
 |-  ( ( N e. NN /\ j e. ( ZZ>= ` N ) ) -> 0 <_ ( 1 / ( j x. ( j + 1 ) ) ) )
193 121 57 140 151 185 192 isumge0 
 |-  ( N e. NN -> 0 <_ sum_ j e. ( ZZ>= ` N ) ( 1 / ( j x. ( j + 1 ) ) ) )
194 116 186 111 193 leadd2dd 
 |-  ( N e. NN -> ( sum_ j e. ( 1 ... ( N - 1 ) ) ( 1 / ( j x. ( j + 1 ) ) ) + 0 ) <_ ( sum_ j e. ( 1 ... ( N - 1 ) ) ( 1 / ( j x. ( j + 1 ) ) ) + sum_ j e. ( ZZ>= ` N ) ( 1 / ( j x. ( j + 1 ) ) ) ) )
195 111 recnd 
 |-  ( N e. NN -> sum_ j e. ( 1 ... ( N - 1 ) ) ( 1 / ( j x. ( j + 1 ) ) ) e. CC )
196 195 addid1d 
 |-  ( N e. NN -> ( sum_ j e. ( 1 ... ( N - 1 ) ) ( 1 / ( j x. ( j + 1 ) ) ) + 0 ) = sum_ j e. ( 1 ... ( N - 1 ) ) ( 1 / ( j x. ( j + 1 ) ) ) )
197 196 eqcomd 
 |-  ( N e. NN -> sum_ j e. ( 1 ... ( N - 1 ) ) ( 1 / ( j x. ( j + 1 ) ) ) = ( sum_ j e. ( 1 ... ( N - 1 ) ) ( 1 / ( j x. ( j + 1 ) ) ) + 0 ) )
198 id 
 |-  ( N e. NN -> N e. NN )
199 139 adantl 
 |-  ( ( N e. NN /\ j e. NN ) -> ( F ` j ) = ( 1 / ( j x. ( j + 1 ) ) ) )
200 133 adantl 
 |-  ( ( N e. NN /\ j e. NN ) -> j e. CC )
201 1cnd 
 |-  ( ( N e. NN /\ j e. NN ) -> 1 e. CC )
202 200 201 addcld 
 |-  ( ( N e. NN /\ j e. NN ) -> ( j + 1 ) e. CC )
203 200 202 mulcld 
 |-  ( ( N e. NN /\ j e. NN ) -> ( j x. ( j + 1 ) ) e. CC )
204 136 adantl 
 |-  ( ( N e. NN /\ j e. NN ) -> j =/= 0 )
205 99 adantl 
 |-  ( ( N e. NN /\ j e. NN ) -> ( j + 1 ) =/= 0 )
206 200 202 204 205 mulne0d 
 |-  ( ( N e. NN /\ j e. NN ) -> ( j x. ( j + 1 ) ) =/= 0 )
207 203 206 reccld 
 |-  ( ( N e. NN /\ j e. NN ) -> ( 1 / ( j x. ( j + 1 ) ) ) e. CC )
208 153 155 mp1i 
 |-  ( N e. NN -> seq 1 ( + , F ) e. dom ~~> )
209 173 121 198 199 207 208 isumsplit 
 |-  ( N e. NN -> sum_ j e. NN ( 1 / ( j x. ( j + 1 ) ) ) = ( sum_ j e. ( 1 ... ( N - 1 ) ) ( 1 / ( j x. ( j + 1 ) ) ) + sum_ j e. ( ZZ>= ` N ) ( 1 / ( j x. ( j + 1 ) ) ) ) )
210 194 197 209 3brtr4d 
 |-  ( N e. NN -> sum_ j e. ( 1 ... ( N - 1 ) ) ( 1 / ( j x. ( j + 1 ) ) ) <_ sum_ j e. NN ( 1 / ( j x. ( j + 1 ) ) ) )
211 1zzd 
 |-  ( T. -> 1 e. ZZ )
212 139 adantl 
 |-  ( ( T. /\ j e. NN ) -> ( F ` j ) = ( 1 / ( j x. ( j + 1 ) ) ) )
213 175 adantl 
 |-  ( ( T. /\ j e. NN ) -> ( 1 / ( j x. ( j + 1 ) ) ) e. CC )
214 153 a1i 
 |-  ( T. -> seq 1 ( + , F ) ~~> 1 )
215 173 211 212 213 214 isumclim 
 |-  ( T. -> sum_ j e. NN ( 1 / ( j x. ( j + 1 ) ) ) = 1 )
216 215 mptru 
 |-  sum_ j e. NN ( 1 / ( j x. ( j + 1 ) ) ) = 1
217 210 216 breqtrdi 
 |-  ( N e. NN -> sum_ j e. ( 1 ... ( N - 1 ) ) ( 1 / ( j x. ( j + 1 ) ) ) <_ 1 )
218 111 112 31 120 217 lemul2ad 
 |-  ( N e. NN -> ( ( 1 / 4 ) x. sum_ j e. ( 1 ... ( N - 1 ) ) ( 1 / ( j x. ( j + 1 ) ) ) ) <_ ( ( 1 / 4 ) x. 1 ) )
219 4cn 
 |-  4 e. CC
220 219 a1i 
 |-  ( N e. NN -> 4 e. CC )
221 113 a1i 
 |-  ( N e. NN -> 0 < 4 )
222 221 gt0ne0d 
 |-  ( N e. NN -> 4 =/= 0 )
223 220 222 reccld 
 |-  ( N e. NN -> ( 1 / 4 ) e. CC )
224 103 recnd 
 |-  ( ( N e. NN /\ j e. ( 1 ... ( N - 1 ) ) ) -> ( 1 / ( j x. ( j + 1 ) ) ) e. CC )
225 62 223 224 fsummulc2 
 |-  ( N e. NN -> ( ( 1 / 4 ) x. sum_ j e. ( 1 ... ( N - 1 ) ) ( 1 / ( j x. ( j + 1 ) ) ) ) = sum_ j e. ( 1 ... ( N - 1 ) ) ( ( 1 / 4 ) x. ( 1 / ( j x. ( j + 1 ) ) ) ) )
226 223 mulid1d 
 |-  ( N e. NN -> ( ( 1 / 4 ) x. 1 ) = ( 1 / 4 ) )
227 218 225 226 3brtr3d 
 |-  ( N e. NN -> sum_ j e. ( 1 ... ( N - 1 ) ) ( ( 1 / 4 ) x. ( 1 / ( j x. ( j + 1 ) ) ) ) <_ ( 1 / 4 ) )
228 89 105 31 110 227 letrd 
 |-  ( N e. NN -> sum_ j e. ( 1 ... ( N - 1 ) ) ( ( B ` j ) - ( B ` ( j + 1 ) ) ) <_ ( 1 / 4 ) )
229 61 228 eqbrtrd 
 |-  ( N e. NN -> ( ( B ` 1 ) - ( B ` N ) ) <_ ( 1 / 4 ) )
230 18 27 31 229 subled 
 |-  ( N e. NN -> ( ( B ` 1 ) - ( 1 / 4 ) ) <_ ( B ` N ) )