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

Theorem etransclem44 38143
 Description: The given finite sum is nonzero. This is the claim proved after equation (7) in [Juillerat] p. 12 . (Contributed by Glauco Siliprandi, 5-Apr-2020.)
Hypotheses
Ref Expression
etransclem44.a
etransclem44.a0
etransclem44.m
etransclem44.p
etransclem44.ap
etransclem44.mp
etransclem44.f
etransclem44.k
Assertion
Ref Expression
etransclem44
Distinct variable groups:   ,   ,   ,,,   ,,,   ,,,
Allowed substitution hints:   (,)   (,)   (,,)

Proof of Theorem etransclem44
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 etransclem44.k . . . 4
21a1i 11 . . 3
3 nfv 1761 . . . . 5
4 nfcv 2592 . . . . 5
5 fzfi 12185 . . . . . . 7
6 fzfi 12185 . . . . . . 7
7 xpfi 7842 . . . . . . 7
85, 6, 7mp2an 678 . . . . . 6
98a1i 11 . . . . 5
10 etransclem44.a . . . . . . . . 9
1110adantr 467 . . . . . . . 8
12 fzssnn0 37539 . . . . . . . . . 10
13 xp1st 6823 . . . . . . . . . 10
1412, 13sseldi 3430 . . . . . . . . 9
1514adantl 468 . . . . . . . 8
1611, 15ffvelrnd 6023 . . . . . . 7
17 reelprrecn 9631 . . . . . . . . 9
1817a1i 11 . . . . . . . 8
19 reopn 37502 . . . . . . . . . 10
20 eqid 2451 . . . . . . . . . . 11 fld fld
2120tgioo2 21821 . . . . . . . . . 10 fldt
2219, 21eleqtri 2527 . . . . . . . . 9 fldt
2322a1i 11 . . . . . . . 8 fldt
24 etransclem44.p . . . . . . . . . 10
25 prmnn 14625 . . . . . . . . . 10
2624, 25syl 17 . . . . . . . . 9
2726adantr 467 . . . . . . . 8
28 etransclem44.m . . . . . . . . 9
2928adantr 467 . . . . . . . 8
30 etransclem44.f . . . . . . . 8
31 xp2nd 6824 . . . . . . . . . 10
32 elfznn0 11887 . . . . . . . . . 10
3331, 32syl 17 . . . . . . . . 9
3433adantl 468 . . . . . . . 8
3515nn0red 10926 . . . . . . . 8
3615nn0zd 11038 . . . . . . . 8
3718, 23, 27, 29, 30, 34, 35, 36etransclem42 38141 . . . . . . 7
3816, 37zmulcld 11046 . . . . . 6
3938zcnd 11041 . . . . 5
40 nn0uz 11193 . . . . . . . 8
4128, 40syl6eleq 2539 . . . . . . 7
42 eluzfz1 11806 . . . . . . 7
4341, 42syl 17 . . . . . 6
44 0zd 10949 . . . . . . . . 9
4528nn0zd 11038 . . . . . . . . . . 11
4626nnzd 11039 . . . . . . . . . . 11
4745, 46zmulcld 11046 . . . . . . . . . 10
48 nnm1nn0 10911 . . . . . . . . . . . 12
4926, 48syl 17 . . . . . . . . . . 11
5049nn0zd 11038 . . . . . . . . . 10
5147, 50zaddcld 11044 . . . . . . . . 9
5244, 51, 503jca 1188 . . . . . . . 8
5349nn0ge0d 10928 . . . . . . . 8
5426nnnn0d 10925 . . . . . . . . . . 11
5528, 54nn0mulcld 10930 . . . . . . . . . 10
5655nn0ge0d 10928 . . . . . . . . 9
5749nn0red 10926 . . . . . . . . . 10
5847zred 11040 . . . . . . . . . 10
5957, 58addge02d 10202 . . . . . . . . 9
6056, 59mpbid 214 . . . . . . . 8
6152, 53, 60jca32 538 . . . . . . 7
62 elfz2 11791 . . . . . . 7
6361, 62sylibr 216 . . . . . 6
64 opelxp 4864 . . . . . 6
6543, 63, 64sylanbrc 670 . . . . 5
66 fveq2 5865 . . . . . . . 8
67 0re 9643 . . . . . . . . 9
68 ovex 6318 . . . . . . . . 9
69 op1stg 6805 . . . . . . . . 9
7067, 68, 69mp2an 678 . . . . . . . 8
7166, 70syl6eq 2501 . . . . . . 7
7271fveq2d 5869 . . . . . 6
73 fveq2 5865 . . . . . . . . 9
74 op2ndg 6806 . . . . . . . . . 10
7567, 68, 74mp2an 678 . . . . . . . . 9
7673, 75syl6eq 2501 . . . . . . . 8
7776fveq2d 5869 . . . . . . 7
7877, 71fveq12d 5871 . . . . . 6
7972, 78oveq12d 6308 . . . . 5
803, 4, 9, 39, 65, 79fsumsplit1 37651 . . . 4
8180oveq1d 6305 . . 3
8212, 43sseldi 3430 . . . . . . 7
8310, 82ffvelrnd 6023 . . . . . 6
8417a1i 11 . . . . . . 7
8522a1i 11 . . . . . . 7 fldt
8667a1i 11 . . . . . . 7
8784, 85, 26, 28, 30, 49, 86, 44etransclem42 38141 . . . . . 6
8883, 87zmulcld 11046 . . . . 5
8988zcnd 11041 . . . 4
90 difss 3560 . . . . . . . 8
91 ssfi 7792 . . . . . . . 8
928, 90, 91mp2an 678 . . . . . . 7
9392a1i 11 . . . . . 6
94 eldifi 3555 . . . . . . 7
9594, 38sylan2 477 . . . . . 6
9693, 95fsumzcl 13801 . . . . 5
9796zcnd 11041 . . . 4
9849faccld 37533 . . . . 5
9998nncnd 10625 . . . 4
10098nnne0d 10654 . . . 4
10189, 97, 99, 100divdird 10421 . . 3
1022, 81, 1013eqtrd 2489 . 2
10326nnne0d 10654 . . 3
10483zcnd 11041 . . . . 5
10587zcnd 11041 . . . . 5
106104, 105, 99, 100divassd 10418 . . . 4
107 etransclem5 38104 . . . . . . 7
108 etransclem11 38110 . . . . . . 7
10984, 85, 26, 28, 30, 49, 107, 108, 43, 86etransclem37 38136 . . . . . 6
11098nnzd 11039 . . . . . . 7
111 dvdsval2 14308 . . . . . . 7
112110, 100, 87, 111syl3anc 1268 . . . . . 6
113109, 112mpbid 214 . . . . 5
11483, 113zmulcld 11046 . . . 4
115106, 114eqeltrd 2529 . . 3
11694, 39sylan2 477 . . . . 5
11793, 99, 116, 100fsumdivc 13847 . . . 4
11816zcnd 11041 . . . . . . . 8
11994, 118sylan2 477 . . . . . . 7
12094, 37sylan2 477 . . . . . . . 8
121120zcnd 11041 . . . . . . 7
12299adantr 467 . . . . . . 7
123100adantr 467 . . . . . . 7
124119, 121, 122, 123divassd 10418 . . . . . 6
12594, 16sylan2 477 . . . . . . 7
12617a1i 11 . . . . . . . . 9
12722a1i 11 . . . . . . . . 9 fldt
12826adantr 467 . . . . . . . . 9
12928adantr 467 . . . . . . . . 9
13094adantl 468 . . . . . . . . . 10
131130, 33syl 17 . . . . . . . . 9
132130, 13syl 17 . . . . . . . . 9
13394, 35sylan2 477 . . . . . . . . 9
134126, 127, 128, 129, 30, 131, 107, 108, 132, 133etransclem37 38136 . . . . . . . 8
135110adantr 467 . . . . . . . . 9
136 dvdsval2 14308 . . . . . . . . 9
137135, 123, 120, 136syl3anc 1268 . . . . . . . 8
138134, 137mpbid 214 . . . . . . 7
139125, 138zmulcld 11046 . . . . . 6
140124, 139eqeltrd 2529 . . . . 5
14193, 140fsumzcl 13801 . . . 4
142117, 141eqeltrd 2529 . . 3
143 1zzd 10968 . . . . . . . . . . . 12
144 zabscl 13376 . . . . . . . . . . . . 13
14583, 144syl 17 . . . . . . . . . . . 12
146143, 50, 1453jca 1188 . . . . . . . . . . 11
147 nn0abscl 13375 . . . . . . . . . . . . . 14
14883, 147syl 17 . . . . . . . . . . . . 13
149 etransclem44.a0 . . . . . . . . . . . . . 14
150104, 149absne0d 13509 . . . . . . . . . . . . 13
151 elnnne0 10883 . . . . . . . . . . . . 13
152148, 150, 151sylanbrc 670 . . . . . . . . . . . 12
153152nnge1d 10652 . . . . . . . . . . 11
154 etransclem44.ap . . . . . . . . . . . 12
155 zltlem1 10989 . . . . . . . . . . . . 13
156145, 46, 155syl2anc 667 . . . . . . . . . . . 12
157154, 156mpbid 214 . . . . . . . . . . 11
158146, 153, 157jca32 538 . . . . . . . . . 10
159 elfz2 11791 . . . . . . . . . 10
160158, 159sylibr 216 . . . . . . . . 9
161 fzm1ndvds 14357 . . . . . . . . 9
16226, 160, 161syl2anc 667 . . . . . . . 8
163 dvdsabsb 14322 . . . . . . . . 9
16446, 83, 163syl2anc 667 . . . . . . . 8
165162, 164mtbird 303 . . . . . . 7
166 etransclem44.mp . . . . . . . 8
16728, 24, 166, 30etransclem41 38140 . . . . . . 7
168165, 167jca 535 . . . . . 6
169 pm4.56 498 . . . . . 6
170168, 169sylib 200 . . . . 5
171 euclemma 14665 . . . . . 6
17224, 83, 113, 171syl3anc 1268 . . . . 5
173170, 172mtbird 303 . . . 4
174106breq2d 4414 . . . 4
175173, 174mtbird 303 . . 3
17646adantr 467 . . . . . . . 8
177176, 125, 1383jca 1188 . . . . . . 7
178 eldifn 3556 . . . . . . . . . 10
17994adantr 467 . . . . . . . . . . . . 13
180 1st2nd2 6830 . . . . . . . . . . . . 13
181179, 180syl 17 . . . . . . . . . . . 12
182 simpr 463 . . . . . . . . . . . . . 14
183 simpl 459 . . . . . . . . . . . . . 14
184182, 183opeq12d 4174 . . . . . . . . . . . . 13
185184adantl 468 . . . . . . . . . . . 12
186181, 185eqtrd 2485 . . . . . . . . . . 11
187 elsn 3982 . . . . . . . . . . 11
188186, 187sylibr 216 . . . . . . . . . 10
189178, 188mtand 665 . . . . . . . . 9
190189adantl 468 . . . . . . . 8
191128, 129, 30, 131, 132, 190, 108etransclem38 38137 . . . . . . 7
192 dvdsmultr2 14340 . . . . . . 7
193177, 191, 192sylc 62 . . . . . 6
194193, 124breqtrrd 4429 . . . . 5
19593, 46, 140, 194fsumdvds 14348 . . . 4
196195, 117breqtrrd 4429 . . 3
19746, 103, 115, 142, 175, 196etransclem9 38108 . 2
198102, 197eqnetrd 2691 1
 Colors of variables: wff setvar class Syntax hints:   wn 3   wi 4   wb 188   wo 370   wa 371   w3a 985   wceq 1444   wcel 1887   wne 2622  crab 2741  cvv 3045   cdif 3401   wss 3404  cif 3881  csn 3968  cpr 3970  cop 3974   class class class wbr 4402   cmpt 4461   cxp 4832   crn 4835  wf 5578  cfv 5582  (class class class)co 6290  c1st 6791  c2nd 6792   cmap 7472  cfn 7569  cc 9537  cr 9538  cc0 9539  c1 9540   caddc 9542   cmul 9544   clt 9675   cle 9676   cmin 9860   cdiv 10269  cn 10609  cn0 10869  cz 10937  cuz 11159  cioo 11635  cfz 11784  cexp 12272  cfa 12459  cabs 13297  csu 13752  cprod 13959   cdvds 14305  cprime 14622   ↾t crest 15319  ctopn 15320  ctg 15336  ℂfldccnfld 18970   cdvn 22819 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-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-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-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-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-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-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-cj 13162  df-re 13163  df-im 13164  df-sqrt 13298  df-abs 13299  df-clim 13552  df-sum 13753  df-prod 13960  df-dvds 14306  df-gcd 14469  df-prm 14623  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-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-limc 22821  df-dv 22822  df-dvn 22823 This theorem is referenced by:  etransclem47  38146
 Copyright terms: Public domain W3C validator