let z be Complex; ( Re (z ^3) = ((Re z) |^ 3) - ((3 * (Re z)) * ((Im z) ^2)) & Im (z ^3) = (- ((Im z) |^ 3)) + ((3 * ((Re z) ^2)) * (Im z)) )
set x = Re z;
set y = Im z;
(Re z) + ((Im z) * <i>) = z
by COMPLEX1:13;
then z ^3 =
(((Re ((((Re z) ^2) - ((Im z) ^2)) + ((2 * ((Re z) * (Im z))) * <i>))) * (Re ((Re z) + ((Im z) * <i>)))) - ((Im ((((Re z) ^2) - ((Im z) ^2)) + ((2 * ((Re z) * (Im z))) * <i>))) * (Im ((Re z) + ((Im z) * <i>))))) + ((((Re ((((Re z) ^2) - ((Im z) ^2)) + ((2 * ((Re z) * (Im z))) * <i>))) * (Im ((Re z) + ((Im z) * <i>)))) + ((Re ((Re z) + ((Im z) * <i>))) * (Im ((((Re z) ^2) - ((Im z) ^2)) + ((2 * ((Re z) * (Im z))) * <i>))))) * <i>)
by COMPLEX1:82
.=
(((((Re z) ^2) - ((Im z) ^2)) * (Re ((Re z) + ((Im z) * <i>)))) - ((Im ((((Re z) ^2) - ((Im z) ^2)) + ((2 * ((Re z) * (Im z))) * <i>))) * (Im ((Re z) + ((Im z) * <i>))))) + ((((Re ((((Re z) ^2) - ((Im z) ^2)) + ((2 * ((Re z) * (Im z))) * <i>))) * (Im ((Re z) + ((Im z) * <i>)))) + ((Re ((Re z) + ((Im z) * <i>))) * (Im ((((Re z) ^2) - ((Im z) ^2)) + ((2 * ((Re z) * (Im z))) * <i>))))) * <i>)
by COMPLEX1:12
.=
(((((Re z) ^2) - ((Im z) ^2)) * (Re ((Re z) + ((Im z) * <i>)))) - ((2 * ((Re z) * (Im z))) * (Im ((Re z) + ((Im z) * <i>))))) + ((((Re ((((Re z) ^2) - ((Im z) ^2)) + ((2 * ((Re z) * (Im z))) * <i>))) * (Im ((Re z) + ((Im z) * <i>)))) + ((Re ((Re z) + ((Im z) * <i>))) * (Im ((((Re z) ^2) - ((Im z) ^2)) + ((2 * ((Re z) * (Im z))) * <i>))))) * <i>)
by COMPLEX1:12
.=
(((((Re z) ^2) - ((Im z) ^2)) * (Re ((Re z) + ((Im z) * <i>)))) - ((2 * ((Re z) * (Im z))) * (Im ((Re z) + ((Im z) * <i>))))) + ((((((Re z) ^2) - ((Im z) ^2)) * (Im ((Re z) + ((Im z) * <i>)))) + ((Re ((Re z) + ((Im z) * <i>))) * (Im ((((Re z) ^2) - ((Im z) ^2)) + ((2 * ((Re z) * (Im z))) * <i>))))) * <i>)
by COMPLEX1:12
.=
(((((Re z) ^2) - ((Im z) ^2)) * (Re ((Re z) + ((Im z) * <i>)))) - ((2 * ((Re z) * (Im z))) * (Im ((Re z) + ((Im z) * <i>))))) + ((((((Re z) ^2) - ((Im z) ^2)) * (Im ((Re z) + ((Im z) * <i>)))) + ((Re ((Re z) + ((Im z) * <i>))) * (2 * ((Re z) * (Im z))))) * <i>)
by COMPLEX1:12
.=
(((((Re z) ^2) - ((Im z) ^2)) * (Re z)) - ((2 * ((Re z) * (Im z))) * (Im ((Re z) + ((Im z) * <i>))))) + ((((((Re z) ^2) - ((Im z) ^2)) * (Im ((Re z) + ((Im z) * <i>)))) + ((Re ((Re z) + ((Im z) * <i>))) * (2 * ((Re z) * (Im z))))) * <i>)
by COMPLEX1:12
.=
(((((Re z) ^2) - ((Im z) ^2)) * (Re z)) - ((2 * ((Re z) * (Im z))) * (Im z))) + ((((((Re z) ^2) - ((Im z) ^2)) * (Im ((Re z) + ((Im z) * <i>)))) + ((Re ((Re z) + ((Im z) * <i>))) * (2 * ((Re z) * (Im z))))) * <i>)
by COMPLEX1:12
.=
(((((Re z) ^2) - ((Im z) ^2)) * (Re z)) - ((2 * ((Re z) * (Im z))) * (Im z))) + ((((((Re z) ^2) - ((Im z) ^2)) * (Im z)) + ((Re ((Re z) + ((Im z) * <i>))) * (2 * ((Re z) * (Im z))))) * <i>)
by COMPLEX1:12
.=
((((((Re z) ^2) * (Re z)) - (((Im z) ^2) * (Re z))) + (0 * (Re z))) - ((2 * ((Re z) * (Im z))) * (Im z))) + (((((((Re z) ^2) - ((Im z) ^2)) + 0) * (Im z)) + ((Re z) * (2 * ((Re z) * (Im z))))) * <i>)
by COMPLEX1:12
.=
((((((Re z) |^ 1) * (Re z)) * (Re z)) - (((Im z) ^2) * (Re z))) - ((2 * ((Re z) * (Im z))) * (Im z))) + ((((((Re z) ^2) * (Im z)) - (((Im z) ^2) * (Im z))) + ((Re z) * (2 * ((Re z) * (Im z))))) * <i>)
.=
(((((Re z) |^ (1 + 1)) * (Re z)) - (((Im z) ^2) * (Re z))) - ((2 * ((Re z) * (Im z))) * (Im z))) + ((((((Re z) ^2) * (Im z)) - (((Im z) ^2) * (Im z))) + ((Re z) * (2 * ((Re z) * (Im z))))) * <i>)
by NEWTON:6
.=
((((Re z) |^ (2 + 1)) - (((Im z) ^2) * (Re z))) - ((2 * ((Re z) * (Im z))) * (Im z))) + ((((((Re z) ^2) * (Im z)) - (((Im z) ^2) * (Im z))) + ((Re z) * (2 * ((Re z) * (Im z))))) * <i>)
by NEWTON:6
.=
((((Re z) |^ 3) - (((Im z) ^2) * (Re z))) - ((2 * ((Re z) * (Im z))) * (Im z))) + ((((((Re z) ^2) * (Im z)) - ((((Im z) |^ 1) * (Im z)) * (Im z))) + ((Re z) * (2 * ((Re z) * (Im z))))) * <i>)
.=
((((Re z) |^ 3) - (((Im z) ^2) * (Re z))) - ((2 * ((Re z) * (Im z))) * (Im z))) + ((((((Re z) ^2) * (Im z)) - (((Im z) |^ (1 + 1)) * (Im z))) + ((Re z) * (2 * ((Re z) * (Im z))))) * <i>)
by NEWTON:6
.=
((((Re z) |^ 3) - (((Im z) ^2) * (Re z))) - (2 * ((Re z) * ((Im z) * (Im z))))) + ((((((Re z) ^2) * (Im z)) - ((Im z) |^ (2 + 1))) + ((Re z) * (2 * ((Re z) * (Im z))))) * <i>)
by NEWTON:6
.=
(((Re z) |^ 3) - ((3 * (Re z)) * ((Im z) ^2))) + (((- ((Im z) |^ 3)) + ((3 * ((Re z) ^2)) * (Im z))) * <i>)
;
hence
( Re (z ^3) = ((Re z) |^ 3) - ((3 * (Re z)) * ((Im z) ^2)) & Im (z ^3) = (- ((Im z) |^ 3)) + ((3 * ((Re z) ^2)) * (Im z)) )
by COMPLEX1:12; verum