let a be Real; :: thesis: for n being natural Number st 0 < a holds

0 < a |^ n

let n be natural Number ; :: thesis: ( 0 < a implies 0 < a |^ n )

A1: n is Nat by TARSKI:1;

defpred S_{1}[ Nat] means 0 < a |^ $1;

assume A2: 0 < a ; :: thesis: 0 < a |^ n

A3: for m being Nat st S_{1}[m] holds

S_{1}[m + 1]
_{1}[ 0 ]
by NEWTON:4;

for m being Nat holds S_{1}[m]
from NAT_1:sch 2(A4, A3);

hence 0 < a |^ n by A1; :: thesis: verum

0 < a |^ n

let n be natural Number ; :: thesis: ( 0 < a implies 0 < a |^ n )

A1: n is Nat by TARSKI:1;

defpred S

assume A2: 0 < a ; :: thesis: 0 < a |^ n

A3: for m being Nat st S

S

proof

A4:
S
let m be Nat; :: thesis: ( S_{1}[m] implies S_{1}[m + 1] )

assume a |^ m > 0 ; :: thesis: S_{1}[m + 1]

then (a |^ m) * a > 0 * a by A2;

hence S_{1}[m + 1]
by NEWTON:6; :: thesis: verum

end;assume a |^ m > 0 ; :: thesis: S

then (a |^ m) * a > 0 * a by A2;

hence S

for m being Nat holds S

hence 0 < a |^ n by A1; :: thesis: verum