discr

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)

	Ref	Expression
Hypotheses	discr.1	$⊢ φ \to A \in ℝ$
	discr.2	$⊢ φ \to B \in ℝ$
	discr.3	$⊢ φ \to C \in ℝ$
	discr.4	$⊢ (φ \land x \in ℝ) \to 0 \leq A x^{2} + B x + C$
Assertion	discr	$⊢ φ \to B^{2} - 4 A C \leq 0$

Proof

Step	Hyp	Ref	Expression
1		discr.1	$⊢ φ \to A \in ℝ$
2		discr.2	$⊢ φ \to B \in ℝ$
3		discr.3	$⊢ φ \to C \in ℝ$
4		discr.4	$⊢ (φ \land x \in ℝ) \to 0 \leq A x^{2} + B x + C$
5	2	adantr	$⊢ (φ \land 0 < A) \to B \in ℝ$
6		resqcl	$⊢ B \in ℝ \to B^{2} \in ℝ$
7	5 6	syl	$⊢ (φ \land 0 < A) \to B^{2} \in ℝ$
8	7	recnd	$⊢ (φ \land 0 < A) \to B^{2} \in ℂ$
9		4re	$⊢ 4 \in ℝ$
10	1	adantr	$⊢ (φ \land 0 < A) \to A \in ℝ$
11	3	adantr	$⊢ (φ \land 0 < A) \to C \in ℝ$
12	10 11	remulcld	$⊢ (φ \land 0 < A) \to A C \in ℝ$
13		remulcl	$⊢ (4 \in ℝ \land A C \in ℝ) \to 4 A C \in ℝ$
14	9 12 13	sylancr	$⊢ (φ \land 0 < A) \to 4 A C \in ℝ$
15	14	recnd	$⊢ (φ \land 0 < A) \to 4 A C \in ℂ$
16		4pos	$⊢ 0 < 4$
17	9 16	elrpii	$⊢ 4 \in ℝ^{+}$
18		simpr	$⊢ (φ \land 0 < A) \to 0 < A$
19	10 18	elrpd	$⊢ (φ \land 0 < A) \to A \in ℝ^{+}$
20		rpmulcl	$⊢ (4 \in ℝ^{+} \land A \in ℝ^{+}) \to 4 A \in ℝ^{+}$
21	17 19 20	sylancr	$⊢ (φ \land 0 < A) \to 4 A \in ℝ^{+}$
22	21	rpcnd	$⊢ (φ \land 0 < A) \to 4 A \in ℂ$
23	21	rpne0d	$⊢ (φ \land 0 < A) \to 4 A \neq 0$
24	8 15 22 23	divsubdird	$⊢ (φ \land 0 < A) \to \frac{B^{2} - 4 A C}{4 A} = (\frac{B^{2}}{4 A}) - (\frac{4 A C}{4 A})$
25	12	recnd	$⊢ (φ \land 0 < A) \to A C \in ℂ$
26	10	recnd	$⊢ (φ \land 0 < A) \to A \in ℂ$
27		4cn	$⊢ 4 \in ℂ$
28	27	a1i	$⊢ (φ \land 0 < A) \to 4 \in ℂ$
29	19	rpne0d	$⊢ (φ \land 0 < A) \to A \neq 0$
30		4ne0	$⊢ 4 \neq 0$
31	30	a1i	$⊢ (φ \land 0 < A) \to 4 \neq 0$
32	25 26 28 29 31	divcan5d	$⊢ (φ \land 0 < A) \to \frac{4 A C}{4 A} = \frac{A C}{A}$
33	11	recnd	$⊢ (φ \land 0 < A) \to C \in ℂ$
34	33 26 29	divcan3d	$⊢ (φ \land 0 < A) \to \frac{A C}{A} = C$
35	32 34	eqtrd	$⊢ (φ \land 0 < A) \to \frac{4 A C}{4 A} = C$
36	35	oveq2d	$⊢ (φ \land 0 < A) \to (\frac{B^{2}}{4 A}) - (\frac{4 A C}{4 A}) = (\frac{B^{2}}{4 A}) - C$
37	24 36	eqtrd	$⊢ (φ \land 0 < A) \to \frac{B^{2} - 4 A C}{4 A} = (\frac{B^{2}}{4 A}) - C$
38	7 21	rerpdivcld	$⊢ (φ \land 0 < A) \to \frac{B^{2}}{4 A} \in ℝ$
39	38	recnd	$⊢ (φ \land 0 < A) \to \frac{B^{2}}{4 A} \in ℂ$
40	39	2timesd	$⊢ (φ \land 0 < A) \to 2 (\frac{B^{2}}{4 A}) = (\frac{B^{2}}{4 A}) + (\frac{B^{2}}{4 A})$
41		2t2e4	$⊢ 2 \cdot 2 = 4$
42	41	oveq1i	$⊢ 2 \cdot 2 A = 4 A$
43		2cnd	$⊢ (φ \land 0 < A) \to 2 \in ℂ$
44	43 43 26	mulassd	$⊢ (φ \land 0 < A) \to 2 \cdot 2 A = 2 2 A$
45	42 44	eqtr3id	$⊢ (φ \land 0 < A) \to 4 A = 2 2 A$
46	45	oveq2d	$⊢ (φ \land 0 < A) \to \frac{2 B^{2}}{4 A} = \frac{2 B^{2}}{2 2 A}$
47	43 8 22 23	divassd	$⊢ (φ \land 0 < A) \to \frac{2 B^{2}}{4 A} = 2 (\frac{B^{2}}{4 A})$
48		2rp	$⊢ 2 \in ℝ^{+}$
49		rpmulcl	$⊢ (2 \in ℝ^{+} \land A \in ℝ^{+}) \to 2 A \in ℝ^{+}$
50	48 19 49	sylancr	$⊢ (φ \land 0 < A) \to 2 A \in ℝ^{+}$
51	50	rpcnd	$⊢ (φ \land 0 < A) \to 2 A \in ℂ$
52	50	rpne0d	$⊢ (φ \land 0 < A) \to 2 A \neq 0$
53		2ne0	$⊢ 2 \neq 0$
54	53	a1i	$⊢ (φ \land 0 < A) \to 2 \neq 0$
55	8 51 43 52 54	divcan5d	$⊢ (φ \land 0 < A) \to \frac{2 B^{2}}{2 2 A} = \frac{B^{2}}{2 A}$
56	46 47 55	3eqtr3d	$⊢ (φ \land 0 < A) \to 2 (\frac{B^{2}}{4 A}) = \frac{B^{2}}{2 A}$
57	40 56	eqtr3d	$⊢ (φ \land 0 < A) \to (\frac{B^{2}}{4 A}) + (\frac{B^{2}}{4 A}) = \frac{B^{2}}{2 A}$
58		oveq1	$⊢ x = - \frac{B}{2 A} \to x^{2} = {(- (\frac{B}{2 A}))}^{2}$
59	58	oveq2d	$⊢ x = - \frac{B}{2 A} \to A x^{2} = A {(- (\frac{B}{2 A}))}^{2}$
60		oveq2	$⊢ x = - \frac{B}{2 A} \to B x = B (- \frac{B}{2 A})$
61	59 60	oveq12d	$⊢ x = - \frac{B}{2 A} \to A x^{2} + B x = A {(- (\frac{B}{2 A}))}^{2} + B (- \frac{B}{2 A})$
62	61	oveq1d	$⊢ x = - \frac{B}{2 A} \to A x^{2} + B x + C = A {(- (\frac{B}{2 A}))}^{2} + B (- \frac{B}{2 A}) + C$
63	62	breq2d	$⊢ x = - \frac{B}{2 A} \to (0 \leq A x^{2} + B x + C \leftrightarrow 0 \leq A {(- (\frac{B}{2 A}))}^{2} + B (- \frac{B}{2 A}) + C)$
64	4	ralrimiva	$⊢ φ \to \forall x \in ℝ 0 \leq A x^{2} + B x + C$
65	64	adantr	$⊢ (φ \land 0 < A) \to \forall x \in ℝ 0 \leq A x^{2} + B x + C$
66	5 50	rerpdivcld	$⊢ (φ \land 0 < A) \to \frac{B}{2 A} \in ℝ$
67	66	renegcld	$⊢ (φ \land 0 < A) \to - \frac{B}{2 A} \in ℝ$
68	63 65 67	rspcdva	$⊢ (φ \land 0 < A) \to 0 \leq A {(- (\frac{B}{2 A}))}^{2} + B (- \frac{B}{2 A}) + C$
69	66	recnd	$⊢ (φ \land 0 < A) \to \frac{B}{2 A} \in ℂ$
70		sqneg	$⊢ \frac{B}{2 A} \in ℂ \to {(- (\frac{B}{2 A}))}^{2} = {(\frac{B}{2 A})}^{2}$
71	69 70	syl	$⊢ (φ \land 0 < A) \to {(- (\frac{B}{2 A}))}^{2} = {(\frac{B}{2 A})}^{2}$
72	5	recnd	$⊢ (φ \land 0 < A) \to B \in ℂ$
73		sqdiv	$⊢ (B \in ℂ \land 2 A \in ℂ \land 2 A \neq 0) \to {(\frac{B}{2 A})}^{2} = \frac{B^{2}}{{2 A}^{2}}$
74	72 51 52 73	syl3anc	$⊢ (φ \land 0 < A) \to {(\frac{B}{2 A})}^{2} = \frac{B^{2}}{{2 A}^{2}}$
75		sqval	$⊢ 2 A \in ℂ \to {2 A}^{2} = 2 A 2 A$
76	51 75	syl	$⊢ (φ \land 0 < A) \to {2 A}^{2} = 2 A 2 A$
77	51 43 26	mulassd	$⊢ (φ \land 0 < A) \to 2 A \cdot 2 A = 2 A 2 A$
78	43 26 43	mul32d	$⊢ (φ \land 0 < A) \to 2 A \cdot 2 = 2 \cdot 2 A$
79	78 42	eqtrdi	$⊢ (φ \land 0 < A) \to 2 A \cdot 2 = 4 A$
80	79	oveq1d	$⊢ (φ \land 0 < A) \to 2 A \cdot 2 A = 4 A A$
81	76 77 80	3eqtr2d	$⊢ (φ \land 0 < A) \to {2 A}^{2} = 4 A A$
82	81	oveq2d	$⊢ (φ \land 0 < A) \to \frac{B^{2}}{{2 A}^{2}} = \frac{B^{2}}{4 A A}$
83	71 74 82	3eqtrd	$⊢ (φ \land 0 < A) \to {(- (\frac{B}{2 A}))}^{2} = \frac{B^{2}}{4 A A}$
84	8 22 26 23 29	divdiv1d	$⊢ (φ \land 0 < A) \to \frac{\frac{B^{2}}{4 A}}{A} = \frac{B^{2}}{4 A A}$
85	83 84	eqtr4d	$⊢ (φ \land 0 < A) \to {(- (\frac{B}{2 A}))}^{2} = \frac{\frac{B^{2}}{4 A}}{A}$
86	85	oveq2d	$⊢ (φ \land 0 < A) \to A {(- (\frac{B}{2 A}))}^{2} = A (\frac{\frac{B^{2}}{4 A}}{A})$
87	39 26 29	divcan2d	$⊢ (φ \land 0 < A) \to A (\frac{\frac{B^{2}}{4 A}}{A}) = \frac{B^{2}}{4 A}$
88	86 87	eqtrd	$⊢ (φ \land 0 < A) \to A {(- (\frac{B}{2 A}))}^{2} = \frac{B^{2}}{4 A}$
89	72 69	mulneg2d	$⊢ (φ \land 0 < A) \to B (- \frac{B}{2 A}) = - B (\frac{B}{2 A})$
90		sqval	$⊢ B \in ℂ \to B^{2} = B B$
91	72 90	syl	$⊢ (φ \land 0 < A) \to B^{2} = B B$
92	91	oveq1d	$⊢ (φ \land 0 < A) \to \frac{B^{2}}{2 A} = \frac{B B}{2 A}$
93	72 72 51 52	divassd	$⊢ (φ \land 0 < A) \to \frac{B B}{2 A} = B (\frac{B}{2 A})$
94	92 93	eqtrd	$⊢ (φ \land 0 < A) \to \frac{B^{2}}{2 A} = B (\frac{B}{2 A})$
95	94	negeqd	$⊢ (φ \land 0 < A) \to - \frac{B^{2}}{2 A} = - B (\frac{B}{2 A})$
96	89 95	eqtr4d	$⊢ (φ \land 0 < A) \to B (- \frac{B}{2 A}) = - \frac{B^{2}}{2 A}$
97	88 96	oveq12d	$⊢ (φ \land 0 < A) \to A {(- (\frac{B}{2 A}))}^{2} + B (- \frac{B}{2 A}) = (\frac{B^{2}}{4 A}) + (- \frac{B^{2}}{2 A})$
98	7 50	rerpdivcld	$⊢ (φ \land 0 < A) \to \frac{B^{2}}{2 A} \in ℝ$
99	98	recnd	$⊢ (φ \land 0 < A) \to \frac{B^{2}}{2 A} \in ℂ$
100	39 99	negsubd	$⊢ (φ \land 0 < A) \to (\frac{B^{2}}{4 A}) + (- \frac{B^{2}}{2 A}) = (\frac{B^{2}}{4 A}) - (\frac{B^{2}}{2 A})$
101	97 100	eqtrd	$⊢ (φ \land 0 < A) \to A {(- (\frac{B}{2 A}))}^{2} + B (- \frac{B}{2 A}) = (\frac{B^{2}}{4 A}) - (\frac{B^{2}}{2 A})$
102	101	oveq1d	$⊢ (φ \land 0 < A) \to A {(- (\frac{B}{2 A}))}^{2} + B (- \frac{B}{2 A}) + C = (\frac{B^{2}}{4 A}) - (\frac{B^{2}}{2 A}) + C$
103	39 33 99	addsubd	$⊢ (φ \land 0 < A) \to (\frac{B^{2}}{4 A}) + C - (\frac{B^{2}}{2 A}) = (\frac{B^{2}}{4 A}) - (\frac{B^{2}}{2 A}) + C$
104	102 103	eqtr4d	$⊢ (φ \land 0 < A) \to A {(- (\frac{B}{2 A}))}^{2} + B (- \frac{B}{2 A}) + C = (\frac{B^{2}}{4 A}) + C - (\frac{B^{2}}{2 A})$
105	68 104	breqtrd	$⊢ (φ \land 0 < A) \to 0 \leq (\frac{B^{2}}{4 A}) + C - (\frac{B^{2}}{2 A})$
106	38 11	readdcld	$⊢ (φ \land 0 < A) \to (\frac{B^{2}}{4 A}) + C \in ℝ$
107	106 98	subge0d	$⊢ (φ \land 0 < A) \to (0 \leq (\frac{B^{2}}{4 A}) + C - (\frac{B^{2}}{2 A}) \leftrightarrow \frac{B^{2}}{2 A} \leq (\frac{B^{2}}{4 A}) + C)$
108	105 107	mpbid	$⊢ (φ \land 0 < A) \to \frac{B^{2}}{2 A} \leq (\frac{B^{2}}{4 A}) + C$
109	57 108	eqbrtrd	$⊢ (φ \land 0 < A) \to (\frac{B^{2}}{4 A}) + (\frac{B^{2}}{4 A}) \leq (\frac{B^{2}}{4 A}) + C$
110	38 11 38	leadd2d	$⊢ (φ \land 0 < A) \to (\frac{B^{2}}{4 A} \leq C \leftrightarrow (\frac{B^{2}}{4 A}) + (\frac{B^{2}}{4 A}) \leq (\frac{B^{2}}{4 A}) + C)$
111	109 110	mpbird	$⊢ (φ \land 0 < A) \to \frac{B^{2}}{4 A} \leq C$
112	38 11	suble0d	$⊢ (φ \land 0 < A) \to ((\frac{B^{2}}{4 A}) - C \leq 0 \leftrightarrow \frac{B^{2}}{4 A} \leq C)$
113	111 112	mpbird	$⊢ (φ \land 0 < A) \to (\frac{B^{2}}{4 A}) - C \leq 0$
114	37 113	eqbrtrd	$⊢ (φ \land 0 < A) \to \frac{B^{2} - 4 A C}{4 A} \leq 0$
115	7 14	resubcld	$⊢ (φ \land 0 < A) \to B^{2} - 4 A C \in ℝ$
116		0red	$⊢ (φ \land 0 < A) \to 0 \in ℝ$
117	115 116 21	ledivmuld	$⊢ (φ \land 0 < A) \to (\frac{B^{2} - 4 A C}{4 A} \leq 0 \leftrightarrow B^{2} - 4 A C \leq 4 A \cdot 0)$
118	114 117	mpbid	$⊢ (φ \land 0 < A) \to B^{2} - 4 A C \leq 4 A \cdot 0$
119	22	mul01d	$⊢ (φ \land 0 < A) \to 4 A \cdot 0 = 0$
120	118 119	breqtrd	$⊢ (φ \land 0 < A) \to B^{2} - 4 A C \leq 0$
121	3	adantr	$⊢ (φ \land (0 = A \land B \neq 0)) \to C \in ℝ$
122	121	ltp1d	$⊢ (φ \land (0 = A \land B \neq 0)) \to C < C + 1$
123		peano2re	$⊢ C \in ℝ \to C + 1 \in ℝ$
124	121 123	syl	$⊢ (φ \land (0 = A \land B \neq 0)) \to C + 1 \in ℝ$
125	121 124	ltnegd	$⊢ (φ \land (0 = A \land B \neq 0)) \to (C < C + 1 \leftrightarrow - (C + 1) < - C)$
126	122 125	mpbid	$⊢ (φ \land (0 = A \land B \neq 0)) \to - (C + 1) < - C$
127		df-neg	$⊢ - C = 0 - C$
128	126 127	breqtrdi	$⊢ (φ \land (0 = A \land B \neq 0)) \to - (C + 1) < 0 - C$
129	124	renegcld	$⊢ (φ \land (0 = A \land B \neq 0)) \to - (C + 1) \in ℝ$
130		0red	$⊢ (φ \land (0 = A \land B \neq 0)) \to 0 \in ℝ$
131	129 121 130	ltaddsubd	$⊢ (φ \land (0 = A \land B \neq 0)) \to (- (C + 1) + C < 0 \leftrightarrow - (C + 1) < 0 - C)$
132	128 131	mpbird	$⊢ (φ \land (0 = A \land B \neq 0)) \to - (C + 1) + C < 0$
133	132	expr	$⊢ (φ \land 0 = A) \to (B \neq 0 \to - (C + 1) + C < 0)$
134		oveq1	$⊢ x = \frac{- (C + 1)}{B} \to x^{2} = {(\frac{- (C + 1)}{B})}^{2}$
135	134	oveq2d	$⊢ x = \frac{- (C + 1)}{B} \to A x^{2} = A {(\frac{- (C + 1)}{B})}^{2}$
136		oveq2	$⊢ x = \frac{- (C + 1)}{B} \to B x = B (\frac{- (C + 1)}{B})$
137	135 136	oveq12d	$⊢ x = \frac{- (C + 1)}{B} \to A x^{2} + B x = A {(\frac{- (C + 1)}{B})}^{2} + B (\frac{- (C + 1)}{B})$
138	137	oveq1d	$⊢ x = \frac{- (C + 1)}{B} \to A x^{2} + B x + C = A {(\frac{- (C + 1)}{B})}^{2} + B (\frac{- (C + 1)}{B}) + C$
139	138	breq2d	$⊢ x = \frac{- (C + 1)}{B} \to (0 \leq A x^{2} + B x + C \leftrightarrow 0 \leq A {(\frac{- (C + 1)}{B})}^{2} + B (\frac{- (C + 1)}{B}) + C)$
140	64	adantr	$⊢ (φ \land (0 = A \land B \neq 0)) \to \forall x \in ℝ 0 \leq A x^{2} + B x + C$
141	2	adantr	$⊢ (φ \land (0 = A \land B \neq 0)) \to B \in ℝ$
142		simprr	$⊢ (φ \land (0 = A \land B \neq 0)) \to B \neq 0$
143	129 141 142	redivcld	$⊢ (φ \land (0 = A \land B \neq 0)) \to \frac{- (C + 1)}{B} \in ℝ$
144	139 140 143	rspcdva	$⊢ (φ \land (0 = A \land B \neq 0)) \to 0 \leq A {(\frac{- (C + 1)}{B})}^{2} + B (\frac{- (C + 1)}{B}) + C$
145		simprl	$⊢ (φ \land (0 = A \land B \neq 0)) \to 0 = A$
146	145	oveq1d	$⊢ (φ \land (0 = A \land B \neq 0)) \to 0 \cdot {(\frac{- (C + 1)}{B})}^{2} = A {(\frac{- (C + 1)}{B})}^{2}$
147	143	recnd	$⊢ (φ \land (0 = A \land B \neq 0)) \to \frac{- (C + 1)}{B} \in ℂ$
148		sqcl	$⊢ \frac{- (C + 1)}{B} \in ℂ \to {(\frac{- (C + 1)}{B})}^{2} \in ℂ$
149	147 148	syl	$⊢ (φ \land (0 = A \land B \neq 0)) \to {(\frac{- (C + 1)}{B})}^{2} \in ℂ$
150	149	mul02d	$⊢ (φ \land (0 = A \land B \neq 0)) \to 0 \cdot {(\frac{- (C + 1)}{B})}^{2} = 0$
151	146 150	eqtr3d	$⊢ (φ \land (0 = A \land B \neq 0)) \to A {(\frac{- (C + 1)}{B})}^{2} = 0$
152	129	recnd	$⊢ (φ \land (0 = A \land B \neq 0)) \to - (C + 1) \in ℂ$
153	141	recnd	$⊢ (φ \land (0 = A \land B \neq 0)) \to B \in ℂ$
154	152 153 142	divcan2d	$⊢ (φ \land (0 = A \land B \neq 0)) \to B (\frac{- (C + 1)}{B}) = - (C + 1)$
155	151 154	oveq12d	$⊢ (φ \land (0 = A \land B \neq 0)) \to A {(\frac{- (C + 1)}{B})}^{2} + B (\frac{- (C + 1)}{B}) = 0 + (- (C + 1))$
156	152	addlidd	$⊢ (φ \land (0 = A \land B \neq 0)) \to 0 + (- (C + 1)) = - (C + 1)$
157	155 156	eqtrd	$⊢ (φ \land (0 = A \land B \neq 0)) \to A {(\frac{- (C + 1)}{B})}^{2} + B (\frac{- (C + 1)}{B}) = - (C + 1)$
158	157	oveq1d	$⊢ (φ \land (0 = A \land B \neq 0)) \to A {(\frac{- (C + 1)}{B})}^{2} + B (\frac{- (C + 1)}{B}) + C = - (C + 1) + C$
159	144 158	breqtrd	$⊢ (φ \land (0 = A \land B \neq 0)) \to 0 \leq - (C + 1) + C$
160		0re	$⊢ 0 \in ℝ$
161	129 121	readdcld	$⊢ (φ \land (0 = A \land B \neq 0)) \to - (C + 1) + C \in ℝ$
162		lenlt	$⊢ (0 \in ℝ \land - (C + 1) + C \in ℝ) \to (0 \leq - (C + 1) + C \leftrightarrow \neg - (C + 1) + C < 0)$
163	160 161 162	sylancr	$⊢ (φ \land (0 = A \land B \neq 0)) \to (0 \leq - (C + 1) + C \leftrightarrow \neg - (C + 1) + C < 0)$
164	159 163	mpbid	$⊢ (φ \land (0 = A \land B \neq 0)) \to \neg - (C + 1) + C < 0$
165	164	expr	$⊢ (φ \land 0 = A) \to (B \neq 0 \to \neg - (C + 1) + C < 0)$
166	133 165	pm2.65d	$⊢ (φ \land 0 = A) \to \neg B \neq 0$
167		nne	$⊢ \neg B \neq 0 \leftrightarrow B = 0$
168	166 167	sylib	$⊢ (φ \land 0 = A) \to B = 0$
169	168	sq0id	$⊢ (φ \land 0 = A) \to B^{2} = 0$
170		simpr	$⊢ (φ \land 0 = A) \to 0 = A$
171	170	oveq1d	$⊢ (φ \land 0 = A) \to 0 \cdot C = A C$
172	3	recnd	$⊢ φ \to C \in ℂ$
173	172	adantr	$⊢ (φ \land 0 = A) \to C \in ℂ$
174	173	mul02d	$⊢ (φ \land 0 = A) \to 0 \cdot C = 0$
175	171 174	eqtr3d	$⊢ (φ \land 0 = A) \to A C = 0$
176	175	oveq2d	$⊢ (φ \land 0 = A) \to 4 A C = 4 \cdot 0$
177	27	mul01i	$⊢ 4 \cdot 0 = 0$
178	176 177	eqtrdi	$⊢ (φ \land 0 = A) \to 4 A C = 0$
179	169 178	oveq12d	$⊢ (φ \land 0 = A) \to B^{2} - 4 A C = 0 - 0$
180		0m0e0	$⊢ 0 - 0 = 0$
181		0le0	$⊢ 0 \leq 0$
182	180 181	eqbrtri	$⊢ 0 - 0 \leq 0$
183	179 182	eqbrtrdi	$⊢ (φ \land 0 = A) \to B^{2} - 4 A C \leq 0$
184		eqid	$⊢ if (1 \leq \frac{B + if (0 \leq C, C, 0) + 1}{- A}, \frac{B + if (0 \leq C, C, 0) + 1}{- A}, 1) = if (1 \leq \frac{B + if (0 \leq C, C, 0) + 1}{- A}, \frac{B + if (0 \leq C, C, 0) + 1}{- A}, 1)$
185	1 2 3 4 184	discr1	$⊢ φ \to 0 \leq A$
186		leloe	$⊢ (0 \in ℝ \land A \in ℝ) \to (0 \leq A \leftrightarrow (0 < A \lor 0 = A))$
187	160 1 186	sylancr	$⊢ φ \to (0 \leq A \leftrightarrow (0 < A \lor 0 = A))$
188	185 187	mpbid	$⊢ φ \to (0 < A \lor 0 = A)$
189	120 183 188	mpjaodan	$⊢ φ \to B^{2} - 4 A C \leq 0$

Metamath Proof Explorer

Theorem discr

Proof