ntalgo_1.miz
begin
theorem ::
NTALGO_1:1
Th1: for x,p be
Integer holds ((x
mod p)
mod p)
= (x
mod p)
proof
let x,p be
Integer;
(x
mod p)
= ((x
+
0 )
mod p)
.= (((x
mod p)
+ (
0
mod p))
mod p) by
NAT_D: 66
.= (((x
mod p)
+
0 )
mod p) by
INT_1: 73;
hence thesis;
end;
Lm1: for a,b be
Integer holds ex A,B be
sequence of
NAT st (A
.
0 )
=
|.a.| & (B
.
0 )
=
|.b.| & (for i be
Nat holds (A
. (i
+ 1))
= (B
. i) & (B
. (i
+ 1))
= ((A
. i)
mod (B
. i)))
proof
let a,b be
Integer;
defpred
P1[
Nat,
Nat,
Nat,
Nat,
Nat] means $4
= $3 & $5
= ($2
mod $3);
A1: for n be
Nat, x be
Element of
NAT , y be
Element of
NAT holds ex x1 be
Element of
NAT , y1 be
Element of
NAT st
P1[n, x, y, x1, y1];
consider A be
sequence of
NAT , B be
sequence of
NAT such that
A2: (A
.
0 )
=
|.a.| & (B
.
0 )
=
|.b.| & for n be
Nat holds
P1[n, (A
. n), (B
. n), (A
. (n
+ 1)), (B
. (n
+ 1))] from
RECDEF_2:sch 3(
A1);
take A, B;
thus thesis by
A2;
end;
Lm2: for a,b be
Integer, A1,B1,A2,B2 be
sequence of
NAT st ((A1
.
0 )
=
|.a.| & (B1
.
0 )
=
|.b.| & (for i be
Nat holds (A1
. (i
+ 1))
= (B1
. i) & (B1
. (i
+ 1))
= ((A1
. i)
mod (B1
. i)))) & ((A2
.
0 )
=
|.a.| & (B2
.
0 )
=
|.b.| & (for i be
Nat holds (A2
. (i
+ 1))
= (B2
. i) & (B2
. (i
+ 1))
= ((A2
. i)
mod (B2
. i)))) holds A1
= A2 & B1
= B2
proof
let a,b be
Integer;
let A1,B1,A2,B2 be
sequence of
NAT ;
assume
A1: (A1
.
0 )
=
|.a.| & (B1
.
0 )
=
|.b.| & for i be
Nat holds (A1
. (i
+ 1))
= (B1
. i) & (B1
. (i
+ 1))
= ((A1
. i)
mod (B1
. i));
assume
A2: (A2
.
0 )
=
|.a.| & (B2
.
0 )
=
|.b.| & for i be
Nat holds (A2
. (i
+ 1))
= (B2
. i) & (B2
. (i
+ 1))
= ((A2
. i)
mod (B2
. i));
defpred
P[
Nat] means (A1
. $1)
= (A2
. $1) & (B1
. $1)
= (B2
. $1);
A3:
P[
0 ] by
A1,
A2;
A4: for n be
Nat st
P[n] holds
P[(n
+ 1)]
proof
let n be
Nat;
assume
A5:
P[n];
A6: (A1
. (n
+ 1))
= (B1
. n) by
A1
.= (A2
. (n
+ 1)) by
A2,
A5;
(B1
. (n
+ 1))
= ((A1
. n)
mod (B1
. n)) by
A1
.= (B2
. (n
+ 1)) by
A2,
A5;
hence
P[(n
+ 1)] by
A6;
end;
for n be
Nat holds
P[n] from
NAT_1:sch 2(
A3,
A4);
hence thesis;
end;
definition
let a,b be
Integer;
::
NTALGO_1:def1
func
ALGO_GCD (a,b) ->
Element of
NAT means
:
Def1: ex A,B be
sequence of
NAT st (A
.
0 )
=
|.a.| & (B
.
0 )
=
|.b.| & (for i be
Nat holds (A
. (i
+ 1))
= (B
. i) & (B
. (i
+ 1))
= ((A
. i)
mod (B
. i))) & it
= (A
. (
min* { i where i be
Nat : (B
. i)
=
0 }));
existence
proof
consider A,B be
sequence of
NAT such that
A1: (A
.
0 )
=
|.a.| & (B
.
0 )
=
|.b.| & (for i be
Nat holds (A
. (i
+ 1))
= (B
. i) & (B
. (i
+ 1))
= ((A
. i)
mod (B
. i))) by
Lm1;
set m = (A
. (
min* { i where i be
Nat : (B
. i)
=
0 }));
m is
Element of
NAT ;
hence thesis by
A1;
end;
uniqueness
proof
let m1,m2 be
Element of
NAT ;
given A1,B1 be
sequence of
NAT such that
A2: (A1
.
0 )
=
|.a.| & (B1
.
0 )
=
|.b.| & (for i be
Nat holds (A1
. (i
+ 1))
= (B1
. i) & (B1
. (i
+ 1))
= ((A1
. i)
mod (B1
. i))) & m1
= (A1
. (
min* { i where i be
Nat : (B1
. i)
=
0 }));
assume ex A2,B2 be
sequence of
NAT st (A2
.
0 )
=
|.a.| & (B2
.
0 )
=
|.b.| & (for i be
Nat holds (A2
. (i
+ 1))
= (B2
. i) & (B2
. (i
+ 1))
= ((A2
. i)
mod (B2
. i))) & m2
= (A2
. (
min* { i where i be
Nat : (B2
. i)
=
0 }));
then
consider A2,B2 be
sequence of
NAT such that
A3: (A2
.
0 )
=
|.a.| & (B2
.
0 )
=
|.b.| & (for i be
Nat holds (A2
. (i
+ 1))
= (B2
. i) & (B2
. (i
+ 1))
= ((A2
. i)
mod (B2
. i))) & m2
= (A2
. (
min* { i where i be
Nat : (B2
. i)
=
0 }));
A1
= A2 & B1
= B2 by
Lm2,
A2,
A3;
hence thesis by
A2,
A3;
end;
end
Lm3: for a,b be
Integer, A,B be
sequence of
NAT st ((A
.
0 )
=
|.a.| & (B
.
0 )
=
|.b.| & (for i be
Nat holds (A
. (i
+ 1))
= (B
. i) & (B
. (i
+ 1))
= ((A
. i)
mod (B
. i)))) holds for i be
Nat st (B
. i)
<>
0 holds ((A
. i)
gcd (B
. i))
= ((A
. (i
+ 1))
gcd (B
. (i
+ 1)))
proof
let a,b be
Integer, A,B be
sequence of
NAT ;
assume
A1: (A
.
0 )
=
|.a.| & (B
.
0 )
=
|.b.| & (for i be
Nat holds (A
. (i
+ 1))
= (B
. i) & (B
. (i
+ 1))
= ((A
. i)
mod (B
. i)));
let i be
Nat;
assume
A2: (B
. i)
<>
0 ;
set k = ((A
. i)
gcd (B
. i));
A4: (B
. (i
+ 1))
= ((A
. i)
mod (B
. i)) by
A1;
(A
. (i
+ 1))
= (B
. i) by
A1;
then
A5: k
divides (A
. (i
+ 1)) by
INT_2:def 2;
A6: k
divides (B
. (i
+ 1))
proof
A7: (B
. (i
+ 1))
= ((A
. i)
- (((A
. i)
div (B
. i))
* (B
. i))) by
A4,
A2,
INT_1:def 10;
A8: k
divides (A
. i) by
INT_2:def 2;
A9: k
divides (B
. i) by
INT_2:def 2;
ex s be
Integer st (A
. i)
= (k
* s) by
A8;
then
consider s,t be
Integer such that
A11: (B
. (i
+ 1))
= ((k
* s)
- (((A
. i)
div (B
. i))
* (k
* t))) by
A7,
A9;
(B
. (i
+ 1))
= ((s
- (((A
. i)
div (B
. i))
* t))
* k) by
A11;
hence k
divides (B
. (i
+ 1));
end;
for m be
Integer st m
divides (A
. (i
+ 1)) & m
divides (B
. (i
+ 1)) holds m
divides k
proof
let m be
Integer;
assume
A12: m
divides (A
. (i
+ 1)) & m
divides (B
. (i
+ 1));
then
A13: m
divides (B
. i) by
A1;
A14: m
divides (A
. i)
proof
(B
. (i
+ 1))
= ((A
. i)
- (((A
. i)
div (B
. i))
* (B
. i))) by
A4,
A2,
INT_1:def 10;
then
A15: (A
. i)
= ((B
. (i
+ 1))
+ (((A
. i)
div (B
. i))
* (B
. i)));
A16: ex s be
Integer st (B
. i)
= (m
* s) by
A13;
A17: ex t be
Integer st (B
. (i
+ 1))
= (m
* t) by
A12;
consider s,t be
Integer such that
A18: (A
. i)
= ((m
* s)
+ (((A
. i)
div (B
. i))
* (m
* t))) by
A15,
A16,
A17;
(A
. i)
= (m
* (s
+ (((A
. i)
div (B
. i))
* t))) by
A18;
hence m
divides (A
. i);
end;
thus m
divides k by
A13,
A14,
INT_2:def 2;
end;
hence ((A
. (i
+ 1))
gcd (B
. (i
+ 1)))
= k by
A5,
A6,
INT_2:def 2;
end;
Lm4: for a,b be
Integer, A,B be
sequence of
NAT st ((A
.
0 )
=
|.a.| & (B
.
0 )
=
|.b.| & (for i be
Nat holds (A
. (i
+ 1))
= (B
. i) & (B
. (i
+ 1))
= ((A
. i)
mod (B
. i)))) holds for i be
Nat st (B
. i)
<>
0 holds ((A
.
0 )
gcd (B
.
0 ))
= ((A
. i)
gcd (B
. i))
proof
let a,b be
Integer, A,B be
sequence of
NAT ;
assume
A1: (A
.
0 )
=
|.a.| & (B
.
0 )
=
|.b.| & (for i be
Nat holds (A
. (i
+ 1))
= (B
. i) & (B
. (i
+ 1))
= ((A
. i)
mod (B
. i)));
defpred
P[
Nat] means (B
. $1)
<>
0 implies ((A
.
0 )
gcd (B
.
0 ))
= ((A
. $1)
gcd (B
. $1));
A2:
P[
0 ];
A3: for i be
Nat st
P[i] holds
P[(i
+ 1)]
proof
let i be
Nat;
assume
A4:
P[i];
(B
. (i
+ 1))
<>
0 implies ((A
.
0 )
gcd (B
.
0 ))
= ((A
. (i
+ 1))
gcd (B
. (i
+ 1)))
proof
assume
A5: (B
. (i
+ 1))
<>
0 ;
(B
. i)
<>
0
proof
assume
A6: (B
. i)
=
0 ;
(B
. (i
+ 1))
= ((A
. i)
mod (B
. i)) by
A1;
hence contradiction by
A5,
A6,
INT_1:def 10;
end;
hence thesis by
A4,
A1,
Lm3;
end;
hence
P[(i
+ 1)];
end;
for i be
Nat holds
P[i] from
NAT_1:sch 2(
A2,
A3);
hence thesis;
end;
Lm5: for a,b be
Integer, A,B be
sequence of
NAT st ((A
.
0 )
=
|.a.| & (B
.
0 )
=
|.b.| & (for i be
Nat holds (A
. (i
+ 1))
= (B
. i) & (B
. (i
+ 1))
= ((A
. i)
mod (B
. i)))) holds { i where i be
Nat : (B
. i)
=
0 } is non
empty
Subset of
NAT
proof
let a,b be
Integer, A,B be
sequence of
NAT ;
assume
A1: (A
.
0 )
=
|.a.| & (B
.
0 )
=
|.b.| & (for i be
Nat holds (A
. (i
+ 1))
= (B
. i) & (B
. (i
+ 1))
= ((A
. i)
mod (B
. i)));
A2: for x be
object st x
in { i where i be
Nat : (B
. i)
=
0 } holds x
in
NAT
proof
let x be
object;
assume x
in { i where i be
Nat : (B
. i)
=
0 };
then ex i be
Nat st x
= i & (B
. i)
=
0 ;
hence x
in
NAT by
ORDINAL1:def 12;
end;
ex m0 be
Nat st (B
. m0)
=
0
proof
assume
A3: not (ex m0 be
Nat st (B
. m0)
=
0 );
A4: for i be
Nat holds (B
. (i
+ 1))
<= ((B
. i)
- 1)
proof
let i be
Nat;
A5: (B
. i)
<>
0 by
A3;
(B
. (i
+ 1))
= ((A
. i)
mod (B
. i)) by
A1;
then ((B
. (i
+ 1))
+ 1)
<= (B
. i) by
NAT_1: 13,
A5,
INT_1: 58;
then (((B
. (i
+ 1))
+ 1)
- 1)
<= ((B
. i)
- 1) by
XREAL_1: 9;
hence (B
. (i
+ 1))
<= ((B
. i)
- 1);
end;
defpred
P[
Nat] means (B
. $1)
<= ((B
.
0 )
- $1);
A6:
P[
0 ];
A7: for i be
Nat st
P[i] holds
P[(i
+ 1)]
proof
let i be
Nat;
assume
A8:
P[i];
A9: (B
. (i
+ 1))
<= ((B
. i)
- 1) by
A4;
((B
. i)
- 1)
<= (((B
.
0 )
- i)
- 1) by
A8,
XREAL_1: 9;
hence
P[(i
+ 1)] by
A9,
XXREAL_0: 2;
end;
A10: for i be
Nat holds
P[i] from
NAT_1:sch 2(
A6,
A7);
(B
. (B
.
0 ))
<= ((B
.
0 )
- (B
.
0 )) by
A10;
hence contradiction by
A3,
NAT_1: 14;
end;
then
consider m0 be
Nat such that
A11: (B
. m0)
=
0 ;
m0
in { i where i be
Nat : (B
. i)
=
0 } by
A11;
hence thesis by
A2,
TARSKI:def 3;
end;
theorem ::
NTALGO_1:2
for a,b be
Integer holds (
ALGO_GCD (a,b))
= (a
gcd b)
proof
let a,b be
Integer;
consider A,B be
sequence of
NAT such that
A1: (A
.
0 )
=
|.a.| & (B
.
0 )
=
|.b.| & (for i be
Nat holds (A
. (i
+ 1))
= (B
. i) & (B
. (i
+ 1))
= ((A
. i)
mod (B
. i))) & (
ALGO_GCD (a,b))
= (A
. (
min* { i where i be
Nat : (B
. i)
=
0 })) by
Def1;
set m0 = (
min* { i where i be
Nat : (B
. i)
=
0 });
A2: { i where i be
Nat : (B
. i)
=
0 } is non
empty
Subset of
NAT by
A1,
Lm5;
then m0
in { i where i be
Nat : (B
. i)
=
0 } by
NAT_1:def 1;
then
A3: ex i be
Nat st m0
= i & (B
. i)
=
0 ;
per cases ;
suppose m0
=
0 ;
hence (
ALGO_GCD (a,b))
= ((A
.
0 )
gcd (B
.
0 )) by
A3,
NEWTON: 52,
A1
.= (a
gcd b) by
A1,
INT_2: 34;
end;
suppose m0
<>
0 ;
then (1
- 1)
<= (m0
- 1) by
XREAL_1: 9,
NAT_1: 14;
then
reconsider m1 = (m0
- 1) as
Element of
NAT by
INT_1: 3;
A5: (B
. m1)
<>
0
proof
assume (B
. m1)
=
0 ;
then
A6: m1
in { i where i be
Nat : (B
. i)
=
0 };
(m0
- 1)
< (m0
-
0 ) by
XREAL_1: 15;
hence contradiction by
A6,
A2,
NAT_1:def 1;
end;
then
A7: ((A
.
0 )
gcd (B
.
0 ))
= ((A
. m1)
gcd (B
. m1)) by
A1,
Lm4;
A8: ((A
. m1)
gcd (B
. m1))
= ((A
. (m1
+ 1))
gcd (B
. (m1
+ 1))) by
Lm3,
A5,
A1;
((A
. m0)
gcd (B
. m0))
= (
ALGO_GCD (a,b)) by
A1,
NEWTON: 52,
A3;
hence thesis by
A8,
A7,
A1,
INT_2: 34;
end;
end;
begin
scheme ::
NTALGO_1:sch1
QuadChoiceRec { A,B,C,D() -> non
empty
set , A0() ->
Element of A() , B0() ->
Element of B() , C0() ->
Element of C() , D0() ->
Element of D() , P[
object,
object,
object,
object,
object,
object,
object,
object,
object] } :
ex f be
sequence of A(), g be
sequence of B(), h be
sequence of C(), i be
sequence of D() st (f
.
0 )
= A0() & (g
.
0 )
= B0() & (h
.
0 )
= C0() & (i
.
0 )
= D0() & for n be
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 be
Nat, x be
Element of A(), y be
Element of B(), z be
Element of C(), w be
Element of D() holds ex x1 be
Element of A(), y1 be
Element of B(), z1 be
Element of C(), w1 be
Element of D() st P[n, x, y, z, w, x1, y1, z1, w1];
defpred
P1[
object,
object,
object,
object,
object] means P[$1, ($2
`1 ), ($2
`2 ), ($3
`1 ), ($3
`2 ), ($4
`1 ), ($4
`2 ), ($5
`1 ), ($5
`2 )];
A2: for n be
Nat, x be
Element of
[:A(), B():], y be
Element of
[:C(), D():] holds ex z be
Element of
[:A(), B():], w be
Element of
[:C(), D():] st
P1[n, x, y, z, w]
proof
let n be
Nat, x be
Element of
[:A(), B():], y be
Element of
[:C(), D():];
(x
`1 ) is
Element of A() & (x
`2 ) is
Element of B() & (y
`1 ) is
Element of C() & (y
`2 ) is
Element of D() by
MCART_1: 10;
then
consider ai be
Element of A(), bi be
Element of B(), ci be
Element of C(), di be
Element of D() such that
A3: P[n, (x
`1 ), (x
`2 ), (y
`1 ), (y
`2 ), ai, bi, ci, di] by
A1;
reconsider z =
[ai, bi] as
Element of
[:A(), B():] by
ZFMISC_1: 87;
reconsider w =
[ci, di] as
Element of
[:C(), D():] by
ZFMISC_1: 87;
take z, w;
thus thesis by
A3;
end;
reconsider AB0 =
[A0(), B0()] as
Element of
[:A(), B():] by
ZFMISC_1: 87;
reconsider CD0 =
[C0(), D0()] as
Element of
[:C(), D():] by
ZFMISC_1: 87;
consider fg be
sequence of
[:A(), B():], hi be
sequence of
[:C(), D():] such that
A4: (fg
.
0 )
= AB0 and
A5: (hi
.
0 )
= CD0 and
A6: for e be
Nat holds
P1[e, (fg
. e), (hi
. e), (fg
. (e
+ 1)), (hi
. (e
+ 1))] from
RECDEF_2:sch 3(
A2);
take (
pr1 fg), (
pr2 fg), (
pr1 hi), (
pr2 hi);
((fg
.
0 )
`1 )
= ((
pr1 fg)
.
0 ) & ((fg
.
0 )
`2 )
= ((
pr2 fg)
.
0 ) & ((hi
.
0 )
`1 )
= ((
pr1 hi)
.
0 ) & ((hi
.
0 )
`2 )
= ((
pr2 hi)
.
0 ) by
FUNCT_2:def 5,
FUNCT_2:def 6;
hence ((
pr1 fg)
.
0 )
= A0() & ((
pr2 fg)
.
0 )
= B0() & ((
pr1 hi)
.
0 )
= C0() & ((
pr2 hi)
.
0 )
= D0() by
A4,
A5;
let i be
Nat;
A7: ((fg
. (i
+ 1))
`1 )
= ((
pr1 fg)
. (i
+ 1)) & ((fg
. (i
+ 1))
`2 )
= ((
pr2 fg)
. (i
+ 1)) & ((hi
. (i
+ 1))
`1 )
= ((
pr1 hi)
. (i
+ 1)) & ((hi
. (i
+ 1))
`2 )
= ((
pr2 hi)
. (i
+ 1)) by
FUNCT_2:def 5,
FUNCT_2:def 6;
reconsider i as
Element of
NAT by
ORDINAL1:def 12;
((fg
. i)
`1 )
= ((
pr1 fg)
. i) & ((fg
. i)
`2 )
= ((
pr2 fg)
. i) & ((hi
. i)
`1 )
= ((
pr1 hi)
. i) & ((hi
. i)
`2 )
= ((
pr2 hi)
. i) by
FUNCT_2:def 5,
FUNCT_2:def 6;
hence thesis by
A6,
A7;
end;
Lm6: for x,y be
Element of
INT holds ex g,w,q,t be
sequence of
INT , a,b,v,u be
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 be
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
let x,y be
Element of
INT ;
defpred
P[
Nat,
Integer,
Integer,
Integer,
Integer,
Integer,
Integer,
Integer,
Integer] means $6
= ($4
div $5) & $7
= ($4
mod $5) & $8
= $5 & $9
= $7;
A1: for n be
Nat, x be
Element of
INT , y be
Element of
INT , z be
Element of
INT , w be
Element of
INT holds ex x1 be
Element of
INT , y1 be
Element of
INT , z1 be
Element of
INT , w1 be
Element of
INT st
P[n, x, y, z, w, x1, y1, z1, w1]
proof
let n be
Nat, x,y,z,w be
Element of
INT ;
reconsider x1 = (z
div w) as
Element of
INT by
INT_1:def 2;
reconsider y1 = (z
mod w) as
Element of
INT by
INT_1:def 2;
set z1 = w;
set w1 = y1;
take x1, y1, z1, w1;
thus
P[n, x, y, z, w, x1, y1, z1, w1];
end;
reconsider i1 = 1 as
Element of
INT by
INT_1:def 2;
reconsider i0 =
0 as
Element of
INT by
INT_1:def 2;
consider q,t,g,w be
sequence of
INT such that
A2: (q
.
0 )
= i0 & (t
.
0 )
= i0 & (g
.
0 )
= x & (w
.
0 )
= y & for i be
Nat holds
P[i, (q
. i), (t
. i), (g
. i), (w
. i), (q
. (i
+ 1)), (t
. (i
+ 1)), (g
. (i
+ 1)), (w
. (i
+ 1))] from
QuadChoiceRec(
A1);
defpred
Q[
Nat,
Integer,
Integer,
Integer,
Integer,
Integer,
Integer,
Integer,
Integer] means $6
= $4 & $7
= $5 & $8
= ($2
- ((q
. ($1
+ 1))
* $4)) & $9
= ($3
- ((q
. ($1
+ 1))
* $5));
A3: for n be
Nat, x,y,z,w be
Element of
INT holds ex x1,y1,z1,w1 be
Element of
INT st
Q[n, x, y, z, w, x1, y1, z1, w1]
proof
let n be
Nat, x,y,z,w be
Element of
INT ;
reconsider qn1 = (q
. (n
+ 1)) as
Element of
INT ;
set x1 = z;
set y1 = w;
reconsider z1 = (x
- ((q
. (n
+ 1))
* z)) as
Element of
INT by
INT_1:def 2;
reconsider w1 = (y
- ((q
. (n
+ 1))
* w)) as
Element of
INT by
INT_1:def 2;
take x1, y1, z1, w1;
thus
Q[n, x, y, z, w, x1, y1, z1, w1];
end;
consider a,b,u,v be
sequence of
INT such that
A4: (a
.
0 )
= i1 & (b
.
0 )
= i0 & (u
.
0 )
= i0 & (v
.
0 )
= i1 & for i be
Nat holds
Q[i, (a
. i), (b
. i), (u
. i), (v
. i), (a
. (i
+ 1)), (b
. (i
+ 1)), (u
. (i
+ 1)), (v
. (i
+ 1))] from
QuadChoiceRec(
A3);
take g, w, q, t, a, b, v, u;
thus thesis by
A2,
A4;
end;
Lm7: for x,y be
Integer, g1,w1,q1,t1,a1,b1,v1,u1,g2,w2,q2,t2,a2,b2,v2,u2 be
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 be
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 be
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
let x,y be
Integer, g1,w1,q1,t1,a1,b1,v1,u1,g2,w2,q2,t2,a2,b2,v2,u2 be
sequence of
INT ;
assume
A1: ((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 be
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))));
assume
A2: ((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 be
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))));
defpred
P[
Nat] means (g1
. $1)
= (g2
. $1) & (w1
. $1)
= (w2
. $1) & (q1
. $1)
= (q2
. $1) & (t1
. $1)
= (t2
. $1) & (a1
. $1)
= (a2
. $1) & (b1
. $1)
= (b2
. $1) & (v1
. $1)
= (v2
. $1) & (u1
. $1)
= (u2
. $1);
A3:
P[
0 ] by
A1,
A2;
A4: for n be
Nat st
P[n] holds
P[(n
+ 1)]
proof
let n be
Nat;
assume
A5:
P[n];
A6: (q1
. (n
+ 1))
= ((g2
. n)
div (w2
. n)) by
A1,
A5
.= (q2
. (n
+ 1)) by
A2;
A7: (t1
. (n
+ 1))
= ((g2
. n)
mod (w2
. n)) by
A1,
A5
.= (t2
. (n
+ 1)) by
A2;
A8: (a1
. (n
+ 1))
= (u2
. n) by
A1,
A5
.= (a2
. (n
+ 1)) by
A2;
A9: (b1
. (n
+ 1))
= (v2
. n) by
A5,
A1
.= (b2
. (n
+ 1)) by
A2;
A10: (g1
. (n
+ 1))
= (w2
. n) by
A5,
A1
.= (g2
. (n
+ 1)) by
A2;
A11: (u1
. (n
+ 1))
= ((a2
. n)
- ((q1
. (n
+ 1))
* (u2
. n))) by
A1,
A5
.= (u2
. (n
+ 1)) by
A2,
A6;
A12: (v1
. (n
+ 1))
= ((b2
. n)
- ((q1
. (n
+ 1))
* (v2
. n))) by
A5,
A1
.= (v2
. (n
+ 1)) by
A2,
A6;
(w1
. (n
+ 1))
= (t2
. (n
+ 1)) by
A7,
A1
.= (w2
. (n
+ 1)) by
A2;
hence
P[(n
+ 1)] by
A6,
A7,
A8,
A9,
A10,
A11,
A12;
end;
for n be
Nat holds
P[n] from
NAT_1:sch 2(
A3,
A4);
hence thesis;
end;
definition
let x,y be
Element of
INT ;
::
NTALGO_1:def2
func
ALGO_EXGCD (x,y) ->
Element of
[:
INT ,
INT ,
INT :] means
:
Def2: ex g,w,q,t be
sequence of
INT , a,b,v,u be
sequence of
INT , istop be
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 be
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 be
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
proof
consider g,w,q,t be
sequence of
INT , a,b,v,u be
sequence of
INT such that
A1: (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 be
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))) by
Lm6;
set istop = (
min* { i where i be
Nat : (w
. i)
=
0 });
now
per cases ;
suppose
A2:
0
<= (g
. istop);
[(a
. istop), (b
. istop), (g
. istop)]
in
[:
INT ,
INT ,
INT :] by
MCART_1: 69;
hence ex xx be
Element of
[:
INT ,
INT ,
INT :] st (
0
<= (g
. istop) implies xx
=
[(a
. istop), (b
. istop), (g
. istop)]) & ((g
. istop)
<
0 implies xx
=
[(
- (a
. istop)), (
- (b
. istop)), (
- (g
. istop))]) by
A2;
end;
suppose
A3: (g
. istop)
<
0 ;
A4: (
- (g
. istop))
in
INT by
INT_1:def 2;
(
- (a
. istop))
in
INT & (
- (b
. istop))
in
INT by
INT_1:def 2;
then
[(
- (a
. istop)), (
- (b
. istop)), (
- (g
. istop))]
in
[:
INT ,
INT ,
INT :] by
A4,
MCART_1: 69;
hence ex xx be
Element of
[:
INT ,
INT ,
INT :] st (
0
<= (g
. istop) implies xx
=
[(a
. istop), (b
. istop), (g
. istop)]) & ((g
. istop)
<
0 implies xx
=
[(
- (a
. istop)), (
- (b
. istop)), (
- (g
. istop))]) by
A3;
end;
end;
then
consider xx be
Element of
[:
INT ,
INT ,
INT :] such that
A5: (
0
<= (g
. istop) implies xx
=
[(a
. istop), (b
. istop), (g
. istop)]) & ((g
. istop)
<
0 implies xx
=
[(
- (a
. istop)), (
- (b
. istop)), (
- (g
. istop))]);
take xx;
thus thesis by
A1,
A5;
end;
uniqueness
proof
let s1,s2 be
Element of
[:
INT ,
INT ,
INT :];
assume
A6: ex g1,w1,q1,t1,a1,b1,v1,u1 be
sequence of
INT , istop1 be
Nat 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 be
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)))) & istop1
= (
min* { i where i be
Nat : (w1
. i)
=
0 }) & (
0
<= (g1
. istop1) implies s1
=
[(a1
. istop1), (b1
. istop1), (g1
. istop1)]) & ((g1
. istop1)
<
0 implies s1
=
[(
- (a1
. istop1)), (
- (b1
. istop1)), (
- (g1
. istop1))]);
assume
A7: ex g2,w2,q2,t2 be
sequence of
INT , a2,b2,v2,u2 be
sequence of
INT , istop2 be
Nat st ((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 be
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)))) & istop2
= (
min* { i where i be
Nat : (w2
. i)
=
0 }) & (
0
<= (g2
. istop2) implies s2
=
[(a2
. istop2), (b2
. istop2), (g2
. istop2)]) & ((g2
. istop2)
<
0 implies s2
=
[(
- (a2
. istop2)), (
- (b2
. istop2)), (
- (g2
. istop2))]);
consider g1,w1,q1,t1 be
sequence of
INT , a1,b1,v1,u1 be
sequence of
INT , istop1 be
Nat such that
A8: ((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 be
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)))) & istop1
= (
min* { k where k be
Nat : (w1
. k)
=
0 }) & (
0
<= (g1
. istop1) implies s1
=
[(a1
. istop1), (b1
. istop1), (g1
. istop1)]) & ((g1
. istop1)
<
0 implies s1
=
[(
- (a1
. istop1)), (
- (b1
. istop1)), (
- (g1
. istop1))]) by
A6;
consider g2,w2,q2,t2 be
sequence of
INT , a2,b2,v2,u2 be
sequence of
INT , istop2 be
Nat such that
A9: ((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 be
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)))) & istop2
= (
min* { k where k be
Nat : (w2
. k)
=
0 }) & (
0
<= (g2
. istop2) implies s2
=
[(a2
. istop2), (b2
. istop2), (g2
. istop2)]) & ((g2
. istop2)
<
0 implies s2
=
[(
- (a2
. istop2)), (
- (b2
. istop2)), (
- (g2
. istop2))]) by
A7;
g1
= g2 & w1
= w2 & a1
= a2 & b1
= b2 by
A8,
A9,
Lm7;
hence s1
= s2 by
A8,
A9;
end;
end
Lm8: for a,b be
Element of
INT , A,B be
sequence of
INT st ((A
.
0 )
= a & (B
.
0 )
= b & (for i be
Nat holds (A
. (i
+ 1))
= (B
. i) & (B
. (i
+ 1))
= ((A
. i)
mod (B
. i)))) holds for i be
Nat st (B
. i)
<>
0 holds ((A
. i)
gcd (B
. i))
= ((A
. (i
+ 1))
gcd (B
. (i
+ 1)))
proof
let a,b be
Element of
INT , A,B be
sequence of
INT ;
assume
A1: (A
.
0 )
= a & (B
.
0 )
= b & (for i be
Nat holds (A
. (i
+ 1))
= (B
. i) & (B
. (i
+ 1))
= ((A
. i)
mod (B
. i)));
let i be
Nat;
assume
A2: (B
. i)
<>
0 ;
set k = ((A
. i)
gcd (B
. i));
A3: (A
. (i
+ 1))
= (B
. i) by
A1;
A4: (B
. (i
+ 1))
= ((A
. i)
mod (B
. i)) by
A1;
A5: k
divides (A
. (i
+ 1)) by
A3,
INT_2:def 2;
A6: k
divides (B
. (i
+ 1))
proof
A7: (B
. (i
+ 1))
= ((A
. i)
- (((A
. i)
div (B
. i))
* (B
. i))) by
A4,
A2,
INT_1:def 10;
A8: k
divides (A
. i) by
INT_2:def 2;
k
divides (B
. i) by
INT_2:def 2;
then
consider s,t be
Integer such that
A11: (B
. (i
+ 1))
= ((k
* s)
- (((A
. i)
div (B
. i))
* (k
* t))) by
A7,
A8;
(B
. (i
+ 1))
= ((s
- (((A
. i)
div (B
. i))
* t))
* k) by
A11;
hence k
divides (B
. (i
+ 1));
end;
for m be
Integer st m
divides (A
. (i
+ 1)) & m
divides (B
. (i
+ 1)) holds m
divides k
proof
let m be
Integer;
assume
A12: m
divides (A
. (i
+ 1)) & m
divides (B
. (i
+ 1));
then
A13: m
divides (B
. i) by
A1;
A14: m
divides (A
. i)
proof
(B
. (i
+ 1))
= ((A
. i)
- (((A
. i)
div (B
. i))
* (B
. i))) by
A4,
A2,
INT_1:def 10;
then
A15: (A
. i)
= ((B
. (i
+ 1))
+ (((A
. i)
div (B
. i))
* (B
. i)));
A16: ex s be
Integer st (B
. i)
= (m
* s) by
A13;
A17: ex t be
Integer st (B
. (i
+ 1))
= (m
* t) by
A12;
consider s,t be
Integer such that
A18: (A
. i)
= ((m
* s)
+ (((A
. i)
div (B
. i))
* (m
* t))) by
A15,
A16,
A17;
(A
. i)
= (m
* (s
+ (((A
. i)
div (B
. i))
* t))) by
A18;
hence m
divides (A
. i);
end;
thus m
divides k by
A13,
A14,
INT_2:def 2;
end;
hence ((A
. (i
+ 1))
gcd (B
. (i
+ 1)))
= k by
A5,
A6,
INT_2:def 2;
end;
Lm9: for a,b be
Element of
INT , A,B be
sequence of
INT st ((A
.
0 )
= a & (B
.
0 )
= b & (for i be
Nat holds (A
. (i
+ 1))
= (B
. i) & (B
. (i
+ 1))
= ((A
. i)
mod (B
. i)))) holds for i be
Nat st (B
. i)
<>
0 holds ((A
.
0 )
gcd (B
.
0 ))
= ((A
. i)
gcd (B
. i))
proof
let a,b be
Element of
INT , A,B be
sequence of
INT ;
assume
A1: (A
.
0 )
= a & (B
.
0 )
= b & (for i be
Nat holds (A
. (i
+ 1))
= (B
. i) & (B
. (i
+ 1))
= ((A
. i)
mod (B
. i)));
defpred
P[
Nat] means (B
. $1)
<>
0 implies ((A
.
0 )
gcd (B
.
0 ))
= ((A
. $1)
gcd (B
. $1));
A2:
P[
0 ];
A3: for i be
Nat st
P[i] holds
P[(i
+ 1)]
proof
let i be
Nat;
assume
A4:
P[i];
(B
. (i
+ 1))
<>
0 implies ((A
.
0 )
gcd (B
.
0 ))
= ((A
. (i
+ 1))
gcd (B
. (i
+ 1)))
proof
assume
A5: (B
. (i
+ 1))
<>
0 ;
(B
. i)
<>
0
proof
assume
A6: (B
. i)
=
0 ;
(B
. (i
+ 1))
= ((A
. i)
mod (B
. i)) by
A1;
hence contradiction by
A5,
A6,
INT_1:def 10;
end;
hence thesis by
A4,
A1,
Lm8;
end;
hence
P[(i
+ 1)];
end;
for i be
Nat holds
P[i] from
NAT_1:sch 2(
A2,
A3);
hence thesis;
end;
theorem ::
NTALGO_1:3
Th3: for i2,i1 be
Integer st i2
<=
0 holds (i1
mod i2)
<=
0
proof
let i2,i1 be
Integer;
assume
A1: i2
<=
0 ;
per cases by
A1;
suppose
A2: i2
<
0 ;
[\(i1
/ i2)/]
<= (i1
/ i2) by
INT_1:def 6;
then ((i1
/ i2)
* i2)
<= ((i1
div i2)
* i2) by
A2,
XREAL_1: 65;
then i1
<= ((i1
div i2)
* i2) by
A2,
XCMPLX_1: 87;
then (i1
- ((i1
div i2)
* i2))
<=
0 by
XREAL_1: 47;
hence (i1
mod i2)
<=
0 by
INT_1:def 10;
end;
suppose i2
=
0 ;
hence (i1
mod i2)
<=
0 by
INT_1:def 10;
end;
end;
theorem ::
NTALGO_1:4
Th4: for i2,i1 be
Integer st i2
<
0 holds (
- (i1
mod i2))
< (
- i2)
proof
let i2,i1 be
Integer;
assume
A1: i2
<
0 ;
((i1
/ i2)
- 1)
<
[\(i1
/ i2)/] by
INT_1:def 6;
then ((i1
div i2)
* i2)
< (((i1
/ i2)
- 1)
* i2) by
A1,
XREAL_1: 69;
then ((i1
div i2)
* i2)
< (((i1
/ i2)
* i2)
- (1
* i2));
then ((i1
div i2)
* i2)
< (i1
- i2) by
A1,
XCMPLX_1: 87;
then (((i1
div i2)
* i2)
- i1)
< ((i1
- i2)
- i1) by
XREAL_1: 14;
then (
- (i1
- ((i1
div i2)
* i2)))
< (
- i2);
hence (
- (i1
mod i2))
< (
- i2) by
A1,
INT_1:def 10;
end;
theorem ::
NTALGO_1:5
Th5: for x,y be
Integer st
|.y.|
<>
0 holds
|.(x
mod y).|
<
|.y.|
proof
let x,y be
Integer;
assume
A1:
|.y.|
<>
0 ;
per cases ;
suppose
A2:
0
< y;
then (x
mod y)
< y by
INT_1: 58;
then
A4:
|.(x
mod y).|
< y by
ABSVALUE:def 1,
A2,
INT_1: 57;
y
<=
|.y.| by
ABSVALUE: 4;
hence
|.(x
mod y).|
<
|.y.| by
A4,
XXREAL_0: 2;
end;
suppose
A5: y
<=
0 ;
A6: y
<>
0 by
A1,
ABSVALUE: 2;
then
A7: (
- (x
mod y))
< (
- y) by
Th4,
A5;
A8: (x
mod y)
<=
0 by
A5,
Th3;
|.(x
mod y).|
= (
- (x
mod y))
proof
per cases ;
suppose (x
mod y)
=
0 ;
hence
|.(x
mod y).|
= (
- (x
mod y)) by
ABSVALUE: 2;
end;
suppose (x
mod y)
<>
0 ;
hence
|.(x
mod y).|
= (
- (x
mod y)) by
A8,
ABSVALUE:def 1;
end;
end;
hence
|.(x
mod y).|
<
|.y.| by
A7,
A6,
A5,
ABSVALUE:def 1;
end;
end;
Lm10: for a,b be
Element of
INT , A,B be
sequence of
INT st ((A
.
0 )
= a & (B
.
0 )
= b & (for i be
Nat holds (A
. (i
+ 1))
= (B
. i) & (B
. (i
+ 1))
= ((A
. i)
mod (B
. i)))) holds { i where i be
Nat : (B
. i)
=
0 } is non
empty
Subset of
NAT
proof
let a,b be
Element of
INT , A,B be
sequence of
INT ;
assume
A1: (A
.
0 )
= a & (B
.
0 )
= b & (for i be
Nat holds (A
. (i
+ 1))
= (B
. i) & (B
. (i
+ 1))
= ((A
. i)
mod (B
. i)));
A2: for x be
object st x
in { i where i be
Nat : (B
. i)
=
0 } holds x
in
NAT
proof
let x be
object;
assume x
in { i where i be
Nat : (B
. i)
=
0 };
then ex i be
Nat st x
= i & (B
. i)
=
0 ;
hence x
in
NAT by
ORDINAL1:def 12;
end;
ex m0 be
Nat st (B
. m0)
=
0
proof
assume
A3: not (ex m0 be
Nat st (B
. m0)
=
0 );
A4: for m0 be
Nat holds
|.(B
. m0).|
<>
0 by
A3,
ABSVALUE: 2;
A5: for i be
Nat holds
|.(B
. (i
+ 1)).|
<= (
|.(B
. i).|
- 1)
proof
let i be
Nat;
|.(B
. (i
+ 1)).|
=
|.((A
. i)
mod (B
. i)).| by
A1;
then
|.(B
. (i
+ 1)).|
<
|.(B
. i).| by
A4,
Th5;
then (
|.(B
. (i
+ 1)).|
+ 1)
<=
|.(B
. i).| by
NAT_1: 13;
then ((
|.(B
. (i
+ 1)).|
+ 1)
- 1)
<= (
|.(B
. i).|
- 1) by
XREAL_1: 9;
hence
|.(B
. (i
+ 1)).|
<= (
|.(B
. i).|
- 1);
end;
defpred
P[
Nat] means
|.(B
. $1).|
<= (
|.(B
.
0 ).|
- $1);
A6:
P[
0 ];
A7: for i be
Nat st
P[i] holds
P[(i
+ 1)]
proof
let i be
Nat;
assume
A8:
P[i];
A9:
|.(B
. (i
+ 1)).|
<= (
|.(B
. i).|
- 1) by
A5;
(
|.(B
. i).|
- 1)
<= ((
|.(B
.
0 ).|
- i)
- 1) by
A8,
XREAL_1: 9;
hence
P[(i
+ 1)] by
A9,
XXREAL_0: 2;
end;
A10: for i be
Nat holds
P[i] from
NAT_1:sch 2(
A6,
A7);
|.(B
.
|.(B
.
0 ).|).|
<= (
|.(B
.
0 ).|
-
|.(B
.
0 ).|) by
A10;
hence contradiction by
A4,
NAT_1: 14;
end;
then
consider m0 be
Nat such that
A11: (B
. m0)
=
0 ;
m0
in { i where i be
Nat : (B
. i)
=
0 } by
A11;
hence thesis by
A2,
TARSKI:def 3;
end;
Lm11: for a be
Element of
INT holds (a
gcd
0 )
=
|.a.| by
WSIERP_1: 8;
Lm12: for x,y be
Element of
INT , g,w,q,t be
sequence of
INT , a,b,v,u be
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 be
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 be
Nat st (w
. i)
<>
0 holds (((a
. (i
+ 1))
* x)
+ ((b
. (i
+ 1))
* y))
= (g
. (i
+ 1))
proof
let x,y be
Element of
INT , g,w,q,t be
sequence of
INT , a,b,v,u be
sequence of
INT ;
assume
A1: (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 be
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));
defpred
P[
Nat] means (w
. $1)
<>
0 implies ((((a
. $1)
* x)
+ ((b
. $1)
* y))
= (g
. $1) & (((a
. ($1
+ 1))
* x)
+ ((b
. ($1
+ 1))
* y))
= (g
. ($1
+ 1)));
A2:
P[
0 ]
proof
assume (w
.
0 )
<>
0 ;
reconsider I0 =
0 as
Element of
NAT ;
(((a
. (I0
+ 1))
* x)
+ ((b
. (I0
+ 1))
* y))
= (((u
.
0 )
* x)
+ ((b
. (I0
+ 1))
* y)) by
A1
.= ((
0
* x)
+ (1
* y)) by
A1
.= (g
. (I0
+ 1)) by
A1;
hence thesis by
A1;
end;
A3: for i be
Nat st
P[i] holds
P[(i
+ 1)]
proof
let i be
Nat;
assume
A4:
P[i];
assume
A5: (w
. (i
+ 1))
<>
0 ;
A6: (w
. i)
<>
0
proof
assume
A7: (w
. i)
=
0 ;
(t
. (i
+ 1))
= ((g
. i)
mod (w
. i)) by
A1
.=
0 by
A7,
INT_1:def 10;
hence contradiction by
A1,
A5;
end;
(((a
. ((i
+ 1)
+ 1))
* x)
+ ((b
. ((i
+ 1)
+ 1))
* y))
= (((u
. (i
+ 1))
* x)
+ ((b
. ((i
+ 1)
+ 1))
* y)) by
A1
.= (((u
. (i
+ 1))
* x)
+ ((v
. (i
+ 1))
* y)) by
A1
.= ((((a
. i)
- ((q
. (i
+ 1))
* (u
. i)))
* x)
+ ((v
. (i
+ 1))
* y)) by
A1
.= ((((a
. i)
- ((q
. (i
+ 1))
* (u
. i)))
* x)
+ (((b
. i)
- ((q
. (i
+ 1))
* (v
. i)))
* y)) by
A1
.= ((g
. i)
- ((q
. (i
+ 1))
* (((u
. i)
* x)
+ ((v
. i)
* y)))) by
A6,
A4
.= ((g
. i)
- ((q
. (i
+ 1))
* (((a
. (i
+ 1))
* x)
+ ((v
. i)
* y)))) by
A1
.= ((g
. i)
- ((q
. (i
+ 1))
* (g
. (i
+ 1)))) by
A6,
A4,
A1
.= ((g
. i)
- (((g
. i)
div (w
. i))
* (g
. (i
+ 1)))) by
A1
.= ((g
. i)
- (((g
. i)
div (w
. i))
* (w
. i))) by
A1
.= ((g
. i)
mod (w
. i)) by
A6,
INT_1:def 10
.= (t
. (i
+ 1)) by
A1
.= (w
. (i
+ 1)) by
A1
.= (g
. ((i
+ 1)
+ 1)) by
A1;
hence thesis by
A6,
A4;
end;
for i be
Nat holds
P[i] from
NAT_1:sch 2(
A2,
A3);
hence thesis;
end;
theorem ::
NTALGO_1:6
Th6: for x,y be
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
let x,y be
Element of
INT ;
consider g,w,q,t be
sequence of
INT , a,b,v,u be
sequence of
INT , istop be
Nat such that
A1: (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 be
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 be
Nat : (w
. i)
=
0 }) & (
0
<= (g
. istop) implies (
ALGO_EXGCD (x,y))
=
[(a
. istop), (b
. istop), (g
. istop)]) & ((g
. istop)
<
0 implies (
ALGO_EXGCD (x,y))
=
[(
- (a
. istop)), (
- (b
. istop)), (
- (g
. istop))]) by
Def2;
A2:
now
let i be
Nat;
thus (g
. (i
+ 1))
= (w
. i) by
A1;
thus (w
. (i
+ 1))
= (t
. (i
+ 1)) by
A1
.= ((g
. i)
mod (w
. i)) by
A1;
end;
A3: { i where i be
Nat : (w
. i)
=
0 } is non
empty
Subset of
NAT by
A1,
A2,
Lm10;
then istop
in { i where i be
Nat : (w
. i)
=
0 } by
A1,
NAT_1:def 1;
then
A4: ex i be
Nat st istop
= i & (w
. i)
=
0 ;
A5: ((
ALGO_EXGCD (x,y))
`3_3 )
=
|.(g
. istop).|
proof
per cases ;
suppose
0
<= (g
. istop);
hence ((
ALGO_EXGCD (x,y))
`3_3 )
=
|.(g
. istop).| by
A1,
ABSVALUE:def 1;
end;
suppose (g
. istop)
<
0 ;
hence ((
ALGO_EXGCD (x,y))
`3_3 )
=
|.(g
. istop).| by
A1,
ABSVALUE:def 1;
end;
end;
per cases ;
suppose
A7: istop
=
0 ;
hence ((
ALGO_EXGCD (x,y))
`3_3 )
= (x
gcd y) by
A1,
A4,
Lm11,
A5;
hence ((((
ALGO_EXGCD (x,y))
`1_3 )
* x)
+ (((
ALGO_EXGCD (x,y))
`2_3 )
* y))
= (x
gcd y) by
A1,
A7;
end;
suppose istop
<>
0 ;
then (1
- 1)
<= (istop
- 1) by
XREAL_1: 9,
NAT_1: 14;
then
reconsider m1 = (istop
- 1) as
Element of
NAT by
INT_1: 3;
A9: (w
. m1)
<>
0
proof
assume (w
. m1)
=
0 ;
then
A10: m1
in { i where i be
Nat : (w
. i)
=
0 };
(istop
- 1)
< (istop
-
0 ) by
XREAL_1: 15;
hence contradiction by
A10,
A1,
A3,
NAT_1:def 1;
end;
A11: ((g
. m1)
gcd (w
. m1))
= ((g
. (m1
+ 1))
gcd (w
. (m1
+ 1))) by
Lm8,
A1,
A9,
A2;
((g
. istop)
gcd (w
. istop))
= ((
ALGO_EXGCD (x,y))
`3_3 ) by
A5,
Lm11,
A4;
hence
A13: ((
ALGO_EXGCD (x,y))
`3_3 )
= (x
gcd y) by
A11,
A9,
A2,
Lm9,
A1;
(((a
. (m1
+ 1))
* x)
+ ((b
. (m1
+ 1))
* y))
= (g
. (m1
+ 1)) by
A9,
Lm12,
A1;
hence ((((
ALGO_EXGCD (x,y))
`1_3 )
* x)
+ (((
ALGO_EXGCD (x,y))
`2_3 )
* y))
= (x
gcd y) by
A13,
A1;
end;
end;
definition
let x,p be
Element of
INT ;
::
NTALGO_1:def3
func
ALGO_INVERSE (x,p) ->
Element of
INT means
:
Def3: for y be
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 be
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
proof
reconsider y = (x
mod p) as
Element of
INT by
INT_1:def 2;
now
per cases ;
suppose
A1: ((
ALGO_EXGCD (p,y))
`3_3 )
= 1;
now
per cases ;
suppose
A2: ((
ALGO_EXGCD (p,y))
`2_3 )
<
0 ;
reconsider z = ((
ALGO_EXGCD (p,y))
`2_3 ) as
Element of
INT ;
reconsider s = (p
+ z) as
Element of
INT by
INT_1:def 2;
ex z be
Element of
INT st z
= ((
ALGO_EXGCD (p,y))
`2_3 ) & s
= (p
+ z);
hence ex s be
Element of
INT st ((((
ALGO_EXGCD (p,y))
`2_3 )
<
0 ) implies (ex z be
Element of
INT st z
= ((
ALGO_EXGCD (p,y))
`2_3 ) & s
= (p
+ z))) & ((
0
<= ((
ALGO_EXGCD (p,y))
`2_3 )) implies s
= ((
ALGO_EXGCD (p,y))
`2_3 )) & (((
ALGO_EXGCD (p,y))
`3_3 )
<> 1 implies s
=
{} ) by
A2,
A1;
end;
suppose
A3: (
0
<= ((
ALGO_EXGCD (p,y))
`2_3 ));
reconsider s = ((
ALGO_EXGCD (p,y))
`2_3 ) as
Element of
INT ;
thus ex s be
Element of
INT st ((((
ALGO_EXGCD (p,y))
`2_3 )
<
0 ) implies (ex z be
Element of
INT st z
= ((
ALGO_EXGCD (p,y))
`2_3 ) & s
= (p
+ z))) & ((
0
<= ((
ALGO_EXGCD (p,y))
`2_3 )) implies s
= ((
ALGO_EXGCD (p,y))
`2_3 )) & (((
ALGO_EXGCD (p,y))
`3_3 )
<> 1 implies s
=
{} ) by
A3,
A1;
end;
end;
hence ex s be
Element of
INT st (((
ALGO_EXGCD (p,y))
`3_3 )
= 1 implies ((((
ALGO_EXGCD (p,y))
`2_3 )
<
0 ) implies (ex z be
Element of
INT st z
= ((
ALGO_EXGCD (p,y))
`2_3 ) & s
= (p
+ z))) & ((
0
<= ((
ALGO_EXGCD (p,y))
`2_3 )) implies s
= ((
ALGO_EXGCD (p,y))
`2_3 ))) & (((
ALGO_EXGCD (p,y))
`3_3 )
<> 1 implies s
=
{} );
end;
suppose
A4: ((
ALGO_EXGCD (p,y))
`3_3 )
<> 1;
reconsider s =
{} as
Element of
INT by
INT_1:def 2;
((
ALGO_EXGCD (p,y))
`3_3 )
<> 1 implies s
=
{} ;
hence ex s be
Element of
INT st (((
ALGO_EXGCD (p,y))
`3_3 )
= 1 implies ((((
ALGO_EXGCD (p,y))
`2_3 )
<
0 ) implies (ex z be
Element of
INT st z
= ((
ALGO_EXGCD (p,y))
`2_3 ) & s
= (p
+ z))) & ((
0
<= ((
ALGO_EXGCD (p,y))
`2_3 )) implies s
= ((
ALGO_EXGCD (p,y))
`2_3 ))) & (((
ALGO_EXGCD (p,y))
`3_3 )
<> 1 implies s
=
{} ) by
A4;
end;
end;
then
consider s be
Element of
INT such that
A5: (((
ALGO_EXGCD (p,y))
`3_3 )
= 1 implies ((((
ALGO_EXGCD (p,y))
`2_3 )
<
0 ) implies (ex z be
Element of
INT st z
= ((
ALGO_EXGCD (p,y))
`2_3 ) & s
= (p
+ z))) & ((
0
<= ((
ALGO_EXGCD (p,y))
`2_3 )) implies s
= ((
ALGO_EXGCD (p,y))
`2_3 ))) & (((
ALGO_EXGCD (p,y))
`3_3 )
<> 1 implies s
=
{} );
take s;
thus for y be
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 be
Element of
INT st z
= ((
ALGO_EXGCD (p,y))
`2_3 ) & s
= (p
+ z))) & ((
0
<= ((
ALGO_EXGCD (p,y))
`2_3 )) implies s
= ((
ALGO_EXGCD (p,y))
`2_3 ))) & (((
ALGO_EXGCD (p,y))
`3_3 )
<> 1 implies s
=
{} ) by
A5;
end;
uniqueness
proof
let s1,s2 be
Element of
INT ;
assume
A6: for y be
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 be
Element of
INT st z
= ((
ALGO_EXGCD (p,y))
`2_3 ) & s1
= (p
+ z))) & ((
0
<= ((
ALGO_EXGCD (p,y))
`2_3 )) implies s1
= ((
ALGO_EXGCD (p,y))
`2_3 ))) & (((
ALGO_EXGCD (p,y))
`3_3 )
<> 1 implies s1
=
{} );
assume
A7: for y be
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 be
Element of
INT st z
= ((
ALGO_EXGCD (p,y))
`2_3 ) & s2
= (p
+ z))) & ((
0
<= ((
ALGO_EXGCD (p,y))
`2_3 )) implies s2
= ((
ALGO_EXGCD (p,y))
`2_3 ))) & (((
ALGO_EXGCD (p,y))
`3_3 )
<> 1 implies s2
=
{} );
reconsider y = (x
mod p) as
Element of
INT by
INT_1:def 2;
thus s1
= s2
proof
per cases ;
suppose
A8: ((
ALGO_EXGCD (p,y))
`3_3 )
= 1;
thus s1
= s2
proof
per cases ;
suppose
A9: ((
ALGO_EXGCD (p,y))
`2_3 )
<
0 ;
then
A10: (ex z be
Element of
INT st z
= ((
ALGO_EXGCD (p,y))
`2_3 ) & s1
= (p
+ z)) by
A6,
A8;
(ex z be
Element of
INT st z
= ((
ALGO_EXGCD (p,y))
`2_3 ) & s2
= (p
+ z)) by
A7,
A8,
A9;
hence s1
= s2 by
A10;
end;
suppose
A11:
0
<= ((
ALGO_EXGCD (p,y))
`2_3 );
hence s1
= ((
ALGO_EXGCD (p,y))
`2_3 ) by
A8,
A6
.= s2 by
A11,
A8,
A7;
end;
end;
end;
suppose
A12: ((
ALGO_EXGCD (p,y))
`3_3 )
<> 1;
hence s1
=
{} by
A6
.= s2 by
A7,
A12;
end;
end;
end;
end
Lm13: for x,y,p be
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
let x,y,p be
Element of
INT ;
assume
A1: y
= (x
mod p) & ((
ALGO_EXGCD (p,y))
`3_3 )
= 1 & p
<>
0 ;
A2: ((
ALGO_EXGCD (p,y))
`3_3 )
= (p
gcd y) & ((((
ALGO_EXGCD (p,y))
`1_3 )
* p)
+ (((
ALGO_EXGCD (p,y))
`2_3 )
* y))
= (p
gcd y) by
Th6;
reconsider s1 = (((
ALGO_EXGCD (p,y))
`1_3 )
* p) as
Integer;
reconsider s2 = (((
ALGO_EXGCD (p,y))
`2_3 )
* y) as
Integer;
reconsider s3 = ((
ALGO_EXGCD (p,y))
`2_3 ) as
Integer;
A3: (p
mod p)
=
0 by
INT_1: 50;
A4: ((((
ALGO_EXGCD (p,y))
`1_3 )
* p)
mod p)
= (((((
ALGO_EXGCD (p,y))
`1_3 )
mod p)
* (p
mod p))
mod p) by
NAT_D: 67
.=
0 by
A3,
INT_1: 73;
reconsider I0 =
0 as
Element of
INT by
INT_1:def 2;
A5: (((((
ALGO_EXGCD (p,y))
`1_3 )
* p)
+ (((
ALGO_EXGCD (p,y))
`2_3 )
* y))
mod p)
= (((s1
mod p)
+ (s2
mod p))
mod p) by
NAT_D: 66
.= ((((
ALGO_EXGCD (p,y))
`2_3 )
* y)
mod p) by
Th1,
A4;
per cases ;
suppose ((
ALGO_EXGCD (p,y))
`2_3 )
<
0 ;
then
consider z be
Element of
INT such that
A6: z
= ((
ALGO_EXGCD (p,y))
`2_3 ) & (
ALGO_INVERSE (x,p))
= (p
+ z) by
Def3,
A1;
thus (((
ALGO_INVERSE (x,p))
* x)
mod p)
= (((p
* x)
+ (z
* x))
mod p) by
A6
.= ((z
* x)
mod p) by
NAT_D: 61
.= (((z
mod p)
* (x
mod p))
mod p) by
NAT_D: 67
.= (((z
mod p)
* ((x
mod p)
mod p))
mod p) by
Th1
.= (1
mod p) by
A5,
A6,
A2,
A1,
NAT_D: 67;
end;
suppose
0
<= ((
ALGO_EXGCD (p,y))
`2_3 );
hence (((
ALGO_INVERSE (x,p))
* x)
mod p)
= ((((
ALGO_EXGCD (p,y))
`2_3 )
* x)
mod p) by
Def3,
A1
.= (((s3
mod p)
* (x
mod p))
mod p) by
NAT_D: 67
.= (((s3
mod p)
* ((x
mod p)
mod p))
mod p) by
Th1
.= (1
mod p) by
A5,
A2,
A1,
NAT_D: 67;
end;
end;
theorem ::
NTALGO_1:7
Th7: for x,p,y be
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
let x,p,y be
Element of
INT ;
assume
A1: y
= (x
mod p) & ((
ALGO_EXGCD (p,y))
`3_3 )
= 1;
per cases ;
suppose
A2: p
=
0 ;
hence (((
ALGO_INVERSE (x,p))
* x)
mod p)
=
0 by
INT_1:def 10
.= (1
mod p) by
A2,
INT_1:def 10;
end;
suppose p
<>
0 ;
hence (((
ALGO_INVERSE (x,p))
* x)
mod p)
= (1
mod p) by
Lm13,
A1;
end;
end;
begin
definition
let nlist be non
empty
FinSequence of
[:
INT ,
INT :];
::
NTALGO_1:def4
func
ALGO_CRT (nlist) ->
Element of
INT means
:
Def4: ((
len nlist)
= 1 implies it
= ((nlist
. 1)
`1 )) & ((
len nlist)
<> 1 implies ex m,n,prodc,prodi be
FinSequence of
INT , M0,M be
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 be
Nat st 1
<= i & i
<= ((
len m)
- 1) holds ex d,x,y be
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 be
Nat st 1
<= i & i
<= ((
len m)
- 1) holds ex u,u0,u1 be
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
proof
per cases ;
suppose
A1: (
len nlist)
= 1;
then 1
in (
dom nlist) by
FINSEQ_3: 25;
then (nlist
. 1)
in
[:
INT ,
INT :] by
FINSEQ_2: 11;
then ((nlist
. 1)
`1 ) is
Element of
INT by
MCART_1: 10;
hence thesis by
A1;
end;
suppose
A2: (
len nlist)
<> 1;
defpred
P[
Nat,
Integer,
Integer] means ex x be
Element of
INT st x
= ((nlist
. $1)
`2 ) & $3
= ($2
* x);
reconsider i1 = 1 as
Element of
INT by
INT_1:def 1;
A3: for n be
Nat st 1
<= n & n
< (
len nlist) holds for z be
Element of
INT holds ex y be
Element of
INT st
P[n, z, y]
proof
let n be
Nat;
assume
A4: 1
<= n & n
< (
len nlist);
let z be
Element of
INT ;
n
in (
dom nlist) by
A4,
FINSEQ_3: 25;
then (nlist
. n)
in
[:
INT ,
INT :] by
FINSEQ_2: 11;
then
reconsider x = ((nlist
. n)
`2 ) as
Element of
INT by
MCART_1: 10;
reconsider y = (z
* x) as
Element of
INT by
INT_1:def 2;
take y;
thus
P[n, z, y];
end;
consider m be
FinSequence of
INT such that
A5: (
len m)
= (
len nlist) & ((m
. 1)
= i1 or (
len nlist)
=
0 ) & for i be
Nat st 1
<= i & i
< (
len nlist) holds
P[i, (m
. i), (m
. (i
+ 1))] from
RECDEF_1:sch 4(
A3);
A6: ((
len m)
- 1)
< ((
len m)
-
0 ) by
XREAL_1: 15;
A7: for i be
Nat st 1
<= i & i
<= ((
len m)
- 1) holds ex x be
Element of
INT st x
= ((nlist
. i)
`2 ) & (m
. (i
+ 1))
= ((m
. i)
* x)
proof
let i be
Nat;
assume 1
<= i & i
<= ((
len m)
- 1);
then 1
<= i & i
< (
len nlist) by
A5,
A6,
XXREAL_0: 2;
hence ex x be
Element of
INT st x
= ((nlist
. i)
`2 ) & (m
. (i
+ 1))
= ((m
. i)
* x) by
A5;
end;
A9: 1
<= (
len m) by
A5,
NAT_1: 14;
then (1
- 1)
<= ((
len m)
- 1) by
XREAL_1: 9;
then
reconsider lm = ((
len m)
- 1) as
Element of
NAT by
INT_1: 3;
defpred
P1[
Nat,
Integer] means ex d,x,y be
Element of
INT st x
= ((nlist
. $1)
`2 ) & (m
. ($1
+ 1))
= ((m
. $1)
* x) & y
= (m
. ($1
+ 1)) & d
= ((nlist
. ($1
+ 1))
`2 ) & $2
= (
ALGO_INVERSE (y,d));
A10: for n be
Nat st n
in (
Seg lm) holds ex z be
Element of
INT st
P1[n, z]
proof
let n be
Nat;
assume
A11: n
in (
Seg lm);
A12: 1
<= n & n
<= ((
len m)
- 1) by
A11,
FINSEQ_1: 1;
then
consider x be
Element of
INT such that
A13: x
= ((nlist
. n)
`2 ) & (m
. (n
+ 1))
= ((m
. n)
* x) by
A7;
reconsider y = (m
. (n
+ 1)) as
Element of
INT by
INT_1:def 2;
(n
+ 1)
<= (((
len m)
- 1)
+ 1) by
A12,
XREAL_1: 6;
then (n
+ 1)
in (
dom nlist) by
A5,
FINSEQ_3: 25,
NAT_1: 12;
then (nlist
. (n
+ 1))
in
[:
INT ,
INT :] by
FINSEQ_2: 11;
then
reconsider d = ((nlist
. (n
+ 1))
`2 ) as
Element of
INT by
MCART_1: 10;
reconsider w = (
ALGO_INVERSE (y,d)) as
Element of
INT ;
take w;
thus
P1[n, w] by
A13;
end;
consider prodi be
FinSequence of
INT such that
A14: (
dom prodi)
= (
Seg lm) & for k be
Nat st k
in (
Seg lm) holds
P1[k, (prodi
. k)] from
FINSEQ_1:sch 5(
A10);
A15: (
len prodi)
= ((
len nlist)
- 1) by
A5,
A14,
FINSEQ_1:def 3;
A16: for i be
Nat st 1
<= i & i
<= ((
len m)
- 1) holds ex d,x,y be
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))
proof
let i be
Nat;
assume 1
<= i & i
<= ((
len m)
- 1);
then i
in (
Seg lm);
hence ex d,x,y be
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)) by
A14;
end;
defpred
P2[
Nat,
Integer] means ex d,x,y be
Element of
INT st x
= ((nlist
. $1)
`2 ) & (m
. ($1
+ 1))
= ((m
. $1)
* x) & y
= (m
. ($1
+ 1)) & d
= ((nlist
. ($1
+ 1))
`2 ) & (prodi
. $1)
= (
ALGO_INVERSE (y,d)) & $2
= y;
A17: for n be
Nat st n
in (
Seg lm) holds ex z be
Element of
INT st
P2[n, z]
proof
let n be
Nat;
assume
A18: n
in (
Seg lm);
1
<= n & n
<= ((
len m)
- 1) by
A18,
FINSEQ_1: 1;
then
consider d,x,y be
Element of
INT such that
A19: x
= ((nlist
. n)
`2 ) & (m
. (n
+ 1))
= ((m
. n)
* x) & y
= (m
. (n
+ 1)) & d
= ((nlist
. (n
+ 1))
`2 ) & (prodi
. n)
= (
ALGO_INVERSE (y,d)) by
A16;
reconsider w = y as
Element of
INT ;
take w;
thus
P2[n, w] by
A19;
end;
consider prodc be
FinSequence of
INT such that
A20: (
dom prodc)
= (
Seg lm) & for k be
Nat st k
in (
Seg lm) holds
P2[k, (prodc
. k)] from
FINSEQ_1:sch 5(
A17);
A21: (
len prodc)
= ((
len nlist)
- 1) by
A5,
A20,
FINSEQ_1:def 3;
A22: for i be
Nat st 1
<= i & i
<= ((
len m)
- 1) holds ex d,x,y be
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
proof
let i be
Nat;
assume 1
<= i & i
<= ((
len m)
- 1);
then i
in (
Seg lm);
hence ex d,x,y be
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 by
A20;
end;
(
len m)
in (
dom nlist) by
A5,
A9,
FINSEQ_3: 25;
then (nlist
. (
len m))
in
[:
INT ,
INT :] by
FINSEQ_2: 11;
then
reconsider M0 = ((nlist
. (
len m))
`2 ) as
Element of
INT by
MCART_1: 10;
1
< (
len m) by
A9,
A2,
A5,
XXREAL_0: 1;
then (1
+ 1)
<= (
len m) by
NAT_1: 13;
then (2
- 1)
<= ((
len m)
- 1) by
XREAL_1: 9;
then
A23: lm
in (
dom prodc) by
A20;
prodc
in (
INT
* ) by
FINSEQ_1:def 11;
then
reconsider MM = (prodc
. ((
len m)
- 1)) as
Element of
INT by
A23,
FINSEQ_1: 84;
reconsider M = (MM
* M0) as
Element of
INT by
INT_1:def 2;
defpred
P4[
Nat,
Integer,
Integer] means ex u,u0,u1 be
Element of
INT st u0
= ((nlist
. ($1
+ 1))
`1 ) & u1
= ((nlist
. ($1
+ 1))
`2 ) & u
= (((u0
- $2)
* (prodi
. $1))
mod u1) & $3
= ($2
+ (u
* (prodc
. $1)));
reconsider i1 = 1 as
Element of
INT by
INT_1:def 1;
A24: for n be
Nat st 1
<= n & n
< (
len nlist) holds for z be
Element of
INT holds ex y be
Element of
INT st
P4[n, z, y]
proof
let n be
Nat;
assume
A25: 1
<= n & n
< (
len nlist);
let z be
Element of
INT ;
1
<= (n
+ 1) & (n
+ 1)
<= (
len m) by
A25,
A5,
NAT_1: 13;
then (n
+ 1)
in (
dom nlist) by
A5,
FINSEQ_3: 25;
then
A26: (nlist
. (n
+ 1))
in
[:
INT ,
INT :] by
FINSEQ_2: 11;
then
reconsider u0 = ((nlist
. (n
+ 1))
`1 ) as
Element of
INT by
MCART_1: 10;
reconsider u1 = ((nlist
. (n
+ 1))
`2 ) as
Element of
INT by
A26,
MCART_1: 10;
reconsider u = (((u0
- z)
* (prodi
. n))
mod u1) as
Element of
INT by
INT_1:def 2;
reconsider y = (z
+ (u
* (prodc
. n))) as
Element of
INT by
INT_1:def 2;
take y;
thus
P4[n, z, y];
end;
1
in (
dom nlist) by
A9,
A5,
FINSEQ_3: 25;
then (nlist
. 1)
in
[:
INT ,
INT :] by
FINSEQ_2: 11;
then
reconsider L1 = ((nlist
. 1)
`1 ) as
Element of
INT by
MCART_1: 10;
consider n be
FinSequence of
INT such that
A27: (
len n)
= (
len nlist) & ((n
. 1)
= L1 or (
len nlist)
=
0 ) & for i be
Nat st 1
<= i & i
< (
len nlist) holds
P4[i, (n
. i), (n
. (i
+ 1))] from
RECDEF_1:sch 4(
A24);
A28: for i be
Nat st 1
<= i & i
<= ((
len m)
- 1) holds ex u,u0,u1 be
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)))
proof
let i be
Nat;
assume 1
<= i & i
<= ((
len m)
- 1);
then
A29: 1
<= i & i
< (
len nlist) by
A5,
A6,
XXREAL_0: 2;
thus ex u,u0,u1 be
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))) by
A27,
A29;
end;
reconsider s = ((n
. (
len m))
mod M) as
Element of
INT by
INT_1:def 2;
M0
= ((nlist
. (
len m))
`2 ) & M
= ((prodc
. ((
len m)
- 1))
* M0) & s
= ((n
. (
len m))
mod M);
hence thesis by
A2,
A28,
A22,
A5,
A27,
A15,
A21;
end;
end;
uniqueness
proof
let s1,s2 be
Element of
INT ;
assume
A30: ((
len nlist)
= 1 implies s1
= ((nlist
. 1)
`1 )) & ((
len nlist)
<> 1 implies ex m,n,prodc,prodi be
FinSequence of
INT , M0,M be
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 be
Nat st 1
<= i & i
<= ((
len m)
- 1) holds ex d,x,y be
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 be
Nat st 1
<= i & i
<= ((
len m)
- 1) holds ex u,u0,u1 be
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)))) & s1
= ((n
. (
len m))
mod M));
assume
A31: ((
len nlist)
= 1 implies s2
= ((nlist
. 1)
`1 )) & ((
len nlist)
<> 1 implies ex m,n,prodc,prodi be
FinSequence of
INT , M0,M be
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 be
Nat st 1
<= i & i
<= ((
len m)
- 1) holds ex d,x,y be
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 be
Nat st 1
<= i & i
<= ((
len m)
- 1) holds ex u,u0,u1 be
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)))) & s2
= ((n
. (
len m))
mod M));
per cases ;
suppose (
len nlist)
= 1;
hence s1
= s2 by
A30,
A31;
end;
suppose
A33: (
len nlist)
<> 1;
consider m1,n1,prodc1,prodi1 be
FinSequence of
INT , M01,M1 be
Element of
INT such that
A34: (
len m1)
= (
len nlist) & (
len n1)
= (
len nlist) & (
len prodc1)
= ((
len nlist)
- 1) & (
len prodi1)
= ((
len nlist)
- 1) & (m1
. 1)
= 1 & (for i be
Nat st 1
<= i & i
<= ((
len m1)
- 1) holds ex d,x,y be
Element of
INT st x
= ((nlist
. i)
`2 ) & (m1
. (i
+ 1))
= ((m1
. i)
* x) & y
= (m1
. (i
+ 1)) & d
= ((nlist
. (i
+ 1))
`2 ) & (prodi1
. i)
= (
ALGO_INVERSE (y,d)) & (prodc1
. i)
= y) & M01
= ((nlist
. (
len m1))
`2 ) & M1
= ((prodc1
. ((
len m1)
- 1))
* M01) & (n1
. 1)
= ((nlist
. 1)
`1 ) & (for i be
Nat st 1
<= i & i
<= ((
len m1)
- 1) holds ex u,u0,u1 be
Element of
INT st u0
= ((nlist
. (i
+ 1))
`1 ) & u1
= ((nlist
. (i
+ 1))
`2 ) & u
= (((u0
- (n1
. i))
* (prodi1
. i))
mod u1) & (n1
. (i
+ 1))
= ((n1
. i)
+ (u
* (prodc1
. i)))) & s1
= ((n1
. (
len m1))
mod M1) by
A33,
A30;
consider m2,n2,prodc2,prodi2 be
FinSequence of
INT , M02,M2 be
Element of
INT such that
A35: (
len m2)
= (
len nlist) & (
len n2)
= (
len nlist) & (
len prodc2)
= ((
len nlist)
- 1) & (
len prodi2)
= ((
len nlist)
- 1) & (m2
. 1)
= 1 & (for i be
Nat st 1
<= i & i
<= ((
len m2)
- 1) holds ex d,x,y be
Element of
INT st x
= ((nlist
. i)
`2 ) & (m2
. (i
+ 1))
= ((m2
. i)
* x) & y
= (m2
. (i
+ 1)) & d
= ((nlist
. (i
+ 1))
`2 ) & (prodi2
. i)
= (
ALGO_INVERSE (y,d)) & (prodc2
. i)
= y) & M02
= ((nlist
. (
len m2))
`2 ) & M2
= ((prodc2
. ((
len m2)
- 1))
* M02) & (n2
. 1)
= ((nlist
. 1)
`1 ) & (for i be
Nat st 1
<= i & i
<= ((
len m2)
- 1) holds ex u,u0,u1 be
Element of
INT st u0
= ((nlist
. (i
+ 1))
`1 ) & u1
= ((nlist
. (i
+ 1))
`2 ) & u
= (((u0
- (n2
. i))
* (prodi2
. i))
mod u1) & (n2
. (i
+ 1))
= ((n2
. i)
+ (u
* (prodc2
. i)))) & s2
= ((n2
. (
len m2))
mod M2) by
A33,
A31;
defpred
EQ[
Nat] means 1
<= $1 & $1
<= (
len m1) implies (m1
. $1)
= (m2
. $1);
A36:
EQ[
0 ];
A37: for i be
Nat st
EQ[i] holds
EQ[(i
+ 1)]
proof
let i be
Nat;
assume
A38:
EQ[i];
assume 1
<= (i
+ 1) & (i
+ 1)
<= (
len m1);
then
A39: (1
- 1)
<= ((i
+ 1)
- 1) & ((i
+ 1)
- 1)
<= ((
len m1)
- 1) by
XREAL_1: 9;
A40: ((
len m1)
- 1)
<= ((
len m1)
-
0 ) by
XREAL_1: 13;
per cases ;
suppose
A41: i
=
0 ;
thus (m1
. (i
+ 1))
= (m2
. (i
+ 1)) by
A34,
A35,
A41;
end;
suppose
A42: i
<>
0 ;
then
A43: 1
<= i by
NAT_1: 14;
A44: ex d,x,y be
Element of
INT st x
= ((nlist
. i)
`2 ) & (m1
. (i
+ 1))
= ((m1
. i)
* x) & y
= (m1
. (i
+ 1)) & d
= ((nlist
. (i
+ 1))
`2 ) & (prodi1
. i)
= (
ALGO_INVERSE (y,d)) & (prodc1
. i)
= y by
A34,
A43,
A39;
1
<= i & i
<= ((
len m2)
- 1) by
A42,
A39,
A34,
A35,
NAT_1: 14;
then ex d,x,y be
Element of
INT st x
= ((nlist
. i)
`2 ) & (m2
. (i
+ 1))
= ((m2
. i)
* x) & y
= (m2
. (i
+ 1)) & d
= ((nlist
. (i
+ 1))
`2 ) & (prodi2
. i)
= (
ALGO_INVERSE (y,d)) & (prodc2
. i)
= y by
A35;
hence (m1
. (i
+ 1))
= (m2
. (i
+ 1)) by
A44,
A39,
A38,
A40,
A42,
NAT_1: 14,
XXREAL_0: 2;
end;
end;
A45: for k be
Nat holds
EQ[k] from
NAT_1:sch 2(
A36,
A37);
A46:
now
let i be
Nat;
assume
A47: 1
<= i & i
<= (
len prodc1);
then
A48: ex d,x,y be
Element of
INT st x
= ((nlist
. i)
`2 ) & (m1
. (i
+ 1))
= ((m1
. i)
* x) & y
= (m1
. (i
+ 1)) & d
= ((nlist
. (i
+ 1))
`2 ) & (prodi1
. i)
= (
ALGO_INVERSE (y,d)) & (prodc1
. i)
= y by
A34;
ex d,x,y be
Element of
INT st x
= ((nlist
. i)
`2 ) & (m2
. (i
+ 1))
= ((m2
. i)
* x) & y
= (m2
. (i
+ 1)) & d
= ((nlist
. (i
+ 1))
`2 ) & (prodi2
. i)
= (
ALGO_INVERSE (y,d)) & (prodc2
. i)
= y by
A35,
A47,
A34;
hence (prodc1
. i)
= (prodc2
. i) by
A48,
A34,
A35,
A45,
FINSEQ_1: 14;
end;
then
A49: prodc1
= prodc2 by
A34,
A35;
A50:
now
let i be
Nat;
assume
A51: 1
<= i & i
<= (
len prodi1);
then
A52: ex d,x,y be
Element of
INT st x
= ((nlist
. i)
`2 ) & (m1
. (i
+ 1))
= ((m1
. i)
* x) & y
= (m1
. (i
+ 1)) & d
= ((nlist
. (i
+ 1))
`2 ) & (prodi1
. i)
= (
ALGO_INVERSE (y,d)) & (prodc1
. i)
= y by
A34;
ex d,x,y be
Element of
INT st x
= ((nlist
. i)
`2 ) & (m2
. (i
+ 1))
= ((m2
. i)
* x) & y
= (m2
. (i
+ 1)) & d
= ((nlist
. (i
+ 1))
`2 ) & (prodi2
. i)
= (
ALGO_INVERSE (y,d)) & (prodc2
. i)
= y by
A35,
A51,
A34;
hence (prodi1
. i)
= (prodi2
. i) by
A52,
A45,
A34,
A35,
FINSEQ_1: 14;
end;
A53: M1
= M2 by
A35,
A34,
A46,
FINSEQ_1: 14;
defpred
EQ[
Nat] means 1
<= $1 & $1
<= (
len n1) implies (n1
. $1)
= (n2
. $1);
A54:
EQ[
0 ];
A55: for k be
Nat st
EQ[k] holds
EQ[(k
+ 1)]
proof
let k be
Nat;
assume
A56:
EQ[k];
assume 1
<= (k
+ 1) & (k
+ 1)
<= (
len n1);
then
A57: (1
- 1)
<= ((k
+ 1)
- 1) & ((k
+ 1)
- 1)
<= ((
len n1)
- 1) by
XREAL_1: 9;
A58: ((
len n1)
- 1)
<= ((
len n1)
-
0 ) by
XREAL_1: 13;
per cases ;
suppose k
=
0 ;
hence (n1
. (k
+ 1))
= (n2
. (k
+ 1)) by
A34,
A35;
end;
suppose
A60: k
<>
0 ;
then
A61: 1
<= k by
NAT_1: 14;
A62: ex u,u0,u1 be
Element of
INT st u0
= ((nlist
. (k
+ 1))
`1 ) & u1
= ((nlist
. (k
+ 1))
`2 ) & u
= (((u0
- (n1
. k))
* (prodi1
. k))
mod u1) & (n1
. (k
+ 1))
= ((n1
. k)
+ (u
* (prodc1
. k))) by
A61,
A57,
A34;
ex u,u0,u1 be
Element of
INT st u0
= ((nlist
. (k
+ 1))
`1 ) & u1
= ((nlist
. (k
+ 1))
`2 ) & u
= (((u0
- (n2
. k))
* (prodi2
. k))
mod u1) & (n2
. (k
+ 1))
= ((n2
. k)
+ (u
* (prodc2
. k))) by
A61,
A57,
A34,
A35;
hence (n1
. (k
+ 1))
= (n2
. (k
+ 1)) by
A49,
A62,
A56,
A58,
A60,
A57,
A34,
A35,
A50,
FINSEQ_1: 14,
NAT_1: 14,
XXREAL_0: 2;
end;
end;
for k be
Nat holds
EQ[k] from
NAT_1:sch 2(
A54,
A55);
hence s1
= s2 by
A53,
A34,
A35,
FINSEQ_1: 14;
end;
end;
end
theorem ::
NTALGO_1:8
Th8: for a,b be
Integer st b
<>
0 holds ((a
mod b),a)
are_congruent_mod b
proof
let a,b be
Integer;
assume b
<>
0 ;
then
A1: (a
mod b)
= (a
- ((a
div b)
* b)) by
INT_1:def 10;
reconsider c = (
- (a
div b)) as
Element of
INT by
INT_1:def 2;
take c;
thus thesis by
A1;
end;
theorem ::
NTALGO_1:9
for a,b be
Integer st b
<>
0 holds ((a
mod b)
gcd b)
= (a
gcd b) by
Th8,
WSIERP_1: 43;
theorem ::
NTALGO_1:10
Th10: for a,b,c be
Integer st c
<>
0 & a
= (b
mod c) & (b,c)
are_coprime holds (a,c)
are_coprime
proof
let a,b,c be
Integer;
assume
A1: c
<>
0 & a
= (b
mod c) & (b,c)
are_coprime ;
then (b
gcd c)
= 1 by
INT_2:def 3;
then (a
gcd c)
= 1 by
A1,
Th8,
WSIERP_1: 43;
hence thesis by
INT_2:def 3;
end;
Lm14: for a,b,c be
Integer st a
= (b
mod c) & c
<>
0 holds ex d be
Element of
INT st a
= (b
+ (d
* c))
proof
let a,b,c be
Integer;
assume a
= (b
mod c) & c
<>
0 ;
then
A1: b
= (((b
div c)
* c)
+ a) by
INT_1: 59;
reconsider x = (
- (b
div c)) as
Element of
INT by
INT_1:def 2;
take x;
thus thesis by
A1;
end;
Lm15: for b,m be
FinSequence of
INT st (
len b)
= (
len m) & (for i be
Nat st i
in (
Seg (
len b)) holds (b
. i)
<>
0 ) & (m
. 1)
= 1 holds for k be
Element of
NAT st 1
<= k & k
<= ((
len b)
- 1) & (for i be
Nat st 1
<= i & i
<= k holds (m
. (i
+ 1))
= ((m
. i)
* (b
. i))) holds (m
. (k
+ 1))
<>
0
proof
let b,m be
FinSequence of
INT ;
assume (
len b)
= (
len m);
assume
A1: (for i be
Nat st i
in (
Seg (
len b)) holds (b
. i)
<>
0 ) & (m
. 1)
= 1;
defpred
P[
Nat] means (1
<= $1 & $1
<= ((
len b)
- 1) & (for i be
Nat st 1
<= i & i
<= $1 holds (m
. (i
+ 1))
= ((m
. i)
* (b
. i)))) implies (m
. ($1
+ 1))
<>
0 ;
reconsider I0 =
0 as
Element of
NAT ;
A2:
P[
0 ];
A3: for k be
Nat st
P[k] holds
P[(k
+ 1)]
proof
let k be
Nat;
assume
A4:
P[k];
assume
A5: 1
<= (k
+ 1) & (k
+ 1)
<= ((
len b)
- 1) & (for i be
Nat st 1
<= i & i
<= (k
+ 1) holds (m
. (i
+ 1))
= ((m
. i)
* (b
. i)));
A6: k
<= (k
+ 1) by
NAT_1: 12;
per cases ;
suppose
A7: k
=
0 ;
A8: (m
. ((k
+ 1)
+ 1))
= ((m
. 1)
* (b
. 1)) by
A5,
A7
.= (b
. 1) by
A1;
(((
len b)
- 1)
+
0 qua
Nat)
<= (((
len b)
- 1)
+ 1) by
XREAL_1: 7;
then (k
+ 1)
<= (
len b) by
A5,
XXREAL_0: 2;
then 1
<= 1 & 1
<= (
len b) by
A5,
XXREAL_0: 2;
then 1
in (
Seg (
len b));
hence (m
. ((k
+ 1)
+ 1))
<>
0 by
A8,
A1;
end;
suppose
A9: k
<>
0 ;
A10:
now
let i be
Nat;
assume 1
<= i & i
<= k;
then 1
<= i & i
<= (k
+ 1) by
NAT_1: 12;
hence (m
. (i
+ 1))
= ((m
. i)
* (b
. i)) by
A5;
end;
thus (m
. ((k
+ 1)
+ 1))
<>
0
proof
A11: ((k
+ 1)
+ 1)
<= (((
len b)
- 1)
+ 1) by
A5,
XREAL_1: 6;
A12: (k
+ 1)
<= ((k
+ 1)
+ 1) by
NAT_1: 12;
A13: 1
<= (k
+ 1) by
NAT_1: 12;
(k
+ 1)
<= (
len b) by
A12,
A11,
XXREAL_0: 2;
then (k
+ 1)
in (
Seg (
len b)) by
A13;
then
A14: (b
. (k
+ 1))
<>
0 by
A1;
(m
. ((k
+ 1)
+ 1))
= ((m
. (k
+ 1))
* (b
. (k
+ 1))) by
A5;
hence (m
. ((k
+ 1)
+ 1))
<>
0 by
A14,
A10,
A4,
A5,
A6,
A9,
NAT_1: 14,
XCMPLX_1: 6,
XXREAL_0: 2;
end;
end;
end;
for k be
Nat holds
P[k] from
NAT_1:sch 2(
A2,
A3);
hence thesis;
end;
Lm16: for b,m be
FinSequence of
INT st 2
<= (
len b) & (for i,j be
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 be
Nat st 1
<= k & k
<= ((
len b)
- 1) & (for i be
Nat st 1
<= i & i
<= k holds (m
. (i
+ 1))
= ((m
. i)
* (b
. i))) holds for j be
Nat st (k
+ 1)
<= j & j
<= (
len b) holds ((m
. (k
+ 1)),(b
. j))
are_coprime
proof
let b,m be
FinSequence of
INT ;
assume 2
<= (
len b);
assume
A1: (for i,j be
Nat st i
in (
Seg (
len b)) & j
in (
Seg (
len b)) & i
<> j holds ((b
. i),(b
. j))
are_coprime ) & (m
. 1)
= 1;
defpred
P[
Nat] means (1
<= $1 & $1
<= ((
len b)
- 1) & (for i be
Nat st 1
<= i & i
<= $1 holds (m
. (i
+ 1))
= ((m
. i)
* (b
. i)))) implies for j be
Nat st ($1
+ 1)
<= j & j
<= (
len b) holds ((m
. ($1
+ 1)),(b
. j))
are_coprime ;
reconsider I0 =
0 as
Element of
NAT ;
A2:
P[
0 ];
A3: for k be
Nat st
P[k] holds
P[(k
+ 1)]
proof
let k be
Nat;
assume
A4:
P[k];
assume
A5: 1
<= (k
+ 1) & (k
+ 1)
<= ((
len b)
- 1) & (for i be
Nat st 1
<= i & i
<= (k
+ 1) holds (m
. (i
+ 1))
= ((m
. i)
* (b
. i)));
A6: k
<= (k
+ 1) by
NAT_1: 12;
per cases ;
suppose
A7: k
=
0 ;
A8: (m
. ((k
+ 1)
+ 1))
= ((m
. 1)
* (b
. 1)) by
A5,
A7
.= (b
. 1) by
A1;
for j be
Nat st ((k
+ 1)
+ 1)
<= j & j
<= (
len b) holds ((m
. ((k
+ 1)
+ 1)),(b
. j))
are_coprime
proof
let j be
Nat;
assume
A9: ((k
+ 1)
+ 1)
<= j & j
<= (
len b);
then
A10: 1
<= j & j
<= (
len b) by
A7,
XXREAL_0: 2;
then
A11: j
in (
Seg (
len b));
1
<= 1 & 1
<= (
len b) by
A10,
XXREAL_0: 2;
then
A12: 1
in (
Seg (
len b));
1
<> j by
A9,
A7;
hence ((m
. ((k
+ 1)
+ 1)),(b
. j))
are_coprime by
A8,
A1,
A11,
A12;
end;
hence thesis;
end;
suppose
A13: k
<>
0 ;
A14:
now
let i be
Nat;
assume 1
<= i & i
<= k;
then 1
<= i & i
<= (k
+ 1) by
NAT_1: 12;
hence (m
. (i
+ 1))
= ((m
. i)
* (b
. i)) by
A5;
end;
thus for j be
Nat st ((k
+ 1)
+ 1)
<= j & j
<= (
len b) holds ((m
. ((k
+ 1)
+ 1)),(b
. j))
are_coprime
proof
let j be
Nat;
assume
A15: ((k
+ 1)
+ 1)
<= j & j
<= (
len b);
(k
+ 1)
<= ((k
+ 1)
+ 1) by
NAT_1: 12;
then
A16: (k
+ 1)
<= j & j
<= (
len b) by
A15,
XXREAL_0: 2;
then
A17: ((m
. (k
+ 1)),(b
. j))
are_coprime by
A14,
A4,
A5,
A6,
A13,
NAT_1: 14,
XXREAL_0: 2;
A18: 1
<= (k
+ 1) by
NAT_1: 12;
(k
+ 1)
<= (
len b) by
A16,
XXREAL_0: 2;
then
A19: (k
+ 1)
in (
Seg (
len b)) by
A18;
1
<= j & j
<= (
len b) by
A16,
A18,
XXREAL_0: 2;
then
A20: j
in (
Seg (
len b));
(k
+ 1)
< j by
A15,
NAT_1: 16,
XXREAL_0: 2;
then
A21: ((b
. (k
+ 1)),(b
. j))
are_coprime by
A1,
A19,
A20;
(m
. ((k
+ 1)
+ 1))
= ((m
. (k
+ 1))
* (b
. (k
+ 1))) by
A5;
hence ((m
. ((k
+ 1)
+ 1)),(b
. j))
are_coprime by
A21,
A17,
INT_2: 26;
end;
end;
end;
for k be
Nat holds
P[k] from
NAT_1:sch 2(
A2,
A3);
hence thesis;
end;
Lm17: for b,m be
FinSequence of
INT st (
len b)
= (
len m) & (m
. 1)
= 1 holds for k be
Element of
NAT st 1
<= k & k
<= ((
len b)
- 1) & (for i be
Nat st 1
<= i & i
<= k holds (m
. (i
+ 1))
= ((m
. i)
* (b
. i))) holds for j be
Nat st 1
<= j & j
<= k holds ((m
. (k
+ 1))
mod (b
. j))
=
0
proof
let b,m be
FinSequence of
INT ;
assume (
len b)
= (
len m);
assume
A1: (m
. 1)
= 1;
defpred
P[
Nat] means (1
<= $1 & $1
<= ((
len b)
- 1) & (for i be
Nat st 1
<= i & i
<= $1 holds (m
. (i
+ 1))
= ((m
. i)
* (b
. i)))) implies for j be
Nat st 1
<= j & j
<= $1 holds ((m
. ($1
+ 1))
mod (b
. j))
=
0 ;
reconsider I0 =
0 as
Element of
NAT ;
A2:
P[
0 ];
A3: for k be
Nat st
P[k] holds
P[(k
+ 1)]
proof
let k be
Nat;
assume
A4:
P[k];
assume
A5: 1
<= (k
+ 1) & (k
+ 1)
<= ((
len b)
- 1) & (for i be
Nat st 1
<= i & i
<= (k
+ 1) holds (m
. (i
+ 1))
= ((m
. i)
* (b
. i)));
A6: k
<= (k
+ 1) by
NAT_1: 12;
per cases ;
suppose
A7: k
=
0 ;
A8: (m
. ((k
+ 1)
+ 1))
= ((m
. 1)
* (b
. 1)) by
A5,
A7
.= (b
. 1) by
A1;
for j be
Nat st 1
<= j & j
<= (k
+ 1) holds ((m
. ((k
+ 1)
+ 1))
mod (b
. j))
=
0
proof
let j be
Nat;
assume 1
<= j & j
<= (k
+ 1);
then j
= 1 by
A7,
XXREAL_0: 1;
hence ((m
. ((k
+ 1)
+ 1))
mod (b
. j))
=
0 by
A8,
INT_1: 50;
end;
hence thesis;
end;
suppose k
<>
0 ;
A9:
now
let i be
Nat;
assume 1
<= i & i
<= k;
then 1
<= i & i
<= (k
+ 1) by
NAT_1: 12;
hence (m
. (i
+ 1))
= ((m
. i)
* (b
. i)) by
A5;
end;
thus for j be
Nat st 1
<= j & j
<= (k
+ 1) holds ((m
. ((k
+ 1)
+ 1))
mod (b
. j))
=
0
proof
let j be
Nat;
assume
A10: 1
<= j & j
<= (k
+ 1);
reconsider bj = (b
. j) as
Element of
INT by
INT_1:def 2;
per cases ;
suppose
A11: j
= (k
+ 1);
thus ((m
. ((k
+ 1)
+ 1))
mod (b
. j))
= (((m
. (k
+ 1))
* (b
. (k
+ 1)))
mod (b
. j)) by
A5
.= ((((m
. (k
+ 1))
mod (b
. j))
* ((b
. (k
+ 1))
mod (b
. j)))
mod (b
. j)) by
NAT_D: 67
.= ((((m
. (k
+ 1))
mod (b
. j))
*
0 qua
Nat)
mod (b
. j)) by
A11,
INT_1: 50
.=
0 by
INT_1: 73;
end;
suppose j
<> (k
+ 1);
then j
< (k
+ 1) by
A10,
XXREAL_0: 1;
then
A12: j
<= k by
NAT_1: 13;
thus ((m
. ((k
+ 1)
+ 1))
mod (b
. j))
= (((m
. (k
+ 1))
* (b
. (k
+ 1)))
mod (b
. j)) by
A5
.= ((((m
. (k
+ 1))
mod (b
. j))
* ((b
. (k
+ 1))
mod (b
. j)))
mod (b
. j)) by
NAT_D: 67
.= ((
0
* ((b
. (k
+ 1))
mod (b
. j)))
mod (b
. j)) by
A12,
A9,
A10,
A4,
A5,
A6,
XXREAL_0: 2
.=
0 by
INT_1: 73;
end;
end;
end;
end;
for k be
Nat holds
P[k] from
NAT_1:sch 2(
A2,
A3);
hence thesis;
end;
theorem ::
NTALGO_1:11
Th11: for nlist be non
empty
FinSequence of
[:
INT ,
INT :], a,b be
FinSequence of
INT st (
len a)
= (
len b) & (
len a)
= (
len nlist) & (for i be
Nat st i
in (
Seg (
len nlist)) holds (b
. i)
<>
0 ) & (for i be
Nat st i
in (
Seg (
len nlist)) holds ((nlist
. i)
`1 )
= (a
. i) & ((nlist
. i)
`2 )
= (b
. i)) & (for i,j be
Nat st i
in (
Seg (
len nlist)) & j
in (
Seg (
len nlist)) & i
<> j holds ((b
. i),(b
. j))
are_coprime ) holds for i be
Nat st i
in (
Seg (
len nlist)) holds ((
ALGO_CRT nlist)
mod (b
. i))
= ((a
. i)
mod (b
. i))
proof
defpred
P[
Nat] means for nlist be non
empty
FinSequence of
[:
INT ,
INT :], a,b be
FinSequence of
INT st (
len nlist)
= $1 & (
len a)
= (
len b) & (
len a)
= (
len nlist) & (for i be
Nat st i
in (
Seg (
len nlist)) holds (b
. i)
<>
0 ) & (for i be
Nat st i
in (
Seg (
len nlist)) holds ((nlist
. i)
`1 )
= (a
. i) & ((nlist
. i)
`2 )
= (b
. i)) & (for i,j be
Nat st i
in (
Seg (
len nlist)) & j
in (
Seg (
len nlist)) & i
<> j holds ((b
. i),(b
. j))
are_coprime ) holds (for i be
Nat st i
in (
Seg (
len nlist)) holds ((
ALGO_CRT nlist)
mod (b
. i))
= ((a
. i)
mod (b
. i)));
A1:
P[
0 ];
A2: for n be
Nat st
P[n] holds
P[(n
+ 1)]
proof
let n be
Nat;
assume
A3:
P[n];
let nlist be non
empty
FinSequence of
[:
INT ,
INT :], a,b be
FinSequence of
INT ;
assume
A4: (
len nlist)
= (n
+ 1) & (
len a)
= (
len b) & (
len a)
= (
len nlist) & (for i be
Nat st i
in (
Seg (
len nlist)) holds (b
. i)
<>
0 ) & (for i be
Nat st i
in (
Seg (
len nlist)) holds ((nlist
. i)
`1 )
= (a
. i) & ((nlist
. i)
`2 )
= (b
. i)) & (for i,j be
Nat st i
in (
Seg (
len nlist)) & j
in (
Seg (
len nlist)) & i
<> j holds ((b
. i),(b
. j))
are_coprime );
per cases ;
suppose
A5: n
=
0 ;
A6: 1
in (
Seg (
len nlist)) by
A5,
A4;
A7: (
ALGO_CRT nlist)
= ((nlist
. 1)
`1 ) by
Def4,
A5,
A4
.= (a
. 1) by
A4,
A6;
thus for i be
Nat st i
in (
Seg (
len nlist)) holds ((
ALGO_CRT nlist)
mod (b
. i))
= ((a
. i)
mod (b
. i)) by
A7,
A5,
A4,
FINSEQ_1: 2,
TARSKI:def 1;
end;
suppose
A8: n
<>
0 ;
then
A9: 1
<= n by
NAT_1: 14;
A10: (
len nlist)
<> 1 by
A4,
A8;
reconsider nlist1 = (nlist
| n) as
FinSequence of
[:
INT ,
INT :];
reconsider a1 = (a
| n) as
FinSequence of
INT ;
reconsider b1 = (b
| n) as
FinSequence of
INT ;
A11: n
<= (n
+ 1) by
NAT_1: 11;
then
A12: (
len a1)
= n by
A4,
FINSEQ_1: 59;
A13: (
len nlist1)
= n by
A11,
A4,
FINSEQ_1: 59;
reconsider nlist1 as non
empty
FinSequence of
[:
INT ,
INT :] by
A8;
A14: (
dom nlist1)
= (
Seg (
len nlist1)) by
FINSEQ_1:def 3
.= (
Seg n) by
A11,
A4,
FINSEQ_1: 59;
n
in
NAT by
ORDINAL1:def 12;
then
A15: (
len nlist1)
= n by
A14,
FINSEQ_1:def 3;
then
A16: (
Seg (
len nlist1))
c= (
Seg (
len nlist)) by
A11,
A4,
FINSEQ_1: 5;
A17: (
len nlist1)
= n & (
len a1)
= (
len b1) & (
len a1)
= (
len nlist1) by
A12,
A11,
A4,
FINSEQ_1: 59;
A18: for i be
Nat st i
in (
Seg (
len nlist1)) holds (b1
. i)
<>
0
proof
let i be
Nat;
assume
A19: i
in (
Seg (
len nlist1));
then (b1
. i)
= (b
. i) by
A15,
FUNCT_1: 49;
hence thesis by
A16,
A19,
A4;
end;
A20: for i be
Nat st i
in (
Seg (
len nlist1)) holds ((nlist1
. i)
`1 )
= (a1
. i) & ((nlist1
. i)
`2 )
= (b1
. i)
proof
let i be
Nat;
assume
A21: i
in (
Seg (
len nlist1));
A22: ((nlist1
. i)
`1 )
= ((nlist
. i)
`1 ) by
A21,
A15,
FUNCT_1: 49
.= (a
. i) by
A21,
A16,
A4
.= (a1
. i) by
A21,
A15,
FUNCT_1: 49;
((nlist1
. i)
`2 )
= ((nlist
. i)
`2 ) by
A21,
A15,
FUNCT_1: 49
.= (b
. i) by
A21,
A16,
A4
.= (b1
. i) by
A21,
A15,
FUNCT_1: 49;
hence thesis by
A22;
end;
A23: for i,j be
Nat st i
in (
Seg (
len nlist1)) & j
in (
Seg (
len nlist1)) & i
<> j holds ((b1
. i),(b1
. j))
are_coprime
proof
let i,j be
Nat;
assume
A24: i
in (
Seg (
len nlist1)) & j
in (
Seg (
len nlist1)) & i
<> j;
A25: (b
. i)
= (b1
. i) by
A24,
A15,
FUNCT_1: 49;
(b
. j)
= (b1
. j) by
A24,
A15,
FUNCT_1: 49;
hence thesis by
A25,
A24,
A16,
A4;
end;
A26: for i be
Nat st i
in (
Seg (
len nlist1)) holds ((
ALGO_CRT nlist1)
mod (b
. i))
= ((a
. i)
mod (b
. i))
proof
let i be
Nat;
assume
A27: i
in (
Seg (
len nlist1));
then (a1
. i)
= (a
. i) & (b1
. i)
= (b
. i) by
A15,
FUNCT_1: 49;
hence ((
ALGO_CRT nlist1)
mod (b
. i))
= ((a
. i)
mod (b
. i)) by
A3,
A17,
A20,
A23,
A18,
A27;
end;
consider m,l,prodc,prodi be
FinSequence of
INT , M0,M be
Element of
INT such that
A28: (
len m)
= (
len nlist) & (
len l)
= (
len nlist) & (
len prodc)
= ((
len nlist)
- 1) & (
len prodi)
= ((
len nlist)
- 1) & (m
. 1)
= 1 & (for i be
Nat st 1
<= i & i
<= ((
len m)
- 1) holds ex d,x,y be
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) & (l
. 1)
= ((nlist
. 1)
`1 ) & (for i be
Nat st 1
<= i & i
<= ((
len m)
- 1) holds ex u,u0,u1 be
Element of
INT st u0
= ((nlist
. (i
+ 1))
`1 ) & u1
= ((nlist
. (i
+ 1))
`2 ) & u
= (((u0
- (l
. i))
* (prodi
. i))
mod u1) & (l
. (i
+ 1))
= ((l
. i)
+ (u
* (prodc
. i)))) & (
ALGO_CRT nlist)
= ((l
. (
len m))
mod M) by
A10,
Def4;
A29: (1
+ 1)
<= (n
+ 1) by
A9,
XREAL_1: 6;
reconsider lb1 = ((
len b)
- 1) as
Nat by
A4;
A30: 1
<= lb1 & lb1
<= lb1 by
A4,
A8,
NAT_1: 14;
A31: for i be
Nat st 1
<= i & i
<= lb1 holds (m
. (i
+ 1))
= ((m
. i)
* (b
. i))
proof
let i be
Nat;
assume
A32: 1
<= i & i
<= lb1;
then
A33: ex d,x,y be
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 by
A4,
A28;
i
in (
Seg (
len nlist1)) by
A32,
A13,
A4;
hence (m
. (i
+ 1))
= ((m
. i)
* (b
. i)) by
A33,
A4,
A16;
end;
A34: ((m
. (
len nlist)),(b
. (
len nlist)))
are_coprime by
A4,
Lm16,
A29,
A28,
A30,
A31;
reconsider nn = n as
Element of
NAT by
ORDINAL1:def 12;
set l1 = (l
| nn), m1 = (m
| nn);
A35: n
<= (n
+ 1) by
NAT_1: 11;
then
A36: (
len l1)
= n by
A4,
A28,
FINSEQ_1: 59;
A37: (
dom m1)
= (
Seg (
len m1)) by
FINSEQ_1:def 3
.= (
Seg n) by
A4,
A28,
A35,
FINSEQ_1: 59;
A38: (
len m1)
= n by
A37,
FINSEQ_1:def 3;
(1
- 1)
<= (n
- 1) by
A9,
XREAL_1: 9;
then
reconsider nn1 = (n
- 1) as
Element of
NAT by
INT_1: 3;
reconsider prodi1 = (prodi
| nn1) as
FinSequence of
INT ;
reconsider prodc1 = (prodc
| nn1) as
FinSequence of
INT ;
A39: (n
- 1)
<= (n
-
0 ) by
XREAL_1: 10;
then
A40: (
len prodi1)
= nn1 by
A4,
A28,
FINSEQ_1: 59;
A41: (
len prodc1)
= nn1 by
A39,
A4,
A28,
FINSEQ_1: 59;
A42: 1
in (
Seg n) by
A9;
A43: (l1
. 1)
= (l
. 1) by
A42,
FUNCT_1: 49
.= ((nlist1
. 1)
`1 ) by
A42,
A28,
FUNCT_1: 49;
A44: (n
- 1)
<= (n
-
0 ) by
XREAL_1: 10;
A45:
now
let i be
Nat;
assume
A46: 1
<= i & i
<= ((
len m1)
- 1);
then
A47: 1
<= i & i
<= (
len m1) by
A38,
A44,
XXREAL_0: 2;
then i
in (
Seg (
len m1));
hence (m1
. i)
= (m
. i) by
A38,
FUNCT_1: 49;
i
in (
Seg (
len l1)) by
A47,
A36,
A38;
hence (l1
. i)
= (l
. i) by
A36,
FUNCT_1: 49;
i
in (
Seg (
len prodi1)) by
A46,
A38,
A40;
hence (prodi1
. i)
= (prodi
. i) by
A40,
FUNCT_1: 49;
i
in (
Seg (
len prodc1)) by
A46,
A38,
A41;
hence (prodc1
. i)
= (prodc
. i) by
A41,
FUNCT_1: 49;
end;
(
len m1)
in (
Seg (
len nlist1)) by
A13,
A38,
FINSEQ_1: 3;
then
A48: (
len m1)
in (
Seg (
len nlist)) by
A16;
A49: (nlist1
. (
len m1))
= (nlist
. (
len m1)) by
A13,
A38,
FINSEQ_1: 3,
FUNCT_1: 49;
(
len m1)
in (
dom nlist) by
A48,
FINSEQ_1:def 3;
then (nlist1
. (
len m1))
in
[:
INT ,
INT :] by
A49,
FINSEQ_2: 11;
then
reconsider M01 = ((nlist1
. (
len m1))
`2 ) as
Element of
INT by
MCART_1: 10;
reconsider M1 = ((prodc1
. ((
len m1)
- 1))
* M01) as
Element of
INT by
INT_1:def 2;
A50: (
len m1)
= (
len nlist1) & (
len l1)
= (
len nlist1) & (
len prodc1)
= ((
len nlist1)
- 1) & (
len prodi1)
= ((
len nlist1)
- 1) & (m1
. 1)
= 1 by
A35,
A4,
A38,
A36,
A41,
A40,
A28,
A42,
FINSEQ_1: 59,
FUNCT_1: 49;
A51: for i be
Nat st 1
<= i & i
<= ((
len m1)
- 1) holds ex d,x,y be
Element of
INT st x
= ((nlist1
. i)
`2 ) & (m1
. (i
+ 1))
= ((m1
. i)
* x) & y
= (m1
. (i
+ 1)) & d
= ((nlist1
. (i
+ 1))
`2 ) & (prodi1
. i)
= (
ALGO_INVERSE (y,d)) & (prodc1
. i)
= y
proof
let i be
Nat;
assume
A52: 1
<= i & i
<= ((
len m1)
- 1);
then
A53: (m1
. i)
= (m
. i) by
A45;
A54: (prodi1
. i)
= (prodi
. i) by
A45,
A52;
A55: (prodc1
. i)
= (prodc
. i) by
A45,
A52;
A56: 1
<= (i
+ 1) by
NAT_1: 12;
(i
+ 1)
<= (((
len m1)
- 1)
+ 1) by
A52,
XREAL_1: 6;
then
A57: (i
+ 1)
in (
Seg (
len m1)) by
A56;
then
A58: (m1
. (i
+ 1))
= (m
. (i
+ 1)) by
A38,
FUNCT_1: 49;
A59: 1
<= i & i
<= (
len m1) by
A52,
A38,
A44,
XXREAL_0: 2;
A60: 1
<= i & i
<= ((
len m)
- 1) by
A28,
A4,
A52,
A38,
A44,
XXREAL_0: 2;
i
in (
Seg (
len nlist1)) by
A38,
A13,
A59;
then
A61: (nlist1
. i)
= (nlist
. i) by
A15,
FUNCT_1: 49;
(nlist1
. (i
+ 1))
= (nlist
. (i
+ 1)) by
A38,
A57,
FUNCT_1: 49;
hence thesis by
A53,
A54,
A55,
A58,
A60,
A61,
A28;
end;
A62: for i be
Nat st 1
<= i & i
<= ((
len m1)
- 1) holds ex u,u0,u1 be
Element of
INT st u0
= ((nlist1
. (i
+ 1))
`1 ) & u1
= ((nlist1
. (i
+ 1))
`2 ) & u
= (((u0
- (l1
. i))
* (prodi1
. i))
mod u1) & (l1
. (i
+ 1))
= ((l1
. i)
+ (u
* (prodc1
. i)))
proof
let i be
Nat;
assume
A63: 1
<= i & i
<= ((
len m1)
- 1);
then
A64: (l1
. i)
= (l
. i) by
A45;
A65: (prodi1
. i)
= (prodi
. i) by
A45,
A63;
A66: (prodc1
. i)
= (prodc
. i) by
A45,
A63;
A67: 1
<= (i
+ 1) by
NAT_1: 12;
(i
+ 1)
<= (((
len m1)
- 1)
+ 1) by
A63,
XREAL_1: 6;
then
A68: (i
+ 1)
in (
Seg (
len m1)) by
A67;
then
A69: (l1
. (i
+ 1))
= (l
. (i
+ 1)) by
A38,
FUNCT_1: 49;
A70: 1
<= i & i
<= ((
len m)
- 1) by
A28,
A4,
A63,
A38,
A44,
XXREAL_0: 2;
(nlist1
. (i
+ 1))
= (nlist
. (i
+ 1)) by
A38,
A68,
FUNCT_1: 49;
hence thesis by
A64,
A65,
A66,
A69,
A70,
A28;
end;
reconsider s = ((l1
. (
len m1))
mod M1) as
Element of
INT by
INT_1:def 2;
A71: 1
<= ((
len m)
- 1) by
A28,
A4,
A8,
NAT_1: 14;
reconsider lm1 = ((
len m)
- 1) as
Element of
NAT by
A28;
A72: 1
<= lm1 & lm1
<= ((
len m)
- 1) by
A28,
A4,
A8,
NAT_1: 14;
consider d,x,y be
Element of
INT such that
A73: x
= ((nlist
. lm1)
`2 ) & (m
. (lm1
+ 1))
= ((m
. lm1)
* x) & y
= (m
. (lm1
+ 1)) & d
= ((nlist
. (lm1
+ 1))
`2 ) & (prodi
. lm1)
= (
ALGO_INVERSE (y,d)) & (prodc
. lm1)
= y by
A28,
A4,
A9;
consider u,u0,u1 be
Element of
INT such that
A74: u0
= ((nlist
. (lm1
+ 1))
`1 ) & u1
= ((nlist
. (lm1
+ 1))
`2 ) & u
= (((u0
- (l
. lm1))
* (prodi
. lm1))
mod u1) & (l
. (lm1
+ 1))
= ((l
. lm1)
+ (u
* (prodc
. lm1))) by
A72,
A28;
A75: (
len nlist)
in (
Seg (
len nlist)) by
FINSEQ_1: 3;
A76: M0
= (b
. (
len nlist)) by
A28,
A4,
A75;
then
A77: M0
<>
0 by
A75,
A4;
then
consider r be
Element of
INT such that
A79: u
= (((u0
- (l
. ((
len m)
- 1)))
* (
ALGO_INVERSE (y,M0)))
+ (r
* M0)) by
Lm14,
A28,
A73,
A74;
A80: y
<>
0 by
A73,
A28,
A4,
Lm15,
A30,
A31;
now
per cases ;
suppose
A81: (
len nlist1)
= 1;
A82: (
ALGO_CRT nlist1)
= ((nlist1
. 1)
`1 ) by
A81,
Def4
.= ((nlist
. 1)
`1 ) by
A42,
FUNCT_1: 49
.= (l
. ((
len m)
- 1)) by
A81,
A4,
A28,
A14,
FINSEQ_1:def 3;
A83: (
ALGO_CRT nlist)
= (((l
. ((
len m)
- 1))
+ (u
* y))
mod M) by
A73,
A74,
A28;
reconsider p =
0 as
Element of
INT by
INT_1:def 2;
A84: (
ALGO_CRT nlist1)
= ((l
. ((
len m)
- 1))
+ (p
* y)) by
A82;
reconsider uy = (u
* y) as
Element of
INT by
INT_1:def 2;
reconsider llm1 = (l
. ((
len m)
- 1)) as
Element of
INT by
INT_1:def 2;
reconsider ly = (llm1
+ uy) as
Element of
INT by
INT_1:def 2;
consider t be
Element of
INT such that
A85: (
ALGO_CRT nlist)
= (ly
+ (t
* M)) by
Lm14,
A83,
A77,
A80,
XCMPLX_1: 6,
A28,
A73;
reconsider qr = (r
+ t) as
Element of
INT by
INT_1:def 2;
(
ALGO_CRT nlist)
= ((((
ALGO_CRT nlist1)
- (((llm1
* (
ALGO_INVERSE (y,M0)))
* y)
+ (p
* y)))
+ ((qr
* M0)
* y))
+ ((u0
* (
ALGO_INVERSE (y,M0)))
* y)) by
A28,
A73,
A79,
A85,
A82;
hence ex p,qr be
Element of
INT st (
ALGO_CRT nlist)
= ((((
ALGO_CRT nlist1)
- ((((l
. ((
len m)
- 1))
* (
ALGO_INVERSE (y,M0)))
* y)
+ (p
* y)))
+ ((qr
* M0)
* y))
+ ((u0
* (
ALGO_INVERSE (y,M0)))
* y)) & (
ALGO_CRT nlist1)
= ((l
. ((
len m)
- 1))
+ (p
* y)) by
A84;
end;
suppose
A86: (
len nlist1)
<> 1;
then
A87: (
ALGO_CRT nlist1)
= s by
Def4,
A50,
A51,
A62,
A43
.= ((l1
. (
len m1))
mod ((prodc1
. ((
len m1)
- 1))
* M01));
A88: (l1
. (
len l1))
= (l
. (
len l1)) by
A8,
A36,
FINSEQ_1: 3,
FUNCT_1: 49
.= (l
. ((
len m)
- 1)) by
A28,
A4,
A35,
FINSEQ_1: 59;
2
<= (
len nlist1) by
A86,
NAT_1: 23;
then (2
- 1)
<= ((
len m1)
- 1) by
A38,
A17,
XREAL_1: 9;
then
A89: 1
<= nn1 & nn1
<= ((
len m1)
- 1) by
A37,
FINSEQ_1:def 3;
A90: M01
= ((nlist
. (
len m1))
`2 ) by
A13,
A38,
FINSEQ_1: 3,
FUNCT_1: 49
.= ((nlist
. ((
len m)
- 1))
`2 ) by
A28,
A4,
A37,
FINSEQ_1:def 3;
consider d1,x1,y1 be
Element of
INT such that
A91: x1
= ((nlist1
. nn1)
`2 ) & (m1
. (nn1
+ 1))
= ((m1
. nn1)
* x1) & y1
= (m1
. (nn1
+ 1)) & d1
= ((nlist1
. (nn1
+ 1))
`2 ) & (prodi1
. nn1)
= (
ALGO_INVERSE (y1,d1)) & (prodc1
. nn1)
= y1 by
A51,
A89;
A92: (
len m1)
= ((
len m)
- 1) by
A28,
A4,
A37,
FINSEQ_1:def 3;
then
A93: lm1
in (
Seg (
len m1)) by
A71;
A94: (
ALGO_CRT nlist1)
= ((l
. ((
len m)
- 1))
mod (y1
* M01)) by
A91,
A87,
A92,
A88,
A4,
A28,
A35,
FINSEQ_1: 59;
A96: y
= (y1
* x) by
A91,
A28,
A4,
A38,
A93,
A73,
FUNCT_1: 49;
then
A97: (y1
* M01)
<>
0 by
A28,
A4,
Lm15,
A30,
A31,
A90,
A73;
consider p be
Element of
INT such that
A98: (
ALGO_CRT nlist1)
= ((l
. ((
len m)
- 1))
+ (p
* (y1
* M01))) by
A94,
Lm14,
A80,
A90,
A73,
A96;
(
ALGO_CRT nlist)
= (((l
. ((
len m)
- 1))
+ (u
* (y1
* x)))
mod ((prodc
. ((
len m)
- 1))
* M0)) by
A91,
A28,
A4,
A38,
A93,
A73,
A74,
FUNCT_1: 49
.= (((l
. ((
len m)
- 1))
+ (u
* (y1
* x)))
mod ((y1
* x)
* M0)) by
A91,
A28,
A4,
A38,
A93,
A73,
FUNCT_1: 49;
then
consider q be
Element of
INT such that
A100: (
ALGO_CRT nlist)
= (((l
. ((
len m)
- 1))
+ (u
* (y1
* x)))
+ (q
* ((y1
* x)
* M0))) by
Lm14,
A90,
A73,
A97,
A77,
XCMPLX_1: 6;
reconsider qr = (r
+ q) as
Element of
INT by
INT_1:def 2;
(((
ALGO_CRT nlist1)
- (p
* (y1
* M01)))
+ (u
* (y1
* x)))
= (((
ALGO_CRT nlist1)
- (p
* (y1
* x)))
+ (u
* (y1
* x))) by
A90,
A73
.= ((((
ALGO_CRT nlist1)
- ((((l
. ((
len m)
- 1))
* (
ALGO_INVERSE (y,M0)))
* y)
+ (p
* y)))
+ ((r
* M0)
* y))
+ ((u0
* (
ALGO_INVERSE (y,M0)))
* y)) by
A96,
A79;
then (
ALGO_CRT nlist)
= (((((
ALGO_CRT nlist1)
- ((((l
. ((
len m)
- 1))
* (
ALGO_INVERSE (y,M0)))
* y)
+ (p
* y)))
+ ((r
* M0)
* y))
+ ((u0
* (
ALGO_INVERSE (y,M0)))
* y))
+ (q
* (y
* M0))) by
A91,
A28,
A4,
A38,
A93,
A73,
A100,
A98,
FUNCT_1: 49
.= ((((
ALGO_CRT nlist1)
- ((((l
. ((
len m)
- 1))
* (
ALGO_INVERSE (y,M0)))
* y)
+ (p
* y)))
+ ((qr
* M0)
* y))
+ ((u0
* (
ALGO_INVERSE (y,M0)))
* y));
hence ex p,qr be
Element of
INT st (
ALGO_CRT nlist)
= ((((
ALGO_CRT nlist1)
- ((((l
. ((
len m)
- 1))
* (
ALGO_INVERSE (y,M0)))
* y)
+ (p
* y)))
+ ((qr
* M0)
* y))
+ ((u0
* (
ALGO_INVERSE (y,M0)))
* y)) & (
ALGO_CRT nlist1)
= ((l
. ((
len m)
- 1))
+ (p
* y)) by
A98,
A96,
A90,
A73;
end;
end;
then
consider p,qr be
Element of
INT such that
A101: (
ALGO_CRT nlist)
= ((((
ALGO_CRT nlist1)
- ((((l
. ((
len m)
- 1))
* (
ALGO_INVERSE (y,M0)))
* y)
+ (p
* y)))
+ ((qr
* M0)
* y))
+ ((u0
* (
ALGO_INVERSE (y,M0)))
* y)) & (
ALGO_CRT nlist1)
= ((l
. ((
len m)
- 1))
+ (p
* y));
reconsider y0 = (y
mod M0) as
Element of
INT by
INT_1:def 2;
(y0
gcd M0)
= 1 by
INT_2:def 3,
A77,
Th10,
A73,
A28,
A76,
A34;
then
A102: ((
ALGO_EXGCD (M0,y0))
`3_3 )
= 1 by
Th6;
A103: (((((l
. ((
len m)
- 1))
* (
ALGO_INVERSE (y,M0)))
* y)
+ (p
* y))
mod M0)
= (((((l
. ((
len m)
- 1))
* ((
ALGO_INVERSE (y,M0))
* y))
mod M0)
+ ((p
* y)
mod M0))
mod M0) by
NAT_D: 66
.= ((((((l
. ((
len m)
- 1))
mod M0)
* (((
ALGO_INVERSE (y,M0))
* y)
mod M0))
mod M0)
+ ((p
* y)
mod M0))
mod M0) by
NAT_D: 67
.= ((((((l
. ((
len m)
- 1))
mod M0)
* (1
mod M0))
mod M0)
+ ((p
* y)
mod M0))
mod M0) by
A102,
Th7
.= (((((l
. ((
len m)
- 1))
* 1)
mod M0)
+ ((p
* y)
mod M0))
mod M0) by
NAT_D: 67
.= ((
ALGO_CRT nlist1)
mod M0) by
A101,
NAT_D: 66;
thus for i be
Nat st i
in (
Seg (
len nlist)) holds ((
ALGO_CRT nlist)
mod (b
. i))
= ((a
. i)
mod (b
. i))
proof
let i be
Nat;
assume
A104: i
in (
Seg (
len nlist));
then
A105: 1
<= i & i
<= (
len nlist) by
FINSEQ_1: 1;
per cases ;
suppose
A106: i
= (
len nlist);
A107: (b
. i)
<>
0 by
A4,
A104;
reconsider I0 =
0 as
Element of
INT by
INT_1:def 2;
reconsider K1y = ((((l
. ((
len m)
- 1))
* (
ALGO_INVERSE (y,M0)))
* y)
+ (p
* y)) as
Element of
INT by
INT_1:def 2;
reconsider K2y = ((qr
* y)
* M0) as
Element of
INT by
INT_1:def 2;
reconsider K3y = (u0
* ((
ALGO_INVERSE (y,M0))
* y)) as
Element of
INT by
INT_1:def 2;
reconsider K4y = (K2y
+ K3y) as
Element of
INT by
INT_1:def 2;
A108: (K2y
mod (b
. i))
= ((((qr
* y)
mod M0)
* (M0
mod M0))
mod M0) by
A76,
A106,
NAT_D: 67
.= ((((qr
* y)
mod M0)
* I0)
mod M0) by
INT_1: 50
.= (I0
mod (b
. i)) by
A106,
A28,
A4,
A75;
A109: (K4y
mod (b
. i))
= (((I0
mod (b
. i))
+ (K3y
mod (b
. i)))
mod (b
. i)) by
A108,
NAT_D: 66
.= ((I0
+ K3y)
mod (b
. i)) by
NAT_D: 66
.= (((u0
mod (b
. i))
* (((
ALGO_INVERSE (y,M0))
* y)
mod (b
. i)))
mod (b
. i)) by
NAT_D: 67
.= (((u0
mod (b
. i))
* (1
mod (b
. i)))
mod (b
. i)) by
A102,
Th7,
A106,
A76
.= ((u0
* 1)
mod (b
. i)) by
NAT_D: 67
.= ((a
. i)
mod (b
. i)) by
A106,
A75,
A28,
A4,
A74;
A110: (((
ALGO_CRT nlist)
+ K1y)
mod (b
. i))
= ((((
ALGO_CRT nlist)
mod (b
. i))
+ ((
ALGO_CRT nlist1)
mod (b
. i)))
mod (b
. i)) by
A103,
A106,
A76,
NAT_D: 66
.= (((
ALGO_CRT nlist)
+ (
ALGO_CRT nlist1))
mod (b
. i)) by
NAT_D: 66;
A111: (((
ALGO_CRT nlist1)
+ K4y)
mod (b
. i))
= ((((
ALGO_CRT nlist1)
mod (b
. i))
+ (K4y
mod (b
. i)))
mod (b
. i)) by
NAT_D: 66
.= (((
ALGO_CRT nlist1)
+ (a
. i))
mod (b
. i)) by
A109,
NAT_D: 66;
reconsider LL = (((
ALGO_CRT nlist1)
+ (a
. i))
mod (b
. i)) as
Element of
INT by
INT_1:def 2;
reconsider LL1 = ((
ALGO_CRT nlist)
+ (
ALGO_CRT nlist1)) as
Element of
INT by
INT_1:def 2;
reconsider bi = (b
. i) as
Element of
INT by
INT_1:def 2;
consider r be
Element of
INT such that
A112: LL
= (LL1
+ (r
* bi)) by
Lm14,
A107,
A110,
A111,
A101;
reconsider LL2 = ((
ALGO_CRT nlist1)
+ (a
. i)) as
Element of
INT by
INT_1:def 2;
consider s be
Element of
INT such that
A113: LL
= (LL2
+ (s
* bi)) by
Lm14,
A107;
reconsider LL3 = (s
- r) as
Element of
INT by
INT_1:def 2;
A114: ((LL3
* (b
. i))
mod (b
. i))
= (((LL3
mod (b
. i))
* ((b
. i)
mod (b
. i)))
mod (b
. i)) by
NAT_D: 67
.= (((LL3
mod (b
. i))
* I0)
mod (b
. i)) by
INT_1: 50
.= (I0
mod (b
. i));
thus ((
ALGO_CRT nlist)
mod (b
. i))
= (((a
. i)
+ ((s
- r)
* (b
. i)))
mod (b
. i)) by
A112,
A113
.= ((((a
. i)
mod (b
. i))
+ (I0
mod (b
. i)))
mod (b
. i)) by
A114,
NAT_D: 66
.= (((a
. i)
+ I0)
mod (b
. i)) by
NAT_D: 66
.= ((a
. i)
mod (b
. i));
end;
suppose i
<> (
len nlist);
then i
< (
len nlist) by
A105,
XXREAL_0: 1;
then (i
+ 1)
<= (
len nlist) by
NAT_1: 13;
then
A115: ((i
+ 1)
- 1)
<= ((
len nlist)
- 1) by
XREAL_1: 9;
then
A116: 1
<= i & i
<= (
len nlist1) by
A35,
A4,
A104,
FINSEQ_1: 1,
FINSEQ_1: 59;
A117: i
in (
Seg (
len nlist1)) by
A115,
A4,
A17,
A105;
reconsider K1 = (((l
. ((
len m)
- 1))
* (
ALGO_INVERSE (y,M0)))
+ p) as
Element of
INT by
INT_1:def 2;
reconsider K2 = ((qr
* M0)
+ (u0
* (
ALGO_INVERSE (y,M0)))) as
Element of
INT by
INT_1:def 2;
reconsider I0 =
0 as
Element of
INT by
INT_1:def 2;
A118: (y
mod (b
. i))
=
0 by
A17,
A73,
Lm17,
A30,
A31,
A4,
A28,
A116;
reconsider K1y = (K1
* y) as
Element of
INT by
INT_1:def 2;
reconsider K2y = (K2
* y) as
Element of
INT by
INT_1:def 2;
A119: ((K1
* y)
mod (b
. i))
= (((K1
mod (b
. i))
* (y
mod (b
. i)))
mod (b
. i)) by
NAT_D: 67
.= (
0
mod (b
. i)) by
A118;
A120: ((K2
* y)
mod (b
. i))
= (((K2
mod (b
. i))
* (y
mod (b
. i)))
mod (b
. i)) by
NAT_D: 67
.= (
0
mod (b
. i)) by
A118;
A121: (((
ALGO_CRT nlist)
+ K1y)
mod (b
. i))
= ((((
ALGO_CRT nlist)
mod (b
. i))
+ (K1y
mod (b
. i)))
mod (b
. i)) by
NAT_D: 66
.= (((
ALGO_CRT nlist)
+ I0)
mod (b
. i)) by
A119,
NAT_D: 66
.= ((
ALGO_CRT nlist)
mod (b
. i));
(((
ALGO_CRT nlist1)
+ K2y)
mod (b
. i))
= ((((
ALGO_CRT nlist1)
mod (b
. i))
+ (K2y
mod (b
. i)))
mod (b
. i)) by
NAT_D: 66
.= (((
ALGO_CRT nlist1)
+ I0)
mod (b
. i)) by
A120,
NAT_D: 66
.= ((
ALGO_CRT nlist1)
mod (b
. i));
hence ((
ALGO_CRT nlist)
mod (b
. i))
= ((a
. i)
mod (b
. i)) by
A117,
A101,
A121,
A26;
end;
end;
end;
end;
for n be
Nat holds
P[n] from
NAT_1:sch 2(
A1,
A2);
hence thesis;
end;
Lm18: for x,y,a,b be
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
let x,y,a,b be
Integer;
assume
A1: (x
mod a)
= (y
mod a) & (x
mod b)
= (y
mod b) & (a,b)
are_coprime ;
set g1 = (x
mod a);
set g2 = (x
mod b);
per cases ;
suppose
A2: (a
* b)
=
0 ;
hence (x
mod (a
* b))
=
0 by
INT_1:def 10
.= (y
mod (a
* b)) by
A2,
INT_1:def 10;
end;
suppose (a
* b)
<>
0 ;
then
A3: a
<>
0 & b
<>
0 ;
then
A4: y
= (((y
div a)
* a)
+ (y
mod a)) by
INT_1: 59;
A5: x
= (((x
div b)
* b)
+ (x
mod b)) by
A3,
INT_1: 59;
(x
- y)
= ((((x
div a)
* a)
+ (x
mod a))
- (((y
div a)
* a)
+ (y
mod a))) by
A3,
A4,
INT_1: 59
.= (((x
div a)
- (y
div a))
* a) by
A1;
then
A6: (x,y)
are_congruent_mod a;
(x
- y)
= ((((x
div b)
* b)
+ (x
mod b))
- (((y
div b)
* b)
+ (y
mod b))) by
A3,
A5,
INT_1: 59
.= (((x
div b)
- (y
div b))
* b) by
A1;
then (x,y)
are_congruent_mod b;
then (x,y)
are_congruent_mod (a
* b) by
A1,
A6,
INT_6: 21;
then
consider p be
Integer such that
A7: (x
- y)
= ((a
* b)
* p);
reconsider I0 =
0 as
Element of
INT by
INT_1:def 2;
thus (x
mod (a
* b))
= ((y
+ ((a
* b)
* p))
mod (a
* b)) by
A7
.= (((y
mod (a
* b))
+ (((a
* b)
* p)
mod (a
* b)))
mod (a
* b)) by
NAT_D: 66
.= (((y
mod (a
* b))
+ ((((a
* b)
mod (a
* b))
* (p
mod (a
* b)))
mod (a
* b)))
mod (a
* b)) by
NAT_D: 67
.= (((y
mod (a
* b))
+ ((I0
* (p
mod (a
* b)))
mod (a
* b)))
mod (a
* b)) by
INT_1: 50
.= ((y
+ I0)
mod (a
* b)) by
NAT_D: 66
.= (y
mod (a
* b));
end;
end;
theorem ::
NTALGO_1:12
Th12: for x,y be
Integer, b,m be non
empty
FinSequence of
INT st 2
<= (
len b) & (for i,j be
Nat st i
in (
Seg (
len b)) & j
in (
Seg (
len b)) & i
<> j holds ((b
. i),(b
. j))
are_coprime ) & (for i be
Nat st i
in (
Seg (
len b)) holds (x
mod (b
. i))
= (y
mod (b
. i))) & (m
. 1)
= 1 holds for k be
Element of
NAT st 1
<= k & k
<= (
len b) & (for i be
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
let x,y be
Integer, b,m be non
empty
FinSequence of
INT ;
assume
A1: 2
<= (
len b);
assume
A2: for i,j be
Nat st i
in (
Seg (
len b)) & j
in (
Seg (
len b)) & i
<> j holds ((b
. i),(b
. j))
are_coprime ;
assume
A3: for i be
Nat st i
in (
Seg (
len b)) holds (x
mod (b
. i))
= (y
mod (b
. i));
assume
A4: (m
. 1)
= 1;
defpred
P[
Nat] means (1
<= $1 & $1
<= (
len b) & (for i be
Nat st 1
<= i & i
<= $1 holds (m
. (i
+ 1))
= ((m
. i)
* (b
. i)))) implies (x
mod (m
. ($1
+ 1)))
= (y
mod (m
. ($1
+ 1)));
reconsider I0 =
0 as
Element of
NAT ;
A5:
P[
0 ];
A6: for k be
Nat st
P[k] holds
P[(k
+ 1)]
proof
let k be
Nat;
assume
A7:
P[k];
assume
A8: 1
<= (k
+ 1) & (k
+ 1)
<= (
len b) & (for i be
Nat st 1
<= i & i
<= (k
+ 1) holds (m
. (i
+ 1))
= ((m
. i)
* (b
. i)));
A9: k
<= (k
+ 1) by
NAT_1: 12;
per cases ;
suppose k
=
0 ;
then
A11: (m
. ((k
+ 1)
+ 1))
= ((m
. 1)
* (b
. 1)) by
A8
.= (b
. 1) by
A4;
1
<= 1 & 1
<= (
len b) by
NAT_1: 14;
then 1
in (
Seg (
len b));
hence (x
mod (m
. ((k
+ 1)
+ 1)))
= (y
mod (m
. ((k
+ 1)
+ 1))) by
A11,
A3;
end;
suppose
A13: k
<>
0 ;
((k
+ 1)
- 1)
<= ((
len b)
- 1) by
A8,
XREAL_1: 9;
then
A14: 1
<= k & k
<= ((
len b)
- 1) by
A13,
NAT_1: 14;
A15:
now
let i be
Nat;
assume 1
<= i & i
<= k;
then 1
<= i & i
<= (k
+ 1) by
NAT_1: 12;
hence (m
. (i
+ 1))
= ((m
. i)
* (b
. i)) by
A8;
end;
A16: (m
. ((k
+ 1)
+ 1))
= ((m
. (k
+ 1))
* (b
. (k
+ 1))) by
A8;
(k
+ 1)
in (
Seg (
len b)) by
A8;
then
A17: (x
mod (b
. (k
+ 1)))
= (y
mod (b
. (k
+ 1))) by
A3;
((m
. (k
+ 1)),(b
. (k
+ 1)))
are_coprime by
Lm16,
A15,
A14,
A1,
A2,
A4,
A8;
hence (x
mod (m
. ((k
+ 1)
+ 1)))
= (y
mod (m
. ((k
+ 1)
+ 1))) by
A16,
A17,
A7,
A13,
A8,
A9,
A15,
Lm18,
NAT_1: 14,
XXREAL_0: 2;
end;
end;
for k be
Nat holds
P[k] from
NAT_1:sch 2(
A5,
A6);
hence thesis;
end;
theorem ::
NTALGO_1:13
Th13: for b be
complex-valued
FinSequence st (
len b)
= 1 holds (
Product b)
= (b
. 1)
proof
let b be
complex-valued
FinSequence;
assume (
len b)
= 1;
then b
=
<*(b
. 1)*> by
FINSEQ_1: 40;
hence (
Product b)
= (b
. 1) by
RVSUM_1: 95;
end;
theorem ::
NTALGO_1:14
Th14: for b be
FinSequence of
INT holds ex m be non
empty
FinSequence of
INT st (
len m)
= ((
len b)
+ 1) & (m
. 1)
= 1 & (for i be
Nat st 1
<= i & i
<= (
len b) holds (m
. (i
+ 1))
= ((m
. i)
* (b
. i))) & (
Product b)
= (m
. ((
len b)
+ 1))
proof
defpred
P[
Nat] means for b be
FinSequence of
INT st (
len b)
= $1 holds ex m be non
empty
FinSequence of
INT st ((
len m)
= ((
len b)
+ 1) & (m
. 1)
= 1 & (for i be
Nat st 1
<= i & i
<= (
len b) holds (m
. (i
+ 1))
= ((m
. i)
* (b
. i)))) & (
Product b)
= (m
. ((
len b)
+ 1));
A1:
P[
0 ]
proof
let b be
FinSequence of
INT ;
assume
A2: (
len b)
=
0 ;
A3: 1
in
INT by
INT_1:def 2;
(
rng
<*1 qua
Integer*>)
=
{1 qua
Integer} by
FINSEQ_1: 39;
then (
rng
<*1 qua
Integer*>)
c=
INT by
A3,
ZFMISC_1: 31;
then
reconsider m =
<*1 qua
Integer*> as non
empty
FinSequence of
INT by
FINSEQ_1:def 4;
A4: (
len m)
= ((
len b)
+ 1) by
A2,
FINSEQ_1: 40;
A5: (m
. 1)
= 1 by
FINSEQ_1: 40;
A6: for i be
Nat st 1
<= i & i
<= (
len b) holds (m
. (i
+ 1))
= ((m
. i)
* (b
. i)) by
A2;
b
= (
<*>
REAL ) by
A2;
hence thesis by
A4,
A5,
A6,
RVSUM_1: 94;
end;
A7: for k be
Nat st
P[k] holds
P[(k
+ 1)]
proof
let k be
Nat;
assume
A8:
P[k];
let b be
FinSequence of
INT ;
assume
A9: (
len b)
= (k
+ 1);
set b1 = (b
| k);
A10: (
len b1)
= k by
A9,
FINSEQ_1: 59,
NAT_1: 12;
then
consider m1 be non
empty
FinSequence of
INT such that
A11: (((
len b1)
+ 1)
= (
len m1) & (m1
. 1)
= 1 & (for i be
Nat st 1
<= i & i
<= (
len b1) holds (m1
. (i
+ 1))
= ((m1
. i)
* (b1
. i)))) & (
Product b1)
= (m1
. ((
len b1)
+ 1)) by
A8;
set m = (m1
^
<*((
Product b1)
* (b
. (
len b)))*>);
A12: ((
Product b1)
* (b
. (
len b)))
in
INT by
A11,
INT_1:def 2;
A13: (
rng
<*((
Product b1)
* (b
. (
len b)))*>)
=
{((
Product b1)
* (b
. (
len b)))} by
FINSEQ_1: 39;
then
A14: (
rng
<*((
Product b1)
* (b
. (
len b)))*>)
c=
INT by
A12,
ZFMISC_1: 31;
A15: (
len m)
= ((
len m1)
+ (
len
<*((
Product b1)
* (b
. (
len b)))*>)) by
FINSEQ_1: 22
.= (((
len b1)
+ 1)
+ 1) by
A11,
FINSEQ_1: 40
.= ((
len b)
+ 1) by
A9,
FINSEQ_1: 59,
NAT_1: 12;
A16: (
rng m)
= ((
rng m1)
\/
{((
Product b1)
* (b
. (
len b)))}) by
A13,
FINSEQ_1: 31;
(
rng m1)
c=
INT by
FINSEQ_1:def 4;
then (
rng m)
c=
INT by
A13,
A16,
A14,
XBOOLE_1: 8;
then
reconsider m as non
empty
FinSequence of
INT by
FINSEQ_1:def 4;
A17: (
len m1)
= (k
+ 1) by
A9,
FINSEQ_1: 59,
NAT_1: 12,
A11;
1
<= 1 & 1
<= (k
+ 1) by
NAT_1: 12;
then 1
in (
dom m1) by
A17,
FINSEQ_3: 25;
then
A18: (m
. 1)
= 1 by
A11,
FINSEQ_1:def 7;
A19: for i be
Nat st 1
<= i & i
<= (
len b) holds (m
. (i
+ 1))
= ((m
. i)
* (b
. i))
proof
let i be
Nat;
assume
A20: 1
<= i & i
<= (
len b);
per cases ;
suppose
A21: i
= (
len b);
((
len b1)
+ 1)
in (
Seg (
len m1)) by
A10,
A17,
FINSEQ_1: 4;
then ((
len b1)
+ 1)
in (
dom m1) by
FINSEQ_1:def 3;
then
A22: (m1
. ((
len b1)
+ 1))
= (m
. ((
len b1)
+ 1)) by
FINSEQ_1:def 7
.= (m
. i) by
A9,
A21,
FINSEQ_1: 59,
NAT_1: 12;
1
in (
Seg 1);
then
A23: 1
in (
dom
<*((
Product b1)
* (b
. (
len b)))*>) by
FINSEQ_1: 38;
thus (m
. (i
+ 1))
= (
<*((
Product b1)
* (b
. (
len b)))*>
. 1) by
A21,
A9,
A17,
A23,
FINSEQ_1:def 7
.= ((m
. i)
* (b
. i)) by
A22,
A21,
A11,
FINSEQ_1: 40;
end;
suppose i
<> (
len b);
then
A24: i
< (
len b) by
A20,
XXREAL_0: 1;
then
A25: 1
<= i & i
<= (
len b1) by
A10,
A9,
A20,
NAT_1: 13;
then
A26: (m1
. (i
+ 1))
= ((m1
. i)
* (b1
. i)) by
A11;
i
in (
Seg (
len m1)) by
A20,
A9,
A17;
then
A27: i
in (
dom m1) by
FINSEQ_1:def 3;
A28: (i
+ 1)
<= (
len m1) by
A9,
A17,
A24,
NAT_1: 13;
1
<= (i
+ 1) by
NAT_1: 12;
then (i
+ 1)
in (
Seg (
len m1)) by
A28;
then
A29: (i
+ 1)
in (
dom m1) by
FINSEQ_1:def 3;
i
in (
Seg k) by
A25,
A10;
then
A30: (b
. i)
= (b1
. i) by
FUNCT_1: 49;
A31: (m
. i)
= (m1
. i) by
A27,
FINSEQ_1:def 7;
thus (m
. (i
+ 1))
= ((m
. i)
* (b
. i)) by
A26,
A29,
A30,
A31,
FINSEQ_1:def 7;
end;
end;
(b
| (k
+ 1))
= (b1
^
<*(b
. (
len b))*>) by
A9,
INT_6: 5;
then
A32: b
= (b1
^
<*(b
. (
len b))*>) by
A9,
FINSEQ_1: 58;
(
len b)
in (
Seg (
len m1)) by
A9,
A17,
FINSEQ_1: 4;
then
A33: (
len b)
in (
dom m1) by
FINSEQ_1:def 3;
A34: 1
<= (
len b) & (
len b)
<= (
len b) by
A9,
NAT_1: 12;
(
Product b)
= ((m1
. ((
len b1)
+ 1))
* (b
. (
len b))) by
A11,
A32,
RVSUM_1: 96
.= ((m1
. (
len b))
* (b
. (
len b))) by
A9,
FINSEQ_1: 59,
NAT_1: 12
.= ((m
. (
len b))
* (b
. (
len b))) by
A33,
FINSEQ_1:def 7
.= (m
. ((
len b)
+ 1)) by
A19,
A34;
hence thesis by
A15,
A18,
A19;
end;
for k be
Nat holds
P[k] from
NAT_1:sch 2(
A1,
A7);
hence thesis;
end;
theorem ::
NTALGO_1:15
for nlist be non
empty
FinSequence of
[:
INT ,
INT :], a,b be non
empty
FinSequence of
INT , x,y be
Element of
INT st (
len a)
= (
len b) & (
len a)
= (
len nlist) & (for i be
Nat st i
in (
Seg (
len nlist)) holds (b
. i)
<>
0 ) & (for i be
Nat st i
in (
Seg (
len nlist)) holds ((nlist
. i)
`1 )
= (a
. i) & ((nlist
. i)
`2 )
= (b
. i)) & (for i,j be
Nat st i
in (
Seg (
len nlist)) & j
in (
Seg (
len nlist)) & i
<> j holds ((b
. i),(b
. j))
are_coprime ) & (for i be
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
let nlist be non
empty
FinSequence of
[:
INT ,
INT :], a,b be non
empty
FinSequence of
INT , x,y be
Element of
INT ;
assume
A1: (
len a)
= (
len b) & (
len a)
= (
len nlist);
assume
A2: for i be
Nat st i
in (
Seg (
len nlist)) holds (b
. i)
<>
0 ;
assume
A3: for i be
Nat st i
in (
Seg (
len nlist)) holds ((nlist
. i)
`1 )
= (a
. i) & ((nlist
. i)
`2 )
= (b
. i);
assume
A4: for i,j be
Nat st i
in (
Seg (
len nlist)) & j
in (
Seg (
len nlist)) & i
<> j holds ((b
. i),(b
. j))
are_coprime ;
assume
A5: for i be
Nat st i
in (
Seg (
len nlist)) holds (x
mod (b
. i))
= ((a
. i)
mod (b
. i));
assume
A6: y
= (
Product b);
A7: for i be
Nat st i
in (
Seg (
len nlist)) holds ((
ALGO_CRT nlist)
mod (b
. i))
= (x
mod (b
. i))
proof
let i be
Nat;
assume
A8: i
in (
Seg (
len nlist));
hence ((
ALGO_CRT nlist)
mod (b
. i))
= ((a
. i)
mod (b
. i)) by
Th11,
A1,
A2,
A3,
A4
.= (x
mod (b
. i)) by
A5,
A8;
end;
per cases ;
suppose
A9: (
len nlist)
= 1;
then
A10: 1
in (
Seg (
len nlist));
thus ((
ALGO_CRT nlist)
mod y)
= ((
ALGO_CRT nlist)
mod (b
. 1)) by
A9,
A1,
Th13,
A6
.= (x
mod (b
. 1)) by
A7,
A10
.= (x
mod y) by
A9,
A1,
Th13,
A6;
end;
suppose
A11: (
len nlist)
<> 1;
then
A12: 2
<= (
len nlist) by
NAT_1: 23;
A13: 2
<= (
len b) by
A1,
A11,
NAT_1: 23;
consider m be non
empty
FinSequence of
INT such that
A14: (
len m)
= ((
len b)
+ 1) & (m
. 1)
= 1 & (for i be
Nat st 1
<= i & i
<= (
len b) holds (m
. (i
+ 1))
= ((m
. i)
* (b
. i))) & (
Product b)
= (m
. ((
len b)
+ 1)) by
Th14;
1
<= (
len b) & (
len b)
<= (
len b) by
A13,
XXREAL_0: 2;
hence ((
ALGO_CRT nlist)
mod y)
= (x
mod y) by
A6,
A14,
Th12,
A1,
A4,
A7,
A12;
end;
end;