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)

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

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

end;

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

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