defpred S_{1}[ 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: S_{1}[ 0 ]
;

A2: for n being Nat st S_{1}[n] holds

S_{1}[n + 1]
_{1}[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) ; :: thesis: verum

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

A2: for n being Nat st S

S

proof

for n being Nat holds S
let n be Nat; :: thesis: ( S_{1}[n] implies S_{1}[n + 1] )

assume A3: S_{1}[n]
; :: thesis: S_{1}[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_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)

end;assume A3: S

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

end;

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)

(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 A7, A5, A4, FINSEQ_1:2, TARSKI:def 1; :: thesis: verum

end;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 A7, A5, A4, FINSEQ_1:2, TARSKI:def 1; :: thesis: verum

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)

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

then 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

( (nlist1 . i) `1 = a1 . i & (nlist1 . i) `2 = b1 . i )

b1 . i,b1 . j are_coprime

(ALGO_CRT nlist1) mod (b . i) = (a . i) mod (b . i)

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)

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;

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 )

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

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;

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

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

then 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

proof

A20:
for i being Nat st i in Seg (len nlist1) holds
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 A15, FUNCT_1:49;

hence b1 . i <> 0 by A16, A19, A4; :: thesis: verum

end;assume A19: i in Seg (len nlist1) ; :: thesis: b1 . i <> 0

then b1 . i = b . i by A15, FUNCT_1:49;

hence b1 . i <> 0 by A16, A19, A4; :: thesis: verum

( (nlist1 . i) `1 = a1 . i & (nlist1 . i) `2 = b1 . i )

proof

A23:
for i, j being Nat st i in Seg (len nlist1) & j in Seg (len nlist1) & i <> j holds
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 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; :: thesis: verum

end;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 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; :: thesis: verum

b1 . i,b1 . j are_coprime

proof

A26:
for i being Nat st i in Seg (len nlist1) holds
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 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; :: thesis: verum

end;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 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; :: thesis: verum

(ALGO_CRT nlist1) mod (b . i) = (a . i) mod (b . i)

proof

consider m, l, prodc, prodi being FinSequence of INT , M0, M being Element of INT such that
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 A15, FUNCT_1:49;

hence (ALGO_CRT nlist1) mod (b . i) = (a . i) mod (b . i) by A3, A17, A20, A23, A18, A27; :: thesis: verum

end;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 A15, FUNCT_1:49;

hence (ALGO_CRT nlist1) mod (b . i) = (a . i) mod (b . i) by A3, A17, A20, A23, A18, A27; :: thesis: verum

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)

proof

A34:
m . (len nlist),b . (len nlist) are_coprime
by A4, Lm16, A29, A28, A30, A31;
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 A4, A28;

i in Seg (len nlist1) by A32, A13, A4;

hence m . (i + 1) = (m . i) * (b . i) by A33, A4, A16; :: thesis: verum

end;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 A4, A28;

i in Seg (len nlist1) by A32, A13, A4;

hence m . (i + 1) = (m . i) * (b . i) by A33, A4, A16; :: thesis: verum

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

len (m | nn) in Seg (len nlist1)
by A13, A38, FINSEQ_1:3;( (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 A38, A44, XXREAL_0:2;

then i in Seg (len (m | nn)) ;

hence (m | nn) . i = m . i by A38, FUNCT_1:49; :: thesis: ( (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; :: thesis: ( 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; :: thesis: prodc1 . i = prodc . i

i in Seg (len prodc1) by A46, A38, A41;

hence prodc1 . i = prodc . i by A41, FUNCT_1:49; :: thesis: verum

end;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 A38, A44, XXREAL_0:2;

then i in Seg (len (m | nn)) ;

hence (m | nn) . i = m . i by A38, FUNCT_1:49; :: thesis: ( (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; :: thesis: ( 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; :: thesis: prodc1 . i = prodc . i

i in Seg (len prodc1) by A46, A38, A41;

hence prodc1 . i = prodc . i by A41, FUNCT_1:49; :: thesis: verum

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

A62:
for i being Nat st 1 <= i & i <= (len (m | nn)) - 1 holds
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 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; :: thesis: verum

end;( 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 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; :: thesis: verum

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

reconsider s = ((l | nn) . (len (m | nn))) mod M1 as Element of INT by INT_1:def 2;
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 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; :: thesis: verum

end;( 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 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; :: thesis: verum

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

then consider p, qr being Element of INT such that ( 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 )
;

end;

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

( 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; :: thesis: verum

end;.= (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; :: thesis: verum

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

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

A99: 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; :: thesis: verum

end;.= ((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;

A99: 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; :: thesis: verum

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

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

end;

suppose A106:
i = len nlist
; :: thesis: (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) ; :: thesis: verum

end;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) ; :: thesis: verum

suppose
i <> len nlist
; :: thesis: (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; :: thesis: verum

end;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; :: thesis: verum

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) ; :: thesis: verum