let a be real number ; :: thesis: for n being Element of NAT st ( a >= 0 or ex m being Element of NAT st n = 2 * m ) holds
a |^ n >= 0
let n be Element of NAT ; :: thesis: ( ( a >= 0 or ex m being Element of NAT st n = 2 * m ) implies a |^ n >= 0 )
assume A1: ( a >= 0 or ex m being Element of NAT st n = 2 * m ) ; :: 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
A4: now
per cases ( a > 0 or a = 0 ) by A3;
suppose A6: a = 0 ; :: thesis: a |^ n >= 0
A7: 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
A9: a |^ n = (a GeoSeq ) . n by PREPOWER:def 1
.= 1 by A8, PREPOWER:4 ;
thus a |^ n >= 0 by A9; :: 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;
A12: a |^ n = (a |^ m) * a by A11, NEWTON:11
.= 0 by A6 ;
thus a |^ n >= 0 by A12; :: thesis: verum
end;
end;
end;
thus a |^ n >= 0 by A7; :: thesis: verum
end;
end;
end;
thus a |^ n >= 0 by A4; :: thesis: verum
end;
A13: now
assume A14: ex m being Element of NAT st n = 2 * m ; :: thesis: a |^ n >= 0
A15: now
per cases ( a >= 0 or a < 0 ) ;
suppose A17: a < 0 ; :: thesis: a |^ n >= 0
A18: (- a) |^ n >= 0 by A2, A17;
thus a |^ n >= 0 by A14, A18, Th1; :: thesis: verum
end;
end;
end;
thus a |^ n >= 0 by A15; :: thesis: verum
end;
thus a |^ n >= 0 by A1, A2, A13; :: thesis: verum