:: Extended Euclidean Algorithm and CRT Algorithm
:: by Hiroyuki Okazaki , Yosiki Aoki and Yasunari Shidama
::
:: Received February 8, 2012
:: Copyright (c) 2012-2021 Association of Mizar Users

theorem Th1: :: NTALGO_1:1

for x, p being Integer holds (x mod p) mod p = x mod p

proof end;

Lm1: for a, b being Integer ex A, B being sequence of NAT st
( A . 0 = |.a.| & B . 0 = |.b.| & ( for i being Nat holds
( A . (i + 1) = B . i & B . (i + 1) = (A . i) mod (B . i) ) ) )

proof end;

Lm2: for a, b being Integer
for A1, B1, A2, B2 being sequence of NAT st A1 . 0 = |.a.| & B1 . 0 = |.b.| & ( for i being Nat holds
( A1 . (i + 1) = B1 . i & B1 . (i + 1) = (A1 . i) mod (B1 . i) ) ) & A2 . 0 = |.a.| & B2 . 0 = |.b.| & ( for i being Nat holds
( A2 . (i + 1) = B2 . i & B2 . (i + 1) = (A2 . i) mod (B2 . i) ) ) holds
( A1 = A2 & B1 = B2 )

proof end;

definition

let a, b be Integer;

func ALGO_GCD (a,b) -> Element of NAT means :Def1: :: NTALGO_1:def 1
ex A, B being sequence of NAT st
( A . 0 = |.a.| & B . 0 = |.b.| & ( for i being Nat holds
( A . (i + 1) = B . i & B . (i + 1) = (A . i) mod (B . i) ) ) & it = A . (min* { i where i is Nat : B . i = 0 } ) );

existence
ex b₁ being Element of NAT ex A, B being sequence of NAT st
( A . 0 = |.a.| & B . 0 = |.b.| & ( for i being Nat holds
( A . (i + 1) = B . i & B . (i + 1) = (A . i) mod (B . i) ) ) & b₁ = A . (min* { i where i is Nat : B . i = 0 } ) )

proof end;

uniqueness
for b₁, b₂ being Element of NAT st ex A, B being sequence of NAT st
( A . 0 = |.a.| & B . 0 = |.b.| & ( for i being Nat holds
( A . (i + 1) = B . i & B . (i + 1) = (A . i) mod (B . i) ) ) & b₁ = A . (min* { i where i is Nat : B . i = 0 } ) ) & ex A, B being sequence of NAT st
( A . 0 = |.a.| & B . 0 = |.b.| & ( for i being Nat holds
( A . (i + 1) = B . i & B . (i + 1) = (A . i) mod (B . i) ) ) & b₂ = A . (min* { i where i is Nat : B . i = 0 } ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def1 defines ALGO_GCD NTALGO_1:def 1 :
for a, b being Integer
for b₃ being Element of NAT holds
( b₃ = ALGO_GCD (a,b) iff ex A, B being sequence of NAT st
( A . 0 = |.a.| & B . 0 = |.b.| & ( for i being Nat holds
( A . (i + 1) = B . i & B . (i + 1) = (A . i) mod (B . i) ) ) & b₃ = A . (min* { i where i is Nat : B . i = 0 } ) ) );

Lm3: for a, b being Integer
for A, B being sequence of NAT st A . 0 = |.a.| & B . 0 = |.b.| & ( for i being Nat holds
( A . (i + 1) = B . i & B . (i + 1) = (A . i) mod (B . i) ) ) holds
for i being Nat st B . i <> 0 holds
(A . i) gcd (B . i) = (A . (i + 1)) gcd (B . (i + 1))

proof end;

Lm4: for a, b being Integer
for A, B being sequence of NAT st A . 0 = |.a.| & B . 0 = |.b.| & ( for i being Nat holds
( A . (i + 1) = B . i & B . (i + 1) = (A . i) mod (B . i) ) ) holds
for i being Nat st B . i <> 0 holds
(A . 0) gcd (B . 0) = (A . i) gcd (B . i)

proof end;

Lm5: for a, b being Integer
for A, B being sequence of NAT st A . 0 = |.a.| & B . 0 = |.b.| & ( for i being Nat holds
( A . (i + 1) = B . i & B . (i + 1) = (A . i) mod (B . i) ) ) holds
{ i where i is Nat : B . i = 0 } is non empty Subset of NAT

proof end;

theorem :: NTALGO_1:2

for a, b being Integer holds ALGO_GCD (a,b) = a gcd b

proof end;

::==========================================================================================
::NZMATH source code
::
:: def extgcd(x,y):
:: """
:: Return a tuple (u,v,d); they are the greatest common divisor d
:: of two integers x and y and u,v such that d = x * u + y * v.
:: """
:: # Crandall & Pomerance "PRIME NUMBERS",Algorithm 2.1.4
:: a,b,g,u,v,w = 1,0,x,0,1,y
:: while w:
:: q,t = divmod(g,w)
:: a,b,g,u,v,w = u,v,w,a-q*u,b-q*v,t
:: if g >= 0:
:: return (a,b,g)
:: else:
:: return (-a,-b,-g)
::==========================================================================================

scheme :: NTALGO_1:sch 1
QuadChoiceRec{ F₁() -> non empty set , F₂() -> non empty set , F₃() -> non empty set , F₄() -> non empty set , F₅() -> Element of F₁(), F₆() -> Element of F₂(), F₇() -> Element of F₃(), F₈() -> Element of F₄(), P₁[ object , object , object , object , object , object , object , object , object ] } :

ex f being sequence of F₁() ex g being sequence of F₂() ex h being sequence of F₃() ex i being sequence of F₄() st
( f . 0 = F₅() & g . 0 = F₆() & h . 0 = F₇() & i . 0 = F₈() & ( for n being Nat holds P₁[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 Nat
for x being Element of F₁()
for y being Element of F₂()
for z being Element of F₃()
for w being Element of F₄() ex x1 being Element of F₁() ex y1 being Element of F₂() ex z1 being Element of F₃() ex w1 being Element of F₄() st P₁[n,x,y,z,w,x1,y1,z1,w1]

proof end;

Lm6: 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 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) ) ) )

proof end;

Lm7: for x, y being Integer
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 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 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 )

proof end;

definition

let x, y be Element of INT ;

func ALGO_EXGCD (x,y) -> Element of [:INT,INT,INT:] means :Def2: :: NTALGO_1:def 2
ex g, w, q, t, a, b, v, u being sequence of INT ex istop being 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 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 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 b₁ being Element of [:INT,INT,INT:] ex g, w, q, t, a, b, v, u being sequence of INT ex istop being 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 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 Nat : w . i = 0 } & ( 0 <= g . istop implies b₁ = [(a . istop),(b . istop),(g . istop)] ) & ( g . istop < 0 implies b₁ = [(- (a . istop)),(- (b . istop)),(- (g . istop))] ) )

proof end;

uniqueness
for b₁, b₂ being Element of [:INT,INT,INT:] st ex g, w, q, t, a, b, v, u being sequence of INT ex istop being 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 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 Nat : w . i = 0 } & ( 0 <= g . istop implies b₁ = [(a . istop),(b . istop),(g . istop)] ) & ( g . istop < 0 implies b₁ = [(- (a . istop)),(- (b . istop)),(- (g . istop))] ) ) & ex g, w, q, t, a, b, v, u being sequence of INT ex istop being 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 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 Nat : w . i = 0 } & ( 0 <= g . istop implies b₂ = [(a . istop),(b . istop),(g . istop)] ) & ( g . istop < 0 implies b₂ = [(- (a . istop)),(- (b . istop)),(- (g . istop))] ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def2 defines ALGO_EXGCD NTALGO_1:def 2 :
for x, y being Element of INT
for b₃ being Element of [:INT,INT,INT:] holds
( b₃ = ALGO_EXGCD (x,y) iff ex g, w, q, t, a, b, v, u being sequence of INT ex istop being 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 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 Nat : w . i = 0 } & ( 0 <= g . istop implies b₃ = [(a . istop),(b . istop),(g . istop)] ) & ( g . istop < 0 implies b₃ = [(- (a . istop)),(- (b . istop)),(- (g . istop))] ) ) );

Lm8: for a, b being Element of INT
for A, B being sequence of INT st A . 0 = a & B . 0 = b & ( for i being Nat holds
( A . (i + 1) = B . i & B . (i + 1) = (A . i) mod (B . i) ) ) holds
for i being Nat st B . i <> 0 holds
(A . i) gcd (B . i) = (A . (i + 1)) gcd (B . (i + 1))

proof end;

Lm9: for a, b being Element of INT
for A, B being sequence of INT st A . 0 = a & B . 0 = b & ( for i being Nat holds
( A . (i + 1) = B . i & B . (i + 1) = (A . i) mod (B . i) ) ) holds
for i being Nat st B . i <> 0 holds
(A . 0) gcd (B . 0) = (A . i) gcd (B . i)

proof end;

theorem Th3: :: NTALGO_1:3

for i2, i1 being Integer st i2 <= 0 holds
i1 mod i2 <= 0

proof end;

theorem Th4: :: NTALGO_1:4

for i2, i1 being Integer st i2 < 0 holds
- (i1 mod i2) < - i2

proof end;

theorem Th5: :: NTALGO_1:5

for x, y being Integer st |.y.| <> 0 holds
|.(x mod y).| < |.y.|

proof end;

Lm10: for a, b being Element of INT
for A, B being sequence of INT st A . 0 = a & B . 0 = b & ( for i being Nat holds
( A . (i + 1) = B . i & B . (i + 1) = (A . i) mod (B . i) ) ) holds
{ i where i is Nat : B . i = 0 } is non empty Subset of NAT

proof end;

Lm11: for a being Element of INT holds a gcd 0 = |.a.|
by WSIERP_1:8;

Lm12: 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 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 Nat st w . i <> 0 holds
((a . (i + 1)) * x) + ((b . (i + 1)) * y) = g . (i + 1)

proof end;

theorem Th6: :: 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 )

proof end;

::==========================================================================================
::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 :Def3: :: 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 b₁ 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 & b<sub>1</sub> = p + z ) ) & ( 0 <= (ALGO_EXGCD (p,y)) `2_3 implies b₁ = (ALGO_EXGCD (p,y)) `2_3 ) ) ) & ( (ALGO_EXGCD (p,y)) `3_3 <> 1 implies b₁ = {} ) )

proof end;

uniqueness
for b₁, b₂ 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 & b<sub>1</sub> = p + z ) ) & ( 0 <= (ALGO_EXGCD (p,y)) `2_3 implies b₁ = (ALGO_EXGCD (p,y)) `2_3 ) ) ) & ( (ALGO_EXGCD (p,y)) `3_3 <> 1 implies b₁ = {} ) ) ) & ( 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 & b<sub>2</sub> = p + z ) ) & ( 0 <= (ALGO_EXGCD (p,y)) `2_3 implies b₂ = (ALGO_EXGCD (p,y)) `2_3 ) ) ) & ( (ALGO_EXGCD (p,y)) `3_3 <> 1 implies b₂ = {} ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def3 defines ALGO_INVERSE NTALGO_1:def 3 :
for x, p, b₃ being Element of INT holds
( b₃ = 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 & b<sub>3</sub> = p + z ) ) & ( 0 <= (ALGO_EXGCD (p,y)) `2_3 implies b₃ = (ALGO_EXGCD (p,y)) `2_3 ) ) ) & ( (ALGO_EXGCD (p,y)) `3_3 <> 1 implies b₃ = {} ) ) );

Lm13: 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

proof end;

theorem Th7: :: 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

proof end;

:: 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 :Def4: :: 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 b₁ being Element of INT st
( ( len nlist = 1 implies b₁ = (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)) ) ) & b₁ = (n . (len m)) mod M ) ) )

proof end;

uniqueness
for b₁, b₂ being Element of INT st ( len nlist = 1 implies b₁ = (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)) ) ) & b<sub>1</sub> = (n . (len m)) mod M ) ) & ( len nlist = 1 implies b<sub>2</sub> = (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)) ) ) & b₂ = (n . (len m)) mod M ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def4 defines ALGO_CRT NTALGO_1:def 4 :
for nlist being non empty FinSequence of [:INT,INT:]
for b₂ being Element of INT holds
( b₂ = ALGO_CRT nlist iff ( ( len nlist = 1 implies b₂ = (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)) ) ) & b₂ = (n . (len m)) mod M ) ) ) );

theorem Th8: :: NTALGO_1:8

for a, b being Integer st b <> 0 holds
a mod b,a are_congruent_mod b

proof end;

theorem :: NTALGO_1:9

for a, b being Integer st b <> 0 holds
(a mod b) gcd b = a gcd b by Th8, WSIERP_1:43;

theorem Th10: :: NTALGO_1:10

for a, b, c being Integer st c <> 0 & a = b mod c & b,c are_coprime holds
a,c are_coprime

proof end;

Lm14: for a, b, c being Integer st a = b mod c & c <> 0 holds
ex d being Element of INT st a = b + (d * c)

proof end;

Lm15: 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

proof end;

Lm16: 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_coprime ) & m . 1 = 1 holds
for k being 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_coprime

proof end;

Lm17: 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

proof end;

theorem Th11: :: 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_coprime ) holds
for i being Nat st i in Seg (len nlist) holds
(ALGO_CRT nlist) mod (b . i) = (a . i) mod (b . i)

proof end;

Lm18: for x, y, a, b being Integer st x mod a = y mod a & x mod b = y mod b & a,b are_coprime holds
x mod (a * b) = y mod (a * b)

proof end;

theorem Th12: :: NTALGO_1:12

for x, y being Integer
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_coprime ) & ( 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))

proof end;

theorem Th13: :: NTALGO_1:13

for b being complex-valued FinSequence st len b = 1 holds
Product b = b . 1

proof end;

theorem Th14: :: 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) )

proof end;

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_coprime ) & ( 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

proof end;