let x be Real; :: 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:11; :: 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 |^ 3) * x = (x |^ 3) * (x to_power 1)
.= (x to_power 3) * (x to_power 1) ;
then A2: (x |^ 3) * x = x to_power (3 + 1) by A1, POWER:27;
x ^2 = x to_power 2 by POWER:46;
then (x ^2) * x = (x to_power 2) * (x to_power 1)
.= x to_power (2 + 1) by A1, POWER:27
.= x |^ 3 by POWER:41 ;
hence ( x |^ 3 = (x ^2) * x & (x |^ 3) * x = x |^ 4 & (x ^2) * (x ^2) = x |^ 4 ) by A2, POWER:41; :: 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:58;
((- x) |^ 3) + (x |^ 3) = - ((x |^ 3) + (- (x |^ 3))) by Lm2, POWER:2
.= (x |^ 3) - (x |^ 3) ;
then A4: (x |^ 3) + (((- x) |^ 3) - ((- x) |^ 3)) = 0 - ((- x) |^ 3) ;
A5: (- x) to_power 2 = (- x) ^2 by POWER:46
.= x ^2 ;
(- x) |^ 3 = (- x) to_power (2 + 1) by POWER:41
.= ((- x) to_power 2) * ((- x) to_power 1) by A3, POWER:27 ;
then A6: (- x) |^ 3 = ((- x) to_power 2) * (- x) ;
(- x) |^ 4 = x |^ 4 by Lm1, POWER:1;
then x |^ 4 = (- x) to_power (3 + 1) by POWER:41
.= ((- x) to_power 3) * ((- x) to_power 1) by A3, POWER:27
.= ((- x) |^ 3) * ((- x) to_power 1) ;
then x |^ 4 = ((- x) |^ 3) * (- x)
.= (x ^2) * (x * x) by A6, A5 ;
hence ( x |^ 3 = (x ^2) * x & (x |^ 3) * x = x |^ 4 & (x ^2) * (x ^2) = x |^ 4 ) by A6, A5, A4; :: thesis: verum
end;
end;