begin
Lm1:
for f being integer-yielding FinSequence holds f is FinSequence of INT
theorem Th1:
theorem Th2:
theorem Th3:
Lm2:
for m1, m2 being complex-valued FinSequence st len m1 = len m2 holds
len (m1 + m2) = len m1
Lm3:
for m1, m2 being complex-valued FinSequence st len m1 = len m2 holds
len (m1 - m2) = len m1
Lm4:
for m1, m2 being complex-valued FinSequence st len m1 = len m2 holds
len (m1 (#) m2) = len m1
theorem Th4:
Lm5:
for z being integer-yielding FinSequence holds z is FinSequence of REAL
theorem Th5:
theorem Th6:
theorem Th7:
theorem Th8:
theorem Th9:
theorem Th10:
Lm6:
for m being integer-yielding FinSequence
for i, j being natural number 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)
theorem
theorem
begin
theorem Th13:
theorem Th14:
theorem Th15:
theorem Th16:
theorem Th17:
theorem Th18:
theorem Th19:
theorem Th20:
theorem Th21:
theorem Th22:
begin
:: deftheorem Def1 defines multiplicative-trivial INT_6:def 1 :
theorem
:: deftheorem Def2 defines Chinese_Remainder INT_6:def 2 :
theorem Th24:
Lm7:
for m being CR_Sequence holds Product m > 0
theorem Th25:
Lm8:
for u being integer-yielding FinSequence
for m being CR_Sequence
for z1, z2 being Integer st 0 <= z1 & z1 < Product m & ( for i being natural number st i in dom m holds
z1,u . i are_congruent_mod m . i ) & 0 <= z2 & z2 < Product m & ( for i being natural number st i in dom m holds
z2,u . i are_congruent_mod m . i ) holds
z1 = z2
begin
:: deftheorem Def3 defines mod INT_6:def 3 :
:: deftheorem Def4 defines CR_coefficients INT_6:def 4 :
theorem Th26:
theorem Th27:
theorem
theorem Th29:
theorem Th30:
:: deftheorem Def5 defines to_int INT_6:def 5 :
theorem Th31:
theorem Th32:
theorem Th33:
Lm9:
for u, v being Integer
for m being CR_Sequence
for i being natural number st i in dom m holds
((mod u,m) - (mod v,m)) . i,u - v are_congruent_mod m . i
theorem Th34:
theorem Th35:
theorem Th36:
theorem Th37:
theorem
theorem
theorem
begin
theorem
theorem