let a be Real; :: thesis: for n being Nat st ( a >= 0 or n is even ) holds
a |^ n >= 0
let n be 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 :: thesis: for a being Real
for n being Nat st a >= 0 holds
a |^ n >= 0
let a be Real; :: thesis: for n being Nat st a >= 0 holds
a |^ n >= 0
let n be Nat; :: thesis: ( a >= 0 implies a |^ n >= 0 )
assume A3: a >= 0 ; :: thesis: a |^ n >= 0
now :: thesis: a |^ n >= 0
per cases ( a > 0 or a = 0 ) by A3;
suppose A4: a = 0 ; :: thesis: a |^ n >= 0
now :: thesis: a |^ n >= 0
per cases ( n = 0 or ex m being Nat st n = m + 1 ) by NAT_1:6;
suppose A5: n = 0 ; :: thesis: a |^ n >= 0
a |^ n = (a GeoSeq) . n by PREPOWER:def 1
.= 1 by A5, PREPOWER:3 ;
hence a |^ n >= 0 ; :: thesis: verum
end;
suppose ex m being Nat st n = m + 1 ; :: thesis: a |^ n >= 0
then consider m being Nat such that
A6: n = m + 1 ;
a |^ n = (a |^ m) * a by A6, NEWTON:6
.= 0 by A4 ;
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 :: thesis: ( n is even implies a |^ n >= 0 )
assume A7: n is even ; :: thesis: a |^ n >= 0
now :: thesis: a |^ n >= 0
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 A7, Th1; :: thesis: verum
end;
end;
end;
hence a |^ n >= 0 ; :: thesis: verum
end;
hence a |^ n >= 0 by A1, A2; :: thesis: verum