let nlist be non empty FinSequence of [:INT,INT:]; :: thesis: for a, b being non empty FinSequence of INT
for x, y being Element of INT st len a = len b & len a = len nlist & ( for i being Nat st i in Seg (len nlist) holds
b . i <> 0 ) & ( for i being Nat st i in Seg (len nlist) holds
( (nlist . i) `1 = a . i & (nlist . i) `2 = b . i ) ) & ( for i, j being Nat st i in Seg (len nlist) & j in Seg (len nlist) & i <> j holds
b . i,b . j are_coprime ) & ( for i being Nat st i in Seg (len nlist) holds
x mod (b . i) = (a . i) mod (b . i) ) & y = Product b holds
(ALGO_CRT nlist) mod y = x mod y
let a, b be non empty FinSequence of INT ; :: thesis: for x, y being Element of INT st len a = len b & len a = len nlist & ( for i being Nat st i in Seg (len nlist) holds
b . i <> 0 ) & ( for i being Nat st i in Seg (len nlist) holds
( (nlist . i) `1 = a . i & (nlist . i) `2 = b . i ) ) & ( for i, j being Nat st i in Seg (len nlist) & j in Seg (len nlist) & i <> j holds
b . i,b . j are_coprime ) & ( for i being Nat st i in Seg (len nlist) holds
x mod (b . i) = (a . i) mod (b . i) ) & y = Product b holds
(ALGO_CRT nlist) mod y = x mod y
let x, y be Element of INT ; :: thesis: ( len a = len b & len a = len nlist & ( for i being Nat st i in Seg (len nlist) holds
b . i <> 0 ) & ( for i being Nat st i in Seg (len nlist) holds
( (nlist . i) `1 = a . i & (nlist . i) `2 = b . i ) ) & ( for i, j being Nat st i in Seg (len nlist) & j in Seg (len nlist) & i <> j holds
b . i,b . j are_coprime ) & ( for i being Nat st i in Seg (len nlist) holds
x mod (b . i) = (a . i) mod (b . i) ) & y = Product b implies (ALGO_CRT nlist) mod y = x mod y )
assume A1: ( len a = len b & len a = len nlist ) ; :: thesis: ( ex i being Nat st
( i in Seg (len nlist) & not b . i <> 0 ) or ex i being Nat st
( i in Seg (len nlist) & not ( (nlist . i) `1 = a . i & (nlist . i) `2 = b . i ) ) or ex i, j being Nat st
( i in Seg (len nlist) & j in Seg (len nlist) & i <> j & not b . i,b . j are_coprime ) or ex i being Nat st
( i in Seg (len nlist) & not x mod (b . i) = (a . i) mod (b . i) ) or not y = Product b or (ALGO_CRT nlist) mod y = x mod y )
assume A2: for i being Nat st i in Seg (len nlist) holds
b . i <> 0 ; :: thesis: ( ex i being Nat st
( i in Seg (len nlist) & not ( (nlist . i) `1 = a . i & (nlist . i) `2 = b . i ) ) or ex i, j being Nat st
( i in Seg (len nlist) & j in Seg (len nlist) & i <> j & not b . i,b . j are_coprime ) or ex i being Nat st
( i in Seg (len nlist) & not x mod (b . i) = (a . i) mod (b . i) ) or not y = Product b or (ALGO_CRT nlist) mod y = x mod y )
assume A3: for i being Nat st i in Seg (len nlist) holds
( (nlist . i) `1 = a . i & (nlist . i) `2 = b . i ) ; :: thesis: ( ex i, j being Nat st
( i in Seg (len nlist) & j in Seg (len nlist) & i <> j & not b . i,b . j are_coprime ) or ex i being Nat st
( i in Seg (len nlist) & not x mod (b . i) = (a . i) mod (b . i) ) or not y = Product b or (ALGO_CRT nlist) mod y = x mod y )
assume A4: for i, j being Nat st i in Seg (len nlist) & j in Seg (len nlist) & i <> j holds
b . i,b . j are_coprime ; :: thesis: ( ex i being Nat st
( i in Seg (len nlist) & not x mod (b . i) = (a . i) mod (b . i) ) or not y = Product b or (ALGO_CRT nlist) mod y = x mod y )
assume A5: for i being Nat st i in Seg (len nlist) holds
x mod (b . i) = (a . i) mod (b . i) ; :: thesis: ( not y = Product b or (ALGO_CRT nlist) mod y = x mod y )
assume A6: y = Product b ; :: thesis: (ALGO_CRT nlist) mod y = x mod y
A7: for i being Nat st i in Seg (len nlist) holds
(ALGO_CRT nlist) mod (b . i) = x mod (b . i)

proof

let i be Nat; :: thesis: ( i in Seg (len nlist) implies (ALGO_CRT nlist) mod (b . i) = x mod (b . i) )
assume A8: i in Seg (len nlist) ; :: thesis: (ALGO_CRT nlist) mod (b . i) = x mod (b . i)
hence (ALGO_CRT nlist) mod (b . i) = (a . i) mod (b . i) by Th11, A1, A2, A3, A4
.= x mod (b . i) by A5, A8 ;
:: thesis: verum

end;

per cases ( len nlist = 1 or len nlist <> 1 ) ;

suppose A9: len nlist = 1 ; :: thesis: (ALGO_CRT nlist) mod y = x mod y

then A10: 1 in Seg (len nlist) ;
thus (ALGO_CRT nlist) mod y = (ALGO_CRT nlist) mod (b . 1) by A9, A1, Th13, A6
.= x mod (b . 1) by A7, A10
.= x mod y by A9, A1, Th13, A6 ; :: thesis: verum

end;

suppose A11: len nlist <> 1 ; :: thesis: (ALGO_CRT nlist) mod y = x mod y

then A12: 2 <= len nlist by NAT_1:23;
A13: 2 <= len b by A1, A11, NAT_1:23;
consider m being non empty FinSequence of INT such that
A14: ( len m = (len b) + 1 & m . 1 = 1 & ( for i being Nat st 1 <= i & i <= len b holds
m . (i + 1) = (m . i) * (b . i) ) & Product b = m . ((len b) + 1) ) by Th14;
( 1 <= len b & len b <= len b ) by A13, XXREAL_0:2;
hence (ALGO_CRT nlist) mod y = x mod y by A6, A14, Th12, A1, A4, A7, A12; :: thesis: verum

end;

end;