let p, q, y be Real; :: thesis: ( Polynom (1,0,p,q,y) = 0 implies for u, v being Real st y = u + v & ((3 * v) * u) + p = 0 & not y = (3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) + (3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) & not y = (3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) + (3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) holds
y = (3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) + (3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) )
set e1 = 1;
assume A1: Polynom (1,0,p,q,y) = 0 ; :: thesis: for u, v being Real st y = u + v & ((3 * v) * u) + p = 0 & not y = (3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) + (3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) & not y = (3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) + (3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) holds
y = (3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) + (3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3)))))
set e3 = (- (p / 3)) |^ 3;
set e2 = q;
let u, v be Real; :: thesis: ( y = u + v & ((3 * v) * u) + p = 0 & not y = (3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) + (3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) & not y = (3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) + (3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) implies y = (3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) + (3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) )
assume that
A2: y = u + v and
A3: ((3 * v) * u) + p = 0 ; :: thesis: ( y = (3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) + (3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) or y = (3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) + (3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) or y = (3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) + (3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) )
set z2 = v |^ 3;
set z1 = u |^ 3;
A4: now :: thesis: for z being Real holds (z - (u |^ 3)) * (z - (v |^ 3)) = ((z ^2) + (q * z)) + ((- (p / 3)) |^ 3)
let z be Real; :: thesis: (z - (u |^ 3)) * (z - (v |^ 3)) = ((z ^2) + (q * z)) + ((- (p / 3)) |^ 3)
thus (z - (u |^ 3)) * (z - (v |^ 3)) = ((z ^2) - (((u |^ 3) + (v |^ 3)) * z)) + ((u |^ 3) * (v |^ 3))
.= ((z ^2) - ((- q) * z)) + ((u |^ 3) * (v |^ 3)) by A1, A2, A3, Th18
.= ((z ^2) + (q * z)) + ((- (p / 3)) |^ 3) by A1, A2, A3, Th18 ; :: thesis: verum
end;
A5: (u |^ 3) + (v |^ 3) = - q by A1, A2, A3, Th18;
then q ^2 = ((u |^ 3) + (v |^ 3)) ^2 by SQUARE_1:3;
then A6: (q ^2) - ((4 * 1) * ((- (p / 3)) |^ 3)) = (- (- ((((u |^ 3) ^2) + ((2 * (u |^ 3)) * (v |^ 3))) + ((v |^ 3) ^2)))) - (4 * ((u |^ 3) * (v |^ 3))) by A1, A2, A3, Th18
.= ((u |^ 3) - (v |^ 3)) ^2 ;
then A7: (q ^2) - ((4 * 1) * ((- (p / 3)) |^ 3)) >= 0 by XREAL_1:63;
then A8: delta (1,q,((- (p / 3)) |^ 3)) >= 0 by QUIN_1:def 1;
((u |^ 3) - (u |^ 3)) * ((u |^ 3) - (v |^ 3)) = 0 * ((u |^ 3) - (v |^ 3)) ;
then A9: Polynom (1,q,((- (p / 3)) |^ 3),(u |^ 3)) = 0 by A4;
((v |^ 3) - (u |^ 3)) * ((v |^ 3) - (v |^ 3)) = ((v |^ 3) - (u |^ 3)) * 0 ;
then A10: Polynom (1,q,((- (p / 3)) |^ 3),(v |^ 3)) = 0 by A4;
A11: (v |^ 3) * (u |^ 3) = (- (p / 3)) |^ 3 by A1, A2, A3, Th18;
now :: thesis: ( ( u |^ 3 = ((- q) + (sqrt (delta (1,q,((- (p / 3)) |^ 3))))) / (2 * 1) & ( y = (3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) + (3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) or y = (3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) + (3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) or y = (3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) + (3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) ) ) or ( u |^ 3 = ((- q) - (sqrt (delta (1,q,((- (p / 3)) |^ 3))))) / (2 * 1) & u |^ 3 = (- (q / 2)) - (sqrt (((q ^2) / 4) - ((- (p / 3)) |^ 3))) & ( y = (3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) + (3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) or y = (3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) + (3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) or y = (3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) + (3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) ) ) )
per cases ( u |^ 3 = ((- q) + (sqrt (delta (1,q,((- (p / 3)) |^ 3))))) / (2 * 1) or u |^ 3 = ((- q) - (sqrt (delta (1,q,((- (p / 3)) |^ 3))))) / (2 * 1) ) by A9, A8, Th5;
case A12: u |^ 3 = ((- q) + (sqrt (delta (1,q,((- (p / 3)) |^ 3))))) / (2 * 1) ; :: thesis: ( y = (3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) + (3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) or y = (3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) + (3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) or y = (3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) + (3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) )
A13: (p / 3) |^ 3 = (p / 3) |^ (2 + 1)
.= ((p / 3) |^ (1 + 1)) * (p / 3) by NEWTON:6
.= (((p / 3) |^ 1) * (p / 3)) * (p / 3) by NEWTON:6
.= ((p / 3) |^ 1) * ((p / 3) ^2)
.= ((p / 3) to_power 1) * ((p / 3) ^2) by POWER:41
.= (p / 3) * ((p / 3) ^2) by POWER:25 ;
A14: (q ^2) - (4 * ((- (p / 3)) |^ 3)) >= 0 by A6, XREAL_1:63;
A15: (- (p / 3)) |^ 3 = (- (p / 3)) |^ (2 + 1)
.= ((- (p / 3)) |^ (1 + 1)) * (- (p / 3)) by NEWTON:6
.= (((- (p / 3)) |^ 1) * (- (p / 3))) * (- (p / 3)) by NEWTON:6
.= ((- (p / 3)) |^ 1) * ((- (p / 3)) ^2) ;
then A16: (- (p / 3)) |^ 3 = ((- (p / 3)) to_power 1) * ((- (p / 3)) ^2) by POWER:41
.= (- (p / 3)) * ((p / 3) ^2) by POWER:25
.= - ((p / 3) * ((p / 3) ^2)) ;
A17: u |^ 3 = ((- q) + (sqrt ((q ^2) - ((4 * 1) * ((- (p / 3)) |^ 3))))) / (2 * 1) by A12, QUIN_1:def 1
.= ((- q) / 2) + ((sqrt ((q ^2) - (4 * ((- (p / 3)) |^ 3)))) / (sqrt 4)) by SQUARE_1:20, XCMPLX_1:62
.= ((- q) / 2) + (sqrt (((q ^2) - (4 * ((- (p / 3)) |^ 3))) / 4)) by A14, SQUARE_1:30
.= ((- q) / 2) + (sqrt (((q ^2) / 4) - (1 * ((- (p / 3)) |^ 3)))) ;
A18: now :: thesis: ( ( u > 0 & u = 3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3)))) ) or ( u = 0 & u = 3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3)))) ) or ( u < 0 & u = 3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3)))) ) )
per cases ( u > 0 or u = 0 or u < 0 ) by XXREAL_0:1;
case A19: u > 0 ; :: thesis: u = 3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))
then A20: (- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))) > 0 by A17, A16, A13, PREPOWER:6;
then u = 3 -Root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3)))) by A17, A16, A13, A19, PREPOWER:def 2;
hence u = 3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3)))) by A20, POWER:def 1; :: thesis: verum
end;
case A21: u = 0 ; :: thesis: u = 3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))
then A22: (- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))) = 0 by A17, A16, A13, NEWTON:11;
then 3 -Root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3)))) = 0 by PREPOWER:def 2;
hence u = 3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3)))) by A21, A22, POWER:def 1; :: thesis: verum
end;
case u < 0 ; :: thesis: u = 3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))
then A23: - u > 0 by XREAL_1:58;
set r = (- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3)));
A24: 3 -root (- 1) = - 1 by Lm1, POWER:8;
(- u) |^ 3 = (- u) |^ (2 + 1)
.= ((- u) |^ (1 + 1)) * (- u) by NEWTON:6
.= (((- u) |^ 1) * (- u)) * (- u) by NEWTON:6
.= ((- u) |^ 1) * ((- u) ^2) ;
then (- u) |^ 3 = ((- u) to_power 1) * ((- u) ^2) by POWER:41;
then A25: (- u) |^ 3 = (- u) * (u ^2) by POWER:25
.= - (u * (u ^2)) ;
u |^ 3 = u |^ (2 + 1)
.= (u |^ (1 + 1)) * u by NEWTON:6
.= ((u |^ 1) * u) * u by NEWTON:6
.= (u |^ 1) * (u * u) ;
then A26: u |^ 3 = (u to_power 1) * (u ^2) by POWER:41;
then A27: (- u) |^ 3 = - ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3)))) by A17, A16, A13, A25, POWER:25;
A28: (- u) |^ 3 = - (u |^ 3) by A25, A26, POWER:25;
then A29: - ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3)))) > 0 by A17, A16, A13, A23, PREPOWER:6;
- (u |^ 3) > 0 by A23, A28, PREPOWER:6;
then - u = 3 -Root (- ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) by A17, A16, A13, A23, A27, PREPOWER:def 2;
then - u = 3 -root ((- 1) * ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) by A29, POWER:def 1;
then - u = (3 -root (- 1)) * (3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) by Lm1, POWER:11;
hence u = 3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3)))) by A24; :: thesis: verum
end;
end;
end;
now :: thesis: ( ( v |^ 3 = ((- q) + (sqrt (delta (1,q,((- (p / 3)) |^ 3))))) / (2 * 1) & ( y = (3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) + (3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) or y = (3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) + (3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) or y = (3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) + (3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) ) ) or ( v |^ 3 = ((- q) - (sqrt (delta (1,q,((- (p / 3)) |^ 3))))) / (2 * 1) & ( y = (3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) + (3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) or y = (3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) + (3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) or y = (3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) + (3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) ) ) )
per cases ( v |^ 3 = ((- q) + (sqrt (delta (1,q,((- (p / 3)) |^ 3))))) / (2 * 1) or v |^ 3 = ((- q) - (sqrt (delta (1,q,((- (p / 3)) |^ 3))))) / (2 * 1) ) by A8, A10, Th5;
case v |^ 3 = ((- q) + (sqrt (delta (1,q,((- (p / 3)) |^ 3))))) / (2 * 1) ; :: thesis: ( y = (3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) + (3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) or y = (3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) + (3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) or y = (3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) + (3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) )
then v |^ 3 = ((- q) + (sqrt ((q ^2) - ((4 * 1) * ((- (p / 3)) |^ 3))))) / (2 * 1) by QUIN_1:def 1;
then v |^ 3 = ((- q) / 2) + ((sqrt ((q ^2) - (4 * ((- (p / 3)) |^ 3)))) / (sqrt 4)) by SQUARE_1:20, XCMPLX_1:62;
then A30: v |^ 3 = ((- q) / 2) + (sqrt (((q ^2) - (4 * ((- (p / 3)) |^ 3))) / 4)) by A7, SQUARE_1:30
.= ((- q) / 2) + (sqrt (((q ^2) / 4) - (1 * ((- (p / 3)) |^ 3)))) ;
A31: (- (p / 3)) |^ 3 = ((- (p / 3)) to_power 1) * ((- (p / 3)) ^2) by A15, POWER:41
.= (- (p / 3)) * ((p / 3) ^2) by POWER:25 ;
now :: thesis: ( ( v > 0 & v = 3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3)))) ) or ( v = 0 & v = 3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3)))) ) or ( v < 0 & v = 3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3)))) ) )
per cases ( v > 0 or v = 0 or v < 0 ) by XXREAL_0:1;
case A32: v > 0 ; :: thesis: v = 3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))
then A33: (- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))) > 0 by A13, A30, A31, PREPOWER:6;
then v = 3 -Root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3)))) by A13, A30, A31, A32, PREPOWER:def 2;
hence v = 3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3)))) by A33, POWER:def 1; :: thesis: verum
end;
case A34: v = 0 ; :: thesis: v = 3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))
then (- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))) = 0 by A13, A30, A31, NEWTON:11;
hence v = 3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3)))) by A34, POWER:5; :: thesis: verum
end;
case v < 0 ; :: thesis: v = 3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))
then A35: - v > 0 by XREAL_1:58;
then A36: (- v) |^ 3 > 0 by PREPOWER:6;
(- v) |^ 3 = (- v) |^ (2 + 1) ;
then (- v) |^ 3 = ((- v) |^ (1 + 1)) * (- v) by NEWTON:6;
then (- v) |^ 3 = (((- v) |^ 1) * (- v)) * (- v) by NEWTON:6;
then (- v) |^ 3 = ((- v) |^ 1) * ((- v) * (- v)) ;
then (- v) |^ 3 = ((- v) to_power 1) * ((- v) ^2) by POWER:41;
then (- v) |^ 3 = (- v) * ((- v) ^2) by POWER:25;
then A37: (- v) |^ 3 = - (v * (v ^2)) ;
v |^ 3 = v |^ (2 + 1) ;
then v |^ 3 = (v |^ (1 + 1)) * v by NEWTON:6;
then v |^ 3 = ((v |^ 1) * v) * v by NEWTON:6;
then v |^ 3 = (v |^ 1) * (v * v) ;
then A38: v |^ 3 = (v to_power 1) * (v ^2) by POWER:41;
then (- v) |^ 3 = - ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3)))) by A13, A30, A31, A37, POWER:25;
then A39: - v = 3 -Root (- ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) by A35, A36, PREPOWER:def 2;
set r = (- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3)));
A40: 3 -root (- 1) = - 1 by Lm1, POWER:8;
- ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3)))) > 0 by A13, A30, A31, A36, A37, A38, POWER:25;
then - v = 3 -root ((- 1) * ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) by A39, POWER:def 1;
then - v = (3 -root (- 1)) * (3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) by Lm1, POWER:11;
hence v = 3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3)))) by A40; :: thesis: verum
end;
end;
end;
hence ( y = (3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) + (3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) or y = (3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) + (3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) or y = (3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) + (3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) ) by A2, A18; :: thesis: verum
end;
case v |^ 3 = ((- q) - (sqrt (delta (1,q,((- (p / 3)) |^ 3))))) / (2 * 1) ; :: thesis: ( y = (3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) + (3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) or y = (3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) + (3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) or y = (3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) + (3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) )
then v |^ 3 = ((- q) - (sqrt ((q ^2) - ((4 * 1) * ((- (p / 3)) |^ 3))))) / (2 * 1) by QUIN_1:def 1;
then v |^ 3 = ((- q) / 2) - ((sqrt ((q ^2) - (4 * ((- (p / 3)) |^ 3)))) / 2) ;
then A41: v |^ 3 = (- (q / 2)) - (sqrt (((q ^2) - (4 * ((- (p / 3)) |^ 3))) / 4)) by A7, SQUARE_1:20, SQUARE_1:30
.= (- (q / 2)) - (sqrt (((q ^2) / 4) - (1 * ((- (p / 3)) |^ 3)))) ;
now :: thesis: ( ( v > 0 & v = 3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3)))) ) or ( v = 0 & v = 3 -Root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3)))) & v = 3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3)))) ) or ( v < 0 & v = 3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3)))) ) )
per cases ( v > 0 or v = 0 or v < 0 ) by XXREAL_0:1;
case A42: v > 0 ; :: thesis: v = 3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))
then (- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))) > 0 by A16, A13, A41, PREPOWER:6;
then A43: v = 3 -Root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3)))) by A16, A13, A41, A42, PREPOWER:def 2;
(- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))) > 0 by A16, A13, A41, A42, PREPOWER:6;
hence v = 3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3)))) by A43, POWER:def 1; :: thesis: verum
end;
case A44: v = 0 ; :: thesis: ( v = 3 -Root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3)))) & v = 3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3)))) )
then A45: (- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))) = 0 by A16, A13, A41, NEWTON:11;
hence v = 3 -Root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3)))) by A44, PREPOWER:def 2; :: thesis: v = 3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))
hence v = 3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3)))) by A45, POWER:def 1; :: thesis: verum
end;
case v < 0 ; :: thesis: v = 3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))
then A46: - v > 0 by XREAL_1:58;
set r = (- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3)));
A47: 3 -root (- 1) = - 1 by Lm1, POWER:8;
v |^ 3 = v |^ (2 + 1) ;
then v |^ 3 = (v |^ (1 + 1)) * v by NEWTON:6;
then A48: v |^ 3 = ((v |^ 1) * v) * v by NEWTON:6;
(- v) |^ 3 = (- v) |^ (2 + 1) ;
then (- v) |^ 3 = ((- v) |^ (1 + 1)) * (- v) by NEWTON:6;
then (- v) |^ 3 = (((- v) |^ 1) * (- v)) * (- v) by NEWTON:6;
then (- v) |^ 3 = ((- v) |^ 1) * ((- v) * (- v)) ;
then A49: (- v) |^ 3 = ((- v) to_power 1) * ((- v) ^2) by POWER:41
.= (- v) * (v ^2) by POWER:25
.= - (v * (v ^2)) ;
(- v) |^ 3 = - (v |^ 3) by A49, A48;
then A50: - ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3)))) > 0 by A16, A13, A41, A46, PREPOWER:6;
(- v) |^ 3 = - ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3)))) by A16, A13, A41, A49, A48;
then - v = 3 -Root (- ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) by A46, A50, PREPOWER:def 2;
then - v = 3 -root ((- 1) * ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) by A50, POWER:def 1;
then - v = (3 -root (- 1)) * (3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) by Lm1, POWER:11;
hence v = 3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3)))) by A47; :: thesis: verum
end;
end;
end;
hence ( y = (3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) + (3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) or y = (3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) + (3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) or y = (3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) + (3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) ) by A2, A18; :: thesis: verum
end;
end;
end;
hence ( y = (3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) + (3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) or y = (3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) + (3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) or y = (3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) + (3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) ) ; :: thesis: verum
end;
case A51: u |^ 3 = ((- q) - (sqrt (delta (1,q,((- (p / 3)) |^ 3))))) / (2 * 1) ; :: thesis: ( u |^ 3 = (- (q / 2)) - (sqrt (((q ^2) / 4) - ((- (p / 3)) |^ 3))) & ( y = (3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) + (3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) or y = (3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) + (3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) or y = (3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) + (3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) ) )
(- (p / 3)) |^ 3 = (- (p / 3)) |^ (2 + 1) ;
then (- (p / 3)) |^ 3 = ((- (p / 3)) |^ (1 + 1)) * (- (p / 3)) by NEWTON:6;
then (- (p / 3)) |^ 3 = (((- (p / 3)) |^ 1) * (- (p / 3))) * (- (p / 3)) by NEWTON:6;
then (- (p / 3)) |^ 3 = ((- (p / 3)) |^ 1) * ((- (p / 3)) * (- (p / 3))) ;
then (- (p / 3)) |^ 3 = ((- (p / 3)) to_power 1) * ((- (p / 3)) ^2) by POWER:41;
then (- (p / 3)) |^ 3 = (- (p / 3)) * ((- (p / 3)) ^2) by POWER:25;
then A52: (- (p / 3)) |^ 3 = - ((p / 3) * ((p / 3) ^2)) ;
u |^ 3 = ((- q) - (sqrt ((q ^2) - ((4 * 1) * ((- (p / 3)) |^ 3))))) / (2 * 1) by A51, QUIN_1:def 1;
then A53: u |^ 3 = ((- q) * (2 ")) - ((sqrt ((q ^2) - (4 * ((- (p / 3)) |^ 3)))) / 2)
.= (- (q / 2)) - (sqrt (((q ^2) - (4 * ((- (p / 3)) |^ 3))) / 4)) by A7, SQUARE_1:20, SQUARE_1:30
.= (- (q / 2)) - (sqrt (((q ^2) / 4) - (1 * ((- (p / 3)) |^ 3)))) ;
hence u |^ 3 = (- (q / 2)) - (sqrt (((q ^2) / 4) - ((- (p / 3)) |^ 3))) ; :: thesis: ( y = (3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) + (3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) or y = (3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) + (3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) or y = (3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) + (3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) )
(p / 3) |^ 3 = (p / 3) |^ (2 + 1) ;
then (p / 3) |^ 3 = ((p / 3) |^ (1 + 1)) * (p / 3) by NEWTON:6;
then (p / 3) |^ 3 = (((p / 3) |^ 1) * (p / 3)) * (p / 3) by NEWTON:6;
then (p / 3) |^ 3 = ((p / 3) |^ 1) * ((p / 3) * (p / 3)) ;
then (p / 3) |^ 3 = ((p / 3) to_power 1) * ((p / 3) ^2) by POWER:41;
then A54: (- (p / 3)) |^ 3 = - ((p / 3) |^ 3) by A52, POWER:25;
A55: now :: thesis: ( ( u > 0 & u = 3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3)))) ) or ( u = 0 & u = 3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3)))) ) or ( u < 0 & u = 3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3)))) ) )
per cases ( u > 0 or u = 0 or u < 0 ) by XXREAL_0:1;
case A56: u > 0 ; :: thesis: u = 3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))
then (- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))) > 0 by A53, A54, PREPOWER:6;
then A57: u = 3 -Root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3)))) by A53, A54, A56, PREPOWER:def 2;
(- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))) > 0 by A53, A54, A56, PREPOWER:6;
hence u = 3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3)))) by A57, POWER:def 1; :: thesis: verum
end;
case A58: u = 0 ; :: thesis: u = 3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))
then (- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))) = 0 by A53, A54, NEWTON:11;
hence u = 3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3)))) by A58, POWER:5; :: thesis: verum
end;
case u < 0 ; :: thesis: u = 3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))
then A59: - u > 0 by XREAL_1:58;
then A60: (- u) |^ 3 > 0 by PREPOWER:6;
(- u) |^ 3 = (- u) |^ (2 + 1) ;
then (- u) |^ 3 = ((- u) |^ (1 + 1)) * (- u) by NEWTON:6;
then (- u) |^ 3 = (((- u) |^ 1) * (- u)) * (- u) by NEWTON:6;
then (- u) |^ 3 = ((- u) |^ 1) * ((- u) * (- u)) ;
then (- u) |^ 3 = ((- u) to_power 1) * ((- u) ^2) by POWER:41;
then (- u) |^ 3 = (- u) * ((- u) ^2) by POWER:25;
then A61: (- u) |^ 3 = - (u * (u ^2)) ;
u |^ 3 = u |^ (2 + 1) ;
then u |^ 3 = (u |^ (1 + 1)) * u by NEWTON:6;
then u |^ 3 = ((u |^ 1) * u) * u by NEWTON:6;
then u |^ 3 = (u |^ 1) * (u * u) ;
then A62: u |^ 3 = (u to_power 1) * (u ^2) by POWER:41;
then - ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3)))) > 0 by A53, A54, A60, A61, POWER:25;
then A63: 3 -Root (- ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) = 3 -root (- ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) by POWER:def 1;
set r = (- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3)));
(- u) |^ 3 = - ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3)))) by A53, A54, A61, A62, POWER:25;
then - u = 3 -root ((- 1) * ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) by A59, A60, A63, PREPOWER:def 2;
then A64: - u = (3 -root (- 1)) * (3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) by Lm1, POWER:11;
3 -root (- 1) = - 1 by Lm1, POWER:8;
hence u = 3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3)))) by A64; :: thesis: verum
end;
end;
end;
now :: thesis: ( ( v |^ 3 = ((- q) + (sqrt (delta (1,q,((- (p / 3)) |^ 3))))) / (2 * 1) & ( y = (3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) + (3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) or y = (3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) + (3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) or y = (3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) + (3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) ) ) or ( v |^ 3 = ((- q) - (sqrt (delta (1,q,((- (p / 3)) |^ 3))))) / (2 * 1) & y = (3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) + (3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) ) )
per cases ( v |^ 3 = ((- q) + (sqrt (delta (1,q,((- (p / 3)) |^ 3))))) / (2 * 1) or v |^ 3 = ((- q) - (sqrt (delta (1,q,((- (p / 3)) |^ 3))))) / (2 * 1) ) by A8, A10, Th5;
case A65: v |^ 3 = ((- q) + (sqrt (delta (1,q,((- (p / 3)) |^ 3))))) / (2 * 1) ; :: thesis: ( y = (3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) + (3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) or y = (3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) + (3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) or y = (3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) + (3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) )
(- (p / 3)) |^ 3 = (- (p / 3)) |^ (2 + 1) ;
then (- (p / 3)) |^ 3 = ((- (p / 3)) |^ (1 + 1)) * (- (p / 3)) by NEWTON:6;
then (- (p / 3)) |^ 3 = (((- (p / 3)) |^ 1) * (- (p / 3))) * (- (p / 3)) by NEWTON:6;
then (- (p / 3)) |^ 3 = ((- (p / 3)) |^ 1) * ((- (p / 3)) * (- (p / 3))) ;
then (- (p / 3)) |^ 3 = ((- (p / 3)) to_power 1) * ((- (p / 3)) ^2) by POWER:41;
then (- (p / 3)) |^ 3 = (- (p / 3)) * ((- (p / 3)) ^2) by POWER:25;
then A66: (- (p / 3)) |^ 3 = - ((p / 3) * ((p / 3) ^2)) ;
(p / 3) |^ 3 = (p / 3) |^ (2 + 1) ;
then (p / 3) |^ 3 = ((p / 3) |^ (1 + 1)) * (p / 3) by NEWTON:6;
then (p / 3) |^ 3 = (((p / 3) |^ 1) * (p / 3)) * (p / 3) by NEWTON:6;
then (p / 3) |^ 3 = ((p / 3) |^ 1) * ((p / 3) * (p / 3)) ;
then (p / 3) |^ 3 = ((p / 3) to_power 1) * ((p / 3) ^2) by POWER:41;
then A67: (- (p / 3)) |^ 3 = - ((p / 3) |^ 3) by A66, POWER:25;
v |^ 3 = ((- q) + (sqrt ((q ^2) - ((4 * 1) * ((- (p / 3)) |^ 3))))) / (2 * 1) by A65, QUIN_1:def 1;
then v |^ 3 = ((- q) / 2) + ((sqrt ((q ^2) - (4 * ((- (p / 3)) |^ 3)))) / (sqrt 4)) by SQUARE_1:20, XCMPLX_1:62;
then A68: v |^ 3 = ((- q) / 2) + (sqrt (((q ^2) - (4 * ((- (p / 3)) |^ 3))) / 4)) by A7, SQUARE_1:30
.= ((- q) / 2) + (sqrt (((q ^2) / 4) - (1 * ((- (p / 3)) |^ 3)))) ;
now :: thesis: ( ( v > 0 & v = 3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3)))) ) or ( v = 0 & v = 3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3)))) ) or ( v < 0 & v = 3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3)))) ) )
per cases ( v > 0 or v = 0 or v < 0 ) by XXREAL_0:1;
case A69: v > 0 ; :: thesis: v = 3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))
then A70: (- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))) > 0 by A68, A67, PREPOWER:6;
then v = 3 -Root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3)))) by A68, A67, A69, PREPOWER:def 2;
hence v = 3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3)))) by A70, POWER:def 1; :: thesis: verum
end;
case A71: v = 0 ; :: thesis: v = 3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))
then (- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))) = 0 by A68, A67, NEWTON:11;
hence v = 3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3)))) by A71, POWER:5; :: thesis: verum
end;
case v < 0 ; :: thesis: v = 3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))
then A72: - v > 0 by XREAL_1:58;
then A73: (- v) |^ 3 > 0 by PREPOWER:6;
(- v) |^ 3 = (- v) |^ (2 + 1) ;
then (- v) |^ 3 = ((- v) |^ (1 + 1)) * (- v) by NEWTON:6;
then (- v) |^ 3 = (((- v) |^ 1) * (- v)) * (- v) by NEWTON:6;
then (- v) |^ 3 = ((- v) |^ 1) * ((- v) * (- v)) ;
then (- v) |^ 3 = ((- v) to_power 1) * ((- v) ^2) by POWER:41;
then (- v) |^ 3 = (- v) * ((- v) ^2) by POWER:25;
then A74: (- v) |^ 3 = - (v * (v ^2)) ;
v |^ 3 = v |^ (2 + 1) ;
then v |^ 3 = (v |^ (1 + 1)) * v by NEWTON:6;
then v |^ 3 = ((v |^ 1) * v) * v by NEWTON:6;
then v |^ 3 = (v |^ 1) * (v * v) ;
then A75: v |^ 3 = (v to_power 1) * (v ^2) by POWER:41;
then A76: - ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3)))) > 0 by A68, A67, A73, A74, POWER:25;
set r = (- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3)));
A77: 3 -root (- 1) = - 1 by Lm1, POWER:8;
v |^ 3 = v * (v ^2) by A75, POWER:25;
then - v = 3 -Root (- ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) by A68, A67, A72, A73, A74, PREPOWER:def 2;
then - v = 3 -root ((- 1) * ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) by A76, POWER:def 1;
then - v = (3 -root (- 1)) * (3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) by Lm1, POWER:11;
hence v = 3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3)))) by A77; :: thesis: verum
end;
end;
end;
hence ( y = (3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) + (3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) or y = (3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) + (3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) or y = (3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) + (3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) ) by A2, A55; :: thesis: verum
end;
case A78: v |^ 3 = ((- q) - (sqrt (delta (1,q,((- (p / 3)) |^ 3))))) / (2 * 1) ; :: thesis: y = (3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) + (3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3)))))
q ^2 = ((u |^ 3) + (v |^ 3)) ^2 by A5, SQUARE_1:3;
then A79: (q ^2) - ((4 * 1) * ((- (p / 3)) |^ 3)) = ((u |^ 3) - (v |^ 3)) ^2 by A11;
(- (p / 3)) |^ 3 = (- (p / 3)) |^ (2 + 1)
.= ((- (p / 3)) |^ (1 + 1)) * (- (p / 3)) by NEWTON:6
.= (((- (p / 3)) |^ 1) * (- (p / 3))) * (- (p / 3)) by NEWTON:6
.= ((- (p / 3)) |^ 1) * ((- (p / 3)) * (- (p / 3))) ;
then (- (p / 3)) |^ 3 = ((- (p / 3)) to_power 1) * ((- (p / 3)) ^2) by POWER:41
.= (- (p / 3)) * ((p / 3) ^2) by POWER:25 ;
then A80: (- (p / 3)) |^ 3 = - ((p / 3) * ((p / 3) ^2)) ;
(p / 3) |^ 3 = (p / 3) |^ (2 + 1)
.= ((p / 3) |^ (1 + 1)) * (p / 3) by NEWTON:6
.= (((p / 3) |^ 1) * (p / 3)) * (p / 3) by NEWTON:6
.= ((p / 3) |^ 1) * ((p / 3) ^2) ;
then (p / 3) |^ 3 = ((p / 3) to_power 1) * ((p / 3) ^2) by POWER:41;
then A81: (- (p / 3)) |^ 3 = - ((p / 3) |^ 3) by A80, POWER:25;
v |^ 3 = ((- q) - (sqrt ((q ^2) - ((4 * 1) * ((- (p / 3)) |^ 3))))) / (2 * 1) by A78, QUIN_1:def 1;
then A82: v |^ 3 = ((- q) / 2) + (sqrt (((q ^2) - (4 * ((- (p / 3)) |^ 3))) / 4)) by A51, A78, A79, SQUARE_1:17
.= ((- q) / 2) + (sqrt (((q ^2) / 4) - (1 * ((- (p / 3)) |^ 3)))) ;
now :: thesis: ( ( v > 0 & v = 3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3)))) ) or ( v = 0 & v = 3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3)))) ) or ( v < 0 & v = 3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3)))) ) )
per cases ( v > 0 or v = 0 or v < 0 ) by XXREAL_0:1;
case A83: v > 0 ; :: thesis: v = 3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))
then A84: (- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))) > 0 by A82, A81, PREPOWER:6;
then v = 3 -Root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3)))) by A82, A81, A83, PREPOWER:def 2;
hence v = 3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3)))) by A84, POWER:def 1; :: thesis: verum
end;
case A85: v = 0 ; :: thesis: v = 3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))
then v |^ 3 = 0 by NEWTON:11;
hence v = 3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3)))) by A82, A81, A85, POWER:5; :: thesis: verum
end;
case v < 0 ; :: thesis: v = 3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))
then A86: - v > 0 by XREAL_1:58;
then A87: (- v) |^ 3 > 0 by PREPOWER:6;
set r = (- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3)));
v |^ 3 = v |^ (2 + 1)
.= (v |^ (1 + 1)) * v by NEWTON:6
.= ((v |^ 1) * v) * v by NEWTON:6
.= (v |^ 1) * (v ^2) ;
then A88: v |^ 3 = (v to_power 1) * (v ^2) by POWER:41;
(- v) |^ 3 = (- v) |^ (2 + 1)
.= ((- v) |^ (1 + 1)) * (- v) by NEWTON:6
.= (((- v) |^ 1) * (- v)) * (- v) by NEWTON:6
.= ((- v) |^ 1) * ((- v) ^2)
.= ((- v) to_power 1) * ((- v) ^2) by POWER:41
.= (- v) * (v ^2) by POWER:25 ;
then A89: (- v) |^ 3 = - (v * (v ^2)) ;
then A90: - (v |^ 3) > 0 by A87, A88, POWER:25;
A91: 3 -root (- 1) = - 1 by Lm1, POWER:8;
(- v) |^ 3 = - (v |^ 3) by A89, A88, POWER:25;
then - v = 3 -Root (- ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) by A82, A81, A86, A87, PREPOWER:def 2;
then - v = 3 -root ((- 1) * ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) by A82, A81, A90, POWER:def 1;
then - v = (3 -root (- 1)) * (3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) by Lm1, POWER:11;
hence v = 3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3)))) by A91; :: thesis: verum
end;
end;
end;
hence y = (3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) + (3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) by A2, A55; :: thesis: verum
end;
end;
end;
hence ( y = (3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) + (3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) or y = (3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) + (3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) or y = (3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) + (3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) ) ; :: thesis: verum
end;
end;
end;
hence ( y = (3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) + (3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) or y = (3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) + (3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) or y = (3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) + (3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) ) ; :: thesis: verum