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