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))))) )
set e1 = 1;
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)))))
set e3 = (- (p / 3)) |^ 3;
set e2 = q;
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 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

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, 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:61;
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:65;
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

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: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 ;
A14: (q ^2) - (4 * ((- (p / 3)) |^ 3)) >= 0 by A6, XREAL_1:65;
A15: (- (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 A16: (- (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)) ;
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:85, XCMPLX_1:63
.= ((- q) / 2) + (sqrt (((q ^2) - (4 * ((- (p / 3)) |^ 3))) / 4)) by A14, SQUARE_1:99
.= ((- q) / 2) + (sqrt (((q ^2) / 4) - (1 * ((- (p / 3)) |^ 3)))) ;

A18: now

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:13;
then u = 3 -Root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3)))) by A17, A16, A13, A19, PREPOWER:def 3;
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: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 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:60;
set r = (- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3)));
A25: 3 -root (- 1) = - 1 by Lm1, POWER:9;
(- 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 A26: (- 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 A27: u |^ 3 = (u to_power 1) * (u ^2) by POWER:46;
then A28: (- u) |^ 3 = - ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3)))) by A17, A16, A13, A26, POWER:30;
A29: (- u) |^ 3 = - (u |^ 3) by A26, A27, POWER:30;
then A30: - ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3)))) > 0 by A17, A16, A13, A23, PREPOWER:13;
- (u |^ 3) > 0 by A23, A29, PREPOWER:13;
then - u = 3 -Root (- ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) by A17, A16, A13, A23, A28, PREPOWER:def 3;
then - u = 3 -root ((- 1) * ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) by A30, POWER:def 1;
then - u = (3 -root (- 1)) * (3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) by Lm1, POWER:12;
hence u = 3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3)))) by A25; :: 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 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:85, XCMPLX_1:63;
then A31: v |^ 3 = ((- q) / 2) + (sqrt (((q ^2) - (4 * ((- (p / 3)) |^ 3))) / 4)) by A7, 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 A15, 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 A33: v > 0 ; :: thesis: v = 3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))

then A34: (- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))) > 0 by A13, A31, A32, PREPOWER:13;
then v = 3 -Root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3)))) by A13, A31, A32, A33, PREPOWER:def 3;
hence v = 3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3)))) by A34, POWER:def 1; :: thesis: verum

end;

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

end;

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

then A36: - v > 0 by XREAL_1:60;
then A37: (- 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 A38: (- 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 A39: v |^ 3 = (v to_power 1) * (v ^2) by POWER:46;
then (- v) |^ 3 = - ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3)))) by A13, A31, A32, A38, POWER:30;
then A40: - v = 3 -Root (- ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) by A36, A37, PREPOWER:def 3;
set r = (- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3)));
A42: 3 -root (- 1) = - 1 by Lm1, POWER:9;
- ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3)))) > 0 by A13, A31, A32, A37, A38, A39, POWER:30;
then - v = 3 -root ((- 1) * ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) by A40, POWER:def 1;
then - v = (3 -root (- 1)) * (3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) by Lm1, POWER:12;
hence v = 3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3)))) by A42; :: 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 A43: v |^ 3 = (- (q / 2)) - (sqrt (((q ^2) - (4 * ((- (p / 3)) |^ 3))) / 4)) by A7, 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 A44: 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, A43, PREPOWER:13;
then A45: v = 3 -Root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3)))) by A16, A13, A43, A44, PREPOWER:def 3;
(- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))) > 0 by A16, A13, A43, A44, PREPOWER:13;
hence v = 3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3)))) by A45, POWER:def 1; :: thesis: verum

end;

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

end;

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

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

A59: now

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

case A60: 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 A57, A58, PREPOWER:13;
then A61: u = 3 -Root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3)))) by A57, A58, A60, PREPOWER:def 3;
(- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))) > 0 by A57, A58, A60, PREPOWER:13;
hence u = 3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3)))) by A61, POWER:def 1; :: thesis: verum

end;

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

end;

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

then A63: - u > 0 by XREAL_1:60;
then A64: (- 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 A65: (- 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 A66: u |^ 3 = (u to_power 1) * (u ^2) by POWER:46;
then - ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3)))) > 0 by A57, A58, A64, A65, POWER:30;
then A67: 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 A57, A58, A65, A66, POWER:30;
then - u = 3 -root ((- 1) * ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) by A63, A64, A67, PREPOWER:def 3;
then A69: - u = (3 -root (- 1)) * (3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) by Lm1, POWER:12;
3 -root (- 1) = - 1 by Lm1, POWER:9;
hence u = 3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3)))) by A69; :: 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 A8, A10, Th5;

case A70: 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: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 A71: (- (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 A72: (- (p / 3)) |^ 3 = - ((p / 3) |^ 3) by A71, POWER:30;
v |^ 3 = ((- q) + (sqrt ((q ^2) - ((4 * 1) * ((- (p / 3)) |^ 3))))) / (2 * 1) by A70, 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 A73: v |^ 3 = ((- q) / 2) + (sqrt (((q ^2) - (4 * ((- (p / 3)) |^ 3))) / 4)) by A7, 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 A74: v > 0 ; :: thesis: v = 3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))

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

end;

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

end;

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

then A77: - v > 0 by XREAL_1:60;
then A78: (- 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 A79: (- 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 A80: v |^ 3 = (v to_power 1) * (v ^2) by POWER:46;
then A81: - ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3)))) > 0 by A73, A72, A78, A79, POWER:30;
set r = (- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3)));
A83: 3 -root (- 1) = - 1 by Lm1, POWER:9;
v |^ 3 = v * (v ^2) by A80, POWER:30;
then - v = 3 -Root (- ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) by A73, A72, A77, A78, A79, PREPOWER:def 3;
then - v = 3 -root ((- 1) * ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) by A81, POWER:def 1;
then - v = (3 -root (- 1)) * (3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) by Lm1, POWER:12;
hence v = 3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3)))) by A83; :: 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, A59; :: thesis: verum

end;

case A84: 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:61;
then A85: (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: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 A86: (- (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 A87: (- (p / 3)) |^ 3 = - ((p / 3) |^ 3) by A86, POWER:30;
v |^ 3 = ((- q) - (sqrt ((q ^2) - ((4 * 1) * ((- (p / 3)) |^ 3))))) / (2 * 1) by A84, QUIN_1:def 1;
then A88: v |^ 3 = ((- q) / 2) + (sqrt (((q ^2) - (4 * ((- (p / 3)) |^ 3))) / 4)) by A55, A84, A85, SQUARE_1:82
.= ((- 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 A89: v > 0 ; :: thesis: v = 3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))

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

end;

case A91: 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 A88, A87, A91, POWER:6; :: thesis: verum

end;

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

then A92: - v > 0 by XREAL_1:60;
then A93: (- v) |^ 3 > 0 by PREPOWER:13;
set r = (- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3)));
v |^ 3 = v |^ (2 + 1)
.= (v |^ (1 + 1)) * v by NEWTON:11
.= ((v |^ 1) * v) * v by NEWTON:11
.= (v |^ 1) * (v ^2) ;
then A94: v |^ 3 = (v to_power 1) * (v ^2) by POWER:46;
(- 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 A95: (- v) |^ 3 = - (v * (v ^2)) ;
then A96: - (v |^ 3) > 0 by A93, A94, POWER:30;
A98: 3 -root (- 1) = - 1 by Lm1, POWER:9;
(- v) |^ 3 = - (v |^ 3) by A95, A94, POWER:30;
then - v = 3 -Root (- ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) by A88, A87, A92, A93, PREPOWER:def 3;
then - v = 3 -root ((- 1) * ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) by A88, A87, A96, POWER:def 1;
then - v = (3 -root (- 1)) * (3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) by Lm1, POWER:12;
hence v = 3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3)))) by A98; :: 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, A59; :: 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