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 
|- ( ph -> A e. RR )
discr.2 
|- ( ph -> B e. RR )
discr.3 
|- ( ph -> C e. RR )
discr.4 
|- ( ( ph /\ x e. RR ) -> 0 <_ ( ( ( A x. ( x ^ 2 ) ) + ( B x. x ) ) + C ) )
discr1.5 
|- X = if ( 1 <_ ( ( ( B + if ( 0 <_ C , C , 0 ) ) + 1 ) / -u A ) , ( ( ( B + if ( 0 <_ C , C , 0 ) ) + 1 ) / -u A ) , 1 )
Assertion discr1 
|- ( ph -> 0 <_ A )

Proof

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