Mathbox for Stefan O'Rear < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  hbtlem5 Structured version   Unicode version

Theorem hbtlem5 27311
 Description: The leading ideal function is strictly monotone. (Contributed by Stefan O'Rear, 1-Apr-2015.)
Hypotheses
Ref Expression
hbtlem.p Poly1
hbtlem.u LIdeal
hbtlem.s ldgIdlSeq
hbtlem3.r
hbtlem3.i
hbtlem3.j
hbtlem3.ij
hbtlem5.e
Assertion
Ref Expression
hbtlem5
Distinct variable groups:   ,   ,   ,
Allowed substitution hints:   ()   ()   ()   ()

Proof of Theorem hbtlem5
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 hbtlem3.ij . 2
2 hbtlem3.j . . . . . . . . 9
3 eqid 2438 . . . . . . . . . 10
4 hbtlem.u . . . . . . . . . 10 LIdeal
53, 4lidlss 16282 . . . . . . . . 9
62, 5syl 16 . . . . . . . 8
76sselda 3350 . . . . . . 7
8 eqid 2438 . . . . . . . 8 deg1 deg1
9 hbtlem.p . . . . . . . 8 Poly1
108, 9, 3deg1cl 20008 . . . . . . 7 deg1
117, 10syl 16 . . . . . 6 deg1
12 elun 3490 . . . . . . 7 deg1 deg1 deg1
13 nnssnn0 10226 . . . . . . . . 9
14 nn0re 10232 . . . . . . . . . 10 deg1 deg1
15 arch 10220 . . . . . . . . . 10 deg1 deg1
1614, 15syl 16 . . . . . . . . 9 deg1 deg1
17 ssrexv 3410 . . . . . . . . 9 deg1 deg1
1813, 16, 17mpsyl 62 . . . . . . . 8 deg1 deg1
19 elsni 3840 . . . . . . . . 9 deg1 deg1
20 0nn0 10238 . . . . . . . . . . 11
21 0re 9093 . . . . . . . . . . . 12
22 mnflt 10724 . . . . . . . . . . . 12
2321, 22ax-mp 8 . . . . . . . . . . 11
24 breq2 4218 . . . . . . . . . . . 12
2524rspcev 3054 . . . . . . . . . . 11
2620, 23, 25mp2an 655 . . . . . . . . . 10
27 breq1 4217 . . . . . . . . . . 11 deg1 deg1
2827rexbidv 2728 . . . . . . . . . 10 deg1 deg1
2926, 28mpbiri 226 . . . . . . . . 9 deg1 deg1
3019, 29syl 16 . . . . . . . 8 deg1 deg1
3118, 30jaoi 370 . . . . . . 7 deg1 deg1 deg1
3212, 31sylbi 189 . . . . . 6 deg1 deg1
3311, 32syl 16 . . . . 5 deg1
34 breq2 4218 . . . . . . . . . . . . 13 deg1 deg1
3534imbi1d 310 . . . . . . . . . . . 12 deg1 deg1
3635ralbidv 2727 . . . . . . . . . . 11 deg1 deg1
3736imbi2d 309 . . . . . . . . . 10 deg1 deg1
38 breq2 4218 . . . . . . . . . . . . 13 deg1 deg1
3938imbi1d 310 . . . . . . . . . . . 12 deg1 deg1
4039ralbidv 2727 . . . . . . . . . . 11 deg1 deg1
4140imbi2d 309 . . . . . . . . . 10 deg1 deg1
42 breq2 4218 . . . . . . . . . . . . . 14 deg1 deg1
4342imbi1d 310 . . . . . . . . . . . . 13 deg1 deg1
4443ralbidv 2727 . . . . . . . . . . . 12 deg1 deg1
45 fveq2 5730 . . . . . . . . . . . . . . 15 deg1 deg1
4645breq1d 4224 . . . . . . . . . . . . . 14 deg1 deg1
47 eleq1 2498 . . . . . . . . . . . . . 14
4846, 47imbi12d 313 . . . . . . . . . . . . 13 deg1 deg1
4948cbvralv 2934 . . . . . . . . . . . 12 deg1 deg1
5044, 49syl6bb 254 . . . . . . . . . . 11 deg1 deg1
5150imbi2d 309 . . . . . . . . . 10 deg1 deg1
52 hbtlem3.r . . . . . . . . . . . . . 14
5352adantr 453 . . . . . . . . . . . . 13
54 eqid 2438 . . . . . . . . . . . . . 14
558, 9, 54, 3deg1lt0 20016 . . . . . . . . . . . . 13 deg1
5653, 7, 55syl2anc 644 . . . . . . . . . . . 12 deg1
579ply1rng 16644 . . . . . . . . . . . . . . . 16
5852, 57syl 16 . . . . . . . . . . . . . . 15
59 hbtlem3.i . . . . . . . . . . . . . . 15
604, 54lidl0cl 16285 . . . . . . . . . . . . . . 15
6158, 59, 60syl2anc 644 . . . . . . . . . . . . . 14
62 eleq1a 2507 . . . . . . . . . . . . . 14
6361, 62syl 16 . . . . . . . . . . . . 13
6463adantr 453 . . . . . . . . . . . 12
6556, 64sylbid 208 . . . . . . . . . . 11 deg1
6665ralrimiva 2791 . . . . . . . . . 10 deg1
6763ad2ant2 980 . . . . . . . . . . . . . . . . 17 deg1
6867sselda 3350 . . . . . . . . . . . . . . . 16 deg1
698, 9, 3deg1cl 20008 . . . . . . . . . . . . . . . 16 deg1
7068, 69syl 16 . . . . . . . . . . . . . . 15 deg1 deg1
71 simpl1 961 . . . . . . . . . . . . . . . 16 deg1
7271nn0zd 10375 . . . . . . . . . . . . . . 15 deg1
73 degltp1le 19998 . . . . . . . . . . . . . . 15 deg1 deg1 deg1
7470, 72, 73syl2anc 644 . . . . . . . . . . . . . 14 deg1 deg1 deg1
75 hbtlem5.e . . . . . . . . . . . . . . . . . . . . 21
76 fveq2 5730 . . . . . . . . . . . . . . . . . . . . . . 23
77 fveq2 5730 . . . . . . . . . . . . . . . . . . . . . . 23
7876, 77sseq12d 3379 . . . . . . . . . . . . . . . . . . . . . 22
7978rspcva 3052 . . . . . . . . . . . . . . . . . . . . 21
8075, 79sylan2 462 . . . . . . . . . . . . . . . . . . . 20
8152adantl 454 . . . . . . . . . . . . . . . . . . . . 21
822adantl 454 . . . . . . . . . . . . . . . . . . . . 21
83 simpl 445 . . . . . . . . . . . . . . . . . . . . 21
84 hbtlem.s . . . . . . . . . . . . . . . . . . . . . 22 ldgIdlSeq
859, 4, 84, 8hbtlem1 27306 . . . . . . . . . . . . . . . . . . . . 21 deg1 coe1
8681, 82, 83, 85syl3anc 1185 . . . . . . . . . . . . . . . . . . . 20 deg1 coe1
8759adantl 454 . . . . . . . . . . . . . . . . . . . . 21
889, 4, 84, 8hbtlem1 27306 . . . . . . . . . . . . . . . . . . . . 21 deg1 coe1
8981, 87, 83, 88syl3anc 1185 . . . . . . . . . . . . . . . . . . . 20 deg1 coe1
9080, 86, 893sstr3d 3392 . . . . . . . . . . . . . . . . . . 19 deg1 coe1 deg1 coe1
91903adant3 978 . . . . . . . . . . . . . . . . . 18 deg1 deg1 coe1 deg1 coe1
9291adantr 453 . . . . . . . . . . . . . . . . 17 deg1 deg1 deg1 coe1 deg1 coe1
93 simpl 445 . . . . . . . . . . . . . . . . . . . 20 deg1
94 simpr 449 . . . . . . . . . . . . . . . . . . . 20 deg1 deg1
95 eqidd 2439 . . . . . . . . . . . . . . . . . . . 20 deg1 coe1 coe1
96 fveq2 5730 . . . . . . . . . . . . . . . . . . . . . . 23 deg1 deg1
9796breq1d 4224 . . . . . . . . . . . . . . . . . . . . . 22 deg1 deg1
98 fveq2 5730 . . . . . . . . . . . . . . . . . . . . . . . 24 coe1 coe1
9998fveq1d 5732 . . . . . . . . . . . . . . . . . . . . . . 23 coe1 coe1
10099eqeq2d 2449 . . . . . . . . . . . . . . . . . . . . . 22 coe1 coe1 coe1 coe1
10197, 100anbi12d 693 . . . . . . . . . . . . . . . . . . . . 21 deg1 coe1 coe1 deg1 coe1 coe1
102101rspcev 3054 . . . . . . . . . . . . . . . . . . . 20 deg1 coe1 coe1 deg1 coe1 coe1
10393, 94, 95, 102syl12anc 1183 . . . . . . . . . . . . . . . . . . 19 deg1 deg1 coe1 coe1
104 fvex 5744 . . . . . . . . . . . . . . . . . . . 20 coe1
105 eqeq1 2444 . . . . . . . . . . . . . . . . . . . . . 22 coe1 coe1 coe1 coe1
106105anbi2d 686 . . . . . . . . . . . . . . . . . . . . 21 coe1 deg1 coe1 deg1 coe1 coe1
107106rexbidv 2728 . . . . . . . . . . . . . . . . . . . 20 coe1 deg1 coe1 deg1 coe1 coe1
108104, 107elab 3084 . . . . . . . . . . . . . . . . . . 19 coe1 deg1 coe1 deg1 coe1 coe1
109103, 108sylibr 205 . . . . . . . . . . . . . . . . . 18 deg1 coe1 deg1 coe1
110109adantl 454 . . . . . . . . . . . . . . . . 17 deg1 deg1 coe1 deg1 coe1
11192, 110sseldd 3351 . . . . . . . . . . . . . . . 16 deg1 deg1 coe1 deg1 coe1
112106rexbidv 2728 . . . . . . . . . . . . . . . . . 18 coe1 deg1 coe1 deg1 coe1 coe1
113104, 112elab 3084 . . . . . . . . . . . . . . . . 17 coe1 deg1 coe1 deg1 coe1 coe1
114 simpll2 998 . . . . . . . . . . . . . . . . . . . . . 22 deg1 deg1 deg1 coe1 coe1
115114, 58syl 16 . . . . . . . . . . . . . . . . . . . . 21 deg1 deg1 deg1 coe1 coe1
116 rnggrp 15671 . . . . . . . . . . . . . . . . . . . . 21
117115, 116syl 16 . . . . . . . . . . . . . . . . . . . 20 deg1 deg1 deg1 coe1 coe1
118114, 6syl 16 . . . . . . . . . . . . . . . . . . . . 21 deg1 deg1 deg1 coe1 coe1
119 simplrl 738 . . . . . . . . . . . . . . . . . . . . 21 deg1 deg1 deg1 coe1 coe1
120118, 119sseldd 3351 . . . . . . . . . . . . . . . . . . . 20 deg1 deg1 deg1 coe1 coe1
1213, 4lidlss 16282 . . . . . . . . . . . . . . . . . . . . . . 23
12259, 121syl 16 . . . . . . . . . . . . . . . . . . . . . 22
123114, 122syl 16 . . . . . . . . . . . . . . . . . . . . 21 deg1 deg1 deg1 coe1 coe1
124 simprl 734 . . . . . . . . . . . . . . . . . . . . 21 deg1 deg1 deg1 coe1 coe1
125123, 124sseldd 3351 . . . . . . . . . . . . . . . . . . . 20 deg1 deg1 deg1 coe1 coe1
126 eqid 2438 . . . . . . . . . . . . . . . . . . . . 21
127 eqid 2438 . . . . . . . . . . . . . . . . . . . . 21
1283, 126, 127grpnpcan 14882 . . . . . . . . . . . . . . . . . . . 20
129117, 120, 125, 128syl3anc 1185 . . . . . . . . . . . . . . . . . . 19 deg1 deg1 deg1 coe1 coe1
130593ad2ant2 980 . . . . . . . . . . . . . . . . . . . . 21 deg1
131130ad2antrr 708 . . . . . . . . . . . . . . . . . . . 20 deg1 deg1 deg1 coe1 coe1
132 simpll1 997 . . . . . . . . . . . . . . . . . . . . . 22 deg1 deg1 deg1 coe1 coe1
133114, 52syl 16 . . . . . . . . . . . . . . . . . . . . . 22 deg1 deg1 deg1 coe1 coe1
134 simplrr 739 . . . . . . . . . . . . . . . . . . . . . 22 deg1 deg1 deg1 coe1 coe1 deg1
135 simprrl 742 . . . . . . . . . . . . . . . . . . . . . 22 deg1 deg1 deg1 coe1 coe1 deg1
136 eqid 2438 . . . . . . . . . . . . . . . . . . . . . 22 coe1 coe1
137 eqid 2438 . . . . . . . . . . . . . . . . . . . . . 22 coe1 coe1
138 simprrr 743 . . . . . . . . . . . . . . . . . . . . . 22 deg1 deg1 deg1 coe1 coe1 coe1 coe1
1398, 9, 3, 127, 132, 133, 120, 134, 125, 135, 136, 137, 138deg1sublt 20035 . . . . . . . . . . . . . . . . . . . . 21 deg1 deg1 deg1 coe1 coe1 deg1
140114, 2syl 16 . . . . . . . . . . . . . . . . . . . . . . 23 deg1 deg1 deg1 coe1 coe1
14113ad2ant2 980 . . . . . . . . . . . . . . . . . . . . . . . . 25 deg1
142141ad2antrr 708 . . . . . . . . . . . . . . . . . . . . . . . 24 deg1 deg1 deg1 coe1 coe1
143142, 124sseldd 3351 . . . . . . . . . . . . . . . . . . . . . . 23 deg1 deg1 deg1 coe1 coe1
1444, 127lidlsubcl 16289 . . . . . . . . . . . . . . . . . . . . . . 23
145115, 140, 119, 143, 144syl22anc 1186 . . . . . . . . . . . . . . . . . . . . . 22 deg1 deg1 deg1 coe1 coe1
146 simpll3 999 . . . . . . . . . . . . . . . . . . . . . 22 deg1 deg1 deg1 coe1 coe1 deg1
147 fveq2 5730 . . . . . . . . . . . . . . . . . . . . . . . . 25 deg1 deg1
148147breq1d 4224 . . . . . . . . . . . . . . . . . . . . . . . 24 deg1 deg1
149 eleq1 2498 . . . . . . . . . . . . . . . . . . . . . . . 24
150148, 149imbi12d 313 . . . . . . . . . . . . . . . . . . . . . . 23 deg1 deg1
151150rspcva 3052 . . . . . . . . . . . . . . . . . . . . . 22 deg1 deg1
152145, 146, 151syl2anc 644 . . . . . . . . . . . . . . . . . . . . 21 deg1 deg1 deg1 coe1 coe1 deg1
153139, 152mpd 15 . . . . . . . . . . . . . . . . . . . 20 deg1 deg1 deg1 coe1 coe1
1544, 126lidlacl 16286 . . . . . . . . . . . . . . . . . . . 20
155115, 131, 153, 124, 154syl22anc 1186 . . . . . . . . . . . . . . . . . . 19 deg1 deg1 deg1 coe1 coe1
156129, 155eqeltrrd 2513 . . . . . . . . . . . . . . . . . 18 deg1 deg1 deg1 coe1 coe1
157156rexlimdvaa 2833 . . . . . . . . . . . . . . . . 17 deg1 deg1 deg1 coe1 coe1
158113, 157syl5bi 210 . . . . . . . . . . . . . . . 16 deg1 deg1 coe1 deg1 coe1
159111, 158mpd 15 . . . . . . . . . . . . . . 15 deg1 deg1
160159expr 600 . . . . . . . . . . . . . 14 deg1 deg1
16174, 160sylbid 208 . . . . . . . . . . . . 13 deg1 deg1
162161ralrimiva 2791 . . . . . . . . . . . 12 deg1 deg1
1631623exp 1153 . . . . . . . . . . 11 deg1 deg1
164163a2d 25 . . . . . . . . . 10 deg1 deg1
16537, 41, 51, 41, 66, 164nn0ind 10368 . . . . . . . . 9 deg1
166 rsp 2768 . . . . . . . . 9 deg1 deg1
167165, 166syl6com 34 . . . . . . . 8 deg1
168167com23 75 . . . . . . 7 deg1
169168imp 420 . . . . . 6 deg1
170169rexlimdv 2831 . . . . 5 deg1
17133, 170mpd 15 . . . 4
172171ex 425 . . 3
173172ssrdv 3356 . 2
1741, 173eqssd 3367 1
 Colors of variables: wff set class Syntax hints:   wi 4   wb 178   wo 359   wa 360   w3a 937   wceq 1653   wcel 1726  cab 2424  wral 2707  wrex 2708   cun 3320   wss 3322  csn 3816   class class class wbr 4214  cfv 5456  (class class class)co 6083  cr 8991  cc0 8992  c1 8993   caddc 8995   cmnf 9120   clt 9122   cle 9123  cn 10002  cn0 10223  cz 10284  cbs 13471   cplusg 13531  c0g 13725  cgrp 14687  csg 14690  crg 15662  LIdealclidl 16244  Poly1cpl1 16573  coe1cco1 16576   deg1 cdg1 19979  ldgIdlSeqcldgis 27304 This theorem is referenced by:  hbt  27313 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 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 4322  ax-sep 4332  ax-nul 4340  ax-pow 4379  ax-pr 4405  ax-un 4703  ax-inf2 7598  ax-cnex 9048  ax-resscn 9049  ax-1cn 9050  ax-icn 9051  ax-addcl 9052  ax-addrcl 9053  ax-mulcl 9054  ax-mulrcl 9055  ax-mulcom 9056  ax-addass 9057  ax-mulass 9058  ax-distr 9059  ax-i2m1 9060  ax-1ne0 9061  ax-1rid 9062  ax-rnegex 9063  ax-rrecex 9064  ax-cnre 9065  ax-pre-lttri 9066  ax-pre-lttrn 9067  ax-pre-ltadd 9068  ax-pre-mulgt0 9069  ax-pre-sup 9070  ax-addf 9071  ax-mulf 9072 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 4215  df-opab 4269  df-mpt 4270  df-tr 4305  df-eprel 4496  df-id 4500  df-po 4505  df-so 4506  df-fr 4543  df-se 4544  df-we 4545  df-ord 4586  df-on 4587  df-lim 4588  df-suc 4589  df-om 4848  df-xp 4886  df-rel 4887  df-cnv 4888  df-co 4889  df-dm 4890  df-rn 4891  df-res 4892  df-ima 4893  df-iota 5420  df-fun 5458  df-fn 5459  df-f 5460  df-f1 5461  df-fo 5462  df-f1o 5463  df-fv 5464  df-isom 5465  df-ov 6086  df-oprab 6087  df-mpt2 6088  df-of 6307  df-ofr 6308  df-1st 6351  df-2nd 6352  df-tpos 6481  df-riota 6551  df-recs 6635  df-rdg 6670  df-1o 6726  df-2o 6727  df-oadd 6730  df-er 6907  df-map 7022  df-pm 7023  df-ixp 7066  df-en 7112  df-dom 7113  df-sdom 7114  df-fin 7115  df-sup 7448  df-oi 7481  df-card 7828  df-pnf 9124  df-mnf 9125  df-xr 9126  df-ltxr 9127  df-le 9128  df-sub 9295  df-neg 9296  df-nn 10003  df-2 10060  df-3 10061  df-4 10062  df-5 10063  df-6 10064  df-7 10065  df-8 10066  df-9 10067  df-10 10068  df-n0 10224  df-z 10285  df-dec 10385  df-uz 10491  df-fz 11046  df-fzo 11138  df-seq 11326  df-hash 11621  df-struct 13473  df-ndx 13474  df-slot 13475  df-base 13476  df-sets 13477  df-ress 13478  df-plusg 13544  df-mulr 13545  df-starv 13546  df-sca 13547  df-vsca 13548  df-tset 13550  df-ple 13551  df-ds 13553  df-unif 13554  df-0g 13729  df-gsum 13730  df-mre 13813  df-mrc 13814  df-acs 13816  df-mnd 14692  df-mhm 14740  df-submnd 14741  df-grp 14814  df-minusg 14815  df-sbg 14816  df-mulg 14817  df-subg 14943  df-ghm 15006  df-cntz 15118  df-cmn 15416  df-abl 15417  df-mgp 15651  df-rng 15665  df-cring 15666  df-ur 15667  df-oppr 15730  df-dvdsr 15748  df-unit 15749  df-invr 15779  df-subrg 15868  df-lmod 15954  df-lss 16011  df-sra 16246  df-rgmod 16247  df-lidl 16248  df-rlreg 16345  df-psr 16419  df-mpl 16421  df-opsr 16427  df-psr1 16578  df-ply1 16580  df-coe1 16583  df-cnfld 16706  df-mdeg 19980  df-deg1 19981  df-ldgis 27305
 Copyright terms: Public domain W3C validator