environ
vocabularies HIDDEN, NUMBERS, INT_1, NAT_1, SUBSET_1, MEMBERED, MEMBER_1, TARSKI, REAL_1, ARYTM_3, FUNCT_1, RELAT_1, FINSET_1, CARD_1, XBOOLE_0, ARYTM_1, INT_2, XXREAL_0, COMPLEX1, NEWTON, SQUARE_1, PARTFUN1, EQREL_1, RELAT_2, EULER_1, FINSEQ_1, FINSEQ_3, ORDINAL4, CARD_3, XCMPLX_0, PRE_POLY, NAT_3, UPROOTS, INT_4;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, CARD_1, ORDINAL1, NUMBERS, MEMBERED, XXREAL_0, XCMPLX_0, XREAL_0, INT_1, REAL_1, INT_2, NAT_D, NEWTON, SQUARE_1, RELAT_1, FUNCT_1, FINSEQ_1, RELSET_1, RVSUM_1, EULER_1, EQREL_1, RELAT_2, PARTFUN1, FINSET_1, NAT_3, UPROOTS, TREES_4, WSIERP_1, MEASURE6, INTEGRA2, RECDEF_1, PRE_POLY;
definitions FUNCT_1, RELAT_2, PARTFUN1, TARSKI, XBOOLE_0, WELLORD2;
theorems FINSEQ_3, FINSEQ_2, ABSVALUE, FINSEQ_5, EULER_2, CARD_2, SEQ_2, RELAT_2, RELSET_1, EQREL_1, ORDERS_1, FINSEQ_4, MOEBIUS1, XBOOLE_0, NAT_3, NEWTON, INT_2, WSIERP_1, CARD_1, PEPIN, NAT_1, XCMPLX_1, XREAL_1, ORDINAL1, EULER_1, FINSEQ_1, XBOOLE_1, TARSKI, ZFMISC_1, RVSUM_1, INT_1, FUNCT_1, XXREAL_0, NAT_D, XREAL_0, INTEGRA2, VALUED_0, FUNCT_2, MEMBER_1, MEMBERED, XTUPLE_0, NUMBERS;
schemes NAT_1, FINSEQ_1, FINSEQ_2, RELSET_1, CLASSES1;
registrations RELAT_1, FINSEQ_1, CARD_1, PARTFUN1, NAT_1, INT_1, MEMBERED, FINSET_1, NEWTON, NAT_3, XXREAL_0, NUMBERS, XREAL_0, ORDINAL1, FUNCT_1, VALUED_0, RELSET_1, PEPIN;
constructors HIDDEN, EULER_1, REAL_1, WELLORD2, BINARITH, WSIERP_1, PEPIN, UPROOTS, NAT_3, NAT_D, MEASURE6, INTEGRA2, RECDEF_1, RELSET_1, NUMBERS;
requirements HIDDEN, REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
equalities INT_1, FINSEQ_1, XCMPLX_0, EULER_1, CARD_1, XBOOLE_0, ORDINAL1;
expansions FUNCT_1, INT_1, FINSEQ_1, XBOOLE_0;
Lm1:
for a being Integer
for X being Subset of INT holds a ++ X c= INT
Lm2:
for a being Integer
for X being Subset of INT holds a ** X c= INT
Lm3:
for x being Integer
for X being Subset of INT
for a being Integer holds
( x in a ** X iff ex y being Integer st
( y in X & x = a * y ) )
Lm4:
for i1, i2, i3 being Integer st i1 divides i2 & i1 divides i3 holds
i1 divides i2 - i3
Lm5:
for a, b, i being Integer st i divides a & i divides a - b holds
i divides b
Lm6:
for p, n being Nat st p is prime & p,n are_coprime holds
not p divides n
Lm7:
for p being Nat st p > 0 holds
p >= 1 + 0
by NAT_1:13;
definition
let m be
Integer;
existence
ex b1 being Relation of INT st
for x, y being Integer holds
( [x,y] in b1 iff x,y are_congruent_mod m )
uniqueness
for b1, b2 being Relation of INT st ( for x, y being Integer holds
( [x,y] in b1 iff x,y are_congruent_mod m ) ) & ( for x, y being Integer holds
( [x,y] in b2 iff x,y are_congruent_mod m ) ) holds
b1 = b2
end;
Lm8:
for m being Integer holds Cong m is Equivalence_Relation of INT
Lm9:
for i1, i2 being Integer
for n being Nat st n > 0 & i1 mod n = 0 holds
(i1 * i2) mod n = 0
Lm10:
for x, y being Integer holds
( ( x divides y implies y mod x = 0 ) & ( x <> 0 & y mod x = 0 implies x divides y ) )
Lm11:
for x, y being Integer st x divides y holds
y = (y div x) * x
Lm12:
for x, y being Integer st ( x <> 0 or y <> 0 ) holds
x div (x gcd y),y div (x gcd y) are_coprime
Lm13:
for i, x, y being Integer st x divides i & y divides i & x,y are_coprime holds
x * y divides i
theorem
for
m1,
m2,
m3,
a,
b,
c being
Integer st
m1 <> 0 &
m2 <> 0 &
m3 <> 0 &
m1,
m2 are_coprime &
m1,
m3 are_coprime &
m2,
m3 are_coprime holds
ex
r,
s being
Integer st
for
x being
Integer st
(x - a) mod m1 = 0 &
(x - b) mod m2 = 0 &
(x - c) mod m3 = 0 holds
(
x,
(a + (m1 * r)) + ((m1 * m2) * s) are_congruent_mod (m1 * m2) * m3 &
((m1 * r) - (b - a)) mod m2 = 0 &
(((m1 * m2) * s) - ((c - a) - (m1 * r))) mod m3 = 0 )