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

Theorem etransclem35 38246
 Description: does not divide the P-1 -th derivative of applied to . This is case 2 of the proof in [Juillerat] p. 13 . (Contributed by Glauco Siliprandi, 5-Apr-2020.)
Hypotheses
Ref Expression
etransclem35.p
etransclem35.m
etransclem35.f
etransclem35.c
etransclem35.d
Assertion
Ref Expression
etransclem35
Distinct variable groups:   ,,,   ,,   ,,,,   ,,,,   ,,,,
Allowed substitution hints:   ()   (,)   (,,,)

Proof of Theorem etransclem35
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 reelprrecn 9649 . . . 4
21a1i 11 . . 3
3 reopn 37591 . . . . 5
4 eqid 2471 . . . . . 6 fld fld
54tgioo2 21899 . . . . 5 fldt
63, 5eleqtri 2547 . . . 4 fldt
76a1i 11 . . 3 fldt
8 etransclem35.p . . 3
9 etransclem35.m . . 3
10 etransclem35.f . . 3
11 nnm1nn0 10935 . . . 4
128, 11syl 17 . . 3
13 etransclem5 38216 . . 3
14 etransclem35.c . . 3
15 0red 9662 . . 3
162, 7, 8, 9, 10, 12, 13, 14, 15etransclem31 38242 . 2
17 nfv 1769 . . 3
18 nfcv 2612 . . 3
1914, 12etransclem16 38227 . . 3
20 simpr 468 . . . . . . . . . . . . 13
2114, 12etransclem12 38223 . . . . . . . . . . . . . 14
2221adantr 472 . . . . . . . . . . . . 13
2320, 22eleqtrd 2551 . . . . . . . . . . . 12
24 rabid 2953 . . . . . . . . . . . 12
2523, 24sylib 201 . . . . . . . . . . 11
2625simprd 470 . . . . . . . . . 10
2726eqcomd 2477 . . . . . . . . 9
2827fveq2d 5883 . . . . . . . 8
2928oveq1d 6323 . . . . . . 7
30 nfcv 2612 . . . . . . . 8
31 fzfid 12224 . . . . . . . 8
32 nn0ex 10899 . . . . . . . . . 10
33 fzssnn0 37627 . . . . . . . . . 10
34 mapss 7532 . . . . . . . . . 10
3532, 33, 34mp2an 686 . . . . . . . . 9
3625simpld 466 . . . . . . . . 9
3735, 36sseldi 3416 . . . . . . . 8
3830, 31, 37mccl 37775 . . . . . . 7
3929, 38eqeltrd 2549 . . . . . 6
4039nnzd 11062 . . . . 5
418adantr 472 . . . . . . 7
429adantr 472 . . . . . . 7
43 elmapi 7511 . . . . . . . 8
4436, 43syl 17 . . . . . . 7
45 0zd 10973 . . . . . . 7
4641, 42, 44, 45etransclem10 38221 . . . . . 6
47 fzfid 12224 . . . . . . 7
488ad2antrr 740 . . . . . . . 8
4944adantr 472 . . . . . . . 8
50 fz1ssfz0 37616 . . . . . . . . . 10
5150sseli 3414 . . . . . . . . 9
5251adantl 473 . . . . . . . 8
53 0zd 10973 . . . . . . . 8
5448, 49, 52, 53etransclem3 38214 . . . . . . 7
5547, 54fprodzcl 14085 . . . . . 6
5646, 55zmulcld 11069 . . . . 5
5740, 56zmulcld 11069 . . . 4
5857zcnd 11064 . . 3
59 nn0uz 11217 . . . . . . . . . . 11
6012, 59syl6eleq 2559 . . . . . . . . . 10
61 eluzfz2 11833 . . . . . . . . . 10
6260, 61syl 17 . . . . . . . . 9
63 eluzfz1 11832 . . . . . . . . . 10
6460, 63syl 17 . . . . . . . . 9
6562, 64ifcld 3915 . . . . . . . 8
6665adantr 472 . . . . . . 7
67 etransclem35.d . . . . . . 7
6866, 67fmptd 6061 . . . . . 6
69 ovex 6336 . . . . . . 7
70 ovex 6336 . . . . . . 7
7169, 70elmap 7518 . . . . . 6
7268, 71sylibr 217 . . . . 5
739, 59syl6eleq 2559 . . . . . . 7
74 fzsscn 37619 . . . . . . . 8
7568ffvelrnda 6037 . . . . . . . 8
7674, 75sseldi 3416 . . . . . . 7
77 fveq2 5879 . . . . . . 7
7873, 76, 77fsum1p 13891 . . . . . 6
7967a1i 11 . . . . . . . 8
80 simpr 468 . . . . . . . . 9
8180iftrued 3880 . . . . . . . 8
82 eluzfz1 11832 . . . . . . . . 9
8373, 82syl 17 . . . . . . . 8
8479, 81, 83, 12fvmptd 5969 . . . . . . 7
85 0p1e1 10743 . . . . . . . . . . 11
8685oveq1i 6318 . . . . . . . . . 10
8786sumeq1i 13841 . . . . . . . . 9
8887a1i 11 . . . . . . . 8
8967fvmpt2 5972 . . . . . . . . . . 11
9051, 65, 89syl2anr 486 . . . . . . . . . 10
91 0red 9662 . . . . . . . . . . . . . 14
92 1red 9676 . . . . . . . . . . . . . . 15
93 elfzelz 11826 . . . . . . . . . . . . . . . 16
9493zred 11063 . . . . . . . . . . . . . . 15
95 0lt1 10157 . . . . . . . . . . . . . . . 16
9695a1i 11 . . . . . . . . . . . . . . 15
97 elfzle1 11828 . . . . . . . . . . . . . . 15
9891, 92, 94, 96, 97ltletrd 9812 . . . . . . . . . . . . . 14
9991, 98gtned 9787 . . . . . . . . . . . . 13
10099neneqd 2648 . . . . . . . . . . . 12
101100iffalsed 3883 . . . . . . . . . . 11
102101adantl 473 . . . . . . . . . 10
10390, 102eqtrd 2505 . . . . . . . . 9
104103sumeq2dv 13846 . . . . . . . 8
105 fzfi 12223 . . . . . . . . . 10
106105olci 398 . . . . . . . . 9
107 sumz 13865 . . . . . . . . 9
108106, 107mp1i 13 . . . . . . . 8
10988, 104, 1083eqtrd 2509 . . . . . . 7
11084, 109oveq12d 6326 . . . . . 6
1118nncnd 10647 . . . . . . . 8
112 1cnd 9677 . . . . . . . 8
113111, 112subcld 10005 . . . . . . 7
114113addid1d 9851 . . . . . 6
11578, 110, 1143eqtrd 2509 . . . . 5
116 fveq1 5878 . . . . . . . 8
117116sumeq2ad 37740 . . . . . . 7
118117eqeq1d 2473 . . . . . 6
119118elrab 3184 . . . . 5
12072, 115, 119sylanbrc 677 . . . 4
121120, 21eleqtrrd 2552 . . 3
122116fveq2d 5883 . . . . . 6
123122prodeq2ad 37769 . . . . 5
124123oveq2d 6324 . . . 4
125 fveq1 5878 . . . . . . 7
126125breq2d 4407 . . . . . 6
127125oveq2d 6324 . . . . . . . . 9
128127fveq2d 5883 . . . . . . . 8
129128oveq2d 6324 . . . . . . 7
130127oveq2d 6324 . . . . . . 7
131129, 130oveq12d 6326 . . . . . 6
132126, 131ifbieq2d 3897 . . . . 5
133116breq2d 4407 . . . . . . 7
134116oveq2d 6324 . . . . . . . . . 10
135134fveq2d 5883 . . . . . . . . 9
136135oveq2d 6324 . . . . . . . 8
137134oveq2d 6324 . . . . . . . 8
138136, 137oveq12d 6326 . . . . . . 7
139133, 138ifbieq2d 3897 . . . . . 6
140139prodeq2ad 37769 . . . . 5
141132, 140oveq12d 6326 . . . 4
142124, 141oveq12d 6326 . . 3
14317, 18, 19, 58, 121, 142fsumsplit1 37747 . 2
14433, 75sseldi 3416 . . . . . . . . . . . 12
145144faccld 37621 . . . . . . . . . . 11
146145nncnd 10647 . . . . . . . . . 10
14777fveq2d 5883 . . . . . . . . . 10
14873, 146, 147fprod1p 14099 . . . . . . . . 9
14984fveq2d 5883 . . . . . . . . . 10
15086prodeq1i 14049 . . . . . . . . . . . 12
151150a1i 11 . . . . . . . . . . 11
152103fveq2d 5883 . . . . . . . . . . . . 13
153 fac0 12500 . . . . . . . . . . . . 13
154152, 153syl6eq 2521 . . . . . . . . . . . 12
155154prodeq2dv 14054 . . . . . . . . . . 11
156 prod1 14075 . . . . . . . . . . . 12
157106, 156mp1i 13 . . . . . . . . . . 11
158151, 155, 1573eqtrd 2509 . . . . . . . . . 10
159149, 158oveq12d 6326 . . . . . . . . 9
16012faccld 37621 . . . . . . . . . . 11
161160nncnd 10647 . . . . . . . . . 10
162161mulid1d 9678 . . . . . . . . 9
163148, 159, 1623eqtrd 2509 . . . . . . . 8
164163oveq2d 6324 . . . . . . 7
165160nnne0d 10676 . . . . . . . 8
166161, 165dividd 10403 . . . . . . 7
167164, 166eqtrd 2505 . . . . . 6
16812nn0red 10950 . . . . . . . . . . . . 13
16984, 168eqeltrd 2549 . . . . . . . . . . . 12
170169, 168lttri3d 9792 . . . . . . . . . . 11
17184, 170mpbid 215 . . . . . . . . . 10
172171simprd 470 . . . . . . . . 9
173172iffalsed 3883 . . . . . . . 8
17484eqcomd 2477 . . . . . . . . . . . . . 14
175113, 174subeq0bd 10066 . . . . . . . . . . . . 13
176175fveq2d 5883 . . . . . . . . . . . 12
177176, 153syl6eq 2521 . . . . . . . . . . 11
178177oveq2d 6324 . . . . . . . . . 10
179161div1d 10397 . . . . . . . . . 10
180178, 179eqtrd 2505 . . . . . . . . 9
181175oveq2d 6324 . . . . . . . . . 10
182 0cnd 9654 . . . . . . . . . . 11
183182exp0d 12448 . . . . . . . . . 10
184181, 183eqtrd 2505 . . . . . . . . 9
185180, 184oveq12d 6326 . . . . . . . 8
186173, 185, 1623eqtrd 2509 . . . . . . 7
187 fzssre 37623 . . . . . . . . . . . 12
18868adantr 472 . . . . . . . . . . . . 13
18951adantl 473 . . . . . . . . . . . . 13
190188, 189ffvelrnd 6038 . . . . . . . . . . . 12
191187, 190sseldi 3416 . . . . . . . . . . 11
1928nnred 10646 . . . . . . . . . . . 12
193192adantr 472 . . . . . . . . . . 11
1948nngt0d 10675 . . . . . . . . . . . . . 14
19515, 192, 194ltled 9800 . . . . . . . . . . . . 13
196195adantr 472 . . . . . . . . . . . 12
197103, 196eqbrtrd 4416 . . . . . . . . . . 11
198191, 193, 197lensymd 9803 . . . . . . . . . 10
199198iffalsed 3883 . . . . . . . . 9
200103oveq2d 6324 . . . . . . . . . . . . . 14
201111adantr 472 . . . . . . . . . . . . . . 15
202201subid1d 9994 . . . . . . . . . . . . . 14
203200, 202eqtrd 2505 . . . . . . . . . . . . 13
204203fveq2d 5883 . . . . . . . . . . . 12
205204oveq2d 6324 . . . . . . . . . . 11
2068nnnn0d 10949 . . . . . . . . . . . . . . 15
207206faccld 37621 . . . . . . . . . . . . . 14
208207nncnd 10647 . . . . . . . . . . . . 13
209207nnne0d 10676 . . . . . . . . . . . . 13
210208, 209dividd 10403 . . . . . . . . . . . 12
211210adantr 472 . . . . . . . . . . 11
212205, 211eqtrd 2505 . . . . . . . . . 10
213 df-neg 9883 . . . . . . . . . . . . 13
214213eqcomi 2480 . . . . . . . . . . . 12
215214a1i 11 . . . . . . . . . . 11
216215, 203oveq12d 6326 . . . . . . . . . 10
217212, 216oveq12d 6326 . . . . . . . . 9
21893znegcld 11065 . . . . . . . . . . . . 13
219218zcnd 11064 . . . . . . . . . . . 12
220219adantl 473 . . . . . . . . . . 11
221206adantr 472 . . . . . . . . . . 11
222220, 221expcld 12454 . . . . . . . . . 10
223222mulid2d 9679 . . . . . . . . 9
224199, 217, 2233eqtrd 2509 . . . . . . . 8
225224prodeq2dv 14054 . . . . . . 7
226186, 225oveq12d 6326 . . . . . 6
227167, 226oveq12d 6326 . . . . 5
228 fzfid 12224 . . . . . . . . 9
229 zexpcl 12325 . . . . . . . . . 10
230218, 206, 229syl2anr 486 . . . . . . . . 9
231228, 230fprodzcl 14085 . . . . . . . 8
232231zcnd 11064 . . . . . . 7
233161, 232mulcld 9681 . . . . . 6
234233mulid2d 9679 . . . . 5
235227, 234eqtrd 2505 . . . 4
236 eldifi 3544 . . . . . . . . . . . . . . 15
23783adantr 472 . . . . . . . . . . . . . . . 16
23844, 237ffvelrnd 6038 . . . . . . . . . . . . . . 15
239236, 238sylan2 482 . . . . . . . . . . . . . 14
240187, 239sseldi 3416 . . . . . . . . . . . . 13
241168adantr 472 . . . . . . . . . . . . 13
242 elfzle2 11829 . . . . . . . . . . . . . 14
243239, 242syl 17 . . . . . . . . . . . . 13
244240, 241, 243lensymd 9803 . . . . . . . . . . . 12
245244iffalsed 3883 . . . . . . . . . . 11
24612nn0zd 11061 . . . . . . . . . . . . . . . 16
247246adantr 472 . . . . . . . . . . . . . . 15
248239elfzelzd 37624 . . . . . . . . . . . . . . 15
249247, 248zsubcld 11068 . . . . . . . . . . . . . 14
250 ffn 5739 . . . . . . . . . . . . . . . . . . . . . 22
25144, 250syl 17 . . . . . . . . . . . . . . . . . . . . 21
252251adantr 472 . . . . . . . . . . . . . . . . . . . 20
253 ffn 5739 . . . . . . . . . . . . . . . . . . . . . 22
25468, 253syl 17 . . . . . . . . . . . . . . . . . . . . 21
255254ad2antrr 740 . . . . . . . . . . . . . . . . . . . 20
256 fveq2 5879 . . . . . . . . . . . . . . . . . . . . . . . . 25
257256adantl 473 . . . . . . . . . . . . . . . . . . . . . . . 24
258 id 22 . . . . . . . . . . . . . . . . . . . . . . . . . 26
259258eqcomd 2477 . . . . . . . . . . . . . . . . . . . . . . . . 25
260259ad2antlr 741 . . . . . . . . . . . . . . . . . . . . . . . 24
26177adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . . 26
26284adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . 26
263261, 262eqtr2d 2506 . . . . . . . . . . . . . . . . . . . . . . . . 25
264263adantlr 729 . . . . . . . . . . . . . . . . . . . . . . . 24
265257, 260, 2643eqtrd 2509 . . . . . . . . . . . . . . . . . . . . . . 23
266265adantllr 733 . . . . . . . . . . . . . . . . . . . . . 22
267266adantlr 729 . . . . . . . . . . . . . . . . . . . . 21
26826ad4antr 746 . . . . . . . . . . . . . . . . . . . . . . 23
269168ad5antr 748 . . . . . . . . . . . . . . . . . . . . . . . . 25
270168ad4antr 746 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
27144adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
27250sseli 3414 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
273272adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
274271, 273ffvelrnd 6038 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
27533, 274sseldi 3416 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
27647, 275fsumnn0cl 13879 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
277276nn0red 10950 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
278277ad3antrrr 744 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
279 0red 9662 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
28044ffvelrnda 6037 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
281187, 280sseldi 3416 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
282281ad2antrr 740 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
283 nfv 1769 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
284 nfcv 2612 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
285 fzfid 12224 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
286 simp-4l 784 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
28774, 274sseldi 3416 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
288286, 287sylancom 680 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
289 1zzd 10992 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
290 elfzel2 11824 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
291290adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
292 elfzelz 11826 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
293292adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
294289, 291, 2933jca 1210 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
295 elfznn0 11913 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
296295adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
297 neqne 2651 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
298297adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
299 elnnne0 10907 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
300296, 298, 299sylanbrc 677 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
301300nnge1d 10674 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
302 elfzle2 11829 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
303302adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
304294, 301, 303jca32 544 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
305 elfz2 11817 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
306304, 305sylibr 217 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
307306adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
308307adantlll 732 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
309 fveq2 5879 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
310283, 284, 285, 288, 308, 309fsumsplit1 37747 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
311310eqcomd 2477 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
312311, 278eqeltrd 2549 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
313 elfzle1 11828 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
314280, 313syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
315314ad2antrr 740 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
316 neqne 2651 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
317316adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
318279, 282, 315, 317leneltd 9806 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
319 diffi 7821 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
320105, 319mp1i 13 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
321 eldifi 3544 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
322321adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
32350, 322sseldi 3416 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
32444ffvelrnda 6037 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
325187, 324sseldi 3416 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
326323, 325syldan 478 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
327 elfzle1 11828 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
328324, 327syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
329323, 328syldan 478 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
330320, 326, 329fsumge0 13932 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
331330adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
332320, 326fsumrecl 13877 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
333332adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
334281, 333addge01d 10222 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
335331, 334mpbid 215 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
336335ad2antrr 740 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
337279, 282, 312, 318, 336ltletrd 9812 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
338337, 311breqtrd 4420 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
339278, 338elrpd 11361 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
340270, 339ltaddrpd 11394 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
341340adantlllr 37424 . . . . . . . . . . . . . . . . . . . . . . . . . 26
342 fveq2 5879 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
343342cbvsumv 13839 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
344343a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
34573ad5antr 748 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
346 simp-5l 786 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
34774, 324sseldi 3416 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
348346, 347sylancom 680 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
349 fveq2 5879 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
350345, 348, 349fsum1p 13891 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
351259ad4antlr 747 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
35286sumeq1i 13841 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
353352a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
354351, 353oveq12d 6326 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
355344, 350, 3543eqtrrd 2510 . . . . . . . . . . . . . . . . . . . . . . . . . 26
356341, 355breqtrd 4420 . . . . . . . . . . . . . . . . . . . . . . . . 25
357269, 356gtned 9787 . . . . . . . . . . . . . . . . . . . . . . . 24
358357neneqd 2648 . . . . . . . . . . . . . . . . . . . . . . 23
359268, 358condan 811 . . . . . . . . . . . . . . . . . . . . . 22
360 simpr 468 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
36133, 66sseldi 3416 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
36267fvmpt2 5972 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
363360, 361, 362syl2anc 673 . . . . . . . . . . . . . . . . . . . . . . . . . 26
364363adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . 25
365 simpr 468 . . . . . . . . . . . . . . . . . . . . . . . . . 26
366365iffalsed 3883 . . . . . . . . . . . . . . . . . . . . . . . . 25
367364, 366eqtr2d 2506 . . . . . . . . . . . . . . . . . . . . . . . 24
368367adantllr 733 . . . . . . . . . . . . . . . . . . . . . . 23
369368adantllr 733 . . . . . . . . . . . . . . . . . . . . . 22
370359, 369eqtrd 2505 . . . . . . . . . . . . . . . . . . . . 21
371267, 370pm2.61dan 808 . . . . . . . . . . . . . . . . . . . 20
372252, 255, 371eqfnfvd 5994 . . . . . . . . . . . . . . . . . . 19
373236, 372sylanl2 663 . . . . . . . . . . . . . . . . . 18
374 eldifsni 4089 . . . . . . . . . . . . . . . . . . . 20
375374neneqd 2648 . . . . . . . . . . . . . . . . . . 19
376375ad2antlr 741 . . . . . . . . . . . . . . . . . 18