defpred S1[ Nat] means for nlist being non empty FinSequence of
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; :: thesis: ( S1[n] implies S1[n + 1] )
assume A3: S1[n] ; :: thesis: S1[n + 1]
let nlist be non empty FinSequence of ; :: 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_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 ; :: 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_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 ) ) ; :: thesis: 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 A5: 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)

A6: 1 in Seg (len nlist) by A5, A4;
A7: ALGO_CRT nlist = (nlist . 1) `1 by Def4, A5, A4
.= a . 1 by A4, A6 ;
thus for i being Nat st i in Seg (len nlist) holds
(ALGO_CRT nlist) mod (b . i) = (a . i) mod (b . i) by ; :: thesis: verum
end;
suppose A8: 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 A9: 1 <= n by NAT_1:14;
A10: len nlist <> 1 by A4, A8;
reconsider nlist1 = nlist | n as FinSequence of ;
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 ;
A13: len nlist1 = n by ;
then reconsider nlist1 = nlist1 as non empty FinSequence of by A8;
A14: dom nlist1 = Seg (len nlist1) by FINSEQ_1:def 3
.= Seg n by ;
n in NAT by ORDINAL1:def 12;
then A15: len nlist1 = n by ;
then A16: Seg (len nlist1) c= Seg (len nlist) by ;
A17: ( len nlist1 = n & len a1 = len b1 & len a1 = len nlist1 ) by ;
A18: 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 A19: i in Seg (len nlist1) ; :: thesis: b1 . i <> 0
then b1 . i = b . i by ;
hence b1 . i <> 0 by A16, A19, A4; :: thesis: verum
end;
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; :: thesis: ( i in Seg (len nlist1) implies ( (nlist1 . i) `1 = a1 . i & (nlist1 . i) `2 = b1 . i ) )
assume A21: i in Seg (len nlist1) ; :: thesis: ( (nlist1 . i) `1 = a1 . i & (nlist1 . i) `2 = b1 . i )
A22: (nlist1 . i) `1 = (nlist . i) `1 by
.= a . i by A21, A16, A4
.= a1 . i by ;
(nlist1 . i) `2 = (nlist . i) `2 by
.= b . i by A21, A16, A4
.= b1 . i by ;
hence ( (nlist1 . i) `1 = a1 . i & (nlist1 . i) `2 = b1 . i ) by A22; :: thesis: 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; :: thesis: ( 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 ) ; :: thesis: b1 . i,b1 . j are_coprime
A25: b . i = b1 . i by ;
b . j = b1 . j by ;
hence b1 . i,b1 . j are_coprime by A25, A24, A16, A4; :: thesis: 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)
proof
let i be Nat; :: thesis: ( i in Seg (len nlist1) implies (ALGO_CRT nlist1) mod (b . i) = (a . i) mod (b . i) )
assume A27: 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 ;
hence (ALGO_CRT nlist1) mod (b . i) = (a . i) mod (b . i) by A3, A17, A20, A23, A18, A27; :: thesis: verum
end;
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 ;
A29: 1 + 1 <= n + 1 by ;
reconsider lb1 = (len b) - 1 as Nat by A4;
A30: ( 1 <= lb1 & lb1 <= lb1 ) by ;
A31: 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 A32: ( 1 <= i & i <= lb1 ) ; :: thesis: m . (i + 1) = (m . i) * (b . i)
then A33: 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 ;
i in Seg (len nlist1) by A32, A13, A4;
hence m . (i + 1) = (m . i) * (b . i) by A33, A4, A16; :: thesis: verum
end;
A34: m . (len nlist),b . (len nlist) are_coprime by A4, Lm16, A29, A28, A30, A31;
reconsider nn = n as Element of NAT by ORDINAL1:def 12;
set l1 = l | nn;
set m1 = m | nn;
A35: n <= n + 1 by NAT_1:11;
then A36: len (l | nn) = n by ;
A37: dom (m | nn) = Seg (len (m | nn)) by FINSEQ_1:def 3
.= Seg n by ;
A38: len (m | nn) = n by ;
1 - 1 <= n - 1 by ;
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 ;
A41: len prodc1 = nn1 by ;
A42: 1 in Seg n by A9;
A43: (l | nn) . 1 = l . 1 by
.= (nlist1 . 1) `1 by ;
A44: n - 1 <= n - 0 by XREAL_1:10;
A45: now :: thesis: 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; :: thesis: ( 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 ) ; :: thesis: ( (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 ;
then i in Seg (len (m | nn)) ;
hence (m | nn) . i = m . i by ; :: thesis: ( (l | nn) . i = l . i & prodi1 . i = prodi . i & prodc1 . i = prodc . i )
i in Seg (len (l | nn)) by ;
hence (l | nn) . i = l . i by ; :: thesis: ( prodi1 . i = prodi . i & prodc1 . i = prodc . i )
i in Seg (len prodi1) by ;
hence prodi1 . i = prodi . i by ; :: thesis: prodc1 . i = prodc . i
i in Seg (len prodc1) by ;
hence prodc1 . i = prodc . i by ; :: thesis: verum
end;
len (m | nn) in Seg (len nlist1) by ;
then A48: len (m | nn) in Seg (len nlist) by A16;
A49: nlist1 . (len (m | nn)) = nlist . (len (m | nn)) by ;
len (m | nn) in dom nlist by ;
then nlist1 . (len (m | nn)) in by ;
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 ;
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; :: thesis: ( 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 ) ; :: thesis: 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 ;
A55: prodc1 . i = prodc . i by ;
A56: 1 <= i + 1 by NAT_1:12;
i + 1 <= ((len (m | nn)) - 1) + 1 by ;
then A57: i + 1 in Seg (len (m | nn)) by A56;
then A58: (m | nn) . (i + 1) = m . (i + 1) by ;
A59: ( 1 <= i & i <= len (m | nn) ) by ;
A60: ( 1 <= i & i <= (len m) - 1 ) by ;
i in Seg (len nlist1) by ;
then A61: nlist1 . i = nlist . i by ;
nlist1 . (i + 1) = nlist . (i + 1) by ;
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; :: thesis: 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; :: thesis: ( 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 ) ; :: thesis: 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 ;
A66: prodc1 . i = prodc . i by ;
A67: 1 <= i + 1 by NAT_1:12;
i + 1 <= ((len (m | nn)) - 1) + 1 by ;
then A68: i + 1 in Seg (len (m | nn)) by A67;
then A69: (l | nn) . (i + 1) = l . (i + 1) by ;
A70: ( 1 <= i & i <= (len m) - 1 ) by ;
nlist1 . (i + 1) = nlist . (i + 1) by ;
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; :: thesis: 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 ;
reconsider lm1 = (len m) - 1 as Element of NAT by A28;
A72: ( 1 <= lm1 & lm1 <= (len m) - 1 ) by ;
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 ;
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 ;
then consider r being Element of INT such that
A79: u = ((u0 - (l . ((len m) - 1))) * (ALGO_INVERSE (y,M0))) + (r * M0) by ;
A80: y <> 0 by A73, A28, A4, Lm15, A30, A31;
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) )
per cases ( len nlist1 = 1 or len nlist1 <> 1 ) ;
suppose A81: 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) )

A82: ALGO_CRT nlist1 = (nlist1 . 1) `1 by
.= (nlist . 1) `1 by
.= l . ((len m) - 1) by ;
A83: ALGO_CRT nlist = ((l . ((len m) - 1)) + (u * y)) mod M by ;
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 ;
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; :: thesis: verum
end;
suppose A86: 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 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
.= l . ((len m) - 1) by ;
2 <= len nlist1 by ;
then 2 - 1 <= (len (m | nn)) - 1 by ;
then A89: ( 1 <= nn1 & nn1 <= (len (m | nn)) - 1 ) by ;
A90: M01 = (nlist . (len (m | nn))) `2 by
.= (nlist . ((len m) - 1)) `2 by ;
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 ;
A92: len (m | nn) = (len m) - 1 by ;
then A93: lm1 in Seg (len (m | nn)) by A71;
A94: ALGO_CRT nlist1 = (l . ((len m) - 1)) mod (y1 * M01) by ;
A96: y = y1 * x by ;
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;
A99: ALGO_CRT nlist = ((l . ((len m) - 1)) + (u * (y1 * x))) mod ((prodc . ((len m) - 1)) * M0) by
.= ((l . ((len m) - 1)) + (u * (y1 * x))) mod ((y1 * x) * M0) by ;
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 ;
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
.= (((ALGO_CRT nlist1) - ((((l . ((len m) - 1)) * (ALGO_INVERSE (y,M0))) * y) + (p * y))) + ((r * M0) * y)) + ((u0 * (ALGO_INVERSE (y,M0))) * y) by ;
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
.= (((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; :: thesis: 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 ;
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
.= ((((l . ((len m) - 1)) * 1) mod M0) + ((p * y) mod M0)) mod M0 by NAT_D:67
.= (ALGO_CRT nlist1) mod M0 by ;
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 A104: i in Seg (len nlist) ; :: thesis: (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 ; :: thesis: (ALGO_CRT nlist) mod (b . i) = (a . i) mod (b . i)
A107: b . i <> 0 by ;
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
.= (((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
.= (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
.= (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
.= ((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 ;
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 ;
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 ;
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
.= (((a . i) mod (b . i)) + (I0 mod (b . i))) mod (b . i) by
.= ((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 ;
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 ;
A117: i in Seg (len nlist1) by ;
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
.= (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
.= (ALGO_CRT nlist1) mod (b . i) ;
hence (ALGO_CRT nlist) mod (b . i) = (a . i) mod (b . i) by ; :: thesis: 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
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) ; :: thesis: verum