let fp be FinSequence of NAT ; :: thesis: ( 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 ; :: thesis: 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 H_{1}( Nat) -> set = { l where l is Element of NAT : (((Product (Del (fp,$1))) * l) - 1) mod (fp . $1) = 0 } ;

defpred S_{1}[ Nat, Nat] means $2 in H_{1}($1);

A5: for a being Nat st a in Seg (len fp) holds

ex n being Element of NAT st S_{1}[a,n]

A9: ( dom s = Seg (len fp) & ( for a being Nat st a in Seg (len fp) holds

S_{1}[a,s . a] ) )
from FINSEQ_1:sch 5(A5);

let fp1 be FinSequence of NAT ; :: thesis: 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 H_{2}( 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 = H_{2}(a) ) )
from FINSEQ_1:sch 2();

for a being Nat st a in dom s1 holds

s1 . a in NAT

set x = Sum s1;

take Sum s1 ; :: thesis: 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

fp . b divides Sum (Del (s1,b))

((Sum s1) - (fp1 . b)) mod (fp . b) = 0

((Sum s1) - (fp1 . b)) mod (fp . b) = 0 ; :: thesis: verum

(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 ; :: thesis: 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 H

defpred S

A5: for a being Nat st a in Seg (len fp) holds

ex n being Element of NAT st S

proof

consider s being FinSequence of NAT such that
let a be Nat; :: thesis: ( a in Seg (len fp) implies ex n being Element of NAT st S_{1}[a,n] )

reconsider l = fp . a as Integer ;

assume a in Seg (len fp) ; :: thesis: ex n being Element of NAT st S_{1}[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 ; :: thesis: S_{1}[a,n]

thus S_{1}[a,n]
by A8; :: thesis: verum

end;reconsider l = fp . a as Integer ;

assume a in Seg (len fp) ; :: thesis: ex n being Element of NAT st S

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 ; :: thesis: S

thus S

A9: ( dom s = Seg (len fp) & ( for a being Nat st a in Seg (len fp) holds

S

let fp1 be FinSequence of NAT ; :: thesis: 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 H

consider s1 being FinSequence such that

A10: ( len s1 = (len fp2) + 1 & ( for a being Nat st a in dom s1 holds

s1 . a = H

for a being Nat st a in dom s1 holds

s1 . a in NAT

proof

then reconsider s1 = s1 as FinSequence of NAT by FINSEQ_2:12;
let a be Nat; :: thesis: ( a in dom s1 implies s1 . a in NAT )

assume A11: a in dom s1 ; :: thesis: s1 . a in NAT

reconsider a = a as Element of NAT by ORDINAL1:def 12;

s1 . a = ((Product (Del (fp,a))) * (s . a)) * (fp1 . a) by A10, A11;

hence s1 . a in NAT by ORDINAL1:def 12; :: thesis: verum

end;assume A11: a in dom s1 ; :: thesis: s1 . a in NAT

reconsider a = a as Element of NAT by ORDINAL1:def 12;

s1 . a = ((Product (Del (fp,a))) * (s . a)) * (fp1 . a) by A10, A11;

hence s1 . a in NAT by ORDINAL1:def 12; :: thesis: verum

set x = Sum s1;

take Sum s1 ; :: thesis: 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

A17:
for b being Element of NAT st b in dom fp holds
let a be Nat; :: thesis: for b being Element of NAT st a in dom fp & b in dom fp & a <> b holds

fp . b divides s1 . a

let b be Element of NAT ; :: thesis: ( 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 ) ; :: thesis: 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; :: thesis: verum

end;fp . b divides s1 . a

let b be Element of NAT ; :: thesis: ( 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 ) ; :: thesis: 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; :: thesis: verum

fp . b divides Sum (Del (s1,b))

proof

for b being Element of NAT st b in dom fp holds
let b be Element of NAT ; :: thesis: ( b in dom fp implies fp . b divides Sum (Del (s1,b)) )

assume A18: b in dom fp ; :: thesis: 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

end;assume A18: b in dom fp ; :: thesis: 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

hence
fp . b divides Sum (Del (s1,b))
by Th36; :: thesis: verum
let a be Nat; :: thesis: ( a in dom (Del (s1,b)) implies fp . b divides (Del (s1,b)) . a )

assume A21: a in dom (Del (s1,b)) ; :: thesis: 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;

end;assume A21: a in dom (Del (s1,b)) ; :: thesis: 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 )
;

end;

suppose A24:
a < b
; :: thesis: fp . b divides (Del (s1,b)) . a

then
(Del (s1,b)) . a = s1 . a
by A19, WSIERP_1:def 1;

hence fp . b divides (Del (s1,b)) . a by A13, A18, A23, A24; :: thesis: verum

end;hence fp . b divides (Del (s1,b)) . a by A13, A18, A23, A24; :: thesis: verum

suppose A25:
a >= b
; :: thesis: 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; :: thesis: verum

end;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; :: thesis: verum

((Sum s1) - (fp1 . b)) mod (fp . b) = 0

proof

hence
for b being Element of NAT st b in dom fp holds
let b be Element of NAT ; :: thesis: ( b in dom fp implies ((Sum s1) - (fp1 . b)) mod (fp . b) = 0 )

assume A27: b in dom fp ; :: thesis: ((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)

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 H_{1}(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 ; :: thesis: verum

end;assume A27: b in dom fp ; :: thesis: ((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)

proof

A32:
( b >= 1 & b <= (len fp2) + 1 )
by A12, A27, FINSEQ_3:25;
reconsider l = Sum (Del (s1,b)) as Integer ;

A31: l mod (fp . b) = 0 by A29, A28, INT_1:62;

((Sum (Del (s1,b))) + ((s1 . b) - (fp1 . b))) mod (fp . b) = ((l mod (fp . b)) + (((s1 . b) - (fp1 . b)) mod (fp . b))) mod (fp . b) by NAT_D:66

.= ((s1 . b) - (fp1 . b)) mod (fp . b) by A31, NAT_D:65 ;

hence ((Sum (Del (s1,b))) + ((s1 . b) - (fp1 . b))) mod (fp . b) = ((s1 . b) - (fp1 . b)) mod (fp . b) ; :: thesis: verum

end;A31: l mod (fp . b) = 0 by A29, A28, INT_1:62;

((Sum (Del (s1,b))) + ((s1 . b) - (fp1 . b))) mod (fp . b) = ((l mod (fp . b)) + (((s1 . b) - (fp1 . b)) mod (fp . b))) mod (fp . b) by NAT_D:66

.= ((s1 . b) - (fp1 . b)) mod (fp . b) by A31, NAT_D:65 ;

hence ((Sum (Del (s1,b))) + ((s1 . b) - (fp1 . b))) mod (fp . b) = ((s1 . b) - (fp1 . b)) mod (fp . b) ; :: thesis: verum

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 H

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 ; :: thesis: verum

((Sum s1) - (fp1 . b)) mod (fp . b) = 0 ; :: thesis: verum