let a be non negative Real; :: thesis: for f being FinSequence of REAL st ( for k being Nat st k in dom f holds
f . k >= a ) holds
Product f >= a |^ (len f)
let f be FinSequence of REAL ; :: thesis: ( ( for k being Nat st k in dom f holds
f . k >= a ) implies Product f >= a |^ (len f) )
assume A1: for k being Nat st k in dom f holds
f . k >= a ; :: thesis: Product f >= a |^ (len f)
a in REAL by XREAL_0:def 1;
then reconsider g = (len f) |-> a as FinSequence of REAL by FINSEQ_2:63;
for r being Real st r in rng f holds
r >= 0
proof
let r be Real; :: thesis: ( r in rng f implies r >= 0 )
assume B1: r in rng f ; :: thesis: r >= 0
consider k being object such that
B2: ( k in dom f & f . k = r ) by B1, FUNCT_1:def 3;
reconsider k = k as Element of NAT by B2;
thus r >= 0 by A1, B2; :: thesis: verum
end;
then reconsider f = f as nonnegative-yielding FinSequence of REAL by PARTFUN3:def 4;
per cases ( a = 0 or a > 0 ) ;
suppose B1: a = 0 ; :: thesis: Product f >= a |^ (len f)
per cases ( f is empty or not f is empty ) ;
suppose not f is empty ; :: thesis: Product f >= a |^ (len f)
then reconsider k = len ((len f) |-> a) as non zero Nat ;
( Product f >= 0 & Product (k |-> a) = 0 ) by B1;
hence Product f >= a |^ (len f) by B1; :: thesis: verum
end;
end;
end;
suppose a > 0 ; :: thesis: Product f >= a |^ (len f)
then reconsider a = a as positive Real ;
A2: for k being Element of NAT st k in dom f holds
( f . k >= ((len f) |-> a) . k & ((len f) |-> a) . k > 0 )
proof
let k be Element of NAT ; :: thesis: ( k in dom f implies ( f . k >= ((len f) |-> a) . k & ((len f) |-> a) . k > 0 ) )
assume B1: k in dom f ; :: thesis: ( f . k >= ((len f) |-> a) . k & ((len f) |-> a) . k > 0 )
reconsider k = k as non zero Nat by B1, FINSEQ_3:25;
((len f) |-> a) . k = a by B1, Lmkdf;
hence ( f . k >= ((len f) |-> a) . k & ((len f) |-> a) . k > 0 ) by A1, B1; :: thesis: verum
end;
len f = len g ;
then dom f = dom g by FINSEQ_3:29;
then ( len f = len g & ( for k being Element of NAT st k in dom g holds
( f . k >= g . k & g . k > 0 ) ) ) by A2;
then Product f >= Product g by NAT_4:54;
hence Product f >= a |^ (len f) by NEWTON:def 1; :: thesis: verum
end;
end;