let c be XFinSequence of REAL ; ex absc being XFinSequence of REAL st
( absc = |.c.| & ( for n being Nat holds (seq_p c) . n <= (seq_p absc) . n ) )
rng |.c.| c= REAL
;
then reconsider absc = |.c.| as XFinSequence of REAL by RELAT_1:def 19;
take
absc
; ( absc = |.c.| & ( for n being Nat holds (seq_p c) . n <= (seq_p absc) . n ) )
thus
absc = |.c.|
; for n being Nat holds (seq_p c) . n <= (seq_p absc) . n
let n be Nat; (seq_p c) . n <= (seq_p absc) . n
CL1:
(seq_p c) . n = Sum (c (#) (seq_a^ (n,1,0)))
by defseqp;
CL2:
(seq_p absc) . n = Sum (absc (#) (seq_a^ (n,1,0)))
by defseqp;
set mc = c (#) (seq_a^ (n,1,0));
set mac = absc (#) (seq_a^ (n,1,0));
px0:
dom c = dom absc
by VALUED_1:def 11;
dom (c (#) (seq_a^ (n,1,0))) = (dom c) /\ (dom (seq_a^ (n,1,0)))
by VALUED_1:def 4;
then px:
len (c (#) (seq_a^ (n,1,0))) = len (absc (#) (seq_a^ (n,1,0)))
by px0, VALUED_1:def 4;
for x being Nat st x in dom (c (#) (seq_a^ (n,1,0))) holds
(c (#) (seq_a^ (n,1,0))) . x <= (absc (#) (seq_a^ (n,1,0))) . x
proof
let x be
Nat;
( x in dom (c (#) (seq_a^ (n,1,0))) implies (c (#) (seq_a^ (n,1,0))) . x <= (absc (#) (seq_a^ (n,1,0))) . x )
CCL1:
(c (#) (seq_a^ (n,1,0))) . x = (c . x) * ((seq_a^ (n,1,0)) . x)
by VALUED_1:5;
CCL2:
(absc (#) (seq_a^ (n,1,0))) . x = (absc . x) * ((seq_a^ (n,1,0)) . x)
by VALUED_1:5;
PX2:
(seq_a^ (n,1,0)) . x =
n to_power ((1 * x) + 0)
by ASYMPT_1:def 1
.=
n to_power x
;
absc . x = |.(c . x).|
by VALUED_1:18;
hence
(
x in dom (c (#) (seq_a^ (n,1,0))) implies
(c (#) (seq_a^ (n,1,0))) . x <= (absc (#) (seq_a^ (n,1,0))) . x )
by XREAL_1:64, CCL1, CCL2, ABSVALUE:4, PX2;
verum
end;
hence
(seq_p c) . n <= (seq_p absc) . n
by CL1, CL2, AFINSQ_2:57, px; verum