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 simpr 
 |-  ( ( A. j e. NN x <_ ( B ` j ) /\ y e. ran B ) -> y e. ran B )
54 8 rgen 
 |-  A. n e. NN ( log ` ( A ` n ) ) e. RR
55 2 fnmpt 
 |-  ( A. n e. NN ( log ` ( A ` n ) ) e. RR -> B Fn NN )
56 fvelrnb 
 |-  ( B Fn NN -> ( y e. ran B <-> E. j e. NN ( B ` j ) = y ) )
57 54 55 56 mp2b 
 |-  ( y e. ran B <-> E. j e. NN ( B ` j ) = y )
58 53 57 sylib 
 |-  ( ( A. j e. NN x <_ ( B ` j ) /\ y e. ran B ) -> E. j e. NN ( B ` j ) = y )
59 nfra1 
 |-  F/ j A. j e. NN x <_ ( B ` j )
60 nfv 
 |-  F/ j y e. ran B
61 59 60 nfan 
 |-  F/ j ( A. j e. NN x <_ ( B ` j ) /\ y e. ran B )
62 nfv 
 |-  F/ j x <_ y
63 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 ) )
64 simp2 
 |-  ( ( ( A. j e. NN x <_ ( B ` j ) /\ y e. ran B ) /\ j e. NN /\ ( B ` j ) = y ) -> j e. NN )
65 rsp 
 |-  ( A. j e. NN x <_ ( B ` j ) -> ( j e. NN -> x <_ ( B ` j ) ) )
66 63 64 65 sylc 
 |-  ( ( ( A. j e. NN x <_ ( B ` j ) /\ y e. ran B ) /\ j e. NN /\ ( B ` j ) = y ) -> x <_ ( B ` j ) )
67 simp3 
 |-  ( ( ( A. j e. NN x <_ ( B ` j ) /\ y e. ran B ) /\ j e. NN /\ ( B ` j ) = y ) -> ( B ` j ) = y )
68 66 67 breqtrd 
 |-  ( ( ( A. j e. NN x <_ ( B ` j ) /\ y e. ran B ) /\ j e. NN /\ ( B ` j ) = y ) -> x <_ y )
69 68 3exp 
 |-  ( ( A. j e. NN x <_ ( B ` j ) /\ y e. ran B ) -> ( j e. NN -> ( ( B ` j ) = y -> x <_ y ) ) )
70 61 62 69 rexlimd 
 |-  ( ( A. j e. NN x <_ ( B ` j ) /\ y e. ran B ) -> ( E. j e. NN ( B ` j ) = y -> x <_ y ) )
71 58 70 mpd 
 |-  ( ( A. j e. NN x <_ ( B ` j ) /\ y e. ran B ) -> x <_ y )
72 71 ralrimiva 
 |-  ( A. j e. NN x <_ ( B ` j ) -> A. y e. ran B x <_ y )
73 72 reximi 
 |-  ( E. x e. RR A. j e. NN x <_ ( B ` j ) -> E. x e. RR A. y e. ran B x <_ y )
74 52 73 ax-mp 
 |-  E. x e. RR A. y e. ran B x <_ y
75 infrecl 
 |-  ( ( ran B C_ RR /\ ran B =/= (/) /\ E. x e. RR A. y e. ran B x <_ y ) -> inf ( ran B , RR , < ) e. RR )
76 13 41 74 75 mp3an 
 |-  inf ( ran B , RR , < ) e. RR
77 nnuz 
 |-  NN = ( ZZ>= ` 1 )
78 1zzd 
 |-  ( T. -> 1 e. ZZ )
79 2 8 fmpti 
 |-  B : NN --> RR
80 79 a1i 
 |-  ( T. -> B : NN --> RR )
81 peano2nn 
 |-  ( j e. NN -> ( j + 1 ) e. NN )
82 1 a1i 
 |-  ( j e. NN -> A = ( n e. NN |-> ( ( ! ` n ) / ( ( sqrt ` ( 2 x. n ) ) x. ( ( n / _e ) ^ n ) ) ) ) )
83 simpr 
 |-  ( ( j e. NN /\ n = ( j + 1 ) ) -> n = ( j + 1 ) )
84 83 fveq2d 
 |-  ( ( j e. NN /\ n = ( j + 1 ) ) -> ( ! ` n ) = ( ! ` ( j + 1 ) ) )
85 83 oveq2d 
 |-  ( ( j e. NN /\ n = ( j + 1 ) ) -> ( 2 x. n ) = ( 2 x. ( j + 1 ) ) )
86 85 fveq2d 
 |-  ( ( j e. NN /\ n = ( j + 1 ) ) -> ( sqrt ` ( 2 x. n ) ) = ( sqrt ` ( 2 x. ( j + 1 ) ) ) )
87 83 oveq1d 
 |-  ( ( j e. NN /\ n = ( j + 1 ) ) -> ( n / _e ) = ( ( j + 1 ) / _e ) )
88 87 83 oveq12d 
 |-  ( ( j e. NN /\ n = ( j + 1 ) ) -> ( ( n / _e ) ^ n ) = ( ( ( j + 1 ) / _e ) ^ ( j + 1 ) ) )
89 86 88 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 ) ) ) )
90 84 89 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 ) ) ) ) )
91 81 nnnn0d 
 |-  ( j e. NN -> ( j + 1 ) e. NN0 )
92 faccl 
 |-  ( ( j + 1 ) e. NN0 -> ( ! ` ( j + 1 ) ) e. NN )
93 nncn 
 |-  ( ( ! ` ( j + 1 ) ) e. NN -> ( ! ` ( j + 1 ) ) e. CC )
94 91 92 93 3syl 
 |-  ( j e. NN -> ( ! ` ( j + 1 ) ) e. CC )
95 2cnd 
 |-  ( j e. NN -> 2 e. CC )
96 nncn 
 |-  ( j e. NN -> j e. CC )
97 1cnd 
 |-  ( j e. NN -> 1 e. CC )
98 96 97 addcld 
 |-  ( j e. NN -> ( j + 1 ) e. CC )
99 95 98 mulcld 
 |-  ( j e. NN -> ( 2 x. ( j + 1 ) ) e. CC )
100 99 sqrtcld 
 |-  ( j e. NN -> ( sqrt ` ( 2 x. ( j + 1 ) ) ) e. CC )
101 ere 
 |-  _e e. RR
102 101 recni 
 |-  _e e. CC
103 102 a1i 
 |-  ( j e. NN -> _e e. CC )
104 0re 
 |-  0 e. RR
105 epos 
 |-  0 < _e
106 104 105 gtneii 
 |-  _e =/= 0
107 106 a1i 
 |-  ( j e. NN -> _e =/= 0 )
108 98 103 107 divcld 
 |-  ( j e. NN -> ( ( j + 1 ) / _e ) e. CC )
109 108 91 expcld 
 |-  ( j e. NN -> ( ( ( j + 1 ) / _e ) ^ ( j + 1 ) ) e. CC )
110 100 109 mulcld 
 |-  ( j e. NN -> ( ( sqrt ` ( 2 x. ( j + 1 ) ) ) x. ( ( ( j + 1 ) / _e ) ^ ( j + 1 ) ) ) e. CC )
111 2rp 
 |-  2 e. RR+
112 111 a1i 
 |-  ( j e. NN -> 2 e. RR+ )
113 nnre 
 |-  ( j e. NN -> j e. RR )
114 104 a1i 
 |-  ( j e. NN -> 0 e. RR )
115 1red 
 |-  ( j e. NN -> 1 e. RR )
116 0le1 
 |-  0 <_ 1
117 116 a1i 
 |-  ( j e. NN -> 0 <_ 1 )
118 nnge1 
 |-  ( j e. NN -> 1 <_ j )
119 114 115 113 117 118 letrd 
 |-  ( j e. NN -> 0 <_ j )
120 113 119 ge0p1rpd 
 |-  ( j e. NN -> ( j + 1 ) e. RR+ )
121 112 120 rpmulcld 
 |-  ( j e. NN -> ( 2 x. ( j + 1 ) ) e. RR+ )
122 121 sqrtgt0d 
 |-  ( j e. NN -> 0 < ( sqrt ` ( 2 x. ( j + 1 ) ) ) )
123 122 gt0ne0d 
 |-  ( j e. NN -> ( sqrt ` ( 2 x. ( j + 1 ) ) ) =/= 0 )
124 81 nnne0d 
 |-  ( j e. NN -> ( j + 1 ) =/= 0 )
125 98 103 124 107 divne0d 
 |-  ( j e. NN -> ( ( j + 1 ) / _e ) =/= 0 )
126 nnz 
 |-  ( j e. NN -> j e. ZZ )
127 126 peano2zd 
 |-  ( j e. NN -> ( j + 1 ) e. ZZ )
128 108 125 127 expne0d 
 |-  ( j e. NN -> ( ( ( j + 1 ) / _e ) ^ ( j + 1 ) ) =/= 0 )
129 100 109 123 128 mulne0d 
 |-  ( j e. NN -> ( ( sqrt ` ( 2 x. ( j + 1 ) ) ) x. ( ( ( j + 1 ) / _e ) ^ ( j + 1 ) ) ) =/= 0 )
130 94 110 129 divcld 
 |-  ( j e. NN -> ( ( ! ` ( j + 1 ) ) / ( ( sqrt ` ( 2 x. ( j + 1 ) ) ) x. ( ( ( j + 1 ) / _e ) ^ ( j + 1 ) ) ) ) e. CC )
131 82 90 81 130 fvmptd 
 |-  ( j e. NN -> ( A ` ( j + 1 ) ) = ( ( ! ` ( j + 1 ) ) / ( ( sqrt ` ( 2 x. ( j + 1 ) ) ) x. ( ( ( j + 1 ) / _e ) ^ ( j + 1 ) ) ) ) )
132 nnrp 
 |-  ( ( ! ` ( j + 1 ) ) e. NN -> ( ! ` ( j + 1 ) ) e. RR+ )
133 91 92 132 3syl 
 |-  ( j e. NN -> ( ! ` ( j + 1 ) ) e. RR+ )
134 121 rpsqrtcld 
 |-  ( j e. NN -> ( sqrt ` ( 2 x. ( j + 1 ) ) ) e. RR+ )
135 epr 
 |-  _e e. RR+
136 135 a1i 
 |-  ( j e. NN -> _e e. RR+ )
137 120 136 rpdivcld 
 |-  ( j e. NN -> ( ( j + 1 ) / _e ) e. RR+ )
138 137 127 rpexpcld 
 |-  ( j e. NN -> ( ( ( j + 1 ) / _e ) ^ ( j + 1 ) ) e. RR+ )
139 134 138 rpmulcld 
 |-  ( j e. NN -> ( ( sqrt ` ( 2 x. ( j + 1 ) ) ) x. ( ( ( j + 1 ) / _e ) ^ ( j + 1 ) ) ) e. RR+ )
140 133 139 rpdivcld 
 |-  ( j e. NN -> ( ( ! ` ( j + 1 ) ) / ( ( sqrt ` ( 2 x. ( j + 1 ) ) ) x. ( ( ( j + 1 ) / _e ) ^ ( j + 1 ) ) ) ) e. RR+ )
141 131 140 eqeltrd 
 |-  ( j e. NN -> ( A ` ( j + 1 ) ) e. RR+ )
142 141 relogcld 
 |-  ( j e. NN -> ( log ` ( A ` ( j + 1 ) ) ) e. RR )
143 nfcv 
 |-  F/_ n ( j + 1 )
144 21 143 nffv 
 |-  F/_ n ( A ` ( j + 1 ) )
145 19 144 nffv 
 |-  F/_ n ( log ` ( A ` ( j + 1 ) ) )
146 2fveq3 
 |-  ( n = ( j + 1 ) -> ( log ` ( A ` n ) ) = ( log ` ( A ` ( j + 1 ) ) ) )
147 143 145 146 2 fvmptf 
 |-  ( ( ( j + 1 ) e. NN /\ ( log ` ( A ` ( j + 1 ) ) ) e. RR ) -> ( B ` ( j + 1 ) ) = ( log ` ( A ` ( j + 1 ) ) ) )
148 81 142 147 syl2anc 
 |-  ( j e. NN -> ( B ` ( j + 1 ) ) = ( log ` ( A ` ( j + 1 ) ) ) )
149 148 142 eqeltrd 
 |-  ( j e. NN -> ( B ` ( j + 1 ) ) e. RR )
150 79 ffvelcdmi 
 |-  ( j e. NN -> ( B ` j ) e. RR )
151 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 ) ) ) )
152 1 2 151 stirlinglem11 
 |-  ( j e. NN -> ( B ` ( j + 1 ) ) < ( B ` j ) )
153 149 150 152 ltled 
 |-  ( j e. NN -> ( B ` ( j + 1 ) ) <_ ( B ` j ) )
154 153 adantl 
 |-  ( ( T. /\ j e. NN ) -> ( B ` ( j + 1 ) ) <_ ( B ` j ) )
155 52 a1i 
 |-  ( T. -> E. x e. RR A. j e. NN x <_ ( B ` j ) )
156 77 78 80 154 155 climinf 
 |-  ( T. -> B ~~> inf ( ran B , RR , < ) )
157 156 mptru 
 |-  B ~~> inf ( ran B , RR , < )
158 breq2 
 |-  ( d = inf ( ran B , RR , < ) -> ( B ~~> d <-> B ~~> inf ( ran B , RR , < ) ) )
159 158 rspcev 
 |-  ( ( inf ( ran B , RR , < ) e. RR /\ B ~~> inf ( ran B , RR , < ) ) -> E. d e. RR B ~~> d )
160 76 157 159 mp2an 
 |-  E. d e. RR B ~~> d