let m be INT -valued FinSequence; :: thesis: for i, j being Nat st i in dom m & j in dom m & j <> i & m . j <> 0 holds
(Product m) / ((m . i) * (m . j)) is Integer
let i9, j9 be Nat; :: thesis: ( i9 in dom m & j9 in dom m & j9 <> i9 & m . j9 <> 0 implies (Product m) / ((m . i9) * (m . j9)) is Integer )
assume that
A1: i9 in dom m and
A2: j9 in dom m and
A3: j9 <> i9 and
A4: m . j9 <> 0 ; :: thesis: (Product m) / ((m . i9) * (m . j9)) is Integer
reconsider i = i9, j = j9 as Element of NAT by ORDINAL1:def 12;
A5: ex z being Integer st z * (m . i) = (Product m) / (m . j) by A1, A2, A3, A4, Lm6;
per cases ( m . i = 0 or m . i <> 0 ) ;
suppose A0: m . i = 0 ; :: thesis: (Product m) / ((m . i9) * (m . j9)) is Integer
thus (Product m) / ((m . i9) * (m . j9)) is Integer by A0; :: thesis: verum
end;
suppose A6: m . i <> 0 ; :: thesis: (Product m) / ((m . i9) * (m . j9)) is Integer
reconsider u = (Product m) / (m . j) as Integer by A2, A4, Th9;
A7: u / (m . i) = (Product m) * (((m . j) ") * ((m . i) "))
.= (Product m) / ((m . i) * (m . j)) by XCMPLX_1:204 ;
m . i divides u by A5, INT_1:def 3;
hence (Product m) / ((m . i9) * (m . j9)) is Integer by A6, A7, WSIERP_1:17; :: thesis: verum
end;
end;