let n be Nat; :: thesis: for p being Prime
for fp being FinSequence of INT st len fp = n + 1 & p > 2 & not p divides fp . (n + 1) holds
for fr being FinSequence of INT st ( for d being Nat st d in dom fr holds
((Poly-INT fp) . (fr . d)) mod p = 0 ) & ( for d, e being Nat st d in dom fr & e in dom fr & d <> e holds
not fr . d,fr . e are_congruent_mod p ) holds
len fr <= n
let p be Prime; :: thesis: for fp being FinSequence of INT st len fp = n + 1 & p > 2 & not p divides fp . (n + 1) holds
for fr being FinSequence of INT st ( for d being Nat st d in dom fr holds
((Poly-INT fp) . (fr . d)) mod p = 0 ) & ( for d, e being Nat st d in dom fr & e in dom fr & d <> e holds
not fr . d,fr . e are_congruent_mod p ) holds
len fr <= n
defpred S₁[ Nat] means for fp being FinSequence of INT st len fp = $1 + 1 & p > 2 & not p divides fp . ($1 + 1) holds
for fr being FinSequence of INT st ( for d being Nat st d in dom fr holds
((Poly-INT fp) . (fr . d)) mod p = 0 ) & ( for d, e being Nat st d in dom fr & e in dom fr & d <> e holds
not fr . d,fr . e are_congruent_mod p ) holds
len fr <= $1;
A1: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A2: S₁[n] ; :: thesis: S₁[n + 1]
let fp be FinSequence of INT ; :: thesis: ( len fp = (n + 1) + 1 & p > 2 & not p divides fp . ((n + 1) + 1) implies for fr being FinSequence of INT st ( for d being Nat st d in dom fr holds
((Poly-INT fp) . (fr . d)) mod p = 0 ) & ( for d, e being Nat st d in dom fr & e in dom fr & d <> e holds
not fr . d,fr . e are_congruent_mod p ) holds
len fr <= n + 1 )
assume that
A3: len fp = (n + 1) + 1 and
A4: p > 2 and
A5: not p divides fp . ((n + 1) + 1) ; :: thesis: for fr being FinSequence of INT st ( for d being Nat st d in dom fr holds
((Poly-INT fp) . (fr . d)) mod p = 0 ) & ( for d, e being Nat st d in dom fr & e in dom fr & d <> e holds
not fr . d,fr . e are_congruent_mod p ) holds
len fr <= n + 1

per cases ( for x being Integer holds ((Poly-INT fp) . x) mod p <> 0 or ex a being Integer st ((Poly-INT fp) . a) mod p = 0 ) ;

suppose A6: for x being Integer holds ((Poly-INT fp) . x) mod p <> 0 ; :: thesis: for fr being FinSequence of INT st ( for d being Nat st d in dom fr holds
((Poly-INT fp) . (fr . d)) mod p = 0 ) & ( for d, e being Nat st d in dom fr & e in dom fr & d <> e holds
not fr . d,fr . e are_congruent_mod p ) holds
len fr <= n + 1

assume ex fr being FinSequence of INT st
( ( for d being Nat st d in dom fr holds
((Poly-INT fp) . (fr . d)) mod p = 0 ) & ( for d, e being Nat st d in dom fr & e in dom fr & d <> e holds
not fr . d,fr . e are_congruent_mod p ) & len fr > n + 1 ) ; :: thesis: contradiction
then consider fr being FinSequence of INT such that
A7: for d being Nat st d in dom fr holds
((Poly-INT fp) . (fr . d)) mod p = 0 and
for d, e being Nat st d in dom fr & e in dom fr & d <> e holds
not fr . d,fr . e are_congruent_mod p and
A8: len fr > n + 1 ;
fr <> {} by A8;
then ((Poly-INT fp) . (fr . 1)) mod p = 0 by A7, FINSEQ_5:6;
hence contradiction by A6; :: thesis: verum

end;

suppose ex a being Integer st ((Poly-INT fp) . a) mod p = 0 ; :: thesis: for fr being FinSequence of INT st ( for d being Nat st d in dom fr holds
((Poly-INT fp) . (fr . d)) mod p = 0 ) & ( for d, e being Nat st d in dom fr & e in dom fr & d <> e holds
not fr . d,fr . e are_congruent_mod p ) holds
len fr <= n + 1

then consider a being Integer such that
A9: ((Poly-INT fp) . a) mod p = 0 ;
assume ex f being FinSequence of INT st
( ( for d being Nat st d in dom f holds
((Poly-INT fp) . (f . d)) mod p = 0 ) & ( for d, e being Nat st d in dom f & e in dom f & d <> e holds
not f . d,f . e are_congruent_mod p ) & len f > n + 1 ) ; :: thesis: contradiction
then consider f being FinSequence of INT such that
A10: for d being Nat st d in dom f holds
((Poly-INT fp) . (f . d)) mod p = 0 and
A11: for d, e being Nat st d in dom f & e in dom f & d <> e holds
not f . d,f . e are_congruent_mod p and
A12: len f > n + 1 ;
consider fk being FinSequence of INT , r being Integer such that
A13: len fk = n + 1 and
A14: for x being Element of INT holds (Poly-INT fp) . x = ((x - a) * ((Poly-INT fk) . x)) + r and
A15: fp . (n + 2) = fk . (n + 1) by A3, Th6;
a is Element of INT by INT_1:def 2;
then A16: ((Poly-INT fp) . a) mod p = (((a - a) * ((Poly-INT fk) . a)) + r) mod p by A14
.= r mod p ;
A17: for d being Element of NAT st d in dom f holds
p divides ((f . d) - a) * ((Poly-INT fk) . (f . d))

proof

let d be Element of NAT ; :: thesis: ( d in dom f implies p divides ((f . d) - a) * ((Poly-INT fk) . (f . d)) )
f . d is Element of INT by INT_1:def 2;
then A18: ((Poly-INT fp) . (f . d)) mod p = ((((f . d) - a) * ((Poly-INT fk) . (f . d))) + r) mod p by A14
.= (((((f . d) - a) * ((Poly-INT fk) . (f . d))) mod p) + (r mod p)) mod p by NAT_D:66
.= (((f . d) - a) * ((Poly-INT fk) . (f . d))) mod p by A9, A16, NAT_D:65 ;
assume d in dom f ; :: thesis: p divides ((f . d) - a) * ((Poly-INT fk) . (f . d))
then (((f . d) - a) * ((Poly-INT fk) . (f . d))) mod p = 0 by A10, A18;
hence p divides ((f . d) - a) * ((Poly-INT fk) . (f . d)) by INT_1:62; :: thesis: verum

end;

per cases ( for d being Nat st d in dom f holds
not p divides (f . d) - a or ex d being Nat st
( d in dom f & p divides (f . d) - a ) ) ;

suppose A19: for d being Nat st d in dom f holds
not p divides (f . d) - a ; :: thesis: contradiction

for d being Nat st d in dom f holds
((Poly-INT fk) . (f . d)) mod p = 0

proof

let d be Nat; :: thesis: ( d in dom f implies ((Poly-INT fk) . (f . d)) mod p = 0 )
assume A20: d in dom f ; :: thesis: ((Poly-INT fk) . (f . d)) mod p = 0
then p divides ((f . d) - a) * ((Poly-INT fk) . (f . d)) by A17;
then ( p divides (f . d) - a or p divides (Poly-INT fk) . (f . d) ) by Th7;
hence ((Poly-INT fk) . (f . d)) mod p = 0 by A19, A20, INT_1:62; :: thesis: verum

end;

then len f <= n by A2, A4, A5, A13, A15, A11;
hence contradiction by A12, XREAL_1:145; :: thesis: verum

end;

suppose ex d being Nat st
( d in dom f & p divides (f . d) - a ) ; :: thesis: contradiction

then consider d9 being Element of NAT such that
A21: d9 in dom f and
A22: p divides (f . d9) - a ;
set f9 = f - {(f . d9)};
A23: for d being Nat st d in dom (f - {(f . d9)}) holds
not p divides ((f - {(f . d9)}) . d) - a

proof

given k being Nat such that A24: k in dom (f - {(f . d9)}) and
A25: p divides ((f - {(f . d9)}) . k) - a ; :: thesis: contradiction
(f - {(f . d9)}) . k in rng (f - {(f . d9)}) by A24, FUNCT_1:3;
then A26: (f - {(f . d9)}) . k in (rng f) \ {(f . d9)} by FINSEQ_3:65;
then (f - {(f . d9)}) . k in rng f by XBOOLE_0:def 5;
then consider w being object such that
A27: w in dom f and
A28: f . w = (f - {(f . d9)}) . k by FUNCT_1:def 3;
reconsider w = w as Element of NAT by A27;
p divides ((f . w) - a) - ((f . d9) - a) by A22, A25, A28, Th1;
then A29: f . w,f . d9 are_congruent_mod p ;
not (f - {(f . d9)}) . k in {(f . d9)} by A26, XBOOLE_0:def 5;
then w <> d9 by A28, TARSKI:def 1;
hence contradiction by A11, A21, A27, A29; :: thesis: verum

end;

A30: for d being Nat st d in dom (f - {(f . d9)}) holds
((Poly-INT fk) . ((f - {(f . d9)}) . d)) mod p = 0

proof

let d be Nat; :: thesis: ( d in dom (f - {(f . d9)}) implies ((Poly-INT fk) . ((f - {(f . d9)}) . d)) mod p = 0 )
assume A31: d in dom (f - {(f . d9)}) ; :: thesis: ((Poly-INT fk) . ((f - {(f . d9)}) . d)) mod p = 0
then (f - {(f . d9)}) . d in rng (f - {(f . d9)}) by FUNCT_1:3;
then (f - {(f . d9)}) . d in (rng f) \ {(f . d9)} by FINSEQ_3:65;
then (f - {(f . d9)}) . d in rng f by XBOOLE_0:def 5;
then ex w being object st
( w in dom f & f . w = (f - {(f . d9)}) . d ) by FUNCT_1:def 3;
then p divides (((f - {(f . d9)}) . d) - a) * ((Poly-INT fk) . ((f - {(f . d9)}) . d)) by A17;
then ( p divides ((f - {(f . d9)}) . d) - a or p divides (Poly-INT fk) . ((f - {(f . d9)}) . d) ) by Th7;
hence ((Poly-INT fk) . ((f - {(f . d9)}) . d)) mod p = 0 by A23, A31, INT_1:62; :: thesis: verum

end;

A32: f is one-to-one by A11, INT_1:11;
then A33: f - {(f . d9)} is one-to-one by FINSEQ_3:87;
A34: for d, e being Nat st d in dom (f - {(f . d9)}) & e in dom (f - {(f . d9)}) & d <> e holds
not (f - {(f . d9)}) . d,(f - {(f . d9)}) . e are_congruent_mod p

proof

let d, e be Nat; :: thesis: ( d in dom (f - {(f . d9)}) & e in dom (f - {(f . d9)}) & d <> e implies not (f - {(f . d9)}) . d,(f - {(f . d9)}) . e are_congruent_mod p )
assume that
A35: d in dom (f - {(f . d9)}) and
A36: e in dom (f - {(f . d9)}) and
A37: d <> e ; :: thesis: not (f - {(f . d9)}) . d,(f - {(f . d9)}) . e are_congruent_mod p
(f - {(f . d9)}) . e in rng (f - {(f . d9)}) by A36, FUNCT_1:3;
then (f - {(f . d9)}) . e in (rng f) \ {(f . d9)} by FINSEQ_3:65;
then (f - {(f . d9)}) . e in rng f by XBOOLE_0:def 5;
then consider w2 being object such that
A38: w2 in dom f and
A39: (f - {(f . d9)}) . e = f . w2 by FUNCT_1:def 3;
(f - {(f . d9)}) . d in rng (f - {(f . d9)}) by A35, FUNCT_1:3;
then (f - {(f . d9)}) . d in (rng f) \ {(f . d9)} by FINSEQ_3:65;
then (f - {(f . d9)}) . d in rng f by XBOOLE_0:def 5;
then consider w1 being object such that
A40: w1 in dom f and
A41: (f - {(f . d9)}) . d = f . w1 by FUNCT_1:def 3;
reconsider w1 = w1, w2 = w2 as Element of NAT by A40, A38;
w1 <> w2 by A33, A35, A36, A37, A41, A39;
hence not (f - {(f . d9)}) . d,(f - {(f . d9)}) . e are_congruent_mod p by A11, A40, A41, A38, A39; :: thesis: verum

end;

f . d9 in rng f by A21, FUNCT_1:3;
then len (f - {(f . d9)}) = (len f) - 1 by A32, FINSEQ_3:90;
then len (f - {(f . d9)}) > (n + 1) - 1 by A12, XREAL_1:9;
hence contradiction by A2, A4, A5, A13, A15, A30, A34; :: thesis: verum

end;

end;

end;

end;

end;

A42: S₁[ 0 ]

proof

let fp be FinSequence of INT ; :: thesis: ( len fp = 0 + 1 & p > 2 & not p divides fp . (0 + 1) implies for fr being FinSequence of INT st ( for d being Nat st d in dom fr holds
((Poly-INT fp) . (fr . d)) mod p = 0 ) & ( for d, e being Nat st d in dom fr & e in dom fr & d <> e holds
not fr . d,fr . e are_congruent_mod p ) holds
len fr <= 0 )
assume that
A43: len fp = 0 + 1 and
p > 2 and
A44: not p divides fp . (0 + 1) ; :: thesis: for fr being FinSequence of INT st ( for d being Nat st d in dom fr holds
((Poly-INT fp) . (fr . d)) mod p = 0 ) & ( for d, e being Nat st d in dom fr & e in dom fr & d <> e holds
not fr . d,fr . e are_congruent_mod p ) holds
len fr <= 0
assume ex fr being FinSequence of INT st
( ( for d being Nat st d in dom fr holds
((Poly-INT fp) . (fr . d)) mod p = 0 ) & ( for d, e being Nat st d in dom fr & e in dom fr & d <> e holds
not fr . d,fr . e are_congruent_mod p ) & len fr > 0 ) ; :: thesis: contradiction
then consider fr being FinSequence of INT such that
A45: for d being Nat st d in dom fr holds
((Poly-INT fp) . (fr . d)) mod p = 0 and
for d, e being Nat st d in dom fr & e in dom fr & d <> e holds
not fr . d,fr . e are_congruent_mod p and
A46: len fr > 0 ;
fr <> {} by A46;
then A47: ((Poly-INT fp) . (fr . 1)) mod p = 0 by A45, FINSEQ_5:6;
A48: fr . 1 in INT by INT_1:def 2;
(Poly-INT fp) . (fr . 1) = (INT --> (fp . 1)) . (fr . 1) by A43, Th3
.= fp . 1 by A48, FUNCOP_1:7 ;
hence contradiction by A44, A47, Lm1; :: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A42, A1);
hence for fp being FinSequence of INT st len fp = n + 1 & p > 2 & not p divides fp . (n + 1) holds
for fr being FinSequence of INT st ( for d being Nat st d in dom fr holds
((Poly-INT fp) . (fr . d)) mod p = 0 ) & ( for d, e being Nat st d in dom fr & e in dom fr & d <> e holds
not fr . d,fr . e are_congruent_mod p ) holds
len fr <= n ; :: thesis: verum