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

Theorem lgseisenlem3 20590
 Description: Lemma for lgseisen 20592. (Contributed by Mario Carneiro, 17-Jun-2015.)
Hypotheses
Ref Expression
lgseisen.1
lgseisen.2
lgseisen.3
lgseisen.4
lgseisen.5
lgseisen.6
lgseisen.7 ℤ/n
lgseisen.8 mulGrp
lgseisen.9 RHom
Assertion
Ref Expression
lgseisenlem3 g
Distinct variable groups:   ,   ,   ,,   ,,   ,   ,,   ,   ,
Allowed substitution hints:   (,)   ()   ()   ()   ()   ()

Proof of Theorem lgseisenlem3
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 oveq2 5866 . . . . . . . . 9
21fveq2d 5529 . . . . . . . 8
32cbvmptv 4111 . . . . . . 7
43oveq2i 5869 . . . . . 6 g g
5 lgseisen.8 . . . . . . . 8 mulGrp
6 eqid 2283 . . . . . . . 8
75, 6mgpbas 15331 . . . . . . 7
8 eqid 2283 . . . . . . 7
9 lgseisen.1 . . . . . . . . . . 11
10 eldifi 3298 . . . . . . . . . . 11
119, 10syl 15 . . . . . . . . . 10
12 lgseisen.7 . . . . . . . . . . 11 ℤ/n
1312znfld 16514 . . . . . . . . . 10 Field
1411, 13syl 15 . . . . . . . . 9 Field
15 isfld 15521 . . . . . . . . . 10 Field
1615simprbi 450 . . . . . . . . 9 Field
1714, 16syl 15 . . . . . . . 8
185crngmgp 15349 . . . . . . . 8 CMnd
1917, 18syl 15 . . . . . . 7 CMnd
20 fzfid 11035 . . . . . . 7
21 crngrng 15351 . . . . . . . . . . . 12
2217, 21syl 15 . . . . . . . . . . 11
23 eqid 2283 . . . . . . . . . . . 12 flds flds
24 lgseisen.9 . . . . . . . . . . . 12 RHom
2523, 24zrhrhm 16466 . . . . . . . . . . 11 flds RingHom
2622, 25syl 15 . . . . . . . . . 10 flds RingHom
27 zsubrg 16425 . . . . . . . . . . . 12 SubRingfld
2823subrgbas 15554 . . . . . . . . . . . 12 SubRingfld flds
2927, 28ax-mp 8 . . . . . . . . . . 11 flds
3029, 6rhmf 15504 . . . . . . . . . 10 flds RingHom
3126, 30syl 15 . . . . . . . . 9
32 2z 10054 . . . . . . . . . 10
33 elfzelz 10798 . . . . . . . . . 10
34 zmulcl 10066 . . . . . . . . . 10
3532, 33, 34sylancr 644 . . . . . . . . 9
36 ffvelrn 5663 . . . . . . . . 9
3731, 35, 36syl2an 463 . . . . . . . 8
38 eqid 2283 . . . . . . . 8
3937, 38fmptd 5684 . . . . . . 7
4038mptpreima 5166 . . . . . . . . 9
41 ssrab2 3258 . . . . . . . . 9
4240, 41eqsstri 3208 . . . . . . . 8
43 ssfi 7083 . . . . . . . 8
4420, 42, 43sylancl 643 . . . . . . 7
45 lgseisen.2 . . . . . . . 8
46 lgseisen.3 . . . . . . . 8
47 lgseisen.4 . . . . . . . 8
48 lgseisen.5 . . . . . . . 8
49 lgseisen.6 . . . . . . . 8
509, 45, 46, 47, 48, 49lgseisenlem2 20589 . . . . . . 7
517, 8, 19, 20, 39, 44, 50gsumf1o 15199 . . . . . 6 g g
524, 51syl5eqr 2329 . . . . 5 g g
539, 45, 46, 47, 48lgseisenlem1 20588 . . . . . . . 8
5448fmpt 5681 . . . . . . . 8
5553, 54sylibr 203 . . . . . . 7
5648a1i 10 . . . . . . 7
57 eqidd 2284 . . . . . . 7
58 oveq2 5866 . . . . . . . 8
5958fveq2d 5529 . . . . . . 7
6055, 56, 57, 59fmptcof 5692 . . . . . 6
6160oveq2d 5874 . . . . 5 g g
62 eldifi 3298 . . . . . . . . . . . . . . . . . . . . . 22
6345, 62syl 15 . . . . . . . . . . . . . . . . . . . . 21
6463adantr 451 . . . . . . . . . . . . . . . . . . . 20
65 prmz 12762 . . . . . . . . . . . . . . . . . . . 20
6664, 65syl 15 . . . . . . . . . . . . . . . . . . 19
67 2nn 9877 . . . . . . . . . . . . . . . . . . . . 21
68 elfznn 10819 . . . . . . . . . . . . . . . . . . . . . 22
6968adantl 452 . . . . . . . . . . . . . . . . . . . . 21
70 nnmulcl 9769 . . . . . . . . . . . . . . . . . . . . 21
7167, 69, 70sylancr 644 . . . . . . . . . . . . . . . . . . . 20
7271nnzd 10116 . . . . . . . . . . . . . . . . . . 19
7366, 72zmulcld 10123 . . . . . . . . . . . . . . . . . 18
7411adantr 451 . . . . . . . . . . . . . . . . . . 19
75 prmnn 12761 . . . . . . . . . . . . . . . . . . 19
7674, 75syl 15 . . . . . . . . . . . . . . . . . 18
7773, 76zmodcld 10990 . . . . . . . . . . . . . . . . 17
7847, 77syl5eqel 2367 . . . . . . . . . . . . . . . 16
7978nn0zd 10115 . . . . . . . . . . . . . . 15
80 m1expcl 11126 . . . . . . . . . . . . . . 15
8179, 80syl 15 . . . . . . . . . . . . . 14
8281, 79zmulcld 10123 . . . . . . . . . . . . 13
8382, 76zmodcld 10990 . . . . . . . . . . . 12
8483nn0cnd 10020 . . . . . . . . . . 11
85 2cn 9816 . . . . . . . . . . . 12
8685a1i 10 . . . . . . . . . . 11
87 2ne0 9829 . . . . . . . . . . . 12
8887a1i 10 . . . . . . . . . . 11
8984, 86, 88divcan2d 9538 . . . . . . . . . 10
9089fveq2d 5529 . . . . . . . . 9
9176nnrpd 10389 . . . . . . . . . . . . 13
92 eqidd 2284 . . . . . . . . . . . . 13
9347oveq1i 5868 . . . . . . . . . . . . . 14
9473zred 10117 . . . . . . . . . . . . . . 15
95 modabs2 10998 . . . . . . . . . . . . . . 15
9694, 91, 95syl2anc 642 . . . . . . . . . . . . . 14
9793, 96syl5eq 2327 . . . . . . . . . . . . 13
9881, 81, 79, 73, 91, 92, 97modmul12d 11003 . . . . . . . . . . . 12
9982zred 10117 . . . . . . . . . . . . 13
100 modabs2 10998 . . . . . . . . . . . . 13
10199, 91, 100syl2anc 642 . . . . . . . . . . . 12
10281zcnd 10118 . . . . . . . . . . . . . 14
10366zcnd 10118 . . . . . . . . . . . . . 14
10472zcnd 10118 . . . . . . . . . . . . . 14
105102, 103, 104mulassd 8858 . . . . . . . . . . . . 13
106105oveq1d 5873 . . . . . . . . . . . 12
10798, 101, 1063eqtr4d 2325 . . . . . . . . . . 11
10811, 75syl 15 . . . . . . . . . . . . 13
109108adantr 451 . . . . . . . . . . . 12
11083nn0zd 10115 . . . . . . . . . . . 12
11181, 66zmulcld 10123 . . . . . . . . . . . . 13
112111, 72zmulcld 10123 . . . . . . . . . . . 12
113 moddvds 12538 . . . . . . . . . . . 12
114109, 110, 112, 113syl3anc 1182 . . . . . . . . . . 11
115107, 114mpbid 201 . . . . . . . . . 10
11676nnnn0d 10018 . . . . . . . . . . 11
11712, 24zndvds 16503 . . . . . . . . . . 11
118116, 110, 112, 117syl3anc 1182 . . . . . . . . . 10
119115, 118mpbird 223 . . . . . . . . 9
12026adantr 451 . . . . . . . . . 10 flds RingHom
121 cnfldmul 16385 . . . . . . . . . . . . 13 fld
12223, 121ressmulr 13261 . . . . . . . . . . . 12 SubRingfld flds
12327, 122ax-mp 8 . . . . . . . . . . 11 flds
124 eqid 2283 . . . . . . . . . . 11
12529, 123, 124rhmmul 15505 . . . . . . . . . 10 flds RingHom
126120, 111, 72, 125syl3anc 1182 . . . . . . . . 9
12790, 119, 1263eqtrd 2319 . . . . . . . 8
128127mpteq2dva 4106 . . . . . . 7
12931adantr 451 . . . . . . . . 9
130 ffvelrn 5663 . . . . . . . . 9
131129, 111, 130syl2anc 642 . . . . . . . 8
132 ffvelrn 5663 . . . . . . . . 9
133129, 72, 132syl2anc 642 . . . . . . . 8
134 eqidd 2284 . . . . . . . 8
135 eqidd 2284 . . . . . . . 8
13620, 131, 133, 134, 135offval2 6095 . . . . . . 7
137128, 136eqtr4d 2318 . . . . . 6
138137oveq2d 5874 . . . . 5 g g
13952, 61, 1383eqtrd 2319 . . . 4 g g
1405, 124mgpplusg 15329 . . . . 5
141 eqid 2283 . . . . . 6
142131, 141fmptd 5684 . . . . 5
143 eqid 2283 . . . . . 6
144133, 143fmptd 5684 . . . . 5
145141mptpreima 5166 . . . . . . 7
146 ssrab2 3258 . . . . . . 7
147145, 146eqsstri 3208 . . . . . 6
148 ssfi 7083 . . . . . 6
14920, 147, 148sylancl 643 . . . . 5
15020, 144fisuppfi 14450 . . . . 5
1517, 8, 140, 19, 20, 142, 144, 149, 150gsumadd 15205 . . . 4 g g g
152139, 151eqtrd 2315 . . 3 g g g
153152oveq1d 5873 . 2 g /r g g g /r g
154 eqid 2283 . . . . . 6 Unit Unit
155154, 5unitsubm 15452 . . . . 5 Unit SubMnd
15622, 155syl 15 . . . 4 Unit SubMnd
157 elfzle2 10800 . . . . . . . . . . 11
158157adantl 452 . . . . . . . . . 10
15969nnred 9761 . . . . . . . . . . 11
160 prmuz2 12776 . . . . . . . . . . . . 13
161 uz2m1nn 10292 . . . . . . . . . . . . 13
16274, 160, 1613syl 18 . . . . . . . . . . . 12
163162nnred 9761 . . . . . . . . . . 11
164 2re 9815 . . . . . . . . . . . 12
165164a1i 10 . . . . . . . . . . 11
166 2pos 9828 . . . . . . . . . . . 12
167166a1i 10 . . . . . . . . . . 11
168 lemuldiv2 9636 . . . . . . . . . . 11
169159, 163, 165, 167, 168syl112anc 1186 . . . . . . . . . 10
170158, 169mpbird 223 . . . . . . . . 9
171 prmz 12762 . . . . . . . . . . . 12
17274, 171syl 15 . . . . . . . . . . 11
173 peano2zm 10062 . . . . . . . . . . 11
174172, 173syl 15 . . . . . . . . . 10
175 fznn 10852 . . . . . . . . . 10
176174, 175syl 15 . . . . . . . . 9
17771, 170, 176mpbir2and 888 . . . . . . . 8
178 fzm1ndvds 12580 . . . . . . . 8
17976, 177, 178syl2anc 642 . . . . . . 7
180 eqid 2283 . . . . . . . . . 10
18112, 24, 180zndvds0 16504 . . . . . . . . 9
182116, 72, 181syl2anc 642 . . . . . . . 8
183182necon3abid 2479 . . . . . . 7
184179, 183mpbird 223 . . . . . 6
18515simplbi 446 . . . . . . . . 9 Field
18614, 185syl 15 . . . . . . . 8
187186adantr 451 . . . . . . 7
1886, 154, 180drngunit 15517 . . . . . . 7 Unit
189187, 188syl 15 . . . . . 6 Unit
190133, 184, 189mpbir2and 888 . . . . 5 Unit
191190, 143fmptd 5684 . . . 4 Unit
1928, 19, 20, 156, 191, 150gsumsubmcl 15201 . . 3 g Unit
193 eqid 2283 . . . 4 /r /r
194 eqid 2283 . . . 4
195154, 193, 194dvrid 15470 . . 3 g Unit g /r g
19622, 192, 195syl2anc 642 . 2 g /r g
1977, 8, 19, 20, 142, 149gsumcl 15198 . . 3 g
1986, 154, 193, 124dvrcan3 15474 . . 3 g g Unit g g /r g g
19922, 197, 192, 198syl3anc 1182 . 2 g g /r g g
200153, 196, 1993eqtr3rd 2324 1 g
 Colors of variables: wff set class Syntax hints:   wn 3   wi 4   wb 176   wa 358   wceq 1623   wcel 1684   wne 2446  wral 2543  crab 2547  cvv 2788   cdif 3149   wss 3152  csn 3640   class class class wbr 4023   cmpt 4077  ccnv 4688  cima 4692   ccom 4693  wf 5251  cfv 5255  (class class class)co 5858   cof 6076  cfn 6863  cc 8735  cr 8736  cc0 8737  c1 8738   cmul 8742   clt 8867   cle 8868   cmin 9037  cneg 9038   cdiv 9423  cn 9746  c2 9795  cn0 9965  cz 10024  cuz 10230  crp 10354  cfz 10782   cmo 10973  cexp 11104   cdivides 12531  cprime 12758  cbs 13148   ↾s cress 13149  cmulr 13209  c0g 13400   g cgsu 13401  SubMndcsubmnd 14414  CMndccmn 15089  mulGrpcmgp 15325  crg 15337  ccrg 15338  cur 15339  Unitcui 15421  /rcdvr 15464   RingHom crh 15494  cdr 15512  Fieldcfield 15513  SubRingcsubrg 15541  ℂfldccnfld 16377  RHomczrh 16451  ℤ/nℤczn 16454 This theorem is referenced by:  lgseisenlem4  20591 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-13 1686  ax-14 1688  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-rep 4131  ax-sep 4141  ax-nul 4149  ax-pow 4188  ax-pr 4214  ax-un 4512  ax-inf2 7342  ax-cnex 8793  ax-resscn 8794  ax-1cn 8795  ax-icn 8796  ax-addcl 8797  ax-addrcl 8798  ax-mulcl 8799  ax-mulrcl 8800  ax-mulcom 8801  ax-addass 8802  ax-mulass 8803  ax-distr 8804  ax-i2m1 8805  ax-1ne0 8806  ax-1rid 8807  ax-rnegex 8808  ax-rrecex 8809  ax-cnre 8810  ax-pre-lttri 8811  ax-pre-lttrn 8812  ax-pre-ltadd 8813  ax-pre-mulgt0 8814  ax-pre-sup 8815  ax-addf 8816  ax-mulf 8817 This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-eu 2147  df-mo 2148  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448  df-nel 2449  df-ral 2548  df-rex 2549  df-reu 2550  df-rmo 2551  df-rab 2552  df-v 2790  df-sbc 2992  df-csb 3082  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-pss 3168  df-nul 3456  df-if 3566  df-pw 3627  df-sn 3646  df-pr 3647  df-tp 3648  df-op 3649  df-uni 3828  df-int 3863  df-iun 3907  df-br 4024  df-opab 4078  df-mpt 4079  df-tr 4114  df-eprel 4305  df-id 4309  df-po 4314  df-so 4315  df-fr 4352  df-se 4353  df-we 4354  df-ord 4395  df-on 4396  df-lim 4397  df-suc 4398  df-om 4657  df-xp 4695  df-rel 4696  df-cnv 4697  df-co 4698  df-dm 4699  df-rn 4700  df-res 4701  df-ima 4702  df-iota 5219  df-fun 5257  df-fn 5258  df-f 5259  df-f1 5260  df-fo 5261  df-f1o 5262  df-fv 5263  df-isom 5264  df-ov 5861  df-oprab 5862  df-mpt2 5863  df-of 6078  df-1st 6122  df-2nd 6123  df-tpos 6234  df-riota 6304  df-recs 6388  df-rdg 6423  df-1o 6479  df-2o 6480  df-oadd 6483  df-er 6660  df-ec 6662  df-qs 6666  df-map 6774  df-en 6864  df-dom 6865  df-sdom 6866  df-fin 6867  df-sup 7194  df-oi 7225  df-card 7572  df-cda 7794  df-pnf 8869  df-mnf 8870  df-xr 8871  df-ltxr 8872  df-le 8873  df-sub 9039  df-neg 9040  df-div 9424  df-nn 9747  df-2 9804  df-3 9805  df-4 9806  df-5 9807  df-6 9808  df-7 9809  df-8 9810  df-9 9811  df-10 9812  df-n0 9966  df-z 10025  df-dec 10125  df-uz 10231  df-rp 10355  df-fz 10783  df-fzo 10871  df-fl 10925  df-mod 10974  df-seq 11047  df-exp 11105  df-hash 11338  df-cj 11584  df-re 11585  df-im 11586  df-sqr 11720  df-abs 11721  df-dvds 12532  df-gcd 12686  df-prm 12759  df-struct 13150  df-ndx 13151  df-slot 13152  df-base 13153  df-sets 13154  df-ress 13155  df-plusg 13221  df-mulr 13222  df-starv 13223  df-sca 13224  df-vsca 13225  df-tset 13227  df-ple 13228  df-ds 13230  df-0g 13404  df-gsum 13405  df-imas 13411  df-divs 13412  df-mnd 14367  df-mhm 14415  df-submnd 14416  df-grp 14489  df-minusg 14490  df-sbg 14491  df-mulg 14492  df-subg 14618  df-nsg 14619  df-eqg 14620  df-ghm 14681  df-cntz 14793  df-cmn 15091  df-abl 15092  df-mgp 15326  df-rng 15340  df-cring 15341  df-ur 15342  df-oppr 15405  df-dvdsr 15423  df-unit 15424  df-invr 15454  df-dvr 15465  df-rnghom 15496  df-drng 15514  df-field 15515  df-subrg 15543  df-lmod 15629  df-lss 15690  df-lsp 15729  df-sra 15925  df-rgmod 15926  df-lidl 15927  df-rsp 15928  df-2idl 15984  df-nzr 16010  df-rlreg 16024  df-domn 16025  df-idom 16026  df-cnfld 16378  df-zrh 16455  df-zn 16458
 Copyright terms: Public domain W3C validator