let r be Real; for n being Nat st 0 < n & 1 < r holds
1 < r |^ n
let n be Nat; ( 0 < n & 1 < r implies 1 < r |^ n )
assume that
A1:
0 < n
and
A2:
r > 1
; 1 < r |^ n
defpred S1[ Nat] means ( 0 < $1 implies 1 < r |^ $1 );
A3:
for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be
Nat;
( S1[k] implies S1[k + 1] )
assume that A4:
S1[
k]
and
0 < k + 1
;
1 < r |^ (k + 1)
end;
A5:
S1[ 0 ]
;
for k being Nat holds S1[k]
from NAT_1:sch 2(A5, A3);
hence
1 < r |^ n
by A1; verum