:: Modular Integer Arithmetic :: by Christoph Schwarzweller :: :: Received May 13, 2008 :: Copyright (c) 2008-2018 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; 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, FUNCT_1; 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 Lm1: for f being INT-valued FinSequence holds f is FinSequence of INT proof let f be INT-valued FinSequence; rng f c= INT by RELAT_1:def 19; hence thesis by FINSEQ_1:def 4; end; 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 proof per cases; suppose n > len f; hence thesis by RFINSEQ:def 1; end; suppose A1: n <= len f; now reconsider f9 = f as FinSequence of INT by Lm1; let u be object; reconsider n9 = n as Element of NAT by ORDINAL1:def 12; A2: rng f c= INT by RELAT_1:def 19; assume u in rng(f/^n); then consider x being object such that A3: x in dom(f/^n) and A4: (f/^n).x = u by FUNCT_1:def 3; reconsider x as Element of NAT by A3; x+n9 in dom f9 by A3,FINSEQ_5:26; then A5: f.(x+n) in rng f by FUNCT_1:def 3; (f/^n).x = f.(x+n) by A1,A3,RFINSEQ:def 1; hence u in INT by A4,A5,A2; end; then rng(f/^n) c= INT by TARSKI:def 3; hence thesis by RELAT_1:def 19; end; end; end; registration let i be Integer; cluster <*i*> -> INT-valued; coherence proof for u be object st u in {i} holds u in INT by INT_1:def 2; then A1: {i} c= INT by TARSKI:def 3; rng(<*i*>) = {i} by FINSEQ_1:39; hence thesis by A1,RELAT_1:def 19; end; end; registration let f,g be INT-valued FinSequence; cluster f ^ g -> INT-valued; coherence proof now let u be object; A1: rng(f^g) = rng f \/ rng g by FINSEQ_1:31; assume A2: u in rng(f^g); now per cases by A2,A1,XBOOLE_0:def 3; case A3: u in rng f; rng f c= INT by RELAT_1:def 19; hence u in INT by A3; end; case A4: u in rng g; rng g c= INT by RELAT_1:def 19; hence u in INT by A4; end; end; hence u in INT; end; then rng(f^g) c= INT by TARSKI:def 3; hence thesis by RELAT_1:def 19; end; 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 INT-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; Lm5: for z being INT-valued FinSequence holds z is FinSequence of REAL proof let f be INT-valued FinSequence; rng f c= REAL; hence thesis by FINSEQ_1:def 4; 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) by FINSEQ_1:40 .= 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 by INT_1:def 10 .= ((a mod n) - (b mod n)) mod n by A1,INT_1:def 10; 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; then a-b,(a mod n)-(b mod n) are_congruent_mod n by INT_2:15; hence thesis by NAT_D:64; 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 INT-valued FinSequence, i being Nat st i in dom m & m.i <> 0 holds Product(m) / m.i is Integer proof let m be INT-valued FinSequence, i9 be Nat; reconsider i = i9 as Element of NAT by ORDINAL1:def 12; reconsider m2 = m/^i as FinSequence of INT by Lm1; reconsider m1 = m|i as FinSequence of INT by Lm1; reconsider m9 = m as FinSequence of INT by Lm1; assume that A1: i9 in dom m and A2: m.i9 <> 0; A3: dom m = Seg(len m) by FINSEQ_1:def 3; then 1 <= i by A1,FINSEQ_1:1; then 1 - 1 <= i - 1 by XREAL_1:9; then reconsider j = i - 1 as Element of NAT by INT_1:3; set f = (m|j) ^ (m/^i); reconsider f as FinSequence of INT by Lm1; 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 by RVSUM_1:95 .= 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; 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; then reconsider z = Product(m) / m.i as Integer by A1,Th9; take z; 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 in dom m & j <> i & m.j <> 0 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 Lm1; assume that A1: i9 in dom m and A2: j9 in dom m and A3: j9 <> i9 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 1 - 1 <= j - 1 by XREAL_1:9; 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 Lm1; 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 1 - 1 <= i - 1 by XREAL_1:9; 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 i-1 > kj by XREAL_1:9; then reconsider a = i-1 - kj as Element of NAT by INT_1:5; 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 by RVSUM_1:95 .= 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 by Lm1; reconsider m1 = m|j as FinSequence of INT by Lm1; 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 by RVSUM_1:95 .= 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; theorem for m being INT-valued FinSequence, i,j being Nat st i in dom m & j in dom m & j <> i & m.j <> 0 holds Product(m) / (m.i * m.j) is Integer proof let m be INT-valued FinSequence, i9,j9 be Nat; assume that A1: i9 in dom m and A2: j9 in dom m and A3: j9 <> i9 and A4: m.j9 <> 0; 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,A2,A3,A4,Lm6; per cases; suppose A0: m.i = 0; thus thesis by A0; end; suppose A6: m.i <> 0; reconsider u = Product(m) / m.j as Integer by A2,A4,Th9; 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; theorem for m being INT-valued FinSequence, i,j being Nat st i in dom m & j in dom m & j <> i & m.j <> 0 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 INT-valued FinSequence; antonym f is multiplicative-trivial for f is non-empty; end; definition let f be INT-valued FinSequence; redefine attr f is multiplicative-trivial means :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 by FINSEQ_1:40; 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 INT-valued FinSequence; 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 Lm1; 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,A3,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,RVSUM_1:95; 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 by A13,Th9; 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,RVSUM_1:95; 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 Lm1; 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 by A18,Th9; 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,RVSUM_1:95 .= 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 INT-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; then reconsider mm = Product(m) / m.k as Integer by Th9; 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 A1,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 Lm5; 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) by FINSEQ_1:40; 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 by NAT_D:62; 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 by NAT_D:62; then s1 = s2 by A3,A9,A2,A8,A14,Lm9; hence thesis by NAT_D:64; end; definition let u be INT-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; set z = Sum(u(#)cz) mod Product(m); take z; 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;