Step | Hyp | Ref
| Expression |
1 | | etransclem23.k |
. . . . . 6
|
2 | | etransclem23.l |
. . . . . . 7
|
3 | 2 | oveq1i 6660 |
. . . . . 6
|
4 | 1, 3 | eqtri 2644 |
. . . . 5
|
5 | 4 | fveq2i 6194 |
. . . 4
|
6 | 5 | a1i 11 |
. . 3
|
7 | | fzfid 12772 |
. . . . 5
|
8 | | etransclem23.a |
. . . . . . . . . 10
|
9 | 8 | adantr 481 |
. . . . . . . . 9
|
10 | | elfznn0 12433 |
. . . . . . . . . 10
|
11 | 10 | adantl 482 |
. . . . . . . . 9
|
12 | 9, 11 | ffvelrnd 6360 |
. . . . . . . 8
|
13 | 12 | zcnd 11483 |
. . . . . . 7
|
14 | | ere 14819 |
. . . . . . . . . 10
|
15 | 14 | recni 10052 |
. . . . . . . . 9
|
16 | 15 | a1i 11 |
. . . . . . . 8
|
17 | | elfzelz 12342 |
. . . . . . . . . 10
|
18 | 17 | zcnd 11483 |
. . . . . . . . 9
|
19 | 18 | adantl 482 |
. . . . . . . 8
|
20 | 16, 19 | cxpcld 24454 |
. . . . . . 7
|
21 | 13, 20 | mulcld 10060 |
. . . . . 6
|
22 | 15 | a1i 11 |
. . . . . . . . 9
|
23 | | elioore 12205 |
. . . . . . . . . . . 12
|
24 | 23 | recnd 10068 |
. . . . . . . . . . 11
|
25 | 24 | adantl 482 |
. . . . . . . . . 10
|
26 | 25 | negcld 10379 |
. . . . . . . . 9
|
27 | 22, 26 | cxpcld 24454 |
. . . . . . . 8
|
28 | | ax-resscn 9993 |
. . . . . . . . . . . . 13
|
29 | 28 | a1i 11 |
. . . . . . . . . . . 12
|
30 | | etransclem23.p |
. . . . . . . . . . . 12
|
31 | | etransclem23.f |
. . . . . . . . . . . 12
|
32 | 29, 30, 31 | etransclem8 40459 |
. . . . . . . . . . 11
|
33 | 32 | adantr 481 |
. . . . . . . . . 10
|
34 | 23 | adantl 482 |
. . . . . . . . . 10
|
35 | 33, 34 | ffvelrnd 6360 |
. . . . . . . . 9
|
36 | 35 | adantlr 751 |
. . . . . . . 8
|
37 | 27, 36 | mulcld 10060 |
. . . . . . 7
|
38 | | reelprrecn 10028 |
. . . . . . . . 9
|
39 | 38 | a1i 11 |
. . . . . . . 8
|
40 | | reopn 39501 |
. . . . . . . . . 10
|
41 | | eqid 2622 |
. . . . . . . . . . 11
ℂfld ℂfld |
42 | 41 | tgioo2 22606 |
. . . . . . . . . 10
ℂfld
↾t |
43 | 40, 42 | eleqtri 2699 |
. . . . . . . . 9
ℂfld
↾t |
44 | 43 | a1i 11 |
. . . . . . . 8
ℂfld
↾t |
45 | 30 | adantr 481 |
. . . . . . . 8
|
46 | | etransclem23.m |
. . . . . . . . . 10
|
47 | 46 | nnnn0d 11351 |
. . . . . . . . 9
|
48 | 47 | adantr 481 |
. . . . . . . 8
|
49 | | etransclem6 40457 |
. . . . . . . . 9
|
50 | | etransclem6 40457 |
. . . . . . . . 9
|
51 | 31, 49, 50 | 3eqtri 2648 |
. . . . . . . 8
|
52 | | 0red 10041 |
. . . . . . . 8
|
53 | 17 | zred 11482 |
. . . . . . . . 9
|
54 | 53 | adantl 482 |
. . . . . . . 8
|
55 | 39, 44, 45, 48, 51, 52, 54 | etransclem18 40469 |
. . . . . . 7
|
56 | 37, 55 | itgcl 23550 |
. . . . . 6
|
57 | 21, 56 | mulcld 10060 |
. . . . 5
|
58 | 7, 57 | fsumcl 14464 |
. . . 4
|
59 | | nnm1nn0 11334 |
. . . . . . 7
|
60 | 30, 59 | syl 17 |
. . . . . 6
|
61 | 60 | faccld 13071 |
. . . . 5
|
62 | 61 | nncnd 11036 |
. . . 4
|
63 | 61 | nnne0d 11065 |
. . . 4
|
64 | 58, 62, 63 | absdivd 14194 |
. . 3
|
65 | 61 | nnred 11035 |
. . . . 5
|
66 | 61 | nnnn0d 11351 |
. . . . . 6
|
67 | 66 | nn0ge0d 11354 |
. . . . 5
|
68 | 65, 67 | absidd 14161 |
. . . 4
|
69 | 68 | oveq2d 6666 |
. . 3
|
70 | 6, 64, 69 | 3eqtrd 2660 |
. 2
|
71 | 2, 58 | syl5eqel 2705 |
. . . . . . 7
|
72 | 71, 62, 63 | divcld 10801 |
. . . . . 6
|
73 | 1, 72 | syl5eqel 2705 |
. . . . 5
|
74 | 73 | abscld 14175 |
. . . 4
|
75 | 70, 74 | eqeltrrd 2702 |
. . 3
|
76 | 46 | nnred 11035 |
. . . . . . . . . . . . . . . 16
|
77 | 30 | nnnn0d 11351 |
. . . . . . . . . . . . . . . 16
|
78 | 76, 77 | reexpcld 13025 |
. . . . . . . . . . . . . . 15
|
79 | | peano2nn0 11333 |
. . . . . . . . . . . . . . . 16
|
80 | 47, 79 | syl 17 |
. . . . . . . . . . . . . . 15
|
81 | 78, 80 | reexpcld 13025 |
. . . . . . . . . . . . . 14
|
82 | 81 | recnd 10068 |
. . . . . . . . . . . . 13
|
83 | 46 | nncnd 11036 |
. . . . . . . . . . . . 13
|
84 | 82, 83 | mulcomd 10061 |
. . . . . . . . . . . 12
|
85 | 30 | nncnd 11036 |
. . . . . . . . . . . . . . . . 17
|
86 | | 1cnd 10056 |
. . . . . . . . . . . . . . . . 17
|
87 | 85, 86 | npcand 10396 |
. . . . . . . . . . . . . . . 16
|
88 | 87 | eqcomd 2628 |
. . . . . . . . . . . . . . 15
|
89 | 88 | oveq2d 6666 |
. . . . . . . . . . . . . 14
|
90 | 80 | nn0cnd 11353 |
. . . . . . . . . . . . . . . . 17
|
91 | 90, 85 | mulcomd 10061 |
. . . . . . . . . . . . . . . 16
|
92 | 91 | oveq2d 6666 |
. . . . . . . . . . . . . . 15
|
93 | 83, 77, 80 | expmuld 13011 |
. . . . . . . . . . . . . . 15
|
94 | 83, 80, 77 | expmuld 13011 |
. . . . . . . . . . . . . . 15
|
95 | 92, 93, 94 | 3eqtr3d 2664 |
. . . . . . . . . . . . . 14
|
96 | 76, 80 | reexpcld 13025 |
. . . . . . . . . . . . . . . 16
|
97 | 96 | recnd 10068 |
. . . . . . . . . . . . . . 15
|
98 | 97, 60 | expp1d 13009 |
. . . . . . . . . . . . . 14
|
99 | 89, 95, 98 | 3eqtr3d 2664 |
. . . . . . . . . . . . 13
|
100 | 99 | oveq2d 6666 |
. . . . . . . . . . . 12
|
101 | 97, 60 | expcld 13008 |
. . . . . . . . . . . . . 14
|
102 | 83, 101, 97 | mul12d 10245 |
. . . . . . . . . . . . 13
|
103 | 83, 97 | mulcld 10060 |
. . . . . . . . . . . . . 14
|
104 | 101, 103 | mulcomd 10061 |
. . . . . . . . . . . . 13
|
105 | 102, 104 | eqtrd 2656 |
. . . . . . . . . . . 12
|
106 | 84, 100, 105 | 3eqtrd 2660 |
. . . . . . . . . . 11
|
107 | 106 | adantr 481 |
. . . . . . . . . 10
|
108 | 107 | oveq2d 6666 |
. . . . . . . . 9
|
109 | 21 | abscld 14175 |
. . . . . . . . . . 11
|
110 | 109 | recnd 10068 |
. . . . . . . . . 10
|
111 | 103 | adantr 481 |
. . . . . . . . . 10
|
112 | 101 | adantr 481 |
. . . . . . . . . 10
|
113 | 110, 111,
112 | mulassd 10063 |
. . . . . . . . 9
|
114 | 108, 113 | eqtr4d 2659 |
. . . . . . . 8
|
115 | 114 | sumeq2dv 14433 |
. . . . . . 7
|
116 | 110, 111 | mulcld 10060 |
. . . . . . . 8
|
117 | 7, 101, 116 | fsummulc1 14517 |
. . . . . . 7
|
118 | 115, 117 | eqtr4d 2659 |
. . . . . 6
|
119 | 118 | oveq1d 6665 |
. . . . 5
|
120 | 7, 116 | fsumcl 14464 |
. . . . . 6
|
121 | 120, 101,
62, 63 | divassd 10836 |
. . . . 5
|
122 | 119, 121 | eqtrd 2656 |
. . . 4
|
123 | 81 | adantr 481 |
. . . . . . . 8
|
124 | 76 | adantr 481 |
. . . . . . . 8
|
125 | 123, 124 | remulcld 10070 |
. . . . . . 7
|
126 | 109, 125 | remulcld 10070 |
. . . . . 6
|
127 | 7, 126 | fsumrecl 14465 |
. . . . 5
|
128 | 127, 61 | nndivred 11069 |
. . . 4
|
129 | 122, 128 | eqeltrrd 2702 |
. . 3
|
130 | | 1red 10055 |
. . 3
|
131 | 58 | abscld 14175 |
. . . . 5
|
132 | 61 | nnrpd 11870 |
. . . . 5
|
133 | 57 | abscld 14175 |
. . . . . . 7
|
134 | 7, 133 | fsumrecl 14465 |
. . . . . 6
|
135 | 7, 57 | fsumabs 14533 |
. . . . . 6
|
136 | 81 | ad2antrr 762 |
. . . . . . . . . 10
|
137 | | ioombl 23333 |
. . . . . . . . . . . 12
|
138 | 137 | a1i 11 |
. . . . . . . . . . 11
|
139 | | 0red 10041 |
. . . . . . . . . . . . . 14
|
140 | | elfzle1 12344 |
. . . . . . . . . . . . . 14
|
141 | | volioo 23337 |
. . . . . . . . . . . . . 14
|
142 | 139, 53, 140, 141 | syl3anc 1326 |
. . . . . . . . . . . . 13
|
143 | 53, 139 | resubcld 10458 |
. . . . . . . . . . . . 13
|
144 | 142, 143 | eqeltrd 2701 |
. . . . . . . . . . . 12
|
145 | 144 | adantl 482 |
. . . . . . . . . . 11
|
146 | 82 | adantr 481 |
. . . . . . . . . . 11
|
147 | | iblconstmpt 40171 |
. . . . . . . . . . 11
|
148 | 138, 145,
146, 147 | syl3anc 1326 |
. . . . . . . . . 10
|
149 | 136, 148 | itgrecl 23564 |
. . . . . . . . 9
|
150 | 109, 149 | remulcld 10070 |
. . . . . . . 8
|
151 | 7, 150 | fsumrecl 14465 |
. . . . . . 7
|
152 | 21, 56 | absmuld 14193 |
. . . . . . . . 9
|
153 | 56 | abscld 14175 |
. . . . . . . . . 10
|
154 | 21 | absge0d 14183 |
. . . . . . . . . 10
|
155 | 37 | abscld 14175 |
. . . . . . . . . . . 12
|
156 | 37, 55 | iblabs 23595 |
. . . . . . . . . . . 12
|
157 | 155, 156 | itgrecl 23564 |
. . . . . . . . . . 11
|
158 | 37, 55 | itgabs 23601 |
. . . . . . . . . . 11
|
159 | 27, 36 | absmuld 14193 |
. . . . . . . . . . . . 13
|
160 | 27 | abscld 14175 |
. . . . . . . . . . . . . . 15
|
161 | | 1red 10055 |
. . . . . . . . . . . . . . 15
|
162 | 36 | abscld 14175 |
. . . . . . . . . . . . . . 15
|
163 | 27 | absge0d 14183 |
. . . . . . . . . . . . . . 15
|
164 | 36 | absge0d 14183 |
. . . . . . . . . . . . . . 15
|
165 | 14 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
|
166 | | 0re 10040 |
. . . . . . . . . . . . . . . . . . . . . 22
|
167 | | epos 14935 |
. . . . . . . . . . . . . . . . . . . . . 22
|
168 | 166, 14, 167 | ltleii 10160 |
. . . . . . . . . . . . . . . . . . . . 21
|
169 | 168 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
|
170 | 23 | renegcld 10457 |
. . . . . . . . . . . . . . . . . . . 20
|
171 | 165, 169,
170 | recxpcld 24469 |
. . . . . . . . . . . . . . . . . . 19
|
172 | 165, 169,
170 | cxpge0d 24470 |
. . . . . . . . . . . . . . . . . . 19
|
173 | 171, 172 | absidd 14161 |
. . . . . . . . . . . . . . . . . 18
|
174 | 173 | adantl 482 |
. . . . . . . . . . . . . . . . 17
|
175 | 171 | adantl 482 |
. . . . . . . . . . . . . . . . . 18
|
176 | | 1red 10055 |
. . . . . . . . . . . . . . . . . 18
|
177 | | 0xr 10086 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
178 | 177 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
|
179 | 53 | rexrd 10089 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
180 | 179 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . 22
|
181 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . . . 22
|
182 | | ioogtlb 39717 |
. . . . . . . . . . . . . . . . . . . . . 22
|
183 | 178, 180,
181, 182 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . . . . 21
|
184 | 23 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . 22
|
185 | 184 | lt0neg2d 10598 |
. . . . . . . . . . . . . . . . . . . . 21
|
186 | 183, 185 | mpbid 222 |
. . . . . . . . . . . . . . . . . . . 20
|
187 | 14 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
|
188 | | 1lt2 11194 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
189 | | egt2lt3 14934 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
190 | 189 | simpli 474 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
191 | | 1re 10039 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
192 | | 2re 11090 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
193 | 191, 192,
14 | lttri 10163 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
194 | 188, 190,
193 | mp2an 708 |
. . . . . . . . . . . . . . . . . . . . . 22
|
195 | 194 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
|
196 | 170 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . 21
|
197 | | 0red 10041 |
. . . . . . . . . . . . . . . . . . . . 21
|
198 | 187, 195,
196, 197 | cxpltd 24465 |
. . . . . . . . . . . . . . . . . . . 20
|
199 | 186, 198 | mpbid 222 |
. . . . . . . . . . . . . . . . . . 19
|
200 | | cxp0 24416 |
. . . . . . . . . . . . . . . . . . . 20
|
201 | 15, 200 | mp1i 13 |
. . . . . . . . . . . . . . . . . . 19
|
202 | 199, 201 | breqtrd 4679 |
. . . . . . . . . . . . . . . . . 18
|
203 | 175, 176,
202 | ltled 10185 |
. . . . . . . . . . . . . . . . 17
|
204 | 174, 203 | eqbrtrd 4675 |
. . . . . . . . . . . . . . . 16
|
205 | 204 | adantll 750 |
. . . . . . . . . . . . . . 15
|
206 | 28 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
|
207 | 30 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . 19
|
208 | 47 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . 19
|
209 | 31, 49 | eqtri 2644 |
. . . . . . . . . . . . . . . . . . 19
|
210 | 23 | adantl 482 |
. . . . . . . . . . . . . . . . . . 19
|
211 | 206, 207,
208, 209, 210 | etransclem13 40464 |
. . . . . . . . . . . . . . . . . 18
|
212 | 211 | fveq2d 6195 |
. . . . . . . . . . . . . . . . 17
|
213 | | nn0uz 11722 |
. . . . . . . . . . . . . . . . . 18
|
214 | 23 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . 22
|
215 | | nn0re 11301 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
216 | 215 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . 22
|
217 | 214, 216 | resubcld 10458 |
. . . . . . . . . . . . . . . . . . . . 21
|
218 | 217 | adantll 750 |
. . . . . . . . . . . . . . . . . . . 20
|
219 | 60, 77 | ifcld 4131 |
. . . . . . . . . . . . . . . . . . . . 21
|
220 | 219 | ad3antrrr 766 |
. . . . . . . . . . . . . . . . . . . 20
|
221 | 218, 220 | reexpcld 13025 |
. . . . . . . . . . . . . . . . . . 19
|
222 | 221 | recnd 10068 |
. . . . . . . . . . . . . . . . . 18
|
223 | 213, 208,
222 | fprodabs 14704 |
. . . . . . . . . . . . . . . . 17
|
224 | | elfznn0 12433 |
. . . . . . . . . . . . . . . . . . . 20
|
225 | 24 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . 22
|
226 | | nn0cn 11302 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
227 | 226 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . 22
|
228 | 225, 227 | subcld 10392 |
. . . . . . . . . . . . . . . . . . . . 21
|
229 | 228 | adantll 750 |
. . . . . . . . . . . . . . . . . . . 20
|
230 | 224, 229 | sylan2 491 |
. . . . . . . . . . . . . . . . . . 19
|
231 | 219 | ad3antrrr 766 |
. . . . . . . . . . . . . . . . . . 19
|
232 | 230, 231 | absexpd 14191 |
. . . . . . . . . . . . . . . . . 18
|
233 | 232 | prodeq2dv 14653 |
. . . . . . . . . . . . . . . . 17
|
234 | 212, 223,
233 | 3eqtrd 2660 |
. . . . . . . . . . . . . . . 16
|
235 | | nfv 1843 |
. . . . . . . . . . . . . . . . . 18
|
236 | | fzfid 12772 |
. . . . . . . . . . . . . . . . . 18
|
237 | 224, 228 | sylan2 491 |
. . . . . . . . . . . . . . . . . . . . 21
|
238 | 237 | abscld 14175 |
. . . . . . . . . . . . . . . . . . . 20
|
239 | 238 | adantll 750 |
. . . . . . . . . . . . . . . . . . 19
|
240 | 239, 231 | reexpcld 13025 |
. . . . . . . . . . . . . . . . . 18
|
241 | 237 | absge0d 14183 |
. . . . . . . . . . . . . . . . . . . 20
|
242 | 241 | adantll 750 |
. . . . . . . . . . . . . . . . . . 19
|
243 | 239, 231,
242 | expge0d 13026 |
. . . . . . . . . . . . . . . . . 18
|
244 | 78 | ad3antrrr 766 |
. . . . . . . . . . . . . . . . . 18
|
245 | 76 | ad3antrrr 766 |
. . . . . . . . . . . . . . . . . . . 20
|
246 | 245, 231 | reexpcld 13025 |
. . . . . . . . . . . . . . . . . . 19
|
247 | 224, 218 | sylan2 491 |
. . . . . . . . . . . . . . . . . . . . . 22
|
248 | 24 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
249 | 224, 227 | sylan2 491 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
250 | 248, 249 | negsubdi2d 10408 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
251 | 250 | adantll 750 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
252 | 224 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
253 | 252 | nn0red 11352 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
254 | | 0red 10041 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
255 | 210 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
256 | | elfzle2 12345 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
257 | 256 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
258 | 197, 184,
183 | ltled 10185 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
259 | 258 | adantll 750 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
260 | 259 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
261 | 253, 254,
245, 255, 257, 260 | le2subd 10647 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
262 | 83 | subid1d 10381 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
263 | 262 | ad3antrrr 766 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
264 | 261, 263 | breqtrd 4679 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
265 | 251, 264 | eqbrtrd 4675 |
. . . . . . . . . . . . . . . . . . . . . 22
|
266 | 247, 245,
265 | lenegcon1d 10609 |
. . . . . . . . . . . . . . . . . . . . 21
|
267 | | elfzel2 12340 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
268 | 267 | zred 11482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
269 | 268 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
270 | 53 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
271 | | iooltub 39735 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
272 | 178, 180,
181, 271 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
273 | | elfzle2 12345 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
274 | 273 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
275 | 184, 270,
269, 272, 274 | ltletrd 10197 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
276 | 184, 269,
275 | ltled 10185 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
277 | 276 | adantll 750 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
278 | 277 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
279 | 252 | nn0ge0d 11354 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
280 | 255, 254,
245, 253, 278, 279 | le2subd 10647 |
. . . . . . . . . . . . . . . . . . . . . 22
|
281 | 280, 263 | breqtrd 4679 |
. . . . . . . . . . . . . . . . . . . . 21
|
282 | 247, 245 | absled 14169 |
. . . . . . . . . . . . . . . . . . . . 21
|
283 | 266, 281,
282 | mpbir2and 957 |
. . . . . . . . . . . . . . . . . . . 20
|
284 | | leexp1a 12919 |
. . . . . . . . . . . . . . . . . . . 20
|
285 | 239, 245,
231, 242, 283, 284 | syl32anc 1334 |
. . . . . . . . . . . . . . . . . . 19
|
286 | 46 | nnge1d 11063 |
. . . . . . . . . . . . . . . . . . . . 21
|
287 | 286 | ad3antrrr 766 |
. . . . . . . . . . . . . . . . . . . 20
|
288 | 219 | nn0zd 11480 |
. . . . . . . . . . . . . . . . . . . . . 22
|
289 | 77 | nn0zd 11480 |
. . . . . . . . . . . . . . . . . . . . . 22
|
290 | | iftrue 4092 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
291 | 290 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
292 | 30 | nnred 11035 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
293 | 292 | lem1d 10957 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
294 | 293 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
295 | 291, 294 | eqbrtrd 4675 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
296 | | iffalse 4095 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
297 | 296 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
298 | 292 | leidd 10594 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
299 | 298 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
300 | 297, 299 | eqbrtrd 4675 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
301 | 295, 300 | pm2.61dan 832 |
. . . . . . . . . . . . . . . . . . . . . 22
|
302 | | eluz2 11693 |
. . . . . . . . . . . . . . . . . . . . . 22
|
303 | 288, 289,
301, 302 | syl3anbrc 1246 |
. . . . . . . . . . . . . . . . . . . . 21
|
304 | 303 | ad3antrrr 766 |
. . . . . . . . . . . . . . . . . . . 20
|
305 | 245, 287,
304 | leexp2ad 13041 |
. . . . . . . . . . . . . . . . . . 19
|
306 | 240, 246,
244, 285, 305 | letrd 10194 |
. . . . . . . . . . . . . . . . . 18
|
307 | 235, 236,
240, 243, 244, 306 | fprodle 14727 |
. . . . . . . . . . . . . . . . 17
|
308 | 78 | recnd 10068 |
. . . . . . . . . . . . . . . . . . . 20
|
309 | | fprodconst 14708 |
. . . . . . . . . . . . . . . . . . . 20
|
310 | 7, 308, 309 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . 19
|
311 | | hashfz0 13219 |
. . . . . . . . . . . . . . . . . . . . 21
|
312 | 47, 311 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
|
313 | 312 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . . 19
|
314 | 310, 313 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . 18
|
315 | 314 | ad2antrr 762 |
. . . . . . . . . . . . . . . . 17
|
316 | 307, 315 | breqtrd 4679 |
. . . . . . . . . . . . . . . 16
|
317 | 234, 316 | eqbrtrd 4675 |
. . . . . . . . . . . . . . 15
|
318 | 160, 161,
162, 136, 163, 164, 205, 317 | lemul12ad 10966 |
. . . . . . . . . . . . . 14
|
319 | 82 | mulid2d 10058 |
. . . . . . . . . . . . . . 15
|
320 | 319 | ad2antrr 762 |
. . . . . . . . . . . . . 14
|
321 | 318, 320 | breqtrd 4679 |
. . . . . . . . . . . . 13
|
322 | 159, 321 | eqbrtrd 4675 |
. . . . . . . . . . . 12
|
323 | 156, 148,
155, 136, 322 | itgle 23576 |
. . . . . . . . . . 11
|
324 | 153, 157,
149, 158, 323 | letrd 10194 |
. . . . . . . . . 10
|
325 | 153, 149,
109, 154, 324 | lemul2ad 10964 |
. . . . . . . . 9
|
326 | 152, 325 | eqbrtrd 4675 |
. . . . . . . 8
|
327 | 7, 133, 150, 326 | fsumle 14531 |
. . . . . . 7
|
328 | | itgconst 23585 |
. . . . . . . . . . 11
|
329 | 138, 145,
146, 328 | syl3anc 1326 |
. . . . . . . . . 10
|
330 | 47 | nn0ge0d 11354 |
. . . . . . . . . . . . . 14
|
331 | 76, 77, 330 | expge0d 13026 |
. . . . . . . . . . . . 13
|
332 | 78, 80, 331 | expge0d 13026 |
. . . . . . . . . . . 12
|
333 | 332 | adantr 481 |
. . . . . . . . . . 11
|
334 | 18 | subid1d 10381 |
. . . . . . . . . . . . . 14
|
335 | 142, 334 | eqtrd 2656 |
. . . . . . . . . . . . 13
|
336 | 335, 273 | eqbrtrd 4675 |
. . . . . . . . . . . 12
|
337 | 336 | adantl 482 |
. . . . . . . . . . 11
|
338 | 145, 124,
123, 333, 337 | lemul2ad 10964 |
. . . . . . . . . 10
|
339 | 329, 338 | eqbrtrd 4675 |
. . . . . . . . 9
|
340 | 149, 125,
109, 154, 339 | lemul2ad 10964 |
. . . . . . . 8
|
341 | 7, 150, 126, 340 | fsumle 14531 |
. . . . . . 7
|
342 | 134, 151,
127, 327, 341 | letrd 10194 |
. . . . . 6
|
343 | 131, 134,
127, 135, 342 | letrd 10194 |
. . . . 5
|
344 | 131, 127,
132, 343 | lediv1dd 11930 |
. . . 4
|
345 | 344, 122 | breqtrd 4679 |
. . 3
|
346 | | etransclem23.lt1 |
. . 3
|
347 | 75, 129, 130, 345, 346 | lelttrd 10195 |
. 2
|
348 | 70, 347 | eqbrtrd 4675 |
1
|