:: NTALGO_1 semantic presentation
begin
theorem LMTh3: :: NTALGO_1:1
for x, p being Integer holds (x mod p) mod p = x mod p
proof
let x, p be Integer; ::_thesis: (x mod p) mod p = x mod p
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_4:12 ;
hence (x mod p) mod p = x mod p ; ::_thesis: verum
end;
LM6: for a being Element of NAT holds a gcd 0 = a
proof
let a be Element of NAT ; ::_thesis: a gcd 0 = a
0 = 0 * a ;
then P2: a divides 0 by INT_1:def_3;
for m being Integer st m divides a & m divides 0 holds
m divides a ;
hence a gcd 0 = a by P2, INT_2:def_2; ::_thesis: verum
end;
LM1: for a, b being Element of INT ex A, B being sequence of NAT st
( A . 0 = abs a & B . 0 = abs b & ( for i being Element of NAT holds
( A . (i + 1) = B . i & B . (i + 1) = (A . i) mod (B . i) ) ) )
proof
let a, b be Element of INT ; ::_thesis: ex A, B being sequence of NAT st
( A . 0 = abs a & B . 0 = abs b & ( for i being Element of NAT holds
( A . (i + 1) = B . i & B . (i + 1) = (A . i) mod (B . i) ) ) )
defpred S1[ Nat, Nat, Nat, Nat, Nat] means ( $4 = $3 & $5 = $2 mod $3 );
Q1: for n, x, y being Element of NAT ex x1, y1 being Element of NAT st S1[n,x,y,x1,y1] ;
consider A, B being Function of NAT,NAT such that
P2: ( A . 0 = abs a & B . 0 = abs b & ( for n being Element of NAT holds S1[n,A . n,B . n,A . (n + 1),B . (n + 1)] ) ) from RECDEF_2:sch_3(Q1);
take A ; ::_thesis: ex B being sequence of NAT st
( A . 0 = abs a & B . 0 = abs b & ( for i being Element of NAT holds
( A . (i + 1) = B . i & B . (i + 1) = (A . i) mod (B . i) ) ) )
take B ; ::_thesis: ( A . 0 = abs a & B . 0 = abs b & ( for i being Element of NAT holds
( A . (i + 1) = B . i & B . (i + 1) = (A . i) mod (B . i) ) ) )
thus ( A . 0 = abs a & B . 0 = abs b & ( for i being Element of NAT holds
( A . (i + 1) = B . i & B . (i + 1) = (A . i) mod (B . i) ) ) ) by P2; ::_thesis: verum
end;
LM2: for a, b being Element of INT
for A1, B1, A2, B2 being sequence of NAT st A1 . 0 = abs a & B1 . 0 = abs b & ( for i being Element of NAT holds
( A1 . (i + 1) = B1 . i & B1 . (i + 1) = (A1 . i) mod (B1 . i) ) ) & A2 . 0 = abs a & B2 . 0 = abs b & ( for i being Element of NAT holds
( A2 . (i + 1) = B2 . i & B2 . (i + 1) = (A2 . i) mod (B2 . i) ) ) holds
( A1 = A2 & B1 = B2 )
proof
let a, b be Element of INT ; ::_thesis: for A1, B1, A2, B2 being sequence of NAT st A1 . 0 = abs a & B1 . 0 = abs b & ( for i being Element of NAT holds
( A1 . (i + 1) = B1 . i & B1 . (i + 1) = (A1 . i) mod (B1 . i) ) ) & A2 . 0 = abs a & B2 . 0 = abs b & ( for i being Element of NAT holds
( A2 . (i + 1) = B2 . i & B2 . (i + 1) = (A2 . i) mod (B2 . i) ) ) holds
( A1 = A2 & B1 = B2 )
let A1, B1, A2, B2 be sequence of NAT; ::_thesis: ( A1 . 0 = abs a & B1 . 0 = abs b & ( for i being Element of NAT holds
( A1 . (i + 1) = B1 . i & B1 . (i + 1) = (A1 . i) mod (B1 . i) ) ) & A2 . 0 = abs a & B2 . 0 = abs b & ( for i being Element of NAT holds
( A2 . (i + 1) = B2 . i & B2 . (i + 1) = (A2 . i) mod (B2 . i) ) ) implies ( A1 = A2 & B1 = B2 ) )
assume P1: ( A1 . 0 = abs a & B1 . 0 = abs b & ( for i being Element of NAT holds
( A1 . (i + 1) = B1 . i & B1 . (i + 1) = (A1 . i) mod (B1 . i) ) ) ) ; ::_thesis: ( not A2 . 0 = abs a or not B2 . 0 = abs b or ex i being Element of NAT st
( A2 . (i + 1) = B2 . i implies not B2 . (i + 1) = (A2 . i) mod (B2 . i) ) or ( A1 = A2 & B1 = B2 ) )
assume P2: ( A2 . 0 = abs a & B2 . 0 = abs b & ( for i being Element of NAT holds
( A2 . (i + 1) = B2 . i & B2 . (i + 1) = (A2 . i) mod (B2 . i) ) ) ) ; ::_thesis: ( A1 = A2 & B1 = B2 )
defpred S1[ Nat] means ( A1 . $1 = A2 . $1 & B1 . $1 = B2 . $1 );
P0: S1[ 0 ] by P1, P2;
PN: for n being Element of NAT st S1[n] holds
S1[n + 1]
proof
let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] )
assume PN1: S1[n] ; ::_thesis: S1[n + 1]
PN2: A1 . (n + 1) = B1 . n by P1
.= A2 . (n + 1) by P2, PN1 ;
B1 . (n + 1) = (A1 . n) mod (B1 . n) by P1
.= B2 . (n + 1) by P2, PN1 ;
hence S1[n + 1] by PN2; ::_thesis: verum
end;
for n being Element of NAT holds S1[n] from NAT_1:sch_1(P0, PN);
hence ( A1 = A2 & B1 = B2 ) by FUNCT_2:def_8; ::_thesis: verum
end;
definition
let a, b be Element of INT ;
func ALGO_GCD (a,b) -> Element of NAT means :defALGOGCD: :: NTALGO_1:def 1
ex A, B being sequence of NAT st
( A . 0 = abs a & B . 0 = abs b & ( for i being Element of NAT holds
( A . (i + 1) = B . i & B . (i + 1) = (A . i) mod (B . i) ) ) & it = A . (min* { i where i is Element of NAT : B . i = 0 } ) );
existence
ex b1 being Element of NAT ex A, B being sequence of NAT st
( A . 0 = abs a & B . 0 = abs b & ( for i being Element of NAT holds
( A . (i + 1) = B . i & B . (i + 1) = (A . i) mod (B . i) ) ) & b1 = A . (min* { i where i is Element of NAT : B . i = 0 } ) )
proof
consider A, B being sequence of NAT such that
P1: ( A . 0 = abs a & B . 0 = abs b & ( for i being Element of NAT holds
( A . (i + 1) = B . i & B . (i + 1) = (A . i) mod (B . i) ) ) ) by LM1;
set m = A . (min* { i where i is Element of NAT : B . i = 0 } );
A . (min* { i where i is Element of NAT : B . i = 0 } ) is Element of NAT ;
hence ex b1 being Element of NAT ex A, B being sequence of NAT st
( A . 0 = abs a & B . 0 = abs b & ( for i being Element of NAT holds
( A . (i + 1) = B . i & B . (i + 1) = (A . i) mod (B . i) ) ) & b1 = A . (min* { i where i is Element of NAT : B . i = 0 } ) ) by P1; ::_thesis: verum
end;
uniqueness
for b1, b2 being Element of NAT st ex A, B being sequence of NAT st
( A . 0 = abs a & B . 0 = abs b & ( for i being Element of NAT holds
( A . (i + 1) = B . i & B . (i + 1) = (A . i) mod (B . i) ) ) & b1 = A . (min* { i where i is Element of NAT : B . i = 0 } ) ) & ex A, B being sequence of NAT st
( A . 0 = abs a & B . 0 = abs b & ( for i being Element of NAT holds
( A . (i + 1) = B . i & B . (i + 1) = (A . i) mod (B . i) ) ) & b2 = A . (min* { i where i is Element of NAT : B . i = 0 } ) ) holds
b1 = b2
proof
let m1, m2 be Element of NAT ; ::_thesis: ( ex A, B being sequence of NAT st
( A . 0 = abs a & B . 0 = abs b & ( for i being Element of NAT holds
( A . (i + 1) = B . i & B . (i + 1) = (A . i) mod (B . i) ) ) & m1 = A . (min* { i where i is Element of NAT : B . i = 0 } ) ) & ex A, B being sequence of NAT st
( A . 0 = abs a & B . 0 = abs b & ( for i being Element of NAT holds
( A . (i + 1) = B . i & B . (i + 1) = (A . i) mod (B . i) ) ) & m2 = A . (min* { i where i is Element of NAT : B . i = 0 } ) ) implies m1 = m2 )
assume ex A1, B1 being sequence of NAT st
( A1 . 0 = abs a & B1 . 0 = abs b & ( for i being Element of NAT holds
( A1 . (i + 1) = B1 . i & B1 . (i + 1) = (A1 . i) mod (B1 . i) ) ) & m1 = A1 . (min* { i where i is Element of NAT : B1 . i = 0 } ) ) ; ::_thesis: ( for A, B being sequence of NAT holds
( not A . 0 = abs a or not B . 0 = abs b or ex i being Element of NAT st
( A . (i + 1) = B . i implies not B . (i + 1) = (A . i) mod (B . i) ) or not m2 = A . (min* { i where i is Element of NAT : B . i = 0 } ) ) or m1 = m2 )
then consider A1, B1 being sequence of NAT such that
P1: ( A1 . 0 = abs a & B1 . 0 = abs b & ( for i being Element of NAT holds
( A1 . (i + 1) = B1 . i & B1 . (i + 1) = (A1 . i) mod (B1 . i) ) ) & m1 = A1 . (min* { i where i is Element of NAT : B1 . i = 0 } ) ) ;
assume ex A2, B2 being sequence of NAT st
( A2 . 0 = abs a & B2 . 0 = abs b & ( for i being Element of NAT holds
( A2 . (i + 1) = B2 . i & B2 . (i + 1) = (A2 . i) mod (B2 . i) ) ) & m2 = A2 . (min* { i where i is Element of NAT : B2 . i = 0 } ) ) ; ::_thesis: m1 = m2
then consider A2, B2 being sequence of NAT such that
P2: ( A2 . 0 = abs a & B2 . 0 = abs b & ( for i being Element of NAT holds
( A2 . (i + 1) = B2 . i & B2 . (i + 1) = (A2 . i) mod (B2 . i) ) ) & m2 = A2 . (min* { i where i is Element of NAT : B2 . i = 0 } ) ) ;
( A1 = A2 & B1 = B2 ) by LM2, P1, P2;
hence m1 = m2 by P1, P2; ::_thesis: verum
end;
end;
:: deftheorem defALGOGCD defines ALGO_GCD NTALGO_1:def_1_:_
for a, b being Element of INT
for b3 being Element of NAT holds
( b3 = ALGO_GCD (a,b) iff ex A, B being sequence of NAT st
( A . 0 = abs a & B . 0 = abs b & ( for i being Element of NAT holds
( A . (i + 1) = B . i & B . (i + 1) = (A . i) mod (B . i) ) ) & b3 = A . (min* { i where i is Element of NAT : B . i = 0 } ) ) );
LM3: for a, b being Element of INT
for A, B being sequence of NAT st A . 0 = abs a & B . 0 = abs b & ( for i being Element of NAT holds
( A . (i + 1) = B . i & B . (i + 1) = (A . i) mod (B . i) ) ) holds
for i being Element of NAT st B . i <> 0 holds
(A . i) gcd (B . i) = (A . (i + 1)) gcd (B . (i + 1))
proof
let a, b be Element of INT ; ::_thesis: for A, B being sequence of NAT st A . 0 = abs a & B . 0 = abs b & ( for i being Element of NAT holds
( A . (i + 1) = B . i & B . (i + 1) = (A . i) mod (B . i) ) ) holds
for i being Element of NAT st B . i <> 0 holds
(A . i) gcd (B . i) = (A . (i + 1)) gcd (B . (i + 1))
let A, B be sequence of NAT; ::_thesis: ( A . 0 = abs a & B . 0 = abs b & ( for i being Element of NAT holds
( A . (i + 1) = B . i & B . (i + 1) = (A . i) mod (B . i) ) ) implies for i being Element of NAT st B . i <> 0 holds
(A . i) gcd (B . i) = (A . (i + 1)) gcd (B . (i + 1)) )
assume AS: ( A . 0 = abs a & B . 0 = abs b & ( for i being Element of NAT holds
( A . (i + 1) = B . i & B . (i + 1) = (A . i) mod (B . i) ) ) ) ; ::_thesis: for i being Element of NAT st B . i <> 0 holds
(A . i) gcd (B . i) = (A . (i + 1)) gcd (B . (i + 1))
let i be Element of NAT ; ::_thesis: ( B . i <> 0 implies (A . i) gcd (B . i) = (A . (i + 1)) gcd (B . (i + 1)) )
assume AS1: B . i <> 0 ; ::_thesis: (A . i) gcd (B . i) = (A . (i + 1)) gcd (B . (i + 1))
set k = (A . i) gcd (B . i);
Q1: A . (i + 1) = B . i by AS;
Q2: B . (i + 1) = (A . i) mod (B . i) by AS;
P1: (A . i) gcd (B . i) divides A . (i + 1) by Q1, INT_2:def_2;
P2: (A . i) gcd (B . i) divides B . (i + 1)
proof
X1: B . (i + 1) = (A . i) - (((A . i) div (B . i)) * (B . i)) by INT_1:def_10, Q2, AS1;
X2: (A . i) gcd (B . i) divides A . i by INT_2:def_2;
X3: (A . i) gcd (B . i) divides B . i by INT_2:def_2;
X4: ex s being Integer st A . i = ((A . i) gcd (B . i)) * s by X2, INT_1:def_3;
ex t being Integer st B . i = ((A . i) gcd (B . i)) * t by X3, INT_1:def_3;
then consider s, t being Integer such that
X5: B . (i + 1) = (((A . i) gcd (B . i)) * s) - (((A . i) div (B . i)) * (((A . i) gcd (B . i)) * t)) by X1, X4;
B . (i + 1) = (s - (((A . i) div (B . i)) * t)) * ((A . i) gcd (B . i)) by X5;
hence (A . i) gcd (B . i) divides B . (i + 1) by INT_1:def_3; ::_thesis: verum
end;
for m being Integer st m divides A . (i + 1) & m divides B . (i + 1) holds
m divides (A . i) gcd (B . i)
proof
let m be Integer; ::_thesis: ( m divides A . (i + 1) & m divides B . (i + 1) implies m divides (A . i) gcd (B . i) )
assume P3: ( m divides A . (i + 1) & m divides B . (i + 1) ) ; ::_thesis: m divides (A . i) gcd (B . i)
then P31: m divides B . i by AS;
P32: m divides A . i
proof
B . (i + 1) = (A . i) - (((A . i) div (B . i)) * (B . i)) by INT_1:def_10, Q2, AS1;
then X1: A . i = (B . (i + 1)) + (((A . i) div (B . i)) * (B . i)) ;
X21: ex s being Integer st B . i = m * s by INT_1:def_3, P31;
X22: ex t being Integer st B . (i + 1) = m * t by INT_1:def_3, P3;
consider s, t being Integer such that
X4: A . i = (m * s) + (((A . i) div (B . i)) * (m * t)) by X1, X21, X22;
A . i = m * (s + (((A . i) div (B . i)) * t)) by X4;
hence m divides A . i by INT_1:def_3; ::_thesis: verum
end;
thus m divides (A . i) gcd (B . i) by P31, P32, INT_2:def_2; ::_thesis: verum
end;
hence (A . (i + 1)) gcd (B . (i + 1)) = (A . i) gcd (B . i) by P1, P2, INT_2:def_2; ::_thesis: verum
end;
LM4: for a, b being Element of INT
for A, B being sequence of NAT st A . 0 = abs a & B . 0 = abs b & ( for i being Element of NAT holds
( A . (i + 1) = B . i & B . (i + 1) = (A . i) mod (B . i) ) ) holds
for i being Element of NAT st B . i <> 0 holds
(A . 0) gcd (B . 0) = (A . i) gcd (B . i)
proof
let a, b be Element of INT ; ::_thesis: for A, B being sequence of NAT st A . 0 = abs a & B . 0 = abs b & ( for i being Element of NAT holds
( A . (i + 1) = B . i & B . (i + 1) = (A . i) mod (B . i) ) ) holds
for i being Element of NAT st B . i <> 0 holds
(A . 0) gcd (B . 0) = (A . i) gcd (B . i)
let A, B be sequence of NAT; ::_thesis: ( A . 0 = abs a & B . 0 = abs b & ( for i being Element of NAT holds
( A . (i + 1) = B . i & B . (i + 1) = (A . i) mod (B . i) ) ) implies for i being Element of NAT st B . i <> 0 holds
(A . 0) gcd (B . 0) = (A . i) gcd (B . i) )
assume AS1: ( A . 0 = abs a & B . 0 = abs b & ( for i being Element of NAT holds
( A . (i + 1) = B . i & B . (i + 1) = (A . i) mod (B . i) ) ) ) ; ::_thesis: for i being Element of NAT st B . i <> 0 holds
(A . 0) gcd (B . 0) = (A . i) gcd (B . i)
defpred S1[ Nat] means ( B . $1 <> 0 implies (A . 0) gcd (B . 0) = (A . $1) gcd (B . $1) );
P0: S1[ 0 ] ;
PN: for i being Element of NAT st S1[i] holds
S1[i + 1]
proof
let i be Element of NAT ; ::_thesis: ( S1[i] implies S1[i + 1] )
assume PN1: S1[i] ; ::_thesis: S1[i + 1]
( B . (i + 1) <> 0 implies (A . 0) gcd (B . 0) = (A . (i + 1)) gcd (B . (i + 1)) )
proof
assume PN2: B . (i + 1) <> 0 ; ::_thesis: (A . 0) gcd (B . 0) = (A . (i + 1)) gcd (B . (i + 1))
B . i <> 0
proof
assume PN4: B . i = 0 ; ::_thesis: contradiction
B . (i + 1) = (A . i) mod (B . i) by AS1;
hence contradiction by PN2, PN4, INT_1:def_10; ::_thesis: verum
end;
hence (A . 0) gcd (B . 0) = (A . (i + 1)) gcd (B . (i + 1)) by PN1, AS1, LM3; ::_thesis: verum
end;
hence S1[i + 1] ; ::_thesis: verum
end;
for i being Element of NAT holds S1[i] from NAT_1:sch_1(P0, PN);
hence for i being Element of NAT st B . i <> 0 holds
(A . 0) gcd (B . 0) = (A . i) gcd (B . i) ; ::_thesis: verum
end;
LM5: for a, b being Element of INT
for A, B being sequence of NAT st A . 0 = abs a & B . 0 = abs b & ( for i being Element of NAT holds
( A . (i + 1) = B . i & B . (i + 1) = (A . i) mod (B . i) ) ) holds
{ i where i is Element of NAT : B . i = 0 } is non empty Subset of NAT
proof
let a, b be Element of INT ; ::_thesis: for A, B being sequence of NAT st A . 0 = abs a & B . 0 = abs b & ( for i being Element of NAT holds
( A . (i + 1) = B . i & B . (i + 1) = (A . i) mod (B . i) ) ) holds
{ i where i is Element of NAT : B . i = 0 } is non empty Subset of NAT
let A, B be sequence of NAT; ::_thesis: ( A . 0 = abs a & B . 0 = abs b & ( for i being Element of NAT holds
( A . (i + 1) = B . i & B . (i + 1) = (A . i) mod (B . i) ) ) implies { i where i is Element of NAT : B . i = 0 } is non empty Subset of NAT )
assume AS1: ( A . 0 = abs a & B . 0 = abs b & ( for i being Element of NAT holds
( A . (i + 1) = B . i & B . (i + 1) = (A . i) mod (B . i) ) ) ) ; ::_thesis: { i where i is Element of NAT : B . i = 0 } is non empty Subset of NAT
P1: for x being set st x in { i where i is Element of NAT : B . i = 0 } holds
x in NAT
proof
let x be set ; ::_thesis: ( x in { i where i is Element of NAT : B . i = 0 } implies x in NAT )
assume x in { i where i is Element of NAT : B . i = 0 } ; ::_thesis: x in NAT
then ex i being Element of NAT st
( x = i & B . i = 0 ) ;
hence x in NAT ; ::_thesis: verum
end;
ex m0 being Element of NAT st B . m0 = 0
proof
assume A2: for m0 being Element of NAT holds not B . m0 = 0 ; ::_thesis: contradiction
A3: for i being Element of NAT holds B . (i + 1) <= (B . i) - 1
proof
let i be Element of NAT ; ::_thesis: B . (i + 1) <= (B . i) - 1
A31: B . i <> 0 by A2;
B . (i + 1) = (A . i) mod (B . i) by AS1;
then B . (i + 1) < B . i by A31, INT_1:58;
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 ; ::_thesis: verum
end;
defpred S1[ Nat] means B . $1 <= (B . 0) - $1;
P0: S1[ 0 ] ;
P1: for i being Element of NAT st S1[i] holds
S1[i + 1]
proof
let i be Element of NAT ; ::_thesis: ( S1[i] implies S1[i + 1] )
assume P11: S1[i] ; ::_thesis: S1[i + 1]
P12: B . (i + 1) <= (B . i) - 1 by A3;
(B . i) - 1 <= ((B . 0) - i) - 1 by P11, XREAL_1:9;
hence S1[i + 1] by XXREAL_0:2, P12; ::_thesis: verum
end;
A4: for i being Element of NAT holds S1[i] from NAT_1:sch_1(P0, P1);
B . (B . 0) <= (B . 0) - (B . 0) by A4;
hence contradiction by A2, NAT_1:14; ::_thesis: verum
end;
then consider m0 being Element of NAT such that
X1: B . m0 = 0 ;
m0 in { i where i is Element of NAT : B . i = 0 } by X1;
hence { i where i is Element of NAT : B . i = 0 } is non empty Subset of NAT by P1, TARSKI:def_3; ::_thesis: verum
end;
theorem :: NTALGO_1:2
for a, b being Element of INT holds ALGO_GCD (a,b) = a gcd b
proof
let a, b be Element of INT ; ::_thesis: ALGO_GCD (a,b) = a gcd b
consider A, B being sequence of NAT such that
P1: ( A . 0 = abs a & B . 0 = abs b & ( for i being Element of NAT holds
( A . (i + 1) = B . i & B . (i + 1) = (A . i) mod (B . i) ) ) & ALGO_GCD (a,b) = A . (min* { i where i is Element of NAT : B . i = 0 } ) ) by defALGOGCD;
set m0 = min* { i where i is Element of NAT : B . i = 0 } ;
X0: { i where i is Element of NAT : B . i = 0 } is non empty Subset of NAT by P1, LM5;
then min* { i where i is Element of NAT : B . i = 0 } in { i where i is Element of NAT : B . i = 0 } by NAT_1:def_1;
then P4: ex i being Element of NAT st
( min* { i where i is Element of NAT : B . i = 0 } = i & B . i = 0 ) ;
percases ( min* { i where i is Element of NAT : B . i = 0 } = 0 or min* { i where i is Element of NAT : B . i = 0 } <> 0 ) ;
supposeC1: min* { i where i is Element of NAT : B . i = 0 } = 0 ; ::_thesis: ALGO_GCD (a,b) = a gcd b
thus ALGO_GCD (a,b) = (A . 0) gcd (B . 0) by P4, C1, LM6, P1
.= a gcd b by INT_2:34, P1 ; ::_thesis: verum
end;
suppose min* { i where i is Element of NAT : B . i = 0 } <> 0 ; ::_thesis: ALGO_GCD (a,b) = a gcd b
then 1 <= min* { i where i is Element of NAT : B . i = 0 } by NAT_1:14;
then 1 - 1 <= (min* { i where i is Element of NAT : B . i = 0 } ) - 1 by XREAL_1:9;
then reconsider m1 = (min* { i where i is Element of NAT : B . i = 0 } ) - 1 as Element of NAT by INT_1:3;
X1: B . m1 <> 0
proof
assume B . m1 = 0 ; ::_thesis: contradiction
then X11: m1 in { i where i is Element of NAT : B . i = 0 } ;
(min* { i where i is Element of NAT : B . i = 0 } ) - 1 < (min* { i where i is Element of NAT : B . i = 0 } ) - 0 by XREAL_1:15;
hence contradiction by X11, X0, NAT_1:def_1; ::_thesis: verum
end;
then X2: (A . 0) gcd (B . 0) = (A . m1) gcd (B . m1) by P1, LM4;
P3: (A . m1) gcd (B . m1) = (A . (m1 + 1)) gcd (B . (m1 + 1)) by LM3, X1, P1;
(A . (min* { i where i is Element of NAT : B . i = 0 } )) gcd (B . (min* { i where i is Element of NAT : B . i = 0 } )) = ALGO_GCD (a,b) by P1, LM6, P4;
hence ALGO_GCD (a,b) = a gcd b by P3, INT_2:34, X2, P1; ::_thesis: verum
end;
end;
end;
begin
scheme :: NTALGO_1:sch 1
QuadChoiceRec{ F1() -> non empty set , F2() -> non empty set , F3() -> non empty set , F4() -> non empty set , F5() -> Element of F1(), F6() -> Element of F2(), F7() -> Element of F3(), F8() -> Element of F4(), P1[ set , set , set , set , set , set , set , set , set ] } :
ex f being Function of NAT,F1() ex g being Function of NAT,F2() ex h being Function of NAT,F3() ex i being Function of NAT,F4() st
( f . 0 = F5() & g . 0 = F6() & h . 0 = F7() & i . 0 = F8() & ( for n being Element of NAT holds P1[n,f . n,g . n,h . n,i . n,f . (n + 1),g . (n + 1),h . (n + 1),i . (n + 1)] ) )
provided
A1: for n being Element of NAT
for x being Element of F1()
for y being Element of F2()
for z being Element of F3()
for w being Element of F4() ex x1 being Element of F1() ex y1 being Element of F2() ex z1 being Element of F3() ex w1 being Element of F4() st P1[n,x,y,z,w,x1,y1,z1,w1]
proof
defpred S1[ set , set , set , set , set ] means P1[$1,$2 `1 ,$2 `2 ,$3 `1 ,$3 `2 ,$4 `1 ,$4 `2 ,$5 `1 ,$5 `2 ];
A2: for n being Element of NAT
for x being Element of [:F1(),F2():]
for y being Element of [:F3(),F4():] ex z being Element of [:F1(),F2():] ex w being Element of [:F3(),F4():] st S1[n,x,y,z,w]
proof
let n be Element of NAT ; ::_thesis: for x being Element of [:F1(),F2():]
for y being Element of [:F3(),F4():] ex z being Element of [:F1(),F2():] ex w being Element of [:F3(),F4():] st S1[n,x,y,z,w]
let x be Element of [:F1(),F2():]; ::_thesis: for y being Element of [:F3(),F4():] ex z being Element of [:F1(),F2():] ex w being Element of [:F3(),F4():] st S1[n,x,y,z,w]
let y be Element of [:F3(),F4():]; ::_thesis: ex z being Element of [:F1(),F2():] ex w being Element of [:F3(),F4():] st S1[n,x,y,z,w]
( x `1 is Element of F1() & x `2 is Element of F2() & y `1 is Element of F3() & y `2 is Element of F4() ) by MCART_1:10;
then consider ai being Element of F1(), bi being Element of F2(), ci being Element of F3(), di being Element of F4() such that
A3: P1[n,x `1 ,x `2 ,y `1 ,y `2 ,ai,bi,ci,di] by A1;
reconsider z = [ai,bi] as Element of [:F1(),F2():] by ZFMISC_1:87;
reconsider w = [ci,di] as Element of [:F3(),F4():] by ZFMISC_1:87;
take z ; ::_thesis: ex w being Element of [:F3(),F4():] st S1[n,x,y,z,w]
take w ; ::_thesis: S1[n,x,y,z,w]
( [ai,bi] `1 = ai & [ai,bi] `2 = bi & [ci,di] `1 = ci & [ci,di] `2 = di ) by MCART_1:7;
hence S1[n,x,y,z,w] by A3; ::_thesis: verum
end;
reconsider AB0 = [F5(),F6()] as Element of [:F1(),F2():] by ZFMISC_1:87;
reconsider CD0 = [F7(),F8()] as Element of [:F3(),F4():] by ZFMISC_1:87;
consider fg being Function of NAT,[:F1(),F2():], hi being Function of NAT,[:F3(),F4():] such that
A4: fg . 0 = AB0 and
A41: hi . 0 = CD0 and
A5: for e being Element of NAT holds S1[e,fg . e,hi . e,fg . (e + 1),hi . (e + 1)] from RECDEF_2:sch_3(A2);
take pr1 fg ; ::_thesis: ex g being Function of NAT,F2() ex h being Function of NAT,F3() ex i being Function of NAT,F4() st
( (pr1 fg) . 0 = F5() & g . 0 = F6() & h . 0 = F7() & i . 0 = F8() & ( for n being Element of NAT holds P1[n,(pr1 fg) . n,g . n,h . n,i . n,(pr1 fg) . (n + 1),g . (n + 1),h . (n + 1),i . (n + 1)] ) )
take pr2 fg ; ::_thesis: ex h being Function of NAT,F3() ex i being Function of NAT,F4() st
( (pr1 fg) . 0 = F5() & (pr2 fg) . 0 = F6() & h . 0 = F7() & i . 0 = F8() & ( for n being Element of NAT holds P1[n,(pr1 fg) . n,(pr2 fg) . n,h . n,i . n,(pr1 fg) . (n + 1),(pr2 fg) . (n + 1),h . (n + 1),i . (n + 1)] ) )
take pr1 hi ; ::_thesis: ex i being Function of NAT,F4() st
( (pr1 fg) . 0 = F5() & (pr2 fg) . 0 = F6() & (pr1 hi) . 0 = F7() & i . 0 = F8() & ( for n being Element of NAT holds P1[n,(pr1 fg) . n,(pr2 fg) . n,(pr1 hi) . n,i . n,(pr1 fg) . (n + 1),(pr2 fg) . (n + 1),(pr1 hi) . (n + 1),i . (n + 1)] ) )
take pr2 hi ; ::_thesis: ( (pr1 fg) . 0 = F5() & (pr2 fg) . 0 = F6() & (pr1 hi) . 0 = F7() & (pr2 hi) . 0 = F8() & ( for n being Element of NAT holds P1[n,(pr1 fg) . n,(pr2 fg) . n,(pr1 hi) . n,(pr2 hi) . n,(pr1 fg) . (n + 1),(pr2 fg) . (n + 1),(pr1 hi) . (n + 1),(pr2 hi) . (n + 1)] ) )
( (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 = F5() & (pr2 fg) . 0 = F6() & (pr1 hi) . 0 = F7() & (pr2 hi) . 0 = F8() ) by A4, A41, XTUPLE_0:def_2, XTUPLE_0:def_3; ::_thesis: for n being Element of NAT holds P1[n,(pr1 fg) . n,(pr2 fg) . n,(pr1 hi) . n,(pr2 hi) . n,(pr1 fg) . (n + 1),(pr2 fg) . (n + 1),(pr1 hi) . (n + 1),(pr2 hi) . (n + 1)]
let i be Element of NAT ; ::_thesis: P1[i,(pr1 fg) . i,(pr2 fg) . i,(pr1 hi) . i,(pr2 hi) . i,(pr1 fg) . (i + 1),(pr2 fg) . (i + 1),(pr1 hi) . (i + 1),(pr2 hi) . (i + 1)]
A6: ( (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;
( (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 P1[i,(pr1 fg) . i,(pr2 fg) . i,(pr1 hi) . i,(pr2 hi) . i,(pr1 fg) . (i + 1),(pr2 fg) . (i + 1),(pr1 hi) . (i + 1),(pr2 hi) . (i + 1)] by A5, A6; ::_thesis: verum
end;
EXLM1: for x, y being Element of INT ex g, w, q, t, a, b, v, u being sequence of INT st
( a . 0 = 1 & b . 0 = 0 & g . 0 = x & q . 0 = 0 & u . 0 = 0 & v . 0 = 1 & w . 0 = y & t . 0 = 0 & ( for i being Element of NAT holds
( q . (i + 1) = (g . i) div (w . i) & t . (i + 1) = (g . i) mod (w . i) & a . (i + 1) = u . i & b . (i + 1) = v . i & g . (i + 1) = w . i & u . (i + 1) = (a . i) - ((q . (i + 1)) * (u . i)) & v . (i + 1) = (b . i) - ((q . (i + 1)) * (v . i)) & w . (i + 1) = t . (i + 1) ) ) )
proof
let x, y be Element of INT ; ::_thesis: ex g, w, q, t, a, b, v, u being sequence of INT st
( a . 0 = 1 & b . 0 = 0 & g . 0 = x & q . 0 = 0 & u . 0 = 0 & v . 0 = 1 & w . 0 = y & t . 0 = 0 & ( for i being Element of NAT holds
( q . (i + 1) = (g . i) div (w . i) & t . (i + 1) = (g . i) mod (w . i) & a . (i + 1) = u . i & b . (i + 1) = v . i & g . (i + 1) = w . i & u . (i + 1) = (a . i) - ((q . (i + 1)) * (u . i)) & v . (i + 1) = (b . i) - ((q . (i + 1)) * (v . i)) & w . (i + 1) = t . (i + 1) ) ) )
defpred S1[ 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 being Element of NAT
for x, y, z, w being Element of INT ex x1, y1, z1, w1 being Element of INT st S1[n,x,y,z,w,x1,y1,z1,w1]
proof
let n be Element of NAT ; ::_thesis: for x, y, z, w being Element of INT ex x1, y1, z1, w1 being Element of INT st S1[n,x,y,z,w,x1,y1,z1,w1]
let x, y, z, w be Element of INT ; ::_thesis: ex x1, y1, z1, w1 being Element of INT st S1[n,x,y,z,w,x1,y1,z1,w1]
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 ; ::_thesis: ex y1, z1, w1 being Element of INT st S1[n,x,y,z,w,x1,y1,z1,w1]
take y1 ; ::_thesis: ex z1, w1 being Element of INT st S1[n,x,y,z,w,x1,y1,z1,w1]
take w ; ::_thesis: ex w1 being Element of INT st S1[n,x,y,z,w,x1,y1,w,w1]
take y1 ; ::_thesis: S1[n,x,y,z,w,x1,y1,w,y1]
thus S1[n,x,y,z,w,x1,y1,w,y1] ; ::_thesis: verum
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 being sequence of INT such that
P1: ( q . 0 = i0 & t . 0 = i0 & g . 0 = x & w . 0 = y & ( for i being Element of NAT holds S1[i,q . i,t . i,g . i,w . i,q . (i + 1),t . (i + 1),g . (i + 1),w . (i + 1)] ) ) from NTALGO_1:sch_1(A1);
defpred S2[ 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) );
A2: for n being Element of NAT
for x, y, z, w being Element of INT ex x1, y1, z1, w1 being Element of INT st S2[n,x,y,z,w,x1,y1,z1,w1]
proof
let n be Element of NAT ; ::_thesis: for x, y, z, w being Element of INT ex x1, y1, z1, w1 being Element of INT st S2[n,x,y,z,w,x1,y1,z1,w1]
let x, y, z, w be Element of INT ; ::_thesis: ex x1, y1, z1, w1 being Element of INT st S2[n,x,y,z,w,x1,y1,z1,w1]
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 z ; ::_thesis: ex y1, z1, w1 being Element of INT st S2[n,x,y,z,w,z,y1,z1,w1]
take w ; ::_thesis: ex z1, w1 being Element of INT st S2[n,x,y,z,w,z,w,z1,w1]
take z1 ; ::_thesis: ex w1 being Element of INT st S2[n,x,y,z,w,z,w,z1,w1]
take w1 ; ::_thesis: S2[n,x,y,z,w,z,w,z1,w1]
thus S2[n,x,y,z,w,z,w,z1,w1] ; ::_thesis: verum
end;
consider a, b, u, v being sequence of INT such that
P2: ( a . 0 = i1 & b . 0 = i0 & u . 0 = i0 & v . 0 = i1 & ( for i being Element of NAT holds S2[i,a . i,b . i,u . i,v . i,a . (i + 1),b . (i + 1),u . (i + 1),v . (i + 1)] ) ) from NTALGO_1:sch_1(A2);
take g ; ::_thesis: ex w, q, t, a, b, v, u being sequence of INT st
( a . 0 = 1 & b . 0 = 0 & g . 0 = x & q . 0 = 0 & u . 0 = 0 & v . 0 = 1 & w . 0 = y & t . 0 = 0 & ( for i being Element of NAT holds
( q . (i + 1) = (g . i) div (w . i) & t . (i + 1) = (g . i) mod (w . i) & a . (i + 1) = u . i & b . (i + 1) = v . i & g . (i + 1) = w . i & u . (i + 1) = (a . i) - ((q . (i + 1)) * (u . i)) & v . (i + 1) = (b . i) - ((q . (i + 1)) * (v . i)) & w . (i + 1) = t . (i + 1) ) ) )
take w ; ::_thesis: ex q, t, a, b, v, u being sequence of INT st
( a . 0 = 1 & b . 0 = 0 & g . 0 = x & q . 0 = 0 & u . 0 = 0 & v . 0 = 1 & w . 0 = y & t . 0 = 0 & ( for i being Element of NAT holds
( q . (i + 1) = (g . i) div (w . i) & t . (i + 1) = (g . i) mod (w . i) & a . (i + 1) = u . i & b . (i + 1) = v . i & g . (i + 1) = w . i & u . (i + 1) = (a . i) - ((q . (i + 1)) * (u . i)) & v . (i + 1) = (b . i) - ((q . (i + 1)) * (v . i)) & w . (i + 1) = t . (i + 1) ) ) )
take q ; ::_thesis: ex t, a, b, v, u being sequence of INT st
( a . 0 = 1 & b . 0 = 0 & g . 0 = x & q . 0 = 0 & u . 0 = 0 & v . 0 = 1 & w . 0 = y & t . 0 = 0 & ( for i being Element of NAT holds
( q . (i + 1) = (g . i) div (w . i) & t . (i + 1) = (g . i) mod (w . i) & a . (i + 1) = u . i & b . (i + 1) = v . i & g . (i + 1) = w . i & u . (i + 1) = (a . i) - ((q . (i + 1)) * (u . i)) & v . (i + 1) = (b . i) - ((q . (i + 1)) * (v . i)) & w . (i + 1) = t . (i + 1) ) ) )
take t ; ::_thesis: ex a, b, v, u being sequence of INT st
( a . 0 = 1 & b . 0 = 0 & g . 0 = x & q . 0 = 0 & u . 0 = 0 & v . 0 = 1 & w . 0 = y & t . 0 = 0 & ( for i being Element of NAT holds
( q . (i + 1) = (g . i) div (w . i) & t . (i + 1) = (g . i) mod (w . i) & a . (i + 1) = u . i & b . (i + 1) = v . i & g . (i + 1) = w . i & u . (i + 1) = (a . i) - ((q . (i + 1)) * (u . i)) & v . (i + 1) = (b . i) - ((q . (i + 1)) * (v . i)) & w . (i + 1) = t . (i + 1) ) ) )
take a ; ::_thesis: ex b, v, u being sequence of INT st
( a . 0 = 1 & b . 0 = 0 & g . 0 = x & q . 0 = 0 & u . 0 = 0 & v . 0 = 1 & w . 0 = y & t . 0 = 0 & ( for i being Element of NAT holds
( q . (i + 1) = (g . i) div (w . i) & t . (i + 1) = (g . i) mod (w . i) & a . (i + 1) = u . i & b . (i + 1) = v . i & g . (i + 1) = w . i & u . (i + 1) = (a . i) - ((q . (i + 1)) * (u . i)) & v . (i + 1) = (b . i) - ((q . (i + 1)) * (v . i)) & w . (i + 1) = t . (i + 1) ) ) )
take b ; ::_thesis: ex v, u being sequence of INT st
( a . 0 = 1 & b . 0 = 0 & g . 0 = x & q . 0 = 0 & u . 0 = 0 & v . 0 = 1 & w . 0 = y & t . 0 = 0 & ( for i being Element of NAT holds
( q . (i + 1) = (g . i) div (w . i) & t . (i + 1) = (g . i) mod (w . i) & a . (i + 1) = u . i & b . (i + 1) = v . i & g . (i + 1) = w . i & u . (i + 1) = (a . i) - ((q . (i + 1)) * (u . i)) & v . (i + 1) = (b . i) - ((q . (i + 1)) * (v . i)) & w . (i + 1) = t . (i + 1) ) ) )
take v ; ::_thesis: ex u being sequence of INT st
( a . 0 = 1 & b . 0 = 0 & g . 0 = x & q . 0 = 0 & u . 0 = 0 & v . 0 = 1 & w . 0 = y & t . 0 = 0 & ( for i being Element of NAT holds
( q . (i + 1) = (g . i) div (w . i) & t . (i + 1) = (g . i) mod (w . i) & a . (i + 1) = u . i & b . (i + 1) = v . i & g . (i + 1) = w . i & u . (i + 1) = (a . i) - ((q . (i + 1)) * (u . i)) & v . (i + 1) = (b . i) - ((q . (i + 1)) * (v . i)) & w . (i + 1) = t . (i + 1) ) ) )
take u ; ::_thesis: ( a . 0 = 1 & b . 0 = 0 & g . 0 = x & q . 0 = 0 & u . 0 = 0 & v . 0 = 1 & w . 0 = y & t . 0 = 0 & ( for i being Element of NAT holds
( q . (i + 1) = (g . i) div (w . i) & t . (i + 1) = (g . i) mod (w . i) & a . (i + 1) = u . i & b . (i + 1) = v . i & g . (i + 1) = w . i & u . (i + 1) = (a . i) - ((q . (i + 1)) * (u . i)) & v . (i + 1) = (b . i) - ((q . (i + 1)) * (v . i)) & w . (i + 1) = t . (i + 1) ) ) )
thus ( a . 0 = 1 & b . 0 = 0 & g . 0 = x & q . 0 = 0 & u . 0 = 0 & v . 0 = 1 & w . 0 = y & t . 0 = 0 & ( for i being Element of NAT holds
( q . (i + 1) = (g . i) div (w . i) & t . (i + 1) = (g . i) mod (w . i) & a . (i + 1) = u . i & b . (i + 1) = v . i & g . (i + 1) = w . i & u . (i + 1) = (a . i) - ((q . (i + 1)) * (u . i)) & v . (i + 1) = (b . i) - ((q . (i + 1)) * (v . i)) & w . (i + 1) = t . (i + 1) ) ) ) by P1, P2; ::_thesis: verum
end;
EXLM2: for x, y being Element of INT
for g1, w1, q1, t1, a1, b1, v1, u1, g2, w2, q2, t2, a2, b2, v2, u2 being sequence of INT st a1 . 0 = 1 & b1 . 0 = 0 & g1 . 0 = x & q1 . 0 = 0 & u1 . 0 = 0 & v1 . 0 = 1 & w1 . 0 = y & t1 . 0 = 0 & ( for i being Element of NAT holds
( q1 . (i + 1) = (g1 . i) div (w1 . i) & t1 . (i + 1) = (g1 . i) mod (w1 . i) & a1 . (i + 1) = u1 . i & b1 . (i + 1) = v1 . i & g1 . (i + 1) = w1 . i & u1 . (i + 1) = (a1 . i) - ((q1 . (i + 1)) * (u1 . i)) & v1 . (i + 1) = (b1 . i) - ((q1 . (i + 1)) * (v1 . i)) & w1 . (i + 1) = t1 . (i + 1) ) ) & a2 . 0 = 1 & b2 . 0 = 0 & g2 . 0 = x & q2 . 0 = 0 & u2 . 0 = 0 & v2 . 0 = 1 & w2 . 0 = y & t2 . 0 = 0 & ( for i being Element of NAT holds
( q2 . (i + 1) = (g2 . i) div (w2 . i) & t2 . (i + 1) = (g2 . i) mod (w2 . i) & a2 . (i + 1) = u2 . i & b2 . (i + 1) = v2 . i & g2 . (i + 1) = w2 . i & u2 . (i + 1) = (a2 . i) - ((q2 . (i + 1)) * (u2 . i)) & v2 . (i + 1) = (b2 . i) - ((q2 . (i + 1)) * (v2 . i)) & w2 . (i + 1) = t2 . (i + 1) ) ) holds
( g1 = g2 & w1 = w2 & q1 = q2 & t1 = t2 & a1 = a2 & b1 = b2 & v1 = v2 & u1 = u2 )
proof
let x, y be Element of INT ; ::_thesis: for g1, w1, q1, t1, a1, b1, v1, u1, g2, w2, q2, t2, a2, b2, v2, u2 being sequence of INT st a1 . 0 = 1 & b1 . 0 = 0 & g1 . 0 = x & q1 . 0 = 0 & u1 . 0 = 0 & v1 . 0 = 1 & w1 . 0 = y & t1 . 0 = 0 & ( for i being Element of NAT holds
( q1 . (i + 1) = (g1 . i) div (w1 . i) & t1 . (i + 1) = (g1 . i) mod (w1 . i) & a1 . (i + 1) = u1 . i & b1 . (i + 1) = v1 . i & g1 . (i + 1) = w1 . i & u1 . (i + 1) = (a1 . i) - ((q1 . (i + 1)) * (u1 . i)) & v1 . (i + 1) = (b1 . i) - ((q1 . (i + 1)) * (v1 . i)) & w1 . (i + 1) = t1 . (i + 1) ) ) & a2 . 0 = 1 & b2 . 0 = 0 & g2 . 0 = x & q2 . 0 = 0 & u2 . 0 = 0 & v2 . 0 = 1 & w2 . 0 = y & t2 . 0 = 0 & ( for i being Element of NAT holds
( q2 . (i + 1) = (g2 . i) div (w2 . i) & t2 . (i + 1) = (g2 . i) mod (w2 . i) & a2 . (i + 1) = u2 . i & b2 . (i + 1) = v2 . i & g2 . (i + 1) = w2 . i & u2 . (i + 1) = (a2 . i) - ((q2 . (i + 1)) * (u2 . i)) & v2 . (i + 1) = (b2 . i) - ((q2 . (i + 1)) * (v2 . i)) & w2 . (i + 1) = t2 . (i + 1) ) ) holds
( g1 = g2 & w1 = w2 & q1 = q2 & t1 = t2 & a1 = a2 & b1 = b2 & v1 = v2 & u1 = u2 )
let g1, w1, q1, t1, a1, b1, v1, u1, g2, w2, q2, t2, a2, b2, v2, u2 be sequence of INT; ::_thesis: ( a1 . 0 = 1 & b1 . 0 = 0 & g1 . 0 = x & q1 . 0 = 0 & u1 . 0 = 0 & v1 . 0 = 1 & w1 . 0 = y & t1 . 0 = 0 & ( for i being Element of NAT holds
( q1 . (i + 1) = (g1 . i) div (w1 . i) & t1 . (i + 1) = (g1 . i) mod (w1 . i) & a1 . (i + 1) = u1 . i & b1 . (i + 1) = v1 . i & g1 . (i + 1) = w1 . i & u1 . (i + 1) = (a1 . i) - ((q1 . (i + 1)) * (u1 . i)) & v1 . (i + 1) = (b1 . i) - ((q1 . (i + 1)) * (v1 . i)) & w1 . (i + 1) = t1 . (i + 1) ) ) & a2 . 0 = 1 & b2 . 0 = 0 & g2 . 0 = x & q2 . 0 = 0 & u2 . 0 = 0 & v2 . 0 = 1 & w2 . 0 = y & t2 . 0 = 0 & ( for i being Element of NAT holds
( q2 . (i + 1) = (g2 . i) div (w2 . i) & t2 . (i + 1) = (g2 . i) mod (w2 . i) & a2 . (i + 1) = u2 . i & b2 . (i + 1) = v2 . i & g2 . (i + 1) = w2 . i & u2 . (i + 1) = (a2 . i) - ((q2 . (i + 1)) * (u2 . i)) & v2 . (i + 1) = (b2 . i) - ((q2 . (i + 1)) * (v2 . i)) & w2 . (i + 1) = t2 . (i + 1) ) ) implies ( g1 = g2 & w1 = w2 & q1 = q2 & t1 = t2 & a1 = a2 & b1 = b2 & v1 = v2 & u1 = u2 ) )
assume P1: ( a1 . 0 = 1 & b1 . 0 = 0 & g1 . 0 = x & q1 . 0 = 0 & u1 . 0 = 0 & v1 . 0 = 1 & w1 . 0 = y & t1 . 0 = 0 & ( for i being Element of NAT holds
( q1 . (i + 1) = (g1 . i) div (w1 . i) & t1 . (i + 1) = (g1 . i) mod (w1 . i) & a1 . (i + 1) = u1 . i & b1 . (i + 1) = v1 . i & g1 . (i + 1) = w1 . i & u1 . (i + 1) = (a1 . i) - ((q1 . (i + 1)) * (u1 . i)) & v1 . (i + 1) = (b1 . i) - ((q1 . (i + 1)) * (v1 . i)) & w1 . (i + 1) = t1 . (i + 1) ) ) ) ; ::_thesis: ( not a2 . 0 = 1 or not b2 . 0 = 0 or not g2 . 0 = x or not q2 . 0 = 0 or not u2 . 0 = 0 or not v2 . 0 = 1 or not w2 . 0 = y or not t2 . 0 = 0 or ex i being Element of NAT st
( 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)) implies not w2 . (i + 1) = t2 . (i + 1) ) or ( g1 = g2 & w1 = w2 & q1 = q2 & t1 = t2 & a1 = a2 & b1 = b2 & v1 = v2 & u1 = u2 ) )
assume P2: ( a2 . 0 = 1 & b2 . 0 = 0 & g2 . 0 = x & q2 . 0 = 0 & u2 . 0 = 0 & v2 . 0 = 1 & w2 . 0 = y & t2 . 0 = 0 & ( for i being Element of NAT holds
( q2 . (i + 1) = (g2 . i) div (w2 . i) & t2 . (i + 1) = (g2 . i) mod (w2 . i) & a2 . (i + 1) = u2 . i & b2 . (i + 1) = v2 . i & g2 . (i + 1) = w2 . i & u2 . (i + 1) = (a2 . i) - ((q2 . (i + 1)) * (u2 . i)) & v2 . (i + 1) = (b2 . i) - ((q2 . (i + 1)) * (v2 . i)) & w2 . (i + 1) = t2 . (i + 1) ) ) ) ; ::_thesis: ( g1 = g2 & w1 = w2 & q1 = q2 & t1 = t2 & a1 = a2 & b1 = b2 & v1 = v2 & u1 = u2 )
defpred S1[ 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 );
P0: S1[ 0 ] by P1, P2;
PN: for n being Element of NAT st S1[n] holds
S1[n + 1]
proof
let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] )
assume PN1: S1[n] ; ::_thesis: S1[n + 1]
X1: q1 . (n + 1) = (g2 . n) div (w2 . n) by P1, PN1
.= q2 . (n + 1) by P2 ;
X2: t1 . (n + 1) = (g2 . n) mod (w2 . n) by P1, PN1
.= t2 . (n + 1) by P2 ;
X3: a1 . (n + 1) = u2 . n by P1, PN1
.= a2 . (n + 1) by P2 ;
X4: b1 . (n + 1) = v2 . n by PN1, P1
.= b2 . (n + 1) by P2 ;
X5: g1 . (n + 1) = w2 . n by PN1, P1
.= g2 . (n + 1) by P2 ;
X6: u1 . (n + 1) = (a2 . n) - ((q1 . (n + 1)) * (u2 . n)) by P1, PN1
.= u2 . (n + 1) by P2, X1 ;
X7: v1 . (n + 1) = (b2 . n) - ((q1 . (n + 1)) * (v2 . n)) by PN1, P1
.= v2 . (n + 1) by P2, X1 ;
w1 . (n + 1) = t2 . (n + 1) by X2, P1
.= w2 . (n + 1) by P2 ;
hence S1[n + 1] by X1, X2, X3, X4, X5, X6, X7; ::_thesis: verum
end;
for n being Element of NAT holds S1[n] from NAT_1:sch_1(P0, PN);
hence ( g1 = g2 & w1 = w2 & q1 = q2 & t1 = t2 & a1 = a2 & b1 = b2 & v1 = v2 & u1 = u2 ) by FUNCT_2:def_8; ::_thesis: verum
end;
definition
let x, y be Element of INT ;
func ALGO_EXGCD (x,y) -> Element of [:INT,INT,INT:] means :defALGOEXGCD: :: NTALGO_1:def 2
ex g, w, q, t, a, b, v, u being sequence of INT ex istop being Element of NAT st
( a . 0 = 1 & b . 0 = 0 & g . 0 = x & q . 0 = 0 & u . 0 = 0 & v . 0 = 1 & w . 0 = y & t . 0 = 0 & ( for i being Element of NAT holds
( q . (i + 1) = (g . i) div (w . i) & t . (i + 1) = (g . i) mod (w . i) & a . (i + 1) = u . i & b . (i + 1) = v . i & g . (i + 1) = w . i & u . (i + 1) = (a . i) - ((q . (i + 1)) * (u . i)) & v . (i + 1) = (b . i) - ((q . (i + 1)) * (v . i)) & w . (i + 1) = t . (i + 1) ) ) & istop = min* { i where i is Element of NAT : w . i = 0 } & ( 0 <= g . istop implies it = [(a . istop),(b . istop),(g . istop)] ) & ( g . istop < 0 implies it = [(- (a . istop)),(- (b . istop)),(- (g . istop))] ) );
existence
ex b1 being Element of [:INT,INT,INT:] ex g, w, q, t, a, b, v, u being sequence of INT ex istop being Element of NAT st
( a . 0 = 1 & b . 0 = 0 & g . 0 = x & q . 0 = 0 & u . 0 = 0 & v . 0 = 1 & w . 0 = y & t . 0 = 0 & ( for i being Element of NAT holds
( q . (i + 1) = (g . i) div (w . i) & t . (i + 1) = (g . i) mod (w . i) & a . (i + 1) = u . i & b . (i + 1) = v . i & g . (i + 1) = w . i & u . (i + 1) = (a . i) - ((q . (i + 1)) * (u . i)) & v . (i + 1) = (b . i) - ((q . (i + 1)) * (v . i)) & w . (i + 1) = t . (i + 1) ) ) & istop = min* { i where i is Element of NAT : w . i = 0 } & ( 0 <= g . istop implies b1 = [(a . istop),(b . istop),(g . istop)] ) & ( g . istop < 0 implies b1 = [(- (a . istop)),(- (b . istop)),(- (g . istop))] ) )
proof
consider g, w, q, t, a, b, v, u being sequence of INT such that
P1: ( a . 0 = 1 & b . 0 = 0 & g . 0 = x & q . 0 = 0 & u . 0 = 0 & v . 0 = 1 & w . 0 = y & t . 0 = 0 & ( for i being Element of NAT holds
( q . (i + 1) = (g . i) div (w . i) & t . (i + 1) = (g . i) mod (w . i) & a . (i + 1) = u . i & b . (i + 1) = v . i & g . (i + 1) = w . i & u . (i + 1) = (a . i) - ((q . (i + 1)) * (u . i)) & v . (i + 1) = (b . i) - ((q . (i + 1)) * (v . i)) & w . (i + 1) = t . (i + 1) ) ) ) by EXLM1;
set istop = min* { i where i is Element of NAT : w . i = 0 } ;
now__::_thesis:_ex_xx_being_Element_of_[:INT,INT,INT:]_st_
(_(_0_<=_g_._(min*__{__i_where_i_is_Element_of_NAT_:_w_._i_=_0__}__)_implies_xx_=_[(a_._(min*__{__i_where_i_is_Element_of_NAT_:_w_._i_=_0__}__)),(b_._(min*__{__i_where_i_is_Element_of_NAT_:_w_._i_=_0__}__)),(g_._(min*__{__i_where_i_is_Element_of_NAT_:_w_._i_=_0__}__))]_)_&_(_g_._(min*__{__i_where_i_is_Element_of_NAT_:_w_._i_=_0__}__)_<_0_implies_xx_=_[(-_(a_._(min*__{__i_where_i_is_Element_of_NAT_:_w_._i_=_0__}__))),(-_(b_._(min*__{__i_where_i_is_Element_of_NAT_:_w_._i_=_0__}__))),(-_(g_._(min*__{__i_where_i_is_Element_of_NAT_:_w_._i_=_0__}__)))]_)_)
percases ( 0 <= g . (min* { i where i is Element of NAT : w . i = 0 } ) or g . (min* { i where i is Element of NAT : w . i = 0 } ) < 0 ) ;
supposeC1: 0 <= g . (min* { i where i is Element of NAT : w . i = 0 } ) ; ::_thesis: ex xx being Element of [:INT,INT,INT:] st
( ( 0 <= g . (min* { i where i is Element of NAT : w . i = 0 } ) implies xx = [(a . (min* { i where i is Element of NAT : w . i = 0 } )),(b . (min* { i where i is Element of NAT : w . i = 0 } )),(g . (min* { i where i is Element of NAT : w . i = 0 } ))] ) & ( g . (min* { i where i is Element of NAT : w . i = 0 } ) < 0 implies xx = [(- (a . (min* { i where i is Element of NAT : w . i = 0 } ))),(- (b . (min* { i where i is Element of NAT : w . i = 0 } ))),(- (g . (min* { i where i is Element of NAT : w . i = 0 } )))] ) )
[(a . (min* { i where i is Element of NAT : w . i = 0 } )),(b . (min* { i where i is Element of NAT : w . i = 0 } )),(g . (min* { i where i is Element of NAT : w . i = 0 } ))] in [:INT,INT,INT:] by MCART_1:69;
hence ex xx being Element of [:INT,INT,INT:] st
( ( 0 <= g . (min* { i where i is Element of NAT : w . i = 0 } ) implies xx = [(a . (min* { i where i is Element of NAT : w . i = 0 } )),(b . (min* { i where i is Element of NAT : w . i = 0 } )),(g . (min* { i where i is Element of NAT : w . i = 0 } ))] ) & ( g . (min* { i where i is Element of NAT : w . i = 0 } ) < 0 implies xx = [(- (a . (min* { i where i is Element of NAT : w . i = 0 } ))),(- (b . (min* { i where i is Element of NAT : w . i = 0 } ))),(- (g . (min* { i where i is Element of NAT : w . i = 0 } )))] ) ) by C1; ::_thesis: verum
end;
supposeC2: g . (min* { i where i is Element of NAT : w . i = 0 } ) < 0 ; ::_thesis: ex xx being Element of [:INT,INT,INT:] st
( ( 0 <= g . (min* { i where i is Element of NAT : w . i = 0 } ) implies xx = [(a . (min* { i where i is Element of NAT : w . i = 0 } )),(b . (min* { i where i is Element of NAT : w . i = 0 } )),(g . (min* { i where i is Element of NAT : w . i = 0 } ))] ) & ( g . (min* { i where i is Element of NAT : w . i = 0 } ) < 0 implies xx = [(- (a . (min* { i where i is Element of NAT : w . i = 0 } ))),(- (b . (min* { i where i is Element of NAT : w . i = 0 } ))),(- (g . (min* { i where i is Element of NAT : w . i = 0 } )))] ) )
X1: - (g . (min* { i where i is Element of NAT : w . i = 0 } )) in INT by INT_1:def_2;
( - (a . (min* { i where i is Element of NAT : w . i = 0 } )) in INT & - (b . (min* { i where i is Element of NAT : w . i = 0 } )) in INT ) by INT_1:def_2;
then [(- (a . (min* { i where i is Element of NAT : w . i = 0 } ))),(- (b . (min* { i where i is Element of NAT : w . i = 0 } ))),(- (g . (min* { i where i is Element of NAT : w . i = 0 } )))] in [:INT,INT,INT:] by MCART_1:69, X1;
hence ex xx being Element of [:INT,INT,INT:] st
( ( 0 <= g . (min* { i where i is Element of NAT : w . i = 0 } ) implies xx = [(a . (min* { i where i is Element of NAT : w . i = 0 } )),(b . (min* { i where i is Element of NAT : w . i = 0 } )),(g . (min* { i where i is Element of NAT : w . i = 0 } ))] ) & ( g . (min* { i where i is Element of NAT : w . i = 0 } ) < 0 implies xx = [(- (a . (min* { i where i is Element of NAT : w . i = 0 } ))),(- (b . (min* { i where i is Element of NAT : w . i = 0 } ))),(- (g . (min* { i where i is Element of NAT : w . i = 0 } )))] ) ) by C2; ::_thesis: verum
end;
end;
end;
then consider xx being Element of [:INT,INT,INT:] such that
P2: ( ( 0 <= g . (min* { i where i is Element of NAT : w . i = 0 } ) implies xx = [(a . (min* { i where i is Element of NAT : w . i = 0 } )),(b . (min* { i where i is Element of NAT : w . i = 0 } )),(g . (min* { i where i is Element of NAT : w . i = 0 } ))] ) & ( g . (min* { i where i is Element of NAT : w . i = 0 } ) < 0 implies xx = [(- (a . (min* { i where i is Element of NAT : w . i = 0 } ))),(- (b . (min* { i where i is Element of NAT : w . i = 0 } ))),(- (g . (min* { i where i is Element of NAT : w . i = 0 } )))] ) ) ;
take xx ; ::_thesis: ex g, w, q, t, a, b, v, u being sequence of INT ex istop being Element of NAT st
( a . 0 = 1 & b . 0 = 0 & g . 0 = x & q . 0 = 0 & u . 0 = 0 & v . 0 = 1 & w . 0 = y & t . 0 = 0 & ( for i being Element of NAT holds
( q . (i + 1) = (g . i) div (w . i) & t . (i + 1) = (g . i) mod (w . i) & a . (i + 1) = u . i & b . (i + 1) = v . i & g . (i + 1) = w . i & u . (i + 1) = (a . i) - ((q . (i + 1)) * (u . i)) & v . (i + 1) = (b . i) - ((q . (i + 1)) * (v . i)) & w . (i + 1) = t . (i + 1) ) ) & istop = min* { i where i is Element of NAT : w . i = 0 } & ( 0 <= g . istop implies xx = [(a . istop),(b . istop),(g . istop)] ) & ( g . istop < 0 implies xx = [(- (a . istop)),(- (b . istop)),(- (g . istop))] ) )
thus ex g, w, q, t, a, b, v, u being sequence of INT ex istop being Element of NAT st
( a . 0 = 1 & b . 0 = 0 & g . 0 = x & q . 0 = 0 & u . 0 = 0 & v . 0 = 1 & w . 0 = y & t . 0 = 0 & ( for i being Element of NAT holds
( q . (i + 1) = (g . i) div (w . i) & t . (i + 1) = (g . i) mod (w . i) & a . (i + 1) = u . i & b . (i + 1) = v . i & g . (i + 1) = w . i & u . (i + 1) = (a . i) - ((q . (i + 1)) * (u . i)) & v . (i + 1) = (b . i) - ((q . (i + 1)) * (v . i)) & w . (i + 1) = t . (i + 1) ) ) & istop = min* { i where i is Element of NAT : w . i = 0 } & ( 0 <= g . istop implies xx = [(a . istop),(b . istop),(g . istop)] ) & ( g . istop < 0 implies xx = [(- (a . istop)),(- (b . istop)),(- (g . istop))] ) ) by P1, P2; ::_thesis: verum
end;
uniqueness
for b1, b2 being Element of [:INT,INT,INT:] st ex g, w, q, t, a, b, v, u being sequence of INT ex istop being Element of NAT st
( a . 0 = 1 & b . 0 = 0 & g . 0 = x & q . 0 = 0 & u . 0 = 0 & v . 0 = 1 & w . 0 = y & t . 0 = 0 & ( for i being Element of NAT holds
( q . (i + 1) = (g . i) div (w . i) & t . (i + 1) = (g . i) mod (w . i) & a . (i + 1) = u . i & b . (i + 1) = v . i & g . (i + 1) = w . i & u . (i + 1) = (a . i) - ((q . (i + 1)) * (u . i)) & v . (i + 1) = (b . i) - ((q . (i + 1)) * (v . i)) & w . (i + 1) = t . (i + 1) ) ) & istop = min* { i where i is Element of NAT : w . i = 0 } & ( 0 <= g . istop implies b1 = [(a . istop),(b . istop),(g . istop)] ) & ( g . istop < 0 implies b1 = [(- (a . istop)),(- (b . istop)),(- (g . istop))] ) ) & ex g, w, q, t, a, b, v, u being sequence of INT ex istop being Element of NAT st
( a . 0 = 1 & b . 0 = 0 & g . 0 = x & q . 0 = 0 & u . 0 = 0 & v . 0 = 1 & w . 0 = y & t . 0 = 0 & ( for i being Element of NAT holds
( q . (i + 1) = (g . i) div (w . i) & t . (i + 1) = (g . i) mod (w . i) & a . (i + 1) = u . i & b . (i + 1) = v . i & g . (i + 1) = w . i & u . (i + 1) = (a . i) - ((q . (i + 1)) * (u . i)) & v . (i + 1) = (b . i) - ((q . (i + 1)) * (v . i)) & w . (i + 1) = t . (i + 1) ) ) & istop = min* { i where i is Element of NAT : w . i = 0 } & ( 0 <= g . istop implies b2 = [(a . istop),(b . istop),(g . istop)] ) & ( g . istop < 0 implies b2 = [(- (a . istop)),(- (b . istop)),(- (g . istop))] ) ) holds
b1 = b2
proof
let s1, s2 be Element of [:INT,INT,INT:]; ::_thesis: ( ex g, w, q, t, a, b, v, u being sequence of INT ex istop being Element of NAT st
( a . 0 = 1 & b . 0 = 0 & g . 0 = x & q . 0 = 0 & u . 0 = 0 & v . 0 = 1 & w . 0 = y & t . 0 = 0 & ( for i being Element of NAT holds
( q . (i + 1) = (g . i) div (w . i) & t . (i + 1) = (g . i) mod (w . i) & a . (i + 1) = u . i & b . (i + 1) = v . i & g . (i + 1) = w . i & u . (i + 1) = (a . i) - ((q . (i + 1)) * (u . i)) & v . (i + 1) = (b . i) - ((q . (i + 1)) * (v . i)) & w . (i + 1) = t . (i + 1) ) ) & istop = min* { i where i is Element of NAT : w . i = 0 } & ( 0 <= g . istop implies s1 = [(a . istop),(b . istop),(g . istop)] ) & ( g . istop < 0 implies s1 = [(- (a . istop)),(- (b . istop)),(- (g . istop))] ) ) & ex g, w, q, t, a, b, v, u being sequence of INT ex istop being Element of NAT st
( a . 0 = 1 & b . 0 = 0 & g . 0 = x & q . 0 = 0 & u . 0 = 0 & v . 0 = 1 & w . 0 = y & t . 0 = 0 & ( for i being Element of NAT holds
( q . (i + 1) = (g . i) div (w . i) & t . (i + 1) = (g . i) mod (w . i) & a . (i + 1) = u . i & b . (i + 1) = v . i & g . (i + 1) = w . i & u . (i + 1) = (a . i) - ((q . (i + 1)) * (u . i)) & v . (i + 1) = (b . i) - ((q . (i + 1)) * (v . i)) & w . (i + 1) = t . (i + 1) ) ) & istop = min* { i where i is Element of NAT : w . i = 0 } & ( 0 <= g . istop implies s2 = [(a . istop),(b . istop),(g . istop)] ) & ( g . istop < 0 implies s2 = [(- (a . istop)),(- (b . istop)),(- (g . istop))] ) ) implies s1 = s2 )
assume A1: ex g1, w1, q1, t1, a1, b1, v1, u1 being sequence of INT ex istop1 being Element of 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 being Element of NAT holds
( q1 . (i + 1) = (g1 . i) div (w1 . i) & t1 . (i + 1) = (g1 . i) mod (w1 . i) & a1 . (i + 1) = u1 . i & b1 . (i + 1) = v1 . i & g1 . (i + 1) = w1 . i & u1 . (i + 1) = (a1 . i) - ((q1 . (i + 1)) * (u1 . i)) & v1 . (i + 1) = (b1 . i) - ((q1 . (i + 1)) * (v1 . i)) & w1 . (i + 1) = t1 . (i + 1) ) ) & istop1 = min* { i where i is Element of 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))] ) ) ; ::_thesis: ( for g, w, q, t, a, b, v, u being sequence of INT
for istop being Element of NAT holds
( not a . 0 = 1 or not b . 0 = 0 or not g . 0 = x or not q . 0 = 0 or not u . 0 = 0 or not v . 0 = 1 or not w . 0 = y or not t . 0 = 0 or ex i being Element of NAT st
( 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)) implies not w . (i + 1) = t . (i + 1) ) or not istop = min* { i where i is Element of NAT : w . i = 0 } or ( 0 <= g . istop & not s2 = [(a . istop),(b . istop),(g . istop)] ) or ( g . istop < 0 & not s2 = [(- (a . istop)),(- (b . istop)),(- (g . istop))] ) ) or s1 = s2 )
assume A2: ex g2, w2, q2, t2, a2, b2, v2, u2 being sequence of INT ex istop2 being Element of 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 being Element of NAT holds
( q2 . (i + 1) = (g2 . i) div (w2 . i) & t2 . (i + 1) = (g2 . i) mod (w2 . i) & a2 . (i + 1) = u2 . i & b2 . (i + 1) = v2 . i & g2 . (i + 1) = w2 . i & u2 . (i + 1) = (a2 . i) - ((q2 . (i + 1)) * (u2 . i)) & v2 . (i + 1) = (b2 . i) - ((q2 . (i + 1)) * (v2 . i)) & w2 . (i + 1) = t2 . (i + 1) ) ) & istop2 = min* { i where i is Element of 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))] ) ) ; ::_thesis: s1 = s2
consider g1, w1, q1, t1, a1, b1, v1, u1 being sequence of INT, istop1 being Element of NAT such that
P1: ( a1 . 0 = 1 & b1 . 0 = 0 & g1 . 0 = x & q1 . 0 = 0 & u1 . 0 = 0 & v1 . 0 = 1 & w1 . 0 = y & t1 . 0 = 0 & ( for i being Element of NAT holds
( q1 . (i + 1) = (g1 . i) div (w1 . i) & t1 . (i + 1) = (g1 . i) mod (w1 . i) & a1 . (i + 1) = u1 . i & b1 . (i + 1) = v1 . i & g1 . (i + 1) = w1 . i & u1 . (i + 1) = (a1 . i) - ((q1 . (i + 1)) * (u1 . i)) & v1 . (i + 1) = (b1 . i) - ((q1 . (i + 1)) * (v1 . i)) & w1 . (i + 1) = t1 . (i + 1) ) ) & istop1 = min* { k where k is Element of 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 A1;
consider g2, w2, q2, t2, a2, b2, v2, u2 being sequence of INT, istop2 being Element of NAT such that
P2: ( a2 . 0 = 1 & b2 . 0 = 0 & g2 . 0 = x & q2 . 0 = 0 & u2 . 0 = 0 & v2 . 0 = 1 & w2 . 0 = y & t2 . 0 = 0 & ( for i being Element of NAT holds
( q2 . (i + 1) = (g2 . i) div (w2 . i) & t2 . (i + 1) = (g2 . i) mod (w2 . i) & a2 . (i + 1) = u2 . i & b2 . (i + 1) = v2 . i & g2 . (i + 1) = w2 . i & u2 . (i + 1) = (a2 . i) - ((q2 . (i + 1)) * (u2 . i)) & v2 . (i + 1) = (b2 . i) - ((q2 . (i + 1)) * (v2 . i)) & w2 . (i + 1) = t2 . (i + 1) ) ) & istop2 = min* { k where k is Element of 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 A2;
( g1 = g2 & w1 = w2 & a1 = a2 & b1 = b2 ) by P1, P2, EXLM2;
hence s1 = s2 by P1, P2; ::_thesis: verum
end;
end;
:: deftheorem defALGOEXGCD defines ALGO_EXGCD NTALGO_1:def_2_:_
for x, y being Element of INT
for b3 being Element of [:INT,INT,INT:] holds
( b3 = ALGO_EXGCD (x,y) iff ex g, w, q, t, a, b, v, u being sequence of INT ex istop being Element of NAT st
( a . 0 = 1 & b . 0 = 0 & g . 0 = x & q . 0 = 0 & u . 0 = 0 & v . 0 = 1 & w . 0 = y & t . 0 = 0 & ( for i being Element of NAT holds
( q . (i + 1) = (g . i) div (w . i) & t . (i + 1) = (g . i) mod (w . i) & a . (i + 1) = u . i & b . (i + 1) = v . i & g . (i + 1) = w . i & u . (i + 1) = (a . i) - ((q . (i + 1)) * (u . i)) & v . (i + 1) = (b . i) - ((q . (i + 1)) * (v . i)) & w . (i + 1) = t . (i + 1) ) ) & istop = min* { i where i is Element of NAT : w . i = 0 } & ( 0 <= g . istop implies b3 = [(a . istop),(b . istop),(g . istop)] ) & ( g . istop < 0 implies b3 = [(- (a . istop)),(- (b . istop)),(- (g . istop))] ) ) );
LM3G: for a, b being Element of INT
for A, B being sequence of INT st A . 0 = a & B . 0 = b & ( for i being Element of NAT holds
( A . (i + 1) = B . i & B . (i + 1) = (A . i) mod (B . i) ) ) holds
for i being Element of NAT st B . i <> 0 holds
(A . i) gcd (B . i) = (A . (i + 1)) gcd (B . (i + 1))
proof
let a, b be Element of INT ; ::_thesis: for A, B being sequence of INT st A . 0 = a & B . 0 = b & ( for i being Element of NAT holds
( A . (i + 1) = B . i & B . (i + 1) = (A . i) mod (B . i) ) ) holds
for i being Element of NAT st B . i <> 0 holds
(A . i) gcd (B . i) = (A . (i + 1)) gcd (B . (i + 1))
let A, B be sequence of INT; ::_thesis: ( A . 0 = a & B . 0 = b & ( for i being Element of NAT holds
( A . (i + 1) = B . i & B . (i + 1) = (A . i) mod (B . i) ) ) implies for i being Element of NAT st B . i <> 0 holds
(A . i) gcd (B . i) = (A . (i + 1)) gcd (B . (i + 1)) )
assume AS: ( A . 0 = a & B . 0 = b & ( for i being Element of NAT holds
( A . (i + 1) = B . i & B . (i + 1) = (A . i) mod (B . i) ) ) ) ; ::_thesis: for i being Element of NAT st B . i <> 0 holds
(A . i) gcd (B . i) = (A . (i + 1)) gcd (B . (i + 1))
let i be Element of NAT ; ::_thesis: ( B . i <> 0 implies (A . i) gcd (B . i) = (A . (i + 1)) gcd (B . (i + 1)) )
assume AS1: B . i <> 0 ; ::_thesis: (A . i) gcd (B . i) = (A . (i + 1)) gcd (B . (i + 1))
set k = (A . i) gcd (B . i);
Q1: A . (i + 1) = B . i by AS;
Q2: B . (i + 1) = (A . i) mod (B . i) by AS;
P1: (A . i) gcd (B . i) divides A . (i + 1) by Q1, INT_2:def_2;
P2: (A . i) gcd (B . i) divides B . (i + 1)
proof
X1: B . (i + 1) = (A . i) - (((A . i) div (B . i)) * (B . i)) by INT_1:def_10, Q2, AS1;
X2: (A . i) gcd (B . i) divides A . i by INT_2:def_2;
X3: (A . i) gcd (B . i) divides B . i by INT_2:def_2;
X4: ex s being Integer st A . i = ((A . i) gcd (B . i)) * s by X2, INT_1:def_3;
ex t being Integer st B . i = ((A . i) gcd (B . i)) * t by X3, INT_1:def_3;
then consider s, t being Integer such that
X5: B . (i + 1) = (((A . i) gcd (B . i)) * s) - (((A . i) div (B . i)) * (((A . i) gcd (B . i)) * t)) by X1, X4;
B . (i + 1) = (s - (((A . i) div (B . i)) * t)) * ((A . i) gcd (B . i)) by X5;
hence (A . i) gcd (B . i) divides B . (i + 1) by INT_1:def_3; ::_thesis: verum
end;
for m being Integer st m divides A . (i + 1) & m divides B . (i + 1) holds
m divides (A . i) gcd (B . i)
proof
let m be Integer; ::_thesis: ( m divides A . (i + 1) & m divides B . (i + 1) implies m divides (A . i) gcd (B . i) )
assume P3: ( m divides A . (i + 1) & m divides B . (i + 1) ) ; ::_thesis: m divides (A . i) gcd (B . i)
then P31: m divides B . i by AS;
P32: m divides A . i
proof
B . (i + 1) = (A . i) - (((A . i) div (B . i)) * (B . i)) by INT_1:def_10, Q2, AS1;
then X1: A . i = (B . (i + 1)) + (((A . i) div (B . i)) * (B . i)) ;
X21: ex s being Integer st B . i = m * s by INT_1:def_3, P31;
X22: ex t being Integer st B . (i + 1) = m * t by INT_1:def_3, P3;
consider s, t being Integer such that
X4: A . i = (m * s) + (((A . i) div (B . i)) * (m * t)) by X1, X21, X22;
A . i = m * (s + (((A . i) div (B . i)) * t)) by X4;
hence m divides A . i by INT_1:def_3; ::_thesis: verum
end;
thus m divides (A . i) gcd (B . i) by P31, P32, INT_2:def_2; ::_thesis: verum
end;
hence (A . (i + 1)) gcd (B . (i + 1)) = (A . i) gcd (B . i) by P1, P2, INT_2:def_2; ::_thesis: verum
end;
LM4G: for a, b being Element of INT
for A, B being sequence of INT st A . 0 = a & B . 0 = b & ( for i being Element of NAT holds
( A . (i + 1) = B . i & B . (i + 1) = (A . i) mod (B . i) ) ) holds
for i being Element of NAT st B . i <> 0 holds
(A . 0) gcd (B . 0) = (A . i) gcd (B . i)
proof
let a, b be Element of INT ; ::_thesis: for A, B being sequence of INT st A . 0 = a & B . 0 = b & ( for i being Element of NAT holds
( A . (i + 1) = B . i & B . (i + 1) = (A . i) mod (B . i) ) ) holds
for i being Element of NAT st B . i <> 0 holds
(A . 0) gcd (B . 0) = (A . i) gcd (B . i)
let A, B be sequence of INT; ::_thesis: ( A . 0 = a & B . 0 = b & ( for i being Element of NAT holds
( A . (i + 1) = B . i & B . (i + 1) = (A . i) mod (B . i) ) ) implies for i being Element of NAT st B . i <> 0 holds
(A . 0) gcd (B . 0) = (A . i) gcd (B . i) )
assume AS1: ( A . 0 = a & B . 0 = b & ( for i being Element of NAT holds
( A . (i + 1) = B . i & B . (i + 1) = (A . i) mod (B . i) ) ) ) ; ::_thesis: for i being Element of NAT st B . i <> 0 holds
(A . 0) gcd (B . 0) = (A . i) gcd (B . i)
defpred S1[ Nat] means ( B . $1 <> 0 implies (A . 0) gcd (B . 0) = (A . $1) gcd (B . $1) );
P0: S1[ 0 ] ;
PN: for i being Element of NAT st S1[i] holds
S1[i + 1]
proof
let i be Element of NAT ; ::_thesis: ( S1[i] implies S1[i + 1] )
assume PN1: S1[i] ; ::_thesis: S1[i + 1]
( B . (i + 1) <> 0 implies (A . 0) gcd (B . 0) = (A . (i + 1)) gcd (B . (i + 1)) )
proof
assume PN2: B . (i + 1) <> 0 ; ::_thesis: (A . 0) gcd (B . 0) = (A . (i + 1)) gcd (B . (i + 1))
B . i <> 0
proof
assume PN4: B . i = 0 ; ::_thesis: contradiction
B . (i + 1) = (A . i) mod (B . i) by AS1;
hence contradiction by PN2, PN4, INT_1:def_10; ::_thesis: verum
end;
hence (A . 0) gcd (B . 0) = (A . (i + 1)) gcd (B . (i + 1)) by PN1, AS1, LM3G; ::_thesis: verum
end;
hence S1[i + 1] ; ::_thesis: verum
end;
for i being Element of NAT holds S1[i] from NAT_1:sch_1(P0, PN);
hence for i being Element of NAT st B . i <> 0 holds
(A . 0) gcd (B . 0) = (A . i) gcd (B . i) ; ::_thesis: verum
end;
theorem INT157A: :: NTALGO_1:3
for i2, i1 being Integer st i2 <= 0 holds
i1 mod i2 <= 0
proof
let i2, i1 be Integer; ::_thesis: ( i2 <= 0 implies i1 mod i2 <= 0 )
assume A1: i2 <= 0 ; ::_thesis: i1 mod i2 <= 0
percases ( i2 < 0 or i2 = 0 ) by A1;
supposeA2: i2 < 0 ; ::_thesis: i1 mod 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; ::_thesis: verum
end;
suppose i2 = 0 ; ::_thesis: i1 mod i2 <= 0
hence i1 mod i2 <= 0 by INT_1:def_10; ::_thesis: verum
end;
end;
end;
theorem INT158A: :: NTALGO_1:4
for i2, i1 being Integer st i2 < 0 holds
- (i1 mod i2) < - i2
proof
let i2, i1 be Integer; ::_thesis: ( i2 < 0 implies - (i1 mod i2) < - i2 )
assume A1: i2 < 0 ; ::_thesis: - (i1 mod i2) < - i2
(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; ::_thesis: verum
end;
theorem LM5G1: :: NTALGO_1:5
for x, y being Element of INT st abs y <> 0 holds
abs (x mod y) < abs y
proof
let x, y be Element of INT ; ::_thesis: ( abs y <> 0 implies abs (x mod y) < abs y )
assume A1: abs y <> 0 ; ::_thesis: abs (x mod y) < abs y
percases ( 0 < y or y <= 0 ) ;
supposeC1: 0 < y ; ::_thesis: abs (x mod y) < abs y
then C2: x mod y < y by INT_1:58;
0 <= x mod y by INT_1:57, C1;
then C3: abs (x mod y) < y by ABSVALUE:def_1, C2;
y <= abs y by ABSVALUE:4;
hence abs (x mod y) < abs y by C3, XXREAL_0:2; ::_thesis: verum
end;
supposeC4: y <= 0 ; ::_thesis: abs (x mod y) < abs y
C40P: y <> 0 by ABSVALUE:2, A1;
C41: - (x mod y) < - y by INT158A, C40P, C4;
XX1: x mod y <= 0 by C4, INT157A;
C42: abs (x mod y) = - (x mod y)
proof
percases ( x mod y = 0 or x mod y <> 0 ) ;
suppose x mod y = 0 ; ::_thesis: abs (x mod y) = - (x mod y)
hence abs (x mod y) = - (x mod y) by ABSVALUE:2; ::_thesis: verum
end;
suppose x mod y <> 0 ; ::_thesis: abs (x mod y) = - (x mod y)
hence abs (x mod y) = - (x mod y) by ABSVALUE:def_1, XX1; ::_thesis: verum
end;
end;
end;
thus abs (x mod y) < abs y by C42, C41, C40P, C4, ABSVALUE:def_1; ::_thesis: verum
end;
end;
end;
LM5G: for a, b being Element of INT
for A, B being sequence of INT st A . 0 = a & B . 0 = b & ( for i being Element of NAT holds
( A . (i + 1) = B . i & B . (i + 1) = (A . i) mod (B . i) ) ) holds
{ i where i is Element of NAT : B . i = 0 } is non empty Subset of NAT
proof
let a, b be Element of INT ; ::_thesis: for A, B being sequence of INT st A . 0 = a & B . 0 = b & ( for i being Element of NAT holds
( A . (i + 1) = B . i & B . (i + 1) = (A . i) mod (B . i) ) ) holds
{ i where i is Element of NAT : B . i = 0 } is non empty Subset of NAT
let A, B be sequence of INT; ::_thesis: ( A . 0 = a & B . 0 = b & ( for i being Element of NAT holds
( A . (i + 1) = B . i & B . (i + 1) = (A . i) mod (B . i) ) ) implies { i where i is Element of NAT : B . i = 0 } is non empty Subset of NAT )
assume AS1: ( A . 0 = a & B . 0 = b & ( for i being Element of NAT holds
( A . (i + 1) = B . i & B . (i + 1) = (A . i) mod (B . i) ) ) ) ; ::_thesis: { i where i is Element of NAT : B . i = 0 } is non empty Subset of NAT
LMM: for x being set st x in { i where i is Element of NAT : B . i = 0 } holds
x in NAT
proof
let x be set ; ::_thesis: ( x in { i where i is Element of NAT : B . i = 0 } implies x in NAT )
assume x in { i where i is Element of NAT : B . i = 0 } ; ::_thesis: x in NAT
then ex i being Element of NAT st
( x = i & B . i = 0 ) ;
hence x in NAT ; ::_thesis: verum
end;
ex m0 being Element of NAT st B . m0 = 0
proof
assume A20: for m0 being Element of NAT holds not B . m0 = 0 ; ::_thesis: contradiction
A2: for m0 being Element of NAT holds abs (B . m0) <> 0
proof
let m0 be Element of NAT ; ::_thesis: abs (B . m0) <> 0
B . m0 <> 0 by A20;
hence abs (B . m0) <> 0 by ABSVALUE:2; ::_thesis: verum
end;
A3: for i being Element of NAT holds abs (B . (i + 1)) <= (abs (B . i)) - 1
proof
let i be Element of NAT ; ::_thesis: abs (B . (i + 1)) <= (abs (B . i)) - 1
abs (B . (i + 1)) = abs ((A . i) mod (B . i)) by AS1;
then abs (B . (i + 1)) < abs (B . i) by A2, LM5G1;
then (abs (B . (i + 1))) + 1 <= abs (B . i) by NAT_1:13;
then ((abs (B . (i + 1))) + 1) - 1 <= (abs (B . i)) - 1 by XREAL_1:9;
hence abs (B . (i + 1)) <= (abs (B . i)) - 1 ; ::_thesis: verum
end;
defpred S1[ Nat] means abs (B . $1) <= (abs (B . 0)) - $1;
P0: S1[ 0 ] ;
P1: for i being Element of NAT st S1[i] holds
S1[i + 1]
proof
let i be Element of NAT ; ::_thesis: ( S1[i] implies S1[i + 1] )
assume P11: S1[i] ; ::_thesis: S1[i + 1]
P12: abs (B . (i + 1)) <= (abs (B . i)) - 1 by A3;
(abs (B . i)) - 1 <= ((abs (B . 0)) - i) - 1 by P11, XREAL_1:9;
hence S1[i + 1] by XXREAL_0:2, P12; ::_thesis: verum
end;
A4: for i being Element of NAT holds S1[i] from NAT_1:sch_1(P0, P1);
abs (B . (abs (B . 0))) <= (abs (B . 0)) - (abs (B . 0)) by A4;
hence contradiction by A2, NAT_1:14; ::_thesis: verum
end;
then consider m0 being Element of NAT such that
X1: B . m0 = 0 ;
m0 in { i where i is Element of NAT : B . i = 0 } by X1;
hence { i where i is Element of NAT : B . i = 0 } is non empty Subset of NAT by LMM, TARSKI:def_3; ::_thesis: verum
end;
LM6G: for a being Element of INT holds a gcd 0 = abs a
by WSIERP_1:8;
LM7G: for x, y being Element of INT
for g, w, q, t, a, b, v, u being sequence of INT st a . 0 = 1 & b . 0 = 0 & g . 0 = x & q . 0 = 0 & u . 0 = 0 & v . 0 = 1 & w . 0 = y & t . 0 = 0 & ( for i being Element of NAT holds
( q . (i + 1) = (g . i) div (w . i) & t . (i + 1) = (g . i) mod (w . i) & a . (i + 1) = u . i & b . (i + 1) = v . i & g . (i + 1) = w . i & u . (i + 1) = (a . i) - ((q . (i + 1)) * (u . i)) & v . (i + 1) = (b . i) - ((q . (i + 1)) * (v . i)) & w . (i + 1) = t . (i + 1) ) ) holds
for i being Element of NAT st w . i <> 0 holds
((a . (i + 1)) * x) + ((b . (i + 1)) * y) = g . (i + 1)
proof
let x, y be Element of INT ; ::_thesis: for g, w, q, t, a, b, v, u being sequence of INT st a . 0 = 1 & b . 0 = 0 & g . 0 = x & q . 0 = 0 & u . 0 = 0 & v . 0 = 1 & w . 0 = y & t . 0 = 0 & ( for i being Element of NAT holds
( q . (i + 1) = (g . i) div (w . i) & t . (i + 1) = (g . i) mod (w . i) & a . (i + 1) = u . i & b . (i + 1) = v . i & g . (i + 1) = w . i & u . (i + 1) = (a . i) - ((q . (i + 1)) * (u . i)) & v . (i + 1) = (b . i) - ((q . (i + 1)) * (v . i)) & w . (i + 1) = t . (i + 1) ) ) holds
for i being Element of NAT st w . i <> 0 holds
((a . (i + 1)) * x) + ((b . (i + 1)) * y) = g . (i + 1)
let g, w, q, t be sequence of INT; ::_thesis: for a, b, v, u being sequence of INT st a . 0 = 1 & b . 0 = 0 & g . 0 = x & q . 0 = 0 & u . 0 = 0 & v . 0 = 1 & w . 0 = y & t . 0 = 0 & ( for i being Element of NAT holds
( q . (i + 1) = (g . i) div (w . i) & t . (i + 1) = (g . i) mod (w . i) & a . (i + 1) = u . i & b . (i + 1) = v . i & g . (i + 1) = w . i & u . (i + 1) = (a . i) - ((q . (i + 1)) * (u . i)) & v . (i + 1) = (b . i) - ((q . (i + 1)) * (v . i)) & w . (i + 1) = t . (i + 1) ) ) holds
for i being Element of NAT st w . i <> 0 holds
((a . (i + 1)) * x) + ((b . (i + 1)) * y) = g . (i + 1)
let a, b, v, u be sequence of INT; ::_thesis: ( a . 0 = 1 & b . 0 = 0 & g . 0 = x & q . 0 = 0 & u . 0 = 0 & v . 0 = 1 & w . 0 = y & t . 0 = 0 & ( for i being Element of NAT holds
( q . (i + 1) = (g . i) div (w . i) & t . (i + 1) = (g . i) mod (w . i) & a . (i + 1) = u . i & b . (i + 1) = v . i & g . (i + 1) = w . i & u . (i + 1) = (a . i) - ((q . (i + 1)) * (u . i)) & v . (i + 1) = (b . i) - ((q . (i + 1)) * (v . i)) & w . (i + 1) = t . (i + 1) ) ) implies for i being Element of NAT st w . i <> 0 holds
((a . (i + 1)) * x) + ((b . (i + 1)) * y) = g . (i + 1) )
assume AS: ( a . 0 = 1 & b . 0 = 0 & g . 0 = x & q . 0 = 0 & u . 0 = 0 & v . 0 = 1 & w . 0 = y & t . 0 = 0 & ( for i being Element of NAT holds
( q . (i + 1) = (g . i) div (w . i) & t . (i + 1) = (g . i) mod (w . i) & a . (i + 1) = u . i & b . (i + 1) = v . i & g . (i + 1) = w . i & u . (i + 1) = (a . i) - ((q . (i + 1)) * (u . i)) & v . (i + 1) = (b . i) - ((q . (i + 1)) * (v . i)) & w . (i + 1) = t . (i + 1) ) ) ) ; ::_thesis: for i being Element of NAT st w . i <> 0 holds
((a . (i + 1)) * x) + ((b . (i + 1)) * y) = g . (i + 1)
defpred S1[ 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) ) );
P0: S1[ 0 ]
proof
assume w . 0 <> 0 ; ::_thesis: ( ((a . 0) * x) + ((b . 0) * y) = g . 0 & ((a . (0 + 1)) * x) + ((b . (0 + 1)) * y) = g . (0 + 1) )
reconsider I0 = 0 as Element of NAT ;
((a . (I0 + 1)) * x) + ((b . (I0 + 1)) * y) = ((u . 0) * x) + ((b . (I0 + 1)) * y) by AS
.= (0 * x) + (1 * y) by AS
.= g . (I0 + 1) by AS ;
hence ( ((a . 0) * x) + ((b . 0) * y) = g . 0 & ((a . (0 + 1)) * x) + ((b . (0 + 1)) * y) = g . (0 + 1) ) by AS; ::_thesis: verum
end;
P1: for i being Element of NAT st S1[i] holds
S1[i + 1]
proof
let i be Element of NAT ; ::_thesis: ( S1[i] implies S1[i + 1] )
assume P12A: S1[i] ; ::_thesis: S1[i + 1]
assume ASX: w . (i + 1) <> 0 ; ::_thesis: ( ((a . (i + 1)) * x) + ((b . (i + 1)) * y) = g . (i + 1) & ((a . ((i + 1) + 1)) * x) + ((b . ((i + 1) + 1)) * y) = g . ((i + 1) + 1) )
XX1: w . i <> 0
proof
assume XX2: w . i = 0 ; ::_thesis: contradiction
t . (i + 1) = (g . i) mod (w . i) by AS
.= 0 by XX2, INT_1:def_10 ;
hence contradiction by AS, ASX; ::_thesis: verum
end;
((a . ((i + 1) + 1)) * x) + ((b . ((i + 1) + 1)) * y) = ((u . (i + 1)) * x) + ((b . ((i + 1) + 1)) * y) by AS
.= ((u . (i + 1)) * x) + ((v . (i + 1)) * y) by AS
.= (((a . i) - ((q . (i + 1)) * (u . i))) * x) + ((v . (i + 1)) * y) by AS
.= (((a . i) - ((q . (i + 1)) * (u . i))) * x) + (((b . i) - ((q . (i + 1)) * (v . i))) * y) by AS
.= (g . i) - ((q . (i + 1)) * (((u . i) * x) + ((v . i) * y))) by XX1, P12A
.= (g . i) - ((q . (i + 1)) * (((a . (i + 1)) * x) + ((v . i) * y))) by AS
.= (g . i) - ((q . (i + 1)) * (g . (i + 1))) by XX1, P12A, AS
.= (g . i) - (((g . i) div (w . i)) * (g . (i + 1))) by AS
.= (g . i) - (((g . i) div (w . i)) * (w . i)) by AS
.= (g . i) mod (w . i) by INT_1:def_10, XX1
.= t . (i + 1) by AS
.= w . (i + 1) by AS
.= g . ((i + 1) + 1) by AS ;
hence ( ((a . (i + 1)) * x) + ((b . (i + 1)) * y) = g . (i + 1) & ((a . ((i + 1) + 1)) * x) + ((b . ((i + 1) + 1)) * y) = g . ((i + 1) + 1) ) by XX1, P12A; ::_thesis: verum
end;
for i being Element of NAT holds S1[i] from NAT_1:sch_1(P0, P1);
hence for i being Element of NAT st w . i <> 0 holds
((a . (i + 1)) * x) + ((b . (i + 1)) * y) = g . (i + 1) ; ::_thesis: verum
end;
theorem Th2: :: NTALGO_1:6
for x, y being Element of INT holds
( (ALGO_EXGCD (x,y)) `3_3 = x gcd y & (((ALGO_EXGCD (x,y)) `1_3) * x) + (((ALGO_EXGCD (x,y)) `2_3) * y) = x gcd y )
proof
let x, y be Element of INT ; ::_thesis: ( (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 )
consider g, w, q, t, a, b, v, u being sequence of INT, istop being Element of NAT such that
P0: ( a . 0 = 1 & b . 0 = 0 & g . 0 = x & q . 0 = 0 & u . 0 = 0 & v . 0 = 1 & w . 0 = y & t . 0 = 0 & ( for i being Element of NAT holds
( q . (i + 1) = (g . i) div (w . i) & t . (i + 1) = (g . i) mod (w . i) & a . (i + 1) = u . i & b . (i + 1) = v . i & g . (i + 1) = w . i & u . (i + 1) = (a . i) - ((q . (i + 1)) * (u . i)) & v . (i + 1) = (b . i) - ((q . (i + 1)) * (v . i)) & w . (i + 1) = t . (i + 1) ) ) & istop = min* { i where i is Element of NAT : w . i = 0 } & ( 0 <= g . istop implies 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 defALGOEXGCD;
P2X: now__::_thesis:_for_i_being_Element_of_NAT_holds_
(_g_._(i_+_1)_=_w_._i_&_w_._(i_+_1)_=_(g_._i)_mod_(w_._i)_)
let i be Element of NAT ; ::_thesis: ( g . (i + 1) = w . i & w . (i + 1) = (g . i) mod (w . i) )
thus g . (i + 1) = w . i by P0; ::_thesis: w . (i + 1) = (g . i) mod (w . i)
thus w . (i + 1) = t . (i + 1) by P0
.= (g . i) mod (w . i) by P0 ; ::_thesis: verum
end;
X0: { i where i is Element of NAT : w . i = 0 } is non empty Subset of NAT by P0, P2X, LM5G;
then istop in { i where i is Element of NAT : w . i = 0 } by P0, NAT_1:def_1;
then P4: ex i being Element of NAT st
( istop = i & w . i = 0 ) ;
XX3: (ALGO_EXGCD (x,y)) `3_3 = abs (g . istop)
proof
percases ( 0 <= g . istop or g . istop < 0 ) ;
suppose 0 <= g . istop ; ::_thesis: (ALGO_EXGCD (x,y)) `3_3 = abs (g . istop)
then abs (g . istop) = g . istop by ABSVALUE:def_1;
hence (ALGO_EXGCD (x,y)) `3_3 = abs (g . istop) by P0, MCART_1:def_7; ::_thesis: verum
end;
supposeXX32: g . istop < 0 ; ::_thesis: (ALGO_EXGCD (x,y)) `3_3 = abs (g . istop)
then abs (g . istop) = - (g . istop) by ABSVALUE:def_1;
hence (ALGO_EXGCD (x,y)) `3_3 = abs (g . istop) by P0, XX32, MCART_1:def_7; ::_thesis: verum
end;
end;
end;
percases ( istop = 0 or istop <> 0 ) ;
supposeC1: istop = 0 ; ::_thesis: ( (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 )
thus R1: (ALGO_EXGCD (x,y)) `3_3 = x gcd y by P0, P4, LM6G, XX3, C1; ::_thesis: (((ALGO_EXGCD (x,y)) `1_3) * x) + (((ALGO_EXGCD (x,y)) `2_3) * y) = x gcd y
thus (((ALGO_EXGCD (x,y)) `1_3) * x) + (((ALGO_EXGCD (x,y)) `2_3) * y) = x gcd y ::_thesis: verum
proof
percases ( 0 <= g . istop or g . istop < 0 ) ;
supposeY11: 0 <= g . istop ; ::_thesis: (((ALGO_EXGCD (x,y)) `1_3) * x) + (((ALGO_EXGCD (x,y)) `2_3) * y) = x gcd y
Y13: (ALGO_EXGCD (x,y)) `1_3 = 1 by C1, P0, Y11, MCART_1:def_5;
(ALGO_EXGCD (x,y)) `2_3 = 0 by C1, P0, MCART_1:def_6;
hence (((ALGO_EXGCD (x,y)) `1_3) * x) + (((ALGO_EXGCD (x,y)) `2_3) * y) = x gcd y by Y11, P0, C1, XX3, ABSVALUE:def_1, Y13, R1; ::_thesis: verum
end;
supposeXX32: g . istop < 0 ; ::_thesis: (((ALGO_EXGCD (x,y)) `1_3) * x) + (((ALGO_EXGCD (x,y)) `2_3) * y) = x gcd y
Y13: (ALGO_EXGCD (x,y)) `1_3 = - 1 by C1, P0, XX32, MCART_1:def_5;
(ALGO_EXGCD (x,y)) `2_3 = 0 by P0, C1, MCART_1:def_6;
hence (((ALGO_EXGCD (x,y)) `1_3) * x) + (((ALGO_EXGCD (x,y)) `2_3) * y) = x gcd y by P0, C1, XX3, ABSVALUE:def_1, XX32, Y13, R1; ::_thesis: verum
end;
end;
end;
end;
suppose istop <> 0 ; ::_thesis: ( (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 )
then 1 <= istop by NAT_1:14;
then 1 - 1 <= istop - 1 by XREAL_1:9;
then reconsider m1 = istop - 1 as Element of NAT by INT_1:3;
X1: w . m1 <> 0
proof
assume w . m1 = 0 ; ::_thesis: contradiction
then X11: m1 in { i where i is Element of NAT : w . i = 0 } ;
istop - 1 < istop - 0 by XREAL_1:15;
hence contradiction by X11, P0, X0, NAT_1:def_1; ::_thesis: verum
end;
P5: (g . m1) gcd (w . m1) = (g . (m1 + 1)) gcd (w . (m1 + 1)) by LM3G, P0, X1, P2X;
R1: (g . istop) gcd (w . istop) = (ALGO_EXGCD (x,y)) `3_3 by XX3, LM6G, P4;
hence RR1: (ALGO_EXGCD (x,y)) `3_3 = x gcd y by P5, X1, P2X, LM4G, P0; ::_thesis: (((ALGO_EXGCD (x,y)) `1_3) * x) + (((ALGO_EXGCD (x,y)) `2_3) * y) = x gcd y
Y1: ((a . (m1 + 1)) * x) + ((b . (m1 + 1)) * y) = g . (m1 + 1) by X1, LM7G, P0;
thus (((ALGO_EXGCD (x,y)) `1_3) * x) + (((ALGO_EXGCD (x,y)) `2_3) * y) = x gcd y ::_thesis: verum
proof
percases ( 0 <= g . istop or g . istop < 0 ) ;
supposeY11: 0 <= g . istop ; ::_thesis: (((ALGO_EXGCD (x,y)) `1_3) * x) + (((ALGO_EXGCD (x,y)) `2_3) * y) = x gcd y
then Y12: (ALGO_EXGCD (x,y)) `3_3 = g . istop by XX3, ABSVALUE:def_1;
(ALGO_EXGCD (x,y)) `1_3 = a . istop by P0, Y11, MCART_1:def_5;
hence (((ALGO_EXGCD (x,y)) `1_3) * x) + (((ALGO_EXGCD (x,y)) `2_3) * y) = x gcd y by RR1, Y1, Y12, P0, MCART_1:def_6; ::_thesis: verum
end;
supposeXX32: g . istop < 0 ; ::_thesis: (((ALGO_EXGCD (x,y)) `1_3) * x) + (((ALGO_EXGCD (x,y)) `2_3) * y) = x gcd y
then Y12: (ALGO_EXGCD (x,y)) `3_3 = - (g . istop) by XX3, ABSVALUE:def_1;
Y13: (ALGO_EXGCD (x,y)) `1_3 = - (a . istop) by P0, XX32, MCART_1:def_5;
(ALGO_EXGCD (x,y)) `2_3 = - (b . istop) by P0, XX32, MCART_1:def_6;
hence (((ALGO_EXGCD (x,y)) `1_3) * x) + (((ALGO_EXGCD (x,y)) `2_3) * y) = x gcd y by Y1, Y12, Y13, R1, P5, X1, P2X, LM4G, P0; ::_thesis: verum
end;
end;
end;
end;
end;
end;
definition
let x, p be Element of INT ;
func ALGO_INVERSE (x,p) -> Element of INT means :definverse: :: NTALGO_1:def 3
for y being Element of INT st y = x mod p holds
( ( (ALGO_EXGCD (p,y)) `3_3 = 1 implies ( ( (ALGO_EXGCD (p,y)) `2_3 < 0 implies ex z being Element of INT st
( z = (ALGO_EXGCD (p,y)) `2_3 & it = p + z ) ) & ( 0 <= (ALGO_EXGCD (p,y)) `2_3 implies it = (ALGO_EXGCD (p,y)) `2_3 ) ) ) & ( (ALGO_EXGCD (p,y)) `3_3 <> 1 implies it = {} ) );
existence
ex b1 being Element of INT st
for y being Element of INT st y = x mod p holds
( ( (ALGO_EXGCD (p,y)) `3_3 = 1 implies ( ( (ALGO_EXGCD (p,y)) `2_3 < 0 implies ex z being Element of INT st
( z = (ALGO_EXGCD (p,y)) `2_3 & b1 = p + z ) ) & ( 0 <= (ALGO_EXGCD (p,y)) `2_3 implies b1 = (ALGO_EXGCD (p,y)) `2_3 ) ) ) & ( (ALGO_EXGCD (p,y)) `3_3 <> 1 implies b1 = {} ) )
proof
reconsider y = x mod p as Element of INT by INT_1:def_2;
now__::_thesis:_ex_s_being_Element_of_INT_st_
(_(_(ALGO_EXGCD_(p,y))_`3_3_=_1_implies_(_(_(ALGO_EXGCD_(p,y))_`2_3_<_0_implies_ex_z_being_Element_of_INT_st_
(_z_=_(ALGO_EXGCD_(p,y))_`2_3_&_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_=_{}_)_)
percases ( (ALGO_EXGCD (p,y)) `3_3 = 1 or (ALGO_EXGCD (p,y)) `3_3 <> 1 ) ;
supposeC1: (ALGO_EXGCD (p,y)) `3_3 = 1 ; ::_thesis: ex s being Element of INT st
( ( (ALGO_EXGCD (p,y)) `3_3 = 1 implies ( ( (ALGO_EXGCD (p,y)) `2_3 < 0 implies ex z being Element of INT st
( z = (ALGO_EXGCD (p,y)) `2_3 & 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 = {} ) )
now__::_thesis:_ex_s_being_Element_of_INT_st_
(_(_(ALGO_EXGCD_(p,y))_`2_3_<_0_implies_ex_z_being_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_=_{}_)_)
percases ( (ALGO_EXGCD (p,y)) `2_3 < 0 or 0 <= (ALGO_EXGCD (p,y)) `2_3 ) ;
supposeC11: (ALGO_EXGCD (p,y)) `2_3 < 0 ; ::_thesis: ex s being Element of INT st
( ( (ALGO_EXGCD (p,y)) `2_3 < 0 implies ex z being 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 = {} ) )
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 being Element of INT st
( z = (ALGO_EXGCD (p,y)) `2_3 & s = p + z ) ;
hence ex s being Element of INT st
( ( (ALGO_EXGCD (p,y)) `2_3 < 0 implies ex z being 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 C11, C1; ::_thesis: verum
end;
supposeC12: 0 <= (ALGO_EXGCD (p,y)) `2_3 ; ::_thesis: ex s being Element of INT st
( ( (ALGO_EXGCD (p,y)) `2_3 < 0 implies ex z being 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 = {} ) )
reconsider s = (ALGO_EXGCD (p,y)) `2_3 as Element of INT ;
thus ex s being Element of INT st
( ( (ALGO_EXGCD (p,y)) `2_3 < 0 implies ex z being 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 C12, C1; ::_thesis: verum
end;
end;
end;
hence ex s being Element of INT st
( ( (ALGO_EXGCD (p,y)) `3_3 = 1 implies ( ( (ALGO_EXGCD (p,y)) `2_3 < 0 implies ex z being Element of INT st
( z = (ALGO_EXGCD (p,y)) `2_3 & 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 = {} ) ) ; ::_thesis: verum
end;
supposeC2: (ALGO_EXGCD (p,y)) `3_3 <> 1 ; ::_thesis: ex s being Element of INT st
( ( (ALGO_EXGCD (p,y)) `3_3 = 1 implies ( ( (ALGO_EXGCD (p,y)) `2_3 < 0 implies ex z being Element of INT st
( z = (ALGO_EXGCD (p,y)) `2_3 & 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 = {} ) )
reconsider s = {} as Element of INT by INT_1:def_2;
( (ALGO_EXGCD (p,y)) `3_3 <> 1 implies s = {} ) ;
hence ex s being Element of INT st
( ( (ALGO_EXGCD (p,y)) `3_3 = 1 implies ( ( (ALGO_EXGCD (p,y)) `2_3 < 0 implies ex z being Element of INT st
( z = (ALGO_EXGCD (p,y)) `2_3 & 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 C2; ::_thesis: verum
end;
end;
end;
then consider s being Element of INT such that
Q1: ( ( (ALGO_EXGCD (p,y)) `3_3 = 1 implies ( ( (ALGO_EXGCD (p,y)) `2_3 < 0 implies ex z being Element of INT st
( z = (ALGO_EXGCD (p,y)) `2_3 & 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 ; ::_thesis: for y being Element of INT st y = x mod p holds
( ( (ALGO_EXGCD (p,y)) `3_3 = 1 implies ( ( (ALGO_EXGCD (p,y)) `2_3 < 0 implies ex z being Element of INT st
( z = (ALGO_EXGCD (p,y)) `2_3 & 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 = {} ) )
thus for y being Element of INT st y = x mod p holds
( ( (ALGO_EXGCD (p,y)) `3_3 = 1 implies ( ( (ALGO_EXGCD (p,y)) `2_3 < 0 implies ex z being Element of INT st
( z = (ALGO_EXGCD (p,y)) `2_3 & 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 Q1; ::_thesis: verum
end;
uniqueness
for b1, b2 being Element of INT st ( for y being Element of INT st y = x mod p holds
( ( (ALGO_EXGCD (p,y)) `3_3 = 1 implies ( ( (ALGO_EXGCD (p,y)) `2_3 < 0 implies ex z being Element of INT st
( z = (ALGO_EXGCD (p,y)) `2_3 & b1 = p + z ) ) & ( 0 <= (ALGO_EXGCD (p,y)) `2_3 implies b1 = (ALGO_EXGCD (p,y)) `2_3 ) ) ) & ( (ALGO_EXGCD (p,y)) `3_3 <> 1 implies b1 = {} ) ) ) & ( for y being Element of INT st y = x mod p holds
( ( (ALGO_EXGCD (p,y)) `3_3 = 1 implies ( ( (ALGO_EXGCD (p,y)) `2_3 < 0 implies ex z being Element of INT st
( z = (ALGO_EXGCD (p,y)) `2_3 & b2 = p + z ) ) & ( 0 <= (ALGO_EXGCD (p,y)) `2_3 implies b2 = (ALGO_EXGCD (p,y)) `2_3 ) ) ) & ( (ALGO_EXGCD (p,y)) `3_3 <> 1 implies b2 = {} ) ) ) holds
b1 = b2
proof
let s1, s2 be Element of INT ; ::_thesis: ( ( for y being Element of INT st y = x mod p holds
( ( (ALGO_EXGCD (p,y)) `3_3 = 1 implies ( ( (ALGO_EXGCD (p,y)) `2_3 < 0 implies ex z being Element of INT st
( z = (ALGO_EXGCD (p,y)) `2_3 & 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 = {} ) ) ) & ( for y being Element of INT st y = x mod p holds
( ( (ALGO_EXGCD (p,y)) `3_3 = 1 implies ( ( (ALGO_EXGCD (p,y)) `2_3 < 0 implies ex z being Element of INT st
( z = (ALGO_EXGCD (p,y)) `2_3 & 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 = {} ) ) ) implies s1 = s2 )
assume A1: for y being Element of INT st y = x mod p holds
( ( (ALGO_EXGCD (p,y)) `3_3 = 1 implies ( ( (ALGO_EXGCD (p,y)) `2_3 < 0 implies ex z being Element of INT st
( z = (ALGO_EXGCD (p,y)) `2_3 & 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 = {} ) ) ; ::_thesis: ( ex y being Element of INT st
( y = x mod p & not ( ( (ALGO_EXGCD (p,y)) `3_3 = 1 implies ( ( (ALGO_EXGCD (p,y)) `2_3 < 0 implies ex z being Element of INT st
( z = (ALGO_EXGCD (p,y)) `2_3 & 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 = {} ) ) ) or s1 = s2 )
assume A2: for y being Element of INT st y = x mod p holds
( ( (ALGO_EXGCD (p,y)) `3_3 = 1 implies ( ( (ALGO_EXGCD (p,y)) `2_3 < 0 implies ex z being Element of INT st
( z = (ALGO_EXGCD (p,y)) `2_3 & 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 = {} ) ) ; ::_thesis: s1 = s2
reconsider y = x mod p as Element of INT by INT_1:def_2;
thus s1 = s2 ::_thesis: verum
proof
percases ( (ALGO_EXGCD (p,y)) `3_3 = 1 or (ALGO_EXGCD (p,y)) `3_3 <> 1 ) ;
supposeC1: (ALGO_EXGCD (p,y)) `3_3 = 1 ; ::_thesis: s1 = s2
thus s1 = s2 ::_thesis: verum
proof
percases ( (ALGO_EXGCD (p,y)) `2_3 < 0 or 0 <= (ALGO_EXGCD (p,y)) `2_3 ) ;
supposeC11: (ALGO_EXGCD (p,y)) `2_3 < 0 ; ::_thesis: s1 = s2
then C12: ex z being Element of INT st
( z = (ALGO_EXGCD (p,y)) `2_3 & s1 = p + z ) by A1, C1;
ex z being Element of INT st
( z = (ALGO_EXGCD (p,y)) `2_3 & s2 = p + z ) by A2, C1, C11;
hence s1 = s2 by C12; ::_thesis: verum
end;
supposeC12: 0 <= (ALGO_EXGCD (p,y)) `2_3 ; ::_thesis: s1 = s2
thus s1 = (ALGO_EXGCD (p,y)) `2_3 by C12, C1, A1
.= s2 by C12, C1, A2 ; ::_thesis: verum
end;
end;
end;
end;
supposeC2: (ALGO_EXGCD (p,y)) `3_3 <> 1 ; ::_thesis: s1 = s2
thus s1 = {} by A1, C2
.= s2 by A2, C2 ; ::_thesis: verum
end;
end;
end;
end;
end;
:: deftheorem definverse defines ALGO_INVERSE NTALGO_1:def_3_:_
for x, p, b3 being Element of INT holds
( b3 = ALGO_INVERSE (x,p) iff for y being Element of INT st y = x mod p holds
( ( (ALGO_EXGCD (p,y)) `3_3 = 1 implies ( ( (ALGO_EXGCD (p,y)) `2_3 < 0 implies ex z being Element of INT st
( z = (ALGO_EXGCD (p,y)) `2_3 & b3 = p + z ) ) & ( 0 <= (ALGO_EXGCD (p,y)) `2_3 implies b3 = (ALGO_EXGCD (p,y)) `2_3 ) ) ) & ( (ALGO_EXGCD (p,y)) `3_3 <> 1 implies b3 = {} ) ) );
LMTh30: for x, y, p being Element of INT st y = x mod p & (ALGO_EXGCD (p,y)) `3_3 = 1 & p <> 0 holds
((ALGO_INVERSE (x,p)) * x) mod p = 1 mod p
proof
let x, y, p be Element of INT ; ::_thesis: ( y = x mod p & (ALGO_EXGCD (p,y)) `3_3 = 1 & p <> 0 implies ((ALGO_INVERSE (x,p)) * x) mod p = 1 mod p )
assume AS: ( y = x mod p & (ALGO_EXGCD (p,y)) `3_3 = 1 & p <> 0 ) ; ::_thesis: ((ALGO_INVERSE (x,p)) * x) mod p = 1 mod p
P3P: ( (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 Th2;
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 ;
P40C2: p mod p = 0 by INT_1:50;
P4: (((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 INT_4:12, P40C2 ;
reconsider I0 = 0 as Element of INT by INT_1:def_2;
P6: ((((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 LMTh3, P4 ;
percases ( (ALGO_EXGCD (p,y)) `2_3 < 0 or 0 <= (ALGO_EXGCD (p,y)) `2_3 ) ;
suppose (ALGO_EXGCD (p,y)) `2_3 < 0 ; ::_thesis: ((ALGO_INVERSE (x,p)) * x) mod p = 1 mod p
then consider z being Element of INT such that
A11: ( z = (ALGO_EXGCD (p,y)) `2_3 & ALGO_INVERSE (x,p) = p + z ) by definverse, AS;
thus ((ALGO_INVERSE (x,p)) * x) mod p = ((p * x) + (z * x)) mod p by A11
.= (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 LMTh3
.= 1 mod p by P6, A11, P3P, AS, NAT_D:67 ; ::_thesis: verum
end;
suppose 0 <= (ALGO_EXGCD (p,y)) `2_3 ; ::_thesis: ((ALGO_INVERSE (x,p)) * x) mod p = 1 mod p
hence ((ALGO_INVERSE (x,p)) * x) mod p = (((ALGO_EXGCD (p,y)) `2_3) * x) mod p by definverse, AS
.= ((s3 mod p) * (x mod p)) mod p by NAT_D:67
.= ((s3 mod p) * ((x mod p) mod p)) mod p by LMTh3
.= 1 mod p by P6, P3P, AS, NAT_D:67 ;
::_thesis: verum
end;
end;
end;
theorem Th3: :: NTALGO_1:7
for x, p, y being Element of INT st y = x mod p & (ALGO_EXGCD (p,y)) `3_3 = 1 holds
((ALGO_INVERSE (x,p)) * x) mod p = 1 mod p
proof
let x, p, y be Element of INT ; ::_thesis: ( y = x mod p & (ALGO_EXGCD (p,y)) `3_3 = 1 implies ((ALGO_INVERSE (x,p)) * x) mod p = 1 mod p )
assume AS: ( y = x mod p & (ALGO_EXGCD (p,y)) `3_3 = 1 ) ; ::_thesis: ((ALGO_INVERSE (x,p)) * x) mod p = 1 mod p
percases ( p = 0 or p <> 0 ) ;
supposeC1: p = 0 ; ::_thesis: ((ALGO_INVERSE (x,p)) * x) mod p = 1 mod p
thus ((ALGO_INVERSE (x,p)) * x) mod p = 0 by C1, INT_1:def_10
.= 1 mod p by C1, INT_1:def_10 ; ::_thesis: verum
end;
suppose p <> 0 ; ::_thesis: ((ALGO_INVERSE (x,p)) * x) mod p = 1 mod p
hence ((ALGO_INVERSE (x,p)) * x) mod p = 1 mod p by LMTh30, AS; ::_thesis: verum
end;
end;
end;
begin
definition
let nlist be non empty FinSequence of [:INT,INT:];
func ALGO_CRT nlist -> Element of INT means :defALGOCRT: :: NTALGO_1:def 4
( ( len nlist = 1 implies it = (nlist . 1) `1 ) & ( len nlist <> 1 implies ex m, n, prodc, prodi being FinSequence of INT ex M0, M being Element of INT st
( len m = len nlist & len n = len nlist & len prodc = (len nlist) - 1 & len prodi = (len nlist) - 1 & m . 1 = 1 & ( for i being Nat st 1 <= i & i <= (len m) - 1 holds
ex d, x, y being Element of INT st
( x = (nlist . i) `2 & m . (i + 1) = (m . i) * x & y = m . (i + 1) & d = (nlist . (i + 1)) `2 & prodi . i = ALGO_INVERSE (y,d) & prodc . i = y ) ) & M0 = (nlist . (len m)) `2 & M = (prodc . ((len m) - 1)) * M0 & n . 1 = (nlist . 1) `1 & ( for i being Nat st 1 <= i & i <= (len m) - 1 holds
ex u, u0, u1 being Element of INT st
( u0 = (nlist . (i + 1)) `1 & u1 = (nlist . (i + 1)) `2 & u = ((u0 - (n . i)) * (prodi . i)) mod u1 & n . (i + 1) = (n . i) + (u * (prodc . i)) ) ) & it = (n . (len m)) mod M ) ) );
existence
ex b1 being Element of INT st
( ( len nlist = 1 implies b1 = (nlist . 1) `1 ) & ( len nlist <> 1 implies ex m, n, prodc, prodi being FinSequence of INT ex M0, M being Element of INT st
( len m = len nlist & len n = len nlist & len prodc = (len nlist) - 1 & len prodi = (len nlist) - 1 & m . 1 = 1 & ( for i being Nat st 1 <= i & i <= (len m) - 1 holds
ex d, x, y being Element of INT st
( x = (nlist . i) `2 & m . (i + 1) = (m . i) * x & y = m . (i + 1) & d = (nlist . (i + 1)) `2 & prodi . i = ALGO_INVERSE (y,d) & prodc . i = y ) ) & M0 = (nlist . (len m)) `2 & M = (prodc . ((len m) - 1)) * M0 & n . 1 = (nlist . 1) `1 & ( for i being Nat st 1 <= i & i <= (len m) - 1 holds
ex u, u0, u1 being Element of INT st
( u0 = (nlist . (i + 1)) `1 & u1 = (nlist . (i + 1)) `2 & u = ((u0 - (n . i)) * (prodi . i)) mod u1 & n . (i + 1) = (n . i) + (u * (prodc . i)) ) ) & b1 = (n . (len m)) mod M ) ) )
proof
percases ( len nlist = 1 or len nlist <> 1 ) ;
supposeA1: len nlist = 1 ; ::_thesis: ex b1 being Element of INT st
( ( len nlist = 1 implies b1 = (nlist . 1) `1 ) & ( len nlist <> 1 implies ex m, n, prodc, prodi being FinSequence of INT ex M0, M being Element of INT st
( len m = len nlist & len n = len nlist & len prodc = (len nlist) - 1 & len prodi = (len nlist) - 1 & m . 1 = 1 & ( for i being Nat st 1 <= i & i <= (len m) - 1 holds
ex d, x, y being Element of INT st
( x = (nlist . i) `2 & m . (i + 1) = (m . i) * x & y = m . (i + 1) & d = (nlist . (i + 1)) `2 & prodi . i = ALGO_INVERSE (y,d) & prodc . i = y ) ) & M0 = (nlist . (len m)) `2 & M = (prodc . ((len m) - 1)) * M0 & n . 1 = (nlist . 1) `1 & ( for i being Nat st 1 <= i & i <= (len m) - 1 holds
ex u, u0, u1 being Element of INT st
( u0 = (nlist . (i + 1)) `1 & u1 = (nlist . (i + 1)) `2 & u = ((u0 - (n . i)) * (prodi . i)) mod u1 & n . (i + 1) = (n . i) + (u * (prodc . i)) ) ) & b1 = (n . (len m)) mod M ) ) )
then 1 in Seg (len nlist) ;
then 1 in dom nlist by FINSEQ_1:def_3;
then nlist . 1 in [:INT,INT:] by FINSEQ_2:11;
then (nlist . 1) `1 is Element of INT by MCART_1:10;
hence ex b1 being Element of INT st
( ( len nlist = 1 implies b1 = (nlist . 1) `1 ) & ( len nlist <> 1 implies ex m, n, prodc, prodi being FinSequence of INT ex M0, M being Element of INT st
( len m = len nlist & len n = len nlist & len prodc = (len nlist) - 1 & len prodi = (len nlist) - 1 & m . 1 = 1 & ( for i being Nat st 1 <= i & i <= (len m) - 1 holds
ex d, x, y being Element of INT st
( x = (nlist . i) `2 & m . (i + 1) = (m . i) * x & y = m . (i + 1) & d = (nlist . (i + 1)) `2 & prodi . i = ALGO_INVERSE (y,d) & prodc . i = y ) ) & M0 = (nlist . (len m)) `2 & M = (prodc . ((len m) - 1)) * M0 & n . 1 = (nlist . 1) `1 & ( for i being Nat st 1 <= i & i <= (len m) - 1 holds
ex u, u0, u1 being Element of INT st
( u0 = (nlist . (i + 1)) `1 & u1 = (nlist . (i + 1)) `2 & u = ((u0 - (n . i)) * (prodi . i)) mod u1 & n . (i + 1) = (n . i) + (u * (prodc . i)) ) ) & b1 = (n . (len m)) mod M ) ) ) by A1; ::_thesis: verum
end;
supposeA2: len nlist <> 1 ; ::_thesis: ex b1 being Element of INT st
( ( len nlist = 1 implies b1 = (nlist . 1) `1 ) & ( len nlist <> 1 implies ex m, n, prodc, prodi being FinSequence of INT ex M0, M being Element of INT st
( len m = len nlist & len n = len nlist & len prodc = (len nlist) - 1 & len prodi = (len nlist) - 1 & m . 1 = 1 & ( for i being Nat st 1 <= i & i <= (len m) - 1 holds
ex d, x, y being Element of INT st
( x = (nlist . i) `2 & m . (i + 1) = (m . i) * x & y = m . (i + 1) & d = (nlist . (i + 1)) `2 & prodi . i = ALGO_INVERSE (y,d) & prodc . i = y ) ) & M0 = (nlist . (len m)) `2 & M = (prodc . ((len m) - 1)) * M0 & n . 1 = (nlist . 1) `1 & ( for i being Nat st 1 <= i & i <= (len m) - 1 holds
ex u, u0, u1 being Element of INT st
( u0 = (nlist . (i + 1)) `1 & u1 = (nlist . (i + 1)) `2 & u = ((u0 - (n . i)) * (prodi . i)) mod u1 & n . (i + 1) = (n . i) + (u * (prodc . i)) ) ) & b1 = (n . (len m)) mod M ) ) )
defpred S1[ Nat, Integer, Integer] means ex x being Element of INT st
( x = (nlist . $1) `2 & $3 = $2 * x );
reconsider i1 = 1 as Element of INT by INT_1:def_1;
X1: for n being Element of NAT st 1 <= n & n < len nlist holds
for z being Element of INT ex y being Element of INT st S1[n,z,y]
proof
let n be Element of NAT ; ::_thesis: ( 1 <= n & n < len nlist implies for z being Element of INT ex y being Element of INT st S1[n,z,y] )
assume X11: ( 1 <= n & n < len nlist ) ; ::_thesis: for z being Element of INT ex y being Element of INT st S1[n,z,y]
let z be Element of INT ; ::_thesis: ex y being Element of INT st S1[n,z,y]
n in Seg (len nlist) by X11;
then n in dom nlist by FINSEQ_1:def_3;
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 ; ::_thesis: S1[n,z,y]
thus S1[n,z,y] ; ::_thesis: verum
end;
consider m being FinSequence of INT such that
X2: ( len m = len nlist & ( m . 1 = i1 or len nlist = 0 ) & ( for i being Element of NAT st 1 <= i & i < len nlist holds
S1[i,m . i,m . (i + 1)] ) ) from RECDEF_1:sch_4(X1);
II: (len m) - 1 < (len m) - 0 by XREAL_1:15;
X3: for i being Nat st 1 <= i & i <= (len m) - 1 holds
ex x being Element of INT st
( x = (nlist . i) `2 & m . (i + 1) = (m . i) * x )
proof
let i be Nat; ::_thesis: ( 1 <= i & i <= (len m) - 1 implies ex x being Element of INT st
( x = (nlist . i) `2 & m . (i + 1) = (m . i) * x ) )
assume ( 1 <= i & i <= (len m) - 1 ) ; ::_thesis: ex x being Element of INT st
( x = (nlist . i) `2 & m . (i + 1) = (m . i) * x )
then X32: ( 1 <= i & i < len nlist ) by X2, II, XXREAL_0:2;
i is Element of NAT by ORDINAL1:def_12;
hence ex x being Element of INT st
( x = (nlist . i) `2 & m . (i + 1) = (m . i) * x ) by X2, X32; ::_thesis: verum
end;
VV2: 1 <= len m by NAT_1:14, X2;
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 S2[ Nat, Integer] means ex d, x, y being 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) );
X4: for n being Nat st n in Seg lm holds
ex z being Element of INT st S2[n,z]
proof
let n be Nat; ::_thesis: ( n in Seg lm implies ex z being Element of INT st S2[n,z] )
assume X41: n in Seg lm ; ::_thesis: ex z being Element of INT st S2[n,z]
X43: ( 1 <= n & n <= (len m) - 1 ) by FINSEQ_1:1, X41;
then consider x being Element of INT such that
X42: ( x = (nlist . n) `2 & m . (n + 1) = (m . n) * x ) by X3;
reconsider y = m . (n + 1) as Element of INT by INT_1:def_2;
n + 1 <= ((len m) - 1) + 1 by X43, XREAL_1:6;
then ( 1 <= n + 1 & n + 1 <= len m ) by NAT_1:12;
then n + 1 in Seg (len nlist) by X2;
then n + 1 in dom nlist by FINSEQ_1:def_3;
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 ; ::_thesis: S2[n,w]
thus S2[n,w] by X42; ::_thesis: verum
end;
consider prodi being FinSequence of INT such that
X5: ( dom prodi = Seg lm & ( for k being Nat st k in Seg lm holds
S2[k,prodi . k] ) ) from FINSEQ_1:sch_5(X4);
X6: len prodi = (len nlist) - 1 by X2, FINSEQ_1:def_3, X5;
X7: for i being Nat st 1 <= i & i <= (len m) - 1 holds
ex d, x, y being Element of INT st
( x = (nlist . i) `2 & m . (i + 1) = (m . i) * x & y = m . (i + 1) & d = (nlist . (i + 1)) `2 & prodi . i = ALGO_INVERSE (y,d) )
proof
let i be Nat; ::_thesis: ( 1 <= i & i <= (len m) - 1 implies ex d, x, y being Element of INT st
( x = (nlist . i) `2 & m . (i + 1) = (m . i) * x & y = m . (i + 1) & d = (nlist . (i + 1)) `2 & prodi . i = ALGO_INVERSE (y,d) ) )
assume ( 1 <= i & i <= (len m) - 1 ) ; ::_thesis: ex d, x, y being Element of INT st
( x = (nlist . i) `2 & m . (i + 1) = (m . i) * x & y = m . (i + 1) & d = (nlist . (i + 1)) `2 & prodi . i = ALGO_INVERSE (y,d) )
then i in Seg lm by FINSEQ_1:1;
hence ex d, x, y being Element of INT st
( x = (nlist . i) `2 & m . (i + 1) = (m . i) * x & y = m . (i + 1) & d = (nlist . (i + 1)) `2 & prodi . i = ALGO_INVERSE (y,d) ) by X5; ::_thesis: verum
end;
defpred S3[ Nat, Integer] means ex d, x, y being 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 );
X8: for n being Nat st n in Seg lm holds
ex z being Element of INT st S3[n,z]
proof
let n be Nat; ::_thesis: ( n in Seg lm implies ex z being Element of INT st S3[n,z] )
assume X41: n in Seg lm ; ::_thesis: ex z being Element of INT st S3[n,z]
( 1 <= n & n <= (len m) - 1 ) by FINSEQ_1:1, X41;
then consider d, x, y being Element of INT such that
X42: ( 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 X7;
reconsider w = y as Element of INT ;
take w ; ::_thesis: S3[n,w]
thus S3[n,w] by X42; ::_thesis: verum
end;
consider prodc being FinSequence of INT such that
X9: ( dom prodc = Seg lm & ( for k being Nat st k in Seg lm holds
S3[k,prodc . k] ) ) from FINSEQ_1:sch_5(X8);
X10: len prodc = (len nlist) - 1 by X2, FINSEQ_1:def_3, X9;
X11: for i being Nat st 1 <= i & i <= (len m) - 1 holds
ex d, x, y being Element of INT st
( x = (nlist . i) `2 & m . (i + 1) = (m . i) * x & y = m . (i + 1) & d = (nlist . (i + 1)) `2 & prodi . i = ALGO_INVERSE (y,d) & prodc . i = y )
proof
let i be Nat; ::_thesis: ( 1 <= i & i <= (len m) - 1 implies ex d, x, y being Element of INT st
( x = (nlist . i) `2 & m . (i + 1) = (m . i) * x & y = m . (i + 1) & d = (nlist . (i + 1)) `2 & prodi . i = ALGO_INVERSE (y,d) & prodc . i = y ) )
assume ( 1 <= i & i <= (len m) - 1 ) ; ::_thesis: ex d, x, y being Element of INT st
( x = (nlist . i) `2 & m . (i + 1) = (m . i) * x & y = m . (i + 1) & d = (nlist . (i + 1)) `2 & prodi . i = ALGO_INVERSE (y,d) & prodc . i = y )
then i in Seg lm by FINSEQ_1:1;
hence ex d, x, y being Element of INT st
( x = (nlist . i) `2 & m . (i + 1) = (m . i) * x & y = m . (i + 1) & d = (nlist . (i + 1)) `2 & prodi . i = ALGO_INVERSE (y,d) & prodc . i = y ) by X9; ::_thesis: verum
end;
len nlist in Seg (len nlist) by FINSEQ_1:3;
then len m in dom nlist by X2, FINSEQ_1:def_3;
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 VV2, A2, X2, XXREAL_0:1;
then 1 + 1 <= len m by NAT_1:13;
then 2 - 1 <= (len m) - 1 by XREAL_1:9;
then VV1: lm in dom prodc by X9;
prodc in INT * by FINSEQ_1:def_11;
then reconsider MM = prodc . ((len m) - 1) as Element of INT by VV1, FINSEQ_1:84;
reconsider M = MM * M0 as Element of INT by INT_1:def_2;
defpred S4[ Nat, Integer, Integer] means ex u, u0, u1 being 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;
X12: for n being Element of NAT st 1 <= n & n < len nlist holds
for z being Element of INT ex y being Element of INT st S4[n,z,y]
proof
let n be Element of NAT ; ::_thesis: ( 1 <= n & n < len nlist implies for z being Element of INT ex y being Element of INT st S4[n,z,y] )
assume X41: ( 1 <= n & n < len nlist ) ; ::_thesis: for z being Element of INT ex y being Element of INT st S4[n,z,y]
let z be Element of INT ; ::_thesis: ex y being Element of INT st S4[n,z,y]
( 1 <= n + 1 & n + 1 <= len m ) by X41, X2, NAT_1:13;
then n + 1 in Seg (len nlist) by X2;
then n + 1 in dom nlist by FINSEQ_1:def_3;
then XX: 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 XX, 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 ; ::_thesis: S4[n,z,y]
thus S4[n,z,y] ; ::_thesis: verum
end;
1 in Seg (len nlist) by VV2, X2;
then 1 in dom nlist by FINSEQ_1:def_3;
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 being FinSequence of INT such that
X13: ( len n = len nlist & ( n . 1 = L1 or len nlist = 0 ) & ( for i being Element of NAT st 1 <= i & i < len nlist holds
S4[i,n . i,n . (i + 1)] ) ) from RECDEF_1:sch_4(X12);
X14: for i being Nat st 1 <= i & i <= (len m) - 1 holds
ex u, u0, u1 being Element of INT st
( u0 = (nlist . (i + 1)) `1 & u1 = (nlist . (i + 1)) `2 & u = ((u0 - (n . i)) * (prodi . i)) mod u1 & n . (i + 1) = (n . i) + (u * (prodc . i)) )
proof
let i be Nat; ::_thesis: ( 1 <= i & i <= (len m) - 1 implies ex u, u0, u1 being Element of INT st
( u0 = (nlist . (i + 1)) `1 & u1 = (nlist . (i + 1)) `2 & u = ((u0 - (n . i)) * (prodi . i)) mod u1 & n . (i + 1) = (n . i) + (u * (prodc . i)) ) )
assume ( 1 <= i & i <= (len m) - 1 ) ; ::_thesis: ex u, u0, u1 being Element of INT st
( u0 = (nlist . (i + 1)) `1 & u1 = (nlist . (i + 1)) `2 & u = ((u0 - (n . i)) * (prodi . i)) mod u1 & n . (i + 1) = (n . i) + (u * (prodc . i)) )
then X32: ( 1 <= i & i < len nlist ) by X2, II, XXREAL_0:2;
i is Element of NAT by ORDINAL1:def_12;
hence ex u, u0, u1 being Element of INT st
( u0 = (nlist . (i + 1)) `1 & u1 = (nlist . (i + 1)) `2 & u = ((u0 - (n . i)) * (prodi . i)) mod u1 & n . (i + 1) = (n . i) + (u * (prodc . i)) ) by X13, X32; ::_thesis: verum
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 ex b1 being Element of INT st
( ( len nlist = 1 implies b1 = (nlist . 1) `1 ) & ( len nlist <> 1 implies ex m, n, prodc, prodi being FinSequence of INT ex M0, M being Element of INT st
( len m = len nlist & len n = len nlist & len prodc = (len nlist) - 1 & len prodi = (len nlist) - 1 & m . 1 = 1 & ( for i being Nat st 1 <= i & i <= (len m) - 1 holds
ex d, x, y being Element of INT st
( x = (nlist . i) `2 & m . (i + 1) = (m . i) * x & y = m . (i + 1) & d = (nlist . (i + 1)) `2 & prodi . i = ALGO_INVERSE (y,d) & prodc . i = y ) ) & M0 = (nlist . (len m)) `2 & M = (prodc . ((len m) - 1)) * M0 & n . 1 = (nlist . 1) `1 & ( for i being Nat st 1 <= i & i <= (len m) - 1 holds
ex u, u0, u1 being Element of INT st
( u0 = (nlist . (i + 1)) `1 & u1 = (nlist . (i + 1)) `2 & u = ((u0 - (n . i)) * (prodi . i)) mod u1 & n . (i + 1) = (n . i) + (u * (prodc . i)) ) ) & b1 = (n . (len m)) mod M ) ) ) by A2, X14, X11, X2, X13, X6, X10; ::_thesis: verum
end;
end;
end;
uniqueness
for b1, b2 being Element of INT st ( len nlist = 1 implies b1 = (nlist . 1) `1 ) & ( len nlist <> 1 implies ex m, n, prodc, prodi being FinSequence of INT ex M0, M being Element of INT st
( len m = len nlist & len n = len nlist & len prodc = (len nlist) - 1 & len prodi = (len nlist) - 1 & m . 1 = 1 & ( for i being Nat st 1 <= i & i <= (len m) - 1 holds
ex d, x, y being Element of INT st
( x = (nlist . i) `2 & m . (i + 1) = (m . i) * x & y = m . (i + 1) & d = (nlist . (i + 1)) `2 & prodi . i = ALGO_INVERSE (y,d) & prodc . i = y ) ) & M0 = (nlist . (len m)) `2 & M = (prodc . ((len m) - 1)) * M0 & n . 1 = (nlist . 1) `1 & ( for i being Nat st 1 <= i & i <= (len m) - 1 holds
ex u, u0, u1 being Element of INT st
( u0 = (nlist . (i + 1)) `1 & u1 = (nlist . (i + 1)) `2 & u = ((u0 - (n . i)) * (prodi . i)) mod u1 & n . (i + 1) = (n . i) + (u * (prodc . i)) ) ) & b1 = (n . (len m)) mod M ) ) & ( len nlist = 1 implies b2 = (nlist . 1) `1 ) & ( len nlist <> 1 implies ex m, n, prodc, prodi being FinSequence of INT ex M0, M being Element of INT st
( len m = len nlist & len n = len nlist & len prodc = (len nlist) - 1 & len prodi = (len nlist) - 1 & m . 1 = 1 & ( for i being Nat st 1 <= i & i <= (len m) - 1 holds
ex d, x, y being Element of INT st
( x = (nlist . i) `2 & m . (i + 1) = (m . i) * x & y = m . (i + 1) & d = (nlist . (i + 1)) `2 & prodi . i = ALGO_INVERSE (y,d) & prodc . i = y ) ) & M0 = (nlist . (len m)) `2 & M = (prodc . ((len m) - 1)) * M0 & n . 1 = (nlist . 1) `1 & ( for i being Nat st 1 <= i & i <= (len m) - 1 holds
ex u, u0, u1 being Element of INT st
( u0 = (nlist . (i + 1)) `1 & u1 = (nlist . (i + 1)) `2 & u = ((u0 - (n . i)) * (prodi . i)) mod u1 & n . (i + 1) = (n . i) + (u * (prodc . i)) ) ) & b2 = (n . (len m)) mod M ) ) holds
b1 = b2
proof
let s1, s2 be Element of INT ; ::_thesis: ( ( len nlist = 1 implies s1 = (nlist . 1) `1 ) & ( len nlist <> 1 implies ex m, n, prodc, prodi being FinSequence of INT ex M0, M being Element of INT st
( len m = len nlist & len n = len nlist & len prodc = (len nlist) - 1 & len prodi = (len nlist) - 1 & m . 1 = 1 & ( for i being Nat st 1 <= i & i <= (len m) - 1 holds
ex d, x, y being Element of INT st
( x = (nlist . i) `2 & m . (i + 1) = (m . i) * x & y = m . (i + 1) & d = (nlist . (i + 1)) `2 & prodi . i = ALGO_INVERSE (y,d) & prodc . i = y ) ) & M0 = (nlist . (len m)) `2 & M = (prodc . ((len m) - 1)) * M0 & n . 1 = (nlist . 1) `1 & ( for i being Nat st 1 <= i & i <= (len m) - 1 holds
ex u, u0, u1 being Element of INT st
( u0 = (nlist . (i + 1)) `1 & u1 = (nlist . (i + 1)) `2 & u = ((u0 - (n . i)) * (prodi . i)) mod u1 & n . (i + 1) = (n . i) + (u * (prodc . i)) ) ) & s1 = (n . (len m)) mod M ) ) & ( len nlist = 1 implies s2 = (nlist . 1) `1 ) & ( len nlist <> 1 implies ex m, n, prodc, prodi being FinSequence of INT ex M0, M being Element of INT st
( len m = len nlist & len n = len nlist & len prodc = (len nlist) - 1 & len prodi = (len nlist) - 1 & m . 1 = 1 & ( for i being Nat st 1 <= i & i <= (len m) - 1 holds
ex d, x, y being Element of INT st
( x = (nlist . i) `2 & m . (i + 1) = (m . i) * x & y = m . (i + 1) & d = (nlist . (i + 1)) `2 & prodi . i = ALGO_INVERSE (y,d) & prodc . i = y ) ) & M0 = (nlist . (len m)) `2 & M = (prodc . ((len m) - 1)) * M0 & n . 1 = (nlist . 1) `1 & ( for i being Nat st 1 <= i & i <= (len m) - 1 holds
ex u, u0, u1 being Element of INT st
( u0 = (nlist . (i + 1)) `1 & u1 = (nlist . (i + 1)) `2 & u = ((u0 - (n . i)) * (prodi . i)) mod u1 & n . (i + 1) = (n . i) + (u * (prodc . i)) ) ) & s2 = (n . (len m)) mod M ) ) implies s1 = s2 )
assume A1: ( ( len nlist = 1 implies s1 = (nlist . 1) `1 ) & ( len nlist <> 1 implies ex m, n, prodc, prodi being FinSequence of INT ex M0, M being Element of INT st
( len m = len nlist & len n = len nlist & len prodc = (len nlist) - 1 & len prodi = (len nlist) - 1 & m . 1 = 1 & ( for i being Nat st 1 <= i & i <= (len m) - 1 holds
ex d, x, y being Element of INT st
( x = (nlist . i) `2 & m . (i + 1) = (m . i) * x & y = m . (i + 1) & d = (nlist . (i + 1)) `2 & prodi . i = ALGO_INVERSE (y,d) & prodc . i = y ) ) & M0 = (nlist . (len m)) `2 & M = (prodc . ((len m) - 1)) * M0 & n . 1 = (nlist . 1) `1 & ( for i being Nat st 1 <= i & i <= (len m) - 1 holds
ex u, u0, u1 being Element of INT st
( u0 = (nlist . (i + 1)) `1 & u1 = (nlist . (i + 1)) `2 & u = ((u0 - (n . i)) * (prodi . i)) mod u1 & n . (i + 1) = (n . i) + (u * (prodc . i)) ) ) & s1 = (n . (len m)) mod M ) ) ) ; ::_thesis: ( ( len nlist = 1 & not s2 = (nlist . 1) `1 ) or ( len nlist <> 1 & ( for m, n, prodc, prodi being FinSequence of INT
for M0, M being Element of INT holds
( not len m = len nlist or not len n = len nlist or not len prodc = (len nlist) - 1 or not len prodi = (len nlist) - 1 or not m . 1 = 1 or ex i being Nat st
( 1 <= i & i <= (len m) - 1 & ( for d, x, y being Element of INT holds
( not x = (nlist . i) `2 or not m . (i + 1) = (m . i) * x or not y = m . (i + 1) or not d = (nlist . (i + 1)) `2 or not prodi . i = ALGO_INVERSE (y,d) or not prodc . i = y ) ) ) or not M0 = (nlist . (len m)) `2 or not M = (prodc . ((len m) - 1)) * M0 or not n . 1 = (nlist . 1) `1 or ex i being Nat st
( 1 <= i & i <= (len m) - 1 & ( for u, u0, u1 being Element of INT holds
( not u0 = (nlist . (i + 1)) `1 or not u1 = (nlist . (i + 1)) `2 or not u = ((u0 - (n . i)) * (prodi . i)) mod u1 or not n . (i + 1) = (n . i) + (u * (prodc . i)) ) ) ) or not s2 = (n . (len m)) mod M ) ) ) or s1 = s2 )
assume A2: ( ( len nlist = 1 implies s2 = (nlist . 1) `1 ) & ( len nlist <> 1 implies ex m, n, prodc, prodi being FinSequence of INT ex M0, M being Element of INT st
( len m = len nlist & len n = len nlist & len prodc = (len nlist) - 1 & len prodi = (len nlist) - 1 & m . 1 = 1 & ( for i being Nat st 1 <= i & i <= (len m) - 1 holds
ex d, x, y being Element of INT st
( x = (nlist . i) `2 & m . (i + 1) = (m . i) * x & y = m . (i + 1) & d = (nlist . (i + 1)) `2 & prodi . i = ALGO_INVERSE (y,d) & prodc . i = y ) ) & M0 = (nlist . (len m)) `2 & M = (prodc . ((len m) - 1)) * M0 & n . 1 = (nlist . 1) `1 & ( for i being Nat st 1 <= i & i <= (len m) - 1 holds
ex u, u0, u1 being Element of INT st
( u0 = (nlist . (i + 1)) `1 & u1 = (nlist . (i + 1)) `2 & u = ((u0 - (n . i)) * (prodi . i)) mod u1 & n . (i + 1) = (n . i) + (u * (prodc . i)) ) ) & s2 = (n . (len m)) mod M ) ) ) ; ::_thesis: s1 = s2
percases ( len nlist = 1 or len nlist <> 1 ) ;
supposeC1: len nlist = 1 ; ::_thesis: s1 = s2
thus s1 = s2 by A1, A2, C1; ::_thesis: verum
end;
supposeC2: len nlist <> 1 ; ::_thesis: s1 = s2
consider m1, n1, prodc1, prodi1 being FinSequence of INT , M01, M1 being Element of INT such that
P1: ( len m1 = len nlist & len n1 = len nlist & len prodc1 = (len nlist) - 1 & len prodi1 = (len nlist) - 1 & m1 . 1 = 1 & ( for i being Nat st 1 <= i & i <= (len m1) - 1 holds
ex d, x, y being 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 being Nat st 1 <= i & i <= (len m1) - 1 holds
ex u, u0, u1 being 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 C2, A1;
consider m2, n2, prodc2, prodi2 being FinSequence of INT , M02, M2 being Element of INT such that
P2: ( len m2 = len nlist & len n2 = len nlist & len prodc2 = (len nlist) - 1 & len prodi2 = (len nlist) - 1 & m2 . 1 = 1 & ( for i being Nat st 1 <= i & i <= (len m2) - 1 holds
ex d, x, y being 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 being Nat st 1 <= i & i <= (len m2) - 1 holds
ex u, u0, u1 being 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 C2, A2;
defpred S1[ Nat] means ( 1 <= $1 & $1 <= len m1 implies m1 . $1 = m2 . $1 );
Q50: S1[ 0 ] ;
Q51: for i being Nat st S1[i] holds
S1[i + 1]
proof
let i be Nat; ::_thesis: ( S1[i] implies S1[i + 1] )
assume Q52: S1[i] ; ::_thesis: S1[i + 1]
assume ( 1 <= i + 1 & i + 1 <= len m1 ) ; ::_thesis: m1 . (i + 1) = m2 . (i + 1)
then Q54: ( 1 - 1 <= (i + 1) - 1 & (i + 1) - 1 <= (len m1) - 1 ) by XREAL_1:9;
Q55: (len m1) - 1 <= (len m1) - 0 by XREAL_1:13;
percases ( i = 0 or i <> 0 ) ;
supposeC1: i = 0 ; ::_thesis: m1 . (i + 1) = m2 . (i + 1)
thus m1 . (i + 1) = m2 . (i + 1) by P1, P2, C1; ::_thesis: verum
end;
supposeQ56P: i <> 0 ; ::_thesis: m1 . (i + 1) = m2 . (i + 1)
then Q56: 1 <= i by NAT_1:14;
Q57: ex d, x, y being 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 P1, Q56, Q54;
( 1 <= i & i <= (len m2) - 1 ) by Q56P, Q54, P1, P2, NAT_1:14;
then ex d, x, y being 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 P2;
hence m1 . (i + 1) = m2 . (i + 1) by Q57, Q54, Q52, Q55, Q56P, NAT_1:14, XXREAL_0:2; ::_thesis: verum
end;
end;
end;
Q0: for k being Nat holds S1[k] from NAT_1:sch_2(Q50, Q51);
QQ3: now__::_thesis:_for_i_being_Nat_st_1_<=_i_&_i_<=_len_prodc1_holds_
prodc1_._i_=_prodc2_._i
let i be Nat; ::_thesis: ( 1 <= i & i <= len prodc1 implies prodc1 . i = prodc2 . i )
assume ASX0: ( 1 <= i & i <= len prodc1 ) ; ::_thesis: prodc1 . i = prodc2 . i
then X1: ex d, x, y being 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 P1;
ex d, x, y being 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 P2, ASX0, P1;
hence prodc1 . i = prodc2 . i by X1, FINSEQ_1:14, P1, P2, Q0; ::_thesis: verum
end;
then Q3: prodc1 = prodc2 by FINSEQ_1:14, P1, P2;
Q3A: now__::_thesis:_for_i_being_Nat_st_1_<=_i_&_i_<=_len_prodi1_holds_
prodi1_._i_=_prodi2_._i
let i be Nat; ::_thesis: ( 1 <= i & i <= len prodi1 implies prodi1 . i = prodi2 . i )
assume ASX0: ( 1 <= i & i <= len prodi1 ) ; ::_thesis: prodi1 . i = prodi2 . i
then X1: ex d, x, y being 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 P1;
ex d, x, y being 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 P2, ASX0, P1;
hence prodi1 . i = prodi2 . i by X1, Q0, FINSEQ_1:14, P1, P2; ::_thesis: verum
end;
Q4: M1 = M2 by P2, FINSEQ_1:14, P1, QQ3;
defpred S2[ Nat] means ( 1 <= $1 & $1 <= len n1 implies n1 . $1 = n2 . $1 );
Q50: S2[ 0 ] ;
Q51: for k being Nat st S2[k] holds
S2[k + 1]
proof
let k be Nat; ::_thesis: ( S2[k] implies S2[k + 1] )
assume Q52: S2[k] ; ::_thesis: S2[k + 1]
assume ( 1 <= k + 1 & k + 1 <= len n1 ) ; ::_thesis: n1 . (k + 1) = n2 . (k + 1)
then Q54: ( 1 - 1 <= (k + 1) - 1 & (k + 1) - 1 <= (len n1) - 1 ) by XREAL_1:9;
Q55: (len n1) - 1 <= (len n1) - 0 by XREAL_1:13;
percases ( k = 0 or k <> 0 ) ;
supposeC1: k = 0 ; ::_thesis: n1 . (k + 1) = n2 . (k + 1)
thus n1 . (k + 1) = n2 . (k + 1) by P1, P2, C1; ::_thesis: verum
end;
supposeASQ56: k <> 0 ; ::_thesis: n1 . (k + 1) = n2 . (k + 1)
then Q56: 1 <= k by NAT_1:14;
Q57: ex u, u0, u1 being 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 Q56, Q54, P1;
ex u, u0, u1 being 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 Q56, Q54, P1, P2;
hence n1 . (k + 1) = n2 . (k + 1) by Q3, Q57, Q52, Q55, ASQ56, NAT_1:14, Q54, XXREAL_0:2, FINSEQ_1:14, P1, P2, Q3A; ::_thesis: verum
end;
end;
end;
for k being Nat holds S2[k] from NAT_1:sch_2(Q50, Q51);
hence s1 = s2 by Q4, P1, P2, FINSEQ_1:14; ::_thesis: verum
end;
end;
end;
end;
:: deftheorem defALGOCRT defines ALGO_CRT NTALGO_1:def_4_:_
for nlist being non empty FinSequence of [:INT,INT:]
for b2 being Element of INT holds
( b2 = ALGO_CRT nlist iff ( ( len nlist = 1 implies b2 = (nlist . 1) `1 ) & ( len nlist <> 1 implies ex m, n, prodc, prodi being FinSequence of INT ex M0, M being Element of INT st
( len m = len nlist & len n = len nlist & len prodc = (len nlist) - 1 & len prodi = (len nlist) - 1 & m . 1 = 1 & ( for i being Nat st 1 <= i & i <= (len m) - 1 holds
ex d, x, y being Element of INT st
( x = (nlist . i) `2 & m . (i + 1) = (m . i) * x & y = m . (i + 1) & d = (nlist . (i + 1)) `2 & prodi . i = ALGO_INVERSE (y,d) & prodc . i = y ) ) & M0 = (nlist . (len m)) `2 & M = (prodc . ((len m) - 1)) * M0 & n . 1 = (nlist . 1) `1 & ( for i being Nat st 1 <= i & i <= (len m) - 1 holds
ex u, u0, u1 being Element of INT st
( u0 = (nlist . (i + 1)) `1 & u1 = (nlist . (i + 1)) `2 & u = ((u0 - (n . i)) * (prodi . i)) mod u1 & n . (i + 1) = (n . i) + (u * (prodc . i)) ) ) & b2 = (n . (len m)) mod M ) ) ) );
theorem LMLmTh4B: :: NTALGO_1:8
for a, b being Element of INT st b <> 0 holds
a mod b,a are_congruent_mod b
proof
let a, b be Element of INT ; ::_thesis: ( b <> 0 implies a mod b,a are_congruent_mod b )
assume b <> 0 ; ::_thesis: a mod b,a are_congruent_mod b
then C1: 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 ; :: according to INT_1:def_5 ::_thesis: b * c = (a mod b) - a
thus b * c = (a mod b) - a by C1; ::_thesis: verum
end;
theorem :: NTALGO_1:9
for a, b being Element of INT st b <> 0 holds
(a mod b) gcd b = a gcd b by INT_4:14, LMLmTh4B;
theorem LmTh4A: :: NTALGO_1:10
for a, b, c being Element of INT st c <> 0 & a = b mod c & b,c are_relative_prime holds
a,c are_relative_prime
proof
let a, b, c be Element of INT ; ::_thesis: ( c <> 0 & a = b mod c & b,c are_relative_prime implies a,c are_relative_prime )
assume A1: ( c <> 0 & a = b mod c & b,c are_relative_prime ) ; ::_thesis: a,c are_relative_prime
then b gcd c = 1 by INT_2:def_3;
then a gcd c = 1 by A1, INT_4:14, LMLmTh4B;
hence a,c are_relative_prime by INT_2:def_3; ::_thesis: verum
end;
LmTh4: for a, b, c being Element of INT st a = b mod c & c <> 0 holds
ex d being Element of INT st a = b + (d * c)
proof
let a, b, c be Element of INT ; ::_thesis: ( a = b mod c & c <> 0 implies ex d being Element of INT st a = b + (d * c) )
assume ( a = b mod c & c <> 0 ) ; ::_thesis: ex d being Element of INT st a = b + (d * c)
then C1: 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 ; ::_thesis: a = b + (x * c)
thus a = b + (x * c) by C1; ::_thesis: verum
end;
LmTh5A: for b, m being FinSequence of INT st len b = len m & ( for i being Nat st i in Seg (len b) holds
b . i <> 0 ) & m . 1 = 1 holds
for k being Element of NAT st 1 <= k & k <= (len b) - 1 & ( for i being Nat st 1 <= i & i <= k holds
m . (i + 1) = (m . i) * (b . i) ) holds
m . (k + 1) <> 0
proof
let b, m be FinSequence of INT ; ::_thesis: ( len b = len m & ( for i being Nat st i in Seg (len b) holds
b . i <> 0 ) & m . 1 = 1 implies for k being Element of NAT st 1 <= k & k <= (len b) - 1 & ( for i being Nat st 1 <= i & i <= k holds
m . (i + 1) = (m . i) * (b . i) ) holds
m . (k + 1) <> 0 )
assume len b = len m ; ::_thesis: ( ex i being Nat st
( i in Seg (len b) & not b . i <> 0 ) or not m . 1 = 1 or for k being Element of NAT st 1 <= k & k <= (len b) - 1 & ( for i being Nat st 1 <= i & i <= k holds
m . (i + 1) = (m . i) * (b . i) ) holds
m . (k + 1) <> 0 )
assume A2: ( ( for i being Nat st i in Seg (len b) holds
b . i <> 0 ) & m . 1 = 1 ) ; ::_thesis: for k being Element of NAT st 1 <= k & k <= (len b) - 1 & ( for i being Nat st 1 <= i & i <= k holds
m . (i + 1) = (m . i) * (b . i) ) holds
m . (k + 1) <> 0
defpred S1[ Nat] means ( 1 <= $1 & $1 <= (len b) - 1 & ( for i being 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 ;
P0: S1[ 0 ] ;
P1: for k being Element of NAT st S1[k] holds
S1[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] )
assume P11: S1[k] ; ::_thesis: S1[k + 1]
assume P12: ( 1 <= k + 1 & k + 1 <= (len b) - 1 & ( for i being Nat st 1 <= i & i <= k + 1 holds
m . (i + 1) = (m . i) * (b . i) ) ) ; ::_thesis: m . ((k + 1) + 1) <> 0
P14: k <= k + 1 by NAT_1:12;
percases ( k = 0 or k <> 0 ) ;
supposeP15: k = 0 ; ::_thesis: m . ((k + 1) + 1) <> 0
P16: m . ((k + 1) + 1) = (m . 1) * (b . 1) by P12, P15
.= b . 1 by A2 ;
((len b) - 1) + 0 <= ((len b) - 1) + 1 by XREAL_1:7;
then k + 1 <= len b by P12, XXREAL_0:2;
then ( 1 <= 1 & 1 <= len b ) by XXREAL_0:2, P12;
then 1 in Seg (len b) ;
hence m . ((k + 1) + 1) <> 0 by P16, A2; ::_thesis: verum
end;
supposeP19: k <> 0 ; ::_thesis: m . ((k + 1) + 1) <> 0
P20: now__::_thesis:_for_i_being_Nat_st_1_<=_i_&_i_<=_k_holds_
m_._(i_+_1)_=_(m_._i)_*_(b_._i)
let i be Nat; ::_thesis: ( 1 <= i & i <= k implies m . (i + 1) = (m . i) * (b . i) )
assume ( 1 <= i & i <= k ) ; ::_thesis: m . (i + 1) = (m . i) * (b . i)
then ( 1 <= i & i <= k + 1 ) by NAT_1:12;
hence m . (i + 1) = (m . i) * (b . i) by P12; ::_thesis: verum
end;
thus m . ((k + 1) + 1) <> 0 ::_thesis: verum
proof
XX6: (k + 1) + 1 <= ((len b) - 1) + 1 by P12, XREAL_1:6;
XX1: k + 1 <= (k + 1) + 1 by NAT_1:12;
XX2: 1 <= k + 1 by NAT_1:12;
k + 1 <= len b by XX1, XX6, XXREAL_0:2;
then k + 1 in Seg (len b) by XX2;
then P23: b . (k + 1) <> 0 by A2;
m . ((k + 1) + 1) = (m . (k + 1)) * (b . (k + 1)) by P12;
hence m . ((k + 1) + 1) <> 0 by P23, P20, P11, P12, P14, XXREAL_0:2, NAT_1:14, P19, XCMPLX_1:6; ::_thesis: verum
end;
end;
end;
end;
for k being Element of NAT holds S1[k] from NAT_1:sch_1(P0, P1);
hence for k being Element of NAT st 1 <= k & k <= (len b) - 1 & ( for i being Nat st 1 <= i & i <= k holds
m . (i + 1) = (m . i) * (b . i) ) holds
m . (k + 1) <> 0 ; ::_thesis: verum
end;
LmTh5: for b, m being FinSequence of INT st 2 <= len b & ( for i, j being Nat st i in Seg (len b) & j in Seg (len b) & i <> j holds
b . i,b . j are_relative_prime ) & m . 1 = 1 holds
for k being Element of NAT st 1 <= k & k <= (len b) - 1 & ( for i being Nat st 1 <= i & i <= k holds
m . (i + 1) = (m . i) * (b . i) ) holds
for j being Nat st k + 1 <= j & j <= len b holds
m . (k + 1),b . j are_relative_prime
proof
let b, m be FinSequence of INT ; ::_thesis: ( 2 <= len b & ( for i, j being Nat st i in Seg (len b) & j in Seg (len b) & i <> j holds
b . i,b . j are_relative_prime ) & m . 1 = 1 implies for k being Element of NAT st 1 <= k & k <= (len b) - 1 & ( for i being Nat st 1 <= i & i <= k holds
m . (i + 1) = (m . i) * (b . i) ) holds
for j being Nat st k + 1 <= j & j <= len b holds
m . (k + 1),b . j are_relative_prime )
assume 2 <= len b ; ::_thesis: ( ex i, j being Nat st
( i in Seg (len b) & j in Seg (len b) & i <> j & not b . i,b . j are_relative_prime ) or not m . 1 = 1 or for k being Element of NAT st 1 <= k & k <= (len b) - 1 & ( for i being Nat st 1 <= i & i <= k holds
m . (i + 1) = (m . i) * (b . i) ) holds
for j being Nat st k + 1 <= j & j <= len b holds
m . (k + 1),b . j are_relative_prime )
assume A2: ( ( for i, j being Nat st i in Seg (len b) & j in Seg (len b) & i <> j holds
b . i,b . j are_relative_prime ) & m . 1 = 1 ) ; ::_thesis: for k being Element of NAT st 1 <= k & k <= (len b) - 1 & ( for i being Nat st 1 <= i & i <= k holds
m . (i + 1) = (m . i) * (b . i) ) holds
for j being Nat st k + 1 <= j & j <= len b holds
m . (k + 1),b . j are_relative_prime
defpred S1[ Nat] means ( 1 <= $1 & $1 <= (len b) - 1 & ( for i being Nat st 1 <= i & i <= $1 holds
m . (i + 1) = (m . i) * (b . i) ) implies for j being Nat st $1 + 1 <= j & j <= len b holds
m . ($1 + 1),b . j are_relative_prime );
reconsider I0 = 0 as Element of NAT ;
P0: S1[ 0 ] ;
P1: for k being Element of NAT st S1[k] holds
S1[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] )
assume P11: S1[k] ; ::_thesis: S1[k + 1]
assume P12: ( 1 <= k + 1 & k + 1 <= (len b) - 1 & ( for i being Nat st 1 <= i & i <= k + 1 holds
m . (i + 1) = (m . i) * (b . i) ) ) ; ::_thesis: for j being Nat st (k + 1) + 1 <= j & j <= len b holds
m . ((k + 1) + 1),b . j are_relative_prime
P14: k <= k + 1 by NAT_1:12;
percases ( k = 0 or k <> 0 ) ;
supposeP15: k = 0 ; ::_thesis: for j being Nat st (k + 1) + 1 <= j & j <= len b holds
m . ((k + 1) + 1),b . j are_relative_prime
P16: m . ((k + 1) + 1) = (m . 1) * (b . 1) by P12, P15
.= b . 1 by A2 ;
for j being Nat st (k + 1) + 1 <= j & j <= len b holds
m . ((k + 1) + 1),b . j are_relative_prime
proof
let j be Nat; ::_thesis: ( (k + 1) + 1 <= j & j <= len b implies m . ((k + 1) + 1),b . j are_relative_prime )
assume XX0: ( (k + 1) + 1 <= j & j <= len b ) ; ::_thesis: m . ((k + 1) + 1),b . j are_relative_prime
then XX2: ( 1 <= j & j <= len b ) by XXREAL_0:2, P15;
then XX1: j in Seg (len b) by FINSEQ_1:1;
( 1 <= 1 & 1 <= len b ) by XXREAL_0:2, XX2;
then XX3: 1 in Seg (len b) ;
1 <> j by XX0, P15;
hence m . ((k + 1) + 1),b . j are_relative_prime by P16, A2, XX1, XX3; ::_thesis: verum
end;
hence for j being Nat st (k + 1) + 1 <= j & j <= len b holds
m . ((k + 1) + 1),b . j are_relative_prime ; ::_thesis: verum
end;
supposeP19: k <> 0 ; ::_thesis: for j being Nat st (k + 1) + 1 <= j & j <= len b holds
m . ((k + 1) + 1),b . j are_relative_prime
P20: now__::_thesis:_for_i_being_Nat_st_1_<=_i_&_i_<=_k_holds_
m_._(i_+_1)_=_(m_._i)_*_(b_._i)
let i be Nat; ::_thesis: ( 1 <= i & i <= k implies m . (i + 1) = (m . i) * (b . i) )
assume ( 1 <= i & i <= k ) ; ::_thesis: m . (i + 1) = (m . i) * (b . i)
then ( 1 <= i & i <= k + 1 ) by NAT_1:12;
hence m . (i + 1) = (m . i) * (b . i) by P12; ::_thesis: verum
end;
thus for j being Nat st (k + 1) + 1 <= j & j <= len b holds
m . ((k + 1) + 1),b . j are_relative_prime ::_thesis: verum
proof
let j be Nat; ::_thesis: ( (k + 1) + 1 <= j & j <= len b implies m . ((k + 1) + 1),b . j are_relative_prime )
assume XX6: ( (k + 1) + 1 <= j & j <= len b ) ; ::_thesis: m . ((k + 1) + 1),b . j are_relative_prime
k + 1 <= (k + 1) + 1 by NAT_1:12;
then XX1: ( k + 1 <= j & j <= len b ) by XX6, XXREAL_0:2;
then P21: m . (k + 1),b . j are_relative_prime by P20, P11, P12, P14, XXREAL_0:2, NAT_1:14, P19;
XX2: 1 <= k + 1 by NAT_1:12;
k + 1 <= len b by XX1, XXREAL_0:2;
then XX3: k + 1 in Seg (len b) by XX2;
( 1 <= j & j <= len b ) by XX1, XX2, XXREAL_0:2;
then XX4: j in Seg (len b) by FINSEQ_1:1;
k + 1 < j by XX6, XXREAL_0:2, NAT_1:16;
then P23: b . (k + 1),b . j are_relative_prime by A2, XX3, XX4;
m . ((k + 1) + 1) = (m . (k + 1)) * (b . (k + 1)) by P12;
hence m . ((k + 1) + 1),b . j are_relative_prime by P23, P21, INT_2:26; ::_thesis: verum
end;
end;
end;
end;
for k being Element of NAT holds S1[k] from NAT_1:sch_1(P0, P1);
hence for k being Element of NAT st 1 <= k & k <= (len b) - 1 & ( for i being Nat st 1 <= i & i <= k holds
m . (i + 1) = (m . i) * (b . i) ) holds
for j being Nat st k + 1 <= j & j <= len b holds
m . (k + 1),b . j are_relative_prime ; ::_thesis: verum
end;
LmTh6: for b, m being FinSequence of INT st len b = len m & m . 1 = 1 holds
for k being Element of NAT st 1 <= k & k <= (len b) - 1 & ( for i being Nat st 1 <= i & i <= k holds
m . (i + 1) = (m . i) * (b . i) ) holds
for j being Nat st 1 <= j & j <= k holds
(m . (k + 1)) mod (b . j) = 0
proof
let b, m be FinSequence of INT ; ::_thesis: ( len b = len m & m . 1 = 1 implies for k being Element of NAT st 1 <= k & k <= (len b) - 1 & ( for i being Nat st 1 <= i & i <= k holds
m . (i + 1) = (m . i) * (b . i) ) holds
for j being Nat st 1 <= j & j <= k holds
(m . (k + 1)) mod (b . j) = 0 )
assume len b = len m ; ::_thesis: ( not m . 1 = 1 or for k being Element of NAT st 1 <= k & k <= (len b) - 1 & ( for i being Nat st 1 <= i & i <= k holds
m . (i + 1) = (m . i) * (b . i) ) holds
for j being Nat st 1 <= j & j <= k holds
(m . (k + 1)) mod (b . j) = 0 )
assume A2: m . 1 = 1 ; ::_thesis: for k being Element of NAT st 1 <= k & k <= (len b) - 1 & ( for i being Nat st 1 <= i & i <= k holds
m . (i + 1) = (m . i) * (b . i) ) holds
for j being Nat st 1 <= j & j <= k holds
(m . (k + 1)) mod (b . j) = 0
defpred S1[ Nat] means ( 1 <= $1 & $1 <= (len b) - 1 & ( for i being Nat st 1 <= i & i <= $1 holds
m . (i + 1) = (m . i) * (b . i) ) implies for j being Nat st 1 <= j & j <= $1 holds
(m . ($1 + 1)) mod (b . j) = 0 );
reconsider I0 = 0 as Element of NAT ;
P0: S1[ 0 ] ;
P1: for k being Element of NAT st S1[k] holds
S1[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] )
assume P11: S1[k] ; ::_thesis: S1[k + 1]
assume P12: ( 1 <= k + 1 & k + 1 <= (len b) - 1 & ( for i being Nat st 1 <= i & i <= k + 1 holds
m . (i + 1) = (m . i) * (b . i) ) ) ; ::_thesis: for j being Nat st 1 <= j & j <= k + 1 holds
(m . ((k + 1) + 1)) mod (b . j) = 0
P14: k <= k + 1 by NAT_1:12;
percases ( k = 0 or k <> 0 ) ;
supposeP15: k = 0 ; ::_thesis: for j being Nat st 1 <= j & j <= k + 1 holds
(m . ((k + 1) + 1)) mod (b . j) = 0
P16: m . ((k + 1) + 1) = (m . 1) * (b . 1) by P12, P15
.= b . 1 by A2 ;
for j being Nat st 1 <= j & j <= k + 1 holds
(m . ((k + 1) + 1)) mod (b . j) = 0
proof
let j be Nat; ::_thesis: ( 1 <= j & j <= k + 1 implies (m . ((k + 1) + 1)) mod (b . j) = 0 )
assume ( 1 <= j & j <= k + 1 ) ; ::_thesis: (m . ((k + 1) + 1)) mod (b . j) = 0
then j = 1 by XXREAL_0:1, P15;
hence (m . ((k + 1) + 1)) mod (b . j) = 0 by INT_1:50, P16; ::_thesis: verum
end;
hence for j being Nat st 1 <= j & j <= k + 1 holds
(m . ((k + 1) + 1)) mod (b . j) = 0 ; ::_thesis: verum
end;
suppose k <> 0 ; ::_thesis: for j being Nat st 1 <= j & j <= k + 1 holds
(m . ((k + 1) + 1)) mod (b . j) = 0
P20: now__::_thesis:_for_i_being_Nat_st_1_<=_i_&_i_<=_k_holds_
m_._(i_+_1)_=_(m_._i)_*_(b_._i)
let i be Nat; ::_thesis: ( 1 <= i & i <= k implies m . (i + 1) = (m . i) * (b . i) )
assume ( 1 <= i & i <= k ) ; ::_thesis: m . (i + 1) = (m . i) * (b . i)
then ( 1 <= i & i <= k + 1 ) by NAT_1:12;
hence m . (i + 1) = (m . i) * (b . i) by P12; ::_thesis: verum
end;
thus for j being Nat st 1 <= j & j <= k + 1 holds
(m . ((k + 1) + 1)) mod (b . j) = 0 ::_thesis: verum
proof
let j be Nat; ::_thesis: ( 1 <= j & j <= k + 1 implies (m . ((k + 1) + 1)) mod (b . j) = 0 )
assume XX6: ( 1 <= j & j <= k + 1 ) ; ::_thesis: (m . ((k + 1) + 1)) mod (b . j) = 0
reconsider bj = b . j as Element of INT by INT_1:def_2;
percases ( j = k + 1 or j <> k + 1 ) ;
supposeXX61: j = k + 1 ; ::_thesis: (m . ((k + 1) + 1)) mod (b . j) = 0
thus (m . ((k + 1) + 1)) mod (b . j) = ((m . (k + 1)) * (b . (k + 1))) mod (b . j) by P12
.= (((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) mod (b . j) by INT_1:50, XX61
.= 0 by INT_4:12 ; ::_thesis: verum
end;
suppose j <> k + 1 ; ::_thesis: (m . ((k + 1) + 1)) mod (b . j) = 0
then j < k + 1 by XX6, XXREAL_0:1;
then XX1: j <= k by NAT_1:13;
thus (m . ((k + 1) + 1)) mod (b . j) = ((m . (k + 1)) * (b . (k + 1))) mod (b . j) by P12
.= (((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 XX1, P20, XX6, P11, P12, P14, XXREAL_0:2
.= 0 by INT_4:12 ; ::_thesis: verum
end;
end;
end;
end;
end;
end;
for k being Element of NAT holds S1[k] from NAT_1:sch_1(P0, P1);
hence for k being Element of NAT st 1 <= k & k <= (len b) - 1 & ( for i being Nat st 1 <= i & i <= k holds
m . (i + 1) = (m . i) * (b . i) ) holds
for j being Nat st 1 <= j & j <= k holds
(m . (k + 1)) mod (b . j) = 0 ; ::_thesis: verum
end;
theorem Th4: :: NTALGO_1:11
for nlist being non empty FinSequence of [:INT,INT:]
for a, b being FinSequence of INT st len a = len b & len a = len nlist & ( for i being Nat st i in Seg (len nlist) holds
b . i <> 0 ) & ( for i being Nat st i in Seg (len nlist) holds
( (nlist . i) `1 = a . i & (nlist . i) `2 = b . i ) ) & ( for i, j being Nat st i in Seg (len nlist) & j in Seg (len nlist) & i <> j holds
b . i,b . j are_relative_prime ) holds
for i being Nat st i in Seg (len nlist) holds
(ALGO_CRT nlist) mod (b . i) = (a . i) mod (b . i)
proof
defpred S1[ Nat] means for nlist being non empty FinSequence of [:INT,INT:]
for a, b being FinSequence of INT st len nlist = $1 & len a = len b & len a = len nlist & ( for i being Nat st i in Seg (len nlist) holds
b . i <> 0 ) & ( for i being Nat st i in Seg (len nlist) holds
( (nlist . i) `1 = a . i & (nlist . i) `2 = b . i ) ) & ( for i, j being Nat st i in Seg (len nlist) & j in Seg (len nlist) & i <> j holds
b . i,b . j are_relative_prime ) holds
for i being Nat st i in Seg (len nlist) holds
(ALGO_CRT nlist) mod (b . i) = (a . i) mod (b . i);
P0: S1[ 0 ] ;
P1: for n being Element of NAT st S1[n] holds
S1[n + 1]
proof
let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] )
assume AS1: S1[n] ; ::_thesis: S1[n + 1]
let nlist be non empty FinSequence of [:INT,INT:]; ::_thesis: for a, b being FinSequence of INT st len nlist = n + 1 & len a = len b & len a = len nlist & ( for i being Nat st i in Seg (len nlist) holds
b . i <> 0 ) & ( for i being Nat st i in Seg (len nlist) holds
( (nlist . i) `1 = a . i & (nlist . i) `2 = b . i ) ) & ( for i, j being Nat st i in Seg (len nlist) & j in Seg (len nlist) & i <> j holds
b . i,b . j are_relative_prime ) holds
for i being Nat st i in Seg (len nlist) holds
(ALGO_CRT nlist) mod (b . i) = (a . i) mod (b . i)
let a, b be FinSequence of INT ; ::_thesis: ( len nlist = n + 1 & len a = len b & len a = len nlist & ( for i being Nat st i in Seg (len nlist) holds
b . i <> 0 ) & ( for i being Nat st i in Seg (len nlist) holds
( (nlist . i) `1 = a . i & (nlist . i) `2 = b . i ) ) & ( for i, j being Nat st i in Seg (len nlist) & j in Seg (len nlist) & i <> j holds
b . i,b . j are_relative_prime ) implies for i being Nat st i in Seg (len nlist) holds
(ALGO_CRT nlist) mod (b . i) = (a . i) mod (b . i) )
assume AS2: ( len nlist = n + 1 & len a = len b & len a = len nlist & ( for i being Nat st i in Seg (len nlist) holds
b . i <> 0 ) & ( for i being Nat st i in Seg (len nlist) holds
( (nlist . i) `1 = a . i & (nlist . i) `2 = b . i ) ) & ( for i, j being Nat st i in Seg (len nlist) & j in Seg (len nlist) & i <> j holds
b . i,b . j are_relative_prime ) ) ; ::_thesis: for i being Nat st i in Seg (len nlist) holds
(ALGO_CRT nlist) mod (b . i) = (a . i) mod (b . i)
percases ( n = 0 or n <> 0 ) ;
supposeP1: n = 0 ; ::_thesis: for i being Nat st i in Seg (len nlist) holds
(ALGO_CRT nlist) mod (b . i) = (a . i) mod (b . i)
P2: 1 in Seg (len nlist) by P1, AS2;
P3: ALGO_CRT nlist = (nlist . 1) `1 by defALGOCRT, P1, AS2
.= a . 1 by AS2, P2 ;
thus for i being Nat st i in Seg (len nlist) holds
(ALGO_CRT nlist) mod (b . i) = (a . i) mod (b . i) by P3, TARSKI:def_1, FINSEQ_1:2, P1, AS2; ::_thesis: verum
end;
supposeNN1: n <> 0 ; ::_thesis: for i being Nat st i in Seg (len nlist) holds
(ALGO_CRT nlist) mod (b . i) = (a . i) mod (b . i)
then NN2: 1 <= n by NAT_1:14;
P4: len nlist <> 1 by AS2, NN1;
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 ;
KK: n <= n + 1 by NAT_1:11;
then D02: len a1 = n by FINSEQ_1:59, AS2;
D22: len nlist1 = n by KK, FINSEQ_1:59, AS2;
then reconsider nlist1 = nlist1 as non empty FinSequence of [:INT,INT:] by NN1;
D23: dom nlist1 = Seg (len nlist1) by FINSEQ_1:def_3
.= Seg n by KK, FINSEQ_1:59, AS2 ;
D25: len nlist1 = n by D23, FINSEQ_1:def_3;
then D28: Seg (len nlist1) c= Seg (len nlist) by KK, FINSEQ_1:5, AS2;
X1: ( len nlist1 = n & len a1 = len b1 & len a1 = len nlist1 ) by D02, KK, FINSEQ_1:59, AS2;
X2A: for i being Nat st i in Seg (len nlist1) holds
b1 . i <> 0
proof
let i be Nat; ::_thesis: ( i in Seg (len nlist1) implies b1 . i <> 0 )
assume D260: i in Seg (len nlist1) ; ::_thesis: b1 . i <> 0
then b1 . i = b . i by FUNCT_1:49, D25;
hence b1 . i <> 0 by D28, D260, AS2; ::_thesis: verum
end;
X2: for i being Nat st i in Seg (len nlist1) holds
( (nlist1 . i) `1 = a1 . i & (nlist1 . i) `2 = b1 . i )
proof
let i be Nat; ::_thesis: ( i in Seg (len nlist1) implies ( (nlist1 . i) `1 = a1 . i & (nlist1 . i) `2 = b1 . i ) )
assume X21: i in Seg (len nlist1) ; ::_thesis: ( (nlist1 . i) `1 = a1 . i & (nlist1 . i) `2 = b1 . i )
X23: (nlist1 . i) `1 = (nlist . i) `1 by X21, FUNCT_1:49, D25
.= a . i by X21, D28, AS2
.= a1 . i by X21, FUNCT_1:49, D25 ;
(nlist1 . i) `2 = (nlist . i) `2 by X21, FUNCT_1:49, D25
.= b . i by X21, D28, AS2
.= b1 . i by X21, FUNCT_1:49, D25 ;
hence ( (nlist1 . i) `1 = a1 . i & (nlist1 . i) `2 = b1 . i ) by X23; ::_thesis: verum
end;
X3: for i, j being Nat st i in Seg (len nlist1) & j in Seg (len nlist1) & i <> j holds
b1 . i,b1 . j are_relative_prime
proof
let i, j be Nat; ::_thesis: ( i in Seg (len nlist1) & j in Seg (len nlist1) & i <> j implies b1 . i,b1 . j are_relative_prime )
assume A1: ( i in Seg (len nlist1) & j in Seg (len nlist1) & i <> j ) ; ::_thesis: b1 . i,b1 . j are_relative_prime
A3: b . i = b1 . i by A1, FUNCT_1:49, D25;
b . j = b1 . j by A1, FUNCT_1:49, D25;
hence b1 . i,b1 . j are_relative_prime by A3, A1, D28, AS2; ::_thesis: verum
end;
X400: for i being Nat st i in Seg (len nlist1) holds
(ALGO_CRT nlist1) mod (b . i) = (a . i) mod (b . i)
proof
let i be Nat; ::_thesis: ( i in Seg (len nlist1) implies (ALGO_CRT nlist1) mod (b . i) = (a . i) mod (b . i) )
assume A1: i in Seg (len nlist1) ; ::_thesis: (ALGO_CRT nlist1) mod (b . i) = (a . i) mod (b . i)
then ( a1 . i = a . i & b1 . i = b . i ) by FUNCT_1:49, D25;
hence (ALGO_CRT nlist1) mod (b . i) = (a . i) mod (b . i) by AS1, X1, X2, X3, X2A, A1; ::_thesis: verum
end;
consider m, l, prodc, prodi being FinSequence of INT , M0, M being Element of INT such that
X5: ( len m = len nlist & len l = len nlist & len prodc = (len nlist) - 1 & len prodi = (len nlist) - 1 & m . 1 = 1 & ( for i being Nat st 1 <= i & i <= (len m) - 1 holds
ex d, x, y being Element of INT st
( x = (nlist . i) `2 & m . (i + 1) = (m . i) * x & y = m . (i + 1) & d = (nlist . (i + 1)) `2 & prodi . i = ALGO_INVERSE (y,d) & prodc . i = y ) ) & M0 = (nlist . (len m)) `2 & M = (prodc . ((len m) - 1)) * M0 & l . 1 = (nlist . 1) `1 & ( for i being Nat st 1 <= i & i <= (len m) - 1 holds
ex u, u0, u1 being Element of INT st
( u0 = (nlist . (i + 1)) `1 & u1 = (nlist . (i + 1)) `2 & u = ((u0 - (l . i)) * (prodi . i)) mod u1 & l . (i + 1) = (l . i) + (u * (prodc . i)) ) ) & ALGO_CRT nlist = (l . (len m)) mod M ) by P4, defALGOCRT;
LmTh51: 1 + 1 <= n + 1 by XREAL_1:6, NN2;
reconsider lb1 = (len b) - 1 as Element of NAT by AS2;
LmTh54: ( 1 <= lb1 & lb1 <= lb1 ) by AS2, NAT_1:14, NN1;
LmTh55: for i being Nat st 1 <= i & i <= lb1 holds
m . (i + 1) = (m . i) * (b . i)
proof
let i be Nat; ::_thesis: ( 1 <= i & i <= lb1 implies m . (i + 1) = (m . i) * (b . i) )
assume PX0: ( 1 <= i & i <= lb1 ) ; ::_thesis: m . (i + 1) = (m . i) * (b . i)
then PX1: ex d, x, y being Element of INT st
( x = (nlist . i) `2 & m . (i + 1) = (m . i) * x & y = m . (i + 1) & d = (nlist . (i + 1)) `2 & prodi . i = ALGO_INVERSE (y,d) & prodc . i = y ) by AS2, X5;
i in Seg (len nlist1) by PX0, D22, AS2, FINSEQ_1:1;
hence m . (i + 1) = (m . i) * (b . i) by PX1, AS2, D28; ::_thesis: verum
end;
LmTh56: m . (len nlist),b . (len nlist) are_relative_prime by AS2, LmTh5, LmTh51, X5, LmTh54, LmTh55;
set l1 = l | n;
set m1 = m | n;
KK: n <= n + 1 by NAT_1:11;
then PD02: len (l | n) = n by AS2, FINSEQ_1:59, X5;
PD11: dom (m | n) = Seg (len (m | n)) by FINSEQ_1:def_3
.= Seg n by AS2, FINSEQ_1:59, X5, KK ;
PD12: len (m | n) = n by PD11, FINSEQ_1:def_3;
1 - 1 <= n - 1 by NN2, XREAL_1:9;
then n - 1 in NAT by INT_1:3;
then reconsider nn1 = n - 1 as Nat ;
reconsider prodi1 = prodi | nn1 as FinSequence of INT ;
reconsider prodc1 = prodc | nn1 as FinSequence of INT ;
XX5: n - 1 <= n - 0 by XREAL_1:10;
then QD02: len prodi1 = nn1 by AS2, X5, FINSEQ_1:59;
QD12: len prodc1 = nn1 by XX5, AS2, X5, FINSEQ_1:59;
PD24: 1 in Seg n by NN2;
PD26X: (l | n) . 1 = l . 1 by FUNCT_1:49, PD24
.= (nlist1 . 1) `1 by FUNCT_1:49, PD24, X5 ;
QKK: n - 1 <= n - 0 by XREAL_1:10;
PD26: now__::_thesis:_for_i_being_Nat_st_1_<=_i_&_i_<=_(len_(m_|_n))_-_1_holds_
(_(m_|_n)_._i_=_m_._i_&_(l_|_n)_._i_=_l_._i_&_prodi1_._i_=_prodi_._i_&_prodc1_._i_=_prodc_._i_)
let i be Nat; ::_thesis: ( 1 <= i & i <= (len (m | n)) - 1 implies ( (m | n) . i = m . i & (l | n) . i = l . i & prodi1 . i = prodi . i & prodc1 . i = prodc . i ) )
assume PD260X: ( 1 <= i & i <= (len (m | n)) - 1 ) ; ::_thesis: ( (m | n) . i = m . i & (l | n) . i = l . i & prodi1 . i = prodi . i & prodc1 . i = prodc . i )
then PD260: ( 1 <= i & i <= len (m | n) ) by PD12, QKK, XXREAL_0:2;
then i in Seg (len (m | n)) by FINSEQ_1:1;
hence (m | n) . i = m . i by FUNCT_1:49, PD12; ::_thesis: ( (l | n) . i = l . i & prodi1 . i = prodi . i & prodc1 . i = prodc . i )
i in Seg (len (l | n)) by FINSEQ_1:1, PD260, PD02, PD12;
hence (l | n) . i = l . i by FUNCT_1:49, PD02; ::_thesis: ( prodi1 . i = prodi . i & prodc1 . i = prodc . i )
i in Seg (len prodi1) by FINSEQ_1:1, PD260X, PD12, QD02;
hence prodi1 . i = prodi . i by FUNCT_1:49, QD02; ::_thesis: prodc1 . i = prodc . i
i in Seg (len prodc1) by FINSEQ_1:1, PD260X, PD12, QD12;
hence prodc1 . i = prodc . i by FUNCT_1:49, QD12; ::_thesis: verum
end;
len (m | n) in Seg (len nlist1) by D22, PD12, FINSEQ_1:3;
then Z1: len (m | n) in Seg (len nlist) by D28;
Z2: nlist1 . (len (m | n)) = nlist . (len (m | n)) by FUNCT_1:49, D22, PD12, FINSEQ_1:3;
len (m | n) in dom nlist by FINSEQ_1:def_3, Z1;
then nlist1 . (len (m | n)) in [:INT,INT:] by FINSEQ_2:11, Z2;
then reconsider M01 = (nlist1 . (len (m | n))) `2 as Element of INT by MCART_1:10;
reconsider M1 = (prodc1 . ((len (m | n)) - 1)) * M01 as Element of INT by INT_1:def_2;
QX1: ( len (m | n) = len nlist1 & len (l | n) = len nlist1 & len prodc1 = (len nlist1) - 1 & len prodi1 = (len nlist1) - 1 & (m | n) . 1 = 1 ) by KK, FINSEQ_1:59, AS2, PD12, PD02, QD12, QD02, X5, FUNCT_1:49, PD24;
QX2: for i being Nat st 1 <= i & i <= (len (m | n)) - 1 holds
ex d, x, y being Element of INT st
( x = (nlist1 . i) `2 & (m | n) . (i + 1) = ((m | n) . i) * x & y = (m | n) . (i + 1) & d = (nlist1 . (i + 1)) `2 & prodi1 . i = ALGO_INVERSE (y,d) & prodc1 . i = y )
proof
let i be Nat; ::_thesis: ( 1 <= i & i <= (len (m | n)) - 1 implies ex d, x, y being Element of INT st
( x = (nlist1 . i) `2 & (m | n) . (i + 1) = ((m | n) . i) * x & y = (m | n) . (i + 1) & d = (nlist1 . (i + 1)) `2 & prodi1 . i = ALGO_INVERSE (y,d) & prodc1 . i = y ) )
assume XQ21: ( 1 <= i & i <= (len (m | n)) - 1 ) ; ::_thesis: ex d, x, y being Element of INT st
( x = (nlist1 . i) `2 & (m | n) . (i + 1) = ((m | n) . i) * x & y = (m | n) . (i + 1) & d = (nlist1 . (i + 1)) `2 & prodi1 . i = ALGO_INVERSE (y,d) & prodc1 . i = y )
then XQ22: (m | n) . i = m . i by PD26;
XQ23: prodi1 . i = prodi . i by PD26, XQ21;
XQ24: prodc1 . i = prodc . i by PD26, XQ21;
XQ25: 1 <= i + 1 by NAT_1:12;
i + 1 <= ((len (m | n)) - 1) + 1 by XQ21, XREAL_1:6;
then YY1: i + 1 in Seg (len (m | n)) by XQ25;
then XQ27: (m | n) . (i + 1) = m . (i + 1) by FUNCT_1:49, PD12;
XQ28: ( 1 <= i & i <= len (m | n) ) by XQ21, PD12, QKK, XXREAL_0:2;
XQ30: ( 1 <= i & i <= (len m) - 1 ) by X5, AS2, XQ21, PD12, QKK, XXREAL_0:2;
i in Seg (len nlist1) by PD12, D22, XQ28, FINSEQ_1:1;
then XQ32: nlist1 . i = nlist . i by FUNCT_1:49, D25;
nlist1 . (i + 1) = nlist . (i + 1) by FUNCT_1:49, PD12, YY1;
hence ex d, x, y being Element of INT st
( x = (nlist1 . i) `2 & (m | n) . (i + 1) = ((m | n) . i) * x & y = (m | n) . (i + 1) & d = (nlist1 . (i + 1)) `2 & prodi1 . i = ALGO_INVERSE (y,d) & prodc1 . i = y ) by XQ22, XQ23, XQ24, XQ27, XQ30, XQ32, X5; ::_thesis: verum
end;
QX4: for i being Nat st 1 <= i & i <= (len (m | n)) - 1 holds
ex u, u0, u1 being Element of INT st
( u0 = (nlist1 . (i + 1)) `1 & u1 = (nlist1 . (i + 1)) `2 & u = ((u0 - ((l | n) . i)) * (prodi1 . i)) mod u1 & (l | n) . (i + 1) = ((l | n) . i) + (u * (prodc1 . i)) )
proof
let i be Nat; ::_thesis: ( 1 <= i & i <= (len (m | n)) - 1 implies ex u, u0, u1 being Element of INT st
( u0 = (nlist1 . (i + 1)) `1 & u1 = (nlist1 . (i + 1)) `2 & u = ((u0 - ((l | n) . i)) * (prodi1 . i)) mod u1 & (l | n) . (i + 1) = ((l | n) . i) + (u * (prodc1 . i)) ) )
assume XQ21: ( 1 <= i & i <= (len (m | n)) - 1 ) ; ::_thesis: ex u, u0, u1 being Element of INT st
( u0 = (nlist1 . (i + 1)) `1 & u1 = (nlist1 . (i + 1)) `2 & u = ((u0 - ((l | n) . i)) * (prodi1 . i)) mod u1 & (l | n) . (i + 1) = ((l | n) . i) + (u * (prodc1 . i)) )
then XQ22: (l | n) . i = l . i by PD26;
XQ23: prodi1 . i = prodi . i by PD26, XQ21;
XQ24: prodc1 . i = prodc . i by PD26, XQ21;
XQ25: 1 <= i + 1 by NAT_1:12;
i + 1 <= ((len (m | n)) - 1) + 1 by XQ21, XREAL_1:6;
then YY1: i + 1 in Seg (len (m | n)) by XQ25;
then XQ27: (l | n) . (i + 1) = l . (i + 1) by FUNCT_1:49, PD12;
XQ30: ( 1 <= i & i <= (len m) - 1 ) by X5, AS2, XQ21, PD12, QKK, XXREAL_0:2;
nlist1 . (i + 1) = nlist . (i + 1) by FUNCT_1:49, PD12, YY1;
hence ex u, u0, u1 being Element of INT st
( u0 = (nlist1 . (i + 1)) `1 & u1 = (nlist1 . (i + 1)) `2 & u = ((u0 - ((l | n) . i)) * (prodi1 . i)) mod u1 & (l | n) . (i + 1) = ((l | n) . i) + (u * (prodc1 . i)) ) by XQ22, XQ23, XQ24, XQ27, XQ30, X5; ::_thesis: verum
end;
reconsider s = ((l | n) . (len (m | n))) mod M1 as Element of INT by INT_1:def_2;
QX12: 1 <= (len m) - 1 by X5, AS2, NAT_1:14, NN1;
reconsider lm1 = (len m) - 1 as Element of NAT by X5;
QX13: ( 1 <= lm1 & lm1 <= (len m) - 1 ) by X5, AS2, NAT_1:14, NN1;
consider d, x, y being Element of INT such that
QX14: ( 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 X5, AS2, NN2;
consider u, u0, u1 being Element of INT such that
QX15: ( 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 QX13, X5;
QX43: len nlist in Seg (len nlist) by FINSEQ_1:3;
QX45: M0 = b . (len nlist) by X5, AS2, QX43;
then QX37B: M0 <> 0 by QX43, AS2;
QX36A: (u0 - (l . ((len m) - 1))) * (ALGO_INVERSE (y,M0)) is Element of INT by INT_1:def_2;
consider r being Element of INT such that
QX37: u = ((u0 - (l . ((len m) - 1))) * (ALGO_INVERSE (y,M0))) + (r * M0) by LmTh4, X5, QX14, QX15, QX36A, QX37B;
QX26A: y <> 0 by QX14, X5, AS2, LmTh5A, LmTh54, LmTh55;
now__::_thesis:_ex_p,_qr_being_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)_)
percases ( len nlist1 = 1 or len nlist1 <> 1 ) ;
supposeAA1: len nlist1 = 1 ; ::_thesis: ex p, qr being 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) )
AAA1: ALGO_CRT nlist1 = (nlist1 . 1) `1 by AA1, defALGOCRT
.= (nlist . 1) `1 by FUNCT_1:49, PD24
.= l . ((len m) - 1) by AA1, AS2, X5, D23, FINSEQ_1:def_3 ;
QX27: ALGO_CRT nlist = ((l . ((len m) - 1)) + (u * y)) mod M by QX14, QX15, X5;
reconsider p = 0 as Element of INT by INT_1:def_2;
QX28: ALGO_CRT nlist1 = (l . ((len m) - 1)) + (p * y) by AAA1;
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;
M = y * M0 by X5, QX14;
then consider t being Element of INT such that
QX30: ALGO_CRT nlist = ly + (t * M) by LmTh4, QX27, QX37B, QX26A, XCMPLX_1:6;
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 X5, QX14, QX37, QX30, AAA1;
hence ex p, qr being 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 QX28; ::_thesis: verum
end;
supposeAA2: len nlist1 <> 1 ; ::_thesis: ex p, qr being 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) )
then QX7: ALGO_CRT nlist1 = s by defALGOCRT, QX1, QX2, QX4, PD26X
.= ((l | n) . (len (m | n))) mod ((prodc1 . ((len (m | n)) - 1)) * M01) ;
QX8: (l | n) . (len (l | n)) = l . (len (l | n)) by FUNCT_1:49, NN1, PD02, FINSEQ_1:3
.= l . ((len m) - 1) by X5, AS2, FINSEQ_1:59, KK ;
2 <= len nlist1 by AA2, NAT_1:23;
then 2 - 1 <= (len (m | n)) - 1 by XREAL_1:9, PD12, X1;
then QX90: ( 1 <= nn1 & nn1 <= (len (m | n)) - 1 ) by PD11, FINSEQ_1:def_3;
QX10: M01 = (nlist . (len (m | n))) `2 by FUNCT_1:49, D22, PD12, FINSEQ_1:3
.= (nlist . ((len m) - 1)) `2 by X5, AS2, PD11, FINSEQ_1:def_3 ;
consider d1, x1, y1 being Element of INT such that
QX16: ( x1 = (nlist1 . nn1) `2 & (m | n) . (nn1 + 1) = ((m | n) . nn1) * x1 & y1 = (m | n) . (nn1 + 1) & d1 = (nlist1 . (nn1 + 1)) `2 & prodi1 . nn1 = ALGO_INVERSE (y1,d1) & prodc1 . nn1 = y1 ) by QX2, QX90;
QX21: len (m | n) = (len m) - 1 by X5, AS2, PD11, FINSEQ_1:def_3;
then QX20: lm1 in Seg (len (m | n)) by QX12;
QX24: ALGO_CRT nlist1 = (l . ((len m) - 1)) mod (y1 * M01) by QX16, QX7, QX21, QX8, AS2, FINSEQ_1:59, X5, KK;
QX24A: ( ALGO_CRT nlist1 is Element of INT & l . ((len m) - 1) is Element of INT & y1 * M01 is Element of INT ) by INT_1:def_2;
QX26: y = y1 * x by QX16, X5, AS2, FUNCT_1:49, PD12, QX20, QX14;
then QX26C: y1 * M01 <> 0 by X5, AS2, LmTh5A, LmTh54, LmTh55, QX10, QX14;
consider p being Element of INT such that
QX30: ALGO_CRT nlist1 = (l . ((len m) - 1)) + (p * (y1 * M01)) by QX24, LmTh4, QX24A, QX26A, QX10, QX14, QX26;
QX27: ALGO_CRT nlist = ((l . ((len m) - 1)) + (u * (y1 * x))) mod ((prodc . ((len m) - 1)) * M0) by QX16, X5, AS2, FUNCT_1:49, PD12, QX20, QX14, QX15
.= ((l . ((len m) - 1)) + (u * (y1 * x))) mod ((y1 * x) * M0) by QX16, X5, AS2, FUNCT_1:49, PD12, QX20, QX14 ;
( ALGO_CRT nlist is Element of INT & (l . ((len m) - 1)) + (u * (y1 * x)) is Element of INT & (y1 * x) * M0 is Element of INT ) by INT_1:def_2;
then consider q being Element of INT such that
QX31: ALGO_CRT nlist = ((l . ((len m) - 1)) + (u * (y1 * x))) + (q * ((y1 * x) * M0)) by QX27, LmTh4, QX10, QX14, QX26C, XCMPLX_1:6, QX37B;
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 QX10, QX14
.= (((ALGO_CRT nlist1) - ((((l . ((len m) - 1)) * (ALGO_INVERSE (y,M0))) * y) + (p * y))) + ((r * M0) * y)) + ((u0 * (ALGO_INVERSE (y,M0))) * y) by QX26, QX37 ;
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 QX16, X5, AS2, FUNCT_1:49, PD12, QX20, QX14, QX31, QX30
.= (((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 being 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 QX30, QX26, QX10, QX14; ::_thesis: verum
end;
end;
end;
then consider p, qr being Element of INT such that
QX41: ( 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,M0 are_relative_prime by QX37B, LmTh4A, QX14, X5, QX45, LmTh56;
then y0 gcd M0 = 1 by INT_2:def_3;
then QX48: (ALGO_EXGCD (M0,y0)) `3_3 = 1 by Th2;
QX50: ((((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 QX48, Th3
.= ((((l . ((len m) - 1)) * 1) mod M0) + ((p * y) mod M0)) mod M0 by NAT_D:67
.= (ALGO_CRT nlist1) mod M0 by QX41, NAT_D:66 ;
thus for i being Nat st i in Seg (len nlist) holds
(ALGO_CRT nlist) mod (b . i) = (a . i) mod (b . i) ::_thesis: verum
proof
let i be Nat; ::_thesis: ( i in Seg (len nlist) implies (ALGO_CRT nlist) mod (b . i) = (a . i) mod (b . i) )
assume VA0: i in Seg (len nlist) ; ::_thesis: (ALGO_CRT nlist) mod (b . i) = (a . i) mod (b . i)
then VA1: ( 1 <= i & i <= len nlist ) by FINSEQ_1:1;
percases ( i = len nlist or i <> len nlist ) ;
supposeVA2: i = len nlist ; ::_thesis: (ALGO_CRT nlist) mod (b . i) = (a . i) mod (b . i)
VA22: b . i <> 0 by AS2, VA0;
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;
VA31: K2y mod (b . i) = (((qr * y) mod M0) * (M0 mod M0)) mod M0 by QX45, VA2, NAT_D:67
.= (((qr * y) mod M0) * I0) mod M0 by INT_1:50
.= I0 mod (b . i) by VA2, X5, AS2, QX43 ;
VA30: K4y mod (b . i) = ((I0 mod (b . i)) + (K3y mod (b . i))) mod (b . i) by VA31, 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 QX48, Th3, VA2, QX45
.= (u0 * 1) mod (b . i) by NAT_D:67
.= (a . i) mod (b . i) by VA2, QX43, X5, AS2, QX15 ;
VA31: ((ALGO_CRT nlist) + K1y) mod (b . i) = (((ALGO_CRT nlist) mod (b . i)) + ((ALGO_CRT nlist1) mod (b . i))) mod (b . i) by QX50, VA2, QX45, NAT_D:66
.= ((ALGO_CRT nlist) + (ALGO_CRT nlist1)) mod (b . i) by NAT_D:66 ;
VA32: ((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 NAT_D:66, VA30 ;
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 being Element of INT such that
VA33: LL = LL1 + (r * bi) by LmTh4, VA22, VA31, VA32, QX41;
reconsider LL2 = (ALGO_CRT nlist1) + (a . i) as Element of INT by INT_1:def_2;
consider s being Element of INT such that
VA34: LL = LL2 + (s * bi) by LmTh4, VA22;
reconsider LL3 = s - r as Element of INT by INT_1:def_2;
VA36: (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 VA33, VA34
.= (((a . i) mod (b . i)) + (I0 mod (b . i))) mod (b . i) by VA36, NAT_D:66
.= ((a . i) + I0) mod (b . i) by NAT_D:66
.= (a . i) mod (b . i) ; ::_thesis: verum
end;
suppose i <> len nlist ; ::_thesis: (ALGO_CRT nlist) mod (b . i) = (a . i) mod (b . i)
then i < len nlist by VA1, XXREAL_0:1;
then i + 1 <= len nlist by NAT_1:13;
then VA22P: (i + 1) - 1 <= (len nlist) - 1 by XREAL_1:9;
then VA22: ( 1 <= i & i <= len nlist1 ) by KK, FINSEQ_1:59, AS2, FINSEQ_1:1, VA0;
VA24: i in Seg (len nlist1) by FINSEQ_1:1, VA22P, AS2, X1, VA1;
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;
VA27: y mod (b . i) = 0 by X1, QX14, LmTh6, LmTh54, LmTh55, AS2, X5, VA22;
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;
VA29: (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 VA27 ;
VA30: (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 VA27 ;
VA31: ((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 NAT_D:66, VA29
.= (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 NAT_D:66, VA30
.= (ALGO_CRT nlist1) mod (b . i) ;
hence (ALGO_CRT nlist) mod (b . i) = (a . i) mod (b . i) by VA24, QX41, VA31, X400; ::_thesis: verum
end;
end;
end;
end;
end;
end;
for n being Element of NAT holds S1[n] from NAT_1:sch_1(P0, P1);
hence for nlist being non empty FinSequence of [:INT,INT:]
for a, b being FinSequence of INT st len a = len b & len a = len nlist & ( for i being Nat st i in Seg (len nlist) holds
b . i <> 0 ) & ( for i being Nat st i in Seg (len nlist) holds
( (nlist . i) `1 = a . i & (nlist . i) `2 = b . i ) ) & ( for i, j being Nat st i in Seg (len nlist) & j in Seg (len nlist) & i <> j holds
b . i,b . j are_relative_prime ) holds
for i being Nat st i in Seg (len nlist) holds
(ALGO_CRT nlist) mod (b . i) = (a . i) mod (b . i) ; ::_thesis: verum
end;
LmTh7A: for x, y, a, b being Element of INT st x mod a = y mod a & x mod b = y mod b & a,b are_relative_prime holds
x mod (a * b) = y mod (a * b)
proof
let x, y, a, b be Element of INT ; ::_thesis: ( x mod a = y mod a & x mod b = y mod b & a,b are_relative_prime implies x mod (a * b) = y mod (a * b) )
assume AS: ( x mod a = y mod a & x mod b = y mod b & a,b are_relative_prime ) ; ::_thesis: x mod (a * b) = y mod (a * b)
set g1 = x mod a;
set g2 = x mod b;
percases ( a * b = 0 or a * b <> 0 ) ;
supposeC1: a * b = 0 ; ::_thesis: x mod (a * b) = y mod (a * b)
thus x mod (a * b) = 0 by INT_1:def_10, C1
.= y mod (a * b) by C1, INT_1:def_10 ; ::_thesis: verum
end;
suppose a * b <> 0 ; ::_thesis: x mod (a * b) = y mod (a * b)
then C3: ( a <> 0 & b <> 0 ) ;
C5: y = ((y div a) * a) + (y mod a) by C3, INT_1:59;
C6: x = ((x div b) * b) + (x mod b) by C3, INT_1:59;
x - y = (((x div a) * a) + (x mod a)) - (((y div a) * a) + (y mod a)) by C3, INT_1:59, C5
.= ((x div a) - (y div a)) * a by AS ;
then a divides x - y by INT_1:def_3;
then C8: x,y are_congruent_mod a by INT_1:def_4;
x - y = (((x div b) * b) + (x mod b)) - (((y div b) * b) + (y mod b)) by C3, INT_1:59, C6
.= ((x div b) - (y div b)) * b by AS ;
then b divides x - y by INT_1:def_3;
then x,y are_congruent_mod b by INT_1:def_4;
then x,y are_congruent_mod a * b by AS, C8, INT_6:21;
then a * b divides x - y by INT_1:def_4;
then consider p being Integer such that
C11: x - y = (a * b) * p by INT_1:def_3;
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 C11
.= ((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) ; ::_thesis: verum
end;
end;
end;
theorem LmTh7: :: NTALGO_1:12
for x, y being Element of INT
for b, m being non empty FinSequence of INT st 2 <= len b & ( for i, j being Nat st i in Seg (len b) & j in Seg (len b) & i <> j holds
b . i,b . j are_relative_prime ) & ( for i being Nat st i in Seg (len b) holds
x mod (b . i) = y mod (b . i) ) & m . 1 = 1 holds
for k being Element of NAT st 1 <= k & k <= len b & ( for i being Nat st 1 <= i & i <= k holds
m . (i + 1) = (m . i) * (b . i) ) holds
x mod (m . (k + 1)) = y mod (m . (k + 1))
proof
let x, y be Element of INT ; ::_thesis: for b, m being non empty FinSequence of INT st 2 <= len b & ( for i, j being Nat st i in Seg (len b) & j in Seg (len b) & i <> j holds
b . i,b . j are_relative_prime ) & ( for i being Nat st i in Seg (len b) holds
x mod (b . i) = y mod (b . i) ) & m . 1 = 1 holds
for k being Element of NAT st 1 <= k & k <= len b & ( for i being Nat st 1 <= i & i <= k holds
m . (i + 1) = (m . i) * (b . i) ) holds
x mod (m . (k + 1)) = y mod (m . (k + 1))
let b, m be non empty FinSequence of INT ; ::_thesis: ( 2 <= len b & ( for i, j being Nat st i in Seg (len b) & j in Seg (len b) & i <> j holds
b . i,b . j are_relative_prime ) & ( for i being Nat st i in Seg (len b) holds
x mod (b . i) = y mod (b . i) ) & m . 1 = 1 implies for k being Element of NAT st 1 <= k & k <= len b & ( for i being Nat st 1 <= i & i <= k holds
m . (i + 1) = (m . i) * (b . i) ) holds
x mod (m . (k + 1)) = y mod (m . (k + 1)) )
assume A1: 2 <= len b ; ::_thesis: ( ex i, j being Nat st
( i in Seg (len b) & j in Seg (len b) & i <> j & not b . i,b . j are_relative_prime ) or ex i being Nat st
( i in Seg (len b) & not x mod (b . i) = y mod (b . i) ) or not m . 1 = 1 or for k being Element of NAT st 1 <= k & k <= len b & ( for i being Nat st 1 <= i & i <= k holds
m . (i + 1) = (m . i) * (b . i) ) holds
x mod (m . (k + 1)) = y mod (m . (k + 1)) )
assume A4: for i, j being Nat st i in Seg (len b) & j in Seg (len b) & i <> j holds
b . i,b . j are_relative_prime ; ::_thesis: ( ex i being Nat st
( i in Seg (len b) & not x mod (b . i) = y mod (b . i) ) or not m . 1 = 1 or for k being Element of NAT st 1 <= k & k <= len b & ( for i being Nat st 1 <= i & i <= k holds
m . (i + 1) = (m . i) * (b . i) ) holds
x mod (m . (k + 1)) = y mod (m . (k + 1)) )
assume A2: for i being Nat st i in Seg (len b) holds
x mod (b . i) = y mod (b . i) ; ::_thesis: ( not m . 1 = 1 or for k being Element of NAT st 1 <= k & k <= len b & ( for i being Nat st 1 <= i & i <= k holds
m . (i + 1) = (m . i) * (b . i) ) holds
x mod (m . (k + 1)) = y mod (m . (k + 1)) )
assume A3: m . 1 = 1 ; ::_thesis: for k being Element of NAT st 1 <= k & k <= len b & ( for i being Nat st 1 <= i & i <= k holds
m . (i + 1) = (m . i) * (b . i) ) holds
x mod (m . (k + 1)) = y mod (m . (k + 1))
defpred S1[ Nat] means ( 1 <= $1 & $1 <= len b & ( for i being 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 ;
P0: S1[ 0 ] ;
P1: for k being Element of NAT st S1[k] holds
S1[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] )
assume P11: S1[k] ; ::_thesis: S1[k + 1]
assume P12: ( 1 <= k + 1 & k + 1 <= len b & ( for i being Nat st 1 <= i & i <= k + 1 holds
m . (i + 1) = (m . i) * (b . i) ) ) ; ::_thesis: x mod (m . ((k + 1) + 1)) = y mod (m . ((k + 1) + 1))
P14: k <= k + 1 by NAT_1:12;
percases ( k = 0 or k <> 0 ) ;
supposeP15: k = 0 ; ::_thesis: x mod (m . ((k + 1) + 1)) = y mod (m . ((k + 1) + 1))
P16: m . ((k + 1) + 1) = (m . 1) * (b . 1) by P12, P15
.= b . 1 by A3 ;
( 1 <= 1 & 1 <= len b ) by NAT_1:14;
then P18: 1 in Seg (len b) ;
thus x mod (m . ((k + 1) + 1)) = y mod (m . ((k + 1) + 1)) by P16, P18, A2; ::_thesis: verum
end;
supposeP181: k <> 0 ; ::_thesis: x mod (m . ((k + 1) + 1)) = y mod (m . ((k + 1) + 1))
(k + 1) - 1 <= (len b) - 1 by P12, XREAL_1:9;
then P19: ( 1 <= k & k <= (len b) - 1 ) by P181, NAT_1:14;
XX1: now__::_thesis:_for_i_being_Nat_st_1_<=_i_&_i_<=_k_holds_
m_._(i_+_1)_=_(m_._i)_*_(b_._i)
let i be Nat; ::_thesis: ( 1 <= i & i <= k implies m . (i + 1) = (m . i) * (b . i) )
assume ( 1 <= i & i <= k ) ; ::_thesis: m . (i + 1) = (m . i) * (b . i)
then ( 1 <= i & i <= k + 1 ) by NAT_1:12;
hence m . (i + 1) = (m . i) * (b . i) by P12; ::_thesis: verum
end;
P22: m . ((k + 1) + 1) = (m . (k + 1)) * (b . (k + 1)) by P12;
k + 1 in Seg (len b) by P12;
then P23: x mod (b . (k + 1)) = y mod (b . (k + 1)) by A2;
P24: m . (k + 1),b . (k + 1) are_relative_prime by LmTh5, XX1, P19, A1, A4, A3, P12;
( m . (k + 1) is Element of INT & b . (k + 1) is Element of INT ) by INT_1:def_2;
hence x mod (m . ((k + 1) + 1)) = y mod (m . ((k + 1) + 1)) by P22, P23, P11, NAT_1:14, P181, P12, P14, XXREAL_0:2, XX1, P24, LmTh7A; ::_thesis: verum
end;
end;
end;
for k being Element of NAT holds S1[k] from NAT_1:sch_1(P0, P1);
hence for k being Element of NAT st 1 <= k & k <= len b & ( for i being Nat st 1 <= i & i <= k holds
m . (i + 1) = (m . i) * (b . i) ) holds
x mod (m . (k + 1)) = y mod (m . (k + 1)) ; ::_thesis: verum
end;
theorem LmTh8: :: NTALGO_1:13
for b being FinSequence of INT st len b = 1 holds
Product b = b . 1
proof
let b be FinSequence of INT ; ::_thesis: ( len b = 1 implies Product b = b . 1 )
assume len b = 1 ; ::_thesis: Product b = b . 1
then b = <*(b . 1)*> by FINSEQ_1:40;
hence Product b = b . 1 by RVSUM_1:95; ::_thesis: verum
end;
theorem LmTh9: :: NTALGO_1:14
for b being FinSequence of INT ex m being non empty FinSequence of INT st
( len m = (len b) + 1 & m . 1 = 1 & ( for i being Nat st 1 <= i & i <= len b holds
m . (i + 1) = (m . i) * (b . i) ) & Product b = m . ((len b) + 1) )
proof
defpred S1[ Nat] means for b being FinSequence of INT st len b = $1 holds
ex m being non empty FinSequence of INT st
( len m = (len b) + 1 & m . 1 = 1 & ( for i being Nat st 1 <= i & i <= len b holds
m . (i + 1) = (m . i) * (b . i) ) & Product b = m . ((len b) + 1) );
P0: S1[ 0 ]
proof
let b be FinSequence of INT ; ::_thesis: ( len b = 0 implies ex m being non empty FinSequence of INT st
( len m = (len b) + 1 & m . 1 = 1 & ( for i being Nat st 1 <= i & i <= len b holds
m . (i + 1) = (m . i) * (b . i) ) & Product b = m . ((len b) + 1) ) )
assume A1: len b = 0 ; ::_thesis: ex m being non empty FinSequence of INT st
( len m = (len b) + 1 & m . 1 = 1 & ( for i being Nat st 1 <= i & i <= len b holds
m . (i + 1) = (m . i) * (b . i) ) & Product b = m . ((len b) + 1) )
I0: 1 in INT by INT_1:def_2;
rng <*1*> = {1} by FINSEQ_1:39;
then rng <*1*> c= INT by ZFMISC_1:31, I0;
then reconsider m = <*1*> as non empty FinSequence of INT by FINSEQ_1:def_4;
P0: len m = (len b) + 1 by A1, FINSEQ_1:40;
P1: m . 1 = 1 by FINSEQ_1:40;
P2: for i being Nat st 1 <= i & i <= len b holds
m . (i + 1) = (m . i) * (b . i) by A1;
b = <*> REAL by A1;
hence ex m being non empty FinSequence of INT st
( len m = (len b) + 1 & m . 1 = 1 & ( for i being Nat st 1 <= i & i <= len b holds
m . (i + 1) = (m . i) * (b . i) ) & Product b = m . ((len b) + 1) ) by P0, P1, P2, A1, RVSUM_1:94; ::_thesis: verum
end;
P1: for k being Element of NAT st S1[k] holds
S1[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A1: S1[k] ; ::_thesis: S1[k + 1]
let b be FinSequence of INT ; ::_thesis: ( len b = k + 1 implies ex m being non empty FinSequence of INT st
( len m = (len b) + 1 & m . 1 = 1 & ( for i being Nat st 1 <= i & i <= len b holds
m . (i + 1) = (m . i) * (b . i) ) & Product b = m . ((len b) + 1) ) )
assume A2: len b = k + 1 ; ::_thesis: ex m being non empty FinSequence of INT st
( len m = (len b) + 1 & m . 1 = 1 & ( for i being Nat st 1 <= i & i <= len b holds
m . (i + 1) = (m . i) * (b . i) ) & Product b = m . ((len b) + 1) )
set b1 = b | k;
P2: len (b | k) = k by FINSEQ_1:59, A2, NAT_1:12;
then consider m1 being non empty FinSequence of INT such that
P4: ( (len (b | k)) + 1 = len m1 & m1 . 1 = 1 & ( for i being Nat st 1 <= i & i <= len (b | k) holds
m1 . (i + 1) = (m1 . i) * ((b | k) . i) ) & Product (b | k) = m1 . ((len (b | k)) + 1) ) by A1;
set m = m1 ^ <*((Product (b | k)) * (b . (len b)))*>;
P5Z: (Product (b | k)) * (b . (len b)) in INT by P4, INT_1:def_2;
P5W: rng <*((Product (b | k)) * (b . (len b)))*> = {((Product (b | k)) * (b . (len b)))} by FINSEQ_1:39;
then P5Q: rng <*((Product (b | k)) * (b . (len b)))*> c= INT by ZFMISC_1:31, P5Z;
P5: len (m1 ^ <*((Product (b | k)) * (b . (len b)))*>) = (len m1) + (len <*((Product (b | k)) * (b . (len b)))*>) by FINSEQ_1:22
.= ((len (b | k)) + 1) + 1 by P4, FINSEQ_1:40
.= (len b) + 1 by FINSEQ_1:59, A2, NAT_1:12 ;
VV2: rng (m1 ^ <*((Product (b | k)) * (b . (len b)))*>) = (rng m1) \/ {((Product (b | k)) * (b . (len b)))} by FINSEQ_1:31, P5W;
rng m1 c= INT by FINSEQ_1:def_4;
then rng (m1 ^ <*((Product (b | k)) * (b . (len b)))*>) c= INT by P5W, VV2, P5Q, XBOOLE_1:8;
then reconsider m = m1 ^ <*((Product (b | k)) * (b . (len b)))*> as non empty FinSequence of INT by FINSEQ_1:def_4;
P5B: len m1 = (len (b | k)) + 1 by P4
.= k + 1 by FINSEQ_1:59, A2, NAT_1:12 ;
( 1 <= 1 & 1 <= k + 1 ) by NAT_1:12;
then 1 in Seg (len m1) by P5B;
then 1 in dom m1 by FINSEQ_1:def_3;
then P8: m . 1 = 1 by P4, FINSEQ_1:def_7;
P9: for i being Nat st 1 <= i & i <= len b holds
m . (i + 1) = (m . i) * (b . i)
proof
let i be Nat; ::_thesis: ( 1 <= i & i <= len b implies m . (i + 1) = (m . i) * (b . i) )
assume P10: ( 1 <= i & i <= len b ) ; ::_thesis: m . (i + 1) = (m . i) * (b . i)
percases ( i = len b or i <> len b ) ;
supposeP11: i = len b ; ::_thesis: m . (i + 1) = (m . i) * (b . i)
(len (b | k)) + 1 in Seg (len m1) by P2, P5B, FINSEQ_1:4;
then (len (b | k)) + 1 in dom m1 by FINSEQ_1:def_3;
then P13: m1 . ((len (b | k)) + 1) = m . ((len (b | k)) + 1) by FINSEQ_1:def_7
.= m . i by A2, FINSEQ_1:59, NAT_1:12, P11 ;
1 in Seg 1 ;
then P13C: 1 in dom <*((Product (b | k)) * (b . (len b)))*> by FINSEQ_1:38;
thus m . (i + 1) = <*((Product (b | k)) * (b . (len b)))*> . 1 by FINSEQ_1:def_7, P11, A2, P5B, P13C
.= (m . i) * (b . i) by P13, P11, P4, FINSEQ_1:40 ; ::_thesis: verum
end;
suppose i <> len b ; ::_thesis: m . (i + 1) = (m . i) * (b . i)
then P12D: i < len b by P10, XXREAL_0:1;
then P12A: ( 1 <= i & i <= len (b | k) ) by P2, A2, NAT_1:13, P10;
then P13: m1 . (i + 1) = (m1 . i) * ((b | k) . i) by P4;
i in Seg (len m1) by FINSEQ_1:1, P10, A2, P5B;
then P13B: i in dom m1 by FINSEQ_1:def_3;
P13E: i + 1 <= len m1 by A2, P5B, P12D, NAT_1:13;
1 <= i + 1 by NAT_1:12;
then i + 1 in Seg (len m1) by P13E;
then P13C: i + 1 in dom m1 by FINSEQ_1:def_3;
i in Seg k by P12A, FINSEQ_1:1, P2;
then P15: b . i = (b | k) . i by FUNCT_1:49;
P16: m . i = m1 . i by FINSEQ_1:def_7, P13B;
thus m . (i + 1) = (m . i) * (b . i) by P13, FINSEQ_1:def_7, P13C, P15, P16; ::_thesis: verum
end;
end;
end;
b | (k + 1) = (b | k) ^ <*(b . (len b))*> by INT_6:5, A2;
then P17: b = (b | k) ^ <*(b . (len b))*> by FINSEQ_1:58, A2;
len b in Seg (len m1) by FINSEQ_1:4, A2, P5B;
then P18: len b in dom m1 by FINSEQ_1:def_3;
P19: ( 1 <= len b & len b <= len b ) by A2, NAT_1:12;
Product b = (m1 . ((len (b | k)) + 1)) * (b . (len b)) by P4, RVSUM_1:96, P17
.= (m1 . (len b)) * (b . (len b)) by A2, FINSEQ_1:59, NAT_1:12
.= (m . (len b)) * (b . (len b)) by FINSEQ_1:def_7, P18
.= m . ((len b) + 1) by P9, P19 ;
hence ex m being non empty FinSequence of INT st
( len m = (len b) + 1 & m . 1 = 1 & ( for i being Nat st 1 <= i & i <= len b holds
m . (i + 1) = (m . i) * (b . i) ) & Product b = m . ((len b) + 1) ) by P5, P8, P9; ::_thesis: verum
end;
for k being Element of NAT holds S1[k] from NAT_1:sch_1(P0, P1);
hence for b being FinSequence of INT ex m being non empty FinSequence of INT st
( len m = (len b) + 1 & m . 1 = 1 & ( for i being Nat st 1 <= i & i <= len b holds
m . (i + 1) = (m . i) * (b . i) ) & Product b = m . ((len b) + 1) ) ; ::_thesis: verum
end;
theorem :: NTALGO_1:15
for nlist being non empty FinSequence of [:INT,INT:]
for a, b being non empty FinSequence of INT
for x, y being Element of INT st len a = len b & len a = len nlist & ( for i being Nat st i in Seg (len nlist) holds
b . i <> 0 ) & ( for i being Nat st i in Seg (len nlist) holds
( (nlist . i) `1 = a . i & (nlist . i) `2 = b . i ) ) & ( for i, j being Nat st i in Seg (len nlist) & j in Seg (len nlist) & i <> j holds
b . i,b . j are_relative_prime ) & ( for i being Nat st i in Seg (len nlist) holds
x mod (b . i) = (a . i) mod (b . i) ) & y = Product b holds
(ALGO_CRT nlist) mod y = x mod y
proof
let nlist be non empty FinSequence of [:INT,INT:]; ::_thesis: for a, b being non empty FinSequence of INT
for x, y being Element of INT st len a = len b & len a = len nlist & ( for i being Nat st i in Seg (len nlist) holds
b . i <> 0 ) & ( for i being Nat st i in Seg (len nlist) holds
( (nlist . i) `1 = a . i & (nlist . i) `2 = b . i ) ) & ( for i, j being Nat st i in Seg (len nlist) & j in Seg (len nlist) & i <> j holds
b . i,b . j are_relative_prime ) & ( for i being Nat st i in Seg (len nlist) holds
x mod (b . i) = (a . i) mod (b . i) ) & y = Product b holds
(ALGO_CRT nlist) mod y = x mod y
let a, b be non empty FinSequence of INT ; ::_thesis: for x, y being Element of INT st len a = len b & len a = len nlist & ( for i being Nat st i in Seg (len nlist) holds
b . i <> 0 ) & ( for i being Nat st i in Seg (len nlist) holds
( (nlist . i) `1 = a . i & (nlist . i) `2 = b . i ) ) & ( for i, j being Nat st i in Seg (len nlist) & j in Seg (len nlist) & i <> j holds
b . i,b . j are_relative_prime ) & ( for i being Nat st i in Seg (len nlist) holds
x mod (b . i) = (a . i) mod (b . i) ) & y = Product b holds
(ALGO_CRT nlist) mod y = x mod y
let x, y be Element of INT ; ::_thesis: ( len a = len b & len a = len nlist & ( for i being Nat st i in Seg (len nlist) holds
b . i <> 0 ) & ( for i being Nat st i in Seg (len nlist) holds
( (nlist . i) `1 = a . i & (nlist . i) `2 = b . i ) ) & ( for i, j being Nat st i in Seg (len nlist) & j in Seg (len nlist) & i <> j holds
b . i,b . j are_relative_prime ) & ( for i being Nat st i in Seg (len nlist) holds
x mod (b . i) = (a . i) mod (b . i) ) & y = Product b implies (ALGO_CRT nlist) mod y = x mod y )
assume A1: ( len a = len b & len a = len nlist ) ; ::_thesis: ( ex i being Nat st
( i in Seg (len nlist) & not b . i <> 0 ) or ex i being Nat st
( i in Seg (len nlist) & not ( (nlist . i) `1 = a . i & (nlist . i) `2 = b . i ) ) or ex i, j being Nat st
( i in Seg (len nlist) & j in Seg (len nlist) & i <> j & not b . i,b . j are_relative_prime ) or ex i being Nat st
( i in Seg (len nlist) & not x mod (b . i) = (a . i) mod (b . i) ) or not y = Product b or (ALGO_CRT nlist) mod y = x mod y )
assume A2: for i being Nat st i in Seg (len nlist) holds
b . i <> 0 ; ::_thesis: ( ex i being Nat st
( i in Seg (len nlist) & not ( (nlist . i) `1 = a . i & (nlist . i) `2 = b . i ) ) or ex i, j being Nat st
( i in Seg (len nlist) & j in Seg (len nlist) & i <> j & not b . i,b . j are_relative_prime ) or ex i being Nat st
( i in Seg (len nlist) & not x mod (b . i) = (a . i) mod (b . i) ) or not y = Product b or (ALGO_CRT nlist) mod y = x mod y )
assume A3: for i being Nat st i in Seg (len nlist) holds
( (nlist . i) `1 = a . i & (nlist . i) `2 = b . i ) ; ::_thesis: ( ex i, j being Nat st
( i in Seg (len nlist) & j in Seg (len nlist) & i <> j & not b . i,b . j are_relative_prime ) or ex i being Nat st
( i in Seg (len nlist) & not x mod (b . i) = (a . i) mod (b . i) ) or not y = Product b or (ALGO_CRT nlist) mod y = x mod y )
assume A4: for i, j being Nat st i in Seg (len nlist) & j in Seg (len nlist) & i <> j holds
b . i,b . j are_relative_prime ; ::_thesis: ( ex i being Nat st
( i in Seg (len nlist) & not x mod (b . i) = (a . i) mod (b . i) ) or not y = Product b or (ALGO_CRT nlist) mod y = x mod y )
assume A5: for i being Nat st i in Seg (len nlist) holds
x mod (b . i) = (a . i) mod (b . i) ; ::_thesis: ( not y = Product b or (ALGO_CRT nlist) mod y = x mod y )
assume A6: y = Product b ; ::_thesis: (ALGO_CRT nlist) mod y = x mod y
P2: for i being Nat st i in Seg (len nlist) holds
(ALGO_CRT nlist) mod (b . i) = x mod (b . i)
proof
let i be Nat; ::_thesis: ( i in Seg (len nlist) implies (ALGO_CRT nlist) mod (b . i) = x mod (b . i) )
assume P21: i in Seg (len nlist) ; ::_thesis: (ALGO_CRT nlist) mod (b . i) = x mod (b . i)
hence (ALGO_CRT nlist) mod (b . i) = (a . i) mod (b . i) by Th4, A1, A2, A3, A4
.= x mod (b . i) by A5, P21 ;
::_thesis: verum
end;
percases ( len nlist = 1 or len nlist <> 1 ) ;
supposeP3: len nlist = 1 ; ::_thesis: (ALGO_CRT nlist) mod y = x mod y
then P5: 1 in Seg (len nlist) ;
thus (ALGO_CRT nlist) mod y = (ALGO_CRT nlist) mod (b . 1) by P3, A1, LmTh8, A6
.= x mod (b . 1) by P2, P5
.= x mod y by P3, A1, LmTh8, A6 ; ::_thesis: verum
end;
supposeP4: len nlist <> 1 ; ::_thesis: (ALGO_CRT nlist) mod y = x mod y
P5: 2 <= len nlist by P4, NAT_1:23;
P6: 2 <= len b by A1, P4, NAT_1:23;
consider m being non empty FinSequence of INT such that
P7: ( len m = (len b) + 1 & m . 1 = 1 & ( for i being Nat st 1 <= i & i <= len b holds
m . (i + 1) = (m . i) * (b . i) ) & Product b = m . ((len b) + 1) ) by LmTh9;
( 1 <= len b & len b <= len b ) by P6, XXREAL_0:2;
hence (ALGO_CRT nlist) mod y = x mod y by A6, P7, LmTh7, A1, A4, P2, P5; ::_thesis: verum
end;
end;
end;