let r be real number ; :: thesis: for n being natural number st 0 < n & 1 < r holds
1 < r |^ n
let n be natural number ; :: thesis: ( 0 < n & 1 < r implies 1 < r |^ n )
assume that
A1: 0 < n and
A2: r > 1 ; :: thesis: 1 < r |^ n
defpred S₁[ natural number ] means ( 0 < $1 implies 1 < r |^ $1 );
A3: S₁[ 0 ] ;
A4: for k being natural number st S₁[k] holds
S₁[k + 1]

proof

let k be natural number ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume that
A5: S₁[k] and
0 < k + 1 ; :: thesis: 1 < r |^ (k + 1)

per cases ( k > 0 or k = 0 ) ;

suppose A6: k > 0 ; :: thesis: 1 < r |^ (k + 1)

A7: r |^ (k + 1) = (r |^ k) * r by NEWTON:11;
1 * r <= (r |^ k) * r by A2, A5, A6, XREAL_1:66;
hence 1 < r |^ (k + 1) by A2, A7, XXREAL_0:2; :: thesis: verum

end;

suppose k = 0 ; :: thesis: 1 < r |^ (k + 1)

hence 1 < r |^ (k + 1) by A2, NEWTON:10; :: thesis: verum

end;

end;

end;

for k being natural number holds S₁[k] from NAT_1:sch 2(A3, A4);
hence 1 < r |^ n by A1; :: thesis: verum