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

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
A4: m |^ (n + 1) = (m |^ n) * (m |^ 1) by NEWTON:8
.= (m |^ n) * m ;
assume A5: S₁[n] ; :: thesis: S₁[n + 1]
S₁[n + 1]

proof

now :: thesis: S₁[n + 1]

per cases ( n = 0 or n <> 0 ) ;

suppose n = 0 ; :: thesis: S₁[n + 1]

hence S₁[n + 1] by A1; :: thesis: verum

end;

suppose n <> 0 ; :: thesis: S₁[n + 1]

then (m |^ n) * m > 1 * m by A1, A5, XREAL_1:68;
hence S₁[n + 1] by A1, A4, XXREAL_0:2; :: thesis: verum

end;

end;

end;

hence S₁[n + 1] ; :: thesis: verum

end;

hence S₁[n + 1] ; :: thesis: verum

end;

A6: S₁[ 0 ] ;
for n being Nat holds S₁[n] from NAT_1:sch 2(A6, A3);
hence m |^ n > 1 by A2; :: thesis: verum