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

a |^ n <= a

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

assume that

A1: 0 < a and

A2: a <= 1 and

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

consider m being Nat such that

A4: n = 1 + m by A3, NAT_1:10;

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

A5: a * a <= a * 1 by A1, A2, XREAL_1:64;

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

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

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

thus a |^ n <= a by A4, A8; :: thesis: verum

a |^ n <= a

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

assume that

A1: 0 < a and

A2: a <= 1 and

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

consider m being Nat such that

A4: n = 1 + m by A3, NAT_1:10;

defpred S

A5: a * a <= a * 1 by A1, A2, XREAL_1:64;

A6: for m1 being Nat st S

S

proof

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

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

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

then a |^ (1 + (m1 + 1)) <= a * a by NEWTON:6;

hence S_{1}[m1 + 1]
by A5, XXREAL_0:2; :: thesis: verum

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

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

then a |^ (1 + (m1 + 1)) <= a * a by NEWTON:6;

hence S

A8: for m1 being Nat holds S

thus a |^ n <= a by A4, A8; :: thesis: verum