Metamath Proof Explorer

Theorem stirlinglem8

Description: If A converges to C , then F converges to C^2 . (Contributed by Glauco Siliprandi, 29-Jun-2017)

Ref Expression
Hypotheses stirlinglem8.1 
|- F/ n ph
stirlinglem8.2 
|- F/_ n A
stirlinglem8.3 
|- F/_ n D
stirlinglem8.4 
|- D = ( n e. NN |-> ( A ` ( 2 x. n ) ) )
stirlinglem8.5 
|- ( ph -> A : NN --> RR+ )
stirlinglem8.6 
|- F = ( n e. NN |-> ( ( ( A ` n ) ^ 4 ) / ( ( D ` n ) ^ 2 ) ) )
stirlinglem8.7 
|- L = ( n e. NN |-> ( ( A ` n ) ^ 4 ) )
stirlinglem8.8 
|- M = ( n e. NN |-> ( ( D ` n ) ^ 2 ) )
stirlinglem8.9 
|- ( ( ph /\ n e. NN ) -> ( D ` n ) e. RR+ )
stirlinglem8.10 
|- ( ph -> C e. RR+ )
stirlinglem8.11 
|- ( ph -> A ~~> C )
Assertion stirlinglem8 
|- ( ph -> F ~~> ( C ^ 2 ) )

Proof

Step Hyp Ref Expression
1 stirlinglem8.1 
 |-  F/ n ph
2 stirlinglem8.2 
 |-  F/_ n A
3 stirlinglem8.3 
 |-  F/_ n D
4 stirlinglem8.4 
 |-  D = ( n e. NN |-> ( A ` ( 2 x. n ) ) )
5 stirlinglem8.5 
 |-  ( ph -> A : NN --> RR+ )
6 stirlinglem8.6 
 |-  F = ( n e. NN |-> ( ( ( A ` n ) ^ 4 ) / ( ( D ` n ) ^ 2 ) ) )
7 stirlinglem8.7 
 |-  L = ( n e. NN |-> ( ( A ` n ) ^ 4 ) )
8 stirlinglem8.8 
 |-  M = ( n e. NN |-> ( ( D ` n ) ^ 2 ) )
9 stirlinglem8.9 
 |-  ( ( ph /\ n e. NN ) -> ( D ` n ) e. RR+ )
10 stirlinglem8.10 
 |-  ( ph -> C e. RR+ )
11 stirlinglem8.11 
 |-  ( ph -> A ~~> C )
12 nfmpt1 
 |-  F/_ n ( n e. NN |-> ( ( A ` n ) ^ 4 ) )
13 7 12 nfcxfr 
 |-  F/_ n L
14 nfmpt1 
 |-  F/_ n ( n e. NN |-> ( ( D ` n ) ^ 2 ) )
15 8 14 nfcxfr 
 |-  F/_ n M
16 nfmpt1 
 |-  F/_ n ( n e. NN |-> ( ( ( A ` n ) ^ 4 ) / ( ( D ` n ) ^ 2 ) ) )
17 6 16 nfcxfr 
 |-  F/_ n F
18 nnuz 
 |-  NN = ( ZZ>= ` 1 )
19 1zzd 
 |-  ( ph -> 1 e. ZZ )
20 rrpsscn 
 |-  RR+ C_ CC
21 fss 
 |-  ( ( A : NN --> RR+ /\ RR+ C_ CC ) -> A : NN --> CC )
22 5 20 21 sylancl 
 |-  ( ph -> A : NN --> CC )
23 4nn0 
 |-  4 e. NN0
24 23 a1i 
 |-  ( ph -> 4 e. NN0 )
25 nnex 
 |-  NN e. _V
26 25 mptex 
 |-  ( n e. NN |-> ( ( A ` n ) ^ 4 ) ) e. _V
27 7 26 eqeltri 
 |-  L e. _V
28 27 a1i 
 |-  ( ph -> L e. _V )
29 simpr 
 |-  ( ( ph /\ n e. NN ) -> n e. NN )
30 5 ffvelrnda 
 |-  ( ( ph /\ n e. NN ) -> ( A ` n ) e. RR+ )
31 30 rpcnd 
 |-  ( ( ph /\ n e. NN ) -> ( A ` n ) e. CC )
32 23 a1i 
 |-  ( ( ph /\ n e. NN ) -> 4 e. NN0 )
33 31 32 expcld 
 |-  ( ( ph /\ n e. NN ) -> ( ( A ` n ) ^ 4 ) e. CC )
34 7 fvmpt2 
 |-  ( ( n e. NN /\ ( ( A ` n ) ^ 4 ) e. CC ) -> ( L ` n ) = ( ( A ` n ) ^ 4 ) )
35 29 33 34 syl2anc 
 |-  ( ( ph /\ n e. NN ) -> ( L ` n ) = ( ( A ` n ) ^ 4 ) )
36 1 2 13 18 19 22 11 24 28 35 climexp 
 |-  ( ph -> L ~~> ( C ^ 4 ) )
37 25 mptex 
 |-  ( n e. NN |-> ( ( ( A ` n ) ^ 4 ) / ( ( D ` n ) ^ 2 ) ) ) e. _V
38 6 37 eqeltri 
 |-  F e. _V
39 38 a1i 
 |-  ( ph -> F e. _V )
40 22 adantr 
 |-  ( ( ph /\ n e. NN ) -> A : NN --> CC )
41 2nn 
 |-  2 e. NN
42 41 a1i 
 |-  ( n e. NN -> 2 e. NN )
43 id 
 |-  ( n e. NN -> n e. NN )
44 42 43 nnmulcld 
 |-  ( n e. NN -> ( 2 x. n ) e. NN )
45 44 adantl 
 |-  ( ( ph /\ n e. NN ) -> ( 2 x. n ) e. NN )
46 40 45 ffvelrnd 
 |-  ( ( ph /\ n e. NN ) -> ( A ` ( 2 x. n ) ) e. CC )
47 1 46 4 fmptdf 
 |-  ( ph -> D : NN --> CC )
48 nfmpt1 
 |-  F/_ n ( n e. NN |-> ( 2 x. n ) )
49 fex 
 |-  ( ( A : NN --> CC /\ NN e. _V ) -> A e. _V )
50 22 25 49 sylancl 
 |-  ( ph -> A e. _V )
51 1nn 
 |-  1 e. NN
52 2cnd 
 |-  ( ph -> 2 e. CC )
53 1cnd 
 |-  ( ph -> 1 e. CC )
54 52 53 mulcld 
 |-  ( ph -> ( 2 x. 1 ) e. CC )
55 oveq2 
 |-  ( n = 1 -> ( 2 x. n ) = ( 2 x. 1 ) )
56 eqid 
 |-  ( n e. NN |-> ( 2 x. n ) ) = ( n e. NN |-> ( 2 x. n ) )
57 55 56 fvmptg 
 |-  ( ( 1 e. NN /\ ( 2 x. 1 ) e. CC ) -> ( ( n e. NN |-> ( 2 x. n ) ) ` 1 ) = ( 2 x. 1 ) )
58 51 54 57 sylancr 
 |-  ( ph -> ( ( n e. NN |-> ( 2 x. n ) ) ` 1 ) = ( 2 x. 1 ) )
59 41 a1i 
 |-  ( ph -> 2 e. NN )
60 51 a1i 
 |-  ( ph -> 1 e. NN )
61 59 60 nnmulcld 
 |-  ( ph -> ( 2 x. 1 ) e. NN )
62 58 61 eqeltrd 
 |-  ( ph -> ( ( n e. NN |-> ( 2 x. n ) ) ` 1 ) e. NN )
63 1red 
 |-  ( n e. NN -> 1 e. RR )
64 42 nnred 
 |-  ( n e. NN -> 2 e. RR )
65 44 nnred 
 |-  ( n e. NN -> ( 2 x. n ) e. RR )
66 42 nnge1d 
 |-  ( n e. NN -> 1 <_ 2 )
67 63 64 65 66 leadd2dd 
 |-  ( n e. NN -> ( ( 2 x. n ) + 1 ) <_ ( ( 2 x. n ) + 2 ) )
68 56 fvmpt2 
 |-  ( ( n e. NN /\ ( 2 x. n ) e. NN ) -> ( ( n e. NN |-> ( 2 x. n ) ) ` n ) = ( 2 x. n ) )
69 44 68 mpdan 
 |-  ( n e. NN -> ( ( n e. NN |-> ( 2 x. n ) ) ` n ) = ( 2 x. n ) )
70 69 oveq1d 
 |-  ( n e. NN -> ( ( ( n e. NN |-> ( 2 x. n ) ) ` n ) + 1 ) = ( ( 2 x. n ) + 1 ) )
71 oveq2 
 |-  ( n = k -> ( 2 x. n ) = ( 2 x. k ) )
72 71 cbvmptv 
 |-  ( n e. NN |-> ( 2 x. n ) ) = ( k e. NN |-> ( 2 x. k ) )
73 72 a1i 
 |-  ( n e. NN -> ( n e. NN |-> ( 2 x. n ) ) = ( k e. NN |-> ( 2 x. k ) ) )
74 simpr 
 |-  ( ( n e. NN /\ k = ( n + 1 ) ) -> k = ( n + 1 ) )
75 74 oveq2d 
 |-  ( ( n e. NN /\ k = ( n + 1 ) ) -> ( 2 x. k ) = ( 2 x. ( n + 1 ) ) )
76 peano2nn 
 |-  ( n e. NN -> ( n + 1 ) e. NN )
77 42 76 nnmulcld 
 |-  ( n e. NN -> ( 2 x. ( n + 1 ) ) e. NN )
78 73 75 76 77 fvmptd 
 |-  ( n e. NN -> ( ( n e. NN |-> ( 2 x. n ) ) ` ( n + 1 ) ) = ( 2 x. ( n + 1 ) ) )
79 2cnd 
 |-  ( n e. NN -> 2 e. CC )
80 nncn 
 |-  ( n e. NN -> n e. CC )
81 1cnd 
 |-  ( n e. NN -> 1 e. CC )
82 79 80 81 adddid 
 |-  ( n e. NN -> ( 2 x. ( n + 1 ) ) = ( ( 2 x. n ) + ( 2 x. 1 ) ) )
83 79 mulid1d 
 |-  ( n e. NN -> ( 2 x. 1 ) = 2 )
84 83 oveq2d 
 |-  ( n e. NN -> ( ( 2 x. n ) + ( 2 x. 1 ) ) = ( ( 2 x. n ) + 2 ) )
85 78 82 84 3eqtrd 
 |-  ( n e. NN -> ( ( n e. NN |-> ( 2 x. n ) ) ` ( n + 1 ) ) = ( ( 2 x. n ) + 2 ) )
86 67 70 85 3brtr4d 
 |-  ( n e. NN -> ( ( ( n e. NN |-> ( 2 x. n ) ) ` n ) + 1 ) <_ ( ( n e. NN |-> ( 2 x. n ) ) ` ( n + 1 ) ) )
87 44 nnzd 
 |-  ( n e. NN -> ( 2 x. n ) e. ZZ )
88 69 87 eqeltrd 
 |-  ( n e. NN -> ( ( n e. NN |-> ( 2 x. n ) ) ` n ) e. ZZ )
89 88 peano2zd 
 |-  ( n e. NN -> ( ( ( n e. NN |-> ( 2 x. n ) ) ` n ) + 1 ) e. ZZ )
90 77 nnzd 
 |-  ( n e. NN -> ( 2 x. ( n + 1 ) ) e. ZZ )
91 78 90 eqeltrd 
 |-  ( n e. NN -> ( ( n e. NN |-> ( 2 x. n ) ) ` ( n + 1 ) ) e. ZZ )
92 eluz 
 |-  ( ( ( ( ( n e. NN |-> ( 2 x. n ) ) ` n ) + 1 ) e. ZZ /\ ( ( n e. NN |-> ( 2 x. n ) ) ` ( n + 1 ) ) e. ZZ ) -> ( ( ( n e. NN |-> ( 2 x. n ) ) ` ( n + 1 ) ) e. ( ZZ>= ` ( ( ( n e. NN |-> ( 2 x. n ) ) ` n ) + 1 ) ) <-> ( ( ( n e. NN |-> ( 2 x. n ) ) ` n ) + 1 ) <_ ( ( n e. NN |-> ( 2 x. n ) ) ` ( n + 1 ) ) ) )
93 89 91 92 syl2anc 
 |-  ( n e. NN -> ( ( ( n e. NN |-> ( 2 x. n ) ) ` ( n + 1 ) ) e. ( ZZ>= ` ( ( ( n e. NN |-> ( 2 x. n ) ) ` n ) + 1 ) ) <-> ( ( ( n e. NN |-> ( 2 x. n ) ) ` n ) + 1 ) <_ ( ( n e. NN |-> ( 2 x. n ) ) ` ( n + 1 ) ) ) )
94 86 93 mpbird 
 |-  ( n e. NN -> ( ( n e. NN |-> ( 2 x. n ) ) ` ( n + 1 ) ) e. ( ZZ>= ` ( ( ( n e. NN |-> ( 2 x. n ) ) ` n ) + 1 ) ) )
95 94 adantl 
 |-  ( ( ph /\ n e. NN ) -> ( ( n e. NN |-> ( 2 x. n ) ) ` ( n + 1 ) ) e. ( ZZ>= ` ( ( ( n e. NN |-> ( 2 x. n ) ) ` n ) + 1 ) ) )
96 25 mptex 
 |-  ( n e. NN |-> ( A ` ( 2 x. n ) ) ) e. _V
97 4 96 eqeltri 
 |-  D e. _V
98 97 a1i 
 |-  ( ph -> D e. _V )
99 4 fvmpt2 
 |-  ( ( n e. NN /\ ( A ` ( 2 x. n ) ) e. CC ) -> ( D ` n ) = ( A ` ( 2 x. n ) ) )
100 29 46 99 syl2anc 
 |-  ( ( ph /\ n e. NN ) -> ( D ` n ) = ( A ` ( 2 x. n ) ) )
101 69 adantl 
 |-  ( ( ph /\ n e. NN ) -> ( ( n e. NN |-> ( 2 x. n ) ) ` n ) = ( 2 x. n ) )
102 101 eqcomd 
 |-  ( ( ph /\ n e. NN ) -> ( 2 x. n ) = ( ( n e. NN |-> ( 2 x. n ) ) ` n ) )
103 102 fveq2d 
 |-  ( ( ph /\ n e. NN ) -> ( A ` ( 2 x. n ) ) = ( A ` ( ( n e. NN |-> ( 2 x. n ) ) ` n ) ) )
104 100 103 eqtrd 
 |-  ( ( ph /\ n e. NN ) -> ( D ` n ) = ( A ` ( ( n e. NN |-> ( 2 x. n ) ) ` n ) ) )
105 1 2 3 48 18 19 50 31 11 62 95 98 104 climsuse 
 |-  ( ph -> D ~~> C )
106 2nn0 
 |-  2 e. NN0
107 106 a1i 
 |-  ( ph -> 2 e. NN0 )
108 25 mptex 
 |-  ( n e. NN |-> ( ( D ` n ) ^ 2 ) ) e. _V
109 8 108 eqeltri 
 |-  M e. _V
110 109 a1i 
 |-  ( ph -> M e. _V )
111 9 rpcnd 
 |-  ( ( ph /\ n e. NN ) -> ( D ` n ) e. CC )
112 111 sqcld 
 |-  ( ( ph /\ n e. NN ) -> ( ( D ` n ) ^ 2 ) e. CC )
113 8 fvmpt2 
 |-  ( ( n e. NN /\ ( ( D ` n ) ^ 2 ) e. CC ) -> ( M ` n ) = ( ( D ` n ) ^ 2 ) )
114 29 112 113 syl2anc 
 |-  ( ( ph /\ n e. NN ) -> ( M ` n ) = ( ( D ` n ) ^ 2 ) )
115 1 3 15 18 19 47 105 107 110 114 climexp 
 |-  ( ph -> M ~~> ( C ^ 2 ) )
116 10 rpcnd 
 |-  ( ph -> C e. CC )
117 10 rpne0d 
 |-  ( ph -> C =/= 0 )
118 2z 
 |-  2 e. ZZ
119 118 a1i 
 |-  ( ph -> 2 e. ZZ )
120 116 117 119 expne0d 
 |-  ( ph -> ( C ^ 2 ) =/= 0 )
121 1 33 7 fmptdf 
 |-  ( ph -> L : NN --> CC )
122 121 ffvelrnda 
 |-  ( ( ph /\ n e. NN ) -> ( L ` n ) e. CC )
123 114 112 eqeltrd 
 |-  ( ( ph /\ n e. NN ) -> ( M ` n ) e. CC )
124 100 oveq1d 
 |-  ( ( ph /\ n e. NN ) -> ( ( D ` n ) ^ 2 ) = ( ( A ` ( 2 x. n ) ) ^ 2 ) )
125 114 124 eqtrd 
 |-  ( ( ph /\ n e. NN ) -> ( M ` n ) = ( ( A ` ( 2 x. n ) ) ^ 2 ) )
126 100 9 eqeltrrd 
 |-  ( ( ph /\ n e. NN ) -> ( A ` ( 2 x. n ) ) e. RR+ )
127 118 a1i 
 |-  ( ( ph /\ n e. NN ) -> 2 e. ZZ )
128 126 127 rpexpcld 
 |-  ( ( ph /\ n e. NN ) -> ( ( A ` ( 2 x. n ) ) ^ 2 ) e. RR+ )
129 125 128 eqeltrd 
 |-  ( ( ph /\ n e. NN ) -> ( M ` n ) e. RR+ )
130 129 rpne0d 
 |-  ( ( ph /\ n e. NN ) -> ( M ` n ) =/= 0 )
131 130 neneqd 
 |-  ( ( ph /\ n e. NN ) -> -. ( M ` n ) = 0 )
132 0cn 
 |-  0 e. CC
133 elsn2g 
 |-  ( 0 e. CC -> ( ( M ` n ) e. { 0 } <-> ( M ` n ) = 0 ) )
134 132 133 ax-mp 
 |-  ( ( M ` n ) e. { 0 } <-> ( M ` n ) = 0 )
135 131 134 sylnibr 
 |-  ( ( ph /\ n e. NN ) -> -. ( M ` n ) e. { 0 } )
136 123 135 eldifd 
 |-  ( ( ph /\ n e. NN ) -> ( M ` n ) e. ( CC \ { 0 } ) )
137 32 nn0zd 
 |-  ( ( ph /\ n e. NN ) -> 4 e. ZZ )
138 30 137 rpexpcld 
 |-  ( ( ph /\ n e. NN ) -> ( ( A ` n ) ^ 4 ) e. RR+ )
139 9 127 rpexpcld 
 |-  ( ( ph /\ n e. NN ) -> ( ( D ` n ) ^ 2 ) e. RR+ )
140 138 139 rpdivcld 
 |-  ( ( ph /\ n e. NN ) -> ( ( ( A ` n ) ^ 4 ) / ( ( D ` n ) ^ 2 ) ) e. RR+ )
141 6 fvmpt2 
 |-  ( ( n e. NN /\ ( ( ( A ` n ) ^ 4 ) / ( ( D ` n ) ^ 2 ) ) e. RR+ ) -> ( F ` n ) = ( ( ( A ` n ) ^ 4 ) / ( ( D ` n ) ^ 2 ) ) )
142 29 140 141 syl2anc 
 |-  ( ( ph /\ n e. NN ) -> ( F ` n ) = ( ( ( A ` n ) ^ 4 ) / ( ( D ` n ) ^ 2 ) ) )
143 7 fvmpt2 
 |-  ( ( n e. NN /\ ( ( A ` n ) ^ 4 ) e. RR+ ) -> ( L ` n ) = ( ( A ` n ) ^ 4 ) )
144 29 138 143 syl2anc 
 |-  ( ( ph /\ n e. NN ) -> ( L ` n ) = ( ( A ` n ) ^ 4 ) )
145 144 114 oveq12d 
 |-  ( ( ph /\ n e. NN ) -> ( ( L ` n ) / ( M ` n ) ) = ( ( ( A ` n ) ^ 4 ) / ( ( D ` n ) ^ 2 ) ) )
146 142 145 eqtr4d 
 |-  ( ( ph /\ n e. NN ) -> ( F ` n ) = ( ( L ` n ) / ( M ` n ) ) )
147 1 13 15 17 18 19 36 39 115 120 122 136 146 climdivf 
 |-  ( ph -> F ~~> ( ( C ^ 4 ) / ( C ^ 2 ) ) )
148 2cn 
 |-  2 e. CC
149 2p2e4 
 |-  ( 2 + 2 ) = 4
150 148 148 149 mvlladdi 
 |-  2 = ( 4 - 2 )
151 150 a1i 
 |-  ( ph -> 2 = ( 4 - 2 ) )
152 151 oveq2d 
 |-  ( ph -> ( C ^ 2 ) = ( C ^ ( 4 - 2 ) ) )
153 24 nn0zd 
 |-  ( ph -> 4 e. ZZ )
154 116 117 119 153 expsubd 
 |-  ( ph -> ( C ^ ( 4 - 2 ) ) = ( ( C ^ 4 ) / ( C ^ 2 ) ) )
155 152 154 eqtrd 
 |-  ( ph -> ( C ^ 2 ) = ( ( C ^ 4 ) / ( C ^ 2 ) ) )
156 147 155 breqtrrd 
 |-  ( ph -> F ~~> ( C ^ 2 ) )