Metamath Proof Explorer

Theorem discr1

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

Ref Expression
Hypotheses discr.1 ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
discr.2 ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
discr.3 ⊢ ( 𝜑 → 𝐶 ∈ ℝ )
discr.4 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → 0 ≤ ( ( ( 𝐴 · ( 𝑥 ↑ 2 ) ) + ( 𝐵 · 𝑥 ) ) + 𝐶 ) )
discr1.5 ⊢ 𝑋 = if ( 1 ≤ ( ( ( 𝐵 + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) + 1 ) / - 𝐴 ) , ( ( ( 𝐵 + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) + 1 ) / - 𝐴 ) , 1 )
Assertion discr1 ( 𝜑 → 0 ≤ 𝐴 )

Proof

Step Hyp Ref Expression
1 discr.1 ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
2 discr.2 ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
3 discr.3 ⊢ ( 𝜑 → 𝐶 ∈ ℝ )
4 discr.4 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → 0 ≤ ( ( ( 𝐴 · ( 𝑥 ↑ 2 ) ) + ( 𝐵 · 𝑥 ) ) + 𝐶 ) )
5 discr1.5 ⊢ 𝑋 = if ( 1 ≤ ( ( ( 𝐵 + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) + 1 ) / - 𝐴 ) , ( ( ( 𝐵 + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) + 1 ) / - 𝐴 ) , 1 )
6 oveq1 ⊢ ( 𝑥 = 𝑋 → ( 𝑥 ↑ 2 ) = ( 𝑋 ↑ 2 ) )
7 6 oveq2d ⊢ ( 𝑥 = 𝑋 → ( 𝐴 · ( 𝑥 ↑ 2 ) ) = ( 𝐴 · ( 𝑋 ↑ 2 ) ) )
8 oveq2 ⊢ ( 𝑥 = 𝑋 → ( 𝐵 · 𝑥 ) = ( 𝐵 · 𝑋 ) )
9 7 8 oveq12d ⊢ ( 𝑥 = 𝑋 → ( ( 𝐴 · ( 𝑥 ↑ 2 ) ) + ( 𝐵 · 𝑥 ) ) = ( ( 𝐴 · ( 𝑋 ↑ 2 ) ) + ( 𝐵 · 𝑋 ) ) )
10 9 oveq1d ⊢ ( 𝑥 = 𝑋 → ( ( ( 𝐴 · ( 𝑥 ↑ 2 ) ) + ( 𝐵 · 𝑥 ) ) + 𝐶 ) = ( ( ( 𝐴 · ( 𝑋 ↑ 2 ) ) + ( 𝐵 · 𝑋 ) ) + 𝐶 ) )
11 10 breq2d ⊢ ( 𝑥 = 𝑋 → ( 0 ≤ ( ( ( 𝐴 · ( 𝑥 ↑ 2 ) ) + ( 𝐵 · 𝑥 ) ) + 𝐶 ) ↔ 0 ≤ ( ( ( 𝐴 · ( 𝑋 ↑ 2 ) ) + ( 𝐵 · 𝑋 ) ) + 𝐶 ) ) )
12 4 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ ℝ 0 ≤ ( ( ( 𝐴 · ( 𝑥 ↑ 2 ) ) + ( 𝐵 · 𝑥 ) ) + 𝐶 ) )
13 12 adantr ⊢ ( ( 𝜑 ∧ 𝐴 < 0 ) → ∀ 𝑥 ∈ ℝ 0 ≤ ( ( ( 𝐴 · ( 𝑥 ↑ 2 ) ) + ( 𝐵 · 𝑥 ) ) + 𝐶 ) )
14 2 adantr ⊢ ( ( 𝜑 ∧ 𝐴 < 0 ) → 𝐵 ∈ ℝ )
15 3 adantr ⊢ ( ( 𝜑 ∧ 𝐴 < 0 ) → 𝐶 ∈ ℝ )
16 0re ⊢ 0 ∈ ℝ
17 ifcl ⊢ ( ( 𝐶 ∈ ℝ ∧ 0 ∈ ℝ ) → if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ∈ ℝ )
18 15 16 17 sylancl ⊢ ( ( 𝜑 ∧ 𝐴 < 0 ) → if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ∈ ℝ )
19 14 18 readdcld ⊢ ( ( 𝜑 ∧ 𝐴 < 0 ) → ( 𝐵 + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) ∈ ℝ )
20 peano2re ⊢ ( ( 𝐵 + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) ∈ ℝ → ( ( 𝐵 + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) + 1 ) ∈ ℝ )
21 19 20 syl ⊢ ( ( 𝜑 ∧ 𝐴 < 0 ) → ( ( 𝐵 + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) + 1 ) ∈ ℝ )
22 1 adantr ⊢ ( ( 𝜑 ∧ 𝐴 < 0 ) → 𝐴 ∈ ℝ )
23 22 renegcld ⊢ ( ( 𝜑 ∧ 𝐴 < 0 ) → - 𝐴 ∈ ℝ )
24 1 lt0neg1d ⊢ ( 𝜑 → ( 𝐴 < 0 ↔ 0 < - 𝐴 ) )
25 24 biimpa ⊢ ( ( 𝜑 ∧ 𝐴 < 0 ) → 0 < - 𝐴 )
26 25 gt0ne0d ⊢ ( ( 𝜑 ∧ 𝐴 < 0 ) → - 𝐴 ≠ 0 )
27 21 23 26 redivcld ⊢ ( ( 𝜑 ∧ 𝐴 < 0 ) → ( ( ( 𝐵 + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) + 1 ) / - 𝐴 ) ∈ ℝ )
28 1re ⊢ 1 ∈ ℝ
29 ifcl ⊢ ( ( ( ( ( 𝐵 + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) + 1 ) / - 𝐴 ) ∈ ℝ ∧ 1 ∈ ℝ ) → if ( 1 ≤ ( ( ( 𝐵 + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) + 1 ) / - 𝐴 ) , ( ( ( 𝐵 + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) + 1 ) / - 𝐴 ) , 1 ) ∈ ℝ )
30 27 28 29 sylancl ⊢ ( ( 𝜑 ∧ 𝐴 < 0 ) → if ( 1 ≤ ( ( ( 𝐵 + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) + 1 ) / - 𝐴 ) , ( ( ( 𝐵 + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) + 1 ) / - 𝐴 ) , 1 ) ∈ ℝ )
31 5 30 eqeltrid ⊢ ( ( 𝜑 ∧ 𝐴 < 0 ) → 𝑋 ∈ ℝ )
32 11 13 31 rspcdva ⊢ ( ( 𝜑 ∧ 𝐴 < 0 ) → 0 ≤ ( ( ( 𝐴 · ( 𝑋 ↑ 2 ) ) + ( 𝐵 · 𝑋 ) ) + 𝐶 ) )
33 resqcl ⊢ ( 𝑋 ∈ ℝ → ( 𝑋 ↑ 2 ) ∈ ℝ )
34 31 33 syl ⊢ ( ( 𝜑 ∧ 𝐴 < 0 ) → ( 𝑋 ↑ 2 ) ∈ ℝ )
35 22 34 remulcld ⊢ ( ( 𝜑 ∧ 𝐴 < 0 ) → ( 𝐴 · ( 𝑋 ↑ 2 ) ) ∈ ℝ )
36 14 31 remulcld ⊢ ( ( 𝜑 ∧ 𝐴 < 0 ) → ( 𝐵 · 𝑋 ) ∈ ℝ )
37 35 36 readdcld ⊢ ( ( 𝜑 ∧ 𝐴 < 0 ) → ( ( 𝐴 · ( 𝑋 ↑ 2 ) ) + ( 𝐵 · 𝑋 ) ) ∈ ℝ )
38 37 15 readdcld ⊢ ( ( 𝜑 ∧ 𝐴 < 0 ) → ( ( ( 𝐴 · ( 𝑋 ↑ 2 ) ) + ( 𝐵 · 𝑋 ) ) + 𝐶 ) ∈ ℝ )
39 22 31 remulcld ⊢ ( ( 𝜑 ∧ 𝐴 < 0 ) → ( 𝐴 · 𝑋 ) ∈ ℝ )
40 39 19 readdcld ⊢ ( ( 𝜑 ∧ 𝐴 < 0 ) → ( ( 𝐴 · 𝑋 ) + ( 𝐵 + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) ) ∈ ℝ )
41 40 31 remulcld ⊢ ( ( 𝜑 ∧ 𝐴 < 0 ) → ( ( ( 𝐴 · 𝑋 ) + ( 𝐵 + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) ) · 𝑋 ) ∈ ℝ )
42 16 a1i ⊢ ( ( 𝜑 ∧ 𝐴 < 0 ) → 0 ∈ ℝ )
43 18 31 remulcld ⊢ ( ( 𝜑 ∧ 𝐴 < 0 ) → ( if ( 0 ≤ 𝐶 , 𝐶 , 0 ) · 𝑋 ) ∈ ℝ )
44 max2 ⊢ ( ( 0 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → 𝐶 ≤ if ( 0 ≤ 𝐶 , 𝐶 , 0 ) )
45 16 15 44 sylancr ⊢ ( ( 𝜑 ∧ 𝐴 < 0 ) → 𝐶 ≤ if ( 0 ≤ 𝐶 , 𝐶 , 0 ) )
46 max1 ⊢ ( ( 0 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → 0 ≤ if ( 0 ≤ 𝐶 , 𝐶 , 0 ) )
47 16 15 46 sylancr ⊢ ( ( 𝜑 ∧ 𝐴 < 0 ) → 0 ≤ if ( 0 ≤ 𝐶 , 𝐶 , 0 ) )
48 max1 ⊢ ( ( 1 ∈ ℝ ∧ ( ( ( 𝐵 + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) + 1 ) / - 𝐴 ) ∈ ℝ ) → 1 ≤ if ( 1 ≤ ( ( ( 𝐵 + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) + 1 ) / - 𝐴 ) , ( ( ( 𝐵 + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) + 1 ) / - 𝐴 ) , 1 ) )
49 28 27 48 sylancr ⊢ ( ( 𝜑 ∧ 𝐴 < 0 ) → 1 ≤ if ( 1 ≤ ( ( ( 𝐵 + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) + 1 ) / - 𝐴 ) , ( ( ( 𝐵 + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) + 1 ) / - 𝐴 ) , 1 ) )
50 49 5 breqtrrdi ⊢ ( ( 𝜑 ∧ 𝐴 < 0 ) → 1 ≤ 𝑋 )
51 18 31 47 50 lemulge11d ⊢ ( ( 𝜑 ∧ 𝐴 < 0 ) → if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ≤ ( if ( 0 ≤ 𝐶 , 𝐶 , 0 ) · 𝑋 ) )
52 15 18 43 45 51 letrd ⊢ ( ( 𝜑 ∧ 𝐴 < 0 ) → 𝐶 ≤ ( if ( 0 ≤ 𝐶 , 𝐶 , 0 ) · 𝑋 ) )
53 15 43 37 52 leadd2dd ⊢ ( ( 𝜑 ∧ 𝐴 < 0 ) → ( ( ( 𝐴 · ( 𝑋 ↑ 2 ) ) + ( 𝐵 · 𝑋 ) ) + 𝐶 ) ≤ ( ( ( 𝐴 · ( 𝑋 ↑ 2 ) ) + ( 𝐵 · 𝑋 ) ) + ( if ( 0 ≤ 𝐶 , 𝐶 , 0 ) · 𝑋 ) ) )
54 39 14 readdcld ⊢ ( ( 𝜑 ∧ 𝐴 < 0 ) → ( ( 𝐴 · 𝑋 ) + 𝐵 ) ∈ ℝ )
55 54 recnd ⊢ ( ( 𝜑 ∧ 𝐴 < 0 ) → ( ( 𝐴 · 𝑋 ) + 𝐵 ) ∈ ℂ )
56 18 recnd ⊢ ( ( 𝜑 ∧ 𝐴 < 0 ) → if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ∈ ℂ )
57 31 recnd ⊢ ( ( 𝜑 ∧ 𝐴 < 0 ) → 𝑋 ∈ ℂ )
58 55 56 57 adddird ⊢ ( ( 𝜑 ∧ 𝐴 < 0 ) → ( ( ( ( 𝐴 · 𝑋 ) + 𝐵 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) · 𝑋 ) = ( ( ( ( 𝐴 · 𝑋 ) + 𝐵 ) · 𝑋 ) + ( if ( 0 ≤ 𝐶 , 𝐶 , 0 ) · 𝑋 ) ) )
59 39 recnd ⊢ ( ( 𝜑 ∧ 𝐴 < 0 ) → ( 𝐴 · 𝑋 ) ∈ ℂ )
60 14 recnd ⊢ ( ( 𝜑 ∧ 𝐴 < 0 ) → 𝐵 ∈ ℂ )
61 59 60 56 addassd ⊢ ( ( 𝜑 ∧ 𝐴 < 0 ) → ( ( ( 𝐴 · 𝑋 ) + 𝐵 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) = ( ( 𝐴 · 𝑋 ) + ( 𝐵 + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) ) )
62 61 oveq1d ⊢ ( ( 𝜑 ∧ 𝐴 < 0 ) → ( ( ( ( 𝐴 · 𝑋 ) + 𝐵 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) · 𝑋 ) = ( ( ( 𝐴 · 𝑋 ) + ( 𝐵 + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) ) · 𝑋 ) )
63 22 recnd ⊢ ( ( 𝜑 ∧ 𝐴 < 0 ) → 𝐴 ∈ ℂ )
64 63 57 57 mulassd ⊢ ( ( 𝜑 ∧ 𝐴 < 0 ) → ( ( 𝐴 · 𝑋 ) · 𝑋 ) = ( 𝐴 · ( 𝑋 · 𝑋 ) ) )
65 sqval ⊢ ( 𝑋 ∈ ℂ → ( 𝑋 ↑ 2 ) = ( 𝑋 · 𝑋 ) )
66 57 65 syl ⊢ ( ( 𝜑 ∧ 𝐴 < 0 ) → ( 𝑋 ↑ 2 ) = ( 𝑋 · 𝑋 ) )
67 66 oveq2d ⊢ ( ( 𝜑 ∧ 𝐴 < 0 ) → ( 𝐴 · ( 𝑋 ↑ 2 ) ) = ( 𝐴 · ( 𝑋 · 𝑋 ) ) )
68 64 67 eqtr4d ⊢ ( ( 𝜑 ∧ 𝐴 < 0 ) → ( ( 𝐴 · 𝑋 ) · 𝑋 ) = ( 𝐴 · ( 𝑋 ↑ 2 ) ) )
69 68 oveq1d ⊢ ( ( 𝜑 ∧ 𝐴 < 0 ) → ( ( ( 𝐴 · 𝑋 ) · 𝑋 ) + ( 𝐵 · 𝑋 ) ) = ( ( 𝐴 · ( 𝑋 ↑ 2 ) ) + ( 𝐵 · 𝑋 ) ) )
70 59 57 60 69 joinlmuladdmuld ⊢ ( ( 𝜑 ∧ 𝐴 < 0 ) → ( ( ( 𝐴 · 𝑋 ) + 𝐵 ) · 𝑋 ) = ( ( 𝐴 · ( 𝑋 ↑ 2 ) ) + ( 𝐵 · 𝑋 ) ) )
71 70 oveq1d ⊢ ( ( 𝜑 ∧ 𝐴 < 0 ) → ( ( ( ( 𝐴 · 𝑋 ) + 𝐵 ) · 𝑋 ) + ( if ( 0 ≤ 𝐶 , 𝐶 , 0 ) · 𝑋 ) ) = ( ( ( 𝐴 · ( 𝑋 ↑ 2 ) ) + ( 𝐵 · 𝑋 ) ) + ( if ( 0 ≤ 𝐶 , 𝐶 , 0 ) · 𝑋 ) ) )
72 58 62 71 3eqtr3d ⊢ ( ( 𝜑 ∧ 𝐴 < 0 ) → ( ( ( 𝐴 · 𝑋 ) + ( 𝐵 + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) ) · 𝑋 ) = ( ( ( 𝐴 · ( 𝑋 ↑ 2 ) ) + ( 𝐵 · 𝑋 ) ) + ( if ( 0 ≤ 𝐶 , 𝐶 , 0 ) · 𝑋 ) ) )
73 53 72 breqtrrd ⊢ ( ( 𝜑 ∧ 𝐴 < 0 ) → ( ( ( 𝐴 · ( 𝑋 ↑ 2 ) ) + ( 𝐵 · 𝑋 ) ) + 𝐶 ) ≤ ( ( ( 𝐴 · 𝑋 ) + ( 𝐵 + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) ) · 𝑋 ) )
74 23 31 remulcld ⊢ ( ( 𝜑 ∧ 𝐴 < 0 ) → ( - 𝐴 · 𝑋 ) ∈ ℝ )
75 19 ltp1d ⊢ ( ( 𝜑 ∧ 𝐴 < 0 ) → ( 𝐵 + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) < ( ( 𝐵 + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) + 1 ) )
76 max2 ⊢ ( ( 1 ∈ ℝ ∧ ( ( ( 𝐵 + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) + 1 ) / - 𝐴 ) ∈ ℝ ) → ( ( ( 𝐵 + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) + 1 ) / - 𝐴 ) ≤ if ( 1 ≤ ( ( ( 𝐵 + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) + 1 ) / - 𝐴 ) , ( ( ( 𝐵 + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) + 1 ) / - 𝐴 ) , 1 ) )
77 28 27 76 sylancr ⊢ ( ( 𝜑 ∧ 𝐴 < 0 ) → ( ( ( 𝐵 + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) + 1 ) / - 𝐴 ) ≤ if ( 1 ≤ ( ( ( 𝐵 + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) + 1 ) / - 𝐴 ) , ( ( ( 𝐵 + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) + 1 ) / - 𝐴 ) , 1 ) )
78 77 5 breqtrrdi ⊢ ( ( 𝜑 ∧ 𝐴 < 0 ) → ( ( ( 𝐵 + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) + 1 ) / - 𝐴 ) ≤ 𝑋 )
79 ledivmul ⊢ ( ( ( ( 𝐵 + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) + 1 ) ∈ ℝ ∧ 𝑋 ∈ ℝ ∧ ( - 𝐴 ∈ ℝ ∧ 0 < - 𝐴 ) ) → ( ( ( ( 𝐵 + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) + 1 ) / - 𝐴 ) ≤ 𝑋 ↔ ( ( 𝐵 + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) + 1 ) ≤ ( - 𝐴 · 𝑋 ) ) )
80 21 31 23 25 79 syl112anc ⊢ ( ( 𝜑 ∧ 𝐴 < 0 ) → ( ( ( ( 𝐵 + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) + 1 ) / - 𝐴 ) ≤ 𝑋 ↔ ( ( 𝐵 + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) + 1 ) ≤ ( - 𝐴 · 𝑋 ) ) )
81 78 80 mpbid ⊢ ( ( 𝜑 ∧ 𝐴 < 0 ) → ( ( 𝐵 + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) + 1 ) ≤ ( - 𝐴 · 𝑋 ) )
82 19 21 74 75 81 ltletrd ⊢ ( ( 𝜑 ∧ 𝐴 < 0 ) → ( 𝐵 + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) < ( - 𝐴 · 𝑋 ) )
83 63 57 mulneg1d ⊢ ( ( 𝜑 ∧ 𝐴 < 0 ) → ( - 𝐴 · 𝑋 ) = - ( 𝐴 · 𝑋 ) )
84 df-neg ⊢ - ( 𝐴 · 𝑋 ) = ( 0 − ( 𝐴 · 𝑋 ) )
85 83 84 eqtrdi ⊢ ( ( 𝜑 ∧ 𝐴 < 0 ) → ( - 𝐴 · 𝑋 ) = ( 0 − ( 𝐴 · 𝑋 ) ) )
86 82 85 breqtrd ⊢ ( ( 𝜑 ∧ 𝐴 < 0 ) → ( 𝐵 + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) < ( 0 − ( 𝐴 · 𝑋 ) ) )
87 39 19 42 ltaddsub2d ⊢ ( ( 𝜑 ∧ 𝐴 < 0 ) → ( ( ( 𝐴 · 𝑋 ) + ( 𝐵 + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) ) < 0 ↔ ( 𝐵 + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) < ( 0 − ( 𝐴 · 𝑋 ) ) ) )
88 86 87 mpbird ⊢ ( ( 𝜑 ∧ 𝐴 < 0 ) → ( ( 𝐴 · 𝑋 ) + ( 𝐵 + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) ) < 0 )
89 28 a1i ⊢ ( ( 𝜑 ∧ 𝐴 < 0 ) → 1 ∈ ℝ )
90 0lt1 ⊢ 0 < 1
91 90 a1i ⊢ ( ( 𝜑 ∧ 𝐴 < 0 ) → 0 < 1 )
92 42 89 31 91 50 ltletrd ⊢ ( ( 𝜑 ∧ 𝐴 < 0 ) → 0 < 𝑋 )
93 ltmul1 ⊢ ( ( ( ( 𝐴 · 𝑋 ) + ( 𝐵 + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) ) ∈ ℝ ∧ 0 ∈ ℝ ∧ ( 𝑋 ∈ ℝ ∧ 0 < 𝑋 ) ) → ( ( ( 𝐴 · 𝑋 ) + ( 𝐵 + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) ) < 0 ↔ ( ( ( 𝐴 · 𝑋 ) + ( 𝐵 + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) ) · 𝑋 ) < ( 0 · 𝑋 ) ) )
94 40 42 31 92 93 syl112anc ⊢ ( ( 𝜑 ∧ 𝐴 < 0 ) → ( ( ( 𝐴 · 𝑋 ) + ( 𝐵 + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) ) < 0 ↔ ( ( ( 𝐴 · 𝑋 ) + ( 𝐵 + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) ) · 𝑋 ) < ( 0 · 𝑋 ) ) )
95 88 94 mpbid ⊢ ( ( 𝜑 ∧ 𝐴 < 0 ) → ( ( ( 𝐴 · 𝑋 ) + ( 𝐵 + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) ) · 𝑋 ) < ( 0 · 𝑋 ) )
96 57 mul02d ⊢ ( ( 𝜑 ∧ 𝐴 < 0 ) → ( 0 · 𝑋 ) = 0 )
97 95 96 breqtrd ⊢ ( ( 𝜑 ∧ 𝐴 < 0 ) → ( ( ( 𝐴 · 𝑋 ) + ( 𝐵 + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) ) · 𝑋 ) < 0 )
98 38 41 42 73 97 lelttrd ⊢ ( ( 𝜑 ∧ 𝐴 < 0 ) → ( ( ( 𝐴 · ( 𝑋 ↑ 2 ) ) + ( 𝐵 · 𝑋 ) ) + 𝐶 ) < 0 )
99 ltnle ⊢ ( ( ( ( ( 𝐴 · ( 𝑋 ↑ 2 ) ) + ( 𝐵 · 𝑋 ) ) + 𝐶 ) ∈ ℝ ∧ 0 ∈ ℝ ) → ( ( ( ( 𝐴 · ( 𝑋 ↑ 2 ) ) + ( 𝐵 · 𝑋 ) ) + 𝐶 ) < 0 ↔ ¬ 0 ≤ ( ( ( 𝐴 · ( 𝑋 ↑ 2 ) ) + ( 𝐵 · 𝑋 ) ) + 𝐶 ) ) )
100 38 16 99 sylancl ⊢ ( ( 𝜑 ∧ 𝐴 < 0 ) → ( ( ( ( 𝐴 · ( 𝑋 ↑ 2 ) ) + ( 𝐵 · 𝑋 ) ) + 𝐶 ) < 0 ↔ ¬ 0 ≤ ( ( ( 𝐴 · ( 𝑋 ↑ 2 ) ) + ( 𝐵 · 𝑋 ) ) + 𝐶 ) ) )
101 98 100 mpbid ⊢ ( ( 𝜑 ∧ 𝐴 < 0 ) → ¬ 0 ≤ ( ( ( 𝐴 · ( 𝑋 ↑ 2 ) ) + ( 𝐵 · 𝑋 ) ) + 𝐶 ) )
102 32 101 pm2.65da ⊢ ( 𝜑 → ¬ 𝐴 < 0 )
103 lelttric ⊢ ( ( 0 ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( 0 ≤ 𝐴 ∨ 𝐴 < 0 ) )
104 16 1 103 sylancr ⊢ ( 𝜑 → ( 0 ≤ 𝐴 ∨ 𝐴 < 0 ) )
105 104 ord ⊢ ( 𝜑 → ( ¬ 0 ≤ 𝐴 → 𝐴 < 0 ) )
106 102 105 mt3d ⊢ ( 𝜑 → 0 ≤ 𝐴 )