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