:: Modular Integer Arithmetic
:: by Christoph Schwarzweller
::
:: Received May 13, 2008
:: Copyright (c) 2008 Association of Mizar Users
intint:
for f being integer-yielding FinSequence holds f is FinSequence of INT
theorem length1a: :: INT_6:1
theorem length2a: :: INT_6:2
theorem length3a: :: INT_6:3
length1:
for m1, m2 being complex-valued FinSequence st len m1 = len m2 holds
len (m1 + m2) = len m1
length2:
for m1, m2 being complex-valued FinSequence st len m1 = len m2 holds
len (m1 - m2) = len m1
length3:
for m1, m2 being complex-valued FinSequence st len m1 = len m2 holds
len (m1 (#) m2) = len m1
theorem Z10: :: INT_6:4
ZZ1:
for z being integer-yielding FinSequence holds z is FinSequence of REAL
theorem th67: :: INT_6:5
theorem mtriv: :: INT_6:6
theorem Th14: :: INT_6:7
theorem div0: :: INT_6:8
theorem prodint: :: INT_6:9
theorem x000: :: INT_6:10
x0000:
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 thabs0: :: INT_6:13
theorem thagcd: :: INT_6:14
theorem thabs1: :: INT_6:15
theorem thgcd0: :: INT_6:16
theorem thgcd4: :: INT_6:17
theorem thgcd3: :: INT_6:18
theorem thgcd2: :: INT_6:19
theorem x1: :: INT_6:20
theorem x1a: :: INT_6:21
theorem thgcd: :: INT_6:22
:: deftheorem DefMTriv defines multiplicative-trivial INT_6:def 1 :
theorem :: INT_6:23
:: deftheorem DefCR defines Chinese_Remainder INT_6:def 2 :
theorem CRsub: :: INT_6:24
x0:
for m being CR_Sequence holds Product m > 0
theorem prodgcd: :: INT_6:25
Th3:
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 Df1 defines mod INT_6:def 3 :
:: deftheorem defCi defines CR_coefficients INT_6:def 4 :
theorem l1: :: INT_6:26
theorem l2: :: INT_6:27
theorem :: INT_6:28
theorem congsum: :: INT_6:29
theorem exnon: :: INT_6:30
:: deftheorem Df5 defines to_int INT_6:def 5 :
theorem lemat2: :: INT_6:31
theorem lemat4: :: INT_6:32
theorem lemat3ap: :: INT_6:33
lemat3mm:
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 lemat3a: :: INT_6:34
theorem lemat3p: :: INT_6:35
theorem lemat3m: :: INT_6:36
theorem lemat3: :: INT_6:37
theorem :: INT_6:38
theorem :: INT_6:39
theorem :: INT_6:40
theorem :: INT_6:41
theorem :: INT_6:42