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 that
A1: x >= 1 and
A2: 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;
<*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;
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;
A4: 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 A5: 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
A6: len f = k + 1 and
A7: for j being Element of NAT st j in dom f holds
f . j > x ; :: thesis: (Product f) * y2 > x
f <> {} by A6;
then consider v being FinSequence, w being set such that
A8: f = v ^ <*w*> by FINSEQ_1:63;
reconsider f1 = v, f2 = <*w*> as FinSequence of REAL by A8, FINSEQ_1:50;
rng f2 c= REAL ;
then {w} c= REAL by FINSEQ_1:55;
then reconsider m = w as Real by ZFMISC_1:37;
k + 1 = (len f1) + (len f2) by A6, A8, FINSEQ_1:35;
then A9: k + 1 = (len f1) + 1 by FINSEQ_1:56;
then A10: f . (len f) = m by A6, A8, FINSEQ_1:59;
len f in Seg (len f) by A6, FINSEQ_1:5;
then A11: len f in dom f by FINSEQ_1:def 3;
then m > 1 by A1, A7, A10, XXREAL_0:2;
then A12: x * m > x by A1, XREAL_1:157;
A13: for j being Element of NAT st j in dom f1 holds
f1 . j > x

proof

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

end;

Product f = (Product f1) * m by A8, RVSUM_1:126;
then A16: (Product f) * y2 = ((Product f1) * y2) * m ;
m > x by A7, A10, A11;
then (Product f) * y2 > x * m by A1, A5, A9, A13, A16, XREAL_1:70;
hence (Product f) * y2 > x by A12, XXREAL_0:2; :: thesis: verum

end;

len ps in Seg (len ps) by FINSEQ_1:5;
then A17: len ps in dom ps by FINSEQ_1:def 3;
reconsider q = ps1 as FinSequence of REAL by A3, FINSEQ_1:50;
A18: for j being Element of NAT st j in dom q holds
q . j > x

proof

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

end;

A21: len q = len q ;
len ps = (len ps1) + (len <*y*>) by A3, FINSEQ_1:35;
then len ps = (len ps1) + 1 by FINSEQ_1:56;
then A22: ps . (len ps) = y2 by A3, FINSEQ_1:59;
A23: 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
A24: len f = 0 and
for j being Element of NAT st j in dom f holds
f . j > x ; :: thesis: (Product f) * y2 > x
f = <*> REAL by A24;
then Product f = 1 by RVSUM_1:124;
hence (Product f) * y2 > x by A2, A22, A17; :: thesis: verum

end;

for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A23, A4);
then (Product q) * y2 > x by A18, A21;
hence Product ps > x by A3, RVSUM_1:126; :: thesis: verum