let fp be FinSequence of NAT ; ( len fp >= 2 & ( for b, c being Element of NAT st b in dom fp & c in dom fp & b <> c holds
(fp . b) gcd (fp . c) = 1 ) & ( for b being Element of NAT st b in dom fp holds
fp . b <> 0 ) implies for fp1 being FinSequence of NAT ex x being Integer st
for b being Element of NAT st b in dom fp holds
(x - (fp1 . b)) mod (fp . b) = 0 )
assume that
A1:
len fp >= 2
and
A2:
for b, c being Element of NAT st b in dom fp & c in dom fp & b <> c holds
(fp . b) gcd (fp . c) = 1
and
A3:
for b being Element of NAT st b in dom fp holds
fp . b <> 0
; for fp1 being FinSequence of NAT ex x being Integer st
for b being Element of NAT st b in dom fp holds
(x - (fp1 . b)) mod (fp . b) = 0
consider fp2 being FinSequence of NAT , q being Element of NAT such that
A4:
fp = fp2 ^ <*q*>
by A1, FINSEQ_2:19;
deffunc H1( Nat) -> set = { l where l is Element of NAT : (((Product (Del (fp,$1))) * l) - 1) mod (fp . $1) = 0 } ;
defpred S1[ Nat, Nat] means $2 in H1($1);
A5:
for a being Nat st a in Seg (len fp) holds
ex n being Element of NAT st S1[a,n]
proof
let a be
Nat;
( a in Seg (len fp) implies ex n being Element of NAT st S1[a,n] )
reconsider l =
fp . a as
Integer ;
assume
a in Seg (len fp)
;
ex n being Element of NAT st S1[a,n]
then A6:
a in dom fp
by FINSEQ_1:def 3;
then
(Product (Del (fp,a))) gcd (fp . a) = 1
by A1, A2, Th31;
then A7:
Product (Del (fp,a)),
l are_coprime
by INT_2:def 3;
l <> 0
by A3, A6;
then consider n being
Nat such that A8:
(((Product (Del (fp,a))) * n) - 1) mod l = 0
by A7, Th16;
reconsider n =
n as
Element of
NAT by ORDINAL1:def 12;
take
n
;
S1[a,n]
thus
S1[
a,
n]
by A8;
verum
end;
consider s being FinSequence of NAT such that
A9:
( dom s = Seg (len fp) & ( for a being Nat st a in Seg (len fp) holds
S1[a,s . a] ) )
from FINSEQ_1:sch 5(A5);
let fp1 be FinSequence of NAT ; ex x being Integer st
for b being Element of NAT st b in dom fp holds
(x - (fp1 . b)) mod (fp . b) = 0
set k = len fp2;
deffunc H2( Nat) -> set = ((Product (Del (fp,$1))) * (s . $1)) * (fp1 . $1);
consider s1 being FinSequence such that
A10:
( len s1 = (len fp2) + 1 & ( for a being Nat st a in dom s1 holds
s1 . a = H2(a) ) )
from FINSEQ_1:sch 2();
for a being Nat st a in dom s1 holds
s1 . a in NAT
then reconsider s1 = s1 as FinSequence of NAT by FINSEQ_2:12;
set x = Sum s1;
take
Sum s1
; for b being Element of NAT st b in dom fp holds
((Sum s1) - (fp1 . b)) mod (fp . b) = 0
A12:
len fp = (len fp2) + 1
by A4, FINSEQ_2:16;
A13:
for a being Nat
for b being Element of NAT st a in dom fp & b in dom fp & a <> b holds
fp . b divides s1 . a
proof
let a be
Nat;
for b being Element of NAT st a in dom fp & b in dom fp & a <> b holds
fp . b divides s1 . alet b be
Element of
NAT ;
( a in dom fp & b in dom fp & a <> b implies fp . b divides s1 . a )
assume that A14:
a in dom fp
and A15:
(
b in dom fp &
a <> b )
;
fp . b divides s1 . a
len fp >= 1
by A1, XXREAL_0:2;
then
fp . b divides (Product (Del (fp,a))) * ((s . a) * (fp1 . a))
by A14, A15, Th35, NAT_D:9;
then A16:
fp . b divides ((Product (Del (fp,a))) * (s . a)) * (fp1 . a)
;
a in dom s1
by A12, A10, A14, FINSEQ_3:29;
hence
fp . b divides s1 . a
by A10, A16;
verum
end;
A17:
for b being Element of NAT st b in dom fp holds
fp . b divides Sum (Del (s1,b))
proof
let b be
Element of
NAT ;
( b in dom fp implies fp . b divides Sum (Del (s1,b)) )
assume A18:
b in dom fp
;
fp . b divides Sum (Del (s1,b))
then
b in Seg (len s1)
by A12, A10, FINSEQ_1:def 3;
then A19:
b in dom s1
by FINSEQ_1:def 3;
then A20:
(len (Del (s1,b))) + 1
= (len fp2) + 1
by A10, WSIERP_1:def 1;
for
a being
Nat st
a in dom (Del (s1,b)) holds
fp . b divides (Del (s1,b)) . a
proof
let a be
Nat;
( a in dom (Del (s1,b)) implies fp . b divides (Del (s1,b)) . a )
assume A21:
a in dom (Del (s1,b))
;
fp . b divides (Del (s1,b)) . a
then A22:
(
a >= 1 &
a <= len fp2 )
by A20, FINSEQ_3:25;
dom (Del (s1,b)) c= dom s1
by WSIERP_1:39;
then
a in dom s1
by A21;
then
a in Seg ((len fp2) + 1)
by A10, FINSEQ_1:def 3;
then A23:
a in dom fp
by A12, FINSEQ_1:def 3;
per cases
( a < b or a >= b )
;
suppose A25:
a >= b
;
fp . b divides (Del (s1,b)) . a
(
a + 1
<= (len fp2) + 1 &
a + 1
> 1 )
by A22, XREAL_1:6, XREAL_1:29;
then A26:
a + 1
in dom fp
by A12, FINSEQ_3:25;
(
(Del (s1,b)) . a = s1 . (a + 1) &
a + 1
> b )
by A19, A25, WSIERP_1:def 1, XREAL_1:39;
hence
fp . b divides (Del (s1,b)) . a
by A13, A18, A26;
verum
end;
hence
fp . b divides Sum (Del (s1,b))
by Th36;
verum
end;
for b being Element of NAT st b in dom fp holds
((Sum s1) - (fp1 . b)) mod (fp . b) = 0
proof
let b be
Element of
NAT ;
( b in dom fp implies ((Sum s1) - (fp1 . b)) mod (fp . b) = 0 )
assume A27:
b in dom fp
;
((Sum s1) - (fp1 . b)) mod (fp . b) = 0
then A28:
fp . b <> 0
by A3;
A29:
fp . b divides Sum (Del (s1,b))
by A17, A27;
A30:
((Sum (Del (s1,b))) + ((s1 . b) - (fp1 . b))) mod (fp . b) = ((s1 . b) - (fp1 . b)) mod (fp . b)
A32:
(
b >= 1 &
b <= (len fp2) + 1 )
by A12, A27, FINSEQ_3:25;
then A33:
b in Seg ((len fp2) + 1)
;
then
b in dom s1
by A10, FINSEQ_1:def 3;
then A34:
(s1 . b) - (fp1 . b) =
(((Product (Del (fp,b))) * (s . b)) * (fp1 . b)) - (1 * (fp1 . b))
by A10
.=
(((Product (Del (fp,b))) * (s . b)) - 1) * (fp1 . b)
;
s . b in H1(
b)
by A12, A9, A33;
then A35:
ex
ll being
Element of
NAT st
(
ll = s . b &
(((Product (Del (fp,b))) * ll) - 1) mod (fp . b) = 0 )
;
A36:
s1 is
FinSequence of
REAL
by FINSEQ_2:24, NUMBERS:19;
b in dom s1
by A10, A32, FINSEQ_3:25;
then ((Sum s1) - (fp1 . b)) mod (fp . b) =
(((Sum (Del (s1,b))) + (s1 . b)) - (fp1 . b)) mod (fp . b)
by WSIERP_1:20, A36
.=
0
by A28, A34, A35, A30, Lm9
;
hence
((Sum s1) - (fp1 . b)) mod (fp . b) = 0
;
verum
end;
hence
for b being Element of NAT st b in dom fp holds
((Sum s1) - (fp1 . b)) mod (fp . b) = 0
; verum