Metamath Proof Explorer


Theorem requad01

Description: A condition for a quadratic equation with real coefficients to have (at least) one real solution. (Contributed by AV, 23-Jan-2023)

Ref Expression
Hypotheses requad2.a
|- ( ph -> A e. RR )
requad2.z
|- ( ph -> A =/= 0 )
requad2.b
|- ( ph -> B e. RR )
requad2.c
|- ( ph -> C e. RR )
requad2.d
|- ( ph -> D = ( ( B ^ 2 ) - ( 4 x. ( A x. C ) ) ) )
Assertion requad01
|- ( ph -> ( E. x e. RR ( ( A x. ( x ^ 2 ) ) + ( ( B x. x ) + C ) ) = 0 <-> 0 <_ D ) )

Proof

Step Hyp Ref Expression
1 requad2.a
 |-  ( ph -> A e. RR )
2 requad2.z
 |-  ( ph -> A =/= 0 )
3 requad2.b
 |-  ( ph -> B e. RR )
4 requad2.c
 |-  ( ph -> C e. RR )
5 requad2.d
 |-  ( ph -> D = ( ( B ^ 2 ) - ( 4 x. ( A x. C ) ) ) )
6 1 recnd
 |-  ( ph -> A e. CC )
7 6 adantr
 |-  ( ( ph /\ x e. RR ) -> A e. CC )
8 2 adantr
 |-  ( ( ph /\ x e. RR ) -> A =/= 0 )
9 3 recnd
 |-  ( ph -> B e. CC )
10 9 adantr
 |-  ( ( ph /\ x e. RR ) -> B e. CC )
11 4 recnd
 |-  ( ph -> C e. CC )
12 11 adantr
 |-  ( ( ph /\ x e. RR ) -> C e. CC )
13 recn
 |-  ( x e. RR -> x e. CC )
14 13 adantl
 |-  ( ( ph /\ x e. RR ) -> x e. CC )
15 5 adantr
 |-  ( ( ph /\ x e. RR ) -> D = ( ( B ^ 2 ) - ( 4 x. ( A x. C ) ) ) )
16 7 8 10 12 14 15 quad
 |-  ( ( ph /\ x e. RR ) -> ( ( ( A x. ( x ^ 2 ) ) + ( ( B x. x ) + C ) ) = 0 <-> ( x = ( ( -u B + ( sqrt ` D ) ) / ( 2 x. A ) ) \/ x = ( ( -u B - ( sqrt ` D ) ) / ( 2 x. A ) ) ) ) )
17 eleq1
 |-  ( x = ( ( -u B + ( sqrt ` D ) ) / ( 2 x. A ) ) -> ( x e. RR <-> ( ( -u B + ( sqrt ` D ) ) / ( 2 x. A ) ) e. RR ) )
18 17 adantl
 |-  ( ( ph /\ x = ( ( -u B + ( sqrt ` D ) ) / ( 2 x. A ) ) ) -> ( x e. RR <-> ( ( -u B + ( sqrt ` D ) ) / ( 2 x. A ) ) e. RR ) )
19 2re
 |-  2 e. RR
20 19 a1i
 |-  ( ph -> 2 e. RR )
21 20 1 remulcld
 |-  ( ph -> ( 2 x. A ) e. RR )
22 21 adantr
 |-  ( ( ph /\ -. 0 <_ D ) -> ( 2 x. A ) e. RR )
23 9 negcld
 |-  ( ph -> -u B e. CC )
24 3 resqcld
 |-  ( ph -> ( B ^ 2 ) e. RR )
25 4re
 |-  4 e. RR
26 25 a1i
 |-  ( ph -> 4 e. RR )
27 1 4 remulcld
 |-  ( ph -> ( A x. C ) e. RR )
28 26 27 remulcld
 |-  ( ph -> ( 4 x. ( A x. C ) ) e. RR )
29 24 28 resubcld
 |-  ( ph -> ( ( B ^ 2 ) - ( 4 x. ( A x. C ) ) ) e. RR )
30 5 29 eqeltrd
 |-  ( ph -> D e. RR )
31 30 recnd
 |-  ( ph -> D e. CC )
32 31 sqrtcld
 |-  ( ph -> ( sqrt ` D ) e. CC )
33 23 32 addcld
 |-  ( ph -> ( -u B + ( sqrt ` D ) ) e. CC )
34 33 adantr
 |-  ( ( ph /\ -. 0 <_ D ) -> ( -u B + ( sqrt ` D ) ) e. CC )
35 3 renegcld
 |-  ( ph -> -u B e. RR )
36 35 adantr
 |-  ( ( ph /\ -. 0 <_ D ) -> -u B e. RR )
37 32 adantr
 |-  ( ( ph /\ -. 0 <_ D ) -> ( sqrt ` D ) e. CC )
38 31 negnegd
 |-  ( ph -> -u -u D = D )
39 38 adantr
 |-  ( ( ph /\ -. 0 <_ D ) -> -u -u D = D )
40 39 eqcomd
 |-  ( ( ph /\ -. 0 <_ D ) -> D = -u -u D )
41 40 fveq2d
 |-  ( ( ph /\ -. 0 <_ D ) -> ( sqrt ` D ) = ( sqrt ` -u -u D ) )
42 30 renegcld
 |-  ( ph -> -u D e. RR )
43 42 adantr
 |-  ( ( ph /\ -. 0 <_ D ) -> -u D e. RR )
44 0red
 |-  ( ph -> 0 e. RR )
45 30 44 ltnled
 |-  ( ph -> ( D < 0 <-> -. 0 <_ D ) )
46 ltle
 |-  ( ( D e. RR /\ 0 e. RR ) -> ( D < 0 -> D <_ 0 ) )
47 30 44 46 syl2anc
 |-  ( ph -> ( D < 0 -> D <_ 0 ) )
48 45 47 sylbird
 |-  ( ph -> ( -. 0 <_ D -> D <_ 0 ) )
49 48 imp
 |-  ( ( ph /\ -. 0 <_ D ) -> D <_ 0 )
50 30 le0neg1d
 |-  ( ph -> ( D <_ 0 <-> 0 <_ -u D ) )
51 50 adantr
 |-  ( ( ph /\ -. 0 <_ D ) -> ( D <_ 0 <-> 0 <_ -u D ) )
52 49 51 mpbid
 |-  ( ( ph /\ -. 0 <_ D ) -> 0 <_ -u D )
53 43 52 sqrtnegd
 |-  ( ( ph /\ -. 0 <_ D ) -> ( sqrt ` -u -u D ) = ( _i x. ( sqrt ` -u D ) ) )
54 41 53 eqtrd
 |-  ( ( ph /\ -. 0 <_ D ) -> ( sqrt ` D ) = ( _i x. ( sqrt ` -u D ) ) )
55 ax-icn
 |-  _i e. CC
56 55 a1i
 |-  ( ( ph /\ -. 0 <_ D ) -> _i e. CC )
57 31 negcld
 |-  ( ph -> -u D e. CC )
58 57 sqrtcld
 |-  ( ph -> ( sqrt ` -u D ) e. CC )
59 58 adantr
 |-  ( ( ph /\ -. 0 <_ D ) -> ( sqrt ` -u D ) e. CC )
60 56 59 mulcomd
 |-  ( ( ph /\ -. 0 <_ D ) -> ( _i x. ( sqrt ` -u D ) ) = ( ( sqrt ` -u D ) x. _i ) )
61 43 52 resqrtcld
 |-  ( ( ph /\ -. 0 <_ D ) -> ( sqrt ` -u D ) e. RR )
62 inelr
 |-  -. _i e. RR
63 eldif
 |-  ( _i e. ( CC \ RR ) <-> ( _i e. CC /\ -. _i e. RR ) )
64 55 62 63 mpbir2an
 |-  _i e. ( CC \ RR )
65 64 a1i
 |-  ( ( ph /\ -. 0 <_ D ) -> _i e. ( CC \ RR ) )
66 30 lt0neg1d
 |-  ( ph -> ( D < 0 <-> 0 < -u D ) )
67 ltne
 |-  ( ( 0 e. RR /\ 0 < -u D ) -> -u D =/= 0 )
68 44 67 sylan
 |-  ( ( ph /\ 0 < -u D ) -> -u D =/= 0 )
69 42 adantr
 |-  ( ( ph /\ 0 < -u D ) -> -u D e. RR )
70 ltle
 |-  ( ( 0 e. RR /\ -u D e. RR ) -> ( 0 < -u D -> 0 <_ -u D ) )
71 44 42 70 syl2anc
 |-  ( ph -> ( 0 < -u D -> 0 <_ -u D ) )
72 71 imp
 |-  ( ( ph /\ 0 < -u D ) -> 0 <_ -u D )
73 sqrt00
 |-  ( ( -u D e. RR /\ 0 <_ -u D ) -> ( ( sqrt ` -u D ) = 0 <-> -u D = 0 ) )
74 69 72 73 syl2anc
 |-  ( ( ph /\ 0 < -u D ) -> ( ( sqrt ` -u D ) = 0 <-> -u D = 0 ) )
75 74 bicomd
 |-  ( ( ph /\ 0 < -u D ) -> ( -u D = 0 <-> ( sqrt ` -u D ) = 0 ) )
76 75 necon3bid
 |-  ( ( ph /\ 0 < -u D ) -> ( -u D =/= 0 <-> ( sqrt ` -u D ) =/= 0 ) )
77 68 76 mpbid
 |-  ( ( ph /\ 0 < -u D ) -> ( sqrt ` -u D ) =/= 0 )
78 77 ex
 |-  ( ph -> ( 0 < -u D -> ( sqrt ` -u D ) =/= 0 ) )
79 66 78 sylbid
 |-  ( ph -> ( D < 0 -> ( sqrt ` -u D ) =/= 0 ) )
80 45 79 sylbird
 |-  ( ph -> ( -. 0 <_ D -> ( sqrt ` -u D ) =/= 0 ) )
81 80 imp
 |-  ( ( ph /\ -. 0 <_ D ) -> ( sqrt ` -u D ) =/= 0 )
82 61 65 81 recnmulnred
 |-  ( ( ph /\ -. 0 <_ D ) -> ( ( sqrt ` -u D ) x. _i ) e/ RR )
83 df-nel
 |-  ( ( ( sqrt ` -u D ) x. _i ) e/ RR <-> -. ( ( sqrt ` -u D ) x. _i ) e. RR )
84 82 83 sylib
 |-  ( ( ph /\ -. 0 <_ D ) -> -. ( ( sqrt ` -u D ) x. _i ) e. RR )
85 60 84 eqneltrd
 |-  ( ( ph /\ -. 0 <_ D ) -> -. ( _i x. ( sqrt ` -u D ) ) e. RR )
86 54 85 eqneltrd
 |-  ( ( ph /\ -. 0 <_ D ) -> -. ( sqrt ` D ) e. RR )
87 37 86 eldifd
 |-  ( ( ph /\ -. 0 <_ D ) -> ( sqrt ` D ) e. ( CC \ RR ) )
88 36 87 readdcnnred
 |-  ( ( ph /\ -. 0 <_ D ) -> ( -u B + ( sqrt ` D ) ) e/ RR )
89 df-nel
 |-  ( ( -u B + ( sqrt ` D ) ) e/ RR <-> -. ( -u B + ( sqrt ` D ) ) e. RR )
90 88 89 sylib
 |-  ( ( ph /\ -. 0 <_ D ) -> -. ( -u B + ( sqrt ` D ) ) e. RR )
91 34 90 eldifd
 |-  ( ( ph /\ -. 0 <_ D ) -> ( -u B + ( sqrt ` D ) ) e. ( CC \ RR ) )
92 2cnd
 |-  ( ph -> 2 e. CC )
93 2ne0
 |-  2 =/= 0
94 93 a1i
 |-  ( ph -> 2 =/= 0 )
95 92 6 94 2 mulne0d
 |-  ( ph -> ( 2 x. A ) =/= 0 )
96 95 adantr
 |-  ( ( ph /\ -. 0 <_ D ) -> ( 2 x. A ) =/= 0 )
97 22 91 96 cndivrenred
 |-  ( ( ph /\ -. 0 <_ D ) -> ( ( -u B + ( sqrt ` D ) ) / ( 2 x. A ) ) e/ RR )
98 df-nel
 |-  ( ( ( -u B + ( sqrt ` D ) ) / ( 2 x. A ) ) e/ RR <-> -. ( ( -u B + ( sqrt ` D ) ) / ( 2 x. A ) ) e. RR )
99 97 98 sylib
 |-  ( ( ph /\ -. 0 <_ D ) -> -. ( ( -u B + ( sqrt ` D ) ) / ( 2 x. A ) ) e. RR )
100 99 ex
 |-  ( ph -> ( -. 0 <_ D -> -. ( ( -u B + ( sqrt ` D ) ) / ( 2 x. A ) ) e. RR ) )
101 100 con4d
 |-  ( ph -> ( ( ( -u B + ( sqrt ` D ) ) / ( 2 x. A ) ) e. RR -> 0 <_ D ) )
102 101 adantr
 |-  ( ( ph /\ x = ( ( -u B + ( sqrt ` D ) ) / ( 2 x. A ) ) ) -> ( ( ( -u B + ( sqrt ` D ) ) / ( 2 x. A ) ) e. RR -> 0 <_ D ) )
103 18 102 sylbid
 |-  ( ( ph /\ x = ( ( -u B + ( sqrt ` D ) ) / ( 2 x. A ) ) ) -> ( x e. RR -> 0 <_ D ) )
104 103 ex
 |-  ( ph -> ( x = ( ( -u B + ( sqrt ` D ) ) / ( 2 x. A ) ) -> ( x e. RR -> 0 <_ D ) ) )
105 eleq1
 |-  ( x = ( ( -u B - ( sqrt ` D ) ) / ( 2 x. A ) ) -> ( x e. RR <-> ( ( -u B - ( sqrt ` D ) ) / ( 2 x. A ) ) e. RR ) )
106 105 adantl
 |-  ( ( ph /\ x = ( ( -u B - ( sqrt ` D ) ) / ( 2 x. A ) ) ) -> ( x e. RR <-> ( ( -u B - ( sqrt ` D ) ) / ( 2 x. A ) ) e. RR ) )
107 23 32 subcld
 |-  ( ph -> ( -u B - ( sqrt ` D ) ) e. CC )
108 107 adantr
 |-  ( ( ph /\ -. 0 <_ D ) -> ( -u B - ( sqrt ` D ) ) e. CC )
109 36 87 resubcnnred
 |-  ( ( ph /\ -. 0 <_ D ) -> ( -u B - ( sqrt ` D ) ) e/ RR )
110 df-nel
 |-  ( ( -u B - ( sqrt ` D ) ) e/ RR <-> -. ( -u B - ( sqrt ` D ) ) e. RR )
111 109 110 sylib
 |-  ( ( ph /\ -. 0 <_ D ) -> -. ( -u B - ( sqrt ` D ) ) e. RR )
112 108 111 eldifd
 |-  ( ( ph /\ -. 0 <_ D ) -> ( -u B - ( sqrt ` D ) ) e. ( CC \ RR ) )
113 22 112 96 cndivrenred
 |-  ( ( ph /\ -. 0 <_ D ) -> ( ( -u B - ( sqrt ` D ) ) / ( 2 x. A ) ) e/ RR )
114 df-nel
 |-  ( ( ( -u B - ( sqrt ` D ) ) / ( 2 x. A ) ) e/ RR <-> -. ( ( -u B - ( sqrt ` D ) ) / ( 2 x. A ) ) e. RR )
115 113 114 sylib
 |-  ( ( ph /\ -. 0 <_ D ) -> -. ( ( -u B - ( sqrt ` D ) ) / ( 2 x. A ) ) e. RR )
116 115 ex
 |-  ( ph -> ( -. 0 <_ D -> -. ( ( -u B - ( sqrt ` D ) ) / ( 2 x. A ) ) e. RR ) )
117 116 con4d
 |-  ( ph -> ( ( ( -u B - ( sqrt ` D ) ) / ( 2 x. A ) ) e. RR -> 0 <_ D ) )
118 117 adantr
 |-  ( ( ph /\ x = ( ( -u B - ( sqrt ` D ) ) / ( 2 x. A ) ) ) -> ( ( ( -u B - ( sqrt ` D ) ) / ( 2 x. A ) ) e. RR -> 0 <_ D ) )
119 106 118 sylbid
 |-  ( ( ph /\ x = ( ( -u B - ( sqrt ` D ) ) / ( 2 x. A ) ) ) -> ( x e. RR -> 0 <_ D ) )
120 119 ex
 |-  ( ph -> ( x = ( ( -u B - ( sqrt ` D ) ) / ( 2 x. A ) ) -> ( x e. RR -> 0 <_ D ) ) )
121 104 120 jaod
 |-  ( ph -> ( ( x = ( ( -u B + ( sqrt ` D ) ) / ( 2 x. A ) ) \/ x = ( ( -u B - ( sqrt ` D ) ) / ( 2 x. A ) ) ) -> ( x e. RR -> 0 <_ D ) ) )
122 121 com23
 |-  ( ph -> ( x e. RR -> ( ( x = ( ( -u B + ( sqrt ` D ) ) / ( 2 x. A ) ) \/ x = ( ( -u B - ( sqrt ` D ) ) / ( 2 x. A ) ) ) -> 0 <_ D ) ) )
123 122 imp
 |-  ( ( ph /\ x e. RR ) -> ( ( x = ( ( -u B + ( sqrt ` D ) ) / ( 2 x. A ) ) \/ x = ( ( -u B - ( sqrt ` D ) ) / ( 2 x. A ) ) ) -> 0 <_ D ) )
124 16 123 sylbid
 |-  ( ( ph /\ x e. RR ) -> ( ( ( A x. ( x ^ 2 ) ) + ( ( B x. x ) + C ) ) = 0 -> 0 <_ D ) )
125 124 rexlimdva
 |-  ( ph -> ( E. x e. RR ( ( A x. ( x ^ 2 ) ) + ( ( B x. x ) + C ) ) = 0 -> 0 <_ D ) )
126 35 adantr
 |-  ( ( ph /\ 0 <_ D ) -> -u B e. RR )
127 30 adantr
 |-  ( ( ph /\ 0 <_ D ) -> D e. RR )
128 simpr
 |-  ( ( ph /\ 0 <_ D ) -> 0 <_ D )
129 127 128 resqrtcld
 |-  ( ( ph /\ 0 <_ D ) -> ( sqrt ` D ) e. RR )
130 126 129 readdcld
 |-  ( ( ph /\ 0 <_ D ) -> ( -u B + ( sqrt ` D ) ) e. RR )
131 19 a1i
 |-  ( ( ph /\ 0 <_ D ) -> 2 e. RR )
132 1 adantr
 |-  ( ( ph /\ 0 <_ D ) -> A e. RR )
133 131 132 remulcld
 |-  ( ( ph /\ 0 <_ D ) -> ( 2 x. A ) e. RR )
134 95 adantr
 |-  ( ( ph /\ 0 <_ D ) -> ( 2 x. A ) =/= 0 )
135 130 133 134 redivcld
 |-  ( ( ph /\ 0 <_ D ) -> ( ( -u B + ( sqrt ` D ) ) / ( 2 x. A ) ) e. RR )
136 oveq1
 |-  ( x = ( ( -u B + ( sqrt ` D ) ) / ( 2 x. A ) ) -> ( x ^ 2 ) = ( ( ( -u B + ( sqrt ` D ) ) / ( 2 x. A ) ) ^ 2 ) )
137 136 oveq2d
 |-  ( x = ( ( -u B + ( sqrt ` D ) ) / ( 2 x. A ) ) -> ( A x. ( x ^ 2 ) ) = ( A x. ( ( ( -u B + ( sqrt ` D ) ) / ( 2 x. A ) ) ^ 2 ) ) )
138 oveq2
 |-  ( x = ( ( -u B + ( sqrt ` D ) ) / ( 2 x. A ) ) -> ( B x. x ) = ( B x. ( ( -u B + ( sqrt ` D ) ) / ( 2 x. A ) ) ) )
139 138 oveq1d
 |-  ( x = ( ( -u B + ( sqrt ` D ) ) / ( 2 x. A ) ) -> ( ( B x. x ) + C ) = ( ( B x. ( ( -u B + ( sqrt ` D ) ) / ( 2 x. A ) ) ) + C ) )
140 137 139 oveq12d
 |-  ( x = ( ( -u B + ( sqrt ` D ) ) / ( 2 x. A ) ) -> ( ( A x. ( x ^ 2 ) ) + ( ( B x. x ) + C ) ) = ( ( A x. ( ( ( -u B + ( sqrt ` D ) ) / ( 2 x. A ) ) ^ 2 ) ) + ( ( B x. ( ( -u B + ( sqrt ` D ) ) / ( 2 x. A ) ) ) + C ) ) )
141 140 eqeq1d
 |-  ( x = ( ( -u B + ( sqrt ` D ) ) / ( 2 x. A ) ) -> ( ( ( A x. ( x ^ 2 ) ) + ( ( B x. x ) + C ) ) = 0 <-> ( ( A x. ( ( ( -u B + ( sqrt ` D ) ) / ( 2 x. A ) ) ^ 2 ) ) + ( ( B x. ( ( -u B + ( sqrt ` D ) ) / ( 2 x. A ) ) ) + C ) ) = 0 ) )
142 141 adantl
 |-  ( ( ( ph /\ 0 <_ D ) /\ x = ( ( -u B + ( sqrt ` D ) ) / ( 2 x. A ) ) ) -> ( ( ( A x. ( x ^ 2 ) ) + ( ( B x. x ) + C ) ) = 0 <-> ( ( A x. ( ( ( -u B + ( sqrt ` D ) ) / ( 2 x. A ) ) ^ 2 ) ) + ( ( B x. ( ( -u B + ( sqrt ` D ) ) / ( 2 x. A ) ) ) + C ) ) = 0 ) )
143 eqidd
 |-  ( ( ph /\ 0 <_ D ) -> ( ( -u B + ( sqrt ` D ) ) / ( 2 x. A ) ) = ( ( -u B + ( sqrt ` D ) ) / ( 2 x. A ) ) )
144 143 orcd
 |-  ( ( ph /\ 0 <_ D ) -> ( ( ( -u B + ( sqrt ` D ) ) / ( 2 x. A ) ) = ( ( -u B + ( sqrt ` D ) ) / ( 2 x. A ) ) \/ ( ( -u B + ( sqrt ` D ) ) / ( 2 x. A ) ) = ( ( -u B - ( sqrt ` D ) ) / ( 2 x. A ) ) ) )
145 6 adantr
 |-  ( ( ph /\ 0 <_ D ) -> A e. CC )
146 2 adantr
 |-  ( ( ph /\ 0 <_ D ) -> A =/= 0 )
147 9 adantr
 |-  ( ( ph /\ 0 <_ D ) -> B e. CC )
148 11 adantr
 |-  ( ( ph /\ 0 <_ D ) -> C e. CC )
149 92 6 mulcld
 |-  ( ph -> ( 2 x. A ) e. CC )
150 33 149 95 divcld
 |-  ( ph -> ( ( -u B + ( sqrt ` D ) ) / ( 2 x. A ) ) e. CC )
151 150 adantr
 |-  ( ( ph /\ 0 <_ D ) -> ( ( -u B + ( sqrt ` D ) ) / ( 2 x. A ) ) e. CC )
152 5 adantr
 |-  ( ( ph /\ 0 <_ D ) -> D = ( ( B ^ 2 ) - ( 4 x. ( A x. C ) ) ) )
153 145 146 147 148 151 152 quad
 |-  ( ( ph /\ 0 <_ D ) -> ( ( ( A x. ( ( ( -u B + ( sqrt ` D ) ) / ( 2 x. A ) ) ^ 2 ) ) + ( ( B x. ( ( -u B + ( sqrt ` D ) ) / ( 2 x. A ) ) ) + C ) ) = 0 <-> ( ( ( -u B + ( sqrt ` D ) ) / ( 2 x. A ) ) = ( ( -u B + ( sqrt ` D ) ) / ( 2 x. A ) ) \/ ( ( -u B + ( sqrt ` D ) ) / ( 2 x. A ) ) = ( ( -u B - ( sqrt ` D ) ) / ( 2 x. A ) ) ) ) )
154 144 153 mpbird
 |-  ( ( ph /\ 0 <_ D ) -> ( ( A x. ( ( ( -u B + ( sqrt ` D ) ) / ( 2 x. A ) ) ^ 2 ) ) + ( ( B x. ( ( -u B + ( sqrt ` D ) ) / ( 2 x. A ) ) ) + C ) ) = 0 )
155 135 142 154 rspcedvd
 |-  ( ( ph /\ 0 <_ D ) -> E. x e. RR ( ( A x. ( x ^ 2 ) ) + ( ( B x. x ) + C ) ) = 0 )
156 155 ex
 |-  ( ph -> ( 0 <_ D -> E. x e. RR ( ( A x. ( x ^ 2 ) ) + ( ( B x. x ) + C ) ) = 0 ) )
157 125 156 impbid
 |-  ( ph -> ( E. x e. RR ( ( A x. ( x ^ 2 ) ) + ( ( B x. x ) + C ) ) = 0 <-> 0 <_ D ) )