let a be real number ; :: thesis: for n being Element of NAT st ( a >= 0 or n is even ) holds
a |^ n >= 0
let n be Element of NAT ; :: thesis: ( ( a >= 0 or n is even ) implies a |^ n >= 0 )
assume A1: ( a >= 0 or n is even ) ; :: thesis: a |^ n >= 0

A2: now

let a be real number ; :: thesis: for n being Element of NAT st a >= 0 holds
a |^ n >= 0
let n be Element of NAT ; :: thesis: ( a >= 0 implies a |^ n >= 0 )
assume A3: a >= 0 ; :: thesis: a |^ n >= 0

now

per cases ( a > 0 or a = 0 ) by A3;

suppose a > 0 ; :: thesis: a |^ n >= 0

hence a |^ n >= 0 by PREPOWER:13; :: thesis: verum

end;

suppose A6: a = 0 ; :: thesis: a |^ n >= 0

now

per cases ( n = 0 or ex m being Nat st n = m + 1 ) by NAT_1:6;

suppose A8: n = 0 ; :: thesis: a |^ n >= 0

a |^ n = (a GeoSeq ) . n by PREPOWER:def 1
.= 1 by A8, PREPOWER:4 ;
hence a |^ n >= 0 ; :: thesis: verum

end;

suppose A10: ex m being Nat st n = m + 1 ; :: thesis: a |^ n >= 0

consider m being Nat such that
A11: n = m + 1 by A10;
a |^ n = (a |^ m) * a by A11, NEWTON:11
.= 0 by A6 ;
hence a |^ n >= 0 ; :: thesis: verum

end;

end;

end;

hence a |^ n >= 0 ; :: thesis: verum

end;

end;

end;

hence a |^ n >= 0 ; :: thesis: verum

end;

now

assume A14: n is even ; :: thesis: a |^ n >= 0

now

per cases ( a >= 0 or a < 0 ) ;

suppose a >= 0 ; :: thesis: a |^ n >= 0

hence a |^ n >= 0 by A2; :: thesis: verum

end;

suppose a < 0 ; :: thesis: a |^ n >= 0

then (- a) |^ n >= 0 by A2;
hence a |^ n >= 0 by A14, Th1; :: thesis: verum

end;

end;

end;

hence a |^ n >= 0 ; :: thesis: verum

end;

hence a |^ n >= 0 by A1, A2; :: thesis: verum