This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem stirlinglem10

Description: A bound for any B(N)-B(N + 1) that will allow to find a lower bound for the whole B sequence. (Contributed by Glauco Siliprandi, 29-Jun-2017)

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

Proof

Step Hyp Ref Expression
1 stirlinglem10.1 
 |-  A = ( n e. NN |-> ( ( ! ` n ) / ( ( sqrt ` ( 2 x. n ) ) x. ( ( n / _e ) ^ n ) ) ) )
2 stirlinglem10.2 
 |-  B = ( n e. NN |-> ( log ` ( A ` n ) ) )
3 stirlinglem10.4 
 |-  K = ( k e. NN |-> ( ( 1 / ( ( 2 x. k ) + 1 ) ) x. ( ( 1 / ( ( 2 x. N ) + 1 ) ) ^ ( 2 x. k ) ) ) )
4 stirlinglem10.5 
 |-  L = ( k e. NN |-> ( ( 1 / ( ( ( 2 x. N ) + 1 ) ^ 2 ) ) ^ k ) )
5 nnuz 
 |-  NN = ( ZZ>= ` 1 )
6 1zzd 
 |-  ( N e. NN -> 1 e. ZZ )
7 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 ) )
8 1 2 7 3 stirlinglem9 
 |-  ( N e. NN -> seq 1 ( + , K ) ~~> ( ( B ` N ) - ( B ` ( N + 1 ) ) ) )
9 2cnd 
 |-  ( N e. NN -> 2 e. CC )
10 nncn 
 |-  ( N e. NN -> N e. CC )
11 9 10 mulcld 
 |-  ( N e. NN -> ( 2 x. N ) e. CC )
12 1cnd 
 |-  ( N e. NN -> 1 e. CC )
13 11 12 addcld 
 |-  ( N e. NN -> ( ( 2 x. N ) + 1 ) e. CC )
14 13 sqcld 
 |-  ( N e. NN -> ( ( ( 2 x. N ) + 1 ) ^ 2 ) e. CC )
15 0red 
 |-  ( N e. NN -> 0 e. RR )
16 1red 
 |-  ( N e. NN -> 1 e. RR )
17 2re 
 |-  2 e. RR
18 17 a1i 
 |-  ( N e. NN -> 2 e. RR )
19 nnre 
 |-  ( N e. NN -> N e. RR )
20 18 19 remulcld 
 |-  ( N e. NN -> ( 2 x. N ) e. RR )
21 20 16 readdcld 
 |-  ( N e. NN -> ( ( 2 x. N ) + 1 ) e. RR )
22 0lt1 
 |-  0 < 1
23 22 a1i 
 |-  ( N e. NN -> 0 < 1 )
24 2rp 
 |-  2 e. RR+
25 24 a1i 
 |-  ( N e. NN -> 2 e. RR+ )
26 nnrp 
 |-  ( N e. NN -> N e. RR+ )
27 25 26 rpmulcld 
 |-  ( N e. NN -> ( 2 x. N ) e. RR+ )
28 16 27 ltaddrp2d 
 |-  ( N e. NN -> 1 < ( ( 2 x. N ) + 1 ) )
29 15 16 21 23 28 lttrd 
 |-  ( N e. NN -> 0 < ( ( 2 x. N ) + 1 ) )
30 29 gt0ne0d 
 |-  ( N e. NN -> ( ( 2 x. N ) + 1 ) =/= 0 )
31 2z 
 |-  2 e. ZZ
32 31 a1i 
 |-  ( N e. NN -> 2 e. ZZ )
33 13 30 32 expne0d 
 |-  ( N e. NN -> ( ( ( 2 x. N ) + 1 ) ^ 2 ) =/= 0 )
34 14 33 reccld 
 |-  ( N e. NN -> ( 1 / ( ( ( 2 x. N ) + 1 ) ^ 2 ) ) e. CC )
35 16 renegcld 
 |-  ( N e. NN -> -u 1 e. RR )
36 21 resqcld 
 |-  ( N e. NN -> ( ( ( 2 x. N ) + 1 ) ^ 2 ) e. RR )
37 36 33 rereccld 
 |-  ( N e. NN -> ( 1 / ( ( ( 2 x. N ) + 1 ) ^ 2 ) ) e. RR )
38 1re 
 |-  1 e. RR
39 lt0neg2 
 |-  ( 1 e. RR -> ( 0 < 1 <-> -u 1 < 0 ) )
40 38 39 ax-mp 
 |-  ( 0 < 1 <-> -u 1 < 0 )
41 23 40 sylib 
 |-  ( N e. NN -> -u 1 < 0 )
42 21 30 sqgt0d 
 |-  ( N e. NN -> 0 < ( ( ( 2 x. N ) + 1 ) ^ 2 ) )
43 36 42 recgt0d 
 |-  ( N e. NN -> 0 < ( 1 / ( ( ( 2 x. N ) + 1 ) ^ 2 ) ) )
44 35 15 37 41 43 lttrd 
 |-  ( N e. NN -> -u 1 < ( 1 / ( ( ( 2 x. N ) + 1 ) ^ 2 ) ) )
45 2nn 
 |-  2 e. NN
46 45 a1i 
 |-  ( N e. NN -> 2 e. NN )
47 expgt1 
 |-  ( ( ( ( 2 x. N ) + 1 ) e. RR /\ 2 e. NN /\ 1 < ( ( 2 x. N ) + 1 ) ) -> 1 < ( ( ( 2 x. N ) + 1 ) ^ 2 ) )
48 21 46 28 47 syl3anc 
 |-  ( N e. NN -> 1 < ( ( ( 2 x. N ) + 1 ) ^ 2 ) )
49 36 42 elrpd 
 |-  ( N e. NN -> ( ( ( 2 x. N ) + 1 ) ^ 2 ) e. RR+ )
50 49 recgt1d 
 |-  ( N e. NN -> ( 1 < ( ( ( 2 x. N ) + 1 ) ^ 2 ) <-> ( 1 / ( ( ( 2 x. N ) + 1 ) ^ 2 ) ) < 1 ) )
51 48 50 mpbid 
 |-  ( N e. NN -> ( 1 / ( ( ( 2 x. N ) + 1 ) ^ 2 ) ) < 1 )
52 37 16 absltd 
 |-  ( N e. NN -> ( ( abs ` ( 1 / ( ( ( 2 x. N ) + 1 ) ^ 2 ) ) ) < 1 <-> ( -u 1 < ( 1 / ( ( ( 2 x. N ) + 1 ) ^ 2 ) ) /\ ( 1 / ( ( ( 2 x. N ) + 1 ) ^ 2 ) ) < 1 ) ) )
53 44 51 52 mpbir2and 
 |-  ( N e. NN -> ( abs ` ( 1 / ( ( ( 2 x. N ) + 1 ) ^ 2 ) ) ) < 1 )
54 1nn0 
 |-  1 e. NN0
55 54 a1i 
 |-  ( N e. NN -> 1 e. NN0 )
56 4 a1i 
 |-  ( ( N e. NN /\ j e. ( ZZ>= ` 1 ) ) -> L = ( k e. NN |-> ( ( 1 / ( ( ( 2 x. N ) + 1 ) ^ 2 ) ) ^ k ) ) )
57 simpr 
 |-  ( ( ( N e. NN /\ j e. ( ZZ>= ` 1 ) ) /\ k = j ) -> k = j )
58 57 oveq2d 
 |-  ( ( ( N e. NN /\ j e. ( ZZ>= ` 1 ) ) /\ k = j ) -> ( ( 1 / ( ( ( 2 x. N ) + 1 ) ^ 2 ) ) ^ k ) = ( ( 1 / ( ( ( 2 x. N ) + 1 ) ^ 2 ) ) ^ j ) )
59 elnnuz 
 |-  ( j e. NN <-> j e. ( ZZ>= ` 1 ) )
60 59 biimpri 
 |-  ( j e. ( ZZ>= ` 1 ) -> j e. NN )
61 60 adantl 
 |-  ( ( N e. NN /\ j e. ( ZZ>= ` 1 ) ) -> j e. NN )
62 34 adantr 
 |-  ( ( N e. NN /\ j e. ( ZZ>= ` 1 ) ) -> ( 1 / ( ( ( 2 x. N ) + 1 ) ^ 2 ) ) e. CC )
63 61 nnnn0d 
 |-  ( ( N e. NN /\ j e. ( ZZ>= ` 1 ) ) -> j e. NN0 )
64 62 63 expcld 
 |-  ( ( N e. NN /\ j e. ( ZZ>= ` 1 ) ) -> ( ( 1 / ( ( ( 2 x. N ) + 1 ) ^ 2 ) ) ^ j ) e. CC )
65 56 58 61 64 fvmptd 
 |-  ( ( N e. NN /\ j e. ( ZZ>= ` 1 ) ) -> ( L ` j ) = ( ( 1 / ( ( ( 2 x. N ) + 1 ) ^ 2 ) ) ^ j ) )
66 34 53 55 65 geolim2 
 |-  ( N e. NN -> seq 1 ( + , L ) ~~> ( ( ( 1 / ( ( ( 2 x. N ) + 1 ) ^ 2 ) ) ^ 1 ) / ( 1 - ( 1 / ( ( ( 2 x. N ) + 1 ) ^ 2 ) ) ) ) )
67 34 exp1d 
 |-  ( N e. NN -> ( ( 1 / ( ( ( 2 x. N ) + 1 ) ^ 2 ) ) ^ 1 ) = ( 1 / ( ( ( 2 x. N ) + 1 ) ^ 2 ) ) )
68 14 33 dividd 
 |-  ( N e. NN -> ( ( ( ( 2 x. N ) + 1 ) ^ 2 ) / ( ( ( 2 x. N ) + 1 ) ^ 2 ) ) = 1 )
69 68 eqcomd 
 |-  ( N e. NN -> 1 = ( ( ( ( 2 x. N ) + 1 ) ^ 2 ) / ( ( ( 2 x. N ) + 1 ) ^ 2 ) ) )
70 69 oveq1d 
 |-  ( N e. NN -> ( 1 - ( 1 / ( ( ( 2 x. N ) + 1 ) ^ 2 ) ) ) = ( ( ( ( ( 2 x. N ) + 1 ) ^ 2 ) / ( ( ( 2 x. N ) + 1 ) ^ 2 ) ) - ( 1 / ( ( ( 2 x. N ) + 1 ) ^ 2 ) ) ) )
71 49 rpcnne0d 
 |-  ( N e. NN -> ( ( ( ( 2 x. N ) + 1 ) ^ 2 ) e. CC /\ ( ( ( 2 x. N ) + 1 ) ^ 2 ) =/= 0 ) )
72 divsubdir 
 |-  ( ( ( ( ( 2 x. N ) + 1 ) ^ 2 ) e. CC /\ 1 e. CC /\ ( ( ( ( 2 x. N ) + 1 ) ^ 2 ) e. CC /\ ( ( ( 2 x. N ) + 1 ) ^ 2 ) =/= 0 ) ) -> ( ( ( ( ( 2 x. N ) + 1 ) ^ 2 ) - 1 ) / ( ( ( 2 x. N ) + 1 ) ^ 2 ) ) = ( ( ( ( ( 2 x. N ) + 1 ) ^ 2 ) / ( ( ( 2 x. N ) + 1 ) ^ 2 ) ) - ( 1 / ( ( ( 2 x. N ) + 1 ) ^ 2 ) ) ) )
73 14 12 71 72 syl3anc 
 |-  ( N e. NN -> ( ( ( ( ( 2 x. N ) + 1 ) ^ 2 ) - 1 ) / ( ( ( 2 x. N ) + 1 ) ^ 2 ) ) = ( ( ( ( ( 2 x. N ) + 1 ) ^ 2 ) / ( ( ( 2 x. N ) + 1 ) ^ 2 ) ) - ( 1 / ( ( ( 2 x. N ) + 1 ) ^ 2 ) ) ) )
74 ax-1cn 
 |-  1 e. CC
75 binom2 
 |-  ( ( ( 2 x. N ) e. CC /\ 1 e. CC ) -> ( ( ( 2 x. N ) + 1 ) ^ 2 ) = ( ( ( ( 2 x. N ) ^ 2 ) + ( 2 x. ( ( 2 x. N ) x. 1 ) ) ) + ( 1 ^ 2 ) ) )
76 11 74 75 sylancl 
 |-  ( N e. NN -> ( ( ( 2 x. N ) + 1 ) ^ 2 ) = ( ( ( ( 2 x. N ) ^ 2 ) + ( 2 x. ( ( 2 x. N ) x. 1 ) ) ) + ( 1 ^ 2 ) ) )
77 76 oveq1d 
 |-  ( N e. NN -> ( ( ( ( 2 x. N ) + 1 ) ^ 2 ) - 1 ) = ( ( ( ( ( 2 x. N ) ^ 2 ) + ( 2 x. ( ( 2 x. N ) x. 1 ) ) ) + ( 1 ^ 2 ) ) - 1 ) )
78 9 10 sqmuld 
 |-  ( N e. NN -> ( ( 2 x. N ) ^ 2 ) = ( ( 2 ^ 2 ) x. ( N ^ 2 ) ) )
79 sq2 
 |-  ( 2 ^ 2 ) = 4
80 79 a1i 
 |-  ( N e. NN -> ( 2 ^ 2 ) = 4 )
81 80 oveq1d 
 |-  ( N e. NN -> ( ( 2 ^ 2 ) x. ( N ^ 2 ) ) = ( 4 x. ( N ^ 2 ) ) )
82 78 81 eqtrd 
 |-  ( N e. NN -> ( ( 2 x. N ) ^ 2 ) = ( 4 x. ( N ^ 2 ) ) )
83 11 mulridd 
 |-  ( N e. NN -> ( ( 2 x. N ) x. 1 ) = ( 2 x. N ) )
84 83 oveq2d 
 |-  ( N e. NN -> ( 2 x. ( ( 2 x. N ) x. 1 ) ) = ( 2 x. ( 2 x. N ) ) )
85 9 9 10 mulassd 
 |-  ( N e. NN -> ( ( 2 x. 2 ) x. N ) = ( 2 x. ( 2 x. N ) ) )
86 2t2e4 
 |-  ( 2 x. 2 ) = 4
87 86 a1i 
 |-  ( N e. NN -> ( 2 x. 2 ) = 4 )
88 87 oveq1d 
 |-  ( N e. NN -> ( ( 2 x. 2 ) x. N ) = ( 4 x. N ) )
89 84 85 88 3eqtr2d 
 |-  ( N e. NN -> ( 2 x. ( ( 2 x. N ) x. 1 ) ) = ( 4 x. N ) )
90 82 89 oveq12d 
 |-  ( N e. NN -> ( ( ( 2 x. N ) ^ 2 ) + ( 2 x. ( ( 2 x. N ) x. 1 ) ) ) = ( ( 4 x. ( N ^ 2 ) ) + ( 4 x. N ) ) )
91 4cn 
 |-  4 e. CC
92 91 a1i 
 |-  ( N e. NN -> 4 e. CC )
93 10 sqcld 
 |-  ( N e. NN -> ( N ^ 2 ) e. CC )
94 92 93 10 adddid 
 |-  ( N e. NN -> ( 4 x. ( ( N ^ 2 ) + N ) ) = ( ( 4 x. ( N ^ 2 ) ) + ( 4 x. N ) ) )
95 10 sqvald 
 |-  ( N e. NN -> ( N ^ 2 ) = ( N x. N ) )
96 10 mulridd 
 |-  ( N e. NN -> ( N x. 1 ) = N )
97 96 eqcomd 
 |-  ( N e. NN -> N = ( N x. 1 ) )
98 95 97 oveq12d 
 |-  ( N e. NN -> ( ( N ^ 2 ) + N ) = ( ( N x. N ) + ( N x. 1 ) ) )
99 10 10 12 adddid 
 |-  ( N e. NN -> ( N x. ( N + 1 ) ) = ( ( N x. N ) + ( N x. 1 ) ) )
100 98 99 eqtr4d 
 |-  ( N e. NN -> ( ( N ^ 2 ) + N ) = ( N x. ( N + 1 ) ) )
101 100 oveq2d 
 |-  ( N e. NN -> ( 4 x. ( ( N ^ 2 ) + N ) ) = ( 4 x. ( N x. ( N + 1 ) ) ) )
102 90 94 101 3eqtr2d 
 |-  ( N e. NN -> ( ( ( 2 x. N ) ^ 2 ) + ( 2 x. ( ( 2 x. N ) x. 1 ) ) ) = ( 4 x. ( N x. ( N + 1 ) ) ) )
103 sq1 
 |-  ( 1 ^ 2 ) = 1
104 103 a1i 
 |-  ( N e. NN -> ( 1 ^ 2 ) = 1 )
105 102 104 oveq12d 
 |-  ( N e. NN -> ( ( ( ( 2 x. N ) ^ 2 ) + ( 2 x. ( ( 2 x. N ) x. 1 ) ) ) + ( 1 ^ 2 ) ) = ( ( 4 x. ( N x. ( N + 1 ) ) ) + 1 ) )
106 105 oveq1d 
 |-  ( N e. NN -> ( ( ( ( ( 2 x. N ) ^ 2 ) + ( 2 x. ( ( 2 x. N ) x. 1 ) ) ) + ( 1 ^ 2 ) ) - 1 ) = ( ( ( 4 x. ( N x. ( N + 1 ) ) ) + 1 ) - 1 ) )
107 10 12 addcld 
 |-  ( N e. NN -> ( N + 1 ) e. CC )
108 10 107 mulcld 
 |-  ( N e. NN -> ( N x. ( N + 1 ) ) e. CC )
109 92 108 mulcld 
 |-  ( N e. NN -> ( 4 x. ( N x. ( N + 1 ) ) ) e. CC )
110 109 12 pncand 
 |-  ( N e. NN -> ( ( ( 4 x. ( N x. ( N + 1 ) ) ) + 1 ) - 1 ) = ( 4 x. ( N x. ( N + 1 ) ) ) )
111 77 106 110 3eqtrd 
 |-  ( N e. NN -> ( ( ( ( 2 x. N ) + 1 ) ^ 2 ) - 1 ) = ( 4 x. ( N x. ( N + 1 ) ) ) )
112 111 oveq1d 
 |-  ( N e. NN -> ( ( ( ( ( 2 x. N ) + 1 ) ^ 2 ) - 1 ) / ( ( ( 2 x. N ) + 1 ) ^ 2 ) ) = ( ( 4 x. ( N x. ( N + 1 ) ) ) / ( ( ( 2 x. N ) + 1 ) ^ 2 ) ) )
113 70 73 112 3eqtr2d 
 |-  ( N e. NN -> ( 1 - ( 1 / ( ( ( 2 x. N ) + 1 ) ^ 2 ) ) ) = ( ( 4 x. ( N x. ( N + 1 ) ) ) / ( ( ( 2 x. N ) + 1 ) ^ 2 ) ) )
114 67 113 oveq12d 
 |-  ( N e. NN -> ( ( ( 1 / ( ( ( 2 x. N ) + 1 ) ^ 2 ) ) ^ 1 ) / ( 1 - ( 1 / ( ( ( 2 x. N ) + 1 ) ^ 2 ) ) ) ) = ( ( 1 / ( ( ( 2 x. N ) + 1 ) ^ 2 ) ) / ( ( 4 x. ( N x. ( N + 1 ) ) ) / ( ( ( 2 x. N ) + 1 ) ^ 2 ) ) ) )
115 4pos 
 |-  0 < 4
116 115 a1i 
 |-  ( N e. NN -> 0 < 4 )
117 116 gt0ne0d 
 |-  ( N e. NN -> 4 =/= 0 )
118 nnne0 
 |-  ( N e. NN -> N =/= 0 )
119 19 16 readdcld 
 |-  ( N e. NN -> ( N + 1 ) e. RR )
120 nngt0 
 |-  ( N e. NN -> 0 < N )
121 19 ltp1d 
 |-  ( N e. NN -> N < ( N + 1 ) )
122 15 19 119 120 121 lttrd 
 |-  ( N e. NN -> 0 < ( N + 1 ) )
123 122 gt0ne0d 
 |-  ( N e. NN -> ( N + 1 ) =/= 0 )
124 10 107 118 123 mulne0d 
 |-  ( N e. NN -> ( N x. ( N + 1 ) ) =/= 0 )
125 92 108 117 124 mulne0d 
 |-  ( N e. NN -> ( 4 x. ( N x. ( N + 1 ) ) ) =/= 0 )
126 12 14 109 14 33 33 125 divdivdivd 
 |-  ( N e. NN -> ( ( 1 / ( ( ( 2 x. N ) + 1 ) ^ 2 ) ) / ( ( 4 x. ( N x. ( N + 1 ) ) ) / ( ( ( 2 x. N ) + 1 ) ^ 2 ) ) ) = ( ( 1 x. ( ( ( 2 x. N ) + 1 ) ^ 2 ) ) / ( ( ( ( 2 x. N ) + 1 ) ^ 2 ) x. ( 4 x. ( N x. ( N + 1 ) ) ) ) ) )
127 12 14 mulcomd 
 |-  ( N e. NN -> ( 1 x. ( ( ( 2 x. N ) + 1 ) ^ 2 ) ) = ( ( ( ( 2 x. N ) + 1 ) ^ 2 ) x. 1 ) )
128 127 oveq1d 
 |-  ( N e. NN -> ( ( 1 x. ( ( ( 2 x. N ) + 1 ) ^ 2 ) ) / ( ( ( ( 2 x. N ) + 1 ) ^ 2 ) x. ( 4 x. ( N x. ( N + 1 ) ) ) ) ) = ( ( ( ( ( 2 x. N ) + 1 ) ^ 2 ) x. 1 ) / ( ( ( ( 2 x. N ) + 1 ) ^ 2 ) x. ( 4 x. ( N x. ( N + 1 ) ) ) ) ) )
129 12 mulridd 
 |-  ( N e. NN -> ( 1 x. 1 ) = 1 )
130 129 eqcomd 
 |-  ( N e. NN -> 1 = ( 1 x. 1 ) )
131 130 oveq1d 
 |-  ( N e. NN -> ( 1 / ( 4 x. ( N x. ( N + 1 ) ) ) ) = ( ( 1 x. 1 ) / ( 4 x. ( N x. ( N + 1 ) ) ) ) )
132 12 92 12 108 117 124 divmuldivd 
 |-  ( N e. NN -> ( ( 1 / 4 ) x. ( 1 / ( N x. ( N + 1 ) ) ) ) = ( ( 1 x. 1 ) / ( 4 x. ( N x. ( N + 1 ) ) ) ) )
133 131 132 eqtr4d 
 |-  ( N e. NN -> ( 1 / ( 4 x. ( N x. ( N + 1 ) ) ) ) = ( ( 1 / 4 ) x. ( 1 / ( N x. ( N + 1 ) ) ) ) )
134 68 133 oveq12d 
 |-  ( N e. NN -> ( ( ( ( ( 2 x. N ) + 1 ) ^ 2 ) / ( ( ( 2 x. N ) + 1 ) ^ 2 ) ) x. ( 1 / ( 4 x. ( N x. ( N + 1 ) ) ) ) ) = ( 1 x. ( ( 1 / 4 ) x. ( 1 / ( N x. ( N + 1 ) ) ) ) ) )
135 14 14 12 109 33 125 divmuldivd 
 |-  ( N e. NN -> ( ( ( ( ( 2 x. N ) + 1 ) ^ 2 ) / ( ( ( 2 x. N ) + 1 ) ^ 2 ) ) x. ( 1 / ( 4 x. ( N x. ( N + 1 ) ) ) ) ) = ( ( ( ( ( 2 x. N ) + 1 ) ^ 2 ) x. 1 ) / ( ( ( ( 2 x. N ) + 1 ) ^ 2 ) x. ( 4 x. ( N x. ( N + 1 ) ) ) ) ) )
136 92 117 reccld 
 |-  ( N e. NN -> ( 1 / 4 ) e. CC )
137 108 124 reccld 
 |-  ( N e. NN -> ( 1 / ( N x. ( N + 1 ) ) ) e. CC )
138 136 137 mulcld 
 |-  ( N e. NN -> ( ( 1 / 4 ) x. ( 1 / ( N x. ( N + 1 ) ) ) ) e. CC )
139 138 mullidd 
 |-  ( N e. NN -> ( 1 x. ( ( 1 / 4 ) x. ( 1 / ( N x. ( N + 1 ) ) ) ) ) = ( ( 1 / 4 ) x. ( 1 / ( N x. ( N + 1 ) ) ) ) )
140 134 135 139 3eqtr3d 
 |-  ( N e. NN -> ( ( ( ( ( 2 x. N ) + 1 ) ^ 2 ) x. 1 ) / ( ( ( ( 2 x. N ) + 1 ) ^ 2 ) x. ( 4 x. ( N x. ( N + 1 ) ) ) ) ) = ( ( 1 / 4 ) x. ( 1 / ( N x. ( N + 1 ) ) ) ) )
141 126 128 140 3eqtrd 
 |-  ( N e. NN -> ( ( 1 / ( ( ( 2 x. N ) + 1 ) ^ 2 ) ) / ( ( 4 x. ( N x. ( N + 1 ) ) ) / ( ( ( 2 x. N ) + 1 ) ^ 2 ) ) ) = ( ( 1 / 4 ) x. ( 1 / ( N x. ( N + 1 ) ) ) ) )
142 114 141 eqtrd 
 |-  ( N e. NN -> ( ( ( 1 / ( ( ( 2 x. N ) + 1 ) ^ 2 ) ) ^ 1 ) / ( 1 - ( 1 / ( ( ( 2 x. N ) + 1 ) ^ 2 ) ) ) ) = ( ( 1 / 4 ) x. ( 1 / ( N x. ( N + 1 ) ) ) ) )
143 66 142 breqtrd 
 |-  ( N e. NN -> seq 1 ( + , L ) ~~> ( ( 1 / 4 ) x. ( 1 / ( N x. ( N + 1 ) ) ) ) )
144 59 biimpi 
 |-  ( j e. NN -> j e. ( ZZ>= ` 1 ) )
145 144 adantl 
 |-  ( ( N e. NN /\ j e. NN ) -> j e. ( ZZ>= ` 1 ) )
146 oveq2 
 |-  ( k = n -> ( 2 x. k ) = ( 2 x. n ) )
147 146 oveq1d 
 |-  ( k = n -> ( ( 2 x. k ) + 1 ) = ( ( 2 x. n ) + 1 ) )
148 147 oveq2d 
 |-  ( k = n -> ( 1 / ( ( 2 x. k ) + 1 ) ) = ( 1 / ( ( 2 x. n ) + 1 ) ) )
149 146 oveq2d 
 |-  ( k = n -> ( ( 1 / ( ( 2 x. N ) + 1 ) ) ^ ( 2 x. k ) ) = ( ( 1 / ( ( 2 x. N ) + 1 ) ) ^ ( 2 x. n ) ) )
150 148 149 oveq12d 
 |-  ( k = n -> ( ( 1 / ( ( 2 x. k ) + 1 ) ) x. ( ( 1 / ( ( 2 x. N ) + 1 ) ) ^ ( 2 x. k ) ) ) = ( ( 1 / ( ( 2 x. n ) + 1 ) ) x. ( ( 1 / ( ( 2 x. N ) + 1 ) ) ^ ( 2 x. n ) ) ) )
151 elfznn 
 |-  ( n e. ( 1 ... j ) -> n e. NN )
152 151 adantl 
 |-  ( ( N e. NN /\ n e. ( 1 ... j ) ) -> n e. NN )
153 2cnd 
 |-  ( ( N e. NN /\ n e. ( 1 ... j ) ) -> 2 e. CC )
154 152 nncnd 
 |-  ( ( N e. NN /\ n e. ( 1 ... j ) ) -> n e. CC )
155 153 154 mulcld 
 |-  ( ( N e. NN /\ n e. ( 1 ... j ) ) -> ( 2 x. n ) e. CC )
156 1cnd 
 |-  ( ( N e. NN /\ n e. ( 1 ... j ) ) -> 1 e. CC )
157 155 156 addcld 
 |-  ( ( N e. NN /\ n e. ( 1 ... j ) ) -> ( ( 2 x. n ) + 1 ) e. CC )
158 0red 
 |-  ( n e. NN -> 0 e. RR )
159 1red 
 |-  ( n e. NN -> 1 e. RR )
160 17 a1i 
 |-  ( n e. NN -> 2 e. RR )
161 nnre 
 |-  ( n e. NN -> n e. RR )
162 160 161 remulcld 
 |-  ( n e. NN -> ( 2 x. n ) e. RR )
163 162 159 readdcld 
 |-  ( n e. NN -> ( ( 2 x. n ) + 1 ) e. RR )
164 22 a1i 
 |-  ( n e. NN -> 0 < 1 )
165 24 a1i 
 |-  ( n e. NN -> 2 e. RR+ )
166 nnrp 
 |-  ( n e. NN -> n e. RR+ )
167 165 166 rpmulcld 
 |-  ( n e. NN -> ( 2 x. n ) e. RR+ )
168 159 167 ltaddrp2d 
 |-  ( n e. NN -> 1 < ( ( 2 x. n ) + 1 ) )
169 158 159 163 164 168 lttrd 
 |-  ( n e. NN -> 0 < ( ( 2 x. n ) + 1 ) )
170 151 169 syl 
 |-  ( n e. ( 1 ... j ) -> 0 < ( ( 2 x. n ) + 1 ) )
171 170 gt0ne0d 
 |-  ( n e. ( 1 ... j ) -> ( ( 2 x. n ) + 1 ) =/= 0 )
172 171 adantl 
 |-  ( ( N e. NN /\ n e. ( 1 ... j ) ) -> ( ( 2 x. n ) + 1 ) =/= 0 )
173 157 172 reccld 
 |-  ( ( N e. NN /\ n e. ( 1 ... j ) ) -> ( 1 / ( ( 2 x. n ) + 1 ) ) e. CC )
174 10 adantr 
 |-  ( ( N e. NN /\ n e. ( 1 ... j ) ) -> N e. CC )
175 153 174 mulcld 
 |-  ( ( N e. NN /\ n e. ( 1 ... j ) ) -> ( 2 x. N ) e. CC )
176 175 156 addcld 
 |-  ( ( N e. NN /\ n e. ( 1 ... j ) ) -> ( ( 2 x. N ) + 1 ) e. CC )
177 30 adantr 
 |-  ( ( N e. NN /\ n e. ( 1 ... j ) ) -> ( ( 2 x. N ) + 1 ) =/= 0 )
178 176 177 reccld 
 |-  ( ( N e. NN /\ n e. ( 1 ... j ) ) -> ( 1 / ( ( 2 x. N ) + 1 ) ) e. CC )
179 2nn0 
 |-  2 e. NN0
180 179 a1i 
 |-  ( ( N e. NN /\ n e. ( 1 ... j ) ) -> 2 e. NN0 )
181 152 nnnn0d 
 |-  ( ( N e. NN /\ n e. ( 1 ... j ) ) -> n e. NN0 )
182 180 181 nn0mulcld 
 |-  ( ( N e. NN /\ n e. ( 1 ... j ) ) -> ( 2 x. n ) e. NN0 )
183 178 182 expcld 
 |-  ( ( N e. NN /\ n e. ( 1 ... j ) ) -> ( ( 1 / ( ( 2 x. N ) + 1 ) ) ^ ( 2 x. n ) ) e. CC )
184 173 183 mulcld 
 |-  ( ( N e. NN /\ n e. ( 1 ... j ) ) -> ( ( 1 / ( ( 2 x. n ) + 1 ) ) x. ( ( 1 / ( ( 2 x. N ) + 1 ) ) ^ ( 2 x. n ) ) ) e. CC )
185 3 150 152 184 fvmptd3 
 |-  ( ( N e. NN /\ n e. ( 1 ... j ) ) -> ( K ` n ) = ( ( 1 / ( ( 2 x. n ) + 1 ) ) x. ( ( 1 / ( ( 2 x. N ) + 1 ) ) ^ ( 2 x. n ) ) ) )
186 185 adantlr 
 |-  ( ( ( N e. NN /\ j e. NN ) /\ n e. ( 1 ... j ) ) -> ( K ` n ) = ( ( 1 / ( ( 2 x. n ) + 1 ) ) x. ( ( 1 / ( ( 2 x. N ) + 1 ) ) ^ ( 2 x. n ) ) ) )
187 169 gt0ne0d 
 |-  ( n e. NN -> ( ( 2 x. n ) + 1 ) =/= 0 )
188 163 187 rereccld 
 |-  ( n e. NN -> ( 1 / ( ( 2 x. n ) + 1 ) ) e. RR )
189 151 188 syl 
 |-  ( n e. ( 1 ... j ) -> ( 1 / ( ( 2 x. n ) + 1 ) ) e. RR )
190 189 adantl 
 |-  ( ( ( N e. NN /\ j e. NN ) /\ n e. ( 1 ... j ) ) -> ( 1 / ( ( 2 x. n ) + 1 ) ) e. RR )
191 21 30 rereccld 
 |-  ( N e. NN -> ( 1 / ( ( 2 x. N ) + 1 ) ) e. RR )
192 191 adantr 
 |-  ( ( N e. NN /\ n e. ( 1 ... j ) ) -> ( 1 / ( ( 2 x. N ) + 1 ) ) e. RR )
193 192 182 reexpcld 
 |-  ( ( N e. NN /\ n e. ( 1 ... j ) ) -> ( ( 1 / ( ( 2 x. N ) + 1 ) ) ^ ( 2 x. n ) ) e. RR )
194 193 adantlr 
 |-  ( ( ( N e. NN /\ j e. NN ) /\ n e. ( 1 ... j ) ) -> ( ( 1 / ( ( 2 x. N ) + 1 ) ) ^ ( 2 x. n ) ) e. RR )
195 190 194 remulcld 
 |-  ( ( ( N e. NN /\ j e. NN ) /\ n e. ( 1 ... j ) ) -> ( ( 1 / ( ( 2 x. n ) + 1 ) ) x. ( ( 1 / ( ( 2 x. N ) + 1 ) ) ^ ( 2 x. n ) ) ) e. RR )
196 186 195 eqeltrd 
 |-  ( ( ( N e. NN /\ j e. NN ) /\ n e. ( 1 ... j ) ) -> ( K ` n ) e. RR )
197 readdcl 
 |-  ( ( n e. RR /\ i e. RR ) -> ( n + i ) e. RR )
198 197 adantl 
 |-  ( ( ( N e. NN /\ j e. NN ) /\ ( n e. RR /\ i e. RR ) ) -> ( n + i ) e. RR )
199 145 196 198 seqcl 
 |-  ( ( N e. NN /\ j e. NN ) -> ( seq 1 ( + , K ) ` j ) e. RR )
200 oveq2 
 |-  ( k = n -> ( ( 1 / ( ( ( 2 x. N ) + 1 ) ^ 2 ) ) ^ k ) = ( ( 1 / ( ( ( 2 x. N ) + 1 ) ^ 2 ) ) ^ n ) )
201 34 adantr 
 |-  ( ( N e. NN /\ n e. ( 1 ... j ) ) -> ( 1 / ( ( ( 2 x. N ) + 1 ) ^ 2 ) ) e. CC )
202 201 181 expcld 
 |-  ( ( N e. NN /\ n e. ( 1 ... j ) ) -> ( ( 1 / ( ( ( 2 x. N ) + 1 ) ^ 2 ) ) ^ n ) e. CC )
203 4 200 152 202 fvmptd3 
 |-  ( ( N e. NN /\ n e. ( 1 ... j ) ) -> ( L ` n ) = ( ( 1 / ( ( ( 2 x. N ) + 1 ) ^ 2 ) ) ^ n ) )
204 37 adantr 
 |-  ( ( N e. NN /\ n e. ( 1 ... j ) ) -> ( 1 / ( ( ( 2 x. N ) + 1 ) ^ 2 ) ) e. RR )
205 204 181 reexpcld 
 |-  ( ( N e. NN /\ n e. ( 1 ... j ) ) -> ( ( 1 / ( ( ( 2 x. N ) + 1 ) ^ 2 ) ) ^ n ) e. RR )
206 203 205 eqeltrd 
 |-  ( ( N e. NN /\ n e. ( 1 ... j ) ) -> ( L ` n ) e. RR )
207 206 adantlr 
 |-  ( ( ( N e. NN /\ j e. NN ) /\ n e. ( 1 ... j ) ) -> ( L ` n ) e. RR )
208 145 207 198 seqcl 
 |-  ( ( N e. NN /\ j e. NN ) -> ( seq 1 ( + , L ) ` j ) e. RR )
209 31 a1i 
 |-  ( n e. ( 1 ... j ) -> 2 e. ZZ )
210 elfzelz 
 |-  ( n e. ( 1 ... j ) -> n e. ZZ )
211 209 210 zmulcld 
 |-  ( n e. ( 1 ... j ) -> ( 2 x. n ) e. ZZ )
212 1exp 
 |-  ( ( 2 x. n ) e. ZZ -> ( 1 ^ ( 2 x. n ) ) = 1 )
213 211 212 syl 
 |-  ( n e. ( 1 ... j ) -> ( 1 ^ ( 2 x. n ) ) = 1 )
214 1exp 
 |-  ( n e. ZZ -> ( 1 ^ n ) = 1 )
215 210 214 syl 
 |-  ( n e. ( 1 ... j ) -> ( 1 ^ n ) = 1 )
216 213 215 eqtr4d 
 |-  ( n e. ( 1 ... j ) -> ( 1 ^ ( 2 x. n ) ) = ( 1 ^ n ) )
217 216 adantl 
 |-  ( ( N e. NN /\ n e. ( 1 ... j ) ) -> ( 1 ^ ( 2 x. n ) ) = ( 1 ^ n ) )
218 176 181 180 expmuld 
 |-  ( ( N e. NN /\ n e. ( 1 ... j ) ) -> ( ( ( 2 x. N ) + 1 ) ^ ( 2 x. n ) ) = ( ( ( ( 2 x. N ) + 1 ) ^ 2 ) ^ n ) )
219 217 218 oveq12d 
 |-  ( ( N e. NN /\ n e. ( 1 ... j ) ) -> ( ( 1 ^ ( 2 x. n ) ) / ( ( ( 2 x. N ) + 1 ) ^ ( 2 x. n ) ) ) = ( ( 1 ^ n ) / ( ( ( ( 2 x. N ) + 1 ) ^ 2 ) ^ n ) ) )
220 156 176 177 182 expdivd 
 |-  ( ( N e. NN /\ n e. ( 1 ... j ) ) -> ( ( 1 / ( ( 2 x. N ) + 1 ) ) ^ ( 2 x. n ) ) = ( ( 1 ^ ( 2 x. n ) ) / ( ( ( 2 x. N ) + 1 ) ^ ( 2 x. n ) ) ) )
221 176 sqcld 
 |-  ( ( N e. NN /\ n e. ( 1 ... j ) ) -> ( ( ( 2 x. N ) + 1 ) ^ 2 ) e. CC )
222 31 a1i 
 |-  ( ( N e. NN /\ n e. ( 1 ... j ) ) -> 2 e. ZZ )
223 176 177 222 expne0d 
 |-  ( ( N e. NN /\ n e. ( 1 ... j ) ) -> ( ( ( 2 x. N ) + 1 ) ^ 2 ) =/= 0 )
224 156 221 223 181 expdivd 
 |-  ( ( N e. NN /\ n e. ( 1 ... j ) ) -> ( ( 1 / ( ( ( 2 x. N ) + 1 ) ^ 2 ) ) ^ n ) = ( ( 1 ^ n ) / ( ( ( ( 2 x. N ) + 1 ) ^ 2 ) ^ n ) ) )
225 219 220 224 3eqtr4d 
 |-  ( ( N e. NN /\ n e. ( 1 ... j ) ) -> ( ( 1 / ( ( 2 x. N ) + 1 ) ) ^ ( 2 x. n ) ) = ( ( 1 / ( ( ( 2 x. N ) + 1 ) ^ 2 ) ) ^ n ) )
226 225 oveq2d 
 |-  ( ( N e. NN /\ n e. ( 1 ... j ) ) -> ( ( 1 / ( ( 2 x. n ) + 1 ) ) x. ( ( 1 / ( ( 2 x. N ) + 1 ) ) ^ ( 2 x. n ) ) ) = ( ( 1 / ( ( 2 x. n ) + 1 ) ) x. ( ( 1 / ( ( ( 2 x. N ) + 1 ) ^ 2 ) ) ^ n ) ) )
227 1rp 
 |-  1 e. RR+
228 227 a1i 
 |-  ( ( N e. NN /\ n e. ( 1 ... j ) ) -> 1 e. RR+ )
229 17 a1i 
 |-  ( ( N e. NN /\ n e. ( 1 ... j ) ) -> 2 e. RR )
230 152 nnred 
 |-  ( ( N e. NN /\ n e. ( 1 ... j ) ) -> n e. RR )
231 229 230 remulcld 
 |-  ( ( N e. NN /\ n e. ( 1 ... j ) ) -> ( 2 x. n ) e. RR )
232 180 nn0ge0d 
 |-  ( ( N e. NN /\ n e. ( 1 ... j ) ) -> 0 <_ 2 )
233 181 nn0ge0d 
 |-  ( ( N e. NN /\ n e. ( 1 ... j ) ) -> 0 <_ n )
234 229 230 232 233 mulge0d 
 |-  ( ( N e. NN /\ n e. ( 1 ... j ) ) -> 0 <_ ( 2 x. n ) )
235 231 234 ge0p1rpd 
 |-  ( ( N e. NN /\ n e. ( 1 ... j ) ) -> ( ( 2 x. n ) + 1 ) e. RR+ )
236 1red 
 |-  ( ( N e. NN /\ n e. ( 1 ... j ) ) -> 1 e. RR )
237 228 rpge0d 
 |-  ( ( N e. NN /\ n e. ( 1 ... j ) ) -> 0 <_ 1 )
238 159 163 168 ltled 
 |-  ( n e. NN -> 1 <_ ( ( 2 x. n ) + 1 ) )
239 151 238 syl 
 |-  ( n e. ( 1 ... j ) -> 1 <_ ( ( 2 x. n ) + 1 ) )
240 239 adantl 
 |-  ( ( N e. NN /\ n e. ( 1 ... j ) ) -> 1 <_ ( ( 2 x. n ) + 1 ) )
241 228 235 236 237 240 lediv2ad 
 |-  ( ( N e. NN /\ n e. ( 1 ... j ) ) -> ( 1 / ( ( 2 x. n ) + 1 ) ) <_ ( 1 / 1 ) )
242 156 div1d 
 |-  ( ( N e. NN /\ n e. ( 1 ... j ) ) -> ( 1 / 1 ) = 1 )
243 241 242 breqtrd 
 |-  ( ( N e. NN /\ n e. ( 1 ... j ) ) -> ( 1 / ( ( 2 x. n ) + 1 ) ) <_ 1 )
244 152 188 syl 
 |-  ( ( N e. NN /\ n e. ( 1 ... j ) ) -> ( 1 / ( ( 2 x. n ) + 1 ) ) e. RR )
245 19 adantr 
 |-  ( ( N e. NN /\ n e. ( 1 ... j ) ) -> N e. RR )
246 229 245 remulcld 
 |-  ( ( N e. NN /\ n e. ( 1 ... j ) ) -> ( 2 x. N ) e. RR )
247 15 19 120 ltled 
 |-  ( N e. NN -> 0 <_ N )
248 247 adantr 
 |-  ( ( N e. NN /\ n e. ( 1 ... j ) ) -> 0 <_ N )
249 229 245 232 248 mulge0d 
 |-  ( ( N e. NN /\ n e. ( 1 ... j ) ) -> 0 <_ ( 2 x. N ) )
250 246 249 ge0p1rpd 
 |-  ( ( N e. NN /\ n e. ( 1 ... j ) ) -> ( ( 2 x. N ) + 1 ) e. RR+ )
251 250 222 rpexpcld 
 |-  ( ( N e. NN /\ n e. ( 1 ... j ) ) -> ( ( ( 2 x. N ) + 1 ) ^ 2 ) e. RR+ )
252 251 rpreccld 
 |-  ( ( N e. NN /\ n e. ( 1 ... j ) ) -> ( 1 / ( ( ( 2 x. N ) + 1 ) ^ 2 ) ) e. RR+ )
253 210 adantl 
 |-  ( ( N e. NN /\ n e. ( 1 ... j ) ) -> n e. ZZ )
254 252 253 rpexpcld 
 |-  ( ( N e. NN /\ n e. ( 1 ... j ) ) -> ( ( 1 / ( ( ( 2 x. N ) + 1 ) ^ 2 ) ) ^ n ) e. RR+ )
255 244 236 254 lemul1d 
 |-  ( ( N e. NN /\ n e. ( 1 ... j ) ) -> ( ( 1 / ( ( 2 x. n ) + 1 ) ) <_ 1 <-> ( ( 1 / ( ( 2 x. n ) + 1 ) ) x. ( ( 1 / ( ( ( 2 x. N ) + 1 ) ^ 2 ) ) ^ n ) ) <_ ( 1 x. ( ( 1 / ( ( ( 2 x. N ) + 1 ) ^ 2 ) ) ^ n ) ) ) )
256 243 255 mpbid 
 |-  ( ( N e. NN /\ n e. ( 1 ... j ) ) -> ( ( 1 / ( ( 2 x. n ) + 1 ) ) x. ( ( 1 / ( ( ( 2 x. N ) + 1 ) ^ 2 ) ) ^ n ) ) <_ ( 1 x. ( ( 1 / ( ( ( 2 x. N ) + 1 ) ^ 2 ) ) ^ n ) ) )
257 202 mullidd 
 |-  ( ( N e. NN /\ n e. ( 1 ... j ) ) -> ( 1 x. ( ( 1 / ( ( ( 2 x. N ) + 1 ) ^ 2 ) ) ^ n ) ) = ( ( 1 / ( ( ( 2 x. N ) + 1 ) ^ 2 ) ) ^ n ) )
258 256 257 breqtrd 
 |-  ( ( N e. NN /\ n e. ( 1 ... j ) ) -> ( ( 1 / ( ( 2 x. n ) + 1 ) ) x. ( ( 1 / ( ( ( 2 x. N ) + 1 ) ^ 2 ) ) ^ n ) ) <_ ( ( 1 / ( ( ( 2 x. N ) + 1 ) ^ 2 ) ) ^ n ) )
259 226 258 eqbrtrd 
 |-  ( ( N e. NN /\ n e. ( 1 ... j ) ) -> ( ( 1 / ( ( 2 x. n ) + 1 ) ) x. ( ( 1 / ( ( 2 x. N ) + 1 ) ) ^ ( 2 x. n ) ) ) <_ ( ( 1 / ( ( ( 2 x. N ) + 1 ) ^ 2 ) ) ^ n ) )
260 259 185 203 3brtr4d 
 |-  ( ( N e. NN /\ n e. ( 1 ... j ) ) -> ( K ` n ) <_ ( L ` n ) )
261 260 adantlr 
 |-  ( ( ( N e. NN /\ j e. NN ) /\ n e. ( 1 ... j ) ) -> ( K ` n ) <_ ( L ` n ) )
262 145 196 207 261 serle 
 |-  ( ( N e. NN /\ j e. NN ) -> ( seq 1 ( + , K ) ` j ) <_ ( seq 1 ( + , L ) ` j ) )
263 5 6 8 143 199 208 262 climle 
 |-  ( N e. NN -> ( ( B ` N ) - ( B ` ( N + 1 ) ) ) <_ ( ( 1 / 4 ) x. ( 1 / ( N x. ( N + 1 ) ) ) ) )