let x be real number ; :: thesis: ( x |^ 3 = (x ^2 ) * x & (x |^ 3) * x = x |^ 4 & (x ^2 ) * (x ^2 ) = x |^ 4 )

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

suppose x = 0 ; :: thesis: ( x |^ 3 = (x ^2 ) * x & (x |^ 3) * x = x |^ 4 & (x ^2 ) * (x ^2 ) = x |^ 4 )

hence ( x |^ 3 = (x ^2 ) * x & (x |^ 3) * x = x |^ 4 & (x ^2 ) * (x ^2 ) = x |^ 4 ) by NEWTON:16; :: thesis: verum

end;

suppose A1: x > 0 ; :: thesis: ( x |^ 3 = (x ^2 ) * x & (x |^ 3) * x = x |^ 4 & (x ^2 ) * (x ^2 ) = x |^ 4 )

x ^2 = x to_power 2 by POWER:53;
then A2: (x ^2 ) * x = (x to_power 2) * (x to_power 1) by POWER:30
.= x to_power (2 + 1) by A1, POWER:32
.= x |^ 3 by POWER:46 ;
(x |^ 3) * x = (x |^ 3) * (x to_power 1) by POWER:30
.= (x to_power 3) * (x to_power 1) ;
then (x |^ 3) * x = x to_power (3 + 1) by A1, POWER:32;
hence ( x |^ 3 = (x ^2 ) * x & (x |^ 3) * x = x |^ 4 & (x ^2 ) * (x ^2 ) = x |^ 4 ) by A2, POWER:46; :: thesis: verum

end;

suppose x < 0 ; :: thesis: ( x |^ 3 = (x ^2 ) * x & (x |^ 3) * x = x |^ 4 & (x ^2 ) * (x ^2 ) = x |^ 4 )

then A3: - x > 0 by XREAL_1:60;
(- x) |^ 3 = (- x) to_power (2 + 1) by POWER:46
.= ((- x) to_power 2) * ((- x) to_power 1) by A3, POWER:32 ;
then A4: (- x) |^ 3 = ((- x) to_power 2) * (- x) by POWER:30;
A5: (- x) to_power 2 = (- x) ^2 by POWER:53
.= x ^2 ;
3 = (2 * 1) + 1 ;
then ((- x) |^ 3) + (x |^ 3) = - ((x |^ 3) + (- (x |^ 3))) by POWER:2
.= (x |^ 3) - (x |^ 3) ;
then A6: (x |^ 3) + (((- x) |^ 3) - ((- x) |^ 3)) = 0 - ((- x) |^ 3) ;
(- x) |^ 4 = x |^ 4 by Lm1, POWER:1;
then x |^ 4 = (- x) to_power (3 + 1) by POWER:46
.= ((- x) to_power 3) * ((- x) to_power 1) by A3, POWER:32
.= ((- x) |^ 3) * ((- x) to_power 1) ;
then x |^ 4 = ((- x) |^ 3) * (- x) by POWER:30
.= (x ^2 ) * (x * x) by A4, A5 ;
hence ( x |^ 3 = (x ^2 ) * x & (x |^ 3) * x = x |^ 4 & (x ^2 ) * (x ^2 ) = x |^ 4 ) by A4, A5, A6; :: thesis: verum

end;

end;