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 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 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 )