let m be INT -valued FinSequence; for i, j being Nat st i in dom m & j in dom m & j <> i & m . j <> 0 holds
ex z being Integer st z * (m . i) = (Product m) / (m . j)
let i9, j9 be Nat; ( i9 in dom m & j9 in dom m & j9 <> i9 & m . j9 <> 0 implies ex z being Integer st z * (m . i9) = (Product m) / (m . j9) )
reconsider m9 = m as FinSequence of INT by Lm1;
assume that
A1:
i9 in dom m
and
A2:
j9 in dom m
and
A3:
j9 <> i9
and
A4:
m . j9 <> 0
; ex z being Integer st z * (m . i9) = (Product m) / (m . j9)
reconsider i = i9, j = j9 as Element of NAT by ORDINAL1:def 12;
A5:
dom m = Seg (len m)
by FINSEQ_1:def 3;
then A6:
j <= len m
by A2, FINSEQ_1:1;
A7:
1 <= j
by A2, A5, FINSEQ_1:1;
then
1 - 1 <= j - 1
by XREAL_1:9;
then reconsider kj = j - 1 as Element of NAT by INT_1:3;
set f = (m | kj) ^ (m /^ j);
reconsider f = (m | kj) ^ (m /^ j) as FinSequence of INT by Lm1;
kj + 1 = j
;
then
kj <= j
by NAT_1:11;
then A8:
len (m | kj) = kj
by A6, FINSEQ_1:59, XXREAL_0:2;
A9:
dom m = Seg (len m)
by FINSEQ_1:def 3;
then A10:
1 <= i
by A1, FINSEQ_1:1;
then
1 - 1 <= i - 1
by XREAL_1:9;
then reconsider ki = i - 1 as Element of NAT by INT_1:3;
A11:
i <= len m
by A1, A9, FINSEQ_1:1;
ex l being Element of NAT st
( l in dom f & f . l = m . i )
proof
per cases
( i < j or i > j )
by A3, XXREAL_0:1;
suppose A15:
i > j
;
ex l being Element of NAT st
( l in dom f & f . l = m . i )then
i - 1
> kj
by XREAL_1:9;
then reconsider a =
(i - 1) - kj as
Element of
NAT by INT_1:5;
i - kj > (kj + 1) - kj
by A15, XREAL_1:9;
then
(i - kj) - 1
> 1
- 1
by XREAL_1:9;
then
ex
g being
Nat st
a = g + 1
by NAT_1:6;
then A16:
1
<= (i - 1) - kj
by NAT_1:11;
A17:
len (m /^ j) = (len m) - j
by A6, RFINSEQ:def 1;
then len f =
kj + ((len m) - j)
by A8, FINSEQ_1:22
.=
(len m) - 1
;
then A18:
ki <= len f
by A11, XREAL_1:9;
i - j <= (len m) - j
by A11, XREAL_1:9;
then
a in Seg (len (m /^ j))
by A17, A16;
then A19:
(i - 1) - kj in dom (m9 /^ j)
by FINSEQ_1:def 3;
ki + 1
> 1
by A7, A15, XXREAL_0:2;
then
ki >= 1
by NAT_1:13;
then
ki in Seg (len f)
by A18;
then A20:
ki in dom f
by FINSEQ_1:def 3;
reconsider D =
INT as
set ;
reconsider ww =
m9 as
FinSequence of
D ;
len (m | kj) < i - 1
by A8, A15, XREAL_1:9;
then f . ki =
(m /^ j) . (ki - kj)
by A8, A18, FINSEQ_1:24
.=
(ww /^ j) /. (ki - kj)
by A19, PARTFUN1:def 6
.=
ww /. (j + a)
by A19, FINSEQ_5:27
.=
m . i
by A1, PARTFUN1:def 6
;
hence
ex
l being
Element of
NAT st
(
l in dom f &
f . l = m . i )
by A20;
verum end;
end;
then consider l being Element of NAT such that
A21:
l in dom f
and
A22:
f . l = m . i
;
l in Seg (len f)
by A21, FINSEQ_1:def 3;
then
1 <= l
by FINSEQ_1:1;
then reconsider kl = l - 1 as Element of NAT by INT_1:5;
l in Seg (len f)
by A21, FINSEQ_1:def 3;
then
kl + 1 <= len f
by FINSEQ_1:1;
then
(f | kl) ^ <*(f . l)*> = f | l
by Th5;
then
f = ((f | kl) ^ <*(f . l)*>) ^ (f /^ l)
by RFINSEQ:8;
then A23: Product f =
(Product ((f | kl) ^ <*(f . l)*>)) * (Product (f /^ l))
by RVSUM_1:97
.=
((Product (f | kl)) * (Product <*(f . l)*>)) * (Product (f /^ l))
by RVSUM_1:97
.=
((Product (f | kl)) * (Product (f /^ l))) * (Product <*(m . i)*>)
by A22
.=
((Product (f | kl)) * (Product (f /^ l))) * (m . i)
.=
(Product ((f | kl) ^ (f /^ l))) * (m . i)
by RVSUM_1:97
;
kj + 1 <= len m
by A2, A5, FINSEQ_1:1;
then A24:
(m | kj) ^ <*(m . j)*> = m | j
by Th5;
reconsider m2 = m /^ j as FinSequence of INT by Lm1;
reconsider m1 = m | j as FinSequence of INT by Lm1;
m9 = m1 ^ m2
by RFINSEQ:8;
then Product m =
(Product ((m | kj) ^ <*(m . j)*>)) * (Product (m /^ j))
by A24, RVSUM_1:97
.=
((Product (m | kj)) * (Product <*(m . j)*>)) * (Product (m /^ j))
by RVSUM_1:97
.=
((Product (m | kj)) * (Product (m /^ j))) * (Product <*(m . j)*>)
.=
((Product (m | kj)) * (Product (m /^ j))) * (m . j)
.=
(Product f) * (m . j)
by RVSUM_1:97
;
then (Product m) / (m . j) =
(Product f) * ((m . j) * ((m . j) "))
.=
(Product f) * 1
by A4, XCMPLX_0:def 7
;
hence
ex z being Integer st z * (m . i9) = (Product m) / (m . j9)
by A23; verum