let p, q, y be real number ; :: thesis: ( Polynom 1,0 ,p,q,y = 0 implies for u, v being real number 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))))) )
assume A1: Polynom 1,0 ,p,q,y = 0 ; :: thesis: for u, v being real number 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)))))
let u, v be real number ; :: 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 A2: ( y = u + v & ((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 z1 = u |^ 3;
set z2 = v |^ 3;
A3: (u |^ 3) + (v |^ 3) = - q by A1, A2, Th18;
A4: (v |^ 3) * (u |^ 3) = (- (p / 3)) |^ 3 by A1, A2, Th18;

A5: now

let z be real number ; :: 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, Th18
.= ((z ^2 ) + (q * z)) + ((- (p / 3)) |^ 3) by A1, A2, Th18 ; :: thesis: verum

end;

set e1 = 1;
set e2 = q;
set e3 = (- (p / 3)) |^ 3;
((u |^ 3) - (u |^ 3)) * ((u |^ 3) - (v |^ 3)) = 0 * ((u |^ 3) - (v |^ 3)) ;
then A6: Polynom 1,q,((- (p / 3)) |^ 3),(u |^ 3) = 0 by A5;
q ^2 = ((u |^ 3) + (v |^ 3)) ^2 by A3, SQUARE_1:61;
then A7: (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, Th18
.= ((u |^ 3) - (v |^ 3)) ^2 ;
then A8: (q ^2 ) - ((4 * 1) * ((- (p / 3)) |^ 3)) >= 0 by XREAL_1:65;
then A9: delta 1,q,((- (p / 3)) |^ 3) >= 0 by QUIN_1:def 1;
((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 A5;

now

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 A6, A9, Th5;

case A11: 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))))) )

A12: (q ^2 ) - (4 * ((- (p / 3)) |^ 3)) >= 0 by A7, XREAL_1:65;
A13: u |^ 3 = ((- q) + (sqrt ((q ^2 ) - ((4 * 1) * ((- (p / 3)) |^ 3))))) / (2 * 1) by A11, QUIN_1:def 1
.= ((- q) / 2) + ((sqrt ((q ^2 ) - (4 * ((- (p / 3)) |^ 3)))) / (sqrt 4)) by SQUARE_1:85, XCMPLX_1:63
.= ((- q) / 2) + (sqrt (((q ^2 ) - (4 * ((- (p / 3)) |^ 3))) / 4)) by A12, SQUARE_1:99
.= ((- q) / 2) + (sqrt (((q ^2 ) / 4) - (1 * ((- (p / 3)) |^ 3)))) ;
A14: (- (p / 3)) |^ 3 = (- (p / 3)) |^ (2 + 1)
.= ((- (p / 3)) |^ (1 + 1)) * (- (p / 3)) by NEWTON:11
.= (((- (p / 3)) |^ 1) * (- (p / 3))) * (- (p / 3)) by NEWTON:11
.= ((- (p / 3)) |^ 1) * ((- (p / 3)) ^2 ) ;
then A15: (- (p / 3)) |^ 3 = ((- (p / 3)) to_power 1) * ((- (p / 3)) ^2 ) by POWER:46
.= (- (p / 3)) * ((p / 3) ^2 ) by POWER:30
.= - ((p / 3) * ((p / 3) ^2 )) ;
A16: (p / 3) |^ 3 = (p / 3) |^ (2 + 1)
.= ((p / 3) |^ (1 + 1)) * (p / 3) by NEWTON:11
.= (((p / 3) |^ 1) * (p / 3)) * (p / 3) by NEWTON:11
.= ((p / 3) |^ 1) * ((p / 3) ^2 )
.= ((p / 3) to_power 1) * ((p / 3) ^2 ) by POWER:46
.= (p / 3) * ((p / 3) ^2 ) by POWER:30 ;

A17: now

per cases ( u > 0 or u = 0 or u < 0 ) by XXREAL_0:1;

case u > 0 ; :: thesis: u = 3 -root ((- (q / 2)) + (sqrt (((q ^2 ) / 4) + ((p / 3) |^ 3))))

then A18: ( u > 0 & (- (q / 2)) + (sqrt (((q ^2 ) / 4) + ((p / 3) |^ 3))) > 0 ) by A13, A15, A16, PREPOWER:13;
then u = 3 -Root ((- (q / 2)) + (sqrt (((q ^2 ) / 4) + ((p / 3) |^ 3)))) by A13, A15, A16, PREPOWER:def 3;
hence u = 3 -root ((- (q / 2)) + (sqrt (((q ^2 ) / 4) + ((p / 3) |^ 3)))) by A18, POWER:def 1; :: thesis: verum

end;

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 A13, A15, A16, NEWTON:16;
then 3 -Root ((- (q / 2)) + (sqrt (((q ^2 ) / 4) + ((p / 3) |^ 3)))) = 0 by PREPOWER:def 3;
hence u = 3 -root ((- (q / 2)) + (sqrt (((q ^2 ) / 4) + ((p / 3) |^ 3)))) by A19, A20, POWER:def 1; :: thesis: verum

end;

case u < 0 ; :: thesis: u = 3 -root ((- (q / 2)) + (sqrt (((q ^2 ) / 4) + ((p / 3) |^ 3))))

then A21: - u > 0 by XREAL_1:60;
(- u) |^ 3 = (- u) |^ (2 + 1)
.= ((- u) |^ (1 + 1)) * (- u) by NEWTON:11
.= (((- u) |^ 1) * (- u)) * (- u) by NEWTON:11
.= ((- u) |^ 1) * ((- u) ^2 ) ;
then (- u) |^ 3 = ((- u) to_power 1) * ((- u) ^2 ) by POWER:46;
then A22: (- u) |^ 3 = (- u) * (u ^2 ) by POWER:30
.= - (u * (u ^2 )) ;
u |^ 3 = u |^ (2 + 1)
.= (u |^ (1 + 1)) * u by NEWTON:11
.= ((u |^ 1) * u) * u by NEWTON:11
.= (u |^ 1) * (u * u) ;
then A23: u |^ 3 = (u to_power 1) * (u ^2 ) by POWER:46;
then A24: (- u) |^ 3 = - (u |^ 3) by A22, POWER:30;
then A25: - (u |^ 3) > 0 by A21, PREPOWER:13;
A26: - ((- (q / 2)) + (sqrt (((q ^2 ) / 4) + ((p / 3) |^ 3)))) > 0 by A13, A15, A16, A21, A24, PREPOWER:13;
(- u) |^ 3 = - ((- (q / 2)) + (sqrt (((q ^2 ) / 4) + ((p / 3) |^ 3)))) by A13, A15, A16, A22, A23, POWER:30;
then A27: - u = 3 -Root (- ((- (q / 2)) + (sqrt (((q ^2 ) / 4) + ((p / 3) |^ 3))))) by A13, A15, A16, A21, A25, PREPOWER:def 3;
set r = (- (q / 2)) + (sqrt (((q ^2 ) / 4) + ((p / 3) |^ 3)));
A28: - u = 3 -root ((- 1) * ((- (q / 2)) + (sqrt (((q ^2 ) / 4) + ((p / 3) |^ 3))))) by A26, A27, POWER:def 1;
A29: 3 = (2 * 1) + 1 ;
then A30: - u = (3 -root (- 1)) * (3 -root ((- (q / 2)) + (sqrt (((q ^2 ) / 4) + ((p / 3) |^ 3))))) by A28, POWER:12;
3 -root (- 1) = - 1 by A29, POWER:9;
hence u = 3 -root ((- (q / 2)) + (sqrt (((q ^2 ) / 4) + ((p / 3) |^ 3)))) by A30; :: thesis: verum

end;

end;

end;

now

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 A9, 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:85, XCMPLX_1:63;
then A31: v |^ 3 = ((- q) / 2) + (sqrt (((q ^2 ) - (4 * ((- (p / 3)) |^ 3))) / 4)) by A8, SQUARE_1:99
.= ((- q) / 2) + (sqrt (((q ^2 ) / 4) - (1 * ((- (p / 3)) |^ 3)))) ;
A32: (- (p / 3)) |^ 3 = ((- (p / 3)) to_power 1) * ((- (p / 3)) ^2 ) by A14, POWER:46
.= (- (p / 3)) * ((p / 3) ^2 ) by POWER:30 ;

now

per cases ( v > 0 or v = 0 or v < 0 ) by XXREAL_0:1;

case v > 0 ; :: thesis: v = 3 -root ((- (q / 2)) + (sqrt (((q ^2 ) / 4) + ((p / 3) |^ 3))))

then A33: ( v > 0 & (- (q / 2)) + (sqrt (((q ^2 ) / 4) + ((p / 3) |^ 3))) > 0 ) by A16, A31, A32, PREPOWER:13;
then v = 3 -Root ((- (q / 2)) + (sqrt (((q ^2 ) / 4) + ((p / 3) |^ 3)))) by A16, A31, A32, PREPOWER:def 3;
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 A16, A31, A32, NEWTON:16;
hence v = 3 -root ((- (q / 2)) + (sqrt (((q ^2 ) / 4) + ((p / 3) |^ 3)))) by A34, POWER:6; :: 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:60;
then A36: (- v) |^ 3 > 0 by PREPOWER:13;
(- v) |^ 3 = (- v) |^ (2 + 1) ;
then (- v) |^ 3 = ((- v) |^ (1 + 1)) * (- v) by NEWTON:11;
then (- v) |^ 3 = (((- v) |^ 1) * (- v)) * (- v) by NEWTON:11;
then (- v) |^ 3 = ((- v) |^ 1) * ((- v) * (- v)) ;
then (- v) |^ 3 = ((- v) to_power 1) * ((- v) ^2 ) by POWER:46;
then (- v) |^ 3 = (- v) * ((- v) ^2 ) by POWER:30;
then A37: (- v) |^ 3 = - (v * (v ^2 )) ;
v |^ 3 = v |^ (2 + 1) ;
then v |^ 3 = (v |^ (1 + 1)) * v by NEWTON:11;
then v |^ 3 = ((v |^ 1) * v) * v by NEWTON:11;
then v |^ 3 = (v |^ 1) * (v * v) ;
then A38: v |^ 3 = (v to_power 1) * (v ^2 ) by POWER:46;
then A39: - ((- (q / 2)) + (sqrt (((q ^2 ) / 4) + ((p / 3) |^ 3)))) > 0 by A16, A31, A32, A36, A37, POWER:30;
(- v) |^ 3 = - ((- (q / 2)) + (sqrt (((q ^2 ) / 4) + ((p / 3) |^ 3)))) by A16, A31, A32, A37, A38, POWER:30;
then A40: - v = 3 -Root (- ((- (q / 2)) + (sqrt (((q ^2 ) / 4) + ((p / 3) |^ 3))))) by A35, A36, PREPOWER:def 3;
set r = (- (q / 2)) + (sqrt (((q ^2 ) / 4) + ((p / 3) |^ 3)));
A41: - v = 3 -root ((- 1) * ((- (q / 2)) + (sqrt (((q ^2 ) / 4) + ((p / 3) |^ 3))))) by A39, A40, POWER:def 1;
A42: 3 = (2 * 1) + 1 ;
then A43: - v = (3 -root (- 1)) * (3 -root ((- (q / 2)) + (sqrt (((q ^2 ) / 4) + ((p / 3) |^ 3))))) by A41, POWER:12;
3 -root (- 1) = - 1 by A42, POWER:9;
hence v = 3 -root ((- (q / 2)) + (sqrt (((q ^2 ) / 4) + ((p / 3) |^ 3)))) by A43; :: 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, A17; :: 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 A44: v |^ 3 = (- (q / 2)) - (sqrt (((q ^2 ) - (4 * ((- (p / 3)) |^ 3))) / 4)) by A8, SQUARE_1:85, SQUARE_1:99
.= (- (q / 2)) - (sqrt (((q ^2 ) / 4) - (1 * ((- (p / 3)) |^ 3)))) ;

now

per cases ( v > 0 or v = 0 or v < 0 ) by XXREAL_0:1;

case A45: v > 0 ; :: thesis: v = 3 -root ((- (q / 2)) - (sqrt (((q ^2 ) / 4) + ((p / 3) |^ 3))))

then A46: (- (q / 2)) - (sqrt (((q ^2 ) / 4) + ((p / 3) |^ 3))) > 0 by A15, A16, A44, PREPOWER:13;
( v > 0 & (- (q / 2)) - (sqrt (((q ^2 ) / 4) + ((p / 3) |^ 3))) > 0 ) by A15, A16, A44, A45, PREPOWER:13;
then v = 3 -Root ((- (q / 2)) - (sqrt (((q ^2 ) / 4) + ((p / 3) |^ 3)))) by A15, A16, A44, PREPOWER:def 3;
hence v = 3 -root ((- (q / 2)) - (sqrt (((q ^2 ) / 4) + ((p / 3) |^ 3)))) by A46, POWER:def 1; :: thesis: verum

end;

case A47: 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 A48: (- (q / 2)) - (sqrt (((q ^2 ) / 4) + ((p / 3) |^ 3))) = 0 by A15, A16, A44, NEWTON:16;
hence v = 3 -Root ((- (q / 2)) - (sqrt (((q ^2 ) / 4) + ((p / 3) |^ 3)))) by A47, PREPOWER:def 3; :: 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 A48, POWER:def 1; :: thesis: verum

end;

case v < 0 ; :: thesis: v = 3 -root ((- (q / 2)) - (sqrt (((q ^2 ) / 4) + ((p / 3) |^ 3))))

then A49: - v > 0 by XREAL_1:60;
(- v) |^ 3 = (- v) |^ (2 + 1) ;
then (- v) |^ 3 = ((- v) |^ (1 + 1)) * (- v) by NEWTON:11;
then (- v) |^ 3 = (((- v) |^ 1) * (- v)) * (- v) by NEWTON:11;
then (- v) |^ 3 = ((- v) |^ 1) * ((- v) * (- v)) ;
then A50: (- v) |^ 3 = ((- v) to_power 1) * ((- v) ^2 ) by POWER:46
.= (- v) * (v ^2 ) by POWER:30
.= - (v * (v ^2 )) ;
v |^ 3 = v |^ (2 + 1) ;
then v |^ 3 = (v |^ (1 + 1)) * v by NEWTON:11;
then A51: v |^ 3 = ((v |^ 1) * v) * v by NEWTON:11;
A52: v to_power 1 = v by POWER:30;
then (- v) |^ 3 = - (v |^ 3) by A50, A51, POWER:46;
then A53: - ((- (q / 2)) - (sqrt (((q ^2 ) / 4) + ((p / 3) |^ 3)))) > 0 by A15, A16, A44, A49, PREPOWER:13;
(- v) |^ 3 = - ((- (q / 2)) - (sqrt (((q ^2 ) / 4) + ((p / 3) |^ 3)))) by A15, A16, A44, A50, A51, A52, POWER:46;
then A54: - v = 3 -Root (- ((- (q / 2)) - (sqrt (((q ^2 ) / 4) + ((p / 3) |^ 3))))) by A49, A53, PREPOWER:def 3;
set r = (- (q / 2)) - (sqrt (((q ^2 ) / 4) + ((p / 3) |^ 3)));
A55: - v = 3 -root ((- 1) * ((- (q / 2)) - (sqrt (((q ^2 ) / 4) + ((p / 3) |^ 3))))) by A53, A54, POWER:def 1;
A56: 3 = (2 * 1) + 1 ;
then A57: - v = (3 -root (- 1)) * (3 -root ((- (q / 2)) - (sqrt (((q ^2 ) / 4) + ((p / 3) |^ 3))))) by A55, POWER:12;
3 -root (- 1) = - 1 by A56, POWER:9;
hence v = 3 -root ((- (q / 2)) - (sqrt (((q ^2 ) / 4) + ((p / 3) |^ 3)))) by A57; :: 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, A17; :: 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 A58: 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))))) ) )

then u |^ 3 = ((- q) - (sqrt ((q ^2 ) - ((4 * 1) * ((- (p / 3)) |^ 3))))) / (2 * 1) by QUIN_1:def 1;
then A59: u |^ 3 = ((- q) * (2 " )) - ((sqrt ((q ^2 ) - (4 * ((- (p / 3)) |^ 3)))) / 2)
.= (- (q / 2)) - (sqrt (((q ^2 ) - (4 * ((- (p / 3)) |^ 3))) / 4)) by A8, SQUARE_1:85, SQUARE_1:99
.= (- (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:11;
then (- (p / 3)) |^ 3 = (((- (p / 3)) |^ 1) * (- (p / 3))) * (- (p / 3)) by NEWTON:11;
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:46;
then (- (p / 3)) |^ 3 = (- (p / 3)) * ((- (p / 3)) ^2 ) by POWER:30;
then A60: (- (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:11;
then (p / 3) |^ 3 = (((p / 3) |^ 1) * (p / 3)) * (p / 3) by NEWTON:11;
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:46;
then A61: (- (p / 3)) |^ 3 = - ((p / 3) |^ 3) by A60, POWER:30;

A62: now

per cases ( u > 0 or u = 0 or u < 0 ) by XXREAL_0:1;

case A63: u > 0 ; :: thesis: u = 3 -root ((- (q / 2)) - (sqrt (((q ^2 ) / 4) + ((p / 3) |^ 3))))

then A64: (- (q / 2)) - (sqrt (((q ^2 ) / 4) + ((p / 3) |^ 3))) > 0 by A59, A61, PREPOWER:13;
( u > 0 & (- (q / 2)) - (sqrt (((q ^2 ) / 4) + ((p / 3) |^ 3))) > 0 ) by A59, A61, A63, PREPOWER:13;
then u = 3 -Root ((- (q / 2)) - (sqrt (((q ^2 ) / 4) + ((p / 3) |^ 3)))) by A59, A61, PREPOWER:def 3;
hence u = 3 -root ((- (q / 2)) - (sqrt (((q ^2 ) / 4) + ((p / 3) |^ 3)))) by A64, POWER:def 1; :: thesis: verum

end;

case A65: 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 A59, A61, NEWTON:16;
hence u = 3 -root ((- (q / 2)) - (sqrt (((q ^2 ) / 4) + ((p / 3) |^ 3)))) by A65, POWER:6; :: thesis: verum

end;

case u < 0 ; :: thesis: u = 3 -root ((- (q / 2)) - (sqrt (((q ^2 ) / 4) + ((p / 3) |^ 3))))

then A66: - u > 0 by XREAL_1:60;
then A67: (- u) |^ 3 > 0 by PREPOWER:13;
(- u) |^ 3 = (- u) |^ (2 + 1) ;
then (- u) |^ 3 = ((- u) |^ (1 + 1)) * (- u) by NEWTON:11;
then (- u) |^ 3 = (((- u) |^ 1) * (- u)) * (- u) by NEWTON:11;
then (- u) |^ 3 = ((- u) |^ 1) * ((- u) * (- u)) ;
then (- u) |^ 3 = ((- u) to_power 1) * ((- u) ^2 ) by POWER:46;
then (- u) |^ 3 = (- u) * ((- u) ^2 ) by POWER:30;
then A68: (- u) |^ 3 = - (u * (u ^2 )) ;
u |^ 3 = u |^ (2 + 1) ;
then u |^ 3 = (u |^ (1 + 1)) * u by NEWTON:11;
then u |^ 3 = ((u |^ 1) * u) * u by NEWTON:11;
then u |^ 3 = (u |^ 1) * (u * u) ;
then A69: u |^ 3 = (u to_power 1) * (u ^2 ) by POWER:46;
then A70: - ((- (q / 2)) - (sqrt (((q ^2 ) / 4) + ((p / 3) |^ 3)))) > 0 by A59, A61, A67, A68, POWER:30;
A71: (- u) |^ 3 = - ((- (q / 2)) - (sqrt (((q ^2 ) / 4) + ((p / 3) |^ 3)))) by A59, A61, A68, A69, POWER:30;
A72: 3 -Root (- ((- (q / 2)) - (sqrt (((q ^2 ) / 4) + ((p / 3) |^ 3))))) = 3 -root (- ((- (q / 2)) - (sqrt (((q ^2 ) / 4) + ((p / 3) |^ 3))))) by A70, POWER:def 1;
set r = (- (q / 2)) - (sqrt (((q ^2 ) / 4) + ((p / 3) |^ 3)));
A73: - u = 3 -root ((- 1) * ((- (q / 2)) - (sqrt (((q ^2 ) / 4) + ((p / 3) |^ 3))))) by A66, A67, A71, A72, PREPOWER:def 3;
A74: 3 = (2 * 1) + 1 ;
then A75: - u = (3 -root (- 1)) * (3 -root ((- (q / 2)) - (sqrt (((q ^2 ) / 4) + ((p / 3) |^ 3))))) by A73, POWER:12;
3 -root (- 1) = - 1 by A74, POWER:9;
hence u = 3 -root ((- (q / 2)) - (sqrt (((q ^2 ) / 4) + ((p / 3) |^ 3)))) by A75; :: thesis: verum

end;

end;

end;

now

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 A9, 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:85, XCMPLX_1:63;
then A76: v |^ 3 = ((- q) / 2) + (sqrt (((q ^2 ) - (4 * ((- (p / 3)) |^ 3))) / 4)) by A8, SQUARE_1:99
.= ((- q) / 2) + (sqrt (((q ^2 ) / 4) - (1 * ((- (p / 3)) |^ 3)))) ;
(- (p / 3)) |^ 3 = (- (p / 3)) |^ (2 + 1) ;
then (- (p / 3)) |^ 3 = ((- (p / 3)) |^ (1 + 1)) * (- (p / 3)) by NEWTON:11;
then (- (p / 3)) |^ 3 = (((- (p / 3)) |^ 1) * (- (p / 3))) * (- (p / 3)) by NEWTON:11;
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:46;
then (- (p / 3)) |^ 3 = (- (p / 3)) * ((- (p / 3)) ^2 ) by POWER:30;
then A77: (- (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:11;
then (p / 3) |^ 3 = (((p / 3) |^ 1) * (p / 3)) * (p / 3) by NEWTON:11;
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:46;
then A78: (- (p / 3)) |^ 3 = - ((p / 3) |^ 3) by A77, POWER:30;

now

per cases ( v > 0 or v = 0 or v < 0 ) by XXREAL_0:1;

case v > 0 ; :: thesis: v = 3 -root ((- (q / 2)) + (sqrt (((q ^2 ) / 4) + ((p / 3) |^ 3))))

then A79: ( v > 0 & (- (q / 2)) + (sqrt (((q ^2 ) / 4) + ((p / 3) |^ 3))) > 0 ) by A76, A78, PREPOWER:13;
then v = 3 -Root ((- (q / 2)) + (sqrt (((q ^2 ) / 4) + ((p / 3) |^ 3)))) by A76, A78, PREPOWER:def 3;
hence v = 3 -root ((- (q / 2)) + (sqrt (((q ^2 ) / 4) + ((p / 3) |^ 3)))) by A79, POWER:def 1; :: thesis: verum

end;

case A80: 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 A76, A78, NEWTON:16;
hence v = 3 -root ((- (q / 2)) + (sqrt (((q ^2 ) / 4) + ((p / 3) |^ 3)))) by A80, POWER:6; :: thesis: verum

end;

case v < 0 ; :: thesis: v = 3 -root ((- (q / 2)) + (sqrt (((q ^2 ) / 4) + ((p / 3) |^ 3))))

then A81: - v > 0 by XREAL_1:60;
then A82: (- v) |^ 3 > 0 by PREPOWER:13;
(- v) |^ 3 = (- v) |^ (2 + 1) ;
then (- v) |^ 3 = ((- v) |^ (1 + 1)) * (- v) by NEWTON:11;
then (- v) |^ 3 = (((- v) |^ 1) * (- v)) * (- v) by NEWTON:11;
then (- v) |^ 3 = ((- v) |^ 1) * ((- v) * (- v)) ;
then (- v) |^ 3 = ((- v) to_power 1) * ((- v) ^2 ) by POWER:46;
then (- v) |^ 3 = (- v) * ((- v) ^2 ) by POWER:30;
then A83: (- v) |^ 3 = - (v * (v ^2 )) ;
v |^ 3 = v |^ (2 + 1) ;
then v |^ 3 = (v |^ (1 + 1)) * v by NEWTON:11;
then v |^ 3 = ((v |^ 1) * v) * v by NEWTON:11;
then v |^ 3 = (v |^ 1) * (v * v) ;
then A84: v |^ 3 = (v to_power 1) * (v ^2 ) by POWER:46;
then A85: v |^ 3 = v * (v ^2 ) by POWER:30;
A86: - ((- (q / 2)) + (sqrt (((q ^2 ) / 4) + ((p / 3) |^ 3)))) > 0 by A76, A78, A82, A83, A84, POWER:30;
A87: - v = 3 -Root (- ((- (q / 2)) + (sqrt (((q ^2 ) / 4) + ((p / 3) |^ 3))))) by A76, A78, A81, A82, A83, A85, PREPOWER:def 3;
set r = (- (q / 2)) + (sqrt (((q ^2 ) / 4) + ((p / 3) |^ 3)));
A88: - v = 3 -root ((- 1) * ((- (q / 2)) + (sqrt (((q ^2 ) / 4) + ((p / 3) |^ 3))))) by A86, A87, POWER:def 1;
A89: 3 = (2 * 1) + 1 ;
then A90: - v = (3 -root (- 1)) * (3 -root ((- (q / 2)) + (sqrt (((q ^2 ) / 4) + ((p / 3) |^ 3))))) by A88, POWER:12;
3 -root (- 1) = - 1 by A89, POWER:9;
hence v = 3 -root ((- (q / 2)) + (sqrt (((q ^2 ) / 4) + ((p / 3) |^ 3)))) by A90; :: 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, A62; :: thesis: verum

end;

case A91: 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)))))

then A92: v |^ 3 = ((- q) - (sqrt ((q ^2 ) - ((4 * 1) * ((- (p / 3)) |^ 3))))) / (2 * 1) by QUIN_1:def 1;
q ^2 = ((u |^ 3) + (v |^ 3)) ^2 by A3, SQUARE_1:61;
then (q ^2 ) - ((4 * 1) * ((- (p / 3)) |^ 3)) = ((u |^ 3) - (v |^ 3)) ^2 by A4;
then A93: v |^ 3 = ((- q) / 2) + (sqrt (((q ^2 ) - (4 * ((- (p / 3)) |^ 3))) / 4)) by A58, A91, A92, SQUARE_1:82
.= ((- q) / 2) + (sqrt (((q ^2 ) / 4) - (1 * ((- (p / 3)) |^ 3)))) ;
(- (p / 3)) |^ 3 = (- (p / 3)) |^ (2 + 1)
.= ((- (p / 3)) |^ (1 + 1)) * (- (p / 3)) by NEWTON:11
.= (((- (p / 3)) |^ 1) * (- (p / 3))) * (- (p / 3)) by NEWTON:11
.= ((- (p / 3)) |^ 1) * ((- (p / 3)) * (- (p / 3))) ;
then (- (p / 3)) |^ 3 = ((- (p / 3)) to_power 1) * ((- (p / 3)) ^2 ) by POWER:46
.= (- (p / 3)) * ((p / 3) ^2 ) by POWER:30 ;
then A94: (- (p / 3)) |^ 3 = - ((p / 3) * ((p / 3) ^2 )) ;
(p / 3) |^ 3 = (p / 3) |^ (2 + 1)
.= ((p / 3) |^ (1 + 1)) * (p / 3) by NEWTON:11
.= (((p / 3) |^ 1) * (p / 3)) * (p / 3) by NEWTON:11
.= ((p / 3) |^ 1) * ((p / 3) ^2 ) ;
then (p / 3) |^ 3 = ((p / 3) to_power 1) * ((p / 3) ^2 ) by POWER:46;
then A95: (- (p / 3)) |^ 3 = - ((p / 3) |^ 3) by A94, POWER:30;

now

per cases ( v > 0 or v = 0 or v < 0 ) by XXREAL_0:1;

case v > 0 ; :: thesis: v = 3 -root ((- (q / 2)) + (sqrt (((q ^2 ) / 4) + ((p / 3) |^ 3))))

then A96: ( v > 0 & (- (q / 2)) + (sqrt (((q ^2 ) / 4) + ((p / 3) |^ 3))) > 0 ) by A93, A95, PREPOWER:13;
then v = 3 -Root ((- (q / 2)) + (sqrt (((q ^2 ) / 4) + ((p / 3) |^ 3)))) by A93, A95, PREPOWER:def 3;
hence v = 3 -root ((- (q / 2)) + (sqrt (((q ^2 ) / 4) + ((p / 3) |^ 3)))) by A96, POWER:def 1; :: thesis: verum

end;

case A97: v = 0 ; :: thesis: v = 3 -root ((- (q / 2)) + (sqrt (((q ^2 ) / 4) + ((p / 3) |^ 3))))

then v |^ 3 = 0 by NEWTON:16;
hence v = 3 -root ((- (q / 2)) + (sqrt (((q ^2 ) / 4) + ((p / 3) |^ 3)))) by A93, A95, A97, POWER:6; :: thesis: verum

end;

case v < 0 ; :: thesis: v = 3 -root ((- (q / 2)) + (sqrt (((q ^2 ) / 4) + ((p / 3) |^ 3))))

then A98: - v > 0 by XREAL_1:60;
then A99: (- v) |^ 3 > 0 by PREPOWER:13;
(- v) |^ 3 = (- v) |^ (2 + 1)
.= ((- v) |^ (1 + 1)) * (- v) by NEWTON:11
.= (((- v) |^ 1) * (- v)) * (- v) by NEWTON:11
.= ((- v) |^ 1) * ((- v) ^2 )
.= ((- v) to_power 1) * ((- v) ^2 ) by POWER:46
.= (- v) * (v ^2 ) by POWER:30 ;
then A100: (- v) |^ 3 = - (v * (v ^2 )) ;
v |^ 3 = v |^ (2 + 1)
.= (v |^ (1 + 1)) * v by NEWTON:11
.= ((v |^ 1) * v) * v by NEWTON:11
.= (v |^ 1) * (v ^2 ) ;
then A101: v |^ 3 = (v to_power 1) * (v ^2 ) by POWER:46;
then A102: (- v) |^ 3 = - (v |^ 3) by A100, POWER:30;
A103: - (v |^ 3) > 0 by A99, A100, A101, POWER:30;
A104: - v = 3 -Root (- ((- (q / 2)) + (sqrt (((q ^2 ) / 4) + ((p / 3) |^ 3))))) by A93, A95, A98, A99, A102, PREPOWER:def 3;
set r = (- (q / 2)) + (sqrt (((q ^2 ) / 4) + ((p / 3) |^ 3)));
A105: - v = 3 -root ((- 1) * ((- (q / 2)) + (sqrt (((q ^2 ) / 4) + ((p / 3) |^ 3))))) by A93, A95, A103, A104, POWER:def 1;
A106: 3 = (2 * 1) + 1 ;
then A107: - v = (3 -root (- 1)) * (3 -root ((- (q / 2)) + (sqrt (((q ^2 ) / 4) + ((p / 3) |^ 3))))) by A105, POWER:12;
3 -root (- 1) = - 1 by A106, POWER:9;
hence v = 3 -root ((- (q / 2)) + (sqrt (((q ^2 ) / 4) + ((p / 3) |^ 3)))) by A107; :: 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, A62; :: 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