discr1 - Metamath Proof Explorer

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

Theorem discr1 12302

Description: A nonnegative quadratic form has nonnegative leading coefficient. (Contributed by Mario Carneiro, 4-Jun-2014.)

**Hypotheses**
Ref	Expression
discr.1
discr.2
discr.3
discr.4
discr1.5

**Assertion**
Ref	Expression
discr1

Distinct variable groups: , , , , ,

**Proof of Theorem discr1**
Step	Hyp	Ref	Expression
1		discr1.5	. . . . 5
2		discr.2	. . . . . . . . . 10
3	2	adantr 465	. . . . . . . . 9
4		discr.3	. . . . . . . . . . 11
5	4	adantr 465	. . . . . . . . . 10
6		0re 9617	. . . . . . . . . 10
7		ifcl 3983	. . . . . . . . . 10
8	5, 6, 7	sylancl 662	. . . . . . . . 9
9	3, 8	readdcld 9644	. . . . . . . 8
10		peano2re 9774	. . . . . . . 8
11	9, 10	syl 16	. . . . . . 7
12		discr.1	. . . . . . . . 9
13	12	adantr 465	. . . . . . . 8
14	13	renegcld 10011	. . . . . . 7
15	12	lt0neg1d 10147	. . . . . . . . 9
16	15	biimpa 484	. . . . . . . 8
17	16	gt0ne0d 10142	. . . . . . 7
18	11, 14, 17	redivcld 10397	. . . . . 6
19		1re 9616	. . . . . 6
20		ifcl 3983	. . . . . 6
21	18, 19, 20	sylancl 662	. . . . 5
22	1, 21	syl5eqel 2549	. . . 4
23		discr.4	. . . . . 6
24	23	ralrimiva 2871	. . . . 5
25	24	adantr 465	. . . 4
26		oveq1 6303	. . . . . . . . 9
27	26	oveq2d 6312	. . . . . . . 8
28		oveq2 6304	. . . . . . . 8
29	27, 28	oveq12d 6314	. . . . . . 7
30	29	oveq1d 6311	. . . . . 6
31	30	breq2d 4464	. . . . 5
32	31	rspcv 3206	. . . 4
33	22, 25, 32	sylc 60	. . 3
34		resqcl 12235	. . . . . . . . 9
35	22, 34	syl 16	. . . . . . . 8
36	13, 35	remulcld 9645	. . . . . . 7
37	3, 22	remulcld 9645	. . . . . . 7
38	36, 37	readdcld 9644	. . . . . 6
39	38, 5	readdcld 9644	. . . . 5
40	13, 22	remulcld 9645	. . . . . . 7
41	40, 9	readdcld 9644	. . . . . 6
42	41, 22	remulcld 9645	. . . . 5
43	6	a1i 11	. . . . 5
44	8, 22	remulcld 9645	. . . . . . 7
45		max2 11417	. . . . . . . . 9
46	6, 5, 45	sylancr 663	. . . . . . . 8
47		max1 11415	. . . . . . . . . 10
48	6, 5, 47	sylancr 663	. . . . . . . . 9
49		max1 11415	. . . . . . . . . . 11
50	19, 18, 49	sylancr 663	. . . . . . . . . 10
51	50, 1	syl6breqr 4492	. . . . . . . . 9
52	8, 22, 48, 51	lemulge11d 10508	. . . . . . . 8
53	5, 8, 44, 46, 52	letrd 9760	. . . . . . 7
54	5, 44, 38, 53	leadd2dd 10192	. . . . . 6
55	40, 3	readdcld 9644	. . . . . . . . 9
56	55	recnd 9643	. . . . . . . 8
57	8	recnd 9643	. . . . . . . 8
58	22	recnd 9643	. . . . . . . 8
59	56, 57, 58	adddird 9642	. . . . . . 7
60	40	recnd 9643	. . . . . . . . 9
61	3	recnd 9643	. . . . . . . . 9
62	60, 61, 57	addassd 9639	. . . . . . . 8
63	62	oveq1d 6311	. . . . . . 7
64	60, 61, 58	adddird 9642	. . . . . . . . 9
65	13	recnd 9643	. . . . . . . . . . . 12
66	65, 58, 58	mulassd 9640	. . . . . . . . . . 11
67		sqval 12227	. . . . . . . . . . . . 13
68	58, 67	syl 16	. . . . . . . . . . . 12
69	68	oveq2d 6312	. . . . . . . . . . 11
70	66, 69	eqtr4d 2501	. . . . . . . . . 10
71	70	oveq1d 6311	. . . . . . . . 9
72	64, 71	eqtrd 2498	. . . . . . . 8
73	72	oveq1d 6311	. . . . . . 7
74	59, 63, 73	3eqtr3d 2506	. . . . . 6
75	54, 74	breqtrrd 4478	. . . . 5
76	14, 22	remulcld 9645	. . . . . . . . . 10
77	9	ltp1d 10501	. . . . . . . . . 10
78		max2 11417	. . . . . . . . . . . . 13
79	19, 18, 78	sylancr 663	. . . . . . . . . . . 12
80	79, 1	syl6breqr 4492	. . . . . . . . . . 11
81		ledivmul 10443	. . . . . . . . . . . 12
82	11, 22, 14, 16, 81	syl112anc 1232	. . . . . . . . . . 11
83	80, 82	mpbid 210	. . . . . . . . . 10
84	9, 11, 76, 77, 83	ltletrd 9763	. . . . . . . . 9
85	65, 58	mulneg1d 10034	. . . . . . . . . 10
86		df-neg 9831	. . . . . . . . . 10
87	85, 86	syl6eq 2514	. . . . . . . . 9
88	84, 87	breqtrd 4476	. . . . . . . 8
89	40, 9, 43	ltaddsub2d 10178	. . . . . . . 8
90	88, 89	mpbird 232	. . . . . . 7
91	19	a1i 11	. . . . . . . . 9
92		0lt1 10100	. . . . . . . . . 10
93	92	a1i 11	. . . . . . . . 9
94	43, 91, 22, 93, 51	ltletrd 9763	. . . . . . . 8
95		ltmul1 10417	. . . . . . . 8
96	41, 43, 22, 94, 95	syl112anc 1232	. . . . . . 7
97	90, 96	mpbid 210	. . . . . 6
98	58	mul02d 9799	. . . . . 6
99	97, 98	breqtrd 4476	. . . . 5
100	39, 42, 43, 75, 99	lelttrd 9761	. . . 4
101		ltnle 9685	. . . . 5
102	39, 6, 101	sylancl 662	. . . 4
103	100, 102	mpbid 210	. . 3
104	33, 103	pm2.65da 576	. 2
105		lelttric 9712	. . . 4
106	6, 12, 105	sylancr 663	. . 3
107	106	ord 377	. 2
108	104, 107	mt3d 125	1

Colors of variables: wff setvar class

Syntax hints: -.wn 3 ->wi 4 <->wb 184 \/wo 368 /\wa 369 =wceq 1395 e.wcel 1818 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 cexp 12166

This theorem is referenced by: discr 12303

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-n0 10821 df-z 10890 df-uz 11111 df-seq 12108 df-exp 12167

W3C validator