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

Theorem etransclem46 38257
 Description: This is the proof for equation *(7) in [Juillerat] p. 12. The proven equality will lead to a contradiction, because the left-hand side goes to for large , but the right-hand side is a non-zero integer. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
Hypotheses
Ref Expression
etransclem46.q Poly
etransclem46.qe0
etransclem46.a coeff
etransclem46.m deg
etransclem46.rex
etransclem46.s
etransclem46.x fldt
etransclem46.p
etransclem46.f
etransclem46.l
etransclem46.r
etransclem46.g
etransclem46.h
Assertion
Ref Expression
etransclem46
Distinct variable groups:   ,,,   ,,,,   ,,   ,,,,   ,   ,,,   ,   ,,,,   ,,,,
Allowed substitution hints:   ()   ()   (,,)   (,)   (,,,)   (,,)

Proof of Theorem etransclem46
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 etransclem46.l . . . 4
21a1i 11 . . 3
3 etransclem46.h . . . . . . . . . . . . . 14
43oveq2i 6319 . . . . . . . . . . . . 13
54a1i 11 . . . . . . . . . . . 12
6 etransclem46.s . . . . . . . . . . . . . 14
76adantr 472 . . . . . . . . . . . . 13
8 ere 14220 . . . . . . . . . . . . . . . . . . . 20
98recni 9673 . . . . . . . . . . . . . . . . . . 19
109a1i 11 . . . . . . . . . . . . . . . . . 18
11 recn 9647 . . . . . . . . . . . . . . . . . . 19
1211negcld 9992 . . . . . . . . . . . . . . . . . 18
1310, 12cxpcld 23732 . . . . . . . . . . . . . . . . 17
1413adantl 473 . . . . . . . . . . . . . . . 16
15 simpr 468 . . . . . . . . . . . . . . . . . 18
16 fzfid 12224 . . . . . . . . . . . . . . . . . . 19
17 elfznn0 11913 . . . . . . . . . . . . . . . . . . . . . 22
186adantr 472 . . . . . . . . . . . . . . . . . . . . . . 23
19 etransclem46.x . . . . . . . . . . . . . . . . . . . . . . . 24 fldt
2019adantr 472 . . . . . . . . . . . . . . . . . . . . . . 23 fldt
21 etransclem46.p . . . . . . . . . . . . . . . . . . . . . . . 24
2221adantr 472 . . . . . . . . . . . . . . . . . . . . . . 23
23 etransclem46.m . . . . . . . . . . . . . . . . . . . . . . . . 25 deg
24 etransclem46.q . . . . . . . . . . . . . . . . . . . . . . . . . . 27 Poly
2524eldifad 3402 . . . . . . . . . . . . . . . . . . . . . . . . . 26 Poly
26 dgrcl 23266 . . . . . . . . . . . . . . . . . . . . . . . . . 26 Poly deg
2725, 26syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 deg
2823, 27syl5eqel 2553 . . . . . . . . . . . . . . . . . . . . . . . 24
2928adantr 472 . . . . . . . . . . . . . . . . . . . . . . 23
30 etransclem46.f . . . . . . . . . . . . . . . . . . . . . . 23
31 simpr 468 . . . . . . . . . . . . . . . . . . . . . . 23
3218, 20, 22, 29, 30, 31etransclem33 38244 . . . . . . . . . . . . . . . . . . . . . 22
3317, 32sylan2 482 . . . . . . . . . . . . . . . . . . . . 21
3433adantlr 729 . . . . . . . . . . . . . . . . . . . 20
35 simplr 770 . . . . . . . . . . . . . . . . . . . 20
3634, 35ffvelrnd 6038 . . . . . . . . . . . . . . . . . . 19
3716, 36fsumcl 13876 . . . . . . . . . . . . . . . . . 18
38 etransclem46.g . . . . . . . . . . . . . . . . . . 19
3938fvmpt2 5972 . . . . . . . . . . . . . . . . . 18
4015, 37, 39syl2anc 673 . . . . . . . . . . . . . . . . 17
4140, 37eqeltrd 2549 . . . . . . . . . . . . . . . 16
4214, 41mulcld 9681 . . . . . . . . . . . . . . 15
4342negcld 9992 . . . . . . . . . . . . . 14
4443adantlr 729 . . . . . . . . . . . . 13
456, 19dvdmsscn 37908 . . . . . . . . . . . . . . . . . . 19
4645, 21, 30etransclem8 38219 . . . . . . . . . . . . . . . . . 18
4746ffvelrnda 6037 . . . . . . . . . . . . . . . . 17
4814, 47mulcld 9681 . . . . . . . . . . . . . . . 16
4948negcld 9992 . . . . . . . . . . . . . . 15
5049negcld 9992 . . . . . . . . . . . . . 14
5150adantlr 729 . . . . . . . . . . . . 13
528a1i 11 . . . . . . . . . . . . . . . . . . . 20
53 0re 9661 . . . . . . . . . . . . . . . . . . . . . 22
54 epos 14336 . . . . . . . . . . . . . . . . . . . . . 22
5553, 8, 54ltleii 9775 . . . . . . . . . . . . . . . . . . . . 21
5655a1i 11 . . . . . . . . . . . . . . . . . . . 20
57 renegcl 9957 . . . . . . . . . . . . . . . . . . . 20
5852, 56, 57recxpcld 23747 . . . . . . . . . . . . . . . . . . 19
5958renegcld 10067 . . . . . . . . . . . . . . . . . 18
6059adantl 473 . . . . . . . . . . . . . . . . 17
61 reelprrecn 9649 . . . . . . . . . . . . . . . . . . . . . 22
6261a1i 11 . . . . . . . . . . . . . . . . . . . . 21
63 cnelprrecn 9650 . . . . . . . . . . . . . . . . . . . . . 22
6463a1i 11 . . . . . . . . . . . . . . . . . . . . 21
6512adantl 473 . . . . . . . . . . . . . . . . . . . . 21
66 neg1rr 10736 . . . . . . . . . . . . . . . . . . . . . 22
6766a1i 11 . . . . . . . . . . . . . . . . . . . . 21
689a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23
69 id 22 . . . . . . . . . . . . . . . . . . . . . . 23
7068, 69cxpcld 23732 . . . . . . . . . . . . . . . . . . . . . 22
7170adantl 473 . . . . . . . . . . . . . . . . . . . . 21
7211adantl 473 . . . . . . . . . . . . . . . . . . . . . 22
73 1red 9676 . . . . . . . . . . . . . . . . . . . . . 22
7462dvmptid 22990 . . . . . . . . . . . . . . . . . . . . . 22
7562, 72, 73, 74dvmptneg 22999 . . . . . . . . . . . . . . . . . . . . 21
76 epr 14337 . . . . . . . . . . . . . . . . . . . . . . . 24
77 dvcxp2 23760 . . . . . . . . . . . . . . . . . . . . . . . 24
7876, 77ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . 23
79 loge 23615 . . . . . . . . . . . . . . . . . . . . . . . . . 26
8079oveq1i 6318 . . . . . . . . . . . . . . . . . . . . . . . . 25
8170mulid2d 9679 . . . . . . . . . . . . . . . . . . . . . . . . 25
8280, 81syl5eq 2517 . . . . . . . . . . . . . . . . . . . . . . . 24
8382mpteq2ia 4478 . . . . . . . . . . . . . . . . . . . . . . 23
8478, 83eqtri 2493 . . . . . . . . . . . . . . . . . . . . . 22
8584a1i 11 . . . . . . . . . . . . . . . . . . . . 21
86 oveq2 6316 . . . . . . . . . . . . . . . . . . . . 21
8762, 64, 65, 67, 71, 71, 75, 85, 86, 86dvmptco 23005 . . . . . . . . . . . . . . . . . . . 20
8887trud 1461 . . . . . . . . . . . . . . . . . . 19
8966a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23
9089recnd 9687 . . . . . . . . . . . . . . . . . . . . . 22
9113, 90mulcomd 9682 . . . . . . . . . . . . . . . . . . . . 21
9213mulm1d 10091 . . . . . . . . . . . . . . . . . . . . 21
9391, 92eqtrd 2505 . . . . . . . . . . . . . . . . . . . 20
9493mpteq2ia 4478 . . . . . . . . . . . . . . . . . . 19
9588, 94eqtri 2493 . . . . . . . . . . . . . . . . . 18
9695a1i 11 . . . . . . . . . . . . . . . . 17
9717adantl 473 . . . . . . . . . . . . . . . . . . . . . 22
98 peano2nn0 10934 . . . . . . . . . . . . . . . . . . . . . 22
9997, 98syl 17 . . . . . . . . . . . . . . . . . . . . 21
100 ovex 6336 . . . . . . . . . . . . . . . . . . . . . 22
101 eleq1 2537 . . . . . . . . . . . . . . . . . . . . . . . 24
102101anbi2d 718 . . . . . . . . . . . . . . . . . . . . . . 23
103 fveq2 5879 . . . . . . . . . . . . . . . . . . . . . . . 24
104103feq1d 5724 . . . . . . . . . . . . . . . . . . . . . . 23
105102, 104imbi12d 327 . . . . . . . . . . . . . . . . . . . . . 22
106 eleq1 2537 . . . . . . . . . . . . . . . . . . . . . . . . 25
107106anbi2d 718 . . . . . . . . . . . . . . . . . . . . . . . 24
108 fveq2 5879 . . . . . . . . . . . . . . . . . . . . . . . . 25
109108feq1d 5724 . . . . . . . . . . . . . . . . . . . . . . . 24
110107, 109imbi12d 327 . . . . . . . . . . . . . . . . . . . . . . 23
111110, 32chvarv 2120 . . . . . . . . . . . . . . . . . . . . . 22
112100, 105, 111vtocl 3086 . . . . . . . . . . . . . . . . . . . . 21
11399, 112syldan 478 . . . . . . . . . . . . . . . . . . . 20
114113adantlr 729 . . . . . . . . . . . . . . . . . . 19
115114, 35ffvelrnd 6038 . . . . . . . . . . . . . . . . . 18
11616, 115fsumcl 13876 . . . . . . . . . . . . . . . . 17
11721, 28, 30, 38etransclem39 38250 . . . . . . . . . . . . . . . . . . . . 21
118117feqmptd 5932 . . . . . . . . . . . . . . . . . . . 20
119118eqcomd 2477 . . . . . . . . . . . . . . . . . . 19
120119oveq2d 6324 . . . . . . . . . . . . . . . . . 18
121 nfcv 2612 . . . . . . . . . . . . . . . . . . 19
122 elfznn0 11913 . . . . . . . . . . . . . . . . . . . 20
123122, 32sylan2 482 . . . . . . . . . . . . . . . . . . 19
124121, 46, 123, 38etransclem2 38213 . . . . . . . . . . . . . . . . . 18
125120, 124eqtrd 2505 . . . . . . . . . . . . . . . . 17
1266, 14, 60, 96, 41, 116, 125dvmptmul 22994 . . . . . . . . . . . . . . . 16
127116, 14mulcomd 9682 . . . . . . . . . . . . . . . . . . 19
128127oveq2d 6324 . . . . . . . . . . . . . . . . . 18
12914negcld 9992 . . . . . . . . . . . . . . . . . . . 20
130129, 41mulcld 9681 . . . . . . . . . . . . . . . . . . 19
13114, 116mulcld 9681 . . . . . . . . . . . . . . . . . . 19
132130, 131addcomd 9853 . . . . . . . . . . . . . . . . . 18
133131, 42negsubd 10011 . . . . . . . . . . . . . . . . . . . 20
13414, 41mulneg1d 10092 . . . . . . . . . . . . . . . . . . . . 21
135134oveq2d 6324 . . . . . . . . . . . . . . . . . . . 20
136116, 41, 14subdir2d 37617 . . . . . . . . . . . . . . . . . . . 20
137133, 135, 1363eqtr4d 2515 . . . . . . . . . . . . . . . . . . 19
13840oveq2d 6324 . . . . . . . . . . . . . . . . . . . . 21
13916, 115, 36fsumsub 13926 . . . . . . . . . . . . . . . . . . . . 21
140 fveq2 5879 . . . . . . . . . . . . . . . . . . . . . . 23
141140fveq1d 5881 . . . . . . . . . . . . . . . . . . . . . 22
142103fveq1d 5881 . . . . . . . . . . . . . . . . . . . . . 22
143 fveq2 5879 . . . . . . . . . . . . . . . . . . . . . . 23
144143fveq1d 5881 . . . . . . . . . . . . . . . . . . . . . 22
145 fveq2 5879 . . . . . . . . . . . . . . . . . . . . . . 23
146145fveq1d 5881 . . . . . . . . . . . . . . . . . . . . . 22
147 etransclem46.r . . . . . . . . . . . . . . . . . . . . . . . . 25
14821nnnn0d 10949 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
14928, 148nn0mulcld 10954 . . . . . . . . . . . . . . . . . . . . . . . . . 26
150 nnm1nn0 10935 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
15121, 150syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26
152149, 151nn0addcld 10953 . . . . . . . . . . . . . . . . . . . . . . . . 25
153147, 152syl5eqel 2553 . . . . . . . . . . . . . . . . . . . . . . . 24
154153adantr 472 . . . . . . . . . . . . . . . . . . . . . . 23
155154nn0zd 11061 . . . . . . . . . . . . . . . . . . . . . 22
156 peano2nn0 10934 . . . . . . . . . . . . . . . . . . . . . . . . 25
157153, 156syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24
158 nn0uz 11217 . . . . . . . . . . . . . . . . . . . . . . . 24
159157, 158syl6eleq 2559 . . . . . . . . . . . . . . . . . . . . . . 23
160159adantr 472 . . . . . . . . . . . . . . . . . . . . . 22
161 elfznn0 11913 . . . . . . . . . . . . . . . . . . . . . . . . 25
162161, 111sylan2 482 . . . . . . . . . . . . . . . . . . . . . . . 24
163162adantlr 729 . . . . . . . . . . . . . . . . . . . . . . 23
164 simplr 770 . . . . . . . . . . . . . . . . . . . . . . 23
165163, 164ffvelrnd 6038 . . . . . . . . . . . . . . . . . . . . . 22
166141, 142, 144, 146, 155, 160, 165telfsum2 13942 . . . . . . . . . . . . . . . . . . . . 21
167138, 139, 1663eqtr2d 2511 . . . . . . . . . . . . . . . . . . . 20
168167oveq2d 6324 . . . . . . . . . . . . . . . . . . 19
169153nn0red 10950 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
170169ltp1d 10559 . . . . . . . . . . . . . . . . . . . . . . . . . 26
171147, 170syl5eqbrr 4430 . . . . . . . . . . . . . . . . . . . . . . . . 25
172 etransclem5 38216 . . . . . . . . . . . . . . . . . . . . . . . . 25
1736, 19, 21, 28, 30, 157, 171, 172etransclem32 38243 . . . . . . . . . . . . . . . . . . . . . . . 24
174173fveq1d 5881 . . . . . . . . . . . . . . . . . . . . . . 23
175 eqid 2471 . . . . . . . . . . . . . . . . . . . . . . . . 25
176175fvmpt2 5972 . . . . . . . . . . . . . . . . . . . . . . . 24
17753, 176mpan2 685 . . . . . . . . . . . . . . . . . . . . . . 23
178174, 177sylan9eq 2525 . . . . . . . . . . . . . . . . . . . . . 22
179 cnex 9638 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
180179a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . 26
181 etransclem46.rex . . . . . . . . . . . . . . . . . . . . . . . . . . 27
1826, 181ssexd 4543 . . . . . . . . . . . . . . . . . . . . . . . . . 26
183 elpm2r 7507 . . . . . . . . . . . . . . . . . . . . . . . . . 26
184180, 182, 46, 181, 183syl22anc 1293 . . . . . . . . . . . . . . . . . . . . . . . . 25
185 dvn0 22957 . . . . . . . . . . . . . . . . . . . . . . . . 25
18645, 184, 185syl2anc 673 . . . . . . . . . . . . . . . . . . . . . . . 24
187186fveq1d 5881 . . . . . . . . . . . . . . . . . . . . . . 23
188187adantr 472 . . . . . . . . . . . . . . . . . . . . . 22
189178, 188oveq12d 6326 . . . . . . . . . . . . . . . . . . . . 21
190 df-neg 9883 . . . . . . . . . . . . . . . . . . . . 21
191189, 190syl6eqr 2523 . . . . . . . . . . . . . . . . . . . 20
192191oveq2d 6324 . . . . . . . . . . . . . . . . . . 19
193137, 168, 1923eqtrd 2509 . . . . . . . . . . . . . . . . . 18
194128, 132, 1933eqtrd 2509 . . . . . . . . . . . . . . . . 17
195194mpteq2dva 4482 . . . . . . . . . . . . . . . 16
19614, 47mulneg2d 10093 . . . . . . . . . . . . . . . . 17
197196mpteq2dva 4482 . . . . . . . . . . . . . . . 16
198126, 195, 1973eqtrd 2509 . . . . . . . . . . . . . . 15
1996, 42, 49, 198dvmptneg 22999 . . . . . . . . . . . . . 14
200199adantr 472 . . . . . . . . . . . . 13
201 0red 9662 . . . . . . . . . . . . . 14
202 elfzelz 11826 . . . . . . . . . . . . . . . 16
203202zred 11063 . . . . . . . . . . . . . . 15
204203adantl 473 . . . . . . . . . . . . . 14
205201, 204iccssred 37698 . . . . . . . . . . . . 13
206 eqid 2471 . . . . . . . . . . . . . 14 fld fld
207206tgioo2 21899 . . . . . . . . . . . . 13 fldt
208 0red 9662 . . . . . . . . . . . . . . 15
209 iccntr 21917 . . . . . . . . . . . . . . 15
210208, 203, 209syl2anc 673 . . . . . . . . . . . . . 14
211210adantl 473 . . . . . . . . . . . . 13
2127, 44, 51, 200, 205, 207, 206, 211dvmptres2 22995 . . . . . . . . . . . 12
2139a1i 11 . . . . . . . . . . . . . . . . 17
214 elioore 11691 . . . . . . . . . . . . . . . . . . . 20
215214recnd 9687 . . . . . . . . . . . . . . . . . . 19
216215adantl 473 . . . . . . . . . . . . . . . . . 18
217216negcld 9992 . . . . . . . . . . . . . . . . 17
218213, 217cxpcld 23732 . . . . . . . . . . . . . . . 16
21946adantr 472 . . . . . . . . . . . . . . . . 17
220214adantl 473 . . . . . . . . . . . . . . . . 17
221219, 220ffvelrnd 6038 . . . . . . . . . . . . . . . 16
222218, 221mulcld 9681 . . . . . . . . . . . . . . 15
223222negnegd 9996 . . . . . . . . . . . . . 14
224223mpteq2dva 4482 . . . . . . . . . . . . 13
225224adantr 472 . . . . . . . . . . . 12
2265, 212, 2253eqtrd 2509 . . . . . . . . . . 11
227226fveq1d 5881 . . . . . . . . . 10
228227adantr 472 . . . . . . . . 9
229 simpr 468 . . . . . . . . . . 11
230 eqid 2471 . . . . . . . . . . . 12
231230fvmpt2 5972 . . . . . . . . . . 11
232229, 222, 231syl2anc 673 . . . . . . . . . 10
233232adantlr 729 . . . . . . . . 9
234228, 233eqtr2d 2506 . . . . . . . 8
235234itgeq2d 37957 . . . . . . 7
236 elfzle1 11828 . . . . . . . . 9
237236adantl 473 . . . . . . . 8
238 eqid 2471 . . . . . . . . . 10
239 eqidd 2472 . . . . . . . . . . . . . . . 16
24086adantl 473 . . . . . . . . . . . . . . . 16
241208, 203iccssred 37698 . . . . . . . . . . . . . . . . . . 19
242 ax-resscn 9614 . . . . . . . . . . . . . . . . . . 19
243241, 242syl6ss 3430 . . . . . . . . . . . . . . . . . 18
244243sselda 3418 . . . . . . . . . . . . . . . . 17
245244negcld 9992 . . . . . . . . . . . . . . . 16
2469a1i 11 . . . . . . . . . . . . . . . . . 18
247 negcl 9895 . . . . . . . . . . . . . . . . . 18
248246, 247cxpcld 23732 . . . . . . . . . . . . . . . . 17
249244, 248syl 17 . . . . . . . . . . . . . . . 16
250239, 240, 245, 249fvmptd 5969 . . . . . . . . . . . . . . 15
251250eqcomd 2477 . . . . . . . . . . . . . 14
252251adantll 728 . . . . . . . . . . . . 13
253252mpteq2dva 4482 . . . . . . . . . . . 12
254 mnfxr 11437 . . . . . . . . . . . . . . . . . 18
255254a1i 11 . . . . . . . . . . . . . . . . 17
256 0red 9662 . . . . . . . . . . . . . . . . 17
257 rpxr 11332 . . . . . . . . . . . . . . . . 17
258 rpgt0 11336 . . . . . . . . . . . . . . . . 17
259255, 256, 257, 258gtnelioc 37683 . . . . . . . . . . . . . . . 16
26076, 259ax-mp 5 . . . . . . . . . . . . . . 15
261 eldif 3400 . . . . . . . . . . . . . . 15
2629, 260, 261mpbir2an 934 . . . . . . . . . . . . . 14
263 cxpcncf2 37875 . . . . . . . . . . . . . 14
264262, 263mp1i 13 . . . . . . . . . . . . 13
265 eqid 2471 . . . . . . . . . . . . . . . 16
266265negcncf 22028 . . . . . . . . . . . . . . 15
267243, 266syl 17 . . . . . . . . . . . . . 14
268267adantl 473 . . . . . . . . . . . . 13
269264, 268cncfmpt1f 22023 . . . . . . . . . . . 12
270253, 269eqeltrd 2549 . . . . . . . . . . 11
271242a1i 11 . . . . . . . . . . . . . 14
27221ad2antrr 740 . . . . . . . . . . . . . 14
27328ad2antrr 740 . . . . . . . . . . . . . 14
274 etransclem6 38217 . . . . . . . . . . . . . . 15
27530, 274eqtri 2493 . . . . . . . . . . . . . 14
276241sselda 3418 . . . . . . . . . . . . . . 15
277276adantll 728 . . . . . . . . . . . . . 14
278271, 272, 273, 275, 277etransclem13 38224 . . . . . . . . . . . . 13
279278mpteq2dva 4482 . . . . . . . . . . . 12
280243adantl 473 . . . . . . . . . . . . 13
281 fzfid 12224 . . . . . . . . . . . . 13
282277recnd 9687 . . . . . . . . . . . . . . . 16
2832823adant3 1050 . . . . . . . . . . . . . . 15
284 elfzelz 11826 . . . . . . . . . . . . . . . . 17
285284zcnd 11064 . . . . . . . . . . . . . . . 16
2862853ad2ant3 1053 . . . . . . . . . . . . . . 15
287283, 286subcld 10005 . . . . . . . . . . . . . 14
28821adantr 472 . . . . . . . . . . . . . . . . . 18
289288, 150syl 17 . . . . . . . . . . . . . . . . 17
290148adantr 472 . . . . . . . . . . . . . . . . 17
291289, 290ifcld 3915 . . . . . . . . . . . . . . . 16
2922913adant3 1050 . . . . . . . . . . . . . . 15
2932923adant1r 1285 . . . . . . . . . . . . . 14
294287, 293expcld 12454 . . . . . . . . . . . . 13
295 nfv 1769 . . . . . . . . . . . . . 14
296243adantr 472 . . . . . . . . . . . . . . . . 17
297 ssid 3437 . . . . . . . . . . . . . . . . . 18
298297a1i 11 . . . . . . . . . . . . . . . . 17
299296, 298idcncfg 37846 . . . . . . . . . . . . . . . 16
300285adantl 473 . . . . . . . . . . . . . . . . 17
301296, 300, 298constcncfg 37845 . . . . . . . . . . . . . . . 16
302299, 301subcncf 37843 . . . . . . . . . . . . . . 15
303302adantll 728 . . . . . . . . . . . . . 14
304151, 148ifcld 3915 . . . . . . . . . . . . . . . 16
305 expcncf 22032 . . . . . . . . . . . . . . . 16
306304, 305syl 17 . . . . . . . . . . . . . . 15
307306ad2antrr 740 . . . . . . . . . . . . . 14
308297a1i 11 . . . . . . . . . . . . . 14
309 oveq1 6315 . . . . . . . . . . . . . 14
310295, 303, 307, 308, 309cncfcompt2 37874 . . . . . . . . . . . . 13
311280, 281, 294, 310fprodcncf 37876 . . . . . . . . . . . 12
312279, 311eqeltrd 2549 . . . . . . . . . . 11
313270, 312mulcncf 22476 . . . . . . . . . 10
314 ioossicc 11745 . . . . . . . . . . 11
315314a1i 11 . . . . . . . . . 10
316297a1i 11 . . . . . . . . . 10
317222adantlr 729 . . . . . . . . . 10
318238, 313, 315, 316, 317cncfmptssg 37844 . . . . . . . . 9
319226, 318eqeltrd 2549 . . . . . . . 8
32019adantr 472 . . . . . . . . . 10 fldt
32121adantr 472 . . . . . . . . . 10
32228adantr 472 . . . . . . . . . 10
323 oveq2 6316 . . . . . . . . . . . . . . 15
324323oveq1d 6323 . . . . . . . . . . . . . 14
325324cbvprodv 14047 . . . . . . . . . . . . 13
326325oveq2i 6319 . . . . . . . . . . . 12
327326mpteq2i 4479 . . . . . . . . . . 11
32830, 327eqtri 2493 . . . . . . . . . 10
3297, 320, 321, 322, 328, 201, 204etransclem18 38229 . . . . . . . . 9
330226, 329eqeltrd 2549 . . . . . . . 8
331 eqid 2471 . . . . . . . . . . . 12
3326, 19, 21, 28, 30, 38etransclem43 38254 . . . . . . . . . . . . . 14
333119, 332eqeltrd 2549 . . . . . . . . . . . . 13
334333adantr 472 . . . . . . . . . . . 12
335117ad2antrr 740 . . . . . . . . . . . . 13
336335, 277ffvelrnd 6038 . . . . . . . . . . . 12
337331, 334, 205, 316, 336cncfmptssg 37844 . . . . . . . . . . 11
338270, 337mulcncf 22476 . . . . . . . . . 10
339338negcncfg 37855 . . . . . . . . 9
3403, 339syl5eqel 2553 . . . . . . . 8
341201, 204, 237, 319, 330, 340ftc2 23075 . . . . . . 7
3423a1i 11 . . . . . . . . . 10
343 negeq 9887 . . . . . . . . . . . . . 14
344343oveq2d 6324 . . . . . . . . . . . . 13
345 fveq2 5879 . . . . . . . . . . . . 13
346344, 345oveq12d 6326 . . . . . . . . . . . 12
347346negeqd 9889 . . . . . . . . . . 11
348347adantl 473 . . . . . . . . . 10
349201rexrd 9708 . . . . . . . . . . 11
350204rexrd 9708 . . . . . . . . . . 11
351 ubicc2 11775 . . . . . . . . . . 11
352349, 350, 237, 351syl3anc 1292 . . . . . . . . . 10
3539a1i 11 . . . . . . . . . . . . . 14
354203recnd 9687 . . . . . . . . . . . . . . 15
355354negcld 9992 . . . . . . . . . . . . . 14
356353, 355cxpcld 23732 . . . . . . . . . . . . 13
357356adantl 473 . . . . . . . . . . . 12
358117adantr 472 . . . . . . . . . . . . 13
359358, 204ffvelrnd 6038 . . . . . . . . . . . 12
360357, 359mulcld 9681 . . . . . . . . . . 11
361360negcld 9992 . . . . . . . . . 10
362342, 348, 352, 361fvmptd 5969 . . . . . . . . 9
363 negeq 9887 . . . . . . . . . . . . . . . 16
364363oveq2d 6324 . . . . . . . . . . . . . . 15
365 neg0 9940 . . . . . . . . . . . . . . . . 17
366365oveq2i 6319 . . . . . . . . . . . . . . . 16
367 cxp0 23694 . . . . . . . . . . . . . . . . 17
3689, 367ax-mp 5 . . . . . . . . . . . . . . . 16
369366, 368eqtri 2493 . . . . . . . . . . . . . . 15
370364, 369syl6eq 2521 . . . . . . . . . . . . . 14
371 fveq2 5879 . . . . . . . . . . . . . 14
372370, 371oveq12d 6326 . . . . . . . . . . . . 13
373 0red 9662 . . . . . . . . . . . . . . 15
374117, 373ffvelrnd 6038 . . . . . . . . . . . . . 14
375374mulid2d 9679 . . . . . . . . . . . . 13
376372, 375sylan9eqr 2527 . . . . . . . . . . . 12
377376negeqd 9889 . . . . . . . . . . 11
378377adantlr 729 . . . . . . . . . 10
379 lbicc2 11774 . . . . . . . . . . 11
380349, 350, 237, 379syl3anc 1292 . . . . . . . . . 10
381374negcld 9992 . . . . . . . . . . 11
382381adantr 472 . . . . . . . . . 10
383342, 378, 380, 382fvmptd 5969 . . . . . . . . 9
384362, 383oveq12d 6326 . . . . . . . 8
385374adantr 472 . . . . . . . . 9
386361, 385subnegd 10012 . . . . . . . 8
387361, 385addcomd 9853 . . . . . . . . 9
388385, 360negsubd 10011 . . . . . . . . 9
389387, 388eqtrd 2505 . . . . . . . 8
390384, 386, 3893eqtrd 2509 . . . . . . 7
391235, 341, 3903eqtrd 2509 . . . . . 6
392391oveq2d 6324 . . . . 5
39325adantr 472 . . . . . . . . . 10 Poly
394 0zd 10973 . . . . . . . . . 10
395 etransclem46.a . . . . . . . . . . 11 coeff
396395coef2 23264 . . . . . . . . . 10 Poly
397393, 394, 396syl2anc 673 . . . . . . . . 9
398 elfznn0 11913 . . . . . . . . . 10
399398adantl 473 . . . . . . . . 9
400397, 399ffvelrnd 6038 . . . . . . . 8
401400zcnd 11064 . . . . . . 7
402353, 354cxpcld 23732 . . . . . . . 8
403402adantl 473 . . . . . . 7
404401, 403mulcld 9681 . . . . . 6
405404, 385, 360subdid 10095 . . . . 5
406392, 405eqtrd 2505 . . . 4
407406sumeq2dv 13846 . . 3
408 fzfid 12224 . . . . 5
409404, 385mulcld 9681 . . . . 5
410404, 360mulcld 9681 . . . . 5
411408, 409, 410fsumsub 13926 . . . 4
412 etransclem46.qe0 . . . . . . . . 9
413412eqcomd 2477 . . . . . . . 8
414395, 23coeid2 23272 . . . . . . . . 9 Poly
41525, 9, 414sylancl 675 . . . . . . . 8
416 cxpexp 23692 . . . . . . . . . . . . 13
417353, 398, 416syl2anc 673 . . . . . . . . . . . 12
418417eqcomd 2477 . . . . . . . . . . 11
419418oveq2d 6324 . . . . . . . . . 10
420419adantl 473 . . . . . . . . 9
421420sumeq2dv 13846 . . . . . . . 8
422413, 415, 4213eqtrd 2509 . . . . . . 7
423422oveq1d 6323 . . . . . 6
424374mul02d 9849 . . . . . 6
425408, 374, 404fsummulc1 13923 . . . . . 6
426423, 424, 4253eqtr3rd 2514 . . . . 5
42738a1i 11 . . . . . . . . . . 11
428 fveq2 5879 . . . . . . . . . . . . 13
429428sumeq2sdv 13847 . . . . . . . . . . . 12
430429adantl 473 . . . . . . . . . . 11
431 fzfid 12224 . . . . . . . . . . . 12
43233adantlr 729 . . . . . . . . . . . . 13
433204adantr 472 . . . . . . . . . . . . 13
434432, 433ffvelrnd 6038 . . . . . . . . . . . 12
435431, 434fsumcl 13876 . . . . . . . . . . 11
436427, 430, 204, 435fvmptd 5969 . . . . . . . . . 10
437436oveq2d 6324 . . . . . . . . 9
438437oveq2d 6324 . . . . . . . 8
439357, 435mulcld 9681 . . . . . . . . 9
440401, 403, 439mulassd 9684 . . . . . . . 8
441368eqcomi 2480 . . . . . . . . . . . . . . 15
442441a1i 11 . . . . . . . . . . . . . 14
443354negidd 9995 . . . . . . . . . . . . . . . 16
444443eqcomd 2477 . . . . . . . . . . . . . . 15
445444oveq2d 6324 . . . . . . . . . . . . . 14
44653, 54gtneii 9764 . . . . . . . . . . . . . . . 16
447446a1i 11 . . . . . . . . . . . . . . 15
448353, 447, 354, 355cxpaddd 23741 . . . . . . . . . . . . . 14
449442, 445, 4483eqtrd 2509 . . . . . . . . . . . . 13
450449oveq1d 6323 . . . . . . . . . . . 12
451450adantl 473 . . . . . . . . . . 11
452435mulid2d 9679 . . . . . . . . . . 11
453403, 357, 435mulassd 9684 . . . . . . . . . . 11
454451, 452, 4533eqtr3rd 2514 . . . . . . . . . 10