:: Modular Integer Arithmetic
:: by Christoph Schwarzweller
::
:: Received May 13, 2008
:: Copyright (c) 2008-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, FINSEQ_1, RELAT_1, TARSKI, VALUED_0, ORDINAL1, RFINSEQ,
XXREAL_0, ARYTM_1, SUBSET_1, FUNCT_1, ARYTM_3, INT_1, ORDINAL4, XBOOLE_0,
NAT_1, VALUED_1, CARD_3, BINOP_2, SETWISEO, BINOP_1, SETWOP_2, CARD_1,
FINSOP_1, PARTFUN1, COMPLEX1, INT_2, PARTFUN3, INT_6, REAL_1;
notations TARSKI, XBOOLE_0, SUBSET_1, INT_1, INT_2, ORDINAL1, NUMBERS,
RELAT_1, PARTFUN1, PARTFUN3, XXREAL_0, XREAL_0, FUNCT_1, VALUED_0,
VALUED_1, BINOP_2, SETWISEO, RFINSEQ, BINOP_1, FINSEQ_1, SETWOP_2,
RVSUM_1, XCMPLX_0, NAT_1, FINSOP_1;
constructors FINSOP_1, RFINSEQ, INT_2, BINOP_2, REAL_1, SETWISEO, SETWOP_2,
PARTFUN3, XXREAL_0, RVSUM_1, BINOP_1, RELSET_1, NAT_D;
registrations NUMBERS, XREAL_0, NAT_1, INT_1, RELAT_1, FINSEQ_1, RVSUM_1,
XBOOLE_0, MEMBERED, BINOP_2, ORDINAL1, XXREAL_0, VALUED_0, VALUED_1,
FUNCT_1, CARD_1;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
definitions INT_2;
equalities XCMPLX_0, FINSEQ_1, ORDINAL1;
expansions INT_2, FINSEQ_1, FUNCT_1;
theorems INT_1, FUNCT_1, FINSEQ_1, RVSUM_1, NAT_1, SETWOP_2, FINSEQ_3,
BINOP_2, SETWISEO, TARSKI, NAT_D, INT_2, XCMPLX_0, XCMPLX_1, XREAL_1,
RFINSEQ, FINSEQ_5, FINSEQ_2, ABSVALUE, PARTFUN3, XBOOLE_0, XXREAL_0,
ORDINAL1, XBOOLE_1, PARTFUN1, XREAL_0, WSIERP_1, VALUED_1, COMPLEX1,
RELAT_1;
schemes FINSEQ_1, NAT_1, INT_1;
begin :: Preliminaries
registration
let f be complex-valued FinSequence, n be Nat;
cluster f|n -> complex-valued;
coherence;
end;
registration
let f be INT-valued FinSequence, n be Nat;
cluster f|n -> INT-valued;
coherence;
end;
registration
let f be INT-valued FinSequence, n be Nat;
cluster f/^n -> INT-valued;
coherence;
end;
registration
let i be Integer;
cluster <*i*> -> INT-valued;
coherence;
end;
registration
let f,g be INT-valued FinSequence;
cluster f ^ g -> INT-valued;
coherence;
end;
theorem Th1:
for f1,f2 being complex-valued FinSequence holds len(f1 + f2) =
min(len f1, len f2)
proof
let f1,f2 be complex-valued FinSequence;
set g = f1 + f2;
consider n1 being Nat such that
A1: dom f1 = Seg n1 by FINSEQ_1:def 2;
n1 in NAT by ORDINAL1:def 12;
then
A2: len f1 = n1 by A1,FINSEQ_1:def 3;
consider n2 being Nat such that
A3: dom f2 = Seg n2 by FINSEQ_1:def 2;
n2 in NAT by ORDINAL1:def 12;
then
A4: len f2 = n2 by A3,FINSEQ_1:def 3;
A5: dom g = dom f1 /\ dom f2 by VALUED_1:def 1;
now
per cases;
case
A6: n1 <= n2;
then dom f1 c= dom f2 by A1,A3,FINSEQ_1:5;
then
A7: dom g = Seg n1 by A1,A5,XBOOLE_1:28;
min(n1,n2) = n1 by A6,XXREAL_0:def 9;
hence thesis by A2,A4,A7,FINSEQ_1:def 3;
end;
case
A8: n2 <= n1;
then dom f2 c= dom f1 by A1,A3,FINSEQ_1:5;
then
A9: dom g = Seg n2 by A3,A5,XBOOLE_1:28;
min(n1,n2) = n2 by A8,XXREAL_0:def 9;
hence thesis by A2,A4,A9,FINSEQ_1:def 3;
end;
end;
hence thesis;
end;
theorem Th2:
for f1, f2 being complex-valued FinSequence holds len(f1 - f2) =
min(len f1, len f2)
proof
let f1,f2 be complex-valued FinSequence;
set g = f1 - f2;
consider n1 being Nat such that
A1: dom f1 = Seg n1 by FINSEQ_1:def 2;
n1 in NAT by ORDINAL1:def 12;
then
A2: len f1 = n1 by A1,FINSEQ_1:def 3;
consider n2 being Nat such that
A3: dom f2 = Seg n2 by FINSEQ_1:def 2;
n2 in NAT by ORDINAL1:def 12;
then
A4: len f2 = n2 by A3,FINSEQ_1:def 3;
A5: dom g = dom f1 /\ dom f2 by VALUED_1:12;
now
per cases;
case
A6: n1 <= n2;
then dom f1 c= dom f2 by A1,A3,FINSEQ_1:5;
then
A7: dom g = Seg n1 by A1,A5,XBOOLE_1:28;
min(n1,n2) = n1 by A6,XXREAL_0:def 9;
hence thesis by A2,A4,A7,FINSEQ_1:def 3;
end;
case
A8: n2 <= n1;
then dom f2 c= dom f1 by A1,A3,FINSEQ_1:5;
then
A9: dom g = Seg n2 by A3,A5,XBOOLE_1:28;
min(n1,n2) = n2 by A8,XXREAL_0:def 9;
hence thesis by A2,A4,A9,FINSEQ_1:def 3;
end;
end;
hence thesis;
end;
theorem Th3:
for f1,f2 being complex-valued FinSequence holds len(f1 (#) f2) =
min(len f1, len f2)
proof
let f1,f2 be complex-valued FinSequence;
set g = f1 (#) f2;
consider n1 being Nat such that
A1: dom f1 = Seg n1 by FINSEQ_1:def 2;
n1 in NAT by ORDINAL1:def 12;
then
A2: len f1 = n1 by A1,FINSEQ_1:def 3;
consider n2 being Nat such that
A3: dom f2 = Seg n2 by FINSEQ_1:def 2;
n2 in NAT by ORDINAL1:def 12;
then
A4: len f2 = n2 by A3,FINSEQ_1:def 3;
A5: dom g = dom f1 /\ dom f2 by VALUED_1:def 4;
now
per cases;
case
A6: n1 <= n2;
then dom f1 c= dom f2 by A1,A3,FINSEQ_1:5;
then
A7: dom g = Seg n1 by A1,A5,XBOOLE_1:28;
min(n1,n2) = n1 by A6,XXREAL_0:def 9;
hence thesis by A2,A4,A7,FINSEQ_1:def 3;
end;
case
A8: n2 <= n1;
then dom f2 c= dom f1 by A1,A3,FINSEQ_1:5;
then
A9: dom g = Seg n2 by A3,A5,XBOOLE_1:28;
min(n1,n2) = n2 by A8,XXREAL_0:def 9;
hence thesis by A2,A4,A9,FINSEQ_1:def 3;
end;
end;
hence thesis;
end;
Lm2: for m1,m2 be complex-valued FinSequence st len m1 = len m2 holds len(m1 +
m2) = len m1
proof
let m1,m2 be complex-valued FinSequence;
assume
A1: len m1 = len m2;
thus len(m1 + m2) = min(len m1, len m2) by Th1
.= len m1 by A1;
end;
Lm3: for m1,m2 be complex-valued FinSequence st len m1 = len m2 holds len(m1 -
m2) = len m1
proof
let m1,m2 be complex-valued FinSequence;
assume
A1: len m1 = len m2;
thus len(m1 - m2) = min(len m1, len m2) by Th2
.= len m1 by A1;
end;
Lm4: for m1,m2 be complex-valued FinSequence st len m1 = len m2 holds len(m1
(#) m2) = len m1
proof
let m1,m2 be complex-valued FinSequence;
assume
A1: len m1 = len m2;
thus len(m1 (#) m2) = min(len m1, len m2) by Th3
.= len m1 by A1;
end;
theorem Th4:
for m1,m2 being complex-valued FinSequence st len m1 = len m2
for k being Nat st k <= len m1 holds (m1(#)m2)|k = (m1|k) (#) (m2|k)
proof
let m1,m2 be complex-valued FinSequence;
assume
A1: len m1 = len m2;
let k9 be Nat;
set p = (m1(#)m2)|k9, q = (m1|k9) (#) (m2|k9);
assume
A2: k9 <= len m1;
then
A3: len(m1|k9) = k9 by FINSEQ_1:59;
reconsider k = k9 as Element of NAT by ORDINAL1:def 12;
A4: k9 <= len(m1(#)m2) by A1,A2,Lm4;
then
A5: len p = k9 by FINSEQ_1:59;
A6: len(m2|k9) = k9 by A1,A2,FINSEQ_1:59;
then
A7: len q = k9 by A3,Lm4;
now
A8: len(m1(#)m2) = len m1 by A1,Lm4;
let j be Nat;
assume that
A9: 1 <= j and
A10: j <= len p;
A11: j in Seg k by A5,A9,A10;
then
A12: j in dom(m1|k) by A3,FINSEQ_1:def 3;
A13: j in dom q by A7,A11,FINSEQ_1:def 3;
A14: j in dom(m2|k) by A6,A11,FINSEQ_1:def 3;
j <= len m1 by A2,A5,A10,XXREAL_0:2;
then j in Seg(len(m1(#)m2)) by A9,A8;
then
A15: j in dom(m1(#)m2) by FINSEQ_1:def 3;
j in dom p by A9,A10,FINSEQ_3:25;
hence p.j = (m1(#)m2).j by FUNCT_1:47
.= m1.j * m2.j by A15,VALUED_1:def 4
.= (m1|k).j * m2.j by A12,FUNCT_1:47
.= (m1|k).j * (m2|k).j by A14,FUNCT_1:47
.= q.j by A13,VALUED_1:def 4;
end;
hence thesis by A4,A7,FINSEQ_1:59;
end;
registration
let F be integer-valued FinSequence;
cluster Sum F -> integer;
coherence
proof
set mc = addcomplex;
consider f being FinSequence of COMPLEX such that
A1: f = F and
A2: Sum F = addcomplex $$ f by RVSUM_1:def 10;
set g = [#](f,the_unity_wrt mc);
defpred P[Nat] means
mc $$ (finSeg $1,[#](f,the_unity_wrt mc)) is integer;
A3: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat;
A4: g.(k+1) is integer
proof
per cases;
suppose
k+1 in dom f;
then g.(k+1) = f.(k+1) by SETWOP_2:20;
hence thesis by A1;
end;
suppose
not k+1 in dom f;
hence thesis by BINOP_2:1,SETWOP_2:20;
end;
end;
assume P[k];
then reconsider a = g.(k+1), b = mc $$(finSeg k,g) as Integer by
A4;
not (k + 1) in Seg k by FINSEQ_3:8;
then mc $$ (finSeg k \/ {.k+1.},g) = mc.(mc $$(finSeg k,g),g.(k+1)) by
SETWOP_2:2
.= b + a by BINOP_2:def 3;
hence thesis by FINSEQ_1:9;
end;
Seg 0 = {}.NAT;
then
A5: P[0] by BINOP_2:1,SETWISEO:31;
A6: for n being Nat holds P[n] from NAT_1:sch 2(A5,A3);
consider n being Nat such that
A7: dom f = Seg n by FINSEQ_1:def 2;
A8: mc $$ f = mc $$ (findom f,[#](f,the_unity_wrt mc)) by SETWOP_2:def 2;
thus thesis by A2,A8,A7,A6;
end;
cluster Product F -> integer;
coherence
proof
set mc = multcomplex;
consider f being FinSequence of COMPLEX such that
A9: f = F and
A10: Product F = multcomplex $$ f by RVSUM_1:def 13;
set g = [#](f,the_unity_wrt mc);
defpred P[Nat] means
mc $$ (finSeg $1,[#](f,the_unity_wrt mc)) is integer;
A11: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat;
A12: g.(k+1) is integer
proof
per cases;
suppose
k+1 in dom f;
then g.(k+1) = f.(k+1) by SETWOP_2:20;
hence thesis by A9;
end;
suppose
not k+1 in dom f;
hence thesis by BINOP_2:6,SETWOP_2:20;
end;
end;
assume P[k];
then reconsider a = g.(k+1), b = mc $$(finSeg k,g) as Integer by
A12;
not (k + 1) in Seg k by FINSEQ_3:8;
then mc $$ (finSeg k \/ {.k+1.},g) = mc.(mc $$(finSeg k,g),g.(k+1)) by
SETWOP_2:2
.= b * a by BINOP_2:def 5;
hence thesis by FINSEQ_1:9;
end;
Seg 0 = {}.NAT;
then
A13: P[0] by BINOP_2:6,SETWISEO:31;
A14: for n being Nat holds P[n] from NAT_1:sch 2(A13,A11);
consider n being Nat such that
A15: dom f = Seg n by FINSEQ_1:def 2;
A16: mc $$ f = mc $$ (findom f,[#](f,the_unity_wrt mc)) by SETWOP_2:def 2;
thus thesis by A10,A16,A15,A14;
end;
end;
theorem Th5:
for f being complex-valued FinSequence, i being Nat st
i+1 <= len f holds f|i ^ <*f.(i+1)*> = f|(i+1)
proof
let f be complex-valued FinSequence, i be Nat;
assume
A1: i + 1 <= len f;
set f1 = f|i ^ <*f.(i+1)*>, f2 = f|(i+1);
A2: i <= i + 1 by NAT_1:11;
reconsider f1 as complex-valued FinSequence;
A3: len f1 = len(f|i) + len(<*f.(i+1)*>) by FINSEQ_1:22
.= len(f|i) + 1 by FINSEQ_1:39
.= i + 1 by A1,A2,FINSEQ_1:59,XXREAL_0:2
.= len f2 by A1,FINSEQ_1:59;
then
A4: dom f1 = Seg(len f2) by FINSEQ_1:def 3
.= dom f2 by FINSEQ_1:def 3;
A5: i <= len f by A1,A2,XXREAL_0:2;
now
let x9 be object;
assume
A6: x9 in dom f1;
then reconsider x = x9 as Element of NAT;
A7: dom f1 = Seg(len f1) by FINSEQ_1:def 3;
then
A8: 1 <= x by A6,FINSEQ_1:1;
x <= len f1 by A6,A7,FINSEQ_1:1;
then
A9: x <= i + 1 by A1,A3,FINSEQ_1:59;
per cases by A9,XXREAL_0:1;
suppose
A10: x = i + 1;
then x in Seg(i+1) by A8;
then
A11: x in dom f2 by A1,FINSEQ_1:17;
dom <*f.(i+1)*> = {1} by FINSEQ_1:2,38;
then
A12: 1 in dom <*f.(i+1)*> by TARSKI:def 1;
len(f|i) = i by A1,A2,FINSEQ_1:59,XXREAL_0:2;
hence f1.x9 = <*f.(i+1)*>.1 by A10,A12,FINSEQ_1:def 7
.= f.(i+1)
.= f2.x9 by A10,A11,FUNCT_1:47;
end;
suppose
x < i + 1;
then
A13: x <= i by NAT_1:13;
1 <= x by A6,A7,FINSEQ_1:1;
then x in Seg i by A13;
then
A14: x in dom(f|i) by A5,FINSEQ_1:17;
hence f1.x9 = (f|i).x by FINSEQ_1:def 7
.= f.x by A14,FUNCT_1:47
.= f2.x9 by A4,A6,FUNCT_1:47;
end;
end;
hence thesis by A4;
end;
theorem Th6:
for f being complex-valued FinSequence st
ex i being Nat st i in dom f & f.i = 0 holds Product(f) = 0
proof
defpred P[Nat] means for f being complex-valued FinSequence st len f = $1
holds (ex i being Nat st i in dom f & f.i = 0) implies Product(f) =
0;
let m be complex-valued FinSequence;
A1: for k being Nat st P[k] holds P[k + 1]
proof
let k be Nat;
assume
A2: P[k];
now
let f be complex-valued FinSequence;
set f1 = f|k;
assume
A3: len f = k + 1;
then
A4: len f1 = k by FINSEQ_1:59,NAT_1:11;
reconsider f1 as complex-valued FinSequence;
f = f1^<*f.(k+1)*> by A3,FINSEQ_3:55;
then
A5: Product(f) = Product(f1) * f.(k+1) by RVSUM_1:96;
assume
A6: ex i being Nat st i in dom f & f.i = 0;
per cases;
suppose
f.(k+1) = 0;
hence Product(f) = 0 by A5;
end;
suppose
A7: f.(k+1) <> 0;
consider j being Nat such that
A8: j in dom f and
A9: f.j = 0 by A6;
reconsider j as Element of NAT by ORDINAL1:def 12;
A10: j in Seg(len f) by A8,FINSEQ_1:def 3;
then j <= k + 1 by A3,FINSEQ_1:1;
then j < k+1 by A7,A9,XXREAL_0:1;
then
A11: j <= k by NAT_1:13;
1 <= j by A10,FINSEQ_1:1;
then j in Seg k by A11;
then
A12: j in dom f1 by A4,FINSEQ_1:def 3;
then f1.j = f.j by FUNCT_1:47;
then Product(f1) = 0 by A2,A4,A9,A12;
hence Product(f) = 0 by A5;
end;
end;
hence thesis;
end;
A13: P[0] proof let f be complex-valued FinSequence;
assume len f = 0;
then Seg len f = {};
hence thesis by FINSEQ_1:def 3;
end;
A14: for k being Nat holds P[k] from NAT_1:sch 2(A13,A1);
A15: ex j being Nat st len m = j;
assume ex i being Nat st i in dom m & m.i = 0;
hence thesis by A14,A15;
end;
theorem Th7:
for n,a,b being Integer holds (a - b) mod n = ((a mod n) - (b mod n)) mod n
proof
let n,a,b be Integer;
per cases;
suppose
A1: n = 0;
hence (a - b) mod n = 0
.= ((a mod n) - (b mod n)) mod n by A1;
end;
suppose
A2: n <> 0;
then
A3: b mod n + (b div n) * n = (b - (b div n) * n) + (b div n) * n by
INT_1:def 10;
a mod n + (a div n) * n = (a - (a div n) * n) + (a div n) * n by A2,
INT_1:def 10;
then (a - b) - ((a mod n) - (b mod n)) = ((a div n) - (b div n)) * n by A3;
then n divides (a - b) - ((a mod n) - (b mod n)) by INT_1:def 3;
hence thesis by NAT_D:64,INT_2:15;
end;
end;
theorem Th8:
for i,j,k being Integer st i divides j holds k*i divides k*j
proof
let i,j,k be Integer;
assume i divides j;
then consider z being Integer such that
A1: i * z = j by INT_1:def 3;
(i*k)*z = j * k by A1;
hence thesis by INT_1:def 3;
end;
theorem Th9:
for m being integer-valued FinSequence, i being Nat holds
Product(m) / m.i is Integer
proof
let m be integer-valued FinSequence, i be Nat;
reconsider m2 = m/^i as FinSequence of INT;
reconsider m1 = m|i as FinSequence of INT by FINSEQ_1:102;
reconsider m9 = m as FinSequence of INT by FINSEQ_1:102;
per cases;
suppose not i in dom m or m.i = 0;
then m.i = 0 by FUNCT_1:def 2;
hence thesis;
end;
suppose that
A1: i in dom m and
A2: m.i <> 0;
A3: dom m = Seg(len m) by FINSEQ_1:def 3;
then 1 <= i by A1,FINSEQ_1:1;
then reconsider j = i - 1 as Element of NAT by INT_1:3;
set f = (m|j) ^ (m/^i);
A4: m9 = m1 ^ m2 by RFINSEQ:8;
j + 1 <= len m by A1,A3,FINSEQ_1:1;
then (m|j) ^ <*m.i*> = (m|i) by Th5;
then Product(m) = Product(m|j ^ <*m.i*>) * Product(m/^i) by A4,RVSUM_1:97
.= Product(m|j) * Product(<*m.i*>) * Product(m/^i) by RVSUM_1:97
.= (Product(m|j) * Product(m/^i)) * Product(<*m.i*>)
.= Product(m|j) * Product(m/^i) * m.i
.= Product(f) * m.i by RVSUM_1:97;
then m.i divides Product(m) by INT_1:def 3;
hence thesis by A2,WSIERP_1:17;
end;
end;
registration
let m be integer-valued FinSequence, i be Nat;
cluster Product(m) / m.i -> integer;
coherence by Th9;
end;
theorem Th10:
for m being INT-valued FinSequence, i being Nat
st i in dom m ex z being Integer st z * m.i = Product(m)
proof
let m be INT-valued FinSequence, i be Nat;
assume
A1: i in dom m;
per cases;
suppose
A2: m.i <> 0;
take z = Product(m) / m.i;
thus z * m.i = Product(m) * ((m.i)" * m.i)
.= Product(m) * 1 by A2,XCMPLX_0:def 7
.= Product(m);
end;
suppose
A3: m.i = 0;
take 1;
thus thesis by A1,A3,Th6;
end;
end;
Lm6: for m being INT-valued FinSequence, i,j being Nat st
i in dom m & j <> i
ex z being Integer st z * m.i = Product(m) / m.j
proof
let m be INT-valued FinSequence, i9,j9 be Nat;
reconsider m9 = m as FinSequence of INT by FINSEQ_1:102;
assume that
A1: i9 in dom m and
A3: j9 <> i9;
per cases;
suppose that
A2: j9 in dom m and
A4: m.j9 <> 0;
reconsider i = i9, j = j9 as Element of NAT by ORDINAL1:def 12;
A5: dom m = Seg len m by FINSEQ_1:def 3;
then
A6: j <= len m by A2,FINSEQ_1:1;
A7: 1 <= j by A2,A5,FINSEQ_1:1;
then reconsider kj = j - 1 as Element of NAT by INT_1:3;
set f = (m|kj) ^ (m/^j);
reconsider f as FinSequence of INT by FINSEQ_1:102;
kj + 1 = j;
then kj <= j by NAT_1:11;
then
A8: len(m|kj) = kj by A6,FINSEQ_1:59,XXREAL_0:2;
A9: dom m = Seg(len m) by FINSEQ_1:def 3;
then
A10: 1 <= i by A1,FINSEQ_1:1;
then reconsider ki = i - 1 as Element of NAT by INT_1:3;
A11: i <= len m by A1,A9,FINSEQ_1:1;
ex l being Element of NAT st l in dom f & f.l = m.i
proof
per cases by A3,XXREAL_0:1;
suppose
A12: i < j;
A13: dom(m|kj) c= dom f by FINSEQ_1:26;
i < kj + 1 by A12;
then i <= j - 1 by NAT_1:13;
then i in Seg kj by A10;
then
A14: i in dom(m|kj) by A8,FINSEQ_1:def 3;
then (m|kj).i = m.i by FUNCT_1:47;
then f.i = m.i by A14,FINSEQ_1:def 7;
hence thesis by A14,A13;
end;
suppose
A15: i > j;
then reconsider a = i-1 - kj as Element of NAT by INT_1:5,XREAL_1:9;
i - kj > (kj + 1) - kj by A15,XREAL_1:9;
then i - kj - 1 > 1 - 1 by XREAL_1:9;
then ex g being Nat st a = g + 1 by NAT_1:6;
then
A16: 1 <= i-1 - kj by NAT_1:11;
A17: len(m/^j) = len m - j by A6,RFINSEQ:def 1;
then len f = kj + (len(m) - j) by A8,FINSEQ_1:22
.= len(m) - 1;
then
A18: ki <= len f by A11,XREAL_1:9;
i - j <= len m - j by A11,XREAL_1:9;
then a in Seg len(m/^j) by A17,A16;
then
A19: i-1 - kj in dom(m9/^j) by FINSEQ_1:def 3;
ki + 1 > 1 by A7,A15,XXREAL_0:2;
then ki >= 1 by NAT_1:13;
then ki in Seg(len f) by A18;
then
A20: ki in dom f by FINSEQ_1:def 3;
reconsider D = INT as set;
reconsider ww = m9 as FinSequence of D;
len(m|kj) < i-1 by A8,A15,XREAL_1:9;
then f.ki = (m/^j).(ki-kj) by A8,A18,FINSEQ_1:24
.= (ww/^j)/.(ki - kj) by A19,PARTFUN1:def 6
.= ww/.(j+a) by A19,FINSEQ_5:27
.= m.i by A1,PARTFUN1:def 6;
hence thesis by A20;
end;
end;
then consider l being Element of NAT such that
A21: l in dom f and
A22: f.l = m.i;
l in Seg(len f) by A21,FINSEQ_1:def 3;
then 1 <= l by FINSEQ_1:1;
then reconsider kl = l - 1 as Element of NAT by INT_1:5;
l in Seg(len f) by A21,FINSEQ_1:def 3;
then kl + 1 <= len f by FINSEQ_1:1;
then (f|kl) ^ <*f.l*> = (f|l) by Th5;
then f = (f|kl) ^ <*f.l*> ^ (f/^l) by RFINSEQ:8;
then
A23: Product(f) = Product((f|kl) ^ <*f.l*>) * Product(f/^l) by RVSUM_1:97
.= Product((f|kl)) * Product(<*f.l*>) * Product(f/^l) by RVSUM_1:97
.= (Product((f|kl)) * Product(f/^l)) * Product(<*m.i*>) by A22
.= Product((f|kl)) * Product(f/^l) * m.i
.= Product((f|kl) ^ (f/^l)) * m.i by RVSUM_1:97;
kj + 1 <= len m by A2,A5,FINSEQ_1:1;
then
A24: (m|kj) ^ <*m.j*> = (m|j) by Th5;
reconsider m2 = m/^j as FinSequence of INT;
reconsider m1 = m|j as FinSequence of INT by FINSEQ_1:102;
m9 = m1 ^ m2 by RFINSEQ:8;
then Product(m) = Product((m|kj) ^ <*m.j*>) * Product(m/^j) by A24,RVSUM_1:97
.= Product((m|kj)) * Product(<*m.j*>) * Product(m/^j) by RVSUM_1:97
.= (Product((m|kj))*Product(m/^j))*Product(<*m.j*>)
.= Product((m|kj)) * Product(m/^j) * m.j
.= Product(f) * m.j by RVSUM_1:97;
then Product(m) / m.j = Product(f) * (m.j * (m.j)")
.= Product(f) * 1 by A4,XCMPLX_0:def 7;
hence thesis by A23;
end;
suppose
k01: m.j9 = 0;
take 0;
0 * m.i9 = Product(m) / 0;
hence thesis by k01;
end;
suppose
k02: not j9 in dom m;
take 0;
0 * m.i9 = Product(m) / 0;
hence thesis by k02,FUNCT_1:def 2;
end;
end;
theorem
for m being INT-valued FinSequence, i,j being Nat st i <> j holds
Product(m) / (m.i * m.j) is Integer
proof
let m be INT-valued FinSequence, i9,j9 be Nat;
assume that
A3: j9 <> i9;
per cases;
suppose that
A1: i9 in dom m;
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,A3,Lm6;
per cases;
suppose m.i = 0;
hence thesis;
end;
suppose
A6: m.i <> 0;
reconsider u = Product(m) / m.j as Integer;
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 thesis by A6,A7,WSIERP_1:17;
end;
end;
suppose not i9 in dom m;
then m.i9 = 0 by FUNCT_1:def 2;
hence thesis;
end;
end;
theorem
for m being INT-valued FinSequence, i,j being Nat st i in dom m & i <> j
ex z being Integer st z * m.i = Product(m) / m.j by Lm6;
begin :: More on Greatest Common Divisors
theorem Th13:
for i being Integer holds |.i.| divides i & i divides |.i.|
proof
let i be Integer;
per cases by ABSVALUE:1;
suppose
|.i.| = i;
hence thesis;
end;
suppose
A1: |.i.| = -i;
then
A2: i * (-1) = |.i.|;
|.i.| * (-1) = i by A1;
hence thesis by A2,INT_1:def 3;
end;
end;
theorem Th14:
for i,j being Integer holds i gcd j = i gcd |.j.|
proof
let i,j be Integer;
set k = i gcd |.j.|;
k divides |.j.| by INT_2:def 2;
then consider x being Integer such that
A1: k*x = |.j.| by INT_1:def 3;
|.j.| divides j by Th13;
then consider y being Integer such that
A2: |.j.| * y = j by INT_1:def 3;
A3: for m being Integer st m divides i & m divides j holds m divides k
proof
j divides |.j.| by Th13;
then consider y being Integer such that
A4: j * y = |.j.| by INT_1:def 3;
let m be Integer;
assume that
A5: m divides i and
A6: m divides j;
consider x being Integer such that
A7: m * x = j by A6,INT_1:def 3;
m * (x * y) = |.j.| by A7,A4;
then m divides |.j.| by INT_1:def 3;
hence thesis by A5,INT_2:def 2;
end;
k * (x * y) = j by A1,A2;
then
A8: k divides j by INT_1:def 3;
k divides i by INT_2:def 2;
hence thesis by A8,A3,INT_2:def 2;
end;
theorem Th15:
for i,j being Integer st i,j are_coprime holds i lcm j = |.i * j.|
proof
let i,j be Integer;
assume
A1: i gcd j = 1;
per cases;
suppose
A2: i = 0 or j = 0;
hence i lcm j = 0 by INT_2:4
.= |.i*j.| by A2,ABSVALUE:2;
end;
suppose
A3: i <> 0 & j <> 0;
A4: for m being Integer st i divides m & j divides m holds |.i*j.| divides m
proof
j divides i lcm j by INT_2:def 1;
then consider kj being Integer such that
A5: j * kj = i lcm j by INT_1:def 3;
i divides i lcm j by INT_2:def 1;
then consider ki being Integer such that
A6: i * ki = i lcm j by INT_1:def 3;
A7: j divides i * j by INT_2:2;
i divides i * j by INT_2:2;
then i lcm j divides i * j by A7,INT_2:def 1;
then consider kij being Integer such that
A8: (i lcm j) * kij = i * j by INT_1:def 3;
i * j = j * (kj * kij) by A5,A8;
then i = kj * kij by A3,XCMPLX_1:5;
then
A9: kij divides i by INT_1:def 3;
i * j = i * (ki * kij) by A6,A8;
then j = ki * kij by A3,XCMPLX_1:5;
then kij divides j by INT_1:def 3;
then
A10: kij divides 1 by A1,A9,INT_2:def 2;
let m be Integer;
assume that
A11: i divides m and
A12: j divides m;
A13: i lcm j divides m by A11,A12,INT_2:def 1;
per cases by A10,INT_2:13;
suppose
kij = 1;
hence thesis by A8,A13,ABSVALUE:def 1;
end;
suppose
A14: kij = -1;
-(i * j) <> 0 by A3,XCMPLX_1:6;
then -(-(i * j)) < 0 by A8,A14;
hence thesis by A8,A13,A14,ABSVALUE:def 1;
end;
end;
j divides |.j.| by Th13;
then j divides |.i.| * |.j.| by INT_2:2;
then
A15: j divides |.i * j.| by COMPLEX1:65;
i divides |.i.| by Th13;
then i divides |.i.| * |.j.| by INT_2:2;
then i divides |.i * j.| by COMPLEX1:65;
hence thesis by A15,A4,INT_2:def 1;
end;
end;
theorem Th16:
for i,j,k being Integer holds (i*j) gcd (i*k) = |.i.| * (j gcd k)
proof
let i,j,k be Integer;
per cases;
suppose
A1: i = 0;
hence (i*j) gcd (i*k) = 0 * (j gcd k) by INT_2:5
.= |.i.| * (j gcd k) by A1,ABSVALUE:def 1;
end;
suppose
A2: i <> 0;
set d = j gcd k, e = (i*j) gcd (i*k);
per cases;
suppose
A3: d = 0;
then
A4: k = 0 by INT_2:5;
j = 0 by A3,INT_2:5;
hence thesis by A3,A4;
end;
suppose
A5: d <> 0;
A6: e divides i*k by INT_2:21;
A7: i * d divides i * k by Th8,INT_2:21;
i * d divides i * j by Th8,INT_2:21;
then i * d divides e by A7,INT_2:22;
then consider g being Integer such that
A8: e = (i * d) * g by INT_1:def 3;
A9: e divides i*j by INT_2:21;
d * g divides j & d * g divides k
proof
consider h1 being Integer such that
A10: ((i*d)*g)*h1 = i*j by A8,A9,INT_1:def 3;
i*((d*g)*h1) = i*j by A10;
then (d*g)*h1 = j by A2,XCMPLX_1:5;
hence d * g divides j by INT_1:def 3;
consider h2 being Integer such that
A11: ((i*d)*g)*h2 = i*k by A8,A6,INT_1:def 3;
i*((d*g)*h2) = i*k by A11;
then (d*g)*h2 = k by A2,XCMPLX_1:5;
hence thesis by INT_1:def 3;
end;
then d * g divides d by INT_2:22;
then consider h3 being Integer such that
A12: (d*g)*h3 = d by INT_1:def 3;
d*(g*h3) = d * 1 by A12;
then g*h3 = 1 by A5,XCMPLX_1:5;
then
A13: g divides 1 by INT_1:def 3;
per cases by A13,INT_2:13;
suppose
A14: g = 1;
i < 0 implies d*i < 0*i by A5,XREAL_1:69;
hence thesis by A8,A14,ABSVALUE:def 1;
end;
suppose
A15: g = -1;
A16: now
assume i > 0;
then -- i > 0;
then -i < 0;
hence d*(-i) < 0*(-i) by A5,XREAL_1:69;
end;
(i*j) gcd (i*k) = (-i)*d by A8,A15;
hence thesis by A2,A16,ABSVALUE:def 1;
end;
end;
end;
end;
theorem Th17:
for i,j being Integer holds (i * j) gcd i = |.i.|
proof
let i,j be Integer;
A1: for m being Integer st m divides i*j & m divides i holds m divides |.i.|
proof
let m be Integer;
assume that
m divides i*j and
A2: m divides i;
consider k being Integer such that
A3: m * k = i by A2,INT_1:def 3;
i divides |.i.| by Th13;
then consider l being Integer such that
A4: i * l = |.i.| by INT_1:def 3;
m * (k * l) = |.i.| by A3,A4;
hence thesis by INT_1:def 3;
end;
A5: |.i.| divides i by Th13;
then |.i.| divides i*j by INT_2:2;
hence thesis by A5,A1,INT_2:def 2;
end;
theorem Th18:
for i,j,k being Integer holds i gcd (j gcd k) = (i gcd j) gcd k
proof
let i,j,k be Integer;
per cases;
suppose
i = 0 & j = 0 & k = 0;
hence thesis;
end;
suppose
A1: i <> 0 or j <> 0 or k <> 0;
A2: now
assume i gcd (j gcd k) = -((i gcd j) gcd k);
then (-((i gcd j) gcd k)) * (-1) <= 0 * (-1);
then
A3: (i gcd j) gcd k = 0;
then i gcd j = 0 by INT_2:5;
hence contradiction by A1,A3,INT_2:5;
end;
A4: i gcd (j gcd k) divides i by INT_2:21;
A5: (i gcd j) gcd k divides k by INT_2:21;
A6: (i gcd j) gcd k divides i gcd j by INT_2:21;
i gcd j divides j by INT_2:21;
then (i gcd j) gcd k divides j by A6,INT_2:9;
then
A7: (i gcd j) gcd k divides j gcd k by A5,INT_2:22;
i gcd j divides i by INT_2:21;
then (i gcd j) gcd k divides i by A6,INT_2:9;
then
A8: (i gcd j) gcd k divides i gcd (j gcd k) by A7,INT_2:22;
A9: i gcd (j gcd k) divides j gcd k by INT_2:21;
j gcd k divides j by INT_2:21;
then i gcd (j gcd k) divides j by A9,INT_2:9;
then
A10: i gcd (j gcd k) divides i gcd j by A4,INT_2:22;
j gcd k divides k by INT_2:21;
then i gcd (j gcd k) divides k by A9,INT_2:9;
then i gcd (j gcd k) divides (i gcd j) gcd k by A10,INT_2:22;
hence thesis by A8,A2,INT_2:11;
end;
end;
theorem Th19:
for i,j,k being Integer st i,j are_coprime holds i gcd (j
* k) = i gcd k
proof
let i,j,k be Integer;
assume
A1: i gcd j = 1;
(i*k) gcd (j*k) = |.k.| * (i gcd j) by Th16;
then i gcd |.k.| = (i gcd (i*k)) gcd (j*k) by A1,Th18
.= |.i.| gcd (j*k) by Th17
.= (j*k) gcd i by Th14;
hence thesis by Th14;
end;
theorem Th20:
for i,j being Integer st i,j are_coprime holds i * j divides i lcm j
proof
let i,j be Integer;
assume i,j are_coprime;
then |.i * j.| divides i lcm j by Th15;
then consider z being Integer such that
A1: |.i*j.| * z = (i lcm j) by INT_1:def 3;
per cases;
suppose
0 <= i*j;
then z*(i*j) = (i lcm j) by A1,ABSVALUE:def 1;
hence thesis by INT_1:def 3;
end;
suppose
A2: 0 > i*j;
(-z)*(i*j) = z*(-(i*j)) .= (i lcm j) by A1,A2,ABSVALUE:def 1;
hence thesis by INT_1:def 3;
end;
end;
theorem Th21:
for x,y,i,j being Integer st i,j are_coprime holds x,y
are_congruent_mod i & x,y are_congruent_mod j implies x,y are_congruent_mod i*j
proof
let x,y,i,j be Integer;
assume i,j are_coprime;
then
A1: i * j divides i lcm j by Th20;
assume that
A2: x,y are_congruent_mod i and
A3: x,y are_congruent_mod j;
A4: j divides (x - y) by A3,INT_2:15;
i divides (x - y) by A2,INT_2:15;
then i lcm j divides (x - y) by A4,INT_2:19;
then i*j divides (x - y) by A1,INT_2:9;
hence thesis by INT_2:15;
end;
theorem Th22:
for i,j being Integer st i,j are_coprime holds ex s being
Integer st s*i,1 are_congruent_mod j
proof
let i,j be Integer;
assume i gcd j = 1;
then consider s,t being Integer such that
A1: 1 = s * i + t * j by NAT_D:68;
take s;
s * i - 1 = (-t) * j by A1;
then j divides (s*i - 1) by INT_1:def 3;
hence thesis by INT_2:15;
end;
begin :: Chinese Remainder Sequences
notation
let f be integer-valued Function;
antonym f is multiplicative-trivial↑ for f is non-empty;
end;
definition
let f be integer-valued FinSequence;
redefine attr f is multiplicative-trivial means :: redefines multiplicative-trivial (INT_6, antonym) → non-empty (FUNCT_1, redefinition) → non-empty (RELAT_1, definition)
:Def1:
ex i being Nat st i in dom f & f.i = 0;
compatibility;
end;
Lm7: for u be object st u in {1} holds u in INT by INT_1:def 1;
registration
cluster multiplicative-trivial for INT-valued FinSequence;
existence
proof
set p = <*0*>;
for u be object st u in {0} holds u in INT by INT_1:def 1;
then {0} c= INT by TARSKI:def 3;
then rng p c= INT by FINSEQ_1:39;
then reconsider f = p as FinSequence of INT by FINSEQ_1:def 4;
take f;
take 1;
len f = 1 by FINSEQ_1:40;
then dom f = Seg 1 by FINSEQ_1:def 3;
hence 1 in dom f;
thus thesis;
end;
cluster non multiplicative-trivial for INT-valued FinSequence;
existence by Def1;
cluster non empty positive-yielding for INT-valued FinSequence;
existence
proof
set p = <*1*>;
{1} c= INT by Lm7,TARSKI:def 3;
then rng p c= INT by FINSEQ_1:39;
then reconsider f = p as FinSequence of INT by FINSEQ_1:def 4;
take f;
now
let r be Real;
assume r in rng f;
then r in {1} by FINSEQ_1:39;
hence 0 < r by TARSKI:def 1;
end;
hence thesis by PARTFUN3:def 1;
end;
end;
theorem
for m being multiplicative-trivial INT-valued FinSequence holds
Product(m) = 0
proof
let m be multiplicative-trivial INT-valued FinSequence;
ex i being Nat st i in dom m & m.i = 0 by Def1;
hence thesis by Th6;
end;
definition
let f be integer-valued Function;
attr f is Chinese_Remainder means
:Def2:
for i,j being Nat st i in dom f & j in dom f & i <> j holds
f.i, f.j are_coprime;
end;
registration
cluster non empty positive-yielding Chinese_Remainder for INT-valued
FinSequence;
existence
proof
set p = <*1*>;
{1} c= INT by Lm7,TARSKI:def 3;
then rng p c= INT by FINSEQ_1:39;
then reconsider f = p as FinSequence of INT by FINSEQ_1:def 4;
take f;
A1: now
let i be Element of NAT;
assume i in dom f;
then i in Seg 1 by FINSEQ_1:38;
hence i = 1 by FINSEQ_1:2,TARSKI:def 1;
end;
A2: now
let i9,j9 be Nat;
assume that
A3: i9 in dom f and
A4: j9 in dom f and
A5: i9 <> j9;
reconsider i = i9,j = j9 as Element of NAT by ORDINAL1:def 12;
i = 1 by A1,A3
.= j by A1,A4;
hence f.i9, f.j9 are_coprime by A5;
end;
now
let r be Real;
assume r in rng f;
then r in {1} by FINSEQ_1:39;
hence 0 < r by TARSKI:def 1;
end;
hence thesis by A2,PARTFUN3:def 1;
end;
end;
definition
mode CR_Sequence is non empty positive-yielding Chinese_Remainder
INT-valued FinSequence;
end;
registration
cluster -> non multiplicative-trivial for CR_Sequence;
coherence
proof
let f be CR_Sequence;
now
let i be Nat;
assume i in dom f;
then f.i in rng f by FUNCT_1:3;
hence f.i <> 0 by PARTFUN3:def 1;
end;
hence thesis;
end;
end;
registration
cluster multiplicative-trivial -> non empty for INT-valued FinSequence;
coherence;
end;
theorem Th24:
for f being CR_Sequence, m being Nat st 0 < m & m <=
len f holds f|m is CR_Sequence
proof
let f be CR_Sequence, m be Nat;
reconsider fm = f|m as FinSequence of INT by FINSEQ_1:102;
assume that
A1: m > 0 and
A2: m <= len f;
A3: len fm = m by A2,FINSEQ_1:59;
A4: now
let i be Element of NAT;
assume i in dom fm;
then
A5: i in Seg m by A3,FINSEQ_1:def 3;
then i <= m by FINSEQ_1:1;
then
A6: i <= len f by A2,XXREAL_0:2;
1 <= i by A5,FINSEQ_1:1;
then i in Seg(len f) by A6;
hence i in dom f by FINSEQ_1:def 3;
end;
A7: now
let i9,j9 be Nat;
assume that
A8: i9 in dom fm and
A9: j9 in dom fm and
A10: i9 <> j9;
reconsider i = i9,j = j9 as Element of NAT by ORDINAL1:def 12;
A11: f.i = fm.i by A8,FUNCT_1:47;
A12: f.j = fm.j by A9,FUNCT_1:47;
A13: j in dom f by A4,A9;
i in dom f by A4,A8;
hence fm.i9, fm.j9 are_coprime by A10,A13,A11,A12,Def2;
end;
now
let r be Real;
assume r in rng fm;
then consider i being object such that
A14: i in dom fm and
A15: fm.i = r by FUNCT_1:def 3;
reconsider i as Element of NAT by A14;
f.i in rng f by A4,A14,FUNCT_1:3;
then f.i > 0 by PARTFUN3:def 1;
hence r > 0 by A14,A15,FUNCT_1:47;
end;
hence thesis by A1,A7,Def2,PARTFUN3:def 1;
end;
Lm8: for m being CR_Sequence holds Product(m) > 0
proof
defpred P[Nat] means for f being CR_Sequence st len f = $1 holds Product(f)
> 0;
let m be CR_Sequence;
A1: ex j being Nat st len m = j;
A2: for k being Nat st P[k] holds P[k + 1]
proof
let k be Nat;
assume
A3: P[k];
now
let f be CR_Sequence;
assume
A4: len f = k + 1;
set f1 = f|k;
per cases;
suppose
k > 0;
then reconsider f1 as CR_Sequence by A4,Th24,NAT_1:11;
A5: f = f1^<*f.(k+1)*> by A4,FINSEQ_3:55;
1 <= k + 1 by NAT_1:11;
then k + 1 in Seg(k+1);
then k+1 in dom f by A4,FINSEQ_1:def 3;
then f.(k+1) in rng f by FUNCT_1:3;
then
A6: f.(k+1) > 0 by PARTFUN3:def 1;
len f1 = k by A4,FINSEQ_1:59,NAT_1:11;
then Product(f1) > 0 by A3;
then 0 * f.(k+1) < Product(f1) * f.(k+1) by A6,XREAL_1:68;
hence Product(f) > 0 by A5,RVSUM_1:96;
end;
suppose
k = 0;
then
A7: f = <*f.1*> by A4,FINSEQ_1:40;
then dom f = Seg 1 by FINSEQ_1:38;
then 1 in dom f;
then f.1 in rng f by FUNCT_1:3;
then f.1 > 0 by PARTFUN3:def 1;
hence Product(f) > 0 by A7;
end;
end;
hence thesis;
end;
A8: P[0];
for k being Nat holds P[k] from NAT_1:sch 2(A8,A2);
hence thesis by A1;
end;
registration
let m be CR_Sequence;
cluster Product(m) -> positive natural;
coherence
proof
Product(m) > 0 by Lm8;
then Product(m) is Element of NAT by INT_1:3;
hence thesis by Lm8;
end;
end;
theorem Th25:
for m being CR_Sequence, i being Nat st i in dom m
for mm being Integer st mm = Product(m) / m.i holds mm, m.i are_coprime
proof
defpred P[Nat] means for m being CR_Sequence st len m = $1 for i being
Nat st i in dom m for mm being Integer st mm = Product(m) / m.i
holds mm, m.i are_coprime;
let m be CR_Sequence, i be Nat;
assume
A1: i in dom m;
let mm be Integer;
A2: ex l be Element of NAT st len m = l;
A3: now
let k be Nat;
assume
A4: P[k];
now
let m be CR_Sequence;
set m1 = m|k;
assume
A5: len m = k+1;
then
A6: m1 ^ <*m.(k+1)*> = m|(k+1) by Th5
.= m by A5,FINSEQ_1:58;
A7: len m1 = k by A5,FINSEQ_1:59,NAT_1:11;
1 <= k + 1 by NAT_1:11;
then k+1 in Seg(k+1);
then
A8: k+1 in dom m by A5,FINSEQ_1:def 3;
let i9 be Nat;
reconsider i = i9 as Element of NAT by ORDINAL1:def 12;
assume
A9: i9 in dom m;
then
A10: i in Seg(k+1) by A5,FINSEQ_1:def 3;
then
A11: i <= k + 1 by FINSEQ_1:1;
let mm be Integer;
assume
A12: mm = Product(m) / m.i9;
per cases;
suppose
k > 0;
then reconsider m1 as CR_Sequence by A5,Th24,NAT_1:11;
per cases;
suppose
A13: i in dom m1;
then i in Seg(k) by A7,FINSEQ_1:def 3;
then i <= k by FINSEQ_1:1;
then i <> k + 1 by NAT_1:13;
then
A14: m.i, m.(k+1) are_coprime by A9,A8,Def2;
reconsider mm1 = Product(m1) / m1.i as Integer;
A15: m1.i = m.i by A13,FUNCT_1:47;
then mm1, m.i are_coprime by A4,A7,A13;
then
A16: m.i gcd (mm1 * m.(k+1)) = m.i gcd m.(k+1) by Th19
.= 1 by A14;
mm1 * m.(k+1) = (Product(m1) * m.(k+1)) * (m.i)" by A15
.= mm by A12,A6,RVSUM_1:96;
hence mm, m.i9 are_coprime by A16;
end;
suppose
A17: not i in dom m1;
m.(k+1) in rng m by A8,FUNCT_1:3;
then
A18: m.(k+1) > 0 by PARTFUN3:def 1;
defpred Q[Nat] means $1 <= len m1 implies for s being Element of NAT
st s = $1 holds Product(m1|s), m.(k+1) are_coprime;
A19: m1|(len m1) = m1 by FINSEQ_1:58;
A20: now
let j be Element of NAT;
assume that
0 <= j and
A21: j < len m1;
assume
A22: Q[j];
now
assume
A23: j+1 <= len m1;
A24: 0 + 1 <= j + 1 by XREAL_1:6;
then j+1 in Seg(len m1) by A23;
then
A25: j+1 in dom m1 by FINSEQ_1:def 3;
j + 1 <= len m by A5,A7,A21,XREAL_1:8;
then j+1 in Seg(len m) by A24;
then
A26: j+1 in dom m by FINSEQ_1:def 3;
j+1 <= k by A5,A23,FINSEQ_1:59,NAT_1:11;
then
A27: j+1 <> k+1 by NAT_1:13;
now
reconsider s9 = j as Element of NAT;
let s be Element of NAT;
A28: m1.(j+1) = m.(j+1) by A25,FUNCT_1:47;
A29: m.(j+1), m.(k+1) are_coprime by A8,A27,A26,Def2;
j <= j + 1 by NAT_1:11;
then
Product(m1|s9), m.(k+1) are_coprime by A22,A23,XXREAL_0:2;
then
A30: Product(m1|s9) * m.(j+1) gcd m.(k+1) = m.(j+1) gcd m.(k+1
) by Th19
.= 1 by A29;
assume
A31: s = j+1;
then m1|s9 ^ <*m1.s*> = m1|s by A23,Th5;
then Product(m1|s) gcd m.(k+1) = 1 by A31,A30,A28,RVSUM_1:96;
hence Product(m1|s), m.(k+1) are_coprime;
end;
hence Q[j+1];
end;
hence Q[j+1];
end;
m1|0 is empty;
then
A32: Q[0] by RVSUM_1:94,WSIERP_1:9;
A33: for j being Element of NAT st 0 <= j & j <= len m1 holds Q[j]
from INT_1:sch 7(A32,A20);
not i in Seg k by A7,A17,FINSEQ_1:def 3;
then not(1 <= i & i <= k);
then not i < k + 1 by A10,FINSEQ_1:1,NAT_1:13;
then
A34: i = k + 1 by A11,XXREAL_0:1;
then mm = (Product(m1)*m.(k+1))*(m.(k+1))" by A12,A6,RVSUM_1:96
.= Product(m1)* (m.(k+1)*(m.(k+1))")
.= Product(m1) * 1 by A18,XCMPLX_0:def 7;
hence mm, m.i9 are_coprime by A34,A33,A19;
end;
end;
suppose
k = 0;
then
A35: m = <*m.1*> by A5,FINSEQ_1:40;
then
A36: dom m = Seg 1 by FINSEQ_1:38;
then
A37: i <= 1 by A9,FINSEQ_1:1;
1 <= i by A9,A36,FINSEQ_1:1;
then
A38: i = 1 by A37,XXREAL_0:1;
Product(m) = m.1 by A35;
then mm = 1 by A12,A38,XCMPLX_0:def 7;
hence mm, m.i9 are_coprime by WSIERP_1:9;
end;
end;
hence P[k+1];
end;
A39: P[0];
A40: for k be Nat holds P[k] from NAT_1:sch 2(A39,A3);
assume mm = Product(m) / m.i;
hence thesis by A1,A40,A2;
end;
Lm9: for u being INT-valued FinSequence, m being CR_Sequence for z1,z2
being Integer st 0 <= z1 & z1 < Product(m) & (for i being Nat st i
in dom m holds z1,u.i are_congruent_mod m.i) & 0 <= z2 & z2 < Product(m) & (for
i being Nat st i in dom m holds z2,u.i are_congruent_mod m.i) holds
z1 = z2
proof
let u be INT-valued FinSequence, m be CR_Sequence;
let z1,z2 being Integer;
assume that
A1: 0 <= z1 and
A2: z1 < Product(m) and
A3: for i being Nat st i in dom m holds z1,u.i
are_congruent_mod m.i and
A4: 0 <= z2 and
A5: z2 < Product(m) and
A6: for i being Nat st i in dom m holds z2,u.i
are_congruent_mod m.i;
defpred P[Nat] means for m1 being CR_Sequence st m1 = m|($1) holds z1, z2
are_congruent_mod Product(m1);
A7: now
let i be Element of NAT;
assume
A8: i in dom m;
then
A9: u.i,z2 are_congruent_mod m.i by A6,INT_1:14;
z1,u.i are_congruent_mod m.i by A3,A8;
hence z1,z2 are_congruent_mod m.i by A9,INT_1:15;
end;
A10: now
let k be Element of NAT;
assume that
0 <= k and
A11: k < len m;
assume
A12: P[k];
now
set m2 = m|k;
let m1 be CR_Sequence;
A13: 1 <= k + 1 by NAT_1:11;
A14: k+1 <= len m by A11,NAT_1:13;
then k+1 in Seg(len m) by A13;
then
A15: k+1 in dom m by FINSEQ_1:def 3;
assume
A16: m1 = m|(k+1);
then
A17: len m1 = k + 1 by A14,FINSEQ_1:59;
then k+1 in Seg(len m1) by A13;
then
A18: k+1 in dom m1 by FINSEQ_1:def 3;
per cases;
suppose
k > 0;
then reconsider m2 as CR_Sequence by A11,Th24;
set mm = Product(m1) / m1.(k+1);
A19: z1, z2 are_congruent_mod Product(m2) by A12;
reconsider m9 = m as FinSequence of INT by FINSEQ_1:102;
A20: m.(k+1) = m1.(k+1) by A16,A18,FUNCT_1:47;
m.(k+1) in rng m by A15,FUNCT_1:3;
then
A21: m1.(k+1) > 0 by A20,PARTFUN3:def 1;
reconsider mm as Integer;
A22: mm * m1.(k+1) = Product(m1) * ((m1.(k+1))" * m1.(k+1))
.= Product(m1) * 1 by A21,XCMPLX_0:def 7
.= Product(m1);
(m9|(k+1))|k = m9|k by FINSEQ_1:82,NAT_1:11;
then m1 = m2^<*m1.(k+1)*> by A16,A17,FINSEQ_3:55;
then Product(m1) = Product(m2) * m1.(k+1) by RVSUM_1:96;
then mm = Product(m2) * (m1.(k+1) * (m1.(k+1))");
then
A23: mm = Product(m2) * 1 by A21,XCMPLX_0:def 7;
z1, z2 are_congruent_mod m1.(k+1) by A7,A15,A20;
hence z1,z2 are_congruent_mod Product m1 by A18,A19,A23,A22,Th21,Th25;
end;
suppose
k = 0;
then
A24: m1 = <*m1.1*> by A17,FINSEQ_1:40;
then dom m1 = Seg 1 by FINSEQ_1:38;
then
A25: 1 in dom m1;
1 <= len m by A14,A13,XXREAL_0:2;
then 1 in Seg(len m);
then
A26: 1 in dom m by FINSEQ_1:def 3;
Product(m1) = m1.1 by A24
.= m.1 by A16,A25,FUNCT_1:47;
hence z1,z2 are_congruent_mod Product(m1) by A7,A26;
end;
end;
hence P[k+1];
end;
A27: m|(len m) = m by FINSEQ_1:58;
A28: P[0];
for k being Element of NAT st 0 <= k & k <= len m holds P[k] from
INT_1:sch 7(A28,A10);
then
A29: z1, z2 are_congruent_mod Product(m) by A27;
thus z1 = z1 mod Product(m) by A1,A2,NAT_D:63
.= z2 mod Product(m) by A29,NAT_D:64
.= z2 by A4,A5,NAT_D:63;
end;
begin :: Integer Arithmetic based on CRT
definition
let u be Integer, m be integer-valued FinSequence;
func mod(u,m) -> FinSequence means
:Def3:
len it = len m & for i being
Nat st i in dom it holds it.i = u mod m.i;
existence
proof
defpred P[set,set] means $2 = u mod m.($1);
A1: for k being Nat st k in Seg(len m) ex x being Element of INT st P[k,x]
proof
let k be Nat;
assume k in Seg(len m);
reconsider j = u mod (m.k) as Element of INT by INT_1:def 2;
take j;
thus thesis;
end;
consider p being FinSequence of INT such that
A2: dom p = Seg len m & for k being Nat st k in Seg len m holds P[k,p.
k] from FINSEQ_1:sch 5(A1);
take p;
thus len p = len m by A2,FINSEQ_1:def 3;
thus thesis by A2;
end;
uniqueness
proof
let z1,z2 be FinSequence;
assume that
A3: len z1 = len m and
A4: for i being Nat st i in dom z1 holds z1.i = u mod (m.i);
assume that
A5: len z2 = len m and
A6: for i being Nat st i in dom z2 holds z2.i = u mod (m.i);
A7: dom z1 = Seg len z1 by FINSEQ_1:def 3
.= dom z2 by A3,A5,FINSEQ_1:def 3;
now
let x be object;
assume
A8: x in dom z1;
then reconsider x9 = x as Element of NAT;
thus z1.x = u mod (m.x9) by A4,A8
.= z2.x by A6,A7,A8;
end;
hence thesis by A7;
end;
end;
registration
let u be Integer, m be INT-valued FinSequence;
cluster mod(u,m) -> INT-valued;
coherence
proof
now
let y be object;
assume y in rng mod(u,m);
then consider x being object such that
A1: x in dom mod(u,m) and
A2: mod(u,m).x = y by FUNCT_1:def 3;
reconsider x as Element of NAT by A1;
reconsider x as Nat;
y = u mod m.x by A1,A2,Def3;
hence y in INT by INT_1:def 2;
end;
then rng mod(u,m) c= INT by TARSKI:def 3;
hence thesis by RELAT_1:def 19;
end;
end;
definition
let m be CR_Sequence;
mode CR_coefficients of m -> FinSequence means
:Def4:
len it = len m & for i
being Nat st i in dom it holds ex s being Integer, mm being Integer
st mm = Product(m) / m.i & s * mm, 1 are_congruent_mod m.i & it.i = s * (
Product(m) / m.i);
existence
proof
defpred P[set,set] means ex s being Integer, mm being Integer st mm =
Product(m) / m.$1 & s * mm, 1 are_congruent_mod m.$1 & $2 = s * (Product(m) / m
.$1);
A1: for k being Nat st k in Seg len m ex x being Element of INT st P[k,x]
proof
let k be Nat;
assume k in Seg(len m);
then
A2: k in dom m by FINSEQ_1:def 3;
reconsider mm = Product(m) / m.k as Integer;
consider s being Integer such that
A3: s * mm, 1 are_congruent_mod m.k by A2,Th22,Th25;
set x = s * mm;
reconsider x as Element of INT by INT_1:def 2;
take x;
take s;
take mm;
thus thesis by A3;
end;
consider p being FinSequence of INT such that
A4: dom p = Seg len m & for k being Nat st k in Seg len m holds P[k,p.
k] from FINSEQ_1:sch 5(A1);
take p;
thus thesis by A4,FINSEQ_1:def 3;
end;
end;
registration
let m be CR_Sequence;
cluster -> INT-valued for CR_coefficients of m;
coherence
proof
let c be CR_coefficients of m;
now
let u be object;
assume u in rng c;
then consider x being object such that
A1: x in dom c and
A2: c.x = u by FUNCT_1:def 3;
reconsider x as Element of NAT by A1;
reconsider x as Nat;
ex s being Integer, mm being Integer st mm = Product(m) / m.x & s
* mm, 1 are_congruent_mod m.x & c.x = s * (Product(m) / m.x) by A1,Def4;
hence u in INT by A2,INT_1:def 2;
end;
then rng c c= INT by TARSKI:def 3;
hence thesis by RELAT_1:def 19;
end;
end;
theorem Th26:
for m being CR_Sequence, c being CR_coefficients of m, i being
Nat st i in dom c holds c.i,1 are_congruent_mod m.i
proof
let m be CR_Sequence, c be CR_coefficients of m, i be Nat;
assume i in dom c;
then
ex s being Integer, mm being Integer st mm = Product(m) / m.i & s * mm
, 1 are_congruent_mod m.i & c.i = s * (Product(m) / m.i) by Def4;
hence thesis;
end;
theorem Th27:
for m being CR_Sequence, c being CR_coefficients of m, i,j being
Nat st i in dom c & j in dom c & i <> j holds c.i,0
are_congruent_mod m.j
proof
let m be CR_Sequence, c be CR_coefficients of m, i,j be Nat;
assume that
A1: i in dom c and
A2: j in dom c and
A3: i <> j;
consider s being Integer, mm being Integer such that
A4: mm = Product(m) / m.i and
s * mm, 1 are_congruent_mod m.i and
A5: c.i = s * (Product(m) / m.i) by A1,Def4;
len m = len c by Def4;
then dom m = Seg(len c) by FINSEQ_1:def 3
.= dom c by FINSEQ_1:def 3;
then consider z being Integer such that
A6: z * m.j = mm by A2,A3,A4,Lm6;
A7: m.j, 0 are_congruent_mod m.j by INT_1:12;
A8: s,s are_congruent_mod m.j by INT_1:11;
z,z are_congruent_mod m.j by INT_1:11;
then z * m.j, z*0 are_congruent_mod m.j by A7,INT_1:18;
then s * mm, s * 0 are_congruent_mod m.j by A6,A8,INT_1:18;
hence thesis by A4,A5;
end;
theorem
for m being CR_Sequence, c1,c2 being CR_coefficients of m, i being
Nat st i in dom c1 holds c1.i,c2.i are_congruent_mod m.i
proof
let m be CR_Sequence, c1,c2 be CR_coefficients of m, i be Nat;
assume
A1: i in dom c1;
then
A2: ex s1 being Integer, mm1 being Integer st mm1 = Product(m ) / m.i & s1
* mm1, 1 are_congruent_mod m.i & c1.i = s1 * (Product(m) / m.i) by Def4;
A3: len c1 = len m by Def4
.= len c2 by Def4;
dom c1 = Seg(len c1) by FINSEQ_1:def 3
.= dom c2 by A3,FINSEQ_1:def 3;
then consider s2 being Integer, mm2 being Integer such that
A4: mm2 = Product(m) / m.i and
A5: s2 * mm2, 1 are_congruent_mod m.i and
A6: c2.i = s2 * (Product(m) / m.i) by A1,Def4;
1, s2 * mm2 are_congruent_mod m.i by A5,INT_1:14;
hence thesis by A2,A4,A6,INT_1:15;
end;
theorem Th29:
for u being INT-valued FinSequence, m being CR_Sequence st
len m = len u for c being CR_coefficients of m, i being Nat st i in
dom m holds Sum(u(#)c),u.i are_congruent_mod m.i
proof
let u be INT-valued FinSequence, m be CR_Sequence;
assume
A1: len m = len u;
let c be CR_coefficients of m, i be Nat;
defpred P[Nat] means for v,cc being INT-valued FinSequence st v = u|(
$1) & cc = c|($1) holds ($1 < i & Sum(v(#)cc), 0 are_congruent_mod m.i) or ($1
>= i & Sum(v(#)cc), u.i are_congruent_mod m.i);
assume
A2: i in dom m;
A3: len m = len c by Def4;
then
A4: dom m = Seg(len c) by FINSEQ_1:def 3
.= dom c by FINSEQ_1:def 3;
A5: now
let k be Element of NAT;
assume that
0 <= k and
A6: k < len u and
A7: P[k];
now
set v9 = u|k, cc9 = c|k;
let v,cc be INT-valued FinSequence;
A8: 0 + 1 <= k + 1 by XREAL_1:6;
reconsider a = v(#)cc, b = v9(#)cc9 as FinSequence of REAL
by FINSEQ_1:102;
assume that
A9: v = u|(k+1) and
A10: cc = c|(k+1);
k+1 <= len u by A6,NAT_1:13;
then len v = k+1 by A9,FINSEQ_1:59;
then k+1 in Seg(len v) by A8;
then k+1 in dom v by FINSEQ_1:def 3;
then
A11: v.(k+1) = u.(k+1) by A9,FUNCT_1:47;
A12: k + 1 <= len c by A1,A3,A6,NAT_1:13;
then k + 1 in Seg(len c) by A8;
then
A13: k + 1 in dom c by FINSEQ_1:def 3;
reconsider r = v.(k+1) * cc.(k+1) as Element of REAL by XREAL_0:def 1;
reconsider s = <*r*> as FinSequence of REAL;
A14: len u = len c by A1,Def4;
len cc = k+1 by A10,A12,FINSEQ_1:59;
then k+1 in Seg(len cc) by A8;
then k+1 in dom cc by FINSEQ_1:def 3;
then
A15: cc.(k+1) = c.(k+1) by A10,FUNCT_1:47;
A16: k+1 <= len u by A6,NAT_1:13;
A17: (u(#)c)|k ^ <*v.(k+1) * cc.(k+1)*> = (u(#)c)|(k+1)
proof
set p = ((u(#)c)|k) ^ <*v.(k+1) * cc.(k+1)*>, q = (u(#)c)|(k+1);
A18: k + 1 <= len(u(#)c) by A1,A3,A16,Lm4;
then
A19: k <= len(u(#)c) by NAT_1:13;
A20: len p = len((u(#)c)|k) + 1 by FINSEQ_2:16
.= k + 1 by A19,FINSEQ_1:59;
A21: k + 1 = len q by A18,FINSEQ_1:59;
now
let j be Nat;
assume that
A22: 1 <= j and
A23: j <= len p;
per cases;
suppose
A24: j in dom((u(#)c)|k);
j in Seg(k+1) by A20,A22,A23;
then
A25: j in dom q by A21,FINSEQ_1:def 3;
thus p.j = ((u(#)c)|k).j by A24,FINSEQ_1:def 7
.= (u(#)c).j by A24,FUNCT_1:47
.= q.j by A25,FUNCT_1:47;
end;
suppose
A26: not j in dom((u(#)c)|k);
k <= len(u(#)c) by A6,A14,Lm4;
then
A27: len((u(#)c)|k) = k by FINSEQ_1:59;
then dom((u(#)c)|k) = Seg k by FINSEQ_1:def 3;
then j > k by A22,A26;
then
A28: j >= k + 1 by NAT_1:13;
then
A29: j = k+1 by A20,A23,XXREAL_0:1;
dom<*v.(k+1)*cc.(k+1)*> = {1} by FINSEQ_1:2,38;
then 1 in dom<*v.(k+1)*cc.(k+1)*> by TARSKI:def 1;
then
A30: p.(k+1) = <*v.(k+1)*cc.(k+1)*>.1 by A27,FINSEQ_1:def 7
.= v.(k+1)*cc.(k+1);
k+1 <= len(u(#)c) by A12,A14,Lm4;
then j in Seg(len(u(#)c)) by A8,A29;
then
A31: j in dom(u(#)c) by FINSEQ_1:def 3;
j in Seg(k+1) by A20,A22,A23;
then j in dom q by A21,FINSEQ_1:def 3;
then q.j = (u(#)c).j by FUNCT_1:47
.= v.(k+1) * cc.(k+1) by A15,A11,A29,A31,VALUED_1:def 4;
hence p.j = q.j by A20,A23,A28,A30,XXREAL_0:1;
end;
end;
hence thesis by A20,A21;
end;
v9 (#) cc9 = (u(#)c)|k by A6,A14,Th4;
then a = b^s by A9,A10,A16,A14,A17,Th4;
then
A32: Sum(v(#)cc) = Sum(b) + Sum s by RVSUM_1:75
.= Sum(v9(#)cc9) + v.(k+1) * cc.(k+1) by RVSUM_1:73;
A33: k < k + 1 by NAT_1:13;
now
per cases by XXREAL_0:1;
case
A34: k + 1 < i;
then k < i by NAT_1:13;
then
A35: Sum(v9(#)cc9), 0 are_congruent_mod m.i by A7;
A36: v.(k+1),v.(k+1) are_congruent_mod m.i by INT_1:11;
cc.(k+1), 0 are_congruent_mod m.i by A2,A4,A13,A15,A34,Th27;
then v.(k+1)*cc.(k+1),v.(k+1)*0 are_congruent_mod m.i by A36,INT_1:18
;
then
Sum(v(#)cc), (0+v.(k+1)*0) are_congruent_mod m.i by A32,A35,INT_1:16;
hence Sum(v(#)cc), 0 are_congruent_mod m.i;
end;
case
A37: k + 1 = i;
A38: v.(k+1),v.(k+1) are_congruent_mod m.i by INT_1:11;
cc.(k+1), 1 are_congruent_mod m.i by A13,A15,A37,Th26;
then
A39: v.(k+1)*cc.(k+1),u.(k+1)*1 are_congruent_mod m.i by A11,A38,INT_1:18;
Sum(v9(#)cc9), 0 are_congruent_mod m.i by A7,A33,A37;
hence Sum(v(#)cc), 0 + u.i are_congruent_mod m.i by A32,A37,A39,
INT_1:16;
end;
case
A40: k + 1 > i;
then k >= i by NAT_1:13;
then
A41: Sum(v9(#)cc9), u.i are_congruent_mod m.i by A7;
A42: v.(k+1),v.(k+1) are_congruent_mod m.i by INT_1:11;
cc.(k+1), 0 are_congruent_mod m.i by A2,A4,A13,A15,A40,Th27;
then v.(k+1)*cc.(k+1),u.(k+1)*0 are_congruent_mod m.i by A11,A42,
INT_1:18;
hence Sum(v(#)cc), u.i + 0 are_congruent_mod m.i by A32,A41,INT_1:16;
end;
end;
hence k+1 < i & Sum(v(#)cc), 0 are_congruent_mod m.i or k+1 >= i & Sum(v
(#)cc), u.i are_congruent_mod m.i;
end;
hence P[k+1];
end;
A43: dom m = Seg(len u) by A1,FINSEQ_1:def 3;
now
let v,cc be INT-valued FinSequence;
assume that
A44: v = u|0 and
cc = c|0;
dom v /\ dom cc = {} by A44;
then dom(v(#)cc) = {} by VALUED_1:def 4;
then v(#)cc = {};
hence
0 < i & Sum(v(#)cc), 0 are_congruent_mod m.i or 0 >= i & Sum(v(#)cc),
u.i are_congruent_mod m.i by A2,A43,FINSEQ_1:1,INT_1:11,RVSUM_1:72;
end;
then
A45: P[0];
A46: for k be Element of NAT st 0 <= k & k <= len u holds P[k] from
INT_1:sch 7(A45,A5);
len u = len c by A1,Def4;
then
A47: c|(len u) = c by FINSEQ_1:58;
A48: u = u|(len u) by FINSEQ_1:58;
i <= len u by A2,A43,FINSEQ_1:1;
hence thesis by A46,A48,A47;
end;
theorem Th30:
for u being INT-valued FinSequence, m being CR_Sequence st
len m = len u for c1,c2 being CR_coefficients of m holds Sum(u(#)c1),Sum(u(#)c2
) are_congruent_mod Product(m)
proof
let u be INT-valued FinSequence, m be CR_Sequence;
assume
A1: len u = len m;
let c1, c2 be CR_coefficients of m;
set s1 = Sum(u(#)c1) mod Product(m), s2 = Sum(u(#)c2) mod Product(m);
A2: s1 < Product(m) by NAT_D:62;
A3: for i being Nat st i in dom m holds s1, u.i are_congruent_mod
m.i
proof
let i be Nat;
s1 mod Product(m) = Sum(u(#)c1) mod Product(m) by NAT_D:65;
then
A4: s1, Sum(u(#)c1) are_congruent_mod Product(m) by NAT_D:64;
assume
A5: i in dom m;
then m.i in rng m by FUNCT_1:3;
then
A6: m.i > 0 by PARTFUN3:def 1;
ex z being Integer st z * m.i = Product(m) by A5,Th10;
then s1, Sum(u(#)c1) are_congruent_mod m.i by A4,INT_1:20;
then
A7: s1 mod m.i = Sum(u(#)c1) mod m.i by NAT_D:64;
Sum(u(#)c1), u.i are_congruent_mod m.i by A1,A5,Th29;
then Sum(u(#)c1) mod m.i = u.i mod m.i by NAT_D:64;
hence thesis by A6,A7,NAT_D:64;
end;
A8: 0 <= s2;
A9: for i being Nat st i in dom m holds s2, u.i
are_congruent_mod m.i
proof
let i be Nat;
s2 mod Product(m) = Sum(u(#)c2) mod Product(m) by NAT_D:65;
then
A10: s2, Sum(u(#)c2) are_congruent_mod Product(m) by NAT_D:64;
assume
A11: i in dom m;
then m.i in rng m by FUNCT_1:3;
then
A12: m.i > 0 by PARTFUN3:def 1;
ex z being Integer st z * m.i = Product(m) by A11,Th10;
then s2, Sum(u(#)c2) are_congruent_mod m.i by A10,INT_1:20;
then
A13: s2 mod m.i = Sum(u(#)c2) mod m.i by NAT_D:64;
Sum(u(#)c2), u.i are_congruent_mod m.i by A1,A11,Th29;
then Sum(u(#)c2) mod m.i = u.i mod m.i by NAT_D:64;
hence thesis by A12,A13,NAT_D:64;
end;
A14: s2 < Product(m) by NAT_D:62;
0 <= s1;
s1 = s2 by A3,A9,A2,A14,Lm9;
hence thesis by NAT_D:64;
end;
definition
let u be integer-valued FinSequence, m be CR_Sequence such that
A1: len m = len u;
func to_int(u,m) -> Integer means
:Def5:
for c being CR_coefficients of m holds it = Sum(u(#)c) mod Product(m);
existence
proof
set cz = the CR_coefficients of m;
take z = Sum(u(#)cz) mod Product(m);
for c be CR_coefficients of m holds z = Sum(u(#)c) mod Product(m)
by NAT_D:64,A1,Th30;
hence thesis;
end;
uniqueness
proof
set c = the CR_coefficients of m;
let z1, z2 be Integer;
assume
A2: for c being CR_coefficients of m holds z1 = Sum(u(#)c) mod Product (m);
assume
A3: for c being CR_coefficients of m holds z2 = Sum(u(#)c) mod Product (m);
thus z1 = Sum(u(#)c) mod Product(m) by A2
.= z2 by A3;
end;
end;
theorem Th31:
for u being INT-valued FinSequence, m being CR_Sequence st
len m = len u holds 0 <= to_int(u,m) & to_int(u,m) < Product(m)
proof
let u be INT-valued FinSequence, m be CR_Sequence;
set z = to_int(u,m);
set c = the CR_coefficients of m;
assume len u = len m;
then z = Sum(u(#)c) mod Product(m) by Def5;
hence thesis by NAT_D:62;
end;
theorem Th32:
for u being Integer, m being CR_Sequence, i being Nat
st i in dom m holds u, mod(u,m).i are_congruent_mod m.i
proof
let u be Integer, m be CR_Sequence;
let i be Nat;
A1: len mod(u,m) = len m by Def3;
assume
A2: i in dom m;
then m.i in rng m by FUNCT_1:3;
then m.i > 0 by PARTFUN3:def 1;
then u mod m.i = u - (u div m.i) * m.i by INT_1:def 10;
then
A3: u - (u mod m.i) = (u div m.i) * m.i;
dom mod(u,m) = Seg(len mod(u,m)) by FINSEQ_1:def 3
.= dom m by A1,FINSEQ_1:def 3;
then mod(u,m).i = u mod m.i by A2,Def3;
hence thesis by A3,INT_1:def 5;
end;
theorem Th33:
for u,v being Integer, m being CR_Sequence, i being Nat
st i in dom m holds (mod(u,m) + mod(v,m)).i, u + v are_congruent_mod m.i
proof
let u,v be Integer, m be CR_Sequence, i be Nat;
assume
A1: i in dom m;
A2: len mod(v,m) = len m by Def3;
then dom mod(v,m) = Seg(len m) by FINSEQ_1:def 3
.= dom m by FINSEQ_1:def 3;
then
A3: mod(v,m).i = v mod m.i by A1,Def3;
A4: len mod(u,m) = len m by Def3;
then len(mod(u,m)+mod(v,m)) = len m by A2,Lm2;
then dom(mod(u,m)+mod(v,m)) = Seg(len m) by FINSEQ_1:def 3
.= dom m by FINSEQ_1:def 3;
then
A5: (mod(u,m)+mod(v,m)).i = (mod(u,m).i) + (mod(v,m).i) by A1,VALUED_1:def 1;
dom mod(u,m) = Seg(len m) by A4,FINSEQ_1:def 3
.= dom m by FINSEQ_1:def 3;
then mod(u,m).i = u mod m.i by A1,Def3;
then
A6: (mod(u,m).i + mod(v,m).i) mod m.i = (u + v) mod m.i by A3,NAT_D:66;
m.i in rng m by A1,FUNCT_1:3;
then m.i > 0 by PARTFUN3:def 1;
hence thesis by A5,A6,NAT_D:64;
end;
Lm10: for u,v being Integer, m being CR_Sequence, i being Nat st i
in dom m holds (mod(u,m) - mod(v,m)).i, u - v are_congruent_mod m.i
proof
let u,v be Integer, m be CR_Sequence, i be Nat;
assume
A1: i in dom m;
A2: len mod(v,m) = len m by Def3;
then dom mod(v,m) = Seg(len m) by FINSEQ_1:def 3
.= dom m by FINSEQ_1:def 3;
then
A3: mod(v,m).i = v mod m.i by A1,Def3;
A4: len mod(u,m) = len m by Def3;
then len(mod(u,m)-mod(v,m)) = len m by A2,Lm3;
then dom(mod(u,m)-mod(v,m)) = Seg(len m) by FINSEQ_1:def 3
.= dom m by FINSEQ_1:def 3;
then
A5: (mod(u,m)-mod(v,m)).i = (mod(u,m).i) - (mod(v,m).i) by A1,VALUED_1:13;
dom mod(u,m) = Seg(len m) by A4,FINSEQ_1:def 3
.= dom m by FINSEQ_1:def 3;
then mod(u,m).i = u mod m.i by A1,Def3;
then
A6: (mod(u,m).i - mod(v,m).i) mod m.i = (u - v) mod m.i by A3,Th7;
m.i in rng m by A1,FUNCT_1:3;
then m.i > 0 by PARTFUN3:def 1;
hence thesis by A5,A6,NAT_D:64;
end;
theorem Th34:
for u,v being Integer, m being CR_Sequence, i being Nat
st i in dom m holds (mod(u,m) (#) mod(v,m)).i, u * v are_congruent_mod m.i
proof
let u,v be Integer, m be CR_Sequence, i be Nat;
assume
A1: i in dom m;
A2: len mod(v,m) = len m by Def3;
then dom mod(v,m) = Seg(len m) by FINSEQ_1:def 3
.= dom m by FINSEQ_1:def 3;
then
A3: mod(v,m).i = v mod m.i by A1,Def3;
A4: len mod(u,m) = len m by Def3;
then len(mod(u,m)(#)mod(v,m)) = len m by A2,Lm4;
then dom(mod(u,m)(#)mod(v,m)) = Seg(len m) by FINSEQ_1:def 3
.= dom m by FINSEQ_1:def 3;
then
A5: (mod(u,m)(#)mod(v,m)).i = ((mod(u,m).i) * (mod(v,m).i)) by A1,
VALUED_1:def 4;
dom mod(u,m) = Seg(len m) by A4,FINSEQ_1:def 3
.= dom m by FINSEQ_1:def 3;
then mod(u,m).i = u mod m.i by A1,Def3;
then
A6: (mod(u,m).i * mod(v,m).i) mod m.i = (u * v) mod m.i by A3,NAT_D:67;
m.i in rng m by A1,FUNCT_1:3;
then m.i > 0 by PARTFUN3:def 1;
hence thesis by A5,A6,NAT_D:64;
end;
theorem Th35:
for u,v being Integer, m being CR_Sequence, i being Nat
st i in dom m holds to_int(mod(u,m) + mod(v,m),m), u + v
are_congruent_mod m.i
proof
let u,v be Integer, m be CR_Sequence, i be Nat;
set z = to_int(mod(u,m) + mod(v,m),m);
set c = the CR_coefficients of m;
A1: len mod(u,m) = len m by Def3;
len mod(v,m) = len m by Def3;
then
A2: len(mod(u,m)+mod(v,m)) = len m by A1,Lm2;
then z = Sum((mod(u,m)+mod(v,m)) (#) c) mod Product(m) by Def5;
then z mod Product(m) = Sum((mod(u,m)+mod(v,m)) (#) c) mod Product(m) by
NAT_D:65;
then
A3: z, Sum((mod(u,m)+mod(v,m)) (#) c) are_congruent_mod Product(m) by NAT_D:64;
assume
A4: i in dom m;
then ex y being Integer st y * m.i = Product(m) by Th10;
then
A5: z, Sum((mod(u,m)+mod(v,m)) (#) c) are_congruent_mod m.i by A3,INT_1:20;
Sum((mod(u,m)+mod(v,m)) (#) c), (mod(u,m)+mod(v,m)).i are_congruent_mod
m.i by A4,A2,Th29;
then
A6: z,(mod(u,m)+mod(v,m)).i are_congruent_mod m.i by A5,INT_1:15;
(mod(u,m)+mod(v,m)).i, u + v are_congruent_mod m.i by A4,Th33;
hence thesis by A6,INT_1:15;
end;
theorem Th36:
for u,v being Integer, m being CR_Sequence, i being Nat
st i in dom m holds to_int(mod(u,m) - mod(v,m),m), u - v
are_congruent_mod m.i
proof
let u,v be Integer, m be CR_Sequence, i be Nat;
set z = to_int((mod(u,m) - mod(v,m)),m);
set c = the CR_coefficients of m;
A1: len mod(u,m) = len m by Def3;
len mod(v,m) = len m by Def3;
then
A2: len(mod(u,m) - mod(v,m)) = len m by A1,Lm3;
then z = Sum((mod(u,m) - mod(v,m)) (#) c) mod Product(m) by Def5;
then z mod Product(m) = Sum((mod(u,m)-mod(v,m)) (#) c) mod Product(m) by
NAT_D:65;
then
A3: z, Sum((mod(u,m)-mod(v,m)) (#) c) are_congruent_mod Product(m) by NAT_D:64;
assume
A4: i in dom m;
then ex y being Integer st y * m.i = Product(m) by Th10;
then
A5: z, Sum((mod(u,m)-mod(v,m)) (#) c) are_congruent_mod m.i by A3,INT_1:20;
Sum((mod(u,m)-mod(v,m)) (#) c), (mod(u,m)-mod(v,m)).i are_congruent_mod
m.i by A4,A2,Th29;
then
A6: z,(mod(u,m)-mod(v,m)).i are_congruent_mod m.i by A5,INT_1:15;
(mod(u,m)-mod(v,m)).i, u - v are_congruent_mod m.i by A4,Lm10;
hence thesis by A6,INT_1:15;
end;
theorem Th37:
for u,v being Integer, m being CR_Sequence, i being Nat
st i in dom m holds to_int(mod(u,m) (#) mod(v,m),m), u * v
are_congruent_mod m.i
proof
let u,v be Integer, m be CR_Sequence, i be Nat;
set z = to_int((mod(u,m) (#) mod(v,m)),m);
set c = the CR_coefficients of m;
A1: len mod(u,m) = len m by Def3;
len mod(v,m) = len m by Def3;
then
A2: len(mod(u,m) (#) mod(v,m)) = len m by A1,Lm4;
then z = Sum((mod(u,m) (#) mod(v,m)) (#) c) mod Product(m) by Def5;
then z mod Product(m) = Sum((mod(u,m)(#)mod(v,m)) (#) c) mod Product(m) by
NAT_D:65;
then
A3: z, Sum((mod(u,m)(#)mod(v,m)) (#) c) are_congruent_mod Product(m) by
NAT_D:64;
assume
A4: i in dom m;
then ex y being Integer st y * m.i = Product(m) by Th10;
then
A5: z, Sum((mod(u,m)(#)mod(v,m)) (#) c) are_congruent_mod m.i by A3,INT_1:20;
Sum((mod(u,m)(#)mod(v,m)) (#) c), (mod(u,m)(#)mod(v,m)).i
are_congruent_mod m.i by A4,A2,Th29;
then
A6: z,(mod(u,m)(#)mod(v,m)).i are_congruent_mod m.i by A5,INT_1:15;
(mod(u,m)(#)mod(v,m)).i, u * v are_congruent_mod m.i by A4,Th34;
hence thesis by A6,INT_1:15;
end;
theorem
for u,v being Integer, m being CR_Sequence st 0 <= u + v & u + v <
Product(m) holds to_int(mod(u,m) + mod(v,m), m) = u + v
proof
let u, v be Integer, m be CR_Sequence;
assume that
A1: 0 <= u + v and
A2: u + v < Product(m);
set z = to_int(mod(u,m) + mod(v,m), m);
A3: for i being Nat st i in dom m holds u + v, mod(u+v,m).i
are_congruent_mod m.i by Th32;
A4: len mod(u+v,m) = len m by Def3;
A5: for i being Nat st i in dom m holds z, mod(u+v,m).i
are_congruent_mod m.i
proof
let i be Nat;
assume
A6: i in dom m;
then z,u + v are_congruent_mod m.i by Th35;
then
A7: z mod m.i = (u+v) mod m.i by NAT_D:64;
dom(mod(u+v,m)) = Seg(len m) by A4,FINSEQ_1:def 3
.= dom m by FINSEQ_1:def 3;
then
A8: mod(u+v,m).i = (u + v) mod m.i by A6,Def3;
m.i in rng m by A6,FUNCT_1:3;
then
A9: m.i > 0 by PARTFUN3:def 1;
then m.i is Element of NAT by INT_1:3;
then (u+v) mod m.i = ((u+v) mod m.i) mod m.i by NAT_D:65;
hence thesis by A8,A7,A9,NAT_D:64;
end;
A10: len mod(u,m) = len m by Def3;
len mod(v,m) = len m by Def3;
then
A11: len(mod(u,m)+mod(v,m)) = len m by A10,Lm2;
then
A12: z < Product(m) by Th31;
0 <= z by A11,Th31;
hence thesis by A1,A2,A3,A12,A5,Lm9;
end;
theorem
for u,v being Integer, m being CR_Sequence st 0 <= u - v & u - v <
Product(m) holds to_int(mod(u,m) - mod(v,m), m) = u - v
proof
let u, v be Integer, m be CR_Sequence;
assume that
A1: 0 <= u - v and
A2: u - v < Product(m);
set z = to_int(mod(u,m) - mod(v,m), m);
A3: for i being Nat st i in dom m holds u - v, mod(u-v,m).i
are_congruent_mod m.i by Th32;
A4: len mod(u-v,m) = len m by Def3;
A5: for i being Nat st i in dom m holds z,mod(u-v,m).i
are_congruent_mod m.i
proof
let i be Nat;
assume
A6: i in dom m;
then z,u - v are_congruent_mod m.i by Th36;
then
A7: z mod m.i = (u-v) mod m.i by NAT_D:64;
dom(mod(u-v,m)) = Seg(len m) by A4,FINSEQ_1:def 3
.= dom m by FINSEQ_1:def 3;
then
A8: mod(u-v,m).i = (u - v) mod m.i by A6,Def3;
m.i in rng m by A6,FUNCT_1:3;
then
A9: m.i > 0 by PARTFUN3:def 1;
then m.i is Element of NAT by INT_1:3;
then (u-v) mod m.i = ((u-v) mod m.i) mod m.i by NAT_D:65;
hence thesis by A8,A7,A9,NAT_D:64;
end;
A10: len mod(u,m) = len m by Def3;
len mod(v,m) = len m by Def3;
then
A11: len(mod(u,m) - mod(v,m)) = len m by A10,Lm3;
then
A12: z < Product(m) by Th31;
0 <= z by A11,Th31;
hence thesis by A1,A2,A3,A12,A5,Lm9;
end;
theorem
for u,v being Integer, m being CR_Sequence st 0 <= u * v & u * v <
Product(m) holds to_int(mod(u,m) (#) mod(v,m), m) = u * v
proof
let u, v be Integer, m be CR_Sequence;
assume that
A1: 0 <= u * v and
A2: u * v < Product(m);
set z = to_int(mod(u,m) (#) mod(v,m), m);
A3: for i being Nat st i in dom m holds u * v,mod(u*v,m).i
are_congruent_mod m.i by Th32;
A4: len mod(u*v,m) = len m by Def3;
A5: for i being Nat st i in dom m holds z,mod(u*v,m).i
are_congruent_mod m.i
proof
let i be Nat;
assume
A6: i in dom m;
then z,u * v are_congruent_mod m.i by Th37;
then
A7: z mod m.i = (u*v) mod m.i by NAT_D:64;
dom(mod(u*v,m)) = Seg(len m) by A4,FINSEQ_1:def 3
.= dom m by FINSEQ_1:def 3;
then
A8: mod(u*v,m).i = (u * v) mod m.i by A6,Def3;
m.i in rng m by A6,FUNCT_1:3;
then
A9: m.i > 0 by PARTFUN3:def 1;
then m.i is Element of NAT by INT_1:3;
then (u*v) mod m.i = ((u*v) mod m.i) mod m.i by NAT_D:65;
hence thesis by A8,A7,A9,NAT_D:64;
end;
A10: len mod(u,m) = len m by Def3;
len mod(v,m) = len m by Def3;
then
A11: len(mod(u,m) (#) mod(v,m)) = len m by A10,Lm4;
then
A12: z < Product(m) by Th31;
0 <= z by A11,Th31;
hence thesis by A1,A2,A3,A12,A5,Lm9;
end;
begin :: Chinese Remainder Theorem Revisited
theorem
for u being INT-valued FinSequence, m being CR_Sequence st len u =
len m ex z being Integer st 0 <= z & z < Product(m) & for i being Nat
st i in dom u holds z,u.i are_congruent_mod m.i
proof
let u be INT-valued FinSequence, m be CR_Sequence;
assume
A1: len u = len m;
take z = to_int(u,m);
now
set c = the CR_coefficients of m;
let i be Nat;
assume
A2: i in dom u;
set s = Sum(u(#)c) mod Product(m);
s mod Product(m) = Sum(u(#)c) mod Product(m) by NAT_D:65;
then
A3: s, Sum(u(#)c) are_congruent_mod Product(m) by NAT_D:64;
A4: dom m = Seg(len u) by A1,FINSEQ_1:def 3
.= dom u by FINSEQ_1:def 3;
then ex y being Integer st y * m.i = Product(m) by A2,Th10;
then s, Sum(u(#)c) are_congruent_mod m.i by A3,INT_1:20;
then
A5: s mod m.i = Sum(u(#)c) mod m.i by NAT_D:64;
dom m = Seg(len u) by A1,FINSEQ_1:def 3
.= dom u by FINSEQ_1:def 3;
then m.i in rng m by A2,FUNCT_1:3;
then
A6: m.i > 0 by PARTFUN3:def 1;
Sum(u(#)c), u.i are_congruent_mod m.i by A1,A2,A4,Th29;
then Sum(u(#)c) mod m.i = u.i mod m.i by NAT_D:64;
then s,u.i are_congruent_mod m.i by A6,A5,NAT_D:64;
hence z,u.i are_congruent_mod m.i by A1,Def5;
end;
hence thesis by A1,Th31;
end;
theorem
for u being INT-valued FinSequence, m being CR_Sequence for z1,z2
being Integer st 0 <= z1 & z1 < Product(m) & (for i being Nat st i
in dom m holds z1,u.i are_congruent_mod m.i) & 0 <= z2 & z2 < Product(m) & (for
i being Nat st i in dom m holds z2,u.i are_congruent_mod m.i) holds
z1 = z2 by Lm9;