let a, b, c be Real; ( not c / a < 0 or ( ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) > 0 & ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) < 0 ) or ( ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) < 0 & ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) > 0 ) )
assume A1:
c / a < 0
; ( ( ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) > 0 & ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) < 0 ) or ( ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) < 0 & ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) > 0 ) )
now ( ( c > 0 & a < 0 & ( ( ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) > 0 & ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) < 0 ) or ( ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) < 0 & ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) > 0 ) ) ) or ( c < 0 & a > 0 & ( ( ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) > 0 & ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) < 0 ) or ( ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) < 0 & ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) > 0 ) ) ) )per cases
( ( c > 0 & a < 0 ) or ( c < 0 & a > 0 ) )
by A1, XREAL_1:143;
case A2:
(
c > 0 &
a < 0 )
;
( ( ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) > 0 & ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) < 0 ) or ( ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) < 0 & ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) > 0 ) )then
4
* a < 4
* 0
by XREAL_1:68;
then
(4 * a) * c < 0 * c
by A2, XREAL_1:68;
then A3:
- ((4 * a) * c) > 0
by XREAL_1:58;
then
(b ^2) + (- ((4 * a) * c)) > (b ^2) + 0
by XREAL_1:8;
then A4:
sqrt ((b ^2) - ((4 * a) * c)) > sqrt (b ^2)
by SQUARE_1:27, XREAL_1:63;
A5:
2
* a < 2
* 0
by A2, XREAL_1:68;
(- ((4 * a) * c)) + (b ^2) > 0 + 0
by A3, XREAL_1:8, XREAL_1:63;
then A6:
- (- (sqrt ((b ^2) - ((4 * a) * c)))) > 0
by SQUARE_1:17, SQUARE_1:27;
then A7:
- (sqrt ((b ^2) - ((4 * a) * c))) < 0
;
now ( ( ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) > 0 & ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) < 0 ) or ( ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) < 0 & ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) > 0 ) )per cases
( b >= 0 or b < 0 )
;
suppose A8:
b >= 0
;
( ( ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) > 0 & ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) < 0 ) or ( ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) < 0 & ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) > 0 ) )then
- b <= - 0
;
then
(- (sqrt ((b ^2) - ((4 * a) * c)))) + (- b) < 0 + 0
by A7;
then
(- b) - (sqrt ((b ^2) - ((4 * a) * c))) < 0
;
then A9:
(- b) - (sqrt (delta (a,b,c))) < 0
by QUIN_1:def 1;
sqrt ((b ^2) - ((4 * a) * c)) > b
by A4, A8, SQUARE_1:22;
then
(- b) + (sqrt ((b ^2) - ((4 * a) * c))) > (0 + b) + (- b)
by XREAL_1:8;
then
((- b) + (sqrt ((b ^2) - ((4 * a) * c)))) / (2 * a) < 0
by A5, XREAL_1:142;
hence
( (
((- b) + (sqrt (delta (a,b,c)))) / (2 * a) > 0 &
((- b) - (sqrt (delta (a,b,c)))) / (2 * a) < 0 ) or (
((- b) + (sqrt (delta (a,b,c)))) / (2 * a) < 0 &
((- b) - (sqrt (delta (a,b,c)))) / (2 * a) > 0 ) )
by A5, A9, QUIN_1:def 1, XREAL_1:140;
verum end; suppose A10:
b < 0
;
( ( ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) > 0 & ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) < 0 ) or ( ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) < 0 & ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) > 0 ) )then
sqrt ((b ^2) - ((4 * a) * c)) > - b
by A4, SQUARE_1:23;
then
- (- (b + (sqrt ((b ^2) - ((4 * a) * c))))) > 0
by XREAL_1:62;
then
(- b) - (sqrt ((b ^2) - ((4 * a) * c))) < 0
;
then A11:
((- b) - (sqrt ((b ^2) - ((4 * a) * c)))) / (2 * a) > 0
by A5, XREAL_1:140;
- b > 0
by A10, XREAL_1:58;
then
(sqrt ((b ^2) - ((4 * a) * c))) + (- b) > 0 + 0
by A6;
then
(sqrt (delta (a,b,c))) + (- b) > 0 + 0
by QUIN_1:def 1;
hence
( (
((- b) + (sqrt (delta (a,b,c)))) / (2 * a) > 0 &
((- b) - (sqrt (delta (a,b,c)))) / (2 * a) < 0 ) or (
((- b) + (sqrt (delta (a,b,c)))) / (2 * a) < 0 &
((- b) - (sqrt (delta (a,b,c)))) / (2 * a) > 0 ) )
by A5, A11, QUIN_1:def 1, XREAL_1:142;
verum end; end; end; hence
( (
((- b) + (sqrt (delta (a,b,c)))) / (2 * a) > 0 &
((- b) - (sqrt (delta (a,b,c)))) / (2 * a) < 0 ) or (
((- b) + (sqrt (delta (a,b,c)))) / (2 * a) < 0 &
((- b) - (sqrt (delta (a,b,c)))) / (2 * a) > 0 ) )
;
verum end; case A12:
(
c < 0 &
a > 0 )
;
( ( ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) > 0 & ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) < 0 ) or ( ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) < 0 & ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) > 0 ) )then
4
* a > 0
by XREAL_1:129;
then
(4 * a) * c < (4 * a) * 0
by A12, XREAL_1:68;
then A13:
- ((4 * a) * c) > 0
by XREAL_1:58;
then
(b ^2) + (- ((4 * a) * c)) > (b ^2) + 0
by XREAL_1:8;
then A14:
sqrt ((b ^2) - ((4 * a) * c)) > sqrt (b ^2)
by SQUARE_1:27, XREAL_1:63;
A15:
2
* a > 0
by A12, XREAL_1:129;
(- ((4 * a) * c)) + (b ^2) > 0 + 0
by A13, XREAL_1:8, XREAL_1:63;
then A16:
- (- (sqrt ((b ^2) - ((4 * a) * c)))) > 0
by SQUARE_1:17, SQUARE_1:27;
then A17:
- (sqrt ((b ^2) - ((4 * a) * c))) < 0
;
now ( ( ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) > 0 & ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) < 0 ) or ( ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) < 0 & ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) > 0 ) )per cases
( b >= 0 or b < 0 )
;
suppose A18:
b >= 0
;
( ( ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) > 0 & ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) < 0 ) or ( ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) < 0 & ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) > 0 ) )then
- b <= - 0
;
then
(- (sqrt ((b ^2) - ((4 * a) * c)))) + (- b) < 0 + 0
by A17;
then
(- b) - (sqrt ((b ^2) - ((4 * a) * c))) < 0
;
then A19:
(- b) - (sqrt (delta (a,b,c))) < 0
by QUIN_1:def 1;
sqrt ((b ^2) - ((4 * a) * c)) > b
by A14, A18, SQUARE_1:22;
then
(- b) + (sqrt ((b ^2) - ((4 * a) * c))) > (0 + b) + (- b)
by XREAL_1:8;
then
((- b) + (sqrt ((b ^2) - ((4 * a) * c)))) / (2 * a) > 0
by A15, XREAL_1:139;
hence
( (
((- b) + (sqrt (delta (a,b,c)))) / (2 * a) > 0 &
((- b) - (sqrt (delta (a,b,c)))) / (2 * a) < 0 ) or (
((- b) + (sqrt (delta (a,b,c)))) / (2 * a) < 0 &
((- b) - (sqrt (delta (a,b,c)))) / (2 * a) > 0 ) )
by A12, A19, QUIN_1:def 1, XREAL_1:129, XREAL_1:141;
verum end; suppose A20:
b < 0
;
( ( ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) > 0 & ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) < 0 ) or ( ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) < 0 & ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) > 0 ) )then
sqrt ((b ^2) - ((4 * a) * c)) > - b
by A14, SQUARE_1:23;
then
- (- (b + (sqrt ((b ^2) - ((4 * a) * c))))) > 0
by XREAL_1:62;
then
(- b) - (sqrt ((b ^2) - ((4 * a) * c))) < 0
;
then A21:
((- b) - (sqrt ((b ^2) - ((4 * a) * c)))) / (2 * a) < 0
by A12, XREAL_1:129, XREAL_1:141;
- b > 0
by A20, XREAL_1:58;
then
(sqrt ((b ^2) - ((4 * a) * c))) + (- b) > 0 + 0
by A16;
then
(sqrt (delta (a,b,c))) + (- b) > 0
by QUIN_1:def 1;
hence
( (
((- b) + (sqrt (delta (a,b,c)))) / (2 * a) > 0 &
((- b) - (sqrt (delta (a,b,c)))) / (2 * a) < 0 ) or (
((- b) + (sqrt (delta (a,b,c)))) / (2 * a) < 0 &
((- b) - (sqrt (delta (a,b,c)))) / (2 * a) > 0 ) )
by A15, A21, QUIN_1:def 1, XREAL_1:139;
verum end; end; end; hence
( (
((- b) + (sqrt (delta (a,b,c)))) / (2 * a) > 0 &
((- b) - (sqrt (delta (a,b,c)))) / (2 * a) < 0 ) or (
((- b) + (sqrt (delta (a,b,c)))) / (2 * a) < 0 &
((- b) - (sqrt (delta (a,b,c)))) / (2 * a) > 0 ) )
;
verum end; end; end;
hence
( ( ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) > 0 & ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) < 0 ) or ( ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) < 0 & ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) > 0 ) )
; verum