let z be Element of COMPLEX ; :: thesis: ( Re (z ^3 ) = ((Re z) |^ 3) - ((3 * (Re z)) * ((Im z) ^2 )) & Im (z ^3 ) = (- ((Im z) |^ 3)) + ((3 * ((Re z) ^2 )) * (Im z)) )
A1: (Re z) + ((Im z) * <i> ) = z by COMPLEX1:29;
set x = Re z;
set y = Im z;
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 A1, COMPLEX1:def 10
.= (((((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:28
.= (((((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:28
.= (((((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:28
.= (((((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:28
.= (((((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:28
.= (((((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:28
.= (((((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:28
.= ((((((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:28
.= ((((((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> ) by NEWTON:10
.= (((((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:11
.= ((((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:11
.= ((((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> ) by NEWTON:10
.= ((((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:11
.= ((((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:11
.= (((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:28; :: thesis: verum