This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 eqtr3id ⊢ ( ( 𝜑 ∧ 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 eqtrdi ⊢ ( ( 𝜑 ∧ 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 addlidd ⊢ ( ( 𝜑 ∧ ( 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 eqtrdi ⊢ ( ( 𝜑 ∧ 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 )