let a be Real; :: thesis: ( 1 < a implies seq_a^ (a,1,0) is V49() )

assume AS: 1 < a ; :: thesis: seq_a^ (a,1,0) is V49()

C1: for n being Element of NAT holds (seq_a^ (a,1,0)) . n < (seq_a^ (a,1,0)) . (n + 1)

for n being Nat holds S . n < S . (n + 1)

assume AS: 1 < a ; :: thesis: seq_a^ (a,1,0) is V49()

C1: for n being Element of NAT holds (seq_a^ (a,1,0)) . n < (seq_a^ (a,1,0)) . (n + 1)

proof

reconsider S = seq_a^ (a,1,0) as Real_Sequence ;
let n be Element of NAT ; :: thesis: (seq_a^ (a,1,0)) . n < (seq_a^ (a,1,0)) . (n + 1)

L2: (seq_a^ (a,1,0)) . n = a to_power ((1 * n) + 0) by ASYMPT_1:def 1

.= a to_power n ;

(seq_a^ (a,1,0)) . (n + 1) = a to_power ((1 * (n + 1)) + 0) by ASYMPT_1:def 1

.= a to_power (n + 1) ;

hence (seq_a^ (a,1,0)) . n < (seq_a^ (a,1,0)) . (n + 1) by L2, LC5aa, AS; :: thesis: verum

end;L2: (seq_a^ (a,1,0)) . n = a to_power ((1 * n) + 0) by ASYMPT_1:def 1

.= a to_power n ;

(seq_a^ (a,1,0)) . (n + 1) = a to_power ((1 * (n + 1)) + 0) by ASYMPT_1:def 1

.= a to_power (n + 1) ;

hence (seq_a^ (a,1,0)) . n < (seq_a^ (a,1,0)) . (n + 1) by L2, LC5aa, AS; :: thesis: verum

for n being Nat holds S . n < S . (n + 1)

proof

hence
seq_a^ (a,1,0) is V49()
by SEQM_3:def 6; :: thesis: verum
let n be Nat; :: thesis: S . n < S . (n + 1)

reconsider n = n as Element of NAT by ORDINAL1:def 12;

(seq_a^ (a,1,0)) . n < (seq_a^ (a,1,0)) . (n + 1) by C1;

hence S . n < S . (n + 1) ; :: thesis: verum

end;reconsider n = n as Element of NAT by ORDINAL1:def 12;

(seq_a^ (a,1,0)) . n < (seq_a^ (a,1,0)) . (n + 1) by C1;

hence S . n < S . (n + 1) ; :: thesis: verum