set g = seq_a^ (2,1,1);
set f = seq_a^ (2,1,0);
set h = (seq_a^ (2,1,0)) /" (seq_a^ (2,1,1));
reconsider f = seq_a^ (2,1,0) as eventually-positive Real_Sequence ;
reconsider g = seq_a^ (2,1,1) as eventually-positive Real_Sequence ;
take f ; :: thesis: ex s1 being eventually-positive Real_Sequence st
( f = seq_a^ (2,1,0) & s1 = seq_a^ (2,1,1) & Big_Oh f = Big_Oh s1 )
take g ; :: thesis: ( f = seq_a^ (2,1,0) & g = seq_a^ (2,1,1) & Big_Oh f = Big_Oh g )
thus ( f = seq_a^ (2,1,0) & g = seq_a^ (2,1,1) ) ; :: thesis: Big_Oh f = Big_Oh g
A1: now :: thesis: for n being Element of NAT holds ((seq_a^ (2,1,0)) /" (seq_a^ (2,1,1))) . n = 2 "
let n be Element of NAT ; :: thesis: ((seq_a^ (2,1,0)) /" (seq_a^ (2,1,1))) . n = 2 "
A2: g . n = 2 to_power ((1 * n) + 1) by Def1;
f . n = 2 to_power ((1 * n) + 0) by Def1;
then ((seq_a^ (2,1,0)) /" (seq_a^ (2,1,1))) . n = (2 to_power n) / (g . n) by Lm4
.= 2 to_power (n - (n + 1)) by A2, POWER:29
.= 2 to_power (0 + (- 1))
.= 1 / (2 to_power 1) by POWER:28
.= 1 / 2 by POWER:25
.= 2 " ;
hence ((seq_a^ (2,1,0)) /" (seq_a^ (2,1,1))) . n = 2 " ; :: thesis: verum
end;
A3: now :: thesis: for p being Real st p > 0 holds
ex N being Nat st
for n being Nat st n >= N holds
|.((((seq_a^ (2,1,0)) /" (seq_a^ (2,1,1))) . n) - (2 ")).| < p
let p be Real; :: thesis: ( p > 0 implies ex N being Nat st
for n being Nat st n >= N holds
|.((((seq_a^ (2,1,0)) /" (seq_a^ (2,1,1))) . n) - (2 ")).| < p )
assume A4: p > 0 ; :: thesis: ex N being Nat st
for n being Nat st n >= N holds
|.((((seq_a^ (2,1,0)) /" (seq_a^ (2,1,1))) . n) - (2 ")).| < p
reconsider N = 0 as Nat ;
take N = N; :: thesis: for n being Nat st n >= N holds
|.((((seq_a^ (2,1,0)) /" (seq_a^ (2,1,1))) . n) - (2 ")).| < p
let n be Nat; :: thesis: ( n >= N implies |.((((seq_a^ (2,1,0)) /" (seq_a^ (2,1,1))) . n) - (2 ")).| < p )
A5: n in NAT by ORDINAL1:def 12;
assume n >= N ; :: thesis: |.((((seq_a^ (2,1,0)) /" (seq_a^ (2,1,1))) . n) - (2 ")).| < p
|.((((seq_a^ (2,1,0)) /" (seq_a^ (2,1,1))) . n) - (2 ")).| = |.((2 ") - (2 ")).| by A1, A5
.= 0 by ABSVALUE:2 ;
hence |.((((seq_a^ (2,1,0)) /" (seq_a^ (2,1,1))) . n) - (2 ")).| < p by A4; :: thesis: verum
end;
then A6: (seq_a^ (2,1,0)) /" (seq_a^ (2,1,1)) is convergent by SEQ_2:def 6;
then lim ((seq_a^ (2,1,0)) /" (seq_a^ (2,1,1))) > 0 by A3, SEQ_2:def 7;
hence Big_Oh f = Big_Oh g by A6, ASYMPT_0:15; :: thesis: verum