let f1, f2 be FinSequence of REAL ; ( len f1 = len f2 & ( for k being Element of NAT st k in dom f1 holds
( f1 . k <= f2 . k & f1 . k > 0 ) ) implies Product f1 <= Product f2 )
defpred S1[ Nat] means for f1, f2 being FinSequence of REAL st len f1 = len f2 & $1 = len f1 & ( for k being Element of NAT st k in dom f1 holds
( f1 . k <= f2 . k & f1 . k > 0 ) ) holds
Product f1 <= Product f2;
assume A1:
len f1 = len f2
; ( ex k being Element of NAT st
( k in dom f1 & not ( f1 . k <= f2 . k & f1 . k > 0 ) ) or Product f1 <= Product f2 )
A2:
for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be
Nat;
( S1[n] implies S1[n + 1] )
assume A3:
S1[
n]
;
S1[n + 1]
for
f1,
f2 being
FinSequence of
REAL st
len f1 = len f2 &
n + 1
= len f1 & ( for
k being
Element of
NAT st
k in dom f1 holds
(
f1 . k <= f2 . k &
f1 . k > 0 ) ) holds
Product f1 <= Product f2
proof
let f1,
f2 be
FinSequence of
REAL ;
( len f1 = len f2 & n + 1 = len f1 & ( for k being Element of NAT st k in dom f1 holds
( f1 . k <= f2 . k & f1 . k > 0 ) ) implies Product f1 <= Product f2 )
assume that A4:
len f1 = len f2
and A5:
n + 1
= len f1
;
( ex k being Element of NAT st
( k in dom f1 & not ( f1 . k <= f2 . k & f1 . k > 0 ) ) or Product f1 <= Product f2 )
consider g2 being
FinSequence of
REAL ,
r2 being
Element of
REAL such that A6:
f2 = g2 ^ <*r2*>
by A4, A5, FINSEQ_2:19;
len f2 = (len g2) + (len <*r2*>)
by A6, FINSEQ_1:22;
then A7:
n + 1
= (len g2) + 1
by A4, A5, FINSEQ_1:39;
A8:
Product f2 = (Product g2) * r2
by A6, RVSUM_1:96;
consider g1 being
FinSequence of
REAL ,
r1 being
Element of
REAL such that A9:
f1 = g1 ^ <*r1*>
by A5, FINSEQ_2:19;
set k1 =
(len g1) + 1;
A10:
Product f1 = (Product g1) * r1
by A9, RVSUM_1:96;
len f1 = (len g1) + (len <*r1*>)
by A9, FINSEQ_1:22;
then A11:
n + 1
= (len g1) + 1
by A5, FINSEQ_1:39;
assume A12:
for
k being
Element of
NAT st
k in dom f1 holds
(
f1 . k <= f2 . k &
f1 . k > 0 )
;
Product f1 <= Product f2
then A17:
for
k being
Element of
NAT st
k in dom g1 holds
g1 . k > 0
;
Product g1 <= Product g2
by A3, A11, A7, A13;
then A18:
Product g2 > 0
by A17, Th41;
n + 1
>= 0 + 1
by XREAL_1:6;
then
(len g1) + 1
in Seg (n + 1)
by A11, FINSEQ_1:1;
then A19:
(len g1) + 1
in dom f1
by A5, FINSEQ_1:def 3;
then
f1 . ((len g1) + 1) <= f2 . ((len g1) + 1)
by A12;
then
r1 <= f2 . ((len g1) + 1)
by A9, FINSEQ_1:42;
then
r1 <= r2
by A6, A11, A7, FINSEQ_1:42;
then A20:
r1 * (Product g2) <= r2 * (Product g2)
by A18, XREAL_1:64;
f1 . ((len g1) + 1) > 0
by A12, A19;
then
r1 > 0
by A9, FINSEQ_1:42;
then
(Product g1) * r1 <= (Product g2) * r1
by A3, A11, A7, A13, XREAL_1:64;
hence
Product f1 <= Product f2
by A10, A8, A20, XXREAL_0:2;
verum
end;
hence
S1[
n + 1]
;
verum
end;
A21:
S1[ 0 ]
A22:
for n being Nat holds S1[n]
from NAT_1:sch 2(A21, A2);
assume
for k being Element of NAT st k in dom f1 holds
( f1 . k <= f2 . k & f1 . k > 0 )
; Product f1 <= Product f2
hence
Product f1 <= Product f2
by A22, A1; verum