:: by Hiroyuki Okazaki , Yosiki Aoki and Yasunari Shidama

::

:: Received February 8, 2012

:: Copyright (c) 2012-2016 Association of Mizar Users

Lm1: for a, b being Element of INT 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 Element of INT

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 Element of INT ;

ex b_{1} 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_{1} = A . (min* { i where i is Nat : B . i = 0 } ) )

for b_{1}, b_{2} 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_{1} = 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_{2} = A . (min* { i where i is Nat : B . i = 0 } ) ) holds

b_{1} = b_{2}

end;
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 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 } ) );

ex b

( 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

proof end;

uniqueness for b

( 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 . 0 = |.a.| & B . 0 = |.b.| & ( for i being Nat holds

( A . (i + 1) = B . i & B . (i + 1) = (A . i) mod (B . i) ) ) & b

b

proof end;

:: deftheorem Def1 defines ALGO_GCD NTALGO_1:def 1 :

for a, b being Element of INT

for b_{3} being Element of NAT holds

( b_{3} = 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_{3} = A . (min* { i where i is Nat : B . i = 0 } ) ) );

for a, b being Element of INT

for b

( b

( 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

Lm3: for a, b being Element of INT

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 Element of INT

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 Element of INT

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;

scheme :: NTALGO_1:sch 1

QuadChoiceRec{ F_{1}() -> non empty set , F_{2}() -> non empty set , F_{3}() -> non empty set , F_{4}() -> non empty set , F_{5}() -> Element of F_{1}(), F_{6}() -> Element of F_{2}(), F_{7}() -> Element of F_{3}(), F_{8}() -> Element of F_{4}(), P_{1}[ object , object , object , object , object , object , object , object , object ] } :

QuadChoiceRec{ F

ex f being sequence of F_{1}() ex g being sequence of F_{2}() ex h being sequence of F_{3}() ex i being sequence of F_{4}() st

( f . 0 = F_{5}() & g . 0 = F_{6}() & h . 0 = F_{7}() & i . 0 = F_{8}() & ( for n being Nat holds P_{1}[n,f . n,g . n,h . n,i . n,f . (n + 1),g . (n + 1),h . (n + 1),i . (n + 1)] ) )

provided( f . 0 = F

A1:
for n being Nat

for x being Element of F_{1}()

for y being Element of F_{2}()

for z being Element of F_{3}()

for w being Element of F_{4}() ex x1 being Element of F_{1}() ex y1 being Element of F_{2}() ex z1 being Element of F_{3}() ex w1 being Element of F_{4}() st P_{1}[n,x,y,z,w,x1,y1,z1,w1]

for x being Element of F

for y being Element of F

for z being Element of F

for w being Element of F

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 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 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 ;

ex b_{1} 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_{1} = [(a . istop),(b . istop),(g . istop)] ) & ( g . istop < 0 implies b_{1} = [(- (a . istop)),(- (b . istop)),(- (g . istop))] ) )

for b_{1}, b_{2} 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_{1} = [(a . istop),(b . istop),(g . istop)] ) & ( g . istop < 0 implies b_{1} = [(- (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_{2} = [(a . istop),(b . istop),(g . istop)] ) & ( g . istop < 0 implies b_{2} = [(- (a . istop)),(- (b . istop)),(- (g . istop))] ) ) holds

b_{1} = b_{2}

end;
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 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))] ) );

ex b

( 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

proof end;

uniqueness for b

( 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 . 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

b

proof end;

:: deftheorem Def2 defines ALGO_EXGCD NTALGO_1:def 2 :

for x, y being Element of INT

for b_{3} being Element of [:INT,INT,INT:] holds

( b_{3} = 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_{3} = [(a . istop),(b . istop),(g . istop)] ) & ( g . istop < 0 implies b_{3} = [(- (a . istop)),(- (b . istop)),(- (g . istop))] ) ) );

for x, y being Element of INT

for b

( b

( 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

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;

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 )

( (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;

definition

let x, p be Element of INT ;

ex b_{1} 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_{1} = p + z ) ) & ( 0 <= (ALGO_EXGCD (p,y)) `2_3 implies b_{1} = (ALGO_EXGCD (p,y)) `2_3 ) ) ) & ( (ALGO_EXGCD (p,y)) `3_3 <> 1 implies b_{1} = {} ) )

for b_{1}, b_{2} 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_{1} = p + z ) ) & ( 0 <= (ALGO_EXGCD (p,y)) `2_3 implies b_{1} = (ALGO_EXGCD (p,y)) `2_3 ) ) ) & ( (ALGO_EXGCD (p,y)) `3_3 <> 1 implies b_{1} = {} ) ) ) & ( 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_{2} = p + z ) ) & ( 0 <= (ALGO_EXGCD (p,y)) `2_3 implies b_{2} = (ALGO_EXGCD (p,y)) `2_3 ) ) ) & ( (ALGO_EXGCD (p,y)) `3_3 <> 1 implies b_{2} = {} ) ) ) holds

b_{1} = b_{2}

end;
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 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 = {} ) );

ex 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

proof end;

uniqueness for b

( ( (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

( ( (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

b

proof end;

:: deftheorem Def3 defines ALGO_INVERSE NTALGO_1:def 3 :

for x, p, b_{3} being Element of INT holds

( b_{3} = 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_{3} = p + z ) ) & ( 0 <= (ALGO_EXGCD (p,y)) `2_3 implies b_{3} = (ALGO_EXGCD (p,y)) `2_3 ) ) ) & ( (ALGO_EXGCD (p,y)) `3_3 <> 1 implies b_{3} = {} ) ) );

for x, p, b

( b

( ( (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

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

((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

::==========================================================================================

:: """

:: 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:];

ex b_{1} being Element of INT st

( ( len nlist = 1 implies b_{1} = (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_{1} = (n . (len m)) mod M ) ) )

for b_{1}, b_{2} being Element of INT st ( len nlist = 1 implies b_{1} = (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_{1} = (n . (len m)) mod M ) ) & ( len nlist = 1 implies b_{2} = (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_{2} = (n . (len m)) mod M ) ) holds

b_{1} = b_{2}

end;
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 ( ( 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 ) ) );

ex b

( ( len nlist = 1 implies b

( 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

proof end;

uniqueness for b

( 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

( 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

b

proof end;

:: deftheorem Def4 defines ALGO_CRT NTALGO_1:def 4 :

for nlist being non empty FinSequence of [:INT,INT:]

for b_{2} being Element of INT holds

( b_{2} = ALGO_CRT nlist iff ( ( len nlist = 1 implies b_{2} = (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_{2} = (n . (len m)) mod M ) ) ) );

for nlist being non empty FinSequence of [:INT,INT:]

for b

( b

( 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

theorem :: NTALGO_1:9

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

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)

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 Element of INT 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 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_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))

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

( 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

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;

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

::=======================================================================================