Step |
Hyp |
Ref |
Expression |
1 |
|
stirlinglem15.1 |
|- F/ n ph |
2 |
|
stirlinglem15.2 |
|- S = ( n e. NN0 |-> ( ( sqrt ` ( ( 2 x. _pi ) x. n ) ) x. ( ( n / _e ) ^ n ) ) ) |
3 |
|
stirlinglem15.3 |
|- A = ( n e. NN |-> ( ( ! ` n ) / ( ( sqrt ` ( 2 x. n ) ) x. ( ( n / _e ) ^ n ) ) ) ) |
4 |
|
stirlinglem15.4 |
|- D = ( n e. NN |-> ( A ` ( 2 x. n ) ) ) |
5 |
|
stirlinglem15.5 |
|- E = ( n e. NN |-> ( ( sqrt ` ( 2 x. n ) ) x. ( ( n / _e ) ^ n ) ) ) |
6 |
|
stirlinglem15.6 |
|- V = ( n e. NN |-> ( ( ( ( 2 ^ ( 4 x. n ) ) x. ( ( ! ` n ) ^ 4 ) ) / ( ( ! ` ( 2 x. n ) ) ^ 2 ) ) / ( ( 2 x. n ) + 1 ) ) ) |
7 |
|
stirlinglem15.7 |
|- F = ( n e. NN |-> ( ( ( A ` n ) ^ 4 ) / ( ( D ` n ) ^ 2 ) ) ) |
8 |
|
stirlinglem15.8 |
|- H = ( n e. NN |-> ( ( n ^ 2 ) / ( n x. ( ( 2 x. n ) + 1 ) ) ) ) |
9 |
|
stirlinglem15.9 |
|- ( ph -> C e. RR+ ) |
10 |
|
stirlinglem15.10 |
|- ( ph -> A ~~> C ) |
11 |
|
nnnn0 |
|- ( n e. NN -> n e. NN0 ) |
12 |
11
|
adantl |
|- ( ( ph /\ n e. NN ) -> n e. NN0 ) |
13 |
|
2cnd |
|- ( ( ph /\ n e. NN ) -> 2 e. CC ) |
14 |
|
picn |
|- _pi e. CC |
15 |
14
|
a1i |
|- ( ( ph /\ n e. NN ) -> _pi e. CC ) |
16 |
13 15
|
mulcld |
|- ( ( ph /\ n e. NN ) -> ( 2 x. _pi ) e. CC ) |
17 |
|
nncn |
|- ( n e. NN -> n e. CC ) |
18 |
17
|
adantl |
|- ( ( ph /\ n e. NN ) -> n e. CC ) |
19 |
16 18
|
mulcld |
|- ( ( ph /\ n e. NN ) -> ( ( 2 x. _pi ) x. n ) e. CC ) |
20 |
19
|
sqrtcld |
|- ( ( ph /\ n e. NN ) -> ( sqrt ` ( ( 2 x. _pi ) x. n ) ) e. CC ) |
21 |
|
ere |
|- _e e. RR |
22 |
21
|
recni |
|- _e e. CC |
23 |
22
|
a1i |
|- ( n e. NN -> _e e. CC ) |
24 |
|
epos |
|- 0 < _e |
25 |
21 24
|
gt0ne0ii |
|- _e =/= 0 |
26 |
25
|
a1i |
|- ( n e. NN -> _e =/= 0 ) |
27 |
17 23 26
|
divcld |
|- ( n e. NN -> ( n / _e ) e. CC ) |
28 |
27 11
|
expcld |
|- ( n e. NN -> ( ( n / _e ) ^ n ) e. CC ) |
29 |
28
|
adantl |
|- ( ( ph /\ n e. NN ) -> ( ( n / _e ) ^ n ) e. CC ) |
30 |
20 29
|
mulcld |
|- ( ( ph /\ n e. NN ) -> ( ( sqrt ` ( ( 2 x. _pi ) x. n ) ) x. ( ( n / _e ) ^ n ) ) e. CC ) |
31 |
2
|
fvmpt2 |
|- ( ( n e. NN0 /\ ( ( sqrt ` ( ( 2 x. _pi ) x. n ) ) x. ( ( n / _e ) ^ n ) ) e. CC ) -> ( S ` n ) = ( ( sqrt ` ( ( 2 x. _pi ) x. n ) ) x. ( ( n / _e ) ^ n ) ) ) |
32 |
12 30 31
|
syl2anc |
|- ( ( ph /\ n e. NN ) -> ( S ` n ) = ( ( sqrt ` ( ( 2 x. _pi ) x. n ) ) x. ( ( n / _e ) ^ n ) ) ) |
33 |
32
|
oveq2d |
|- ( ( ph /\ n e. NN ) -> ( ( ! ` n ) / ( S ` n ) ) = ( ( ! ` n ) / ( ( sqrt ` ( ( 2 x. _pi ) x. n ) ) x. ( ( n / _e ) ^ n ) ) ) ) |
34 |
15
|
sqrtcld |
|- ( ( ph /\ n e. NN ) -> ( sqrt ` _pi ) e. CC ) |
35 |
|
2cnd |
|- ( n e. NN -> 2 e. CC ) |
36 |
35 17
|
mulcld |
|- ( n e. NN -> ( 2 x. n ) e. CC ) |
37 |
36
|
sqrtcld |
|- ( n e. NN -> ( sqrt ` ( 2 x. n ) ) e. CC ) |
38 |
37
|
adantl |
|- ( ( ph /\ n e. NN ) -> ( sqrt ` ( 2 x. n ) ) e. CC ) |
39 |
34 38 29
|
mulassd |
|- ( ( ph /\ n e. NN ) -> ( ( ( sqrt ` _pi ) x. ( sqrt ` ( 2 x. n ) ) ) x. ( ( n / _e ) ^ n ) ) = ( ( sqrt ` _pi ) x. ( ( sqrt ` ( 2 x. n ) ) x. ( ( n / _e ) ^ n ) ) ) ) |
40 |
|
nfmpt1 |
|- F/_ n ( n e. NN |-> ( ( ( A ` n ) ^ 4 ) / ( ( D ` n ) ^ 2 ) ) ) |
41 |
7 40
|
nfcxfr |
|- F/_ n F |
42 |
|
nfmpt1 |
|- F/_ n ( n e. NN |-> ( ( n ^ 2 ) / ( n x. ( ( 2 x. n ) + 1 ) ) ) ) |
43 |
8 42
|
nfcxfr |
|- F/_ n H |
44 |
|
nfmpt1 |
|- F/_ n ( n e. NN |-> ( ( ( ( 2 ^ ( 4 x. n ) ) x. ( ( ! ` n ) ^ 4 ) ) / ( ( ! ` ( 2 x. n ) ) ^ 2 ) ) / ( ( 2 x. n ) + 1 ) ) ) |
45 |
6 44
|
nfcxfr |
|- F/_ n V |
46 |
|
nnuz |
|- NN = ( ZZ>= ` 1 ) |
47 |
|
1zzd |
|- ( ph -> 1 e. ZZ ) |
48 |
|
nfmpt1 |
|- F/_ n ( n e. NN |-> ( ( ! ` n ) / ( ( sqrt ` ( 2 x. n ) ) x. ( ( n / _e ) ^ n ) ) ) ) |
49 |
3 48
|
nfcxfr |
|- F/_ n A |
50 |
|
nfmpt1 |
|- F/_ n ( n e. NN |-> ( A ` ( 2 x. n ) ) ) |
51 |
4 50
|
nfcxfr |
|- F/_ n D |
52 |
|
faccl |
|- ( n e. NN0 -> ( ! ` n ) e. NN ) |
53 |
11 52
|
syl |
|- ( n e. NN -> ( ! ` n ) e. NN ) |
54 |
53
|
nnrpd |
|- ( n e. NN -> ( ! ` n ) e. RR+ ) |
55 |
|
2rp |
|- 2 e. RR+ |
56 |
55
|
a1i |
|- ( n e. NN -> 2 e. RR+ ) |
57 |
|
nnrp |
|- ( n e. NN -> n e. RR+ ) |
58 |
56 57
|
rpmulcld |
|- ( n e. NN -> ( 2 x. n ) e. RR+ ) |
59 |
58
|
rpsqrtcld |
|- ( n e. NN -> ( sqrt ` ( 2 x. n ) ) e. RR+ ) |
60 |
|
epr |
|- _e e. RR+ |
61 |
60
|
a1i |
|- ( n e. NN -> _e e. RR+ ) |
62 |
57 61
|
rpdivcld |
|- ( n e. NN -> ( n / _e ) e. RR+ ) |
63 |
|
nnz |
|- ( n e. NN -> n e. ZZ ) |
64 |
62 63
|
rpexpcld |
|- ( n e. NN -> ( ( n / _e ) ^ n ) e. RR+ ) |
65 |
59 64
|
rpmulcld |
|- ( n e. NN -> ( ( sqrt ` ( 2 x. n ) ) x. ( ( n / _e ) ^ n ) ) e. RR+ ) |
66 |
54 65
|
rpdivcld |
|- ( n e. NN -> ( ( ! ` n ) / ( ( sqrt ` ( 2 x. n ) ) x. ( ( n / _e ) ^ n ) ) ) e. RR+ ) |
67 |
3 66
|
fmpti |
|- A : NN --> RR+ |
68 |
67
|
a1i |
|- ( ph -> A : NN --> RR+ ) |
69 |
|
eqid |
|- ( n e. NN |-> ( ( A ` n ) ^ 4 ) ) = ( n e. NN |-> ( ( A ` n ) ^ 4 ) ) |
70 |
|
eqid |
|- ( n e. NN |-> ( ( D ` n ) ^ 2 ) ) = ( n e. NN |-> ( ( D ` n ) ^ 2 ) ) |
71 |
67
|
a1i |
|- ( n e. NN -> A : NN --> RR+ ) |
72 |
|
2nn |
|- 2 e. NN |
73 |
72
|
a1i |
|- ( n e. NN -> 2 e. NN ) |
74 |
|
id |
|- ( n e. NN -> n e. NN ) |
75 |
73 74
|
nnmulcld |
|- ( n e. NN -> ( 2 x. n ) e. NN ) |
76 |
71 75
|
ffvelrnd |
|- ( n e. NN -> ( A ` ( 2 x. n ) ) e. RR+ ) |
77 |
4
|
fvmpt2 |
|- ( ( n e. NN /\ ( A ` ( 2 x. n ) ) e. RR+ ) -> ( D ` n ) = ( A ` ( 2 x. n ) ) ) |
78 |
76 77
|
mpdan |
|- ( n e. NN -> ( D ` n ) = ( A ` ( 2 x. n ) ) ) |
79 |
78 76
|
eqeltrd |
|- ( n e. NN -> ( D ` n ) e. RR+ ) |
80 |
79
|
adantl |
|- ( ( ph /\ n e. NN ) -> ( D ` n ) e. RR+ ) |
81 |
1 49 51 4 68 7 69 70 80 9 10
|
stirlinglem8 |
|- ( ph -> F ~~> ( C ^ 2 ) ) |
82 |
|
nnex |
|- NN e. _V |
83 |
82
|
mptex |
|- ( n e. NN |-> ( ( ( ( 2 ^ ( 4 x. n ) ) x. ( ( ! ` n ) ^ 4 ) ) / ( ( ! ` ( 2 x. n ) ) ^ 2 ) ) / ( ( 2 x. n ) + 1 ) ) ) e. _V |
84 |
6 83
|
eqeltri |
|- V e. _V |
85 |
84
|
a1i |
|- ( ph -> V e. _V ) |
86 |
|
eqid |
|- ( n e. NN |-> ( 1 - ( 1 / ( ( 2 x. n ) + 1 ) ) ) ) = ( n e. NN |-> ( 1 - ( 1 / ( ( 2 x. n ) + 1 ) ) ) ) |
87 |
|
eqid |
|- ( n e. NN |-> ( 1 / ( ( 2 x. n ) + 1 ) ) ) = ( n e. NN |-> ( 1 / ( ( 2 x. n ) + 1 ) ) ) |
88 |
|
eqid |
|- ( n e. NN |-> ( 1 / n ) ) = ( n e. NN |-> ( 1 / n ) ) |
89 |
8 86 87 88
|
stirlinglem1 |
|- H ~~> ( 1 / 2 ) |
90 |
89
|
a1i |
|- ( ph -> H ~~> ( 1 / 2 ) ) |
91 |
53
|
nncnd |
|- ( n e. NN -> ( ! ` n ) e. CC ) |
92 |
37 28
|
mulcld |
|- ( n e. NN -> ( ( sqrt ` ( 2 x. n ) ) x. ( ( n / _e ) ^ n ) ) e. CC ) |
93 |
58
|
sqrtgt0d |
|- ( n e. NN -> 0 < ( sqrt ` ( 2 x. n ) ) ) |
94 |
93
|
gt0ne0d |
|- ( n e. NN -> ( sqrt ` ( 2 x. n ) ) =/= 0 ) |
95 |
|
nnne0 |
|- ( n e. NN -> n =/= 0 ) |
96 |
17 23 95 26
|
divne0d |
|- ( n e. NN -> ( n / _e ) =/= 0 ) |
97 |
27 96 63
|
expne0d |
|- ( n e. NN -> ( ( n / _e ) ^ n ) =/= 0 ) |
98 |
37 28 94 97
|
mulne0d |
|- ( n e. NN -> ( ( sqrt ` ( 2 x. n ) ) x. ( ( n / _e ) ^ n ) ) =/= 0 ) |
99 |
91 92 98
|
divcld |
|- ( n e. NN -> ( ( ! ` n ) / ( ( sqrt ` ( 2 x. n ) ) x. ( ( n / _e ) ^ n ) ) ) e. CC ) |
100 |
3
|
fvmpt2 |
|- ( ( n e. NN /\ ( ( ! ` n ) / ( ( sqrt ` ( 2 x. n ) ) x. ( ( n / _e ) ^ n ) ) ) e. CC ) -> ( A ` n ) = ( ( ! ` n ) / ( ( sqrt ` ( 2 x. n ) ) x. ( ( n / _e ) ^ n ) ) ) ) |
101 |
99 100
|
mpdan |
|- ( n e. NN -> ( A ` n ) = ( ( ! ` n ) / ( ( sqrt ` ( 2 x. n ) ) x. ( ( n / _e ) ^ n ) ) ) ) |
102 |
101 99
|
eqeltrd |
|- ( n e. NN -> ( A ` n ) e. CC ) |
103 |
|
4nn0 |
|- 4 e. NN0 |
104 |
103
|
a1i |
|- ( n e. NN -> 4 e. NN0 ) |
105 |
102 104
|
expcld |
|- ( n e. NN -> ( ( A ` n ) ^ 4 ) e. CC ) |
106 |
79
|
rpcnd |
|- ( n e. NN -> ( D ` n ) e. CC ) |
107 |
106
|
sqcld |
|- ( n e. NN -> ( ( D ` n ) ^ 2 ) e. CC ) |
108 |
79
|
rpne0d |
|- ( n e. NN -> ( D ` n ) =/= 0 ) |
109 |
|
2z |
|- 2 e. ZZ |
110 |
109
|
a1i |
|- ( n e. NN -> 2 e. ZZ ) |
111 |
106 108 110
|
expne0d |
|- ( n e. NN -> ( ( D ` n ) ^ 2 ) =/= 0 ) |
112 |
105 107 111
|
divcld |
|- ( n e. NN -> ( ( ( A ` n ) ^ 4 ) / ( ( D ` n ) ^ 2 ) ) e. CC ) |
113 |
7
|
fvmpt2 |
|- ( ( n e. NN /\ ( ( ( A ` n ) ^ 4 ) / ( ( D ` n ) ^ 2 ) ) e. CC ) -> ( F ` n ) = ( ( ( A ` n ) ^ 4 ) / ( ( D ` n ) ^ 2 ) ) ) |
114 |
112 113
|
mpdan |
|- ( n e. NN -> ( F ` n ) = ( ( ( A ` n ) ^ 4 ) / ( ( D ` n ) ^ 2 ) ) ) |
115 |
114 112
|
eqeltrd |
|- ( n e. NN -> ( F ` n ) e. CC ) |
116 |
115
|
adantl |
|- ( ( ph /\ n e. NN ) -> ( F ` n ) e. CC ) |
117 |
17
|
sqcld |
|- ( n e. NN -> ( n ^ 2 ) e. CC ) |
118 |
|
1cnd |
|- ( n e. NN -> 1 e. CC ) |
119 |
36 118
|
addcld |
|- ( n e. NN -> ( ( 2 x. n ) + 1 ) e. CC ) |
120 |
17 119
|
mulcld |
|- ( n e. NN -> ( n x. ( ( 2 x. n ) + 1 ) ) e. CC ) |
121 |
75
|
nnred |
|- ( n e. NN -> ( 2 x. n ) e. RR ) |
122 |
|
1red |
|- ( n e. NN -> 1 e. RR ) |
123 |
75
|
nngt0d |
|- ( n e. NN -> 0 < ( 2 x. n ) ) |
124 |
|
0lt1 |
|- 0 < 1 |
125 |
124
|
a1i |
|- ( n e. NN -> 0 < 1 ) |
126 |
121 122 123 125
|
addgt0d |
|- ( n e. NN -> 0 < ( ( 2 x. n ) + 1 ) ) |
127 |
126
|
gt0ne0d |
|- ( n e. NN -> ( ( 2 x. n ) + 1 ) =/= 0 ) |
128 |
17 119 95 127
|
mulne0d |
|- ( n e. NN -> ( n x. ( ( 2 x. n ) + 1 ) ) =/= 0 ) |
129 |
117 120 128
|
divcld |
|- ( n e. NN -> ( ( n ^ 2 ) / ( n x. ( ( 2 x. n ) + 1 ) ) ) e. CC ) |
130 |
8
|
fvmpt2 |
|- ( ( n e. NN /\ ( ( n ^ 2 ) / ( n x. ( ( 2 x. n ) + 1 ) ) ) e. CC ) -> ( H ` n ) = ( ( n ^ 2 ) / ( n x. ( ( 2 x. n ) + 1 ) ) ) ) |
131 |
129 130
|
mpdan |
|- ( n e. NN -> ( H ` n ) = ( ( n ^ 2 ) / ( n x. ( ( 2 x. n ) + 1 ) ) ) ) |
132 |
131 129
|
eqeltrd |
|- ( n e. NN -> ( H ` n ) e. CC ) |
133 |
132
|
adantl |
|- ( ( ph /\ n e. NN ) -> ( H ` n ) e. CC ) |
134 |
112 129
|
mulcld |
|- ( n e. NN -> ( ( ( ( A ` n ) ^ 4 ) / ( ( D ` n ) ^ 2 ) ) x. ( ( n ^ 2 ) / ( n x. ( ( 2 x. n ) + 1 ) ) ) ) e. CC ) |
135 |
3 4 5 6
|
stirlinglem3 |
|- V = ( n e. NN |-> ( ( ( ( A ` n ) ^ 4 ) / ( ( D ` n ) ^ 2 ) ) x. ( ( n ^ 2 ) / ( n x. ( ( 2 x. n ) + 1 ) ) ) ) ) |
136 |
135
|
fvmpt2 |
|- ( ( n e. NN /\ ( ( ( ( A ` n ) ^ 4 ) / ( ( D ` n ) ^ 2 ) ) x. ( ( n ^ 2 ) / ( n x. ( ( 2 x. n ) + 1 ) ) ) ) e. CC ) -> ( V ` n ) = ( ( ( ( A ` n ) ^ 4 ) / ( ( D ` n ) ^ 2 ) ) x. ( ( n ^ 2 ) / ( n x. ( ( 2 x. n ) + 1 ) ) ) ) ) |
137 |
134 136
|
mpdan |
|- ( n e. NN -> ( V ` n ) = ( ( ( ( A ` n ) ^ 4 ) / ( ( D ` n ) ^ 2 ) ) x. ( ( n ^ 2 ) / ( n x. ( ( 2 x. n ) + 1 ) ) ) ) ) |
138 |
114 131
|
oveq12d |
|- ( n e. NN -> ( ( F ` n ) x. ( H ` n ) ) = ( ( ( ( A ` n ) ^ 4 ) / ( ( D ` n ) ^ 2 ) ) x. ( ( n ^ 2 ) / ( n x. ( ( 2 x. n ) + 1 ) ) ) ) ) |
139 |
137 138
|
eqtr4d |
|- ( n e. NN -> ( V ` n ) = ( ( F ` n ) x. ( H ` n ) ) ) |
140 |
139
|
adantl |
|- ( ( ph /\ n e. NN ) -> ( V ` n ) = ( ( F ` n ) x. ( H ` n ) ) ) |
141 |
1 41 43 45 46 47 81 85 90 116 133 140
|
climmulf |
|- ( ph -> V ~~> ( ( C ^ 2 ) x. ( 1 / 2 ) ) ) |
142 |
6
|
wallispi2 |
|- V ~~> ( _pi / 2 ) |
143 |
|
climuni |
|- ( ( V ~~> ( ( C ^ 2 ) x. ( 1 / 2 ) ) /\ V ~~> ( _pi / 2 ) ) -> ( ( C ^ 2 ) x. ( 1 / 2 ) ) = ( _pi / 2 ) ) |
144 |
141 142 143
|
sylancl |
|- ( ph -> ( ( C ^ 2 ) x. ( 1 / 2 ) ) = ( _pi / 2 ) ) |
145 |
144
|
oveq1d |
|- ( ph -> ( ( ( C ^ 2 ) x. ( 1 / 2 ) ) / ( 1 / 2 ) ) = ( ( _pi / 2 ) / ( 1 / 2 ) ) ) |
146 |
9
|
rpcnd |
|- ( ph -> C e. CC ) |
147 |
146
|
sqcld |
|- ( ph -> ( C ^ 2 ) e. CC ) |
148 |
|
1cnd |
|- ( ph -> 1 e. CC ) |
149 |
148
|
halfcld |
|- ( ph -> ( 1 / 2 ) e. CC ) |
150 |
|
2cnd |
|- ( ph -> 2 e. CC ) |
151 |
|
2pos |
|- 0 < 2 |
152 |
151
|
a1i |
|- ( ph -> 0 < 2 ) |
153 |
152
|
gt0ne0d |
|- ( ph -> 2 =/= 0 ) |
154 |
150 153
|
recne0d |
|- ( ph -> ( 1 / 2 ) =/= 0 ) |
155 |
147 149 154
|
divcan4d |
|- ( ph -> ( ( ( C ^ 2 ) x. ( 1 / 2 ) ) / ( 1 / 2 ) ) = ( C ^ 2 ) ) |
156 |
14
|
a1i |
|- ( ph -> _pi e. CC ) |
157 |
124
|
a1i |
|- ( ph -> 0 < 1 ) |
158 |
157
|
gt0ne0d |
|- ( ph -> 1 =/= 0 ) |
159 |
156 148 150 158 153
|
divcan7d |
|- ( ph -> ( ( _pi / 2 ) / ( 1 / 2 ) ) = ( _pi / 1 ) ) |
160 |
156
|
div1d |
|- ( ph -> ( _pi / 1 ) = _pi ) |
161 |
159 160
|
eqtrd |
|- ( ph -> ( ( _pi / 2 ) / ( 1 / 2 ) ) = _pi ) |
162 |
145 155 161
|
3eqtr3d |
|- ( ph -> ( C ^ 2 ) = _pi ) |
163 |
162
|
fveq2d |
|- ( ph -> ( sqrt ` ( C ^ 2 ) ) = ( sqrt ` _pi ) ) |
164 |
9
|
rprege0d |
|- ( ph -> ( C e. RR /\ 0 <_ C ) ) |
165 |
|
sqrtsq |
|- ( ( C e. RR /\ 0 <_ C ) -> ( sqrt ` ( C ^ 2 ) ) = C ) |
166 |
164 165
|
syl |
|- ( ph -> ( sqrt ` ( C ^ 2 ) ) = C ) |
167 |
163 166
|
eqtr3d |
|- ( ph -> ( sqrt ` _pi ) = C ) |
168 |
167
|
adantr |
|- ( ( ph /\ n e. NN ) -> ( sqrt ` _pi ) = C ) |
169 |
168
|
oveq1d |
|- ( ( ph /\ n e. NN ) -> ( ( sqrt ` _pi ) x. ( ( sqrt ` ( 2 x. n ) ) x. ( ( n / _e ) ^ n ) ) ) = ( C x. ( ( sqrt ` ( 2 x. n ) ) x. ( ( n / _e ) ^ n ) ) ) ) |
170 |
146
|
adantr |
|- ( ( ph /\ n e. NN ) -> C e. CC ) |
171 |
92
|
adantl |
|- ( ( ph /\ n e. NN ) -> ( ( sqrt ` ( 2 x. n ) ) x. ( ( n / _e ) ^ n ) ) e. CC ) |
172 |
170 171
|
mulcomd |
|- ( ( ph /\ n e. NN ) -> ( C x. ( ( sqrt ` ( 2 x. n ) ) x. ( ( n / _e ) ^ n ) ) ) = ( ( ( sqrt ` ( 2 x. n ) ) x. ( ( n / _e ) ^ n ) ) x. C ) ) |
173 |
39 169 172
|
3eqtrd |
|- ( ( ph /\ n e. NN ) -> ( ( ( sqrt ` _pi ) x. ( sqrt ` ( 2 x. n ) ) ) x. ( ( n / _e ) ^ n ) ) = ( ( ( sqrt ` ( 2 x. n ) ) x. ( ( n / _e ) ^ n ) ) x. C ) ) |
174 |
173
|
oveq2d |
|- ( ( ph /\ n e. NN ) -> ( ( ! ` n ) / ( ( ( sqrt ` _pi ) x. ( sqrt ` ( 2 x. n ) ) ) x. ( ( n / _e ) ^ n ) ) ) = ( ( ! ` n ) / ( ( ( sqrt ` ( 2 x. n ) ) x. ( ( n / _e ) ^ n ) ) x. C ) ) ) |
175 |
|
2re |
|- 2 e. RR |
176 |
175
|
a1i |
|- ( ( ph /\ n e. NN ) -> 2 e. RR ) |
177 |
|
pire |
|- _pi e. RR |
178 |
177
|
a1i |
|- ( ( ph /\ n e. NN ) -> _pi e. RR ) |
179 |
176 178
|
remulcld |
|- ( ( ph /\ n e. NN ) -> ( 2 x. _pi ) e. RR ) |
180 |
|
0le2 |
|- 0 <_ 2 |
181 |
180
|
a1i |
|- ( ( ph /\ n e. NN ) -> 0 <_ 2 ) |
182 |
|
0re |
|- 0 e. RR |
183 |
|
pipos |
|- 0 < _pi |
184 |
182 177 183
|
ltleii |
|- 0 <_ _pi |
185 |
184
|
a1i |
|- ( ( ph /\ n e. NN ) -> 0 <_ _pi ) |
186 |
176 178 181 185
|
mulge0d |
|- ( ( ph /\ n e. NN ) -> 0 <_ ( 2 x. _pi ) ) |
187 |
12
|
nn0red |
|- ( ( ph /\ n e. NN ) -> n e. RR ) |
188 |
12
|
nn0ge0d |
|- ( ( ph /\ n e. NN ) -> 0 <_ n ) |
189 |
179 186 187 188
|
sqrtmuld |
|- ( ( ph /\ n e. NN ) -> ( sqrt ` ( ( 2 x. _pi ) x. n ) ) = ( ( sqrt ` ( 2 x. _pi ) ) x. ( sqrt ` n ) ) ) |
190 |
176 181 178 185
|
sqrtmuld |
|- ( ( ph /\ n e. NN ) -> ( sqrt ` ( 2 x. _pi ) ) = ( ( sqrt ` 2 ) x. ( sqrt ` _pi ) ) ) |
191 |
190
|
oveq1d |
|- ( ( ph /\ n e. NN ) -> ( ( sqrt ` ( 2 x. _pi ) ) x. ( sqrt ` n ) ) = ( ( ( sqrt ` 2 ) x. ( sqrt ` _pi ) ) x. ( sqrt ` n ) ) ) |
192 |
13
|
sqrtcld |
|- ( ( ph /\ n e. NN ) -> ( sqrt ` 2 ) e. CC ) |
193 |
18
|
sqrtcld |
|- ( ( ph /\ n e. NN ) -> ( sqrt ` n ) e. CC ) |
194 |
192 34 193
|
mulassd |
|- ( ( ph /\ n e. NN ) -> ( ( ( sqrt ` 2 ) x. ( sqrt ` _pi ) ) x. ( sqrt ` n ) ) = ( ( sqrt ` 2 ) x. ( ( sqrt ` _pi ) x. ( sqrt ` n ) ) ) ) |
195 |
192 34 193
|
mul12d |
|- ( ( ph /\ n e. NN ) -> ( ( sqrt ` 2 ) x. ( ( sqrt ` _pi ) x. ( sqrt ` n ) ) ) = ( ( sqrt ` _pi ) x. ( ( sqrt ` 2 ) x. ( sqrt ` n ) ) ) ) |
196 |
176 181 187 188
|
sqrtmuld |
|- ( ( ph /\ n e. NN ) -> ( sqrt ` ( 2 x. n ) ) = ( ( sqrt ` 2 ) x. ( sqrt ` n ) ) ) |
197 |
196
|
eqcomd |
|- ( ( ph /\ n e. NN ) -> ( ( sqrt ` 2 ) x. ( sqrt ` n ) ) = ( sqrt ` ( 2 x. n ) ) ) |
198 |
197
|
oveq2d |
|- ( ( ph /\ n e. NN ) -> ( ( sqrt ` _pi ) x. ( ( sqrt ` 2 ) x. ( sqrt ` n ) ) ) = ( ( sqrt ` _pi ) x. ( sqrt ` ( 2 x. n ) ) ) ) |
199 |
195 198
|
eqtrd |
|- ( ( ph /\ n e. NN ) -> ( ( sqrt ` 2 ) x. ( ( sqrt ` _pi ) x. ( sqrt ` n ) ) ) = ( ( sqrt ` _pi ) x. ( sqrt ` ( 2 x. n ) ) ) ) |
200 |
191 194 199
|
3eqtrd |
|- ( ( ph /\ n e. NN ) -> ( ( sqrt ` ( 2 x. _pi ) ) x. ( sqrt ` n ) ) = ( ( sqrt ` _pi ) x. ( sqrt ` ( 2 x. n ) ) ) ) |
201 |
189 200
|
eqtrd |
|- ( ( ph /\ n e. NN ) -> ( sqrt ` ( ( 2 x. _pi ) x. n ) ) = ( ( sqrt ` _pi ) x. ( sqrt ` ( 2 x. n ) ) ) ) |
202 |
201
|
oveq1d |
|- ( ( ph /\ n e. NN ) -> ( ( sqrt ` ( ( 2 x. _pi ) x. n ) ) x. ( ( n / _e ) ^ n ) ) = ( ( ( sqrt ` _pi ) x. ( sqrt ` ( 2 x. n ) ) ) x. ( ( n / _e ) ^ n ) ) ) |
203 |
202
|
oveq2d |
|- ( ( ph /\ n e. NN ) -> ( ( ! ` n ) / ( ( sqrt ` ( ( 2 x. _pi ) x. n ) ) x. ( ( n / _e ) ^ n ) ) ) = ( ( ! ` n ) / ( ( ( sqrt ` _pi ) x. ( sqrt ` ( 2 x. n ) ) ) x. ( ( n / _e ) ^ n ) ) ) ) |
204 |
91
|
adantl |
|- ( ( ph /\ n e. NN ) -> ( ! ` n ) e. CC ) |
205 |
94
|
adantl |
|- ( ( ph /\ n e. NN ) -> ( sqrt ` ( 2 x. n ) ) =/= 0 ) |
206 |
22
|
a1i |
|- ( ( ph /\ n e. NN ) -> _e e. CC ) |
207 |
25
|
a1i |
|- ( ( ph /\ n e. NN ) -> _e =/= 0 ) |
208 |
18 206 207
|
divcld |
|- ( ( ph /\ n e. NN ) -> ( n / _e ) e. CC ) |
209 |
95
|
adantl |
|- ( ( ph /\ n e. NN ) -> n =/= 0 ) |
210 |
18 206 209 207
|
divne0d |
|- ( ( ph /\ n e. NN ) -> ( n / _e ) =/= 0 ) |
211 |
63
|
adantl |
|- ( ( ph /\ n e. NN ) -> n e. ZZ ) |
212 |
208 210 211
|
expne0d |
|- ( ( ph /\ n e. NN ) -> ( ( n / _e ) ^ n ) =/= 0 ) |
213 |
38 29 205 212
|
mulne0d |
|- ( ( ph /\ n e. NN ) -> ( ( sqrt ` ( 2 x. n ) ) x. ( ( n / _e ) ^ n ) ) =/= 0 ) |
214 |
9
|
rpne0d |
|- ( ph -> C =/= 0 ) |
215 |
214
|
adantr |
|- ( ( ph /\ n e. NN ) -> C =/= 0 ) |
216 |
204 171 170 213 215
|
divdiv1d |
|- ( ( ph /\ n e. NN ) -> ( ( ( ! ` n ) / ( ( sqrt ` ( 2 x. n ) ) x. ( ( n / _e ) ^ n ) ) ) / C ) = ( ( ! ` n ) / ( ( ( sqrt ` ( 2 x. n ) ) x. ( ( n / _e ) ^ n ) ) x. C ) ) ) |
217 |
174 203 216
|
3eqtr4d |
|- ( ( ph /\ n e. NN ) -> ( ( ! ` n ) / ( ( sqrt ` ( ( 2 x. _pi ) x. n ) ) x. ( ( n / _e ) ^ n ) ) ) = ( ( ( ! ` n ) / ( ( sqrt ` ( 2 x. n ) ) x. ( ( n / _e ) ^ n ) ) ) / C ) ) |
218 |
99
|
ancli |
|- ( n e. NN -> ( n e. NN /\ ( ( ! ` n ) / ( ( sqrt ` ( 2 x. n ) ) x. ( ( n / _e ) ^ n ) ) ) e. CC ) ) |
219 |
218
|
adantl |
|- ( ( ph /\ n e. NN ) -> ( n e. NN /\ ( ( ! ` n ) / ( ( sqrt ` ( 2 x. n ) ) x. ( ( n / _e ) ^ n ) ) ) e. CC ) ) |
220 |
219 100
|
syl |
|- ( ( ph /\ n e. NN ) -> ( A ` n ) = ( ( ! ` n ) / ( ( sqrt ` ( 2 x. n ) ) x. ( ( n / _e ) ^ n ) ) ) ) |
221 |
220
|
eqcomd |
|- ( ( ph /\ n e. NN ) -> ( ( ! ` n ) / ( ( sqrt ` ( 2 x. n ) ) x. ( ( n / _e ) ^ n ) ) ) = ( A ` n ) ) |
222 |
221
|
oveq1d |
|- ( ( ph /\ n e. NN ) -> ( ( ( ! ` n ) / ( ( sqrt ` ( 2 x. n ) ) x. ( ( n / _e ) ^ n ) ) ) / C ) = ( ( A ` n ) / C ) ) |
223 |
33 217 222
|
3eqtrd |
|- ( ( ph /\ n e. NN ) -> ( ( ! ` n ) / ( S ` n ) ) = ( ( A ` n ) / C ) ) |
224 |
1 223
|
mpteq2da |
|- ( ph -> ( n e. NN |-> ( ( ! ` n ) / ( S ` n ) ) ) = ( n e. NN |-> ( ( A ` n ) / C ) ) ) |
225 |
102
|
adantl |
|- ( ( ph /\ n e. NN ) -> ( A ` n ) e. CC ) |
226 |
225 170 215
|
divrec2d |
|- ( ( ph /\ n e. NN ) -> ( ( A ` n ) / C ) = ( ( 1 / C ) x. ( A ` n ) ) ) |
227 |
1 226
|
mpteq2da |
|- ( ph -> ( n e. NN |-> ( ( A ` n ) / C ) ) = ( n e. NN |-> ( ( 1 / C ) x. ( A ` n ) ) ) ) |
228 |
146 214
|
reccld |
|- ( ph -> ( 1 / C ) e. CC ) |
229 |
82
|
mptex |
|- ( n e. NN |-> ( ( 1 / C ) x. ( A ` n ) ) ) e. _V |
230 |
229
|
a1i |
|- ( ph -> ( n e. NN |-> ( ( 1 / C ) x. ( A ` n ) ) ) e. _V ) |
231 |
3
|
a1i |
|- ( k e. NN -> A = ( n e. NN |-> ( ( ! ` n ) / ( ( sqrt ` ( 2 x. n ) ) x. ( ( n / _e ) ^ n ) ) ) ) ) |
232 |
|
simpr |
|- ( ( k e. NN /\ n = k ) -> n = k ) |
233 |
232
|
fveq2d |
|- ( ( k e. NN /\ n = k ) -> ( ! ` n ) = ( ! ` k ) ) |
234 |
232
|
oveq2d |
|- ( ( k e. NN /\ n = k ) -> ( 2 x. n ) = ( 2 x. k ) ) |
235 |
234
|
fveq2d |
|- ( ( k e. NN /\ n = k ) -> ( sqrt ` ( 2 x. n ) ) = ( sqrt ` ( 2 x. k ) ) ) |
236 |
232
|
oveq1d |
|- ( ( k e. NN /\ n = k ) -> ( n / _e ) = ( k / _e ) ) |
237 |
236 232
|
oveq12d |
|- ( ( k e. NN /\ n = k ) -> ( ( n / _e ) ^ n ) = ( ( k / _e ) ^ k ) ) |
238 |
235 237
|
oveq12d |
|- ( ( k e. NN /\ n = k ) -> ( ( sqrt ` ( 2 x. n ) ) x. ( ( n / _e ) ^ n ) ) = ( ( sqrt ` ( 2 x. k ) ) x. ( ( k / _e ) ^ k ) ) ) |
239 |
233 238
|
oveq12d |
|- ( ( k e. NN /\ n = k ) -> ( ( ! ` n ) / ( ( sqrt ` ( 2 x. n ) ) x. ( ( n / _e ) ^ n ) ) ) = ( ( ! ` k ) / ( ( sqrt ` ( 2 x. k ) ) x. ( ( k / _e ) ^ k ) ) ) ) |
240 |
|
id |
|- ( k e. NN -> k e. NN ) |
241 |
|
nnnn0 |
|- ( k e. NN -> k e. NN0 ) |
242 |
|
faccl |
|- ( k e. NN0 -> ( ! ` k ) e. NN ) |
243 |
|
nncn |
|- ( ( ! ` k ) e. NN -> ( ! ` k ) e. CC ) |
244 |
241 242 243
|
3syl |
|- ( k e. NN -> ( ! ` k ) e. CC ) |
245 |
|
2cnd |
|- ( k e. NN -> 2 e. CC ) |
246 |
|
nncn |
|- ( k e. NN -> k e. CC ) |
247 |
245 246
|
mulcld |
|- ( k e. NN -> ( 2 x. k ) e. CC ) |
248 |
247
|
sqrtcld |
|- ( k e. NN -> ( sqrt ` ( 2 x. k ) ) e. CC ) |
249 |
22
|
a1i |
|- ( k e. NN -> _e e. CC ) |
250 |
25
|
a1i |
|- ( k e. NN -> _e =/= 0 ) |
251 |
246 249 250
|
divcld |
|- ( k e. NN -> ( k / _e ) e. CC ) |
252 |
251 241
|
expcld |
|- ( k e. NN -> ( ( k / _e ) ^ k ) e. CC ) |
253 |
248 252
|
mulcld |
|- ( k e. NN -> ( ( sqrt ` ( 2 x. k ) ) x. ( ( k / _e ) ^ k ) ) e. CC ) |
254 |
55
|
a1i |
|- ( k e. NN -> 2 e. RR+ ) |
255 |
|
nnrp |
|- ( k e. NN -> k e. RR+ ) |
256 |
254 255
|
rpmulcld |
|- ( k e. NN -> ( 2 x. k ) e. RR+ ) |
257 |
256
|
sqrtgt0d |
|- ( k e. NN -> 0 < ( sqrt ` ( 2 x. k ) ) ) |
258 |
257
|
gt0ne0d |
|- ( k e. NN -> ( sqrt ` ( 2 x. k ) ) =/= 0 ) |
259 |
|
nnne0 |
|- ( k e. NN -> k =/= 0 ) |
260 |
246 249 259 250
|
divne0d |
|- ( k e. NN -> ( k / _e ) =/= 0 ) |
261 |
|
nnz |
|- ( k e. NN -> k e. ZZ ) |
262 |
251 260 261
|
expne0d |
|- ( k e. NN -> ( ( k / _e ) ^ k ) =/= 0 ) |
263 |
248 252 258 262
|
mulne0d |
|- ( k e. NN -> ( ( sqrt ` ( 2 x. k ) ) x. ( ( k / _e ) ^ k ) ) =/= 0 ) |
264 |
244 253 263
|
divcld |
|- ( k e. NN -> ( ( ! ` k ) / ( ( sqrt ` ( 2 x. k ) ) x. ( ( k / _e ) ^ k ) ) ) e. CC ) |
265 |
231 239 240 264
|
fvmptd |
|- ( k e. NN -> ( A ` k ) = ( ( ! ` k ) / ( ( sqrt ` ( 2 x. k ) ) x. ( ( k / _e ) ^ k ) ) ) ) |
266 |
265 264
|
eqeltrd |
|- ( k e. NN -> ( A ` k ) e. CC ) |
267 |
266
|
adantl |
|- ( ( ph /\ k e. NN ) -> ( A ` k ) e. CC ) |
268 |
|
nfcv |
|- F/_ k ( ( 1 / C ) x. ( A ` n ) ) |
269 |
|
nfcv |
|- F/_ n 1 |
270 |
|
nfcv |
|- F/_ n / |
271 |
|
nfcv |
|- F/_ n C |
272 |
269 270 271
|
nfov |
|- F/_ n ( 1 / C ) |
273 |
|
nfcv |
|- F/_ n x. |
274 |
|
nfcv |
|- F/_ n k |
275 |
49 274
|
nffv |
|- F/_ n ( A ` k ) |
276 |
272 273 275
|
nfov |
|- F/_ n ( ( 1 / C ) x. ( A ` k ) ) |
277 |
|
fveq2 |
|- ( n = k -> ( A ` n ) = ( A ` k ) ) |
278 |
277
|
oveq2d |
|- ( n = k -> ( ( 1 / C ) x. ( A ` n ) ) = ( ( 1 / C ) x. ( A ` k ) ) ) |
279 |
268 276 278
|
cbvmpt |
|- ( n e. NN |-> ( ( 1 / C ) x. ( A ` n ) ) ) = ( k e. NN |-> ( ( 1 / C ) x. ( A ` k ) ) ) |
280 |
279
|
a1i |
|- ( ( ph /\ k e. NN ) -> ( n e. NN |-> ( ( 1 / C ) x. ( A ` n ) ) ) = ( k e. NN |-> ( ( 1 / C ) x. ( A ` k ) ) ) ) |
281 |
280
|
fveq1d |
|- ( ( ph /\ k e. NN ) -> ( ( n e. NN |-> ( ( 1 / C ) x. ( A ` n ) ) ) ` k ) = ( ( k e. NN |-> ( ( 1 / C ) x. ( A ` k ) ) ) ` k ) ) |
282 |
|
simpr |
|- ( ( ph /\ k e. NN ) -> k e. NN ) |
283 |
146
|
adantr |
|- ( ( ph /\ k e. NN ) -> C e. CC ) |
284 |
214
|
adantr |
|- ( ( ph /\ k e. NN ) -> C =/= 0 ) |
285 |
283 284
|
reccld |
|- ( ( ph /\ k e. NN ) -> ( 1 / C ) e. CC ) |
286 |
285 267
|
mulcld |
|- ( ( ph /\ k e. NN ) -> ( ( 1 / C ) x. ( A ` k ) ) e. CC ) |
287 |
|
eqid |
|- ( k e. NN |-> ( ( 1 / C ) x. ( A ` k ) ) ) = ( k e. NN |-> ( ( 1 / C ) x. ( A ` k ) ) ) |
288 |
287
|
fvmpt2 |
|- ( ( k e. NN /\ ( ( 1 / C ) x. ( A ` k ) ) e. CC ) -> ( ( k e. NN |-> ( ( 1 / C ) x. ( A ` k ) ) ) ` k ) = ( ( 1 / C ) x. ( A ` k ) ) ) |
289 |
282 286 288
|
syl2anc |
|- ( ( ph /\ k e. NN ) -> ( ( k e. NN |-> ( ( 1 / C ) x. ( A ` k ) ) ) ` k ) = ( ( 1 / C ) x. ( A ` k ) ) ) |
290 |
281 289
|
eqtrd |
|- ( ( ph /\ k e. NN ) -> ( ( n e. NN |-> ( ( 1 / C ) x. ( A ` n ) ) ) ` k ) = ( ( 1 / C ) x. ( A ` k ) ) ) |
291 |
46 47 10 228 230 267 290
|
climmulc2 |
|- ( ph -> ( n e. NN |-> ( ( 1 / C ) x. ( A ` n ) ) ) ~~> ( ( 1 / C ) x. C ) ) |
292 |
146 214
|
recid2d |
|- ( ph -> ( ( 1 / C ) x. C ) = 1 ) |
293 |
291 292
|
breqtrd |
|- ( ph -> ( n e. NN |-> ( ( 1 / C ) x. ( A ` n ) ) ) ~~> 1 ) |
294 |
227 293
|
eqbrtrd |
|- ( ph -> ( n e. NN |-> ( ( A ` n ) / C ) ) ~~> 1 ) |
295 |
224 294
|
eqbrtrd |
|- ( ph -> ( n e. NN |-> ( ( ! ` n ) / ( S ` n ) ) ) ~~> 1 ) |