Theorem discr1

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

	Ref	Expression
Hypotheses	discr.1	$$⊢\phi \to A\in ℝ$$
	discr.2	$$⊢\phi \to B\in ℝ$$
	discr.3	$$⊢\phi \to C\in ℝ$$
	discr.4	$$⊢\left(\phi \wedge x\in ℝ\right)\to 0\le A{x}^2+Bx+C$$
	discr1.5	$$⊢X=if\left(1\le \frac{B+if\left(0\le C,C,0\right)+1}{-A},\frac{B+if\left(0\le C,C,0\right)+1}{-A},1\right)$$
Assertion	discr1	$$⊢\phi \to 0\le A$$

Proof

Step	Hyp	Ref	Expression
1		discr.1	$$⊢\phi \to A\in ℝ$$
2		discr.2	$$⊢\phi \to B\in ℝ$$
3		discr.3	$$⊢\phi \to C\in ℝ$$
4		discr.4	$$⊢\left(\phi \wedge x\in ℝ\right)\to 0\le A{x}^2+Bx+C$$
5		discr1.5	$$⊢X=if\left(1\le \frac{B+if\left(0\le C,C,0\right)+1}{-A},\frac{B+if\left(0\le C,C,0\right)+1}{-A},1\right)$$
6		oveq1	$$⊢x=X\to x^2=X^2$$
7	6	oveq2d	$$⊢x=X\to A{x}^2=A{X}^2$$
8		oveq2	$$⊢x=X\to Bx=BX$$
9	7 8	oveq12d	$$⊢x=X\to A{x}^2+Bx=A{X}^2+BX$$
10	9	oveq1d	$$⊢x=X\to A{x}^2+Bx+C=A{X}^2+BX+C$$
11	10	breq2d	$$⊢x=X\to \left(0\le A{x}^2+Bx+C\leftrightarrow 0\le A{X}^2+BX+C\right)$$
12	4	ralrimiva	$$⊢\phi \to \forall x\in ℝ0\le A{x}^2+Bx+C$$
13	12	adantr	$$⊢\left(\phi \wedge A<0\right)\to \forall x\in ℝ0\le A{x}^2+Bx+C$$
14	2	adantr	$$⊢\left(\phi \wedge A<0\right)\to B\in ℝ$$
15	3	adantr	$$⊢\left(\phi \wedge A<0\right)\to C\in ℝ$$
16		0re	$$⊢0\in ℝ$$
17		ifcl	$$⊢\left(C\in ℝ\wedge 0\in ℝ\right)\to if\left(0\le C,C,0\right)\in ℝ$$
18	15 16 17	sylancl	$$⊢\left(\phi \wedge A<0\right)\to if\left(0\le C,C,0\right)\in ℝ$$
19	14 18	readdcld	$$⊢\left(\phi \wedge A<0\right)\to B+if\left(0\le C,C,0\right)\in ℝ$$
20		peano2re	$$⊢B+if\left(0\le C,C,0\right)\in ℝ\to B+if\left(0\le C,C,0\right)+1\in ℝ$$
21	19 20	syl	$$⊢\left(\phi \wedge A<0\right)\to B+if\left(0\le C,C,0\right)+1\in ℝ$$
22	1	adantr	$$⊢\left(\phi \wedge A<0\right)\to A\in ℝ$$
23	22	renegcld	$$⊢\left(\phi \wedge A<0\right)\to -A\in ℝ$$
24	1	lt0neg1d	$$⊢\phi \to \left(A<0\leftrightarrow 0<-A\right)$$
25	24	biimpa	$$⊢\left(\phi \wedge A<0\right)\to 0<-A$$
26	25	gt0ne0d	$$⊢\left(\phi \wedge A<0\right)\to -A\ne 0$$
27	21 23 26	redivcld	$$⊢\left(\phi \wedge A<0\right)\to \frac{B+if\left(0\le C,C,0\right)+1}{-A}\in ℝ$$
28		1re	$$⊢1\in ℝ$$
29		ifcl	$$⊢\left(\frac{B+if\left(0\le C,C,0\right)+1}{-A}\in ℝ\wedge 1\in ℝ\right)\to if\left(1\le \frac{B+if\left(0\le C,C,0\right)+1}{-A},\frac{B+if\left(0\le C,C,0\right)+1}{-A},1\right)\in ℝ$$
30	27 28 29	sylancl	$$⊢\left(\phi \wedge A<0\right)\to if\left(1\le \frac{B+if\left(0\le C,C,0\right)+1}{-A},\frac{B+if\left(0\le C,C,0\right)+1}{-A},1\right)\in ℝ$$
31	5 30	eqeltrid	$$⊢\left(\phi \wedge A<0\right)\to X\in ℝ$$
32	11 13 31	rspcdva	$$⊢\left(\phi \wedge A<0\right)\to 0\le A{X}^2+BX+C$$
33		resqcl	$$⊢X\in ℝ\to X^2\in ℝ$$
34	31 33	syl	$$⊢\left(\phi \wedge A<0\right)\to X^2\in ℝ$$
35	22 34	remulcld	$$⊢\left(\phi \wedge A<0\right)\to A{X}^2\in ℝ$$
36	14 31	remulcld	$$⊢\left(\phi \wedge A<0\right)\to BX\in ℝ$$
37	35 36	readdcld	$$⊢\left(\phi \wedge A<0\right)\to A{X}^2+BX\in ℝ$$
38	37 15	readdcld	$$⊢\left(\phi \wedge A<0\right)\to A{X}^2+BX+C\in ℝ$$
39	22 31	remulcld	$$⊢\left(\phi \wedge A<0\right)\to AX\in ℝ$$
40	39 19	readdcld	$$⊢\left(\phi \wedge A<0\right)\to AX+B+if\left(0\le C,C,0\right)\in ℝ$$
41	40 31	remulcld	$$⊢\left(\phi \wedge A<0\right)\to \left(AX+B+if\left(0\le C,C,0\right)\right)X\in ℝ$$
42	16	a1i	$$⊢\left(\phi \wedge A<0\right)\to 0\in ℝ$$
43	18 31	remulcld	$$⊢\left(\phi \wedge A<0\right)\to if\left(0\le C,C,0\right)X\in ℝ$$
44		max2	$$⊢\left(0\in ℝ\wedge C\in ℝ\right)\to C\le if\left(0\le C,C,0\right)$$
45	16 15 44	sylancr	$$⊢\left(\phi \wedge A<0\right)\to C\le if\left(0\le C,C,0\right)$$
46		max1	$$⊢\left(0\in ℝ\wedge C\in ℝ\right)\to 0\le if\left(0\le C,C,0\right)$$
47	16 15 46	sylancr	$$⊢\left(\phi \wedge A<0\right)\to 0\le if\left(0\le C,C,0\right)$$
48		max1	$$⊢\left(1\in ℝ\wedge \frac{B+if\left(0\le C,C,0\right)+1}{-A}\in ℝ\right)\to 1\le if\left(1\le \frac{B+if\left(0\le C,C,0\right)+1}{-A},\frac{B+if\left(0\le C,C,0\right)+1}{-A},1\right)$$
49	28 27 48	sylancr	$$⊢\left(\phi \wedge A<0\right)\to 1\le if\left(1\le \frac{B+if\left(0\le C,C,0\right)+1}{-A},\frac{B+if\left(0\le C,C,0\right)+1}{-A},1\right)$$
50	49 5	breqtrrdi	$$⊢\left(\phi \wedge A<0\right)\to 1\le X$$
51	18 31 47 50	lemulge11d	$$⊢\left(\phi \wedge A<0\right)\to if\left(0\le C,C,0\right)\le if\left(0\le C,C,0\right)X$$
52	15 18 43 45 51	letrd	$$⊢\left(\phi \wedge A<0\right)\to C\le if\left(0\le C,C,0\right)X$$
53	15 43 37 52	leadd2dd	$$⊢\left(\phi \wedge A<0\right)\to A{X}^2+BX+C\le A{X}^2+BX+if\left(0\le C,C,0\right)X$$
54	39 14	readdcld	$$⊢\left(\phi \wedge A<0\right)\to AX+B\in ℝ$$
55	54	recnd	$$⊢\left(\phi \wedge A<0\right)\to AX+B\in ℂ$$
56	18	recnd	$$⊢\left(\phi \wedge A<0\right)\to if\left(0\le C,C,0\right)\in ℂ$$
57	31	recnd	$$⊢\left(\phi \wedge A<0\right)\to X\in ℂ$$
58	55 56 57	adddird	$$⊢\left(\phi \wedge A<0\right)\to \left(AX+B+if\left(0\le C,C,0\right)\right)X=\left(AX+B\right)X+if\left(0\le C,C,0\right)X$$
59	39	recnd	$$⊢\left(\phi \wedge A<0\right)\to AX\in ℂ$$
60	14	recnd	$$⊢\left(\phi \wedge A<0\right)\to B\in ℂ$$
61	59 60 56	addassd	$$⊢\left(\phi \wedge A<0\right)\to AX+B+if\left(0\le C,C,0\right)=AX+B+if\left(0\le C,C,0\right)$$
62	61	oveq1d	$$⊢\left(\phi \wedge A<0\right)\to \left(AX+B+if\left(0\le C,C,0\right)\right)X=\left(AX+B+if\left(0\le C,C,0\right)\right)X$$
63	22	recnd	$$⊢\left(\phi \wedge A<0\right)\to A\in ℂ$$
64	63 57 57	mulassd	$$⊢\left(\phi \wedge A<0\right)\to AXX=AXX$$
65		sqval	$$⊢X\in ℂ\to X^2=XX$$
66	57 65	syl	$$⊢\left(\phi \wedge A<0\right)\to X^2=XX$$
67	66	oveq2d	$$⊢\left(\phi \wedge A<0\right)\to A{X}^2=AXX$$
68	64 67	eqtr4d	$$⊢\left(\phi \wedge A<0\right)\to AXX=A{X}^2$$
69	68	oveq1d	$$⊢\left(\phi \wedge A<0\right)\to AXX+BX=A{X}^2+BX$$
70	59 57 60 69	joinlmuladdmuld	$$⊢\left(\phi \wedge A<0\right)\to \left(AX+B\right)X=A{X}^2+BX$$
71	70	oveq1d	$$⊢\left(\phi \wedge A<0\right)\to \left(AX+B\right)X+if\left(0\le C,C,0\right)X=A{X}^2+BX+if\left(0\le C,C,0\right)X$$
72	58 62 71	3eqtr3d	$$⊢\left(\phi \wedge A<0\right)\to \left(AX+B+if\left(0\le C,C,0\right)\right)X=A{X}^2+BX+if\left(0\le C,C,0\right)X$$
73	53 72	breqtrrd	$$⊢\left(\phi \wedge A<0\right)\to A{X}^2+BX+C\le \left(AX+B+if\left(0\le C,C,0\right)\right)X$$
74	23 31	remulcld	$$⊢\left(\phi \wedge A<0\right)\to \left(-A\right)X\in ℝ$$
75	19	ltp1d	$$⊢\left(\phi \wedge A<0\right)\to B+if\left(0\le C,C,0\right)<B+if\left(0\le C,C,0\right)+1$$
76		max2	$$⊢\left(1\in ℝ\wedge \frac{B+if\left(0\le C,C,0\right)+1}{-A}\in ℝ\right)\to \frac{B+if\left(0\le C,C,0\right)+1}{-A}\le if\left(1\le \frac{B+if\left(0\le C,C,0\right)+1}{-A},\frac{B+if\left(0\le C,C,0\right)+1}{-A},1\right)$$
77	28 27 76	sylancr	$$⊢\left(\phi \wedge A<0\right)\to \frac{B+if\left(0\le C,C,0\right)+1}{-A}\le if\left(1\le \frac{B+if\left(0\le C,C,0\right)+1}{-A},\frac{B+if\left(0\le C,C,0\right)+1}{-A},1\right)$$
78	77 5	breqtrrdi	$$⊢\left(\phi \wedge A<0\right)\to \frac{B+if\left(0\le C,C,0\right)+1}{-A}\le X$$
79		ledivmul	$$⊢\left(B+if\left(0\le C,C,0\right)+1\in ℝ\wedge X\in ℝ\wedge \left(-A\in ℝ\wedge 0<-A\right)\right)\to \left(\frac{B+if\left(0\le C,C,0\right)+1}{-A}\le X\leftrightarrow B+if\left(0\le C,C,0\right)+1\le \left(-A\right)X\right)$$
80	21 31 23 25 79	syl112anc	$$⊢\left(\phi \wedge A<0\right)\to \left(\frac{B+if\left(0\le C,C,0\right)+1}{-A}\le X\leftrightarrow B+if\left(0\le C,C,0\right)+1\le \left(-A\right)X\right)$$
81	78 80	mpbid	$$⊢\left(\phi \wedge A<0\right)\to B+if\left(0\le C,C,0\right)+1\le \left(-A\right)X$$
82	19 21 74 75 81	ltletrd	$$⊢\left(\phi \wedge A<0\right)\to B+if\left(0\le C,C,0\right)<\left(-A\right)X$$
83	63 57	mulneg1d	$$⊢\left(\phi \wedge A<0\right)\to \left(-A\right)X=-AX$$
84		df-neg	$$⊢-AX=0-AX$$
85	83 84	eqtrdi	$$⊢\left(\phi \wedge A<0\right)\to \left(-A\right)X=0-AX$$
86	82 85	breqtrd	$$⊢\left(\phi \wedge A<0\right)\to B+if\left(0\le C,C,0\right)<0-AX$$
87	39 19 42	ltaddsub2d	$$⊢\left(\phi \wedge A<0\right)\to \left(AX+B+if\left(0\le C,C,0\right)<0\leftrightarrow B+if\left(0\le C,C,0\right)<0-AX\right)$$
88	86 87	mpbird	$$⊢\left(\phi \wedge A<0\right)\to AX+B+if\left(0\le C,C,0\right)<0$$
89	28	a1i	$$⊢\left(\phi \wedge A<0\right)\to 1\in ℝ$$
90		0lt1	$$⊢0<1$$
91	90	a1i	$$⊢\left(\phi \wedge A<0\right)\to 0<1$$
92	42 89 31 91 50	ltletrd	$$⊢\left(\phi \wedge A<0\right)\to 0<X$$
93		ltmul1	$$⊢\left(AX+B+if\left(0\le C,C,0\right)\in ℝ\wedge 0\in ℝ\wedge \left(X\in ℝ\wedge 0<X\right)\right)\to \left(AX+B+if\left(0\le C,C,0\right)<0\leftrightarrow \left(AX+B+if\left(0\le C,C,0\right)\right)X<0\cdot X\right)$$
94	40 42 31 92 93	syl112anc	$$⊢\left(\phi \wedge A<0\right)\to \left(AX+B+if\left(0\le C,C,0\right)<0\leftrightarrow \left(AX+B+if\left(0\le C,C,0\right)\right)X<0\cdot X\right)$$
95	88 94	mpbid	$$⊢\left(\phi \wedge A<0\right)\to \left(AX+B+if\left(0\le C,C,0\right)\right)X<0\cdot X$$
96	57	mul02d	$$⊢\left(\phi \wedge A<0\right)\to 0\cdot X=0$$
97	95 96	breqtrd	$$⊢\left(\phi \wedge A<0\right)\to \left(AX+B+if\left(0\le C,C,0\right)\right)X<0$$
98	38 41 42 73 97	lelttrd	$$⊢\left(\phi \wedge A<0\right)\to A{X}^2+BX+C<0$$
99		ltnle	$$⊢\left(A{X}^2+BX+C\in ℝ\wedge 0\in ℝ\right)\to \left(A{X}^2+BX+C<0\leftrightarrow \neg 0\le A{X}^2+BX+C\right)$$
100	38 16 99	sylancl	$$⊢\left(\phi \wedge A<0\right)\to \left(A{X}^2+BX+C<0\leftrightarrow \neg 0\le A{X}^2+BX+C\right)$$
101	98 100	mpbid	$$⊢\left(\phi \wedge A<0\right)\to \neg 0\le A{X}^2+BX+C$$
102	32 101	pm2.65da	$$⊢\phi \to \neg A<0$$
103		lelttric	$$⊢\left(0\in ℝ\wedge A\in ℝ\right)\to \left(0\le A\vee A<0\right)$$
104	16 1 103	sylancr	$$⊢\phi \to \left(0\le A\vee A<0\right)$$
105	104	ord	$$⊢\phi \to \left(\neg 0\le A\to A<0\right)$$
106	102 105	mt3d	$$⊢\phi \to 0\le A$$