let x, y be Integer; :: thesis: for b, m being non empty FinSequence of INT st 2 <= len b & ( for i, j being Nat st i in Seg (len b) & j in Seg (len b) & i <> j holds

b . i,b . j are_coprime ) & ( for i being Nat st i in Seg (len b) holds

x mod (b . i) = y mod (b . i) ) & m . 1 = 1 holds

for k being Element of NAT st 1 <= k & k <= len b & ( for i being Nat st 1 <= i & i <= k holds

m . (i + 1) = (m . i) * (b . i) ) holds

x mod (m . (k + 1)) = y mod (m . (k + 1))

let b, m be non empty FinSequence of INT ; :: thesis: ( 2 <= len b & ( for i, j being Nat st i in Seg (len b) & j in Seg (len b) & i <> j holds

b . i,b . j are_coprime ) & ( for i being Nat st i in Seg (len b) holds

x mod (b . i) = y mod (b . i) ) & m . 1 = 1 implies for k being Element of NAT st 1 <= k & k <= len b & ( for i being Nat st 1 <= i & i <= k holds

m . (i + 1) = (m . i) * (b . i) ) holds

x mod (m . (k + 1)) = y mod (m . (k + 1)) )

assume A1: 2 <= len b ; :: thesis: ( ex i, j being Nat st

( i in Seg (len b) & j in Seg (len b) & i <> j & not b . i,b . j are_coprime ) or ex i being Nat st

( i in Seg (len b) & not x mod (b . i) = y mod (b . i) ) or not m . 1 = 1 or for k being Element of NAT st 1 <= k & k <= len b & ( for i being Nat st 1 <= i & i <= k holds

m . (i + 1) = (m . i) * (b . i) ) holds

x mod (m . (k + 1)) = y mod (m . (k + 1)) )

assume A2: for i, j being Nat st i in Seg (len b) & j in Seg (len b) & i <> j holds

b . i,b . j are_coprime ; :: thesis: ( ex i being Nat st

( i in Seg (len b) & not x mod (b . i) = y mod (b . i) ) or not m . 1 = 1 or for k being Element of NAT st 1 <= k & k <= len b & ( for i being Nat st 1 <= i & i <= k holds

m . (i + 1) = (m . i) * (b . i) ) holds

x mod (m . (k + 1)) = y mod (m . (k + 1)) )

assume A3: for i being Nat st i in Seg (len b) holds

x mod (b . i) = y mod (b . i) ; :: thesis: ( not m . 1 = 1 or for k being Element of NAT st 1 <= k & k <= len b & ( for i being Nat st 1 <= i & i <= k holds

m . (i + 1) = (m . i) * (b . i) ) holds

x mod (m . (k + 1)) = y mod (m . (k + 1)) )

assume A4: m . 1 = 1 ; :: thesis: for k being Element of NAT st 1 <= k & k <= len b & ( for i being Nat st 1 <= i & i <= k holds

m . (i + 1) = (m . i) * (b . i) ) holds

x mod (m . (k + 1)) = y mod (m . (k + 1))

defpred S_{1}[ Nat] means ( 1 <= $1 & $1 <= len b & ( for i being Nat st 1 <= i & i <= $1 holds

m . (i + 1) = (m . i) * (b . i) ) implies x mod (m . ($1 + 1)) = y mod (m . ($1 + 1)) );

reconsider I0 = 0 as Element of NAT ;

A5: S_{1}[ 0 ]
;

A6: for k being Nat st S_{1}[k] holds

S_{1}[k + 1]
_{1}[k]
from NAT_1:sch 2(A5, A6);

hence for k being Element of NAT st 1 <= k & k <= len b & ( for i being Nat st 1 <= i & i <= k holds

m . (i + 1) = (m . i) * (b . i) ) holds

x mod (m . (k + 1)) = y mod (m . (k + 1)) ; :: thesis: verum

b . i,b . j are_coprime ) & ( for i being Nat st i in Seg (len b) holds

x mod (b . i) = y mod (b . i) ) & m . 1 = 1 holds

for k being Element of NAT st 1 <= k & k <= len b & ( for i being Nat st 1 <= i & i <= k holds

m . (i + 1) = (m . i) * (b . i) ) holds

x mod (m . (k + 1)) = y mod (m . (k + 1))

let b, m be non empty FinSequence of INT ; :: thesis: ( 2 <= len b & ( for i, j being Nat st i in Seg (len b) & j in Seg (len b) & i <> j holds

b . i,b . j are_coprime ) & ( for i being Nat st i in Seg (len b) holds

x mod (b . i) = y mod (b . i) ) & m . 1 = 1 implies for k being Element of NAT st 1 <= k & k <= len b & ( for i being Nat st 1 <= i & i <= k holds

m . (i + 1) = (m . i) * (b . i) ) holds

x mod (m . (k + 1)) = y mod (m . (k + 1)) )

assume A1: 2 <= len b ; :: thesis: ( ex i, j being Nat st

( i in Seg (len b) & j in Seg (len b) & i <> j & not b . i,b . j are_coprime ) or ex i being Nat st

( i in Seg (len b) & not x mod (b . i) = y mod (b . i) ) or not m . 1 = 1 or for k being Element of NAT st 1 <= k & k <= len b & ( for i being Nat st 1 <= i & i <= k holds

m . (i + 1) = (m . i) * (b . i) ) holds

x mod (m . (k + 1)) = y mod (m . (k + 1)) )

assume A2: for i, j being Nat st i in Seg (len b) & j in Seg (len b) & i <> j holds

b . i,b . j are_coprime ; :: thesis: ( ex i being Nat st

( i in Seg (len b) & not x mod (b . i) = y mod (b . i) ) or not m . 1 = 1 or for k being Element of NAT st 1 <= k & k <= len b & ( for i being Nat st 1 <= i & i <= k holds

m . (i + 1) = (m . i) * (b . i) ) holds

x mod (m . (k + 1)) = y mod (m . (k + 1)) )

assume A3: for i being Nat st i in Seg (len b) holds

x mod (b . i) = y mod (b . i) ; :: thesis: ( not m . 1 = 1 or for k being Element of NAT st 1 <= k & k <= len b & ( for i being Nat st 1 <= i & i <= k holds

m . (i + 1) = (m . i) * (b . i) ) holds

x mod (m . (k + 1)) = y mod (m . (k + 1)) )

assume A4: m . 1 = 1 ; :: thesis: for k being Element of NAT st 1 <= k & k <= len b & ( for i being Nat st 1 <= i & i <= k holds

m . (i + 1) = (m . i) * (b . i) ) holds

x mod (m . (k + 1)) = y mod (m . (k + 1))

defpred S

m . (i + 1) = (m . i) * (b . i) ) implies x mod (m . ($1 + 1)) = y mod (m . ($1 + 1)) );

reconsider I0 = 0 as Element of NAT ;

A5: S

A6: for k being Nat st S

S

proof

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

assume A7: S_{1}[k]
; :: thesis: S_{1}[k + 1]

assume A8: ( 1 <= k + 1 & k + 1 <= len b & ( for i being Nat st 1 <= i & i <= k + 1 holds

m . (i + 1) = (m . i) * (b . i) ) ) ; :: thesis: x mod (m . ((k + 1) + 1)) = y mod (m . ((k + 1) + 1))

A9: k <= k + 1 by NAT_1:12;

end;assume A7: S

assume A8: ( 1 <= k + 1 & k + 1 <= len b & ( for i being Nat st 1 <= i & i <= k + 1 holds

m . (i + 1) = (m . i) * (b . i) ) ) ; :: thesis: x mod (m . ((k + 1) + 1)) = y mod (m . ((k + 1) + 1))

A9: k <= k + 1 by NAT_1:12;

per cases
( k = 0 or k <> 0 )
;

end;

suppose
k = 0
; :: thesis: x mod (m . ((k + 1) + 1)) = y mod (m . ((k + 1) + 1))

then A11: m . ((k + 1) + 1) =
(m . 1) * (b . 1)
by A8

.= b . 1 by A4 ;

( 1 <= 1 & 1 <= len b ) by NAT_1:14;

then 1 in Seg (len b) ;

hence x mod (m . ((k + 1) + 1)) = y mod (m . ((k + 1) + 1)) by A11, A3; :: thesis: verum

end;.= b . 1 by A4 ;

( 1 <= 1 & 1 <= len b ) by NAT_1:14;

then 1 in Seg (len b) ;

hence x mod (m . ((k + 1) + 1)) = y mod (m . ((k + 1) + 1)) by A11, A3; :: thesis: verum

suppose A13:
k <> 0
; :: thesis: x mod (m . ((k + 1) + 1)) = y mod (m . ((k + 1) + 1))

(k + 1) - 1 <= (len b) - 1
by A8, XREAL_1:9;

then A14: ( 1 <= k & k <= (len b) - 1 ) by A13, NAT_1:14;

k + 1 in Seg (len b) by A8;

then A17: x mod (b . (k + 1)) = y mod (b . (k + 1)) by A3;

m . (k + 1),b . (k + 1) are_coprime by Lm16, A15, A14, A1, A2, A4, A8;

hence x mod (m . ((k + 1) + 1)) = y mod (m . ((k + 1) + 1)) by A16, A17, A7, A13, A8, A9, A15, Lm18, NAT_1:14, XXREAL_0:2; :: thesis: verum

end;then A14: ( 1 <= k & k <= (len b) - 1 ) by A13, NAT_1:14;

A15: now :: thesis: for i being Nat st 1 <= i & i <= k holds

m . (i + 1) = (m . i) * (b . i)

A16:
m . ((k + 1) + 1) = (m . (k + 1)) * (b . (k + 1))
by A8;m . (i + 1) = (m . i) * (b . i)

let i be Nat; :: thesis: ( 1 <= i & i <= k implies m . (i + 1) = (m . i) * (b . i) )

assume ( 1 <= i & i <= k ) ; :: thesis: m . (i + 1) = (m . i) * (b . i)

then ( 1 <= i & i <= k + 1 ) by NAT_1:12;

hence m . (i + 1) = (m . i) * (b . i) by A8; :: thesis: verum

end;assume ( 1 <= i & i <= k ) ; :: thesis: m . (i + 1) = (m . i) * (b . i)

then ( 1 <= i & i <= k + 1 ) by NAT_1:12;

hence m . (i + 1) = (m . i) * (b . i) by A8; :: thesis: verum

k + 1 in Seg (len b) by A8;

then A17: x mod (b . (k + 1)) = y mod (b . (k + 1)) by A3;

m . (k + 1),b . (k + 1) are_coprime by Lm16, A15, A14, A1, A2, A4, A8;

hence x mod (m . ((k + 1) + 1)) = y mod (m . ((k + 1) + 1)) by A16, A17, A7, A13, A8, A9, A15, Lm18, NAT_1:14, XXREAL_0:2; :: thesis: verum

hence for k being Element of NAT st 1 <= k & k <= len b & ( for i being Nat st 1 <= i & i <= k holds

m . (i + 1) = (m . i) * (b . i) ) holds

x mod (m . (k + 1)) = y mod (m . (k + 1)) ; :: thesis: verum