Metamath Proof Explorer

Theorem stirlinglem13

Description: B is decreasing and has a lower bound, then it converges. Since B is log A , in another theorem it is proven that A converges as well. (Contributed by Glauco Siliprandi, 29-Jun-2017)

Ref Expression
Hypotheses stirlinglem13.1 
|- A = ( n e. NN |-> ( ( ! ` n ) / ( ( sqrt ` ( 2 x. n ) ) x. ( ( n / _e ) ^ n ) ) ) )
stirlinglem13.2 
|- B = ( n e. NN |-> ( log ` ( A ` n ) ) )
Assertion stirlinglem13 
|- E. d e. RR B ~~> d

Proof

Step Hyp Ref Expression
1 stirlinglem13.1 
 |-  A = ( n e. NN |-> ( ( ! ` n ) / ( ( sqrt ` ( 2 x. n ) ) x. ( ( n / _e ) ^ n ) ) ) )
2 stirlinglem13.2 
 |-  B = ( n e. NN |-> ( log ` ( A ` n ) ) )
3 vex 
 |-  y e. _V
4 2 elrnmpt 
 |-  ( y e. _V -> ( y e. ran B <-> E. n e. NN y = ( log ` ( A ` n ) ) ) )
5 3 4 ax-mp 
 |-  ( y e. ran B <-> E. n e. NN y = ( log ` ( A ` n ) ) )
6 simpr 
 |-  ( ( n e. NN /\ y = ( log ` ( A ` n ) ) ) -> y = ( log ` ( A ` n ) ) )
7 1 stirlinglem2 
 |-  ( n e. NN -> ( A ` n ) e. RR+ )
8 7 relogcld 
 |-  ( n e. NN -> ( log ` ( A ` n ) ) e. RR )
9 8 adantr 
 |-  ( ( n e. NN /\ y = ( log ` ( A ` n ) ) ) -> ( log ` ( A ` n ) ) e. RR )
10 6 9 eqeltrd 
 |-  ( ( n e. NN /\ y = ( log ` ( A ` n ) ) ) -> y e. RR )
11 10 rexlimiva 
 |-  ( E. n e. NN y = ( log ` ( A ` n ) ) -> y e. RR )
12 5 11 sylbi 
 |-  ( y e. ran B -> y e. RR )
13 12 ssriv 
 |-  ran B C_ RR
14 1nn 
 |-  1 e. NN
15 1 stirlinglem2 
 |-  ( 1 e. NN -> ( A ` 1 ) e. RR+ )
16 relogcl 
 |-  ( ( A ` 1 ) e. RR+ -> ( log ` ( A ` 1 ) ) e. RR )
17 14 15 16 mp2b 
 |-  ( log ` ( A ` 1 ) ) e. RR
18 nfcv 
 |-  F/_ n 1
19 nfcv 
 |-  F/_ n log
20 nfmpt1 
 |-  F/_ n ( n e. NN |-> ( ( ! ` n ) / ( ( sqrt ` ( 2 x. n ) ) x. ( ( n / _e ) ^ n ) ) ) )
21 1 20 nfcxfr 
 |-  F/_ n A
22 21 18 nffv 
 |-  F/_ n ( A ` 1 )
23 19 22 nffv 
 |-  F/_ n ( log ` ( A ` 1 ) )
24 2fveq3 
 |-  ( n = 1 -> ( log ` ( A ` n ) ) = ( log ` ( A ` 1 ) ) )
25 18 23 24 2 fvmptf 
 |-  ( ( 1 e. NN /\ ( log ` ( A ` 1 ) ) e. RR ) -> ( B ` 1 ) = ( log ` ( A ` 1 ) ) )
26 14 17 25 mp2an 
 |-  ( B ` 1 ) = ( log ` ( A ` 1 ) )
27 2fveq3 
 |-  ( j = 1 -> ( log ` ( A ` j ) ) = ( log ` ( A ` 1 ) ) )
28 27 rspceeqv 
 |-  ( ( 1 e. NN /\ ( B ` 1 ) = ( log ` ( A ` 1 ) ) ) -> E. j e. NN ( B ` 1 ) = ( log ` ( A ` j ) ) )
29 14 26 28 mp2an 
 |-  E. j e. NN ( B ` 1 ) = ( log ` ( A ` j ) )
30 26 17 eqeltri 
 |-  ( B ` 1 ) e. RR
31 nfcv 
 |-  F/_ j ( log ` ( A ` n ) )
32 nfcv 
 |-  F/_ n j
33 21 32 nffv 
 |-  F/_ n ( A ` j )
34 19 33 nffv 
 |-  F/_ n ( log ` ( A ` j ) )
35 2fveq3 
 |-  ( n = j -> ( log ` ( A ` n ) ) = ( log ` ( A ` j ) ) )
36 31 34 35 cbvmpt 
 |-  ( n e. NN |-> ( log ` ( A ` n ) ) ) = ( j e. NN |-> ( log ` ( A ` j ) ) )
37 2 36 eqtri 
 |-  B = ( j e. NN |-> ( log ` ( A ` j ) ) )
38 37 elrnmpt 
 |-  ( ( B ` 1 ) e. RR -> ( ( B ` 1 ) e. ran B <-> E. j e. NN ( B ` 1 ) = ( log ` ( A ` j ) ) ) )
39 30 38 ax-mp 
 |-  ( ( B ` 1 ) e. ran B <-> E. j e. NN ( B ` 1 ) = ( log ` ( A ` j ) ) )
40 29 39 mpbir 
 |-  ( B ` 1 ) e. ran B
41 40 ne0ii 
 |-  ran B =/= (/)
42 4re 
 |-  4 e. RR
43 4ne0 
 |-  4 =/= 0
44 42 43 rereccli 
 |-  ( 1 / 4 ) e. RR
45 30 44 resubcli 
 |-  ( ( B ` 1 ) - ( 1 / 4 ) ) e. RR
46 eqid 
 |-  ( n e. NN |-> ( 1 / ( n x. ( n + 1 ) ) ) ) = ( n e. NN |-> ( 1 / ( n x. ( n + 1 ) ) ) )
47 1 2 46 stirlinglem12 
 |-  ( j e. NN -> ( ( B ` 1 ) - ( 1 / 4 ) ) <_ ( B ` j ) )
48 47 rgen 
 |-  A. j e. NN ( ( B ` 1 ) - ( 1 / 4 ) ) <_ ( B ` j )
49 breq1 
 |-  ( x = ( ( B ` 1 ) - ( 1 / 4 ) ) -> ( x <_ ( B ` j ) <-> ( ( B ` 1 ) - ( 1 / 4 ) ) <_ ( B ` j ) ) )
50 49 ralbidv 
 |-  ( x = ( ( B ` 1 ) - ( 1 / 4 ) ) -> ( A. j e. NN x <_ ( B ` j ) <-> A. j e. NN ( ( B ` 1 ) - ( 1 / 4 ) ) <_ ( B ` j ) ) )
51 50 rspcev 
 |-  ( ( ( ( B ` 1 ) - ( 1 / 4 ) ) e. RR /\ A. j e. NN ( ( B ` 1 ) - ( 1 / 4 ) ) <_ ( B ` j ) ) -> E. x e. RR A. j e. NN x <_ ( B ` j ) )
52 45 48 51 mp2an 
 |-  E. x e. RR A. j e. NN x <_ ( B ` j )
53 8 rgen 
 |-  A. n e. NN ( log ` ( A ` n ) ) e. RR
54 2 fnmpt 
 |-  ( A. n e. NN ( log ` ( A ` n ) ) e. RR -> B Fn NN )
55 fvelrnb 
 |-  ( B Fn NN -> ( y e. ran B <-> E. j e. NN ( B ` j ) = y ) )
56 53 54 55 mp2b 
 |-  ( y e. ran B <-> E. j e. NN ( B ` j ) = y )
57 56 bilani 
 |-  ( ( A. j e. NN x <_ ( B ` j ) /\ y e. ran B ) -> E. j e. NN ( B ` j ) = y )
58 nfra1 
 |-  F/ j A. j e. NN x <_ ( B ` j )
59 nfv 
 |-  F/ j y e. ran B
60 58 59 nfan 
 |-  F/ j ( A. j e. NN x <_ ( B ` j ) /\ y e. ran B )
61 nfv 
 |-  F/ j x <_ y
62 simp1l 
 |-  ( ( ( A. j e. NN x <_ ( B ` j ) /\ y e. ran B ) /\ j e. NN /\ ( B ` j ) = y ) -> A. j e. NN x <_ ( B ` j ) )
63 simp2 
 |-  ( ( ( A. j e. NN x <_ ( B ` j ) /\ y e. ran B ) /\ j e. NN /\ ( B ` j ) = y ) -> j e. NN )
64 rsp 
 |-  ( A. j e. NN x <_ ( B ` j ) -> ( j e. NN -> x <_ ( B ` j ) ) )
65 62 63 64 sylc 
 |-  ( ( ( A. j e. NN x <_ ( B ` j ) /\ y e. ran B ) /\ j e. NN /\ ( B ` j ) = y ) -> x <_ ( B ` j ) )
66 simp3 
 |-  ( ( ( A. j e. NN x <_ ( B ` j ) /\ y e. ran B ) /\ j e. NN /\ ( B ` j ) = y ) -> ( B ` j ) = y )
67 65 66 breqtrd 
 |-  ( ( ( A. j e. NN x <_ ( B ` j ) /\ y e. ran B ) /\ j e. NN /\ ( B ` j ) = y ) -> x <_ y )
68 67 3exp 
 |-  ( ( A. j e. NN x <_ ( B ` j ) /\ y e. ran B ) -> ( j e. NN -> ( ( B ` j ) = y -> x <_ y ) ) )
69 60 61 68 rexlimd 
 |-  ( ( A. j e. NN x <_ ( B ` j ) /\ y e. ran B ) -> ( E. j e. NN ( B ` j ) = y -> x <_ y ) )
70 57 69 mpd 
 |-  ( ( A. j e. NN x <_ ( B ` j ) /\ y e. ran B ) -> x <_ y )
71 70 ralrimiva 
 |-  ( A. j e. NN x <_ ( B ` j ) -> A. y e. ran B x <_ y )
72 71 reximi 
 |-  ( E. x e. RR A. j e. NN x <_ ( B ` j ) -> E. x e. RR A. y e. ran B x <_ y )
73 52 72 ax-mp 
 |-  E. x e. RR A. y e. ran B x <_ y
74 infrecl 
 |-  ( ( ran B C_ RR /\ ran B =/= (/) /\ E. x e. RR A. y e. ran B x <_ y ) -> inf ( ran B , RR , < ) e. RR )
75 13 41 73 74 mp3an 
 |-  inf ( ran B , RR , < ) e. RR
76 nnuz 
 |-  NN = ( ZZ>= ` 1 )
77 1zzd 
 |-  ( T. -> 1 e. ZZ )
78 2 8 fmpti 
 |-  B : NN --> RR
79 78 a1i 
 |-  ( T. -> B : NN --> RR )
80 peano2nn 
 |-  ( j e. NN -> ( j + 1 ) e. NN )
81 1 a1i 
 |-  ( j e. NN -> A = ( n e. NN |-> ( ( ! ` n ) / ( ( sqrt ` ( 2 x. n ) ) x. ( ( n / _e ) ^ n ) ) ) ) )
82 simpr 
 |-  ( ( j e. NN /\ n = ( j + 1 ) ) -> n = ( j + 1 ) )
83 82 fveq2d 
 |-  ( ( j e. NN /\ n = ( j + 1 ) ) -> ( ! ` n ) = ( ! ` ( j + 1 ) ) )
84 82 oveq2d 
 |-  ( ( j e. NN /\ n = ( j + 1 ) ) -> ( 2 x. n ) = ( 2 x. ( j + 1 ) ) )
85 84 fveq2d 
 |-  ( ( j e. NN /\ n = ( j + 1 ) ) -> ( sqrt ` ( 2 x. n ) ) = ( sqrt ` ( 2 x. ( j + 1 ) ) ) )
86 82 oveq1d 
 |-  ( ( j e. NN /\ n = ( j + 1 ) ) -> ( n / _e ) = ( ( j + 1 ) / _e ) )
87 86 82 oveq12d 
 |-  ( ( j e. NN /\ n = ( j + 1 ) ) -> ( ( n / _e ) ^ n ) = ( ( ( j + 1 ) / _e ) ^ ( j + 1 ) ) )
88 85 87 oveq12d 
 |-  ( ( j e. NN /\ n = ( j + 1 ) ) -> ( ( sqrt ` ( 2 x. n ) ) x. ( ( n / _e ) ^ n ) ) = ( ( sqrt ` ( 2 x. ( j + 1 ) ) ) x. ( ( ( j + 1 ) / _e ) ^ ( j + 1 ) ) ) )
89 83 88 oveq12d 
 |-  ( ( j e. NN /\ n = ( j + 1 ) ) -> ( ( ! ` n ) / ( ( sqrt ` ( 2 x. n ) ) x. ( ( n / _e ) ^ n ) ) ) = ( ( ! ` ( j + 1 ) ) / ( ( sqrt ` ( 2 x. ( j + 1 ) ) ) x. ( ( ( j + 1 ) / _e ) ^ ( j + 1 ) ) ) ) )
90 80 nnnn0d 
 |-  ( j e. NN -> ( j + 1 ) e. NN0 )
91 faccl 
 |-  ( ( j + 1 ) e. NN0 -> ( ! ` ( j + 1 ) ) e. NN )
92 nncn 
 |-  ( ( ! ` ( j + 1 ) ) e. NN -> ( ! ` ( j + 1 ) ) e. CC )
93 90 91 92 3syl 
 |-  ( j e. NN -> ( ! ` ( j + 1 ) ) e. CC )
94 2cnd 
 |-  ( j e. NN -> 2 e. CC )
95 nncn 
 |-  ( j e. NN -> j e. CC )
96 1cnd 
 |-  ( j e. NN -> 1 e. CC )
97 95 96 addcld 
 |-  ( j e. NN -> ( j + 1 ) e. CC )
98 94 97 mulcld 
 |-  ( j e. NN -> ( 2 x. ( j + 1 ) ) e. CC )
99 98 sqrtcld 
 |-  ( j e. NN -> ( sqrt ` ( 2 x. ( j + 1 ) ) ) e. CC )
100 ere 
 |-  _e e. RR
101 100 recni 
 |-  _e e. CC
102 101 a1i 
 |-  ( j e. NN -> _e e. CC )
103 0re 
 |-  0 e. RR
104 epos 
 |-  0 < _e
105 103 104 gtneii 
 |-  _e =/= 0
106 105 a1i 
 |-  ( j e. NN -> _e =/= 0 )
107 97 102 106 divcld 
 |-  ( j e. NN -> ( ( j + 1 ) / _e ) e. CC )
108 107 90 expcld 
 |-  ( j e. NN -> ( ( ( j + 1 ) / _e ) ^ ( j + 1 ) ) e. CC )
109 99 108 mulcld 
 |-  ( j e. NN -> ( ( sqrt ` ( 2 x. ( j + 1 ) ) ) x. ( ( ( j + 1 ) / _e ) ^ ( j + 1 ) ) ) e. CC )
110 2rp 
 |-  2 e. RR+
111 110 a1i 
 |-  ( j e. NN -> 2 e. RR+ )
112 nnre 
 |-  ( j e. NN -> j e. RR )
113 103 a1i 
 |-  ( j e. NN -> 0 e. RR )
114 1red 
 |-  ( j e. NN -> 1 e. RR )
115 0le1 
 |-  0 <_ 1
116 115 a1i 
 |-  ( j e. NN -> 0 <_ 1 )
117 nnge1 
 |-  ( j e. NN -> 1 <_ j )
118 113 114 112 116 117 letrd 
 |-  ( j e. NN -> 0 <_ j )
119 112 118 ge0p1rpd 
 |-  ( j e. NN -> ( j + 1 ) e. RR+ )
120 111 119 rpmulcld 
 |-  ( j e. NN -> ( 2 x. ( j + 1 ) ) e. RR+ )
121 120 sqrtgt0d 
 |-  ( j e. NN -> 0 < ( sqrt ` ( 2 x. ( j + 1 ) ) ) )
122 121 gt0ne0d 
 |-  ( j e. NN -> ( sqrt ` ( 2 x. ( j + 1 ) ) ) =/= 0 )
123 80 nnne0d 
 |-  ( j e. NN -> ( j + 1 ) =/= 0 )
124 97 102 123 106 divne0d 
 |-  ( j e. NN -> ( ( j + 1 ) / _e ) =/= 0 )
125 nnz 
 |-  ( j e. NN -> j e. ZZ )
126 125 peano2zd 
 |-  ( j e. NN -> ( j + 1 ) e. ZZ )
127 107 124 126 expne0d 
 |-  ( j e. NN -> ( ( ( j + 1 ) / _e ) ^ ( j + 1 ) ) =/= 0 )
128 99 108 122 127 mulne0d 
 |-  ( j e. NN -> ( ( sqrt ` ( 2 x. ( j + 1 ) ) ) x. ( ( ( j + 1 ) / _e ) ^ ( j + 1 ) ) ) =/= 0 )
129 93 109 128 divcld 
 |-  ( j e. NN -> ( ( ! ` ( j + 1 ) ) / ( ( sqrt ` ( 2 x. ( j + 1 ) ) ) x. ( ( ( j + 1 ) / _e ) ^ ( j + 1 ) ) ) ) e. CC )
130 81 89 80 129 fvmptd 
 |-  ( j e. NN -> ( A ` ( j + 1 ) ) = ( ( ! ` ( j + 1 ) ) / ( ( sqrt ` ( 2 x. ( j + 1 ) ) ) x. ( ( ( j + 1 ) / _e ) ^ ( j + 1 ) ) ) ) )
131 nnrp 
 |-  ( ( ! ` ( j + 1 ) ) e. NN -> ( ! ` ( j + 1 ) ) e. RR+ )
132 90 91 131 3syl 
 |-  ( j e. NN -> ( ! ` ( j + 1 ) ) e. RR+ )
133 120 rpsqrtcld 
 |-  ( j e. NN -> ( sqrt ` ( 2 x. ( j + 1 ) ) ) e. RR+ )
134 epr 
 |-  _e e. RR+
135 134 a1i 
 |-  ( j e. NN -> _e e. RR+ )
136 119 135 rpdivcld 
 |-  ( j e. NN -> ( ( j + 1 ) / _e ) e. RR+ )
137 136 126 rpexpcld 
 |-  ( j e. NN -> ( ( ( j + 1 ) / _e ) ^ ( j + 1 ) ) e. RR+ )
138 133 137 rpmulcld 
 |-  ( j e. NN -> ( ( sqrt ` ( 2 x. ( j + 1 ) ) ) x. ( ( ( j + 1 ) / _e ) ^ ( j + 1 ) ) ) e. RR+ )
139 132 138 rpdivcld 
 |-  ( j e. NN -> ( ( ! ` ( j + 1 ) ) / ( ( sqrt ` ( 2 x. ( j + 1 ) ) ) x. ( ( ( j + 1 ) / _e ) ^ ( j + 1 ) ) ) ) e. RR+ )
140 130 139 eqeltrd 
 |-  ( j e. NN -> ( A ` ( j + 1 ) ) e. RR+ )
141 140 relogcld 
 |-  ( j e. NN -> ( log ` ( A ` ( j + 1 ) ) ) e. RR )
142 nfcv 
 |-  F/_ n ( j + 1 )
143 21 142 nffv 
 |-  F/_ n ( A ` ( j + 1 ) )
144 19 143 nffv 
 |-  F/_ n ( log ` ( A ` ( j + 1 ) ) )
145 2fveq3 
 |-  ( n = ( j + 1 ) -> ( log ` ( A ` n ) ) = ( log ` ( A ` ( j + 1 ) ) ) )
146 142 144 145 2 fvmptf 
 |-  ( ( ( j + 1 ) e. NN /\ ( log ` ( A ` ( j + 1 ) ) ) e. RR ) -> ( B ` ( j + 1 ) ) = ( log ` ( A ` ( j + 1 ) ) ) )
147 80 141 146 syl2anc 
 |-  ( j e. NN -> ( B ` ( j + 1 ) ) = ( log ` ( A ` ( j + 1 ) ) ) )
148 147 141 eqeltrd 
 |-  ( j e. NN -> ( B ` ( j + 1 ) ) e. RR )
149 78 ffvelcdmi 
 |-  ( j e. NN -> ( B ` j ) e. RR )
150 eqid 
 |-  ( z e. NN |-> ( ( 1 / ( ( 2 x. z ) + 1 ) ) x. ( ( 1 / ( ( 2 x. j ) + 1 ) ) ^ ( 2 x. z ) ) ) ) = ( z e. NN |-> ( ( 1 / ( ( 2 x. z ) + 1 ) ) x. ( ( 1 / ( ( 2 x. j ) + 1 ) ) ^ ( 2 x. z ) ) ) )
151 1 2 150 stirlinglem11 
 |-  ( j e. NN -> ( B ` ( j + 1 ) ) < ( B ` j ) )
152 148 149 151 ltled 
 |-  ( j e. NN -> ( B ` ( j + 1 ) ) <_ ( B ` j ) )
153 152 adantl 
 |-  ( ( T. /\ j e. NN ) -> ( B ` ( j + 1 ) ) <_ ( B ` j ) )
154 52 a1i 
 |-  ( T. -> E. x e. RR A. j e. NN x <_ ( B ` j ) )
155 76 77 79 153 154 climinf 
 |-  ( T. -> B ~~> inf ( ran B , RR , < ) )
156 155 mptru 
 |-  B ~~> inf ( ran B , RR , < )
157 breq2 
 |-  ( d = inf ( ran B , RR , < ) -> ( B ~~> d <-> B ~~> inf ( ran B , RR , < ) ) )
158 157 rspcev 
 |-  ( ( inf ( ran B , RR , < ) e. RR /\ B ~~> inf ( ran B , RR , < ) ) -> E. d e. RR B ~~> d )
159 75 156 158 mp2an 
 |-  E. d e. RR B ~~> d