let x, y be Integer; 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 ; ( 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
; ( 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
; ( 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)
; ( 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
; 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 S1[ 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:
S1[ 0 ]
;
A6:
for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be
Nat;
( S1[k] implies S1[k + 1] )
assume A7:
S1[
k]
;
S1[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) ) )
;
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 )
;
suppose A13:
k <> 0
;
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;
A15:
now for i being Nat st 1 <= i & i <= k holds
m . (i + 1) = (m . i) * (b . i)let i be
Nat;
( 1 <= i & i <= k implies m . (i + 1) = (m . i) * (b . i) )assume
( 1
<= i &
i <= k )
;
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;
verum end; A16:
m . ((k + 1) + 1) = (m . (k + 1)) * (b . (k + 1))
by A8;
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;
verum end; end;
end;
for k being Nat holds S1[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))
; verum