let n be Nat; :: thesis: for a being Real st 1 < a holds
a to_power n < a to_power (n + 1)
let a be Real; :: thesis: ( 1 < a implies a to_power n < a to_power (n + 1) )
assume AS: 1 < a ; :: thesis: a to_power n < a to_power (n + 1)
LP3: a to_power (n + 1) = (a to_power n) * (a to_power 1) by FIB_NUM2:5
.= (a to_power n) * a by POWER:25 ;
a to_power n > 0 by POWER:34, AS;
then 1 * (a to_power n) < (a to_power n) * a by XREAL_1:68, AS;
hence a to_power n < a to_power (n + 1) by LP3; :: thesis: verum