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 object such that
A3: ps = ps1 ^ <*y*> by FINSEQ_1:46;
<*y*> is FinSequence of REAL by A3, FINSEQ_1:36;
then rng <*y*> c= REAL by FINSEQ_1:def 4;
then {y} c= REAL by FINSEQ_1:38;
then reconsider y2 = y as Element of REAL by ZFMISC_1:31;
defpred S₁[ 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 Nat st S₁[k] holds
S₁[k + 1]

proof

let k be 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 object such that
A8: f = v ^ <*w*> by FINSEQ_1:46;
reconsider f1 = v, f2 = <*w*> as FinSequence of REAL by A8, FINSEQ_1:36;
rng f2 c= REAL ;
then {w} c= REAL by FINSEQ_1:38;
then reconsider m = w as Element of REAL by ZFMISC_1:31;
k + 1 = (len f1) + (len f2) by A6, A8, FINSEQ_1:22;
then A9: k + 1 = (len f1) + 1 by FINSEQ_1:39;
then A10: f . (len f) = m by A6, A8, FINSEQ_1:42;
len f in Seg (len f) by A6, FINSEQ_1:3;
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:155;
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:26;
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:96;
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:68;
hence (Product f) * y2 > x by A12, XXREAL_0:2; :: thesis: verum

end;

len ps in Seg (len ps) by FINSEQ_1:3;
then A17: len ps in dom ps by FINSEQ_1:def 3;
reconsider q = ps1 as FinSequence of REAL by A3, FINSEQ_1:36;
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:26;
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:22;
then len ps = (len ps1) + 1 by FINSEQ_1:39;
then A22: ps . (len ps) = y2 by A3, FINSEQ_1:42;
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:94;
hence (Product f) * y2 > x by A2, A22, A17; :: thesis: verum

end;

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