Mathbox for Glauco Siliprandi < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  etransclem23 Structured version   Visualization version   Unicode version

Theorem etransclem23 38122
 Description: This is the claim proof in [Juillerat] p. 14 (but in our proof, Stirling's approximation is not used). (Contributed by Glauco Siliprandi, 5-Apr-2020.)
Hypotheses
Ref Expression
etransclem23.a
etransclem23.l
etransclem23.k
etransclem23.p
etransclem23.m
etransclem23.f
etransclem23.lt1
Assertion
Ref Expression
etransclem23
Distinct variable groups:   ,,   ,,   ,,
Allowed substitution hints:   (,)   (,)   (,)   (,)

Proof of Theorem etransclem23
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 etransclem23.k . . . . . 6
2 etransclem23.l . . . . . . 7
32oveq1i 6300 . . . . . 6
41, 3eqtri 2473 . . . . 5
54fveq2i 5868 . . . 4
65a1i 11 . . 3
7 fzfid 12186 . . . . 5
8 etransclem23.a . . . . . . . . . 10
98adantr 467 . . . . . . . . 9
10 elfznn0 11887 . . . . . . . . . 10
1110adantl 468 . . . . . . . . 9
129, 11ffvelrnd 6023 . . . . . . . 8
1312zcnd 11041 . . . . . . 7
14 ere 14143 . . . . . . . . . 10
1514recni 9655 . . . . . . . . 9
1615a1i 11 . . . . . . . 8
17 elfzelz 11800 . . . . . . . . . 10
1817zcnd 11041 . . . . . . . . 9
1918adantl 468 . . . . . . . 8
2016, 19cxpcld 23653 . . . . . . 7
2113, 20mulcld 9663 . . . . . 6
2215a1i 11 . . . . . . . . 9
23 elioore 11666 . . . . . . . . . . . 12
2423recnd 9669 . . . . . . . . . . 11
2524adantl 468 . . . . . . . . . 10
2625negcld 9973 . . . . . . . . 9
2722, 26cxpcld 23653 . . . . . . . 8
28 ax-resscn 9596 . . . . . . . . . . . . 13
2928a1i 11 . . . . . . . . . . . 12
30 etransclem23.p . . . . . . . . . . . 12
31 etransclem23.f . . . . . . . . . . . 12
3229, 30, 31etransclem8 38107 . . . . . . . . . . 11
3332adantr 467 . . . . . . . . . 10
3423adantl 468 . . . . . . . . . 10
3533, 34ffvelrnd 6023 . . . . . . . . 9
3635adantlr 721 . . . . . . . 8
3727, 36mulcld 9663 . . . . . . 7
38 reelprrecn 9631 . . . . . . . . 9
3938a1i 11 . . . . . . . 8
40 reopn 37502 . . . . . . . . . 10
41 eqid 2451 . . . . . . . . . . 11 fld fld
4241tgioo2 21821 . . . . . . . . . 10 fldt
4340, 42eleqtri 2527 . . . . . . . . 9 fldt
4443a1i 11 . . . . . . . 8 fldt
4530adantr 467 . . . . . . . 8
46 etransclem23.m . . . . . . . . . 10
4746nnnn0d 10925 . . . . . . . . 9
4847adantr 467 . . . . . . . 8
49 etransclem6 38105 . . . . . . . . 9
50 etransclem6 38105 . . . . . . . . 9
5131, 49, 503eqtri 2477 . . . . . . . 8
52 0red 9644 . . . . . . . 8
5317zred 11040 . . . . . . . . 9
5453adantl 468 . . . . . . . 8
5539, 44, 45, 48, 51, 52, 54etransclem18 38117 . . . . . . 7
5637, 55itgcl 22741 . . . . . 6
5721, 56mulcld 9663 . . . . 5
587, 57fsumcl 13799 . . . 4
59 nnm1nn0 10911 . . . . . . 7
6030, 59syl 17 . . . . . 6
6160faccld 37533 . . . . 5
6261nncnd 10625 . . . 4
6361nnne0d 10654 . . . 4
6458, 62, 63absdivd 13517 . . 3
6561nnred 10624 . . . . 5
6661nnnn0d 10925 . . . . . 6
6766nn0ge0d 10928 . . . . 5
6865, 67absidd 13484 . . . 4
6968oveq2d 6306 . . 3
706, 64, 693eqtrd 2489 . 2
712, 58syl5eqel 2533 . . . . . . 7
7271, 62, 63divcld 10383 . . . . . 6
731, 72syl5eqel 2533 . . . . 5
7473abscld 13498 . . . 4
7570, 74eqeltrrd 2530 . . 3
7646nnred 10624 . . . . . . . . . . . . . . . 16
7730nnnn0d 10925 . . . . . . . . . . . . . . . 16
7876, 77reexpcld 12433 . . . . . . . . . . . . . . 15
79 peano2nn0 10910 . . . . . . . . . . . . . . . 16
8047, 79syl 17 . . . . . . . . . . . . . . 15
8178, 80reexpcld 12433 . . . . . . . . . . . . . 14
8281recnd 9669 . . . . . . . . . . . . 13
8346nncnd 10625 . . . . . . . . . . . . 13
8482, 83mulcomd 9664 . . . . . . . . . . . 12
8530nncnd 10625 . . . . . . . . . . . . . . . . 17
86 1cnd 9659 . . . . . . . . . . . . . . . . 17
8785, 86npcand 9990 . . . . . . . . . . . . . . . 16
8887eqcomd 2457 . . . . . . . . . . . . . . 15
8988oveq2d 6306 . . . . . . . . . . . . . 14
9080nn0cnd 10927 . . . . . . . . . . . . . . . . 17
9190, 85mulcomd 9664 . . . . . . . . . . . . . . . 16
9291oveq2d 6306 . . . . . . . . . . . . . . 15
9383, 77, 80expmuld 12419 . . . . . . . . . . . . . . 15
9483, 80, 77expmuld 12419 . . . . . . . . . . . . . . 15
9592, 93, 943eqtr3d 2493 . . . . . . . . . . . . . 14
9676, 80reexpcld 12433 . . . . . . . . . . . . . . . 16
9796recnd 9669 . . . . . . . . . . . . . . 15
9897, 60expp1d 12417 . . . . . . . . . . . . . 14
9989, 95, 983eqtr3d 2493 . . . . . . . . . . . . 13
10099oveq2d 6306 . . . . . . . . . . . 12
10197, 60expcld 12416 . . . . . . . . . . . . . 14
10283, 101, 97mul12d 9842 . . . . . . . . . . . . 13
10383, 97mulcld 9663 . . . . . . . . . . . . . 14
104101, 103mulcomd 9664 . . . . . . . . . . . . 13
105102, 104eqtrd 2485 . . . . . . . . . . . 12
10684, 100, 1053eqtrd 2489 . . . . . . . . . . 11
107106adantr 467 . . . . . . . . . 10
108107oveq2d 6306 . . . . . . . . 9
10921abscld 13498 . . . . . . . . . . 11
110109recnd 9669 . . . . . . . . . 10
111103adantr 467 . . . . . . . . . 10
112101adantr 467 . . . . . . . . . 10
113110, 111, 112mulassd 9666 . . . . . . . . 9
114108, 113eqtr4d 2488 . . . . . . . 8
115114sumeq2dv 13769 . . . . . . 7
116110, 111mulcld 9663 . . . . . . . 8
1177, 101, 116fsummulc1 13846 . . . . . . 7
118115, 117eqtr4d 2488 . . . . . 6
119118oveq1d 6305 . . . . 5
1207, 116fsumcl 13799 . . . . . 6
121120, 101, 62, 63divassd 10418 . . . . 5
122119, 121eqtrd 2485 . . . 4
12381adantr 467 . . . . . . . 8
12476adantr 467 . . . . . . . 8
125123, 124remulcld 9671 . . . . . . 7
126109, 125remulcld 9671 . . . . . 6
1277, 126fsumrecl 13800 . . . . 5
128127, 61nndivred 10658 . . . 4
129122, 128eqeltrrd 2530 . . 3
130 1red 9658 . . 3
13158abscld 13498 . . . . 5
13261nnrpd 11339 . . . . 5
13357abscld 13498 . . . . . . 7
1347, 133fsumrecl 13800 . . . . . 6
1357, 57fsumabs 13861 . . . . . 6
13681ad2antrr 732 . . . . . . . . . 10
137 ioombl 22518 . . . . . . . . . . . 12
138137a1i 11 . . . . . . . . . . 11
139 0red 9644 . . . . . . . . . . . . . 14
140 elfzle1 11802 . . . . . . . . . . . . . 14
141 volioo 37825 . . . . . . . . . . . . . 14
142139, 53, 140, 141syl3anc 1268 . . . . . . . . . . . . 13
14353, 139resubcld 10047 . . . . . . . . . . . . 13
144142, 143eqeltrd 2529 . . . . . . . . . . . 12
145144adantl 468 . . . . . . . . . . 11
14682adantr 467 . . . . . . . . . . 11
147 iblconstmpt 37832 . . . . . . . . . . 11
148138, 145, 146, 147syl3anc 1268 . . . . . . . . . 10
149136, 148itgrecl 22755 . . . . . . . . 9
150109, 149remulcld 9671 . . . . . . . 8
1517, 150fsumrecl 13800 . . . . . . 7
15221, 56absmuld 13516 . . . . . . . . 9
15356abscld 13498 . . . . . . . . . 10
15421absge0d 13506 . . . . . . . . . 10
15537abscld 13498 . . . . . . . . . . . 12
15637, 55iblabs 22786 . . . . . . . . . . . 12
157155, 156itgrecl 22755 . . . . . . . . . . 11
15837, 55itgabs 22792 . . . . . . . . . . 11
15927, 36absmuld 13516 . . . . . . . . . . . . 13
16027abscld 13498 . . . . . . . . . . . . . . 15
161 1red 9658 . . . . . . . . . . . . . . 15
16236abscld 13498 . . . . . . . . . . . . . . 15
16327absge0d 13506 . . . . . . . . . . . . . . 15
16436absge0d 13506 . . . . . . . . . . . . . . 15
16514a1i 11 . . . . . . . . . . . . . . . . . . . 20
166 0re 9643 . . . . . . . . . . . . . . . . . . . . . 22
167 epos 14259 . . . . . . . . . . . . . . . . . . . . . 22
168166, 14, 167ltleii 9757 . . . . . . . . . . . . . . . . . . . . 21
169168a1i 11 . . . . . . . . . . . . . . . . . . . 20
17023renegcld 10046 . . . . . . . . . . . . . . . . . . . 20
171165, 169, 170recxpcld 23668 . . . . . . . . . . . . . . . . . . 19
172165, 169, 170cxpge0d 23669 . . . . . . . . . . . . . . . . . . 19
173171, 172absidd 13484 . . . . . . . . . . . . . . . . . 18
174173adantl 468 . . . . . . . . . . . . . . . . 17
175171adantl 468 . . . . . . . . . . . . . . . . . 18
176 1red 9658 . . . . . . . . . . . . . . . . . 18
177 0xr 9687 . . . . . . . . . . . . . . . . . . . . . . 23
178177a1i 11 . . . . . . . . . . . . . . . . . . . . . 22
17953rexrd 9690 . . . . . . . . . . . . . . . . . . . . . . 23
180179adantr 467 . . . . . . . . . . . . . . . . . . . . . 22
181 simpr 463 . . . . . . . . . . . . . . . . . . . . . 22
182 ioogtlb 37592 . . . . . . . . . . . . . . . . . . . . . 22
183178, 180, 181, 182syl3anc 1268 . . . . . . . . . . . . . . . . . . . . 21
18423adantl 468 . . . . . . . . . . . . . . . . . . . . . 22
185184lt0neg2d 10184 . . . . . . . . . . . . . . . . . . . . 21
186183, 185mpbid 214 . . . . . . . . . . . . . . . . . . . 20
18714a1i 11 . . . . . . . . . . . . . . . . . . . . 21
188 1lt2 10776 . . . . . . . . . . . . . . . . . . . . . . 23
189 egt2lt3 14258 . . . . . . . . . . . . . . . . . . . . . . . 24
190189simpli 460 . . . . . . . . . . . . . . . . . . . . . . 23
191 1re 9642 . . . . . . . . . . . . . . . . . . . . . . . 24
192 2re 10679 . . . . . . . . . . . . . . . . . . . . . . . 24
193191, 192, 14lttri 9760 . . . . . . . . . . . . . . . . . . . . . . 23
194188, 190, 193mp2an 678 . . . . . . . . . . . . . . . . . . . . . 22
195194a1i 11 . . . . . . . . . . . . . . . . . . . . 21
196170adantl 468 . . . . . . . . . . . . . . . . . . . . 21
197 0red 9644 . . . . . . . . . . . . . . . . . . . . 21
198187, 195, 196, 197cxpltd 23664 . . . . . . . . . . . . . . . . . . . 20
199186, 198mpbid 214 . . . . . . . . . . . . . . . . . . 19
200 cxp0 23615 . . . . . . . . . . . . . . . . . . . 20
20115, 200mp1i 13 . . . . . . . . . . . . . . . . . . 19
202199, 201breqtrd 4427 . . . . . . . . . . . . . . . . . 18
203175, 176, 202ltled 9783 . . . . . . . . . . . . . . . . 17
204174, 203eqbrtrd 4423 . . . . . . . . . . . . . . . 16
205204adantll 720 . . . . . . . . . . . . . . 15
20628a1i 11 . . . . . . . . . . . . . . . . . . 19
20730ad2antrr 732 . . . . . . . . . . . . . . . . . . 19
20847ad2antrr 732 . . . . . . . . . . . . . . . . . . 19
20931, 49eqtri 2473 . . . . . . . . . . . . . . . . . . 19
21023adantl 468 . . . . . . . . . . . . . . . . . . 19
211206, 207, 208, 209, 210etransclem13 38112 . . . . . . . . . . . . . . . . . 18
212211fveq2d 5869 . . . . . . . . . . . . . . . . 17
213 nn0uz 11193 . . . . . . . . . . . . . . . . . 18
21423adantr 467 . . . . . . . . . . . . . . . . . . . . . 22
215 nn0re 10878 . . . . . . . . . . . . . . . . . . . . . . 23
216215adantl 468 . . . . . . . . . . . . . . . . . . . . . 22
217214, 216resubcld 10047 . . . . . . . . . . . . . . . . . . . . 21
218217adantll 720 . . . . . . . . . . . . . . . . . . . 20
21960, 77ifcld 3924 . . . . . . . . . . . . . . . . . . . . 21
220219ad3antrrr 736 . . . . . . . . . . . . . . . . . . . 20
221218, 220reexpcld 12433 . . . . . . . . . . . . . . . . . . 19
222221recnd 9669 . . . . . . . . . . . . . . . . . 18
223213, 208, 222fprodabs 14028 . . . . . . . . . . . . . . . . 17
224 elfznn0 11887 . . . . . . . . . . . . . . . . . . . 20
22524adantr 467 . . . . . . . . . . . . . . . . . . . . . 22
226 nn0cn 10879 . . . . . . . . . . . . . . . . . . . . . . 23
227226adantl 468 . . . . . . . . . . . . . . . . . . . . . 22
228225, 227subcld 9986 . . . . . . . . . . . . . . . . . . . . 21
229228adantll 720 . . . . . . . . . . . . . . . . . . . 20
230224, 229sylan2 477 . . . . . . . . . . . . . . . . . . 19
231219ad3antrrr 736 . . . . . . . . . . . . . . . . . . 19
232230, 231absexpd 13514 . . . . . . . . . . . . . . . . . 18
233232prodeq2dv 13977 . . . . . . . . . . . . . . . . 17
234212, 223, 2333eqtrd 2489 . . . . . . . . . . . . . . . 16
235 nfv 1761 . . . . . . . . . . . . . . . . . 18
236 fzfid 12186 . . . . . . . . . . . . . . . . . 18
237224, 228sylan2 477 . . . . . . . . . . . . . . . . . . . . 21
238237abscld 13498 . . . . . . . . . . . . . . . . . . . 20
239238adantll 720 . . . . . . . . . . . . . . . . . . 19
240239, 231reexpcld 12433 . . . . . . . . . . . . . . . . . 18
241237absge0d 13506 . . . . . . . . . . . . . . . . . . . 20
242241adantll 720 . . . . . . . . . . . . . . . . . . 19
243239, 231, 242expge0d 12434 . . . . . . . . . . . . . . . . . 18
24478ad3antrrr 736 . . . . . . . . . . . . . . . . . 18
24576ad3antrrr 736 . . . . . . . . . . . . . . . . . . . 20
246245, 231reexpcld 12433 . . . . . . . . . . . . . . . . . . 19
247224, 218sylan2 477 . . . . . . . . . . . . . . . . . . . . . 22
24824adantr 467 . . . . . . . . . . . . . . . . . . . . . . . . 25
249224, 227sylan2 477 . . . . . . . . . . . . . . . . . . . . . . . . 25
250248, 249negsubdi2d 10002 . . . . . . . . . . . . . . . . . . . . . . . 24
251250adantll 720 . . . . . . . . . . . . . . . . . . . . . . 23
252224adantl 468 . . . . . . . . . . . . . . . . . . . . . . . . . 26
253252nn0red 10926 . . . . . . . . . . . . . . . . . . . . . . . . 25
254 0red 9644 . . . . . . . . . . . . . . . . . . . . . . . . 25
255210adantr 467 . . . . . . . . . . . . . . . . . . . . . . . . 25
256 elfzle2 11803 . . . . . . . . . . . . . . . . . . . . . . . . . 26
257256adantl 468 . . . . . . . . . . . . . . . . . . . . . . . . 25
258197, 184, 183ltled 9783 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
259258adantll 720 . . . . . . . . . . . . . . . . . . . . . . . . . 26
260259adantr 467 . . . . . . . . . . . . . . . . . . . . . . . . 25
261253, 254, 245, 255, 257, 260le2subd 10233 . . . . . . . . . . . . . . . . . . . . . . . 24
26283subid1d 9975 . . . . . . . . . . . . . . . . . . . . . . . . 25
263262ad3antrrr 736 . . . . . . . . . . . . . . . . . . . . . . . 24
264261, 263breqtrd 4427 . . . . . . . . . . . . . . . . . . . . . . 23
265251, 264eqbrtrd 4423 . . . . . . . . . . . . . . . . . . . . . 22
266247, 245, 265lenegcon1d 10195 . . . . . . . . . . . . . . . . . . . . 21
267 elfzel2 11798 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
268267zred 11040 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
269268adantr 467 . . . . . . . . . . . . . . . . . . . . . . . . . 26
27053adantr 467 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
271 iooltub 37610 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
272178, 180, 181, 271syl3anc 1268 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
273 elfzle2 11803 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
274273adantr 467 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
275184, 270, 269, 272, 274ltletrd 9795 . . . . . . . . . . . . . . . . . . . . . . . . . 26
276184, 269, 275ltled 9783 . . . . . . . . . . . . . . . . . . . . . . . . 25
277276adantll 720 . . . . . . . . . . . . . . . . . . . . . . . 24
278277adantr 467 . . . . . . . . . . . . . . . . . . . . . . 23
279252nn0ge0d 10928 . . . . . . . . . . . . . . . . . . . . . . 23
280255, 254, 245, 253, 278, 279le2subd 10233 . . . . . . . . . . . . . . . . . . . . . 22
281280, 263breqtrd 4427 . . . . . . . . . . . . . . . . . . . . 21
282247, 245absled 13492 . . . . . . . . . . . . . . . . . . . . 21
283266, 281, 282mpbir2and 933 . . . . . . . . . . . . . . . . . . . 20
284 leexp1a 12331 . . . . . . . . . . . . . . . . . . . 20
285239, 245, 231, 242, 283, 284syl32anc 1276 . . . . . . . . . . . . . . . . . . 19
28646nnge1d 10652 . . . . . . . . . . . . . . . . . . . . 21
287286ad3antrrr 736 . . . . . . . . . . . . . . . . . . . 20
288219nn0zd 11038 . . . . . . . . . . . . . . . . . . . . . 22
28977nn0zd 11038 . . . . . . . . . . . . . . . . . . . . . 22
290 iftrue 3887 . . . . . . . . . . . . . . . . . . . . . . . . 25
291290adantl 468 . . . . . . . . . . . . . . . . . . . . . . . 24
29230nnred 10624 . . . . . . . . . . . . . . . . . . . . . . . . . 26
293292lem1d 10540 . . . . . . . . . . . . . . . . . . . . . . . . 25
294293adantr 467 . . . . . . . . . . . . . . . . . . . . . . . 24
295291, 294eqbrtrd 4423 . . . . . . . . . . . . . . . . . . . . . . 23
296 iffalse 3890 . . . . . . . . . . . . . . . . . . . . . . . . 25
297296adantl 468 . . . . . . . . . . . . . . . . . . . . . . . 24
298292leidd 10180 . . . . . . . . . . . . . . . . . . . . . . . . 25
299298adantr 467 . . . . . . . . . . . . . . . . . . . . . . . 24
300297, 299eqbrtrd 4423 . . . . . . . . . . . . . . . . . . . . . . 23
301295, 300pm2.61dan 800 . . . . . . . . . . . . . . . . . . . . . 22
302 eluz2 11165 . . . . . . . . . . . . . . . . . . . . . 22
303288, 289, 301, 302syl3anbrc 1192 . . . . . . . . . . . . . . . . . . . . 21
304303ad3antrrr 736 . . . . . . . . . . . . . . . . . . . 20
305245, 287, 304leexp2ad 12448 . . . . . . . . . . . . . . . . . . 19
306240, 246, 244, 285, 305letrd 9792 . . . . . . . . . . . . . . . . . 18
307235, 236, 240, 243, 244, 306fprodle 14050 . . . . . . . . . . . . . . . . 17
30878recnd 9669 . . . . . . . . . . . . . . . . . . . 20
309 fprodconst 14032 . . . . . . . . . . . . . . . . . . . 20
3107, 308, 309syl2anc 667 . . . . . . . . . . . . . . . . . . 19
311 hashfz0 12604 . . . . . . . . . . . . . . . . . . . . 21
31247, 311syl 17 . . . . . . . . . . . . . . . . . . . 20
313312oveq2d 6306 . . . . . . . . . . . . . . . . . . 19
314310, 313eqtrd 2485 . . . . . . . . . . . . . . . . . 18
315314ad2antrr 732 . . . . . . . . . . . . . . . . 17
316307, 315breqtrd 4427 . . . . . . . . . . . . . . . 16
317234, 316eqbrtrd 4423 . . . . . . . . . . . . . . 15
318160, 161, 162, 136, 163, 164, 205, 317lemul12ad 10549 . . . . . . . . . . . . . 14
31982mulid2d 9661 . . . . . . . . . . . . . . 15
320319ad2antrr 732 . . . . . . . . . . . . . 14
321318, 320breqtrd 4427 . . . . . . . . . . . . 13
322159, 321eqbrtrd 4423 . . . . . . . . . . . 12
323156, 148, 155, 136, 322itgle 22767 . . . . . . . . . . 11
324153, 157, 149, 158, 323letrd 9792 . . . . . . . . . 10
325153, 149, 109, 154, 324lemul2ad 10547 . . . . . . . . 9
326152, 325eqbrtrd 4423 . . . . . . . 8
3277, 133, 150, 326fsumle 13859 . . . . . . 7
328 itgconst 22776 . . . . . . . . . . 11
329138, 145, 146, 328syl3anc 1268 . . . . . . . . . 10
33047nn0ge0d 10928 . . . . . . . . . . . . . 14
33176, 77, 330expge0d 12434 . . . . . . . . . . . . 13
33278, 80, 331expge0d 12434 . . . . . . . . . . . 12
333332adantr 467 . . . . . . . . . . 11
33418subid1d 9975 . . . . . . . . . . . . . 14
335142, 334eqtrd 2485 . . . . . . . . . . . . 13
336335, 273eqbrtrd 4423 . . . . . . . . . . . 12
337336adantl 468 . . . . . . . . . . 11
338145, 124, 123, 333, 337lemul2ad 10547 . . . . . . . . . 10
339329, 338eqbrtrd 4423 . . . . . . . . 9
340149, 125, 109, 154, 339lemul2ad 10547 . . . . . . . 8
3417, 150, 126, 340fsumle 13859 . . . . . . 7
342134, 151, 127, 327, 341letrd 9792 . . . . . 6
343131, 134, 127, 135, 342letrd 9792 . . . . 5
344131, 127, 132, 343lediv1dd 11396 . . . 4
345344, 122breqtrd 4427 . . 3
346 etransclem23.lt1 . . 3
34775, 129, 130, 345, 346lelttrd 9793 . 2
34870, 347eqbrtrd 4423 1
 Colors of variables: wff setvar class Syntax hints:   wn 3   wi 4   wa 371   wceq 1444   wcel 1887   wss 3404  cif 3881  cpr 3970   class class class wbr 4402   cmpt 4461   cdm 4834   crn 4835  wf 5578  cfv 5582  (class class class)co 6290  cfn 7569  cc 9537  cr 9538  cc0 9539  c1 9540   caddc 9542   cmul 9544  cxr 9674   clt 9675   cle 9676   cmin 9860  cneg 9861   cdiv 10269  cn 10609  c2 10659  c3 10660  cn0 10869  cz 10937  cuz 11159  cioo 11635  cfz 11784  cexp 12272  cfa 12459  chash 12515  cabs 13297  csu 13752  cprod 13959  ceu 14115   ↾t crest 15319  ctopn 15320  ctg 15336  ℂfldccnfld 18970  cvol 22415  cibl 22575  citg 22576   ccxp 23505 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-8 1889  ax-9 1896  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091  ax-ext 2431  ax-rep 4515  ax-sep 4525  ax-nul 4534  ax-pow 4581  ax-pr 4639  ax-un 6583  ax-inf2 8146  ax-cc 8865  ax-cnex 9595  ax-resscn 9596  ax-1cn 9597  ax-icn 9598  ax-addcl 9599  ax-addrcl 9600  ax-mulcl 9601  ax-mulrcl 9602  ax-mulcom 9603  ax-addass 9604  ax-mulass 9605  ax-distr 9606  ax-i2m1 9607  ax-1ne0 9608  ax-1rid 9609  ax-rnegex 9610  ax-rrecex 9611  ax-cnre 9612  ax-pre-lttri 9613  ax-pre-lttrn 9614  ax-pre-ltadd 9615  ax-pre-mulgt0 9616  ax-pre-sup 9617  ax-addf 9618  ax-mulf 9619 This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3or 986  df-3an 987  df-tru 1447  df-fal 1450  df-ex 1664  df-nf 1668  df-sb 1798  df-eu 2303  df-mo 2304  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2581  df-ne 2624  df-nel 2625  df-ral 2742  df-rex 2743  df-reu 2744  df-rmo 2745  df-rab 2746  df-v 3047  df-sbc 3268  df-csb 3364  df-dif 3407  df-un 3409  df-in 3411  df-ss 3418  df-pss 3420  df-nul 3732  df-if 3882  df-pw 3953  df-sn 3969  df-pr 3971  df-tp 3973  df-op 3975  df-uni 4199  df-int 4235  df-iun 4280  df-iin 4281  df-disj 4374  df-br 4403  df-opab 4462  df-mpt 4463  df-tr 4498  df-eprel 4745  df-id 4749  df-po 4755  df-so 4756  df-fr 4793  df-se 4794  df-we 4795  df-xp 4840  df-rel 4841  df-cnv 4842  df-co 4843  df-dm 4844  df-rn 4845  df-res 4846  df-ima 4847  df-pred 5380  df-ord 5426  df-on 5427  df-lim 5428  df-suc 5429  df-iota 5546  df-fun 5584  df-fn 5585  df-f 5586  df-f1 5587  df-fo 5588  df-f1o 5589  df-fv 5590  df-isom 5591  df-riota 6252  df-ov 6293  df-oprab 6294  df-mpt2 6295  df-of 6531  df-ofr 6532  df-om 6693  df-1st 6793  df-2nd 6794  df-supp 6915  df-wrecs 7028  df-recs 7090  df-rdg 7128  df-1o 7182  df-2o 7183  df-oadd 7186  df-omul 7187  df-er 7363  df-map 7474  df-pm 7475  df-ixp 7523  df-en 7570  df-dom 7571  df-sdom 7572  df-fin 7573  df-fsupp 7884  df-fi 7925  df-sup 7956  df-inf 7957  df-oi 8025  df-card 8373  df-acn 8376  df-cda 8598  df-pnf 9677  df-mnf 9678  df-xr 9679  df-ltxr 9680  df-le 9681  df-sub 9862  df-neg 9863  df-div 10270  df-nn 10610  df-2 10668  df-3 10669  df-4 10670  df-5 10671  df-6 10672  df-7 10673  df-8 10674  df-9 10675  df-10 10676  df-n0 10870  df-z 10938  df-dec 11052  df-uz 11160  df-q 11265  df-rp 11303  df-xneg 11409  df-xadd 11410  df-xmul 11411  df-ioo 11639  df-ioc 11640  df-ico 11641  df-icc 11642  df-fz 11785  df-fzo 11916  df-fl 12028  df-mod 12097  df-seq 12214  df-exp 12273  df-fac 12460  df-bc 12488  df-hash 12516  df-shft 13130  df-cj 13162  df-re 13163  df-im 13164  df-sqrt 13298  df-abs 13299  df-limsup 13526  df-clim 13552  df-rlim 13553  df-sum 13753  df-prod 13960  df-ef 14121  df-e 14122  df-sin 14123  df-cos 14124  df-tan 14125  df-pi 14126  df-struct 15123  df-ndx 15124  df-slot 15125  df-base 15126  df-sets 15127  df-ress 15128  df-plusg 15203  df-mulr 15204  df-starv 15205  df-sca 15206  df-vsca 15207  df-ip 15208  df-tset 15209  df-ple 15210  df-ds 15212  df-unif 15213  df-hom 15214  df-cco 15215  df-rest 15321  df-topn 15322  df-0g 15340  df-gsum 15341  df-topgen 15342  df-pt 15343  df-prds 15346  df-xrs 15400  df-qtop 15406  df-imas 15407  df-xps 15410  df-mre 15492  df-mrc 15493  df-acs 15495  df-mgm 16488  df-sgrp 16527  df-mnd 16537  df-submnd 16583  df-mulg 16676  df-cntz 16971  df-cmn 17432  df-psmet 18962  df-xmet 18963  df-met 18964  df-bl 18965  df-mopn 18966  df-fbas 18967  df-fg 18968  df-cnfld 18971  df-top 19921  df-bases 19922  df-topon 19923  df-topsp 19924  df-cld 20034  df-ntr 20035  df-cls 20036  df-nei 20114  df-lp 20152  df-perf 20153  df-cn 20243  df-cnp 20244  df-haus 20331  df-cmp 20402  df-tx 20577  df-hmeo 20770  df-fil 20861  df-fm 20953  df-flim 20954  df-flf 20955  df-xms 21335  df-ms 21336  df-tms 21337  df-cncf 21910  df-ovol 22416  df-vol 22418  df-mbf 22577  df-itg1 22578  df-itg2 22579  df-ibl 22580  df-itg 22581  df-0p 22628  df-limc 22821  df-dv 22822  df-log 23506  df-cxp 23507 This theorem is referenced by:  etransclem47  38146
 Copyright terms: Public domain W3C validator