Theorem discr 12303

Description: If a quadratic polynomial with real coefficients is nonnegative for all values, then its discriminant is nonpositive. (Contributed by NM, 10-Aug-1999.) (Revised by Mario Carneiro, 4-Jun-2014.)

Hypotheses

Ref	Expression
discr.1
discr.2
discr.3
discr.4

Assertion

Ref	Expression
discr

Distinct variable groups:   ,   ,   ,   ,

Proof of Theorem discr

Step	Hyp	Ref	Expression
1		discr.2	. . . . . . . . . 10
2	1	adantr 465	. . . . . . . . 9
3		resqcl 12235	. . . . . . . . 9
4	2, 3	syl 16	. . . . . . . 8
5	4	recnd 9643	. . . . . . 7
6		4re 10637	. . . . . . . . 9
7		discr.1	. . . . . . . . . . 11
8	7	adantr 465	. . . . . . . . . 10
9		discr.3	. . . . . . . . . . 11
10	9	adantr 465	. . . . . . . . . 10
11	8, 10	remulcld 9645	. . . . . . . . 9
12		remulcl 9598	. . . . . . . . 9
13	6, 11, 12	sylancr 663	. . . . . . . 8
14	13	recnd 9643	. . . . . . 7
15		4pos 10656	. . . . . . . . . 10
16	6, 15	elrpii 11252	. . . . . . . . 9
17		simpr 461	. . . . . . . . . 10
18	8, 17	elrpd 11283	. . . . . . . . 9
19		rpmulcl 11270	. . . . . . . . 9
20	16, 18, 19	sylancr 663	. . . . . . . 8
21	20	rpcnd 11287	. . . . . . 7
22	20	rpne0d 11290	. . . . . . 7
23	5, 14, 21, 22	divsubdird 10384	. . . . . 6
24	11	recnd 9643	. . . . . . . . 9
25	8	recnd 9643	. . . . . . . . 9
26		4cn 10638	. . . . . . . . . 10
27	26	a1i 11	. . . . . . . . 9
28	18	rpne0d 11290	. . . . . . . . 9
29		4ne0 10657	. . . . . . . . . 10
30	29	a1i 11	. . . . . . . . 9
31	24, 25, 27, 28, 30	divcan5d 10371	. . . . . . . 8
32	10	recnd 9643	. . . . . . . . 9
33	32, 25, 28	divcan3d 10350	. . . . . . . 8
34	31, 33	eqtrd 2498	. . . . . . 7
35	34	oveq2d 6312	. . . . . 6
36	23, 35	eqtrd 2498	. . . . 5
37	4, 20	rerpdivcld 11312	. . . . . . . . . . 11
38	37	recnd 9643	. . . . . . . . . 10
39	38	2timesd 10806	. . . . . . . . 9
40		2t2e4 10710	. . . . . . . . . . . . 13
41	40	oveq1i 6306	. . . . . . . . . . . 12
42		2cnd 10633	. . . . . . . . . . . . 13
43	42, 42, 25	mulassd 9640	. . . . . . . . . . . 12
44	41, 43	syl5eqr 2512	. . . . . . . . . . 11
45	44	oveq2d 6312	. . . . . . . . . 10
46	42, 5, 21, 22	divassd 10380	. . . . . . . . . 10
47		2rp 11254	. . . . . . . . . . . . 13
48		rpmulcl 11270	. . . . . . . . . . . . 13
49	47, 18, 48	sylancr 663	. . . . . . . . . . . 12
50	49	rpcnd 11287	. . . . . . . . . . 11
51	49	rpne0d 11290	. . . . . . . . . . 11
52		2ne0 10653	. . . . . . . . . . . 12
53	52	a1i 11	. . . . . . . . . . 11
54	5, 50, 42, 51, 53	divcan5d 10371	. . . . . . . . . 10
55	45, 46, 54	3eqtr3d 2506	. . . . . . . . 9
56	39, 55	eqtr3d 2500	. . . . . . . 8
57	2, 49	rerpdivcld 11312	. . . . . . . . . . . 12
58	57	renegcld 10011	. . . . . . . . . . 11
59		discr.4	. . . . . . . . . . . . 13
60	59	ralrimiva 2871	. . . . . . . . . . . 12
61	60	adantr 465	. . . . . . . . . . 11
62		oveq1 6303	. . . . . . . . . . . . . . . 16
63	62	oveq2d 6312	. . . . . . . . . . . . . . 15
64		oveq2 6304	. . . . . . . . . . . . . . 15
65	63, 64	oveq12d 6314	. . . . . . . . . . . . . 14
66	65	oveq1d 6311	. . . . . . . . . . . . 13
67	66	breq2d 4464	. . . . . . . . . . . 12
68	67	rspcv 3206	. . . . . . . . . . 11
69	58, 61, 68	sylc 60	. . . . . . . . . 10
70	57	recnd 9643	. . . . . . . . . . . . . . . . . . 19
71		sqneg 12228	. . . . . . . . . . . . . . . . . . 19
72	70, 71	syl 16	. . . . . . . . . . . . . . . . . 18
73	2	recnd 9643	. . . . . . . . . . . . . . . . . . 19
74		sqdiv 12233	. . . . . . . . . . . . . . . . . . 19
75	73, 50, 51, 74	syl3anc 1228	. . . . . . . . . . . . . . . . . 18
76		sqval 12227	. . . . . . . . . . . . . . . . . . . . 21
77	50, 76	syl 16	. . . . . . . . . . . . . . . . . . . 20
78	50, 42, 25	mulassd 9640	. . . . . . . . . . . . . . . . . . . 20
79	42, 25, 42	mul32d 9811	. . . . . . . . . . . . . . . . . . . . . 22
80	79, 41	syl6eq 2514	. . . . . . . . . . . . . . . . . . . . 21
81	80	oveq1d 6311	. . . . . . . . . . . . . . . . . . . 20
82	77, 78, 81	3eqtr2d 2504	. . . . . . . . . . . . . . . . . . 19
83	82	oveq2d 6312	. . . . . . . . . . . . . . . . . 18
84	72, 75, 83	3eqtrd 2502	. . . . . . . . . . . . . . . . 17
85	5, 21, 25, 22, 28	divdiv1d 10376	. . . . . . . . . . . . . . . . 17
86	84, 85	eqtr4d 2501	. . . . . . . . . . . . . . . 16
87	86	oveq2d 6312	. . . . . . . . . . . . . . 15
88	38, 25, 28	divcan2d 10347	. . . . . . . . . . . . . . 15
89	87, 88	eqtrd 2498	. . . . . . . . . . . . . 14
90	73, 70	mulneg2d 10035	. . . . . . . . . . . . . . 15
91		sqval 12227	. . . . . . . . . . . . . . . . . . 19
92	73, 91	syl 16	. . . . . . . . . . . . . . . . . 18
93	92	oveq1d 6311	. . . . . . . . . . . . . . . . 17
94	73, 73, 50, 51	divassd 10380	. . . . . . . . . . . . . . . . 17
95	93, 94	eqtrd 2498	. . . . . . . . . . . . . . . 16
96	95	negeqd 9837	. . . . . . . . . . . . . . 15
97	90, 96	eqtr4d 2501	. . . . . . . . . . . . . 14
98	89, 97	oveq12d 6314	. . . . . . . . . . . . 13
99	4, 49	rerpdivcld 11312	. . . . . . . . . . . . . . 15
100	99	recnd 9643	. . . . . . . . . . . . . 14
101	38, 100	negsubd 9960	. . . . . . . . . . . . 13
102	98, 101	eqtrd 2498	. . . . . . . . . . . 12
103	102	oveq1d 6311	. . . . . . . . . . 11
104	38, 32, 100	addsubd 9975	. . . . . . . . . . 11
105	103, 104	eqtr4d 2501	. . . . . . . . . 10
106	69, 105	breqtrd 4476	. . . . . . . . 9
107	37, 10	readdcld 9644	. . . . . . . . . 10
108	107, 99	subge0d 10167	. . . . . . . . 9
109	106, 108	mpbid 210	. . . . . . . 8
110	56, 109	eqbrtrd 4472	. . . . . . 7
111	37, 10, 37	leadd2d 10172	. . . . . . 7
112	110, 111	mpbird 232	. . . . . 6
113	37, 10	suble0d 10168	. . . . . 6
114	112, 113	mpbird 232	. . . . 5
115	36, 114	eqbrtrd 4472	. . . 4
116	4, 13	resubcld 10012	. . . . 5
117		0red 9618	. . . . 5
118	116, 117, 20	ledivmuld 11334	. . . 4
119	115, 118	mpbid 210	. . 3
120	21	mul01d 9800	. . 3
121	119, 120	breqtrd 4476	. 2
122	9	adantr 465	. . . . . . . . . . . 12
123	122	ltp1d 10501	. . . . . . . . . . 11
124		peano2re 9774	. . . . . . . . . . . . 13
125	122, 124	syl 16	. . . . . . . . . . . 12
126	122, 125	ltnegd 10155	. . . . . . . . . . 11
127	123, 126	mpbid 210	. . . . . . . . . 10
128		df-neg 9831	. . . . . . . . . 10
129	127, 128	syl6breq 4491	. . . . . . . . 9
130	125	renegcld 10011	. . . . . . . . . 10
131		0red 9618	. . . . . . . . . 10
132	130, 122, 131	ltaddsubd 10177	. . . . . . . . 9
133	129, 132	mpbird 232	. . . . . . . 8
134	133	expr 615	. . . . . . 7
135	1	adantr 465	. . . . . . . . . . . 12
136		simprr 757	. . . . . . . . . . . 12
137	130, 135, 136	redivcld 10397	. . . . . . . . . . 11
138	60	adantr 465	. . . . . . . . . . 11
139		oveq1 6303	. . . . . . . . . . . . . . . 16
140	139	oveq2d 6312	. . . . . . . . . . . . . . 15
141		oveq2 6304	. . . . . . . . . . . . . . 15
142	140, 141	oveq12d 6314	. . . . . . . . . . . . . 14
143	142	oveq1d 6311	. . . . . . . . . . . . 13
144	143	breq2d 4464	. . . . . . . . . . . 12
145	144	rspcv 3206	. . . . . . . . . . 11
146	137, 138, 145	sylc 60	. . . . . . . . . 10
147		simprl 756	. . . . . . . . . . . . . . 15
148	147	oveq1d 6311	. . . . . . . . . . . . . 14
149	137	recnd 9643	. . . . . . . . . . . . . . . 16
150		sqcl 12230	. . . . . . . . . . . . . . . 16
151	149, 150	syl 16	. . . . . . . . . . . . . . 15
152	151	mul02d 9799	. . . . . . . . . . . . . 14
153	148, 152	eqtr3d 2500	. . . . . . . . . . . . 13
154	130	recnd 9643	. . . . . . . . . . . . . 14
155	135	recnd 9643	. . . . . . . . . . . . . 14
156	154, 155, 136	divcan2d 10347	. . . . . . . . . . . . 13
157	153, 156	oveq12d 6314	. . . . . . . . . . . 12
158	154	addid2d 9802	. . . . . . . . . . . 12
159	157, 158	eqtrd 2498	. . . . . . . . . . 11
160	159	oveq1d 6311	. . . . . . . . . 10
161	146, 160	breqtrd 4476	. . . . . . . . 9
162		0re 9617	. . . . . . . . . 10
163	130, 122	readdcld 9644	. . . . . . . . . 10
164		lenlt 9684	. . . . . . . . . 10
165	162, 163, 164	sylancr 663	. . . . . . . . 9
166	161, 165	mpbid 210	. . . . . . . 8
167	166	expr 615	. . . . . . 7
168	134, 167	pm2.65d 175	. . . . . 6
169		nne 2658	. . . . . 6
170	168, 169	sylib 196	. . . . 5
171	170	sq0id 12261	. . . 4
172		simpr 461	. . . . . . . 8
173	172	oveq1d 6311	. . . . . . 7
174	9	recnd 9643	. . . . . . . . 9
175	174	adantr 465	. . . . . . . 8
176	175	mul02d 9799	. . . . . . 7
177	173, 176	eqtr3d 2500	. . . . . 6
178	177	oveq2d 6312	. . . . 5
179	26	mul01i 9791	. . . . 5
180	178, 179	syl6eq 2514	. . . 4
181	171, 180	oveq12d 6314	. . 3
182		0m0e0 10670	. . . 4
183		0le0 10650	. . . 4
184	182, 183	eqbrtri 4471	. . 3
185	181, 184	syl6eqbr 4489	. 2
186		eqid 2457	. . . 4
187	7, 1, 9, 59, 186	discr1 12302	. . 3
188		leloe 9692	. . . 4
189	162, 7, 188	sylancr 663	. . 3
190	187, 189	mpbid 210	. 2
191	121, 185, 190	mpjaodan 786	1

Syntax hints:  -.wn 3  ->wi 4  <->wb 184  \/wo 368  /\wa 369  =wceq 1395  e.wcel 1818  =/=wne 2652  A.wral 2807  ifcif 3941   class class class wbr 4452  (class class class)co 6296  cc 9511  cr 9512  0cc0 9513  1c1 9514  caddc 9516  cmul 9518  clt 9649  cle 9650  cmin 9828  -ucneg 9829  cdiv 10231  2c2 10610  4c4 10612  crp 11249  cexp 12166

This theorem is referenced by:  csbren  21826  normlem6  26032

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-8 1820  ax-9 1822  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-sep 4573  ax-nul 4581  ax-pow 4630  ax-pr 4691  ax-un 6592  ax-cnex 9569  ax-resscn 9570  ax-1cn 9571  ax-icn 9572  ax-addcl 9573  ax-addrcl 9574  ax-mulcl 9575  ax-mulrcl 9576  ax-mulcom 9577  ax-addass 9578  ax-mulass 9579  ax-distr 9580  ax-i2m1 9581  ax-1ne0 9582  ax-1rid 9583  ax-rnegex 9584  ax-rrecex 9585  ax-cnre 9586  ax-pre-lttri 9587  ax-pre-lttrn 9588  ax-pre-ltadd 9589  ax-pre-mulgt0 9590

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-eu 2286  df-mo 2287  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-nel 2655  df-ral 2812  df-rex 2813  df-reu 2814  df-rmo 2815  df-rab 2816  df-v 3111  df-sbc 3328  df-csb 3435  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-pss 3491  df-nul 3785  df-if 3942  df-pw 4014  df-sn 4030  df-pr 4032  df-tp 4034  df-op 4036  df-uni 4250  df-iun 4332  df-br 4453  df-opab 4511  df-mpt 4512  df-tr 4546  df-eprel 4796  df-id 4800  df-po 4805  df-so 4806  df-fr 4843  df-we 4845  df-ord 4886  df-on 4887  df-lim 4888  df-suc 4889  df-xp 5010  df-rel 5011  df-cnv 5012  df-co 5013  df-dm 5014  df-rn 5015  df-res 5016  df-ima 5017  df-iota 5556  df-fun 5595  df-fn 5596  df-f 5597  df-f1 5598  df-fo 5599  df-f1o 5600  df-fv 5601  df-riota 6257  df-ov 6299  df-oprab 6300  df-mpt2 6301  df-om 6701  df-2nd 6801  df-recs 7061  df-rdg 7095  df-er 7330  df-en 7537  df-dom 7538  df-sdom 7539  df-pnf 9651  df-mnf 9652  df-xr 9653  df-ltxr 9654  df-le 9655  df-sub 9830  df-neg 9831  df-div 10232  df-nn 10562  df-2 10619  df-3 10620  df-4 10621  df-n0 10821  df-z 10890  df-uz 11111  df-rp 11250  df-seq 12108  df-exp 12167