let a be Real; :: thesis: for n being natural Number st 1 <= a & 1 <= n holds

a <= a |^ n

let n be natural Number ; :: thesis: ( 1 <= a & 1 <= n implies a <= a |^ n )

assume that

A1: 1 <= a and

A2: 1 <= n ; :: thesis: a <= a |^ n

consider m being Nat such that

A3: n = m + 1 by A2, NAT_1:6;

defpred S_{1}[ Nat] means a <= a |^ ($1 + 1);

A4: for m1 being Nat st S_{1}[m1] holds

S_{1}[m1 + 1]
_{1}[ 0 ]
;

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

thus a <= a |^ n by A3, A6; :: thesis: verum

a <= a |^ n

let n be natural Number ; :: thesis: ( 1 <= a & 1 <= n implies a <= a |^ n )

assume that

A1: 1 <= a and

A2: 1 <= n ; :: thesis: a <= a |^ n

consider m being Nat such that

A3: n = m + 1 by A2, NAT_1:6;

defpred S

A4: for m1 being Nat st S

S

proof

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

assume a <= a |^ (m1 + 1) ; :: thesis: S_{1}[m1 + 1]

then a * 1 <= (a |^ (m1 + 1)) * a by A1, XREAL_1:66;

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

end;assume a <= a |^ (m1 + 1) ; :: thesis: S

then a * 1 <= (a |^ (m1 + 1)) * a by A1, XREAL_1:66;

hence S

A6: for m1 being Nat holds S

thus a <= a |^ n by A3, A6; :: thesis: verum