Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  srgbinomlem4 Structured version   Unicode version

Theorem srgbinomlem4 17711
 Description: Lemma 4 for srgbinomlem 17712. (Contributed by AV, 24-Aug-2019.) (Proof shortened by AV, 19-Nov-2019.)
Hypotheses
Ref Expression
srgbinom.s
srgbinom.m
srgbinom.t .g
srgbinom.a
srgbinom.g mulGrp
srgbinom.e .g
srgbinomlem.r SRing
srgbinomlem.a
srgbinomlem.b
srgbinomlem.c
srgbinomlem.n
srgbinomlem.i g
Assertion
Ref Expression
srgbinomlem4 g
Distinct variable groups:   ,   ,   ,   ,   ,   ,   ,   ,   ,
Allowed substitution hints:   ()   ()   ()

Proof of Theorem srgbinomlem4
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 srgbinomlem.i . . 3 g
21oveq1d 6320 . 2 g
3 srgbinom.s . . . 4
4 eqid 2429 . . . 4
5 srgbinom.a . . . 4
6 srgbinom.m . . . 4
7 srgbinomlem.r . . . 4 SRing
8 ovex 6333 . . . . 5
98a1i 11 . . . 4
10 srgbinomlem.b . . . 4
11 simpl 458 . . . . 5
12 srgbinomlem.n . . . . . 6
13 elfzelz 11798 . . . . . 6
14 bccl 12504 . . . . . 6
1512, 13, 14syl2an 479 . . . . 5
16 fznn0sub 11829 . . . . . 6
1716adantl 467 . . . . 5
18 elfznn0 11885 . . . . . 6
1918adantl 467 . . . . 5
20 srgbinom.t . . . . . 6 .g
21 srgbinom.g . . . . . 6 mulGrp
22 srgbinom.e . . . . . 6 .g
23 srgbinomlem.a . . . . . 6
24 srgbinomlem.c . . . . . 6
253, 6, 20, 5, 21, 22, 7, 23, 10, 24, 12srgbinomlem2 17709 . . . . 5
2611, 15, 17, 19, 25syl13anc 1266 . . . 4
27 eqid 2429 . . . . 5
28 fzfid 12183 . . . . 5
29 ovex 6333 . . . . . 6
3029a1i 11 . . . . 5
31 fvex 5891 . . . . . 6
3231a1i 11 . . . . 5
3327, 28, 30, 32fsuppmptdm 7900 . . . 4 finSupp
343, 4, 5, 6, 7, 9, 10, 26, 33srgsummulcr 17705 . . 3 g g
35 srgcmn 17677 . . . . . 6 SRing CMnd
367, 35syl 17 . . . . 5 CMnd
37 1z 10967 . . . . . 6
3837a1i 11 . . . . 5
39 0zd 10949 . . . . 5
4012nn0zd 11038 . . . . 5
417adantr 466 . . . . . 6 SRing
4210adantr 466 . . . . . 6
433, 6srgcl 17681 . . . . . 6 SRing
4441, 26, 42, 43syl3anc 1264 . . . . 5
45 oveq2 6313 . . . . . . 7
46 oveq2 6313 . . . . . . . . 9
4746oveq1d 6320 . . . . . . . 8
48 oveq1 6312 . . . . . . . 8
4947, 48oveq12d 6323 . . . . . . 7
5045, 49oveq12d 6323 . . . . . 6
5150oveq1d 6320 . . . . 5
523, 4, 36, 38, 39, 40, 44, 51gsummptshft 17504 . . . 4 g g
5312nn0cnd 10927 . . . . . . . . . . . . 13
5453adantr 466 . . . . . . . . . . . 12
55 elfzelz 11798 . . . . . . . . . . . . . 14
5655adantl 467 . . . . . . . . . . . . 13
5756zcnd 11041 . . . . . . . . . . . 12
58 1cnd 9658 . . . . . . . . . . . 12
5954, 57, 58subsub3d 10015 . . . . . . . . . . 11
6059oveq1d 6320 . . . . . . . . . 10
6160oveq1d 6320 . . . . . . . . 9
6261oveq2d 6321 . . . . . . . 8
6362oveq1d 6320 . . . . . . 7
647adantr 466 . . . . . . . . . 10 SRing
65 peano2zm 10980 . . . . . . . . . . . 12
6655, 65syl 17 . . . . . . . . . . 11
67 bccl 12504 . . . . . . . . . . 11
6812, 66, 67syl2an 479 . . . . . . . . . 10
6921srgmgp 17679 . . . . . . . . . . . . 13 SRing
707, 69syl 17 . . . . . . . . . . . 12
7170adantr 466 . . . . . . . . . . 11
72 0p1e1 10721 . . . . . . . . . . . . . . 15
7372oveq1i 6315 . . . . . . . . . . . . . 14
7473eleq2i 2507 . . . . . . . . . . . . 13
75 fznn0sub 11829 . . . . . . . . . . . . . 14
7675a1i 11 . . . . . . . . . . . . 13
7774, 76syl5bi 220 . . . . . . . . . . . 12
7877imp 430 . . . . . . . . . . 11
7923adantr 466 . . . . . . . . . . 11
8021, 3mgpbas 17664 . . . . . . . . . . . 12
8180, 22mulgnn0cl 16725 . . . . . . . . . . 11
8271, 78, 79, 81syl3anc 1264 . . . . . . . . . 10
83 elfznn 11826 . . . . . . . . . . . . . 14
84 nnm1nn0 10911 . . . . . . . . . . . . . 14
8583, 84syl 17 . . . . . . . . . . . . 13
8674, 85sylbi 198 . . . . . . . . . . . 12
8786adantl 467 . . . . . . . . . . 11
8810adantr 466 . . . . . . . . . . 11
8980, 22mulgnn0cl 16725 . . . . . . . . . . 11
9071, 87, 88, 89syl3anc 1264 . . . . . . . . . 10
913, 20, 6srgmulgass 17699 . . . . . . . . . 10 SRing
9264, 68, 82, 90, 91syl13anc 1266 . . . . . . . . 9
9392eqcomd 2437 . . . . . . . 8
9493oveq1d 6320 . . . . . . 7
95 srgmnd 17678 . . . . . . . . . . . 12 SRing
967, 95syl 17 . . . . . . . . . . 11
9796adantr 466 . . . . . . . . . 10
983, 20mulgnn0cl 16725 . . . . . . . . . 10
9997, 68, 82, 98syl3anc 1264 . . . . . . . . 9
1003, 6srgass 17682 . . . . . . . . 9 SRing
10164, 99, 90, 88, 100syl13anc 1266 . . . . . . . 8
10221, 6mgpplusg 17662 . . . . . . . . . . . 12
10380, 22, 102mulgnn0p1 16720 . . . . . . . . . . 11
104103eqcomd 2437 . . . . . . . . . 10
10571, 87, 88, 104syl3anc 1264 . . . . . . . . 9
106105oveq2d 6321 . . . . . . . 8
10755zcnd 11041 . . . . . . . . . . . 12
108 1cnd 9658 . . . . . . . . . . . 12
109107, 108npcand 9989 . . . . . . . . . . 11
110109adantl 467 . . . . . . . . . 10
111110oveq1d 6320 . . . . . . . . 9
112111oveq2d 6321 . . . . . . . 8
113101, 106, 1123eqtrd 2474 . . . . . . 7
11463, 94, 1133eqtrd 2474 . . . . . 6
115114mpteq2dva 4512 . . . . 5
116115oveq2d 6321 . . . 4 g g
117 mpteq1 4506 . . . . . . . 8
11873, 117ax-mp 5 . . . . . . 7
119 oveq1 6312 . . . . . . . . . . 11
120119oveq2d 6321 . . . . . . . . . 10
121 oveq2 6313 . . . . . . . . . . 11
122121oveq1d 6320 . . . . . . . . . 10
123120, 122oveq12d 6323 . . . . . . . . 9
124 oveq1 6312 . . . . . . . . 9
125123, 124oveq12d 6323 . . . . . . . 8
126125cbvmptv 4518 . . . . . . 7
127118, 126eqtri 2458 . . . . . 6
128127oveq2i 6316 . . . . 5 g g
129 fzfid 12183 . . . . . . . . 9
130 simpl 458 . . . . . . . . . . 11
131 elfzelz 11798 . . . . . . . . . . . . 13
132 peano2zm 10980 . . . . . . . . . . . . 13
133131, 132syl 17 . . . . . . . . . . . 12
134 bccl 12504 . . . . . . . . . . . 12
13512, 133, 134syl2an 479 . . . . . . . . . . 11
136 fznn0sub 11829 . . . . . . . . . . . 12
137136adantl 467 . . . . . . . . . . 11
138 elfznn 11826 . . . . . . . . . . . . 13
139138nnnn0d 10925 . . . . . . . . . . . 12
140139adantl 467 . . . . . . . . . . 11
1413, 6, 20, 5, 21, 22, 7, 23, 10, 24, 12srgbinomlem2 17709 . . . . . . . . . . 11
142130, 135, 137, 140, 141syl13anc 1266 . . . . . . . . . 10
143142ralrimiva 2846 . . . . . . . . 9
1443, 36, 129, 143gsummptcl 17534 . . . . . . . 8 g
1453, 5, 4mndlid 16508 . . . . . . . 8 g g g
14696, 144, 145syl2anc 665 . . . . . . 7 g g
147 0nn0 10884 . . . . . . . . . . 11
148147a1i 11 . . . . . . . . . 10
149 id 23 . . . . . . . . . . 11
150 0z 10948 . . . . . . . . . . . . . 14
151150, 37pm3.2i 456 . . . . . . . . . . . . 13
152 zsubcl 10979 . . . . . . . . . . . . 13
153151, 152mp1i 13 . . . . . . . . . . . 12
154 bccl 12504 . . . . . . . . . . . 12
15512, 153, 154syl2anc 665 . . . . . . . . . . 11
156 nn0cn 10879 . . . . . . . . . . . . . . 15
157 peano2cn 9804 . . . . . . . . . . . . . . 15
158156, 157syl 17 . . . . . . . . . . . . . 14
159158subid1d 9974 . . . . . . . . . . . . 13
160 peano2nn0 10910 . . . . . . . . . . . . 13
161159, 160eqeltrd 2517 . . . . . . . . . . . 12
16212, 161syl 17 . . . . . . . . . . 11
1633, 6, 20, 5, 21, 22, 7, 23, 10, 24, 12srgbinomlem2 17709 . . . . . . . . . . 11
164149, 155, 162, 148, 163syl13anc 1266 . . . . . . . . . 10
165 oveq1 6312 . . . . . . . . . . . . 13
166165oveq2d 6321 . . . . . . . . . . . 12
167 oveq2 6313 . . . . . . . . . . . . . 14
168167oveq1d 6320 . . . . . . . . . . . . 13
169 oveq1 6312 . . . . . . . . . . . . 13
170168, 169oveq12d 6323 . . . . . . . . . . . 12
171166, 170oveq12d 6323 . . . . . . . . . . 11
1723, 171gsumsn 17522 . . . . . . . . . 10 g
17396, 148, 164, 172syl3anc 1264 . . . . . . . . 9 g
174 0lt1 10135 . . . . . . . . . . . . . . 15
175174a1i 11 . . . . . . . . . . . . . 14
176175, 72syl6breqr 4466 . . . . . . . . . . . . 13
177 0re 9642 . . . . . . . . . . . . . . 15
178 1re 9641 . . . . . . . . . . . . . . 15
179177, 178, 1773pm3.2i 1183 . . . . . . . . . . . . . 14
180 ltsubadd 10083 . . . . . . . . . . . . . 14
181179, 180mp1i 13 . . . . . . . . . . . . 13
182176, 181mpbird 235 . . . . . . . . . . . 12
183182orcd 393 . . . . . . . . . . 11
184 bcval4 12489 . . . . . . . . . . 11
18512, 153, 183, 184syl3anc 1264 . . . . . . . . . 10
186185oveq1d 6320 . . . . . . . . 9
18780, 22mulgnn0cl 16725 . . . . . . . . . . . 12
18870, 162, 23, 187syl3anc 1264 . . . . . . . . . . 11
18980, 22mulgnn0cl 16725 . . . . . . . . . . . 12
19070, 148, 10, 189syl3anc 1264 . . . . . . . . . . 11
1913, 6srgcl 17681 . . . . . . . . . . 11 SRing
1927, 188, 190, 191syl3anc 1264 . . . . . . . . . 10
1933, 4, 20mulg0 16714 . . . . . . . . . 10
194192, 193syl 17 . . . . . . . . 9
195173, 186, 1943eqtrrd 2475 . . . . . . . 8 g
196195oveq1d 6320 . . . . . . 7 g g g
197146, 196eqtr3d 2472 . . . . . 6 g g g
1987adantr 466 . . . . . . . . 9 SRing
19970adantr 466 . . . . . . . . . 10
20023adantr 466 . . . . . . . . . 10
20180, 22mulgnn0cl 16725 . . . . . . . . . 10
202199, 137, 200, 201syl3anc 1264 . . . . . . . . 9
20310adantr 466 . . . . . . . . . 10
20480, 22mulgnn0cl 16725 . . . . . . . . . 10
205199, 140, 203, 204syl3anc 1264 . . . . . . . . 9
2063, 20, 6srgmulgass 17699 . . . . . . . . 9 SRing
207198, 135, 202, 205, 206syl13anc 1266 . . . . . . . 8
208207mpteq2dva 4512 . . . . . . 7
209208oveq2d 6321 . . . . . 6 g g
21012, 160syl 17 . . . . . . . 8
211 simpl 458 . . . . . . . . 9
212 elfzelz 11798 . . . . . . . . . . 11
213212, 132syl 17 . . . . . . . . . 10
21412, 213, 134syl2an 479 . . . . . . . . 9
215 fznn0sub 11829 . . . . . . . . . 10
216215adantl 467 . . . . . . . . 9
217 elfznn0 11885 . . . . . . . . . 10
218217adantl 467 . . . . . . . . 9
219211, 214, 216, 218, 141syl13anc 1266 . . . . . . . 8
2203, 5, 36, 210, 219gsummptfzsplitl 17501 . . . . . . 7 g g g
221 snfi 7657 . . . . . . . . . 10
222221a1i 11 . . . . . . . . 9
223171eleq1d 2498 . . . . . . . . . . . 12
224223ralsng 4037 . . . . . . . . . . 11
225147, 224ax-mp 5 . . . . . . . . . 10
226164, 225sylibr 215 . . . . . . . . 9
2273, 36, 222, 226gsummptcl 17534 . . . . . . . 8 g
2283, 5cmncom 17381 . . . . . . . 8 CMnd g g g g g g
22936, 144, 227, 228syl3anc 1264 . . . . . . 7 g g g g
230220, 229eqtrd 2470 . . . . . 6 g g g
231197, 209, 2303eqtr4d 2480 . . . . 5 g g
232128, 231syl5eq 2482 . . . 4 g g
23352, 116, 2323eqtrd 2474 . . 3 g g
23434, 233eqtr3d 2472 . 2 g g
2352, 234sylan9eqr 2492 1 g
 Colors of variables: wff setvar class Syntax hints:   wi 4   wb 187   wo 369   wa 370   w3a 982   wceq 1437   wcel 1870  wral 2782  cvv 3087  csn 4002   class class class wbr 4426   cmpt 4484  cfv 5601  (class class class)co 6305  cfn 7577  cc 9536  cr 9537  cc0 9538  c1 9539   caddc 9541   clt 9674   cmin 9859  cn 10609  cn0 10869  cz 10937  cfz 11782   cbc 12484  cbs 15084   cplusg 15152  cmulr 15153  c0g 15297   g cgsu 15298  cmnd 16486  .gcmg 16623  CMndccmn 17365  mulGrpcmgp 17658  SRingcsrg 17674 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-8 1872  ax-9 1874  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407  ax-rep 4538  ax-sep 4548  ax-nul 4556  ax-pow 4603  ax-pr 4661  ax-un 6597  ax-inf2 8146  ax-cnex 9594  ax-resscn 9595  ax-1cn 9596  ax-icn 9597  ax-addcl 9598  ax-addrcl 9599  ax-mulcl 9600  ax-mulrcl 9601  ax-mulcom 9602  ax-addass 9603  ax-mulass 9604  ax-distr 9605  ax-i2m1 9606  ax-1ne0 9607  ax-1rid 9608  ax-rnegex 9609  ax-rrecex 9610  ax-cnre 9611  ax-pre-lttri 9612  ax-pre-lttrn 9613  ax-pre-ltadd 9614  ax-pre-mulgt0 9615 This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-eu 2270  df-mo 2271  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-ne 2627  df-nel 2628  df-ral 2787  df-rex 2788  df-reu 2789  df-rmo 2790  df-rab 2791  df-v 3089  df-sbc 3306  df-csb 3402  df-dif 3445  df-un 3447  df-in 3449  df-ss 3456  df-pss 3458  df-nul 3768  df-if 3916  df-pw 3987  df-sn 4003  df-pr 4005  df-tp 4007  df-op 4009  df-uni 4223  df-int 4259  df-iun 4304  df-iin 4305  df-br 4427  df-opab 4485  df-mpt 4486  df-tr 4521  df-eprel 4765  df-id 4769  df-po 4775  df-so 4776  df-fr 4813  df-se 4814  df-we 4815  df-xp 4860  df-rel 4861  df-cnv 4862  df-co 4863  df-dm 4864  df-rn 4865  df-res 4866  df-ima 4867  df-pred 5399  df-ord 5445  df-on 5446  df-lim 5447  df-suc 5448  df-iota 5565  df-fun 5603  df-fn 5604  df-f 5605  df-f1 5606  df-fo 5607  df-f1o 5608  df-fv 5609  df-isom 5610  df-riota 6267  df-ov 6308  df-oprab 6309  df-mpt2 6310  df-of 6545  df-om 6707  df-1st 6807  df-2nd 6808  df-supp 6926  df-wrecs 7036  df-recs 7098  df-rdg 7136  df-1o 7190  df-oadd 7194  df-er 7371  df-map 7482  df-en 7578  df-dom 7579  df-sdom 7580  df-fin 7581  df-fsupp 7890  df-oi 8025  df-card 8372  df-pnf 9676  df-mnf 9677  df-xr 9678  df-ltxr 9679  df-le 9680  df-sub 9861  df-neg 9862  df-div 10269  df-nn 10610  df-2 10668  df-n0 10870  df-z 10938  df-uz 11160  df-rp 11303  df-fz 11783  df-fzo 11914  df-seq 12211  df-fac 12457  df-bc 12485  df-hash 12513  df-ndx 15087  df-slot 15088  df-base 15089  df-sets 15090  df-ress 15091  df-plusg 15165  df-0g 15299  df-gsum 15300  df-mre 15443  df-mrc 15444  df-acs 15446  df-mgm 16439  df-sgrp 16478  df-mnd 16488  df-mhm 16533  df-submnd 16534  df-mulg 16627  df-cntz 16922  df-cmn 17367  df-mgp 17659  df-srg 17675 This theorem is referenced by:  srgbinomlem  17712
 Copyright terms: Public domain W3C validator