let ps be non empty FinSequence of REAL ; :: thesis: for x being Real st x >= 1 & ( for i being Element of NAT st i in dom ps holds
ps . i > x ) holds
Product ps > x
let x be Real; :: thesis: ( x >= 1 & ( for i being Element of NAT st i in dom ps holds
ps . i > x ) implies Product ps > x )
assume A1: ( x >= 1 & ( for j being Element of NAT st j in dom ps holds
ps . j > x ) ) ; :: thesis: Product ps > x
consider ps1 being FinSequence, y being set such that
A3: ps = ps1 ^ <*y*> by FINSEQ_1:63;
len ps = (len ps1) + (len <*y*>) by A3, FINSEQ_1:35;
then A4: len ps = (len ps1) + 1 by FINSEQ_1:56;
<*y*> is FinSequence of REAL by A3, FINSEQ_1:50;
then rng <*y*> c= REAL by FINSEQ_1:def 4;
then {y} c= REAL by FINSEQ_1:55;
then reconsider y2 = y as Real by ZFMISC_1:37;
A5: ps . (len ps) = y2 by A3, A4, FINSEQ_1:59;
len ps in Seg (len ps) by FINSEQ_1:5;
then A6: len ps in dom ps by FINSEQ_1:def 3;
reconsider q = ps1 as FinSequence of REAL by A3, FINSEQ_1:50;
A7: for j being Element of NAT st j in dom q holds
q . j > x

proof

let j be Element of NAT ; :: thesis: ( j in dom q implies q . j > x )
assume A8: j in dom q ; :: thesis: q . j > x
A9: dom q c= dom ps by A3, FINSEQ_1:39;
ps . j = q . j by A3, A8, FINSEQ_1:def 7;
hence q . j > x by A1, A8, A9; :: thesis: verum

end;

defpred S₁[ Element of NAT ] means for f being FinSequence of REAL st len f = $1 & ( for j being Element of NAT st j in dom f holds
f . j > x ) holds
(Product f) * y2 > x;
A10: S₁[ 0 ]

proof

let f be FinSequence of REAL ; :: thesis: ( len f = 0 & ( for j being Element of NAT st j in dom f holds
f . j > x ) implies (Product f) * y2 > x )
assume that
A11: len f = 0 and
for j being Element of NAT st j in dom f holds
f . j > x ; :: thesis: (Product f) * y2 > x
Product f = 1 by A11, FINSEQ_1:32, RVSUM_1:124;
hence (Product f) * y2 > x by A1, A5, A6; :: thesis: verum

end;

A12: for k being Element of NAT st S₁[k] holds
S₁[k + 1]

proof

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A13: S₁[k] ; :: thesis: S₁[k + 1]
let f be FinSequence of REAL ; :: thesis: ( len f = k + 1 & ( for j being Element of NAT st j in dom f holds
f . j > x ) implies (Product f) * y2 > x )
assume that
A14: len f = k + 1 and
A15: for j being Element of NAT st j in dom f holds
f . j > x ; :: thesis: (Product f) * y2 > x
f <> {} by A14;
then consider v being FinSequence, w being set such that
A16: f = v ^ <*w*> by FINSEQ_1:63;
reconsider f1 = v, f2 = <*w*> as FinSequence of REAL by A16, FINSEQ_1:50;
k + 1 = (len f1) + (len f2) by A14, A16, FINSEQ_1:35;
then A17: k + 1 = (len f1) + 1 by FINSEQ_1:56;
B20: for j being Element of NAT st j in dom f1 holds
f1 . j > x

proof

let j be Element of NAT ; :: thesis: ( j in dom f1 implies f1 . j > x )
assume A18: j in dom f1 ; :: thesis: f1 . j > x
A19: dom f1 c= dom f by A16, FINSEQ_1:39;
f . j = f1 . j by A16, A18, FINSEQ_1:def 7;
hence f1 . j > x by A15, A18, A19; :: thesis: verum

end;

rng f2 c= REAL ;
then {w} c= REAL by FINSEQ_1:55;
then reconsider m = w as Real by ZFMISC_1:37;
A21: f . (len f) = m by A14, A16, A17, FINSEQ_1:59;
len f in Seg (len f) by A14, FINSEQ_1:5;
then B22: len f in dom f by FINSEQ_1:def 3;
then A22: m > x by A15, A21;
m > 1 by A1, A15, A21, B22, XXREAL_0:2;
then A23: x * m > x by A1, XREAL_1:157;
Product f = (Product f1) * m by A16, RVSUM_1:126;
then (Product f) * y2 = ((Product f1) * y2) * m ;
then (Product f) * y2 > x * m by A1, B20, A22, A13, A17, XREAL_1:70;
hence (Product f) * y2 > x by A23, XXREAL_0:2; :: thesis: verum

end;

A24: for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A10, A12);
len q = len q ;
then (Product q) * y2 > x by A7, A24;
hence Product ps > x by A3, RVSUM_1:126; :: thesis: verum