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

Theorem ig1pdvds 20104
 Description: The monic generator of an ideal divides all elements of the ideal. (Contributed by Stefan O'Rear, 29-Mar-2015.)
Hypotheses
Ref Expression
ig1pval.p Poly1
ig1pval.g idlGen1p
ig1pcl.u LIdeal
ig1pdvds.d r
Assertion
Ref Expression
ig1pdvds

Proof of Theorem ig1pdvds
StepHypRef Expression
1 drngrng 15847 . . . . . . 7
2 ig1pval.p . . . . . . . 8 Poly1
32ply1rng 16647 . . . . . . 7
41, 3syl 16 . . . . . 6
543ad2ant1 979 . . . . 5
6 eqid 2438 . . . . . . . 8
7 ig1pcl.u . . . . . . . 8 LIdeal
86, 7lidlss 16285 . . . . . . 7
983ad2ant2 980 . . . . . 6
10 ig1pval.g . . . . . . . 8 idlGen1p
112, 10, 7ig1pcl 20103 . . . . . . 7
12113adant3 978 . . . . . 6
139, 12sseldd 3351 . . . . 5
14 ig1pdvds.d . . . . . 6 r
15 eqid 2438 . . . . . 6
166, 14, 15dvdsr01 15765 . . . . 5
175, 13, 16syl2anc 644 . . . 4
19 eleq2 2499 . . . . . 6
2019biimpac 474 . . . . 5
21203ad2antl3 1122 . . . 4
22 elsni 3840 . . . 4
2321, 22syl 16 . . 3
2418, 23breqtrrd 4241 . 2
25 simpl1 961 . . . . . . . 8
2625, 1syl 16 . . . . . . 7
27 simpl2 962 . . . . . . . . 9
2827, 8syl 16 . . . . . . . 8
29 simpl3 963 . . . . . . . 8
3028, 29sseldd 3351 . . . . . . 7
31 simpr 449 . . . . . . . . . 10
32 eqid 2438 . . . . . . . . . . 11 deg1 deg1
33 eqid 2438 . . . . . . . . . . 11 Monic1p Monic1p
342, 10, 15, 7, 32, 33ig1pval3 20102 . . . . . . . . . 10 Monic1p deg1 deg1
3525, 27, 31, 34syl3anc 1185 . . . . . . . . 9 Monic1p deg1 deg1
3635simp2d 971 . . . . . . . 8 Monic1p
37 eqid 2438 . . . . . . . . 9 Unic1p Unic1p
3837, 33mon1puc1p 20078 . . . . . . . 8 Monic1p Unic1p
3926, 36, 38syl2anc 644 . . . . . . 7 Unic1p
40 eqid 2438 . . . . . . . 8 rem1p rem1p
4140, 2, 6, 37, 32r1pdeglt 20086 . . . . . . 7 Unic1p deg1 rem1p deg1
4226, 30, 39, 41syl3anc 1185 . . . . . 6 deg1 rem1p deg1
4335simp3d 972 . . . . . 6 deg1 deg1
4442, 43breqtrd 4239 . . . . 5 deg1 rem1p deg1
4532, 2, 6deg1xrf 20009 . . . . . . 7 deg1
4635simp1d 970 . . . . . . . . . . 11
4728, 46sseldd 3351 . . . . . . . . . 10
48 eqid 2438 . . . . . . . . . . 11 quot1p quot1p
49 eqid 2438 . . . . . . . . . . 11
50 eqid 2438 . . . . . . . . . . 11
5140, 2, 6, 48, 49, 50r1pval 20084 . . . . . . . . . 10 rem1p quot1p
5230, 47, 51syl2anc 644 . . . . . . . . 9 rem1p quot1p
5326, 3syl 16 . . . . . . . . . 10
5448, 2, 6, 37q1pcl 20083 . . . . . . . . . . . 12 Unic1p quot1p
5526, 30, 39, 54syl3anc 1185 . . . . . . . . . . 11 quot1p
567, 6, 49lidlmcl 16293 . . . . . . . . . . 11 quot1p quot1p
5753, 27, 55, 46, 56syl22anc 1186 . . . . . . . . . 10 quot1p
587, 50lidlsubcl 16292 . . . . . . . . . 10 quot1p quot1p
5953, 27, 29, 57, 58syl22anc 1186 . . . . . . . . 9 quot1p
6052, 59eqeltrd 2512 . . . . . . . 8 rem1p
6128, 60sseldd 3351 . . . . . . 7 rem1p
62 ffvelrn 5871 . . . . . . 7 deg1 rem1p deg1 rem1p
6345, 61, 62sylancr 646 . . . . . 6 deg1 rem1p
6428ssdifd 3485 . . . . . . . . . 10
65 imass2 5243 . . . . . . . . . 10 deg1 deg1
6664, 65syl 16 . . . . . . . . 9 deg1 deg1
6732, 2, 15, 6deg1n0ima 20017 . . . . . . . . . . 11 deg1
6826, 67syl 16 . . . . . . . . . 10 deg1
69 nn0uz 10525 . . . . . . . . . 10
7068, 69syl6sseq 3396 . . . . . . . . 9 deg1
7166, 70sstrd 3360 . . . . . . . 8 deg1
72 uzssz 10510 . . . . . . . . 9
73 zssre 10294 . . . . . . . . . 10
74 ressxr 9134 . . . . . . . . . 10
7573, 74sstri 3359 . . . . . . . . 9
7672, 75sstri 3359 . . . . . . . 8
7771, 76syl6ss 3362 . . . . . . 7 deg1
787, 15lidl0cl 16288 . . . . . . . . . . . 12
7953, 27, 78syl2anc 644 . . . . . . . . . . 11
8079snssd 3945 . . . . . . . . . 10
8131necomd 2689 . . . . . . . . . 10
82 pssdifn0 3691 . . . . . . . . . 10
8380, 81, 82syl2anc 644 . . . . . . . . 9
84 ffn 5594 . . . . . . . . . . . 12 deg1 deg1
8545, 84ax-mp 5 . . . . . . . . . . 11 deg1
8628ssdifssd 3487 . . . . . . . . . . 11
87 fnimaeq0 5569 . . . . . . . . . . 11 deg1 deg1
8885, 86, 87sylancr 646 . . . . . . . . . 10 deg1
8988necon3bid 2638 . . . . . . . . 9 deg1
9083, 89mpbird 225 . . . . . . . 8 deg1
91 infmssuzcl 10564 . . . . . . . 8 deg1 deg1 deg1 deg1
9271, 90, 91syl2anc 644 . . . . . . 7 deg1 deg1
9377, 92sseldd 3351 . . . . . 6 deg1
94 xrltnle 9149 . . . . . 6 deg1 rem1p deg1 deg1 rem1p deg1 deg1 deg1 rem1p
9563, 93, 94syl2anc 644 . . . . 5 deg1 rem1p deg1 deg1 deg1 rem1p
9644, 95mpbid 203 . . . 4 deg1 deg1 rem1p
9771adantr 453 . . . . . . 7 rem1p deg1
9885a1i 11 . . . . . . . 8 rem1p deg1
9986adantr 453 . . . . . . . 8 rem1p
10060adantr 453 . . . . . . . . 9 rem1p rem1p
101 simpr 449 . . . . . . . . 9 rem1p rem1p
102 eldifsn 3929 . . . . . . . . 9 rem1p rem1p rem1p
103100, 101, 102sylanbrc 647 . . . . . . . 8 rem1p rem1p
104 fnfvima 5979 . . . . . . . 8 deg1 rem1p deg1 rem1p deg1
10598, 99, 103, 104syl3anc 1185 . . . . . . 7 rem1p deg1 rem1p deg1
106 infmssuzle 10563 . . . . . . 7 deg1 deg1 rem1p deg1 deg1 deg1 rem1p
10797, 105, 106syl2anc 644 . . . . . 6 rem1p deg1 deg1 rem1p
108107ex 425 . . . . 5 rem1p deg1 deg1 rem1p
109108necon1bd 2674 . . . 4 deg1 deg1 rem1p rem1p
11096, 109mpd 15 . . 3 rem1p
1112, 14, 6, 37, 15, 40dvdsr1p 20089 . . . 4 Unic1p rem1p
11226, 30, 39, 111syl3anc 1185 . . 3 rem1p
113110, 112mpbird 225 . 2
11424, 113pm2.61dane 2684 1
 Colors of variables: wff set class Syntax hints:   wn 3   wi 4   wb 178   wa 360   w3a 937   wceq 1653   wcel 1726   wne 2601   cdif 3319   wss 3322  c0 3630  csn 3816   class class class wbr 4215  ccnv 4880  cima 4884   wfn 5452  wf 5453  cfv 5457  (class class class)co 6084  csup 7448  cr 8994  cc0 8995  cxr 9124   clt 9125   cle 9126  cn0 10226  cz 10287  cuz 10493  cbs 13474  cmulr 13535  c0g 13728  csg 14693  crg 15665  rcdsr 15748  cdr 15840  LIdealclidl 16247  Poly1cpl1 16576   deg1 cdg1 19982  Monic1pcmn1 20053  Unic1pcuc1p 20054  quot1pcq1p 20055  rem1pcr1p 20056  idlGen1pcig1p 20057 This theorem is referenced by:  ig1prsp  20105 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-13 1728  ax-14 1730  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419  ax-rep 4323  ax-sep 4333  ax-nul 4341  ax-pow 4380  ax-pr 4406  ax-un 4704  ax-inf2 7599  ax-cnex 9051  ax-resscn 9052  ax-1cn 9053  ax-icn 9054  ax-addcl 9055  ax-addrcl 9056  ax-mulcl 9057  ax-mulrcl 9058  ax-mulcom 9059  ax-addass 9060  ax-mulass 9061  ax-distr 9062  ax-i2m1 9063  ax-1ne0 9064  ax-1rid 9065  ax-rnegex 9066  ax-rrecex 9067  ax-cnre 9068  ax-pre-lttri 9069  ax-pre-lttrn 9070  ax-pre-ltadd 9071  ax-pre-mulgt0 9072  ax-pre-sup 9073  ax-addf 9074  ax-mulf 9075 This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3or 938  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-eu 2287  df-mo 2288  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-nel 2604  df-ral 2712  df-rex 2713  df-reu 2714  df-rmo 2715  df-rab 2716  df-v 2960  df-sbc 3164  df-csb 3254  df-dif 3325  df-un 3327  df-in 3329  df-ss 3336  df-pss 3338  df-nul 3631  df-if 3742  df-pw 3803  df-sn 3822  df-pr 3823  df-tp 3824  df-op 3825  df-uni 4018  df-int 4053  df-iun 4097  df-iin 4098  df-br 4216  df-opab 4270  df-mpt 4271  df-tr 4306  df-eprel 4497  df-id 4501  df-po 4506  df-so 4507  df-fr 4544  df-se 4545  df-we 4546  df-ord 4587  df-on 4588  df-lim 4589  df-suc 4590  df-om 4849  df-xp 4887  df-rel 4888  df-cnv 4889  df-co 4890  df-dm 4891  df-rn 4892  df-res 4893  df-ima 4894  df-iota 5421  df-fun 5459  df-fn 5460  df-f 5461  df-f1 5462  df-fo 5463  df-f1o 5464  df-fv 5465  df-isom 5466  df-ov 6087  df-oprab 6088  df-mpt2 6089  df-of 6308  df-ofr 6309  df-1st 6352  df-2nd 6353  df-tpos 6482  df-riota 6552  df-recs 6636  df-rdg 6671  df-1o 6727  df-2o 6728  df-oadd 6731  df-er 6908  df-map 7023  df-pm 7024  df-ixp 7067  df-en 7113  df-dom 7114  df-sdom 7115  df-fin 7116  df-sup 7449  df-oi 7482  df-card 7831  df-pnf 9127  df-mnf 9128  df-xr 9129  df-ltxr 9130  df-le 9131  df-sub 9298  df-neg 9299  df-nn 10006  df-2 10063  df-3 10064  df-4 10065  df-5 10066  df-6 10067  df-7 10068  df-8 10069  df-9 10070  df-10 10071  df-n0 10227  df-z 10288  df-dec 10388  df-uz 10494  df-fz 11049  df-fzo 11141  df-seq 11329  df-hash 11624  df-struct 13476  df-ndx 13477  df-slot 13478  df-base 13479  df-sets 13480  df-ress 13481  df-plusg 13547  df-mulr 13548  df-starv 13549  df-sca 13550  df-vsca 13551  df-tset 13553  df-ple 13554  df-ds 13556  df-unif 13557  df-0g 13732  df-gsum 13733  df-mre 13816  df-mrc 13817  df-acs 13819  df-mnd 14695  df-mhm 14743  df-submnd 14744  df-grp 14817  df-minusg 14818  df-sbg 14819  df-mulg 14820  df-subg 14946  df-ghm 15009  df-cntz 15121  df-cmn 15419  df-abl 15420  df-mgp 15654  df-rng 15668  df-cring 15669  df-ur 15670  df-oppr 15733  df-dvdsr 15751  df-unit 15752  df-invr 15782  df-drng 15842  df-subrg 15871  df-lmod 15957  df-lss 16014  df-sra 16249  df-rgmod 16250  df-lidl 16251  df-rlreg 16348  df-ascl 16379  df-psr 16422  df-mvr 16423  df-mpl 16424  df-opsr 16430  df-psr1 16581  df-vr1 16582  df-ply1 16583  df-coe1 16586  df-cnfld 16709  df-mdeg 19983  df-deg1 19984  df-mon1 20058  df-uc1p 20059  df-q1p 20060  df-r1p 20061  df-ig1p 20062
 Copyright terms: Public domain W3C validator