Theorem 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	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
	discr.2	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
	discr.3	⊢ ( 𝜑 → 𝐶 ∈ ℝ )
	discr.4	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → 0 ≤ ( ( ( 𝐴 · ( 𝑥 ↑ 2 ) ) + ( 𝐵 · 𝑥 ) ) + 𝐶 ) )
Assertion	discr	⊢ ( 𝜑 → ( ( 𝐵 ↑ 2 ) − ( 4 · ( 𝐴 · 𝐶 ) ) ) ≤ 0 )

Proof

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