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

proof

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

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

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

then ( r |^ (k + 1) = (r |^ k) * r & 1 * r <= (r |^ k) * r ) by A2, A4, NEWTON:6, XREAL_1:64;
hence 1 < r |^ (k + 1) by A2, XXREAL_0:2; :: thesis: verum

end;

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

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

end;

end;

end;

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