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_coprime ) holds
for i being Nat st i in Seg (len nlist) holds
(ALGO_CRT nlist) mod (b . i) = (a . i) mod (b . i);
A1:
S1[ 0 ]
;
A2:
for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be
Nat;
( S1[n] implies S1[n + 1] )
assume A3:
S1[
n]
;
S1[n + 1]
let nlist be non
empty FinSequence of
[:INT,INT:];
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_coprime ) 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 ;
( 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_coprime ) implies for i being Nat st i in Seg (len nlist) holds
(ALGO_CRT nlist) mod (b . i) = (a . i) mod (b . i) )
assume A4:
(
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_coprime ) )
;
for i being Nat st i in Seg (len nlist) holds
(ALGO_CRT nlist) mod (b . i) = (a . i) mod (b . i)
per cases
( n = 0 or n <> 0 )
;
suppose A8:
n <> 0
;
for i being Nat st i in Seg (len nlist) holds
(ALGO_CRT nlist) mod (b . i) = (a . i) mod (b . i)then A9:
1
<= n
by NAT_1:14;
A10:
len nlist <> 1
by A4, A8;
reconsider nlist1 =
nlist | n as
FinSequence of
[:INT,INT:] ;
reconsider a1 =
a | n as
FinSequence of
INT ;
reconsider b1 =
b | n as
FinSequence of
INT ;
A11:
n <= n + 1
by NAT_1:11;
then A12:
len a1 = n
by A4, FINSEQ_1:59;
A13:
len nlist1 = n
by A11, A4, FINSEQ_1:59;
reconsider nlist1 =
nlist1 as non
empty FinSequence of
[:INT,INT:] by A8;
A14:
dom nlist1 =
Seg (len nlist1)
by FINSEQ_1:def 3
.=
Seg n
by A11, A4, FINSEQ_1:59
;
n in NAT
by ORDINAL1:def 12;
then A15:
len nlist1 = n
by A14, FINSEQ_1:def 3;
then A16:
Seg (len nlist1) c= Seg (len nlist)
by A11, A4, FINSEQ_1:5;
A17:
(
len nlist1 = n &
len a1 = len b1 &
len a1 = len nlist1 )
by A12, A11, A4, FINSEQ_1:59;
A18:
for
i being
Nat st
i in Seg (len nlist1) holds
b1 . i <> 0
A20:
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;
( i in Seg (len nlist1) implies ( (nlist1 . i) `1 = a1 . i & (nlist1 . i) `2 = b1 . i ) )
assume A21:
i in Seg (len nlist1)
;
( (nlist1 . i) `1 = a1 . i & (nlist1 . i) `2 = b1 . i )
A22:
(nlist1 . i) `1 =
(nlist . i) `1
by A21, A15, FUNCT_1:49
.=
a . i
by A21, A16, A4
.=
a1 . i
by A21, A15, FUNCT_1:49
;
(nlist1 . i) `2 =
(nlist . i) `2
by A21, A15, FUNCT_1:49
.=
b . i
by A21, A16, A4
.=
b1 . i
by A21, A15, FUNCT_1:49
;
hence
(
(nlist1 . i) `1 = a1 . i &
(nlist1 . i) `2 = b1 . i )
by A22;
verum
end; A23:
for
i,
j being
Nat st
i in Seg (len nlist1) &
j in Seg (len nlist1) &
i <> j holds
b1 . i,
b1 . j are_coprime
proof
let i,
j be
Nat;
( i in Seg (len nlist1) & j in Seg (len nlist1) & i <> j implies b1 . i,b1 . j are_coprime )
assume A24:
(
i in Seg (len nlist1) &
j in Seg (len nlist1) &
i <> j )
;
b1 . i,b1 . j are_coprime
A25:
b . i = b1 . i
by A24, A15, FUNCT_1:49;
b . j = b1 . j
by A24, A15, FUNCT_1:49;
hence
b1 . i,
b1 . j are_coprime
by A25, A24, A16, A4;
verum
end; A26:
for
i being
Nat st
i in Seg (len nlist1) holds
(ALGO_CRT nlist1) mod (b . i) = (a . i) mod (b . i)
consider m,
l,
prodc,
prodi being
FinSequence of
INT ,
M0,
M being
Element of
INT such that A28:
(
len m = len nlist &
len l = len nlist &
len prodc = (len nlist) - 1 &
len prodi = (len nlist) - 1 &
m . 1
= 1 & ( for
i 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 A10, Def4;
A29:
1
+ 1
<= n + 1
by A9, XREAL_1:6;
reconsider lb1 =
(len b) - 1 as
Nat by A4;
A30:
( 1
<= lb1 &
lb1 <= lb1 )
by A4, A8, NAT_1:14;
A31:
for
i being
Nat st 1
<= i &
i <= lb1 holds
m . (i + 1) = (m . i) * (b . i)
A34:
m . (len nlist),
b . (len nlist) are_coprime
by A4, Lm16, A29, A28, A30, A31;
reconsider nn =
n as
Element of
NAT by ORDINAL1:def 12;
set l1 =
l | nn;
set m1 =
m | nn;
A35:
n <= n + 1
by NAT_1:11;
then A36:
len (l | nn) = n
by A4, A28, FINSEQ_1:59;
A37:
dom (m | nn) =
Seg (len (m | nn))
by FINSEQ_1:def 3
.=
Seg n
by A4, A28, A35, FINSEQ_1:59
;
A38:
len (m | nn) = n
by A37, FINSEQ_1:def 3;
1
- 1
<= n - 1
by A9, XREAL_1:9;
then reconsider nn1 =
n - 1 as
Element of
NAT by INT_1:3;
reconsider prodi1 =
prodi | nn1 as
FinSequence of
INT ;
reconsider prodc1 =
prodc | nn1 as
FinSequence of
INT ;
A39:
n - 1
<= n - 0
by XREAL_1:10;
then A40:
len prodi1 = nn1
by A4, A28, FINSEQ_1:59;
A41:
len prodc1 = nn1
by A39, A4, A28, FINSEQ_1:59;
A42:
1
in Seg n
by A9;
A43:
(l | nn) . 1 =
l . 1
by A42, FUNCT_1:49
.=
(nlist1 . 1) `1
by A42, A28, FUNCT_1:49
;
A44:
n - 1
<= n - 0
by XREAL_1:10;
A45:
now for i being Nat st 1 <= i & i <= (len (m | nn)) - 1 holds
( (m | nn) . i = m . i & (l | nn) . i = l . i & prodi1 . i = prodi . i & prodc1 . i = prodc . i )let i be
Nat;
( 1 <= i & i <= (len (m | nn)) - 1 implies ( (m | nn) . i = m . i & (l | nn) . i = l . i & prodi1 . i = prodi . i & prodc1 . i = prodc . i ) )assume A46:
( 1
<= i &
i <= (len (m | nn)) - 1 )
;
( (m | nn) . i = m . i & (l | nn) . i = l . i & prodi1 . i = prodi . i & prodc1 . i = prodc . i )then A47:
( 1
<= i &
i <= len (m | nn) )
by A38, A44, XXREAL_0:2;
then
i in Seg (len (m | nn))
;
hence
(m | nn) . i = m . i
by A38, FUNCT_1:49;
( (l | nn) . i = l . i & prodi1 . i = prodi . i & prodc1 . i = prodc . i )
i in Seg (len (l | nn))
by A47, A36, A38;
hence
(l | nn) . i = l . i
by A36, FUNCT_1:49;
( prodi1 . i = prodi . i & prodc1 . i = prodc . i )
i in Seg (len prodi1)
by A46, A38, A40;
hence
prodi1 . i = prodi . i
by A40, FUNCT_1:49;
prodc1 . i = prodc . i
i in Seg (len prodc1)
by A46, A38, A41;
hence
prodc1 . i = prodc . i
by A41, FUNCT_1:49;
verum end;
len (m | nn) in Seg (len nlist1)
by A13, A38, FINSEQ_1:3;
then A48:
len (m | nn) in Seg (len nlist)
by A16;
A49:
nlist1 . (len (m | nn)) = nlist . (len (m | nn))
by A13, A38, FINSEQ_1:3, FUNCT_1:49;
len (m | nn) in dom nlist
by A48, FINSEQ_1:def 3;
then
nlist1 . (len (m | nn)) in [:INT,INT:]
by A49, FINSEQ_2:11;
then reconsider M01 =
(nlist1 . (len (m | nn))) `2 as
Element of
INT by MCART_1:10;
reconsider M1 =
(prodc1 . ((len (m | nn)) - 1)) * M01 as
Element of
INT by INT_1:def 2;
A50:
(
len (m | nn) = len nlist1 &
len (l | nn) = len nlist1 &
len prodc1 = (len nlist1) - 1 &
len prodi1 = (len nlist1) - 1 &
(m | nn) . 1
= 1 )
by A35, A4, A38, A36, A41, A40, A28, A42, FINSEQ_1:59, FUNCT_1:49;
A51:
for
i being
Nat st 1
<= i &
i <= (len (m | nn)) - 1 holds
ex
d,
x,
y being
Element of
INT st
(
x = (nlist1 . i) `2 &
(m | nn) . (i + 1) = ((m | nn) . i) * x &
y = (m | nn) . (i + 1) &
d = (nlist1 . (i + 1)) `2 &
prodi1 . i = ALGO_INVERSE (
y,
d) &
prodc1 . i = y )
proof
let i be
Nat;
( 1 <= i & i <= (len (m | nn)) - 1 implies ex d, x, y being Element of INT st
( x = (nlist1 . i) `2 & (m | nn) . (i + 1) = ((m | nn) . i) * x & y = (m | nn) . (i + 1) & d = (nlist1 . (i + 1)) `2 & prodi1 . i = ALGO_INVERSE (y,d) & prodc1 . i = y ) )
assume A52:
( 1
<= i &
i <= (len (m | nn)) - 1 )
;
ex d, x, y being Element of INT st
( x = (nlist1 . i) `2 & (m | nn) . (i + 1) = ((m | nn) . i) * x & y = (m | nn) . (i + 1) & d = (nlist1 . (i + 1)) `2 & prodi1 . i = ALGO_INVERSE (y,d) & prodc1 . i = y )
then A53:
(m | nn) . i = m . i
by A45;
A54:
prodi1 . i = prodi . i
by A45, A52;
A55:
prodc1 . i = prodc . i
by A45, A52;
A56:
1
<= i + 1
by NAT_1:12;
i + 1
<= ((len (m | nn)) - 1) + 1
by A52, XREAL_1:6;
then A57:
i + 1
in Seg (len (m | nn))
by A56;
then A58:
(m | nn) . (i + 1) = m . (i + 1)
by A38, FUNCT_1:49;
A59:
( 1
<= i &
i <= len (m | nn) )
by A52, A38, A44, XXREAL_0:2;
A60:
( 1
<= i &
i <= (len m) - 1 )
by A28, A4, A52, A38, A44, XXREAL_0:2;
i in Seg (len nlist1)
by A38, A13, A59;
then A61:
nlist1 . i = nlist . i
by A15, FUNCT_1:49;
nlist1 . (i + 1) = nlist . (i + 1)
by A38, A57, FUNCT_1:49;
hence
ex
d,
x,
y being
Element of
INT st
(
x = (nlist1 . i) `2 &
(m | nn) . (i + 1) = ((m | nn) . i) * x &
y = (m | nn) . (i + 1) &
d = (nlist1 . (i + 1)) `2 &
prodi1 . i = ALGO_INVERSE (
y,
d) &
prodc1 . i = y )
by A53, A54, A55, A58, A60, A61, A28;
verum
end; A62:
for
i being
Nat st 1
<= i &
i <= (len (m | nn)) - 1 holds
ex
u,
u0,
u1 being
Element of
INT st
(
u0 = (nlist1 . (i + 1)) `1 &
u1 = (nlist1 . (i + 1)) `2 &
u = ((u0 - ((l | nn) . i)) * (prodi1 . i)) mod u1 &
(l | nn) . (i + 1) = ((l | nn) . i) + (u * (prodc1 . i)) )
proof
let i be
Nat;
( 1 <= i & i <= (len (m | nn)) - 1 implies ex u, u0, u1 being Element of INT st
( u0 = (nlist1 . (i + 1)) `1 & u1 = (nlist1 . (i + 1)) `2 & u = ((u0 - ((l | nn) . i)) * (prodi1 . i)) mod u1 & (l | nn) . (i + 1) = ((l | nn) . i) + (u * (prodc1 . i)) ) )
assume A63:
( 1
<= i &
i <= (len (m | nn)) - 1 )
;
ex u, u0, u1 being Element of INT st
( u0 = (nlist1 . (i + 1)) `1 & u1 = (nlist1 . (i + 1)) `2 & u = ((u0 - ((l | nn) . i)) * (prodi1 . i)) mod u1 & (l | nn) . (i + 1) = ((l | nn) . i) + (u * (prodc1 . i)) )
then A64:
(l | nn) . i = l . i
by A45;
A65:
prodi1 . i = prodi . i
by A45, A63;
A66:
prodc1 . i = prodc . i
by A45, A63;
A67:
1
<= i + 1
by NAT_1:12;
i + 1
<= ((len (m | nn)) - 1) + 1
by A63, XREAL_1:6;
then A68:
i + 1
in Seg (len (m | nn))
by A67;
then A69:
(l | nn) . (i + 1) = l . (i + 1)
by A38, FUNCT_1:49;
A70:
( 1
<= i &
i <= (len m) - 1 )
by A28, A4, A63, A38, A44, XXREAL_0:2;
nlist1 . (i + 1) = nlist . (i + 1)
by A38, A68, FUNCT_1:49;
hence
ex
u,
u0,
u1 being
Element of
INT st
(
u0 = (nlist1 . (i + 1)) `1 &
u1 = (nlist1 . (i + 1)) `2 &
u = ((u0 - ((l | nn) . i)) * (prodi1 . i)) mod u1 &
(l | nn) . (i + 1) = ((l | nn) . i) + (u * (prodc1 . i)) )
by A64, A65, A66, A69, A70, A28;
verum
end; reconsider s =
((l | nn) . (len (m | nn))) mod M1 as
Element of
INT by INT_1:def 2;
A71:
1
<= (len m) - 1
by A28, A4, A8, NAT_1:14;
reconsider lm1 =
(len m) - 1 as
Element of
NAT by A28;
A72:
( 1
<= lm1 &
lm1 <= (len m) - 1 )
by A28, A4, A8, NAT_1:14;
consider d,
x,
y being
Element of
INT such that A73:
(
x = (nlist . lm1) `2 &
m . (lm1 + 1) = (m . lm1) * x &
y = m . (lm1 + 1) &
d = (nlist . (lm1 + 1)) `2 &
prodi . lm1 = ALGO_INVERSE (
y,
d) &
prodc . lm1 = y )
by A28, A4, A9;
consider u,
u0,
u1 being
Element of
INT such that A74:
(
u0 = (nlist . (lm1 + 1)) `1 &
u1 = (nlist . (lm1 + 1)) `2 &
u = ((u0 - (l . lm1)) * (prodi . lm1)) mod u1 &
l . (lm1 + 1) = (l . lm1) + (u * (prodc . lm1)) )
by A72, A28;
A75:
len nlist in Seg (len nlist)
by FINSEQ_1:3;
A76:
M0 = b . (len nlist)
by A28, A4, A75;
then A77:
M0 <> 0
by A75, A4;
then consider r being
Element of
INT such that A79:
u = ((u0 - (l . ((len m) - 1))) * (ALGO_INVERSE (y,M0))) + (r * M0)
by Lm14, A28, A73, A74;
A80:
y <> 0
by A73, A28, A4, Lm15, A30, A31;
now 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) )per cases
( len nlist1 = 1 or len nlist1 <> 1 )
;
suppose A81:
len nlist1 = 1
;
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) )A82:
ALGO_CRT nlist1 =
(nlist1 . 1) `1
by A81, Def4
.=
(nlist . 1) `1
by A42, FUNCT_1:49
.=
l . ((len m) - 1)
by A81, A4, A28, A14, FINSEQ_1:def 3
;
A83:
ALGO_CRT nlist = ((l . ((len m) - 1)) + (u * y)) mod M
by A73, A74, A28;
reconsider p =
0 as
Element of
INT by INT_1:def 2;
A84:
ALGO_CRT nlist1 = (l . ((len m) - 1)) + (p * y)
by A82;
reconsider uy =
u * y as
Element of
INT by INT_1:def 2;
reconsider llm1 =
l . ((len m) - 1) as
Element of
INT by INT_1:def 2;
reconsider ly =
llm1 + uy as
Element of
INT by INT_1:def 2;
consider t being
Element of
INT such that A85:
ALGO_CRT nlist = ly + (t * M)
by Lm14, A83, A77, A80, XCMPLX_1:6, A28, A73;
reconsider qr =
r + t as
Element of
INT by INT_1:def 2;
ALGO_CRT nlist = (((ALGO_CRT nlist1) - (((llm1 * (ALGO_INVERSE (y,M0))) * y) + (p * y))) + ((qr * M0) * y)) + ((u0 * (ALGO_INVERSE (y,M0))) * y)
by A28, A73, A79, A85, A82;
hence
ex
p,
qr 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 A84;
verum end; suppose A86:
len nlist1 <> 1
;
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 A87:
ALGO_CRT nlist1 =
s
by Def4, A50, A51, A62, A43
.=
((l | nn) . (len (m | nn))) mod ((prodc1 . ((len (m | nn)) - 1)) * M01)
;
A88:
(l | nn) . (len (l | nn)) =
l . (len (l | nn))
by A8, A36, FINSEQ_1:3, FUNCT_1:49
.=
l . ((len m) - 1)
by A28, A4, A35, FINSEQ_1:59
;
2
<= len nlist1
by A86, NAT_1:23;
then
2
- 1
<= (len (m | nn)) - 1
by A38, A17, XREAL_1:9;
then A89:
( 1
<= nn1 &
nn1 <= (len (m | nn)) - 1 )
by A37, FINSEQ_1:def 3;
A90:
M01 =
(nlist . (len (m | nn))) `2
by A13, A38, FINSEQ_1:3, FUNCT_1:49
.=
(nlist . ((len m) - 1)) `2
by A28, A4, A37, FINSEQ_1:def 3
;
consider d1,
x1,
y1 being
Element of
INT such that A91:
(
x1 = (nlist1 . nn1) `2 &
(m | nn) . (nn1 + 1) = ((m | nn) . nn1) * x1 &
y1 = (m | nn) . (nn1 + 1) &
d1 = (nlist1 . (nn1 + 1)) `2 &
prodi1 . nn1 = ALGO_INVERSE (
y1,
d1) &
prodc1 . nn1 = y1 )
by A51, A89;
A92:
len (m | nn) = (len m) - 1
by A28, A4, A37, FINSEQ_1:def 3;
then A93:
lm1 in Seg (len (m | nn))
by A71;
A94:
ALGO_CRT nlist1 = (l . ((len m) - 1)) mod (y1 * M01)
by A91, A87, A92, A88, A4, A28, A35, FINSEQ_1:59;
A96:
y = y1 * x
by A91, A28, A4, A38, A93, A73, FUNCT_1:49;
then A97:
y1 * M01 <> 0
by A28, A4, Lm15, A30, A31, A90, A73;
consider p being
Element of
INT such that A98:
ALGO_CRT nlist1 = (l . ((len m) - 1)) + (p * (y1 * M01))
by A94, Lm14, A80, A90, A73, A96;
ALGO_CRT nlist =
((l . ((len m) - 1)) + (u * (y1 * x))) mod ((prodc . ((len m) - 1)) * M0)
by A91, A28, A4, A38, A93, A73, A74, FUNCT_1:49
.=
((l . ((len m) - 1)) + (u * (y1 * x))) mod ((y1 * x) * M0)
by A91, A28, A4, A38, A93, A73, FUNCT_1:49
;
then consider q being
Element of
INT such that A100:
ALGO_CRT nlist = ((l . ((len m) - 1)) + (u * (y1 * x))) + (q * ((y1 * x) * M0))
by Lm14, A90, A73, A97, A77, XCMPLX_1:6;
reconsider qr =
r + q as
Element of
INT by INT_1:def 2;
((ALGO_CRT nlist1) - (p * (y1 * M01))) + (u * (y1 * x)) =
((ALGO_CRT nlist1) - (p * (y1 * x))) + (u * (y1 * x))
by A90, A73
.=
(((ALGO_CRT nlist1) - ((((l . ((len m) - 1)) * (ALGO_INVERSE (y,M0))) * y) + (p * y))) + ((r * M0) * y)) + ((u0 * (ALGO_INVERSE (y,M0))) * y)
by A96, A79
;
then ALGO_CRT nlist =
((((ALGO_CRT nlist1) - ((((l . ((len m) - 1)) * (ALGO_INVERSE (y,M0))) * y) + (p * y))) + ((r * M0) * y)) + ((u0 * (ALGO_INVERSE (y,M0))) * y)) + (q * (y * M0))
by A91, A28, A4, A38, A93, A73, A100, A98, FUNCT_1:49
.=
(((ALGO_CRT nlist1) - ((((l . ((len m) - 1)) * (ALGO_INVERSE (y,M0))) * y) + (p * y))) + ((qr * M0) * y)) + ((u0 * (ALGO_INVERSE (y,M0))) * y)
;
hence
ex
p,
qr 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 A98, A96, A90, A73;
verum end; end; end; then consider p,
qr being
Element of
INT such that A101:
(
ALGO_CRT nlist = (((ALGO_CRT nlist1) - ((((l . ((len m) - 1)) * (ALGO_INVERSE (y,M0))) * y) + (p * y))) + ((qr * M0) * y)) + ((u0 * (ALGO_INVERSE (y,M0))) * y) &
ALGO_CRT nlist1 = (l . ((len m) - 1)) + (p * y) )
;
reconsider y0 =
y mod M0 as
Element of
INT by INT_1:def 2;
y0 gcd M0 = 1
by INT_2:def 3, A77, Th10, A73, A28, A76, A34;
then A102:
(ALGO_EXGCD (M0,y0)) `3_3 = 1
by Th6;
A103:
((((l . ((len m) - 1)) * (ALGO_INVERSE (y,M0))) * y) + (p * y)) mod M0 =
((((l . ((len m) - 1)) * ((ALGO_INVERSE (y,M0)) * y)) mod M0) + ((p * y) mod M0)) mod M0
by NAT_D:66
.=
(((((l . ((len m) - 1)) mod M0) * (((ALGO_INVERSE (y,M0)) * y) mod M0)) mod M0) + ((p * y) mod M0)) mod M0
by NAT_D:67
.=
(((((l . ((len m) - 1)) mod M0) * (1 mod M0)) mod M0) + ((p * y) mod M0)) mod M0
by A102, Th7
.=
((((l . ((len m) - 1)) * 1) mod M0) + ((p * y) mod M0)) mod M0
by NAT_D:67
.=
(ALGO_CRT nlist1) mod M0
by A101, NAT_D:66
;
thus
for
i being
Nat st
i in Seg (len nlist) holds
(ALGO_CRT nlist) mod (b . i) = (a . i) mod (b . i)
verumproof
let i be
Nat;
( i in Seg (len nlist) implies (ALGO_CRT nlist) mod (b . i) = (a . i) mod (b . i) )
assume A104:
i in Seg (len nlist)
;
(ALGO_CRT nlist) mod (b . i) = (a . i) mod (b . i)
then A105:
( 1
<= i &
i <= len nlist )
by FINSEQ_1:1;
per cases
( i = len nlist or i <> len nlist )
;
suppose A106:
i = len nlist
;
(ALGO_CRT nlist) mod (b . i) = (a . i) mod (b . i)A107:
b . i <> 0
by A4, A104;
reconsider I0 =
0 as
Element of
INT by INT_1:def 2;
reconsider K1y =
(((l . ((len m) - 1)) * (ALGO_INVERSE (y,M0))) * y) + (p * y) as
Element of
INT by INT_1:def 2;
reconsider K2y =
(qr * y) * M0 as
Element of
INT by INT_1:def 2;
reconsider K3y =
u0 * ((ALGO_INVERSE (y,M0)) * y) as
Element of
INT by INT_1:def 2;
reconsider K4y =
K2y + K3y as
Element of
INT by INT_1:def 2;
A108:
K2y mod (b . i) =
(((qr * y) mod M0) * (M0 mod M0)) mod M0
by A76, A106, NAT_D:67
.=
(((qr * y) mod M0) * I0) mod M0
by INT_1:50
.=
I0 mod (b . i)
by A106, A28, A4, A75
;
A109:
K4y mod (b . i) =
((I0 mod (b . i)) + (K3y mod (b . i))) mod (b . i)
by A108, NAT_D:66
.=
(I0 + K3y) mod (b . i)
by NAT_D:66
.=
((u0 mod (b . i)) * (((ALGO_INVERSE (y,M0)) * y) mod (b . i))) mod (b . i)
by NAT_D:67
.=
((u0 mod (b . i)) * (1 mod (b . i))) mod (b . i)
by A102, Th7, A106, A76
.=
(u0 * 1) mod (b . i)
by NAT_D:67
.=
(a . i) mod (b . i)
by A106, A75, A28, A4, A74
;
A110:
((ALGO_CRT nlist) + K1y) mod (b . i) =
(((ALGO_CRT nlist) mod (b . i)) + ((ALGO_CRT nlist1) mod (b . i))) mod (b . i)
by A103, A106, A76, NAT_D:66
.=
((ALGO_CRT nlist) + (ALGO_CRT nlist1)) mod (b . i)
by NAT_D:66
;
A111:
((ALGO_CRT nlist1) + K4y) mod (b . i) =
(((ALGO_CRT nlist1) mod (b . i)) + (K4y mod (b . i))) mod (b . i)
by NAT_D:66
.=
((ALGO_CRT nlist1) + (a . i)) mod (b . i)
by A109, NAT_D:66
;
reconsider LL =
((ALGO_CRT nlist1) + (a . i)) mod (b . i) as
Element of
INT by INT_1:def 2;
reconsider LL1 =
(ALGO_CRT nlist) + (ALGO_CRT nlist1) as
Element of
INT by INT_1:def 2;
reconsider bi =
b . i as
Element of
INT by INT_1:def 2;
consider r being
Element of
INT such that A112:
LL = LL1 + (r * bi)
by Lm14, A107, A110, A111, A101;
reconsider LL2 =
(ALGO_CRT nlist1) + (a . i) as
Element of
INT by INT_1:def 2;
consider s being
Element of
INT such that A113:
LL = LL2 + (s * bi)
by Lm14, A107;
reconsider LL3 =
s - r as
Element of
INT by INT_1:def 2;
A114:
(LL3 * (b . i)) mod (b . i) =
((LL3 mod (b . i)) * ((b . i) mod (b . i))) mod (b . i)
by NAT_D:67
.=
((LL3 mod (b . i)) * I0) mod (b . i)
by INT_1:50
.=
I0 mod (b . i)
;
thus (ALGO_CRT nlist) mod (b . i) =
((a . i) + ((s - r) * (b . i))) mod (b . i)
by A112, A113
.=
(((a . i) mod (b . i)) + (I0 mod (b . i))) mod (b . i)
by A114, NAT_D:66
.=
((a . i) + I0) mod (b . i)
by NAT_D:66
.=
(a . i) mod (b . i)
;
verum end; suppose
i <> len nlist
;
(ALGO_CRT nlist) mod (b . i) = (a . i) mod (b . i)then
i < len nlist
by A105, XXREAL_0:1;
then
i + 1
<= len nlist
by NAT_1:13;
then A115:
(i + 1) - 1
<= (len nlist) - 1
by XREAL_1:9;
then A116:
( 1
<= i &
i <= len nlist1 )
by A35, A4, A104, FINSEQ_1:1, FINSEQ_1:59;
A117:
i in Seg (len nlist1)
by A115, A4, A17, A105;
reconsider K1 =
((l . ((len m) - 1)) * (ALGO_INVERSE (y,M0))) + p as
Element of
INT by INT_1:def 2;
reconsider K2 =
(qr * M0) + (u0 * (ALGO_INVERSE (y,M0))) as
Element of
INT by INT_1:def 2;
reconsider I0 =
0 as
Element of
INT by INT_1:def 2;
A118:
y mod (b . i) = 0
by A17, A73, Lm17, A30, A31, A4, A28, A116;
reconsider K1y =
K1 * y as
Element of
INT by INT_1:def 2;
reconsider K2y =
K2 * y as
Element of
INT by INT_1:def 2;
A119:
(K1 * y) mod (b . i) =
((K1 mod (b . i)) * (y mod (b . i))) mod (b . i)
by NAT_D:67
.=
0 mod (b . i)
by A118
;
A120:
(K2 * y) mod (b . i) =
((K2 mod (b . i)) * (y mod (b . i))) mod (b . i)
by NAT_D:67
.=
0 mod (b . i)
by A118
;
A121:
((ALGO_CRT nlist) + K1y) mod (b . i) =
(((ALGO_CRT nlist) mod (b . i)) + (K1y mod (b . i))) mod (b . i)
by NAT_D:66
.=
((ALGO_CRT nlist) + I0) mod (b . i)
by A119, NAT_D:66
.=
(ALGO_CRT nlist) mod (b . i)
;
((ALGO_CRT nlist1) + K2y) mod (b . i) =
(((ALGO_CRT nlist1) mod (b . i)) + (K2y mod (b . i))) mod (b . i)
by NAT_D:66
.=
((ALGO_CRT nlist1) + I0) mod (b . i)
by A120, NAT_D:66
.=
(ALGO_CRT nlist1) mod (b . i)
;
hence
(ALGO_CRT nlist) mod (b . i) = (a . i) mod (b . i)
by A117, A101, A121, A26;
verum end; end;
end; end; end;
end;
for n being Nat holds S1[n]
from NAT_1:sch 2(A1, A2);
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_coprime ) holds
for i being Nat st i in Seg (len nlist) holds
(ALGO_CRT nlist) mod (b . i) = (a . i) mod (b . i)
; verum