![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > MPE Home > Th. List > zringlpirlem3 | Unicode version |
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.) |
Ref | Expression |
---|---|
zringlpirlem.i | |
zringlpirlem.n0 | |
zringlpirlem.g | |
zringlpirlem.x |
Ref | Expression |
---|---|
zringlpirlem3 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | zringlpirlem.i | . . . . . . . . 9 | |
2 | zringbas 17982 | . . . . . . . . . 10 | |
3 | eqid 2450 | . . . . . . . . . 10 | |
4 | 2, 3 | lidlss 17381 | . . . . . . . . 9 |
5 | 1, 4 | syl 16 | . . . . . . . 8 |
6 | zringlpirlem.x | . . . . . . . 8 | |
7 | 5, 6 | sseldd 3439 | . . . . . . 7 |
8 | 7 | zred 10832 | . . . . . 6 |
9 | inss2 3653 | . . . . . . . 8 | |
10 | zringlpirlem.g | . . . . . . . . 9 | |
11 | nnuz 10981 | . . . . . . . . . . 11 | |
12 | 9, 11 | sseqtri 3470 | . . . . . . . . . 10 |
13 | zringlpirlem.n0 | . . . . . . . . . . 11 | |
14 | 1, 13 | zringlpirlem1 17996 | . . . . . . . . . 10 |
15 | infmssuzcl 11023 | . . . . . . . . . 10 | |
16 | 12, 14, 15 | sylancr 663 | . . . . . . . . 9 |
17 | 10, 16 | syl5eqel 2540 | . . . . . . . 8 |
18 | 9, 17 | sseldi 3436 | . . . . . . 7 |
19 | 18 | nnrpd 11111 | . . . . . 6 |
20 | modlt 11803 | . . . . . 6 | |
21 | 8, 19, 20 | syl2anc 661 | . . . . 5 |
22 | 7, 18 | zmodcld 11813 | . . . . . . 7 |
23 | 22 | nn0red 10722 | . . . . . 6 |
24 | 18 | nnred 10422 | . . . . . 6 |
25 | 23, 24 | ltnled 9606 | . . . . 5 |
26 | 21, 25 | mpbid 210 | . . . 4 |
27 | 7 | zcnd 10833 | . . . . . . . . . . 11 |
28 | 18 | nncnd 10423 | . . . . . . . . . . . 12 |
29 | 8, 18 | nndivred 10455 | . . . . . . . . . . . . . 14 |
30 | 29 | flcld 11733 | . . . . . . . . . . . . 13 |
31 | 30 | zcnd 10833 | . . . . . . . . . . . 12 |
32 | 28, 31 | mulcld 9491 | . . . . . . . . . . 11 |
33 | 27, 32 | negsubd 9810 | . . . . . . . . . 10 |
34 | 30 | znegcld 10834 | . . . . . . . . . . . . . 14 |
35 | 34 | zcnd 10833 | . . . . . . . . . . . . 13 |
36 | 35, 28 | mulcomd 9492 | . . . . . . . . . . . 12 |
37 | 28, 31 | mulneg2d 9883 | . . . . . . . . . . . 12 |
38 | 36, 37 | eqtrd 2490 | . . . . . . . . . . 11 |
39 | 38 | oveq2d 6190 | . . . . . . . . . 10 |
40 | modval 11795 | . . . . . . . . . . 11 | |
41 | 8, 19, 40 | syl2anc 661 | . . . . . . . . . 10 |
42 | 33, 39, 41 | 3eqtr4rd 2501 | . . . . . . . . 9 |
43 | zringrng 17979 | . . . . . . . . . . 11 | |
44 | 43 | a1i 11 | . . . . . . . . . 10 |
45 | 1, 13, 10 | zringlpirlem2 17997 | . . . . . . . . . . 11 |
46 | zringmulr 17985 | . . . . . . . . . . . 12 | |
47 | 3, 2, 46 | lidlmcl 17389 | . . . . . . . . . . 11 |
48 | 44, 1, 34, 45, 47 | syl22anc 1220 | . . . . . . . . . 10 |
49 | zringplusg 17983 | . . . . . . . . . . 11 | |
50 | 3, 49 | lidlacl 17385 | . . . . . . . . . 10 |
51 | 44, 1, 6, 48, 50 | syl22anc 1220 | . . . . . . . . 9 |
52 | 42, 51 | eqeltrd 2536 | . . . . . . . 8 |
53 | 52 | adantr 465 | . . . . . . 7 |
54 | simpr 461 | . . . . . . 7 | |
55 | 53, 54 | elind 3622 | . . . . . 6 |
56 | infmssuzle 11022 | . . . . . 6 | |
57 | 12, 55, 56 | sylancr 663 | . . . . 5 |
58 | 10, 57 | syl5eqbr 4407 | . . . 4 |
59 | 26, 58 | mtand 659 | . . 3 |
60 | elnn0 10666 | . . . 4 | |
61 | 22, 60 | sylib 196 | . . 3 |
62 | orel1 382 | . . 3 | |
63 | 59, 61, 62 | sylc 60 | . 2 |
64 | dvdsval3 13625 | . . 3 | |
65 | 18, 7, 64 | syl2anc 661 | . 2 |
66 | 63, 65 | mpbird 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^i cin 3409 C_ wss 3410 c0 3719 { csn 3959 class class class wbr 4374
`' ccnv 4921 ` cfv 5500 (class class class)co 6174
sup csup 7775
cr 9366 0 cc0 9367 1 c1 9368
caddc 9370 cmul 9372 clt 9503 cle 9504 cmin 9680 -u cneg 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 |