:: Modular Integer Arithmetic
:: by Christoph Schwarzweller
::
:: Received May 13, 2008
:: Copyright (c) 2008 Association of Mizar Users
Lm1:
for f being integer-yielding FinSequence holds f is FinSequence of INT
theorem Th1: :: INT_6:1
theorem Th2: :: INT_6:2
theorem Th3: :: INT_6:3
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: :: INT_6:4
Lm5:
for z being integer-yielding FinSequence holds z is FinSequence of REAL
theorem Th5: :: INT_6:5
theorem Th6: :: INT_6:6
theorem Th7: :: INT_6:7
theorem Th8: :: INT_6:8
theorem Th9: :: INT_6:9
theorem Th10: :: INT_6:10
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 :: INT_6:11
theorem :: INT_6:12
theorem Th13: :: INT_6:13
theorem Th14: :: INT_6:14
theorem Th15: :: INT_6:15
theorem Th16: :: INT_6:16
theorem Th17: :: INT_6:17
theorem Th18: :: INT_6:18
theorem Th19: :: INT_6:19
theorem Th20: :: INT_6:20
theorem Th21: :: INT_6:21
theorem Th22: :: INT_6:22
:: deftheorem Def1 defines multiplicative-trivial INT_6:def 1 :
theorem :: INT_6:23
:: deftheorem Def2 defines Chinese_Remainder INT_6:def 2 :
theorem Th24: :: INT_6:24
Lm7:
for m being CR_Sequence holds Product m > 0
theorem Th25: :: INT_6:25
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
:: deftheorem Def3 defines mod INT_6:def 3 :
:: deftheorem Def4 defines CR_coefficients INT_6:def 4 :
theorem Th26: :: INT_6:26
theorem Th27: :: INT_6:27
theorem :: INT_6:28
theorem Th29: :: INT_6:29
theorem Th30: :: INT_6:30
:: deftheorem Def5 defines to_int INT_6:def 5 :
theorem Th31: :: INT_6:31
theorem Th32: :: INT_6:32
theorem Th33: :: INT_6:33
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: :: INT_6:34
theorem Th35: :: INT_6:35
theorem Th36: :: INT_6:36
theorem Th37: :: INT_6:37
theorem :: INT_6:38
theorem :: INT_6:39
theorem :: INT_6:40
theorem :: INT_6:41
theorem :: INT_6:42