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₁[ Nat] means a |^ (1 + $1) <= a;
A5: a * a <= a * 1 by A1, A2, XREAL_1:64;
A6: for m1 being Nat st S₁[m1] holds
S₁[m1 + 1]

proof

let m1 be Nat; :: thesis: ( S₁[m1] implies S₁[m1 + 1] )
assume a |^ (1 + m1) <= a ; :: thesis: S₁[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₁[m1 + 1] by A5, XXREAL_0:2; :: thesis: verum

end;

A7: S₁[ 0 ] ;
A8: for m1 being Nat holds S₁[m1] from NAT_1:sch 2(A7, A6);
thus a |^ n <= a by A4, A8; :: thesis: verum