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

Theorem zringlpirlem3 17998
Description: Lemma for zringlpir 17999. All elements of a nonzero ideal of integers are divided by the least one. (Contributed by Stefan O'Rear, 3-Jan-2015.) (Revised by AV, 9-Jun-2019.)
Hypotheses
Ref Expression
zringlpirlem.i
zringlpirlem.n0
zringlpirlem.g
zringlpirlem.x
Assertion
Ref Expression
zringlpirlem3

Proof of Theorem zringlpirlem3
StepHypRef Expression
1 zringlpirlem.i . . . . . . . . 9
2 zringbas 17982 . . . . . . . . . 10
3 eqid 2450 . . . . . . . . . 10
42, 3lidlss 17381 . . . . . . . . 9
51, 4syl 16 . . . . . . . 8
6 zringlpirlem.x . . . . . . . 8
75, 6sseldd 3439 . . . . . . 7
87zred 10832 . . . . . 6
9 inss2 3653 . . . . . . . 8
10 zringlpirlem.g . . . . . . . . 9
11 nnuz 10981 . . . . . . . . . . 11
129, 11sseqtri 3470 . . . . . . . . . 10
13 zringlpirlem.n0 . . . . . . . . . . 11
141, 13zringlpirlem1 17996 . . . . . . . . . 10
15 infmssuzcl 11023 . . . . . . . . . 10
1612, 14, 15sylancr 663 . . . . . . . . 9
1710, 16syl5eqel 2540 . . . . . . . 8
189, 17sseldi 3436 . . . . . . 7
1918nnrpd 11111 . . . . . 6
20 modlt 11803 . . . . . 6
218, 19, 20syl2anc 661 . . . . 5
227, 18zmodcld 11813 . . . . . . 7
2322nn0red 10722 . . . . . 6
2418nnred 10422 . . . . . 6
2523, 24ltnled 9606 . . . . 5
2621, 25mpbid 210 . . . 4
277zcnd 10833 . . . . . . . . . . 11
2818nncnd 10423 . . . . . . . . . . . 12
298, 18nndivred 10455 . . . . . . . . . . . . . 14
3029flcld 11733 . . . . . . . . . . . . 13
3130zcnd 10833 . . . . . . . . . . . 12
3228, 31mulcld 9491 . . . . . . . . . . 11
3327, 32negsubd 9810 . . . . . . . . . 10
3430znegcld 10834 . . . . . . . . . . . . . 14
3534zcnd 10833 . . . . . . . . . . . . 13
3635, 28mulcomd 9492 . . . . . . . . . . . 12
3728, 31mulneg2d 9883 . . . . . . . . . . . 12
3836, 37eqtrd 2490 . . . . . . . . . . 11
3938oveq2d 6190 . . . . . . . . . 10
40 modval 11795 . . . . . . . . . . 11
418, 19, 40syl2anc 661 . . . . . . . . . 10
4233, 39, 413eqtr4rd 2501 . . . . . . . . 9
43 zringrng 17979 . . . . . . . . . . 11
4443a1i 11 . . . . . . . . . 10
451, 13, 10zringlpirlem2 17997 . . . . . . . . . . 11
46 zringmulr 17985 . . . . . . . . . . . 12
473, 2, 46lidlmcl 17389 . . . . . . . . . . 11
4844, 1, 34, 45, 47syl22anc 1220 . . . . . . . . . 10
49 zringplusg 17983 . . . . . . . . . . 11
503, 49lidlacl 17385 . . . . . . . . . 10
5144, 1, 6, 48, 50syl22anc 1220 . . . . . . . . 9
5242, 51eqeltrd 2536 . . . . . . . 8
5352adantr 465 . . . . . . 7
54 simpr 461 . . . . . . 7
5553, 54elind 3622 . . . . . 6
56 infmssuzle 11022 . . . . . 6
5712, 55, 56sylancr 663 . . . . 5
5810, 57syl5eqbr 4407 . . . 4
5926, 58mtand 659 . . 3
60 elnn0 10666 . . . 4
6122, 60sylib 196 . . 3
62 orel1 382 . . 3
6359, 61, 62sylc 60 . 2
64 dvdsval3 13625 . . 3
6518, 7, 64syl2anc 661 . 2
6663, 65mpbird 232 1
Colors of variables: wff setvar class
Syntax hints:  -.wn 3  ->wi 4  <->wb 184  \/wo 368  /\wa 369  =wceq 1370  e.wcel 1757  =/=wne 2641  i^icin 3409  C_wss 3410   c0 3719  {csn 3959   class class class wbr 4374  `'ccnv 4921  `cfv 5500  (class class class)co 6174  supcsup 7775   cr 9366  0cc0 9367  1c1 9368   caddc 9370   cmul 9372   clt 9503   cle 9504   cmin 9680  -ucneg 9681   cdiv 10078   cn 10407   cn0 10664   cz 10731   cuz 10946   crp 11076   cfl 11725   cmo 11793   cdivides 13621   crg 16735   clidl 17341   zring 17976
This theorem is referenced by:  zringlpir  17999
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1709  ax-7 1729  ax-8 1759  ax-9 1761  ax-10 1776  ax-11 1781  ax-12 1793  ax-13 1944  ax-ext 2429  ax-rep 4485  ax-sep 4495  ax-nul 4503  ax-pow 4552  ax-pr 4613  ax-un 6456  ax-cnex 9423  ax-resscn 9424  ax-1cn 9425  ax-icn 9426  ax-addcl 9427  ax-addrcl 9428  ax-mulcl 9429  ax-mulrcl 9430  ax-mulcom 9431  ax-addass 9432  ax-mulass 9433  ax-distr 9434  ax-i2m1 9435  ax-1ne0 9436  ax-1rid 9437  ax-rnegex 9438  ax-rrecex 9439  ax-cnre 9440  ax-pre-lttri 9441  ax-pre-lttrn 9442  ax-pre-ltadd 9443  ax-pre-mulgt0 9444  ax-pre-sup 9445  ax-addf 9446  ax-mulf 9447
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1702  df-eu 2263  df-mo 2264  df-clab 2436  df-cleq 2442  df-clel 2445  df-nfc 2598  df-ne 2643  df-nel 2644  df-ral 2797  df-rex 2798  df-reu 2799  df-rmo 2800  df-rab 2801  df-v 3054  df-sbc 3269  df-csb 3371  df-dif 3413  df-un 3415  df-in 3417  df-ss 3424  df-pss 3426  df-nul 3720  df-if 3874  df-pw 3944  df-sn 3960  df-pr 3962  df-tp 3964  df-op 3966  df-uni 4174  df-int 4211  df-iun 4255  df-br 4375  df-opab 4433  df-mpt 4434  df-tr 4468  df-eprel 4714  df-id 4718  df-po 4723  df-so 4724  df-fr 4761  df-we 4763  df-ord 4804  df-on 4805  df-lim 4806  df-suc 4807  df-xp 4928  df-rel 4929  df-cnv 4930  df-co 4931  df-dm 4932  df-rn 4933  df-res 4934  df-ima 4935  df-iota 5463  df-fun 5502  df-fn 5503  df-f 5504  df-f1 5505  df-fo 5506  df-f1o 5507  df-fv 5508  df-riota 6135  df-ov 6177  df-oprab 6178  df-mpt2 6179  df-om 6561  df-1st 6661  df-2nd 6662  df-recs 6916  df-rdg 6950  df-1o 7004  df-oadd 7008  df-er 7185  df-en 7395  df-dom 7396  df-sdom 7397  df-fin 7398  df-sup 7776  df-pnf 9505  df-mnf 9506  df-xr 9507  df-ltxr 9508  df-le 9509  df-sub 9682  df-neg 9683  df-div 10079  df-nn 10408  df-2 10465  df-3 10466  df-4 10467  df-5 10468  df-6 10469  df-7 10470  df-8 10471  df-9 10472  df-10 10473  df-n0 10665  df-z 10732  df-dec 10841  df-uz 10947  df-rp 11077  df-fz 11523  df-fl 11727  df-mod 11794  df-seq 11892  df-exp 11951  df-cj 12674  df-re 12675  df-im 12676  df-sqr 12810  df-abs 12811  df-dvds 13622  df-struct 14262  df-ndx 14263  df-slot 14264  df-base 14265  df-sets 14266  df-ress 14267  df-plusg 14337  df-mulr 14338  df-starv 14339  df-sca 14340  df-vsca 14341  df-ip 14342  df-tset 14343  df-ple 14344  df-ds 14346  df-unif 14347  df-0g 14466  df-mnd 15501  df-grp 15631  df-minusg 15632  df-sbg 15633  df-subg 15764  df-cmn 16367  df-mgp 16681  df-ur 16693  df-rng 16737  df-cring 16738  df-subrg 16953  df-lmod 17040  df-lss 17104  df-sra 17343  df-rgmod 17344  df-lidl 17345  df-cnfld 17912  df-zring 17977
  Copyright terms: Public domain W3C validator