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_{1}[ 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_{1}[k] holds

S_{1}[k + 1]

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

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_{1}[ 0 ]
_{1}[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

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

f . j > x ) holds

(Product f) * y2 > x;

A4: for k being Nat st S

S

proof

len ps in Seg (len ps)
by FINSEQ_1:3;
let k be Nat; :: thesis: ( S_{1}[k] implies S_{1}[k + 1] )

assume A5: S_{1}[k]
; :: thesis: S_{1}[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

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;assume A5: S

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

Product f = (Product f1) * m
by A8, RVSUM_1:96;
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;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

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

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

A21:
len q = len q
;
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;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

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

proof

for k being Nat holds S
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;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

then (Product q) * y2 > x by A18, A21;

hence Product ps > x by A3, RVSUM_1:96; :: thesis: verum