:: Extended Euclidean Algorithm and CRT Algorithm :: by Hiroyuki Okazaki , Yosiki Aoki and Yasunari Shidama :: :: Received February 8, 2012 :: Copyright (c) 2012 Association of Mizar Users begin theorem LMTh3: :: NTALGO_1:1 for x, p being Integer holds (x mod p) mod p = x mod p proofend; LM6: for a being Element of NAT holds a gcd 0 = a proofend; LM1: for a, b being Element of INT ex A, B being sequence of NAT st ( A . 0 = abs a & B . 0 = abs b & ( for i being Element of NAT holds ( A . (i + 1) = B . i & B . (i + 1) = (A . i) mod (B . i) ) ) ) proofend; LM2: for a, b being Element of INT for A1, B1, A2, B2 being sequence of NAT st A1 . 0 = abs a & B1 . 0 = abs b & ( for i being Element of NAT holds ( A1 . (i + 1) = B1 . i & B1 . (i + 1) = (A1 . i) mod (B1 . i) ) ) & A2 . 0 = abs a & B2 . 0 = abs b & ( for i being Element of NAT holds ( A2 . (i + 1) = B2 . i & B2 . (i + 1) = (A2 . i) mod (B2 . i) ) ) holds ( A1 = A2 & B1 = B2 ) proofend; definition let a, b be Element of INT ; func ALGO_GCD (a,b) -> Element of NAT means :defALGOGCD: :: NTALGO_1:def 1 ex A, B being sequence of NAT st ( A . 0 = abs a & B . 0 = abs b & ( for i being Element of NAT holds ( A . (i + 1) = B . i & B . (i + 1) = (A . i) mod (B . i) ) ) & it = A . (min* { i where i is Element of NAT : B . i = 0 } ) ); existence ex b1 being Element of NAT ex A, B being sequence of NAT st ( A . 0 = abs a & B . 0 = abs b & ( for i being Element of NAT holds ( A . (i + 1) = B . i & B . (i + 1) = (A . i) mod (B . i) ) ) & b1 = A . (min* { i where i is Element of NAT : B . i = 0 } ) ) proofend; uniqueness for b1, b2 being Element of NAT st ex A, B being sequence of NAT st ( A . 0 = abs a & B . 0 = abs b & ( for i being Element of NAT holds ( A . (i + 1) = B . i & B . (i + 1) = (A . i) mod (B . i) ) ) & b1 = A . (min* { i where i is Element of NAT : B . i = 0 } ) ) & ex A, B being sequence of NAT st ( A . 0 = abs a & B . 0 = abs b & ( for i being Element of NAT holds ( A . (i + 1) = B . i & B . (i + 1) = (A . i) mod (B . i) ) ) & b2 = A . (min* { i where i is Element of NAT : B . i = 0 } ) ) holds b1 = b2 proofend; end; :: deftheorem defALGOGCD defines ALGO_GCD NTALGO_1:def_1_:_ for a, b being Element of INT for b3 being Element of NAT holds ( b3 = ALGO_GCD (a,b) iff ex A, B being sequence of NAT st ( A . 0 = abs a & B . 0 = abs b & ( for i being Element of NAT holds ( A . (i + 1) = B . i & B . (i + 1) = (A . i) mod (B . i) ) ) & b3 = A . (min* { i where i is Element of NAT : B . i = 0 } ) ) ); LM3: for a, b being Element of INT for A, B being sequence of NAT st A . 0 = abs a & B . 0 = abs b & ( for i being Element of NAT holds ( A . (i + 1) = B . i & B . (i + 1) = (A . i) mod (B . i) ) ) holds for i being Element of NAT st B . i <> 0 holds (A . i) gcd (B . i) = (A . (i + 1)) gcd (B . (i + 1)) proofend; LM4: for a, b being Element of INT for A, B being sequence of NAT st A . 0 = abs a & B . 0 = abs b & ( for i being Element of NAT holds ( A . (i + 1) = B . i & B . (i + 1) = (A . i) mod (B . i) ) ) holds for i being Element of NAT st B . i <> 0 holds (A . 0) gcd (B . 0) = (A . i) gcd (B . i) proofend; LM5: for a, b being Element of INT for A, B being sequence of NAT st A . 0 = abs a & B . 0 = abs b & ( for i being Element of NAT holds ( A . (i + 1) = B . i & B . (i + 1) = (A . i) mod (B . i) ) ) holds { i where i is Element of NAT : B . i = 0 } is non empty Subset of NAT proofend; theorem :: NTALGO_1:2 for a, b being Element of INT holds ALGO_GCD (a,b) = a gcd b proofend; begin scheme :: NTALGO_1:sch 1 QuadChoiceRec{ F1() -> non empty set , F2() -> non empty set , F3() -> non empty set , F4() -> non empty set , F5() -> Element of F1(), F6() -> Element of F2(), F7() -> Element of F3(), F8() -> Element of F4(), P1[ set , set , set , set , set , set , set , set , set ] } : ex f being Function of NAT,F1() ex g being Function of NAT,F2() ex h being Function of NAT,F3() ex i being Function of NAT,F4() st ( f . 0 = F5() & g . 0 = F6() & h . 0 = F7() & i . 0 = F8() & ( for n being Element of NAT holds P1[n,f . n,g . n,h . n,i . n,f . (n + 1),g . (n + 1),h . (n + 1),i . (n + 1)] ) ) provided A1: for n being Element of NAT for x being Element of F1() for y being Element of F2() for z being Element of F3() for w being Element of F4() ex x1 being Element of F1() ex y1 being Element of F2() ex z1 being Element of F3() ex w1 being Element of F4() st P1[n,x,y,z,w,x1,y1,z1,w1] proofend; EXLM1: for x, y being Element of INT ex g, w, q, t, a, b, v, u being sequence of INT st ( a . 0 = 1 & b . 0 = 0 & g . 0 = x & q . 0 = 0 & u . 0 = 0 & v . 0 = 1 & w . 0 = y & t . 0 = 0 & ( for i being Element of NAT holds ( q . (i + 1) = (g . i) div (w . i) & t . (i + 1) = (g . i) mod (w . i) & a . (i + 1) = u . i & b . (i + 1) = v . i & g . (i + 1) = w . i & u . (i + 1) = (a . i) - ((q . (i + 1)) * (u . i)) & v . (i + 1) = (b . i) - ((q . (i + 1)) * (v . i)) & w . (i + 1) = t . (i + 1) ) ) ) proofend; EXLM2: for x, y being Element of INT for g1, w1, q1, t1, a1, b1, v1, u1, g2, w2, q2, t2, a2, b2, v2, u2 being sequence of INT st a1 . 0 = 1 & b1 . 0 = 0 & g1 . 0 = x & q1 . 0 = 0 & u1 . 0 = 0 & v1 . 0 = 1 & w1 . 0 = y & t1 . 0 = 0 & ( for i being Element of NAT holds ( q1 . (i + 1) = (g1 . i) div (w1 . i) & t1 . (i + 1) = (g1 . i) mod (w1 . i) & a1 . (i + 1) = u1 . i & b1 . (i + 1) = v1 . i & g1 . (i + 1) = w1 . i & u1 . (i + 1) = (a1 . i) - ((q1 . (i + 1)) * (u1 . i)) & v1 . (i + 1) = (b1 . i) - ((q1 . (i + 1)) * (v1 . i)) & w1 . (i + 1) = t1 . (i + 1) ) ) & a2 . 0 = 1 & b2 . 0 = 0 & g2 . 0 = x & q2 . 0 = 0 & u2 . 0 = 0 & v2 . 0 = 1 & w2 . 0 = y & t2 . 0 = 0 & ( for i being Element of NAT holds ( q2 . (i + 1) = (g2 . i) div (w2 . i) & t2 . (i + 1) = (g2 . i) mod (w2 . i) & a2 . (i + 1) = u2 . i & b2 . (i + 1) = v2 . i & g2 . (i + 1) = w2 . i & u2 . (i + 1) = (a2 . i) - ((q2 . (i + 1)) * (u2 . i)) & v2 . (i + 1) = (b2 . i) - ((q2 . (i + 1)) * (v2 . i)) & w2 . (i + 1) = t2 . (i + 1) ) ) holds ( g1 = g2 & w1 = w2 & q1 = q2 & t1 = t2 & a1 = a2 & b1 = b2 & v1 = v2 & u1 = u2 ) proofend; definition let x, y be Element of INT ; func ALGO_EXGCD (x,y) -> Element of [:INT,INT,INT:] means :defALGOEXGCD: :: NTALGO_1:def 2 ex g, w, q, t, a, b, v, u being sequence of INT ex istop being Element of NAT st ( a . 0 = 1 & b . 0 = 0 & g . 0 = x & q . 0 = 0 & u . 0 = 0 & v . 0 = 1 & w . 0 = y & t . 0 = 0 & ( for i being Element of NAT holds ( q . (i + 1) = (g . i) div (w . i) & t . (i + 1) = (g . i) mod (w . i) & a . (i + 1) = u . i & b . (i + 1) = v . i & g . (i + 1) = w . i & u . (i + 1) = (a . i) - ((q . (i + 1)) * (u . i)) & v . (i + 1) = (b . i) - ((q . (i + 1)) * (v . i)) & w . (i + 1) = t . (i + 1) ) ) & istop = min* { i where i is Element of NAT : w . i = 0 } & ( 0 <= g . istop implies it = [(a . istop),(b . istop),(g . istop)] ) & ( g . istop < 0 implies it = [(- (a . istop)),(- (b . istop)),(- (g . istop))] ) ); existence ex b1 being Element of [:INT,INT,INT:] ex g, w, q, t, a, b, v, u being sequence of INT ex istop being Element of NAT st ( a . 0 = 1 & b . 0 = 0 & g . 0 = x & q . 0 = 0 & u . 0 = 0 & v . 0 = 1 & w . 0 = y & t . 0 = 0 & ( for i being Element of NAT holds ( q . (i + 1) = (g . i) div (w . i) & t . (i + 1) = (g . i) mod (w . i) & a . (i + 1) = u . i & b . (i + 1) = v . i & g . (i + 1) = w . i & u . (i + 1) = (a . i) - ((q . (i + 1)) * (u . i)) & v . (i + 1) = (b . i) - ((q . (i + 1)) * (v . i)) & w . (i + 1) = t . (i + 1) ) ) & istop = min* { i where i is Element of NAT : w . i = 0 } & ( 0 <= g . istop implies b1 = [(a . istop),(b . istop),(g . istop)] ) & ( g . istop < 0 implies b1 = [(- (a . istop)),(- (b . istop)),(- (g . istop))] ) ) proofend; uniqueness for b1, b2 being Element of [:INT,INT,INT:] st ex g, w, q, t, a, b, v, u being sequence of INT ex istop being Element of NAT st ( a . 0 = 1 & b . 0 = 0 & g . 0 = x & q . 0 = 0 & u . 0 = 0 & v . 0 = 1 & w . 0 = y & t . 0 = 0 & ( for i being Element of NAT holds ( q . (i + 1) = (g . i) div (w . i) & t . (i + 1) = (g . i) mod (w . i) & a . (i + 1) = u . i & b . (i + 1) = v . i & g . (i + 1) = w . i & u . (i + 1) = (a . i) - ((q . (i + 1)) * (u . i)) & v . (i + 1) = (b . i) - ((q . (i + 1)) * (v . i)) & w . (i + 1) = t . (i + 1) ) ) & istop = min* { i where i is Element of NAT : w . i = 0 } & ( 0 <= g . istop implies b1 = [(a . istop),(b . istop),(g . istop)] ) & ( g . istop < 0 implies b1 = [(- (a . istop)),(- (b . istop)),(- (g . istop))] ) ) & ex g, w, q, t, a, b, v, u being sequence of INT ex istop being Element of NAT st ( a . 0 = 1 & b . 0 = 0 & g . 0 = x & q . 0 = 0 & u . 0 = 0 & v . 0 = 1 & w . 0 = y & t . 0 = 0 & ( for i being Element of NAT holds ( q . (i + 1) = (g . i) div (w . i) & t . (i + 1) = (g . i) mod (w . i) & a . (i + 1) = u . i & b . (i + 1) = v . i & g . (i + 1) = w . i & u . (i + 1) = (a . i) - ((q . (i + 1)) * (u . i)) & v . (i + 1) = (b . i) - ((q . (i + 1)) * (v . i)) & w . (i + 1) = t . (i + 1) ) ) & istop = min* { i where i is Element of NAT : w . i = 0 } & ( 0 <= g . istop implies b2 = [(a . istop),(b . istop),(g . istop)] ) & ( g . istop < 0 implies b2 = [(- (a . istop)),(- (b . istop)),(- (g . istop))] ) ) holds b1 = b2 proofend; end; :: deftheorem defALGOEXGCD defines ALGO_EXGCD NTALGO_1:def_2_:_ for x, y being Element of INT for b3 being Element of [:INT,INT,INT:] holds ( b3 = ALGO_EXGCD (x,y) iff ex g, w, q, t, a, b, v, u being sequence of INT ex istop being Element of NAT st ( a . 0 = 1 & b . 0 = 0 & g . 0 = x & q . 0 = 0 & u . 0 = 0 & v . 0 = 1 & w . 0 = y & t . 0 = 0 & ( for i being Element of NAT holds ( q . (i + 1) = (g . i) div (w . i) & t . (i + 1) = (g . i) mod (w . i) & a . (i + 1) = u . i & b . (i + 1) = v . i & g . (i + 1) = w . i & u . (i + 1) = (a . i) - ((q . (i + 1)) * (u . i)) & v . (i + 1) = (b . i) - ((q . (i + 1)) * (v . i)) & w . (i + 1) = t . (i + 1) ) ) & istop = min* { i where i is Element of NAT : w . i = 0 } & ( 0 <= g . istop implies b3 = [(a . istop),(b . istop),(g . istop)] ) & ( g . istop < 0 implies b3 = [(- (a . istop)),(- (b . istop)),(- (g . istop))] ) ) ); LM3G: for a, b being Element of INT for A, B being sequence of INT st A . 0 = a & B . 0 = b & ( for i being Element of NAT holds ( A . (i + 1) = B . i & B . (i + 1) = (A . i) mod (B . i) ) ) holds for i being Element of NAT st B . i <> 0 holds (A . i) gcd (B . i) = (A . (i + 1)) gcd (B . (i + 1)) proofend; LM4G: for a, b being Element of INT for A, B being sequence of INT st A . 0 = a & B . 0 = b & ( for i being Element of NAT holds ( A . (i + 1) = B . i & B . (i + 1) = (A . i) mod (B . i) ) ) holds for i being Element of NAT st B . i <> 0 holds (A . 0) gcd (B . 0) = (A . i) gcd (B . i) proofend; theorem INT157A: :: NTALGO_1:3 for i2, i1 being Integer st i2 <= 0 holds i1 mod i2 <= 0 proofend; theorem INT158A: :: NTALGO_1:4 for i2, i1 being Integer st i2 < 0 holds - (i1 mod i2) < - i2 proofend; theorem LM5G1: :: NTALGO_1:5 for x, y being Element of INT st abs y <> 0 holds abs (x mod y) < abs y proofend; LM5G: for a, b being Element of INT for A, B being sequence of INT st A . 0 = a & B . 0 = b & ( for i being Element of NAT holds ( A . (i + 1) = B . i & B . (i + 1) = (A . i) mod (B . i) ) ) holds { i where i is Element of NAT : B . i = 0 } is non empty Subset of NAT proofend; LM6G: for a being Element of INT holds a gcd 0 = abs a by WSIERP_1:8; LM7G: for x, y being Element of INT for g, w, q, t, a, b, v, u being sequence of INT st a . 0 = 1 & b . 0 = 0 & g . 0 = x & q . 0 = 0 & u . 0 = 0 & v . 0 = 1 & w . 0 = y & t . 0 = 0 & ( for i being Element of NAT holds ( q . (i + 1) = (g . i) div (w . i) & t . (i + 1) = (g . i) mod (w . i) & a . (i + 1) = u . i & b . (i + 1) = v . i & g . (i + 1) = w . i & u . (i + 1) = (a . i) - ((q . (i + 1)) * (u . i)) & v . (i + 1) = (b . i) - ((q . (i + 1)) * (v . i)) & w . (i + 1) = t . (i + 1) ) ) holds for i being Element of NAT st w . i <> 0 holds ((a . (i + 1)) * x) + ((b . (i + 1)) * y) = g . (i + 1) proofend; theorem Th2: :: NTALGO_1:6 for x, y being Element of INT holds ( (ALGO_EXGCD (x,y)) `3_3 = x gcd y & (((ALGO_EXGCD (x,y)) `1_3) * x) + (((ALGO_EXGCD (x,y)) `2_3) * y) = x gcd y ) proofend; ::========================================================================================== ::NZMATH source code :: def inverse(x,p): :: """ :: This function returns inverse of x for modulo p. :: """ :: x = x % p :: y = gcd.extgcd(p,x) :: if y[2] == 1: :: if y[1] < 0: :: r = p + y[1] :: return r :: else: :: return y[1] :: raise ZeroDivisionError("There is no inverse for %d modulo %d." % (x,p)) ::======================================================================================= definition let x, p be Element of INT ; func ALGO_INVERSE (x,p) -> Element of INT means :definverse: :: NTALGO_1:def 3 for y being Element of INT st y = x mod p holds ( ( (ALGO_EXGCD (p,y)) `3_3 = 1 implies ( ( (ALGO_EXGCD (p,y)) `2_3 < 0 implies ex z being Element of INT st ( z = (ALGO_EXGCD (p,y)) `2_3 & it = p + z ) ) & ( 0 <= (ALGO_EXGCD (p,y)) `2_3 implies it = (ALGO_EXGCD (p,y)) `2_3 ) ) ) & ( (ALGO_EXGCD (p,y)) `3_3 <> 1 implies it = {} ) ); existence ex b1 being Element of INT st for y being Element of INT st y = x mod p holds ( ( (ALGO_EXGCD (p,y)) `3_3 = 1 implies ( ( (ALGO_EXGCD (p,y)) `2_3 < 0 implies ex z being Element of INT st ( z = (ALGO_EXGCD (p,y)) `2_3 & b1 = p + z ) ) & ( 0 <= (ALGO_EXGCD (p,y)) `2_3 implies b1 = (ALGO_EXGCD (p,y)) `2_3 ) ) ) & ( (ALGO_EXGCD (p,y)) `3_3 <> 1 implies b1 = {} ) ) proofend; uniqueness for b1, b2 being Element of INT st ( for y being Element of INT st y = x mod p holds ( ( (ALGO_EXGCD (p,y)) `3_3 = 1 implies ( ( (ALGO_EXGCD (p,y)) `2_3 < 0 implies ex z being Element of INT st ( z = (ALGO_EXGCD (p,y)) `2_3 & b1 = p + z ) ) & ( 0 <= (ALGO_EXGCD (p,y)) `2_3 implies b1 = (ALGO_EXGCD (p,y)) `2_3 ) ) ) & ( (ALGO_EXGCD (p,y)) `3_3 <> 1 implies b1 = {} ) ) ) & ( for y being Element of INT st y = x mod p holds ( ( (ALGO_EXGCD (p,y)) `3_3 = 1 implies ( ( (ALGO_EXGCD (p,y)) `2_3 < 0 implies ex z being Element of INT st ( z = (ALGO_EXGCD (p,y)) `2_3 & b2 = p + z ) ) & ( 0 <= (ALGO_EXGCD (p,y)) `2_3 implies b2 = (ALGO_EXGCD (p,y)) `2_3 ) ) ) & ( (ALGO_EXGCD (p,y)) `3_3 <> 1 implies b2 = {} ) ) ) holds b1 = b2 proofend; end; :: deftheorem definverse defines ALGO_INVERSE NTALGO_1:def_3_:_ for x, p, b3 being Element of INT holds ( b3 = ALGO_INVERSE (x,p) iff for y being Element of INT st y = x mod p holds ( ( (ALGO_EXGCD (p,y)) `3_3 = 1 implies ( ( (ALGO_EXGCD (p,y)) `2_3 < 0 implies ex z being Element of INT st ( z = (ALGO_EXGCD (p,y)) `2_3 & b3 = p + z ) ) & ( 0 <= (ALGO_EXGCD (p,y)) `2_3 implies b3 = (ALGO_EXGCD (p,y)) `2_3 ) ) ) & ( (ALGO_EXGCD (p,y)) `3_3 <> 1 implies b3 = {} ) ) ); LMTh30: for x, y, p being Element of INT st y = x mod p & (ALGO_EXGCD (p,y)) `3_3 = 1 & p <> 0 holds ((ALGO_INVERSE (x,p)) * x) mod p = 1 mod p proofend; theorem Th3: :: NTALGO_1:7 for x, p, y being Element of INT st y = x mod p & (ALGO_EXGCD (p,y)) `3_3 = 1 holds ((ALGO_INVERSE (x,p)) * x) mod p = 1 mod p proofend; begin :: def ALGO_CRT(nlist): :: """ :: This function is Chinese Remainder Theorem using Algorithm 2.1.7 :: of C.Pomerance and R.Crandall's book. :: :: For example: :: >>> ALGO_CRT([(1,2),(2,3),(3,5)]) :: 23 :: """ :: r = len(nlist) :: if r == 1 : :: return nlist [ 0 ] [ 0 ] :: :: product = [] :: prodinv = [] :: m = 1 :: for i in range(1,r): :: m = m*nlist[i-1][1] :: c = inverse(m,nlist[i][1]) :: product.append(m) :: prodinv.append(c) :: :: M = product[r-2]*nlist[r-1][1] :: n = nlist[0][0] :: for i in range(1,r): :: u = ((nlist[i][0]-n)*prodinv[i-1]) % nlist[i][1] :: n += u*product[i-1] :: return n % M ::========================================================================================== definition let nlist be non empty FinSequence of [:INT,INT:]; func ALGO_CRT nlist -> Element of INT means :defALGOCRT: :: NTALGO_1:def 4 ( ( len nlist = 1 implies it = (nlist . 1) `1 ) & ( len nlist <> 1 implies ex m, n, prodc, prodi being FinSequence of INT ex M0, M being Element of INT st ( len m = len nlist & len n = len nlist & len prodc = (len nlist) - 1 & len prodi = (len nlist) - 1 & m . 1 = 1 & ( for i being Nat st 1 <= i & i <= (len m) - 1 holds ex d, x, y being Element of INT st ( x = (nlist . i) `2 & m . (i + 1) = (m . i) * x & y = m . (i + 1) & d = (nlist . (i + 1)) `2 & prodi . i = ALGO_INVERSE (y,d) & prodc . i = y ) ) & M0 = (nlist . (len m)) `2 & M = (prodc . ((len m) - 1)) * M0 & n . 1 = (nlist . 1) `1 & ( for i being Nat st 1 <= i & i <= (len m) - 1 holds ex u, u0, u1 being Element of INT st ( u0 = (nlist . (i + 1)) `1 & u1 = (nlist . (i + 1)) `2 & u = ((u0 - (n . i)) * (prodi . i)) mod u1 & n . (i + 1) = (n . i) + (u * (prodc . i)) ) ) & it = (n . (len m)) mod M ) ) ); existence ex b1 being Element of INT st ( ( len nlist = 1 implies b1 = (nlist . 1) `1 ) & ( len nlist <> 1 implies ex m, n, prodc, prodi being FinSequence of INT ex M0, M being Element of INT st ( len m = len nlist & len n = len nlist & len prodc = (len nlist) - 1 & len prodi = (len nlist) - 1 & m . 1 = 1 & ( for i being Nat st 1 <= i & i <= (len m) - 1 holds ex d, x, y being Element of INT st ( x = (nlist . i) `2 & m . (i + 1) = (m . i) * x & y = m . (i + 1) & d = (nlist . (i + 1)) `2 & prodi . i = ALGO_INVERSE (y,d) & prodc . i = y ) ) & M0 = (nlist . (len m)) `2 & M = (prodc . ((len m) - 1)) * M0 & n . 1 = (nlist . 1) `1 & ( for i being Nat st 1 <= i & i <= (len m) - 1 holds ex u, u0, u1 being Element of INT st ( u0 = (nlist . (i + 1)) `1 & u1 = (nlist . (i + 1)) `2 & u = ((u0 - (n . i)) * (prodi . i)) mod u1 & n . (i + 1) = (n . i) + (u * (prodc . i)) ) ) & b1 = (n . (len m)) mod M ) ) ) proofend; uniqueness for b1, b2 being Element of INT st ( len nlist = 1 implies b1 = (nlist . 1) `1 ) & ( len nlist <> 1 implies ex m, n, prodc, prodi being FinSequence of INT ex M0, M being Element of INT st ( len m = len nlist & len n = len nlist & len prodc = (len nlist) - 1 & len prodi = (len nlist) - 1 & m . 1 = 1 & ( for i being Nat st 1 <= i & i <= (len m) - 1 holds ex d, x, y being Element of INT st ( x = (nlist . i) `2 & m . (i + 1) = (m . i) * x & y = m . (i + 1) & d = (nlist . (i + 1)) `2 & prodi . i = ALGO_INVERSE (y,d) & prodc . i = y ) ) & M0 = (nlist . (len m)) `2 & M = (prodc . ((len m) - 1)) * M0 & n . 1 = (nlist . 1) `1 & ( for i being Nat st 1 <= i & i <= (len m) - 1 holds ex u, u0, u1 being Element of INT st ( u0 = (nlist . (i + 1)) `1 & u1 = (nlist . (i + 1)) `2 & u = ((u0 - (n . i)) * (prodi . i)) mod u1 & n . (i + 1) = (n . i) + (u * (prodc . i)) ) ) & b1 = (n . (len m)) mod M ) ) & ( len nlist = 1 implies b2 = (nlist . 1) `1 ) & ( len nlist <> 1 implies ex m, n, prodc, prodi being FinSequence of INT ex M0, M being Element of INT st ( len m = len nlist & len n = len nlist & len prodc = (len nlist) - 1 & len prodi = (len nlist) - 1 & m . 1 = 1 & ( for i being Nat st 1 <= i & i <= (len m) - 1 holds ex d, x, y being Element of INT st ( x = (nlist . i) `2 & m . (i + 1) = (m . i) * x & y = m . (i + 1) & d = (nlist . (i + 1)) `2 & prodi . i = ALGO_INVERSE (y,d) & prodc . i = y ) ) & M0 = (nlist . (len m)) `2 & M = (prodc . ((len m) - 1)) * M0 & n . 1 = (nlist . 1) `1 & ( for i being Nat st 1 <= i & i <= (len m) - 1 holds ex u, u0, u1 being Element of INT st ( u0 = (nlist . (i + 1)) `1 & u1 = (nlist . (i + 1)) `2 & u = ((u0 - (n . i)) * (prodi . i)) mod u1 & n . (i + 1) = (n . i) + (u * (prodc . i)) ) ) & b2 = (n . (len m)) mod M ) ) holds b1 = b2 proofend; end; :: deftheorem defALGOCRT defines ALGO_CRT NTALGO_1:def_4_:_ for nlist being non empty FinSequence of [:INT,INT:] for b2 being Element of INT holds ( b2 = ALGO_CRT nlist iff ( ( len nlist = 1 implies b2 = (nlist . 1) `1 ) & ( len nlist <> 1 implies ex m, n, prodc, prodi being FinSequence of INT ex M0, M being Element of INT st ( len m = len nlist & len n = len nlist & len prodc = (len nlist) - 1 & len prodi = (len nlist) - 1 & m . 1 = 1 & ( for i being Nat st 1 <= i & i <= (len m) - 1 holds ex d, x, y being Element of INT st ( x = (nlist . i) `2 & m . (i + 1) = (m . i) * x & y = m . (i + 1) & d = (nlist . (i + 1)) `2 & prodi . i = ALGO_INVERSE (y,d) & prodc . i = y ) ) & M0 = (nlist . (len m)) `2 & M = (prodc . ((len m) - 1)) * M0 & n . 1 = (nlist . 1) `1 & ( for i being Nat st 1 <= i & i <= (len m) - 1 holds ex u, u0, u1 being Element of INT st ( u0 = (nlist . (i + 1)) `1 & u1 = (nlist . (i + 1)) `2 & u = ((u0 - (n . i)) * (prodi . i)) mod u1 & n . (i + 1) = (n . i) + (u * (prodc . i)) ) ) & b2 = (n . (len m)) mod M ) ) ) ); theorem LMLmTh4B: :: NTALGO_1:8 for a, b being Element of INT st b <> 0 holds a mod b,a are_congruent_mod b proofend; theorem :: NTALGO_1:9 for a, b being Element of INT st b <> 0 holds (a mod b) gcd b = a gcd b by INT_4:14, LMLmTh4B; theorem LmTh4A: :: NTALGO_1:10 for a, b, c being Element of INT st c <> 0 & a = b mod c & b,c are_relative_prime holds a,c are_relative_prime proofend; LmTh4: for a, b, c being Element of INT st a = b mod c & c <> 0 holds ex d being Element of INT st a = b + (d * c) proofend; LmTh5A: for b, m being FinSequence of INT st len b = len m & ( for i being Nat st i in Seg (len b) holds b . i <> 0 ) & m . 1 = 1 holds for k being Element of NAT st 1 <= k & k <= (len b) - 1 & ( for i being Nat st 1 <= i & i <= k holds m . (i + 1) = (m . i) * (b . i) ) holds m . (k + 1) <> 0 proofend; LmTh5: for b, m being FinSequence of INT st 2 <= len b & ( for i, j being Nat st i in Seg (len b) & j in Seg (len b) & i <> j holds b . i,b . j are_relative_prime ) & m . 1 = 1 holds for k being Element of NAT st 1 <= k & k <= (len b) - 1 & ( for i being Nat st 1 <= i & i <= k holds m . (i + 1) = (m . i) * (b . i) ) holds for j being Nat st k + 1 <= j & j <= len b holds m . (k + 1),b . j are_relative_prime proofend; LmTh6: for b, m being FinSequence of INT st len b = len m & m . 1 = 1 holds for k being Element of NAT st 1 <= k & k <= (len b) - 1 & ( for i being Nat st 1 <= i & i <= k holds m . (i + 1) = (m . i) * (b . i) ) holds for j being Nat st 1 <= j & j <= k holds (m . (k + 1)) mod (b . j) = 0 proofend; theorem Th4: :: NTALGO_1:11 for nlist being non empty FinSequence of [:INT,INT:] for a, b being FinSequence of INT st len a = len b & len a = len nlist & ( for i being Nat st i in Seg (len nlist) holds b . i <> 0 ) & ( for i being Nat st i in Seg (len nlist) holds ( (nlist . i) `1 = a . i & (nlist . i) `2 = b . i ) ) & ( for i, j being Nat st i in Seg (len nlist) & j in Seg (len nlist) & i <> j holds b . i,b . j are_relative_prime ) holds for i being Nat st i in Seg (len nlist) holds (ALGO_CRT nlist) mod (b . i) = (a . i) mod (b . i) proofend; LmTh7A: for x, y, a, b being Element of INT st x mod a = y mod a & x mod b = y mod b & a,b are_relative_prime holds x mod (a * b) = y mod (a * b) proofend; theorem LmTh7: :: NTALGO_1:12 for x, y being Element of INT for b, m being non empty FinSequence of INT st 2 <= len b & ( for i, j being Nat st i in Seg (len b) & j in Seg (len b) & i <> j holds b . i,b . j are_relative_prime ) & ( for i being Nat st i in Seg (len b) holds x mod (b . i) = y mod (b . i) ) & m . 1 = 1 holds for k being Element of NAT st 1 <= k & k <= len b & ( for i being Nat st 1 <= i & i <= k holds m . (i + 1) = (m . i) * (b . i) ) holds x mod (m . (k + 1)) = y mod (m . (k + 1)) proofend; theorem LmTh8: :: NTALGO_1:13 for b being FinSequence of INT st len b = 1 holds Product b = b . 1 proofend; theorem LmTh9: :: NTALGO_1:14 for b being FinSequence of INT ex m being non empty FinSequence of INT st ( len m = (len b) + 1 & m . 1 = 1 & ( for i being Nat st 1 <= i & i <= len b holds m . (i + 1) = (m . i) * (b . i) ) & Product b = m . ((len b) + 1) ) proofend; theorem :: NTALGO_1:15 for nlist being non empty FinSequence of [:INT,INT:] for a, b being non empty FinSequence of INT for x, y being Element of INT st len a = len b & len a = len nlist & ( for i being Nat st i in Seg (len nlist) holds b . i <> 0 ) & ( for i being Nat st i in Seg (len nlist) holds ( (nlist . i) `1 = a . i & (nlist . i) `2 = b . i ) ) & ( for i, j being Nat st i in Seg (len nlist) & j in Seg (len nlist) & i <> j holds b . i,b . j are_relative_prime ) & ( for i being Nat st i in Seg (len nlist) holds x mod (b . i) = (a . i) mod (b . i) ) & y = Product b holds (ALGO_CRT nlist) mod y = x mod y proofend;