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