let p, q, y be Real; ( 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
; 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; ( 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
; ( 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;
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 ( ( 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)
;
( 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 ( ( 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
u < 0
;
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;
verum end; end; end; now ( ( 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)
;
( 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 ( ( 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
v < 0
;
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;
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;
verum end; case
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))))) )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 ( ( 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
;
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;
verum end; case
v < 0
;
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;
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;
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))))) )
;
verum end; case A51:
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))))) ) )
(- (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)))
;
( 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 ( ( 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
u < 0
;
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;
verum end; end; end; now ( ( 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)
;
( 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 ( ( 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
v < 0
;
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;
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;
verum end; case A78:
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)))))
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 ( ( 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
v < 0
;
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;
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;
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))))) )
;
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))))) )
; verum