let n, k be Nat; :: thesis:
let p be INT -valued Polynomial of ((2 + n) + k),F_Real; :: thesis:
let X be n -element XFinSequence of NAT ; :: thesis:
let x be Element of NAT ; :: thesis:
set x1 = x + 1;
thus ( ( for z being Element of NAT st z <= x holds
ex y being k -element XFinSequence of NAT st
( ( for i being Nat st i in k holds
y . i <= x ) & eval (p,(@ ((<%z,x%> ^ X) ^ y))) = 0 ) ) implies ex Y being k -element XFinSequence of NAT ex Z, K being Element of NAT st
( K > x & K >= (sum_of_coefficients |.p.|) * ((((x ^2) + 1) * (Product (1 + X))) |^ (degree p)) & ( for i being Nat st i in k holds
Y . i > x + 1 ) & 1 + ((Z + 1) * (K !)) = Product (1 + ((K !) * (idseq (x + 1)))) & eval (p,(@ ((<%Z,x%> ^ X) ^ Y))), 0 are_congruent_mod 1 + ((Z + 1) * (K !)) & ( for i being Nat st i in k holds
Product (((Y . i) + 1) + (- (idseq (x + 1)))), 0 are_congruent_mod 1 + ((Z + 1) * (K !)) ) ) ) :: thesis:

assume A1: for z being Element of NAT st z <= x holds
ex y being k -element XFinSequence of NAT st
( ( for i being Nat st i in k holds
y . i <= x ) & eval (p,(@ ((<%z,x%> ^ X) ^ y))) = 0 ) ; :: thesis:
defpred S₁[ object , object ] means ( $1 in NAT & $2 is k -element XFinSequence of NAT & ( for z being Element of NAT
for y being k -element XFinSequence of NAT st z = $1 & y = $2 holds
( ( for i being Nat st i in k holds
y . i <= x ) & eval (p,(@ ((<%z,x%> ^ X) ^ y))) = 0 ) ) );
A2: for i being Nat st i in x + 1 holds
ex g being object st S₁[i,g]

let i be Nat; :: thesis:
assume i in x + 1 ; :: thesis:
then A3: i in Segm (x + 1) ;
reconsider z = i as Element of NAT by ORDINAL1:def 12;
i < x + 1 by A3, NAT_1:44;
then i <= x by NAT_1:13;
then consider y being k -element XFinSequence of NAT such that
A4: for i being Nat st i in k holds
y . i <= x and
A5: eval (p,(@ ((<%z,x%> ^ X) ^ y))) = 0 by A1;
take y ; :: thesis:
thus S₁[i,y] by A4, A5, ORDINAL1:def 12; :: thesis:

end;

consider YY being XFinSequence such that
A6: ( dom YY = x + 1 & ( for i being Nat st i in x + 1 holds
S₁[i,YY . i] ) ) from AFINSQ_1:sch 1(A2);
YY is XFinSequence-yielding by A6;
then reconsider YY = YY as XFinSequence-yielding XFinSequence ;
defpred S₂[ object , object ] means verum;
set M = { ((YY . i) . j) where i, j is Nat : S₂[i,j] } ;
A7: { ((YY . i) . j) where i, j is Nat : S₂[i,j] } is finite from HILB10_5:sch 1();
A8: { ((YY . i) . j) where i, j is Nat : S₂[i,j] } is natural-membered

proof

let x be object ; :: according to MEMBERED:def 6 :: thesis:
assume x in { ((YY . i) . j) where i, j is Nat : S₂[i,j] } ; :: thesis:
then consider i, j being Nat such that
A9: ( x = (YY . i) . j & S₂[i,j] ) ;

per cases ;

suppose i in dom YY ; :: thesis:

then S₁[i,YY . i] by A6;
hence x is natural by A9; :: thesis:

end;

suppose not i in dom YY ; :: thesis:

then YY . i = {} by FUNCT_1:def 2;
hence x is natural by A9; :: thesis:

end;

then reconsider Mx = { ((YY . i) . j) where i, j is Nat : S₂[i,j] } \/ {x,1} as non empty finite natural-membered set by A7;
set K = (x + 1) + ((sum_of_coefficients |.p.|) * ((((x ^2) + 1) * (Product (1 + X))) |^ (degree p)));
set h = 1 + ((((x + 1) + ((sum_of_coefficients |.p.|) * ((((x ^2) + 1) * (Product (1 + X))) |^ (degree p)))) !) * (idseq (x + 1)));
A10: len (1 + ((((x + 1) + ((sum_of_coefficients |.p.|) * ((((x ^2) + 1) * (Product (1 + X))) |^ (degree p)))) !) * (idseq (x + 1)))) = x + 1 by CARD_1:def 7;
A11: for i being Nat st i in dom (1 + ((((x + 1) + ((sum_of_coefficients |.p.|) * ((((x ^2) + 1) * (Product (1 + X))) |^ (degree p)))) !) * (idseq (x + 1)))) holds
(1 + ((((x + 1) + ((sum_of_coefficients |.p.|) * ((((x ^2) + 1) * (Product (1 + X))) |^ (degree p)))) !) * (idseq (x + 1)))) . i = ((((x + 1) + ((sum_of_coefficients |.p.|) * ((((x ^2) + 1) * (Product (1 + X))) |^ (degree p)))) !) * i) + 1

proof

let i be Nat; :: thesis:
assume A12: i in dom (1 + ((((x + 1) + ((sum_of_coefficients |.p.|) * ((((x ^2) + 1) * (Product (1 + X))) |^ (degree p)))) !) * (idseq (x + 1)))) ; :: thesis:
A13: ( dom (1 + ((((x + 1) + ((sum_of_coefficients |.p.|) * ((((x ^2) + 1) * (Product (1 + X))) |^ (degree p)))) !) * (idseq (x + 1)))) = dom ((((x + 1) + ((sum_of_coefficients |.p.|) * ((((x ^2) + 1) * (Product (1 + X))) |^ (degree p)))) !) * (idseq (x + 1))) & dom ((((x + 1) + ((sum_of_coefficients |.p.|) * ((((x ^2) + 1) * (Product (1 + X))) |^ (degree p)))) !) * (idseq (x + 1))) = dom (idseq (x + 1)) ) by VALUED_1:def 2, VALUED_1:def 5;
thus (1 + ((((x + 1) + ((sum_of_coefficients |.p.|) * ((((x ^2) + 1) * (Product (1 + X))) |^ (degree p)))) !) * (idseq (x + 1)))) . i = 1 + (((((x + 1) + ((sum_of_coefficients |.p.|) * ((((x ^2) + 1) * (Product (1 + X))) |^ (degree p)))) !) * (idseq (x + 1))) . i) by A12, VALUED_1:def 2
.= 1 + ((((x + 1) + ((sum_of_coefficients |.p.|) * ((((x ^2) + 1) * (Product (1 + X))) |^ (degree p)))) !) * ((idseq (x + 1)) . i)) by A12, A13, VALUED_1:def 5
.= ((((x + 1) + ((sum_of_coefficients |.p.|) * ((((x ^2) + 1) * (Product (1 + X))) |^ (degree p)))) !) * i) + 1 by A12, A13, FINSEQ_2:49 ; :: thesis:

end;

A14: ( (x + 1) + ((sum_of_coefficients |.p.|) * ((((x ^2) + 1) * (Product (1 + X))) |^ (degree p))) >= x + 1 & x + 1 > 0 ) by NAT_1:11;
reconsider h = 1 + ((((x + 1) + ((sum_of_coefficients |.p.|) * ((((x ^2) + 1) * (Product (1 + X))) |^ (degree p)))) !) * (idseq (x + 1))) as CR_Sequence by NAT_1:11, Th2;
rng h c= NAT by VALUED_0:def 6;
then A15: h is FinSequence of NAT by FINSEQ_1:def 4;
0 + 1 <= x + 1 by NAT_1:13;
then ( h . 1 divides Product h & h . 1 = ((((x + 1) + ((sum_of_coefficients |.p.|) * ((((x ^2) + 1) * (Product (1 + X))) |^ (degree p)))) !) * 1) + 1 ) by A11, A15, INT_4:32, A10, FINSEQ_3:25;
then ( h . 1 <= Product h & h . 1 > ((x + 1) + ((sum_of_coefficients |.p.|) * ((((x ^2) + 1) * (Product (1 + X))) |^ (degree p)))) ! ) by INT_2:27, NAT_1:13;
then ( (x + 1) + ((sum_of_coefficients |.p.|) * ((((x ^2) + 1) * (Product (1 + X))) |^ (degree p))) <= ((x + 1) + ((sum_of_coefficients |.p.|) * ((((x ^2) + 1) * (Product (1 + X))) |^ (degree p)))) ! & ((x + 1) + ((sum_of_coefficients |.p.|) * ((((x ^2) + 1) * (Product (1 + X))) |^ (degree p)))) ! < Product h ) by XXREAL_0:2, NEWTON:38;
then ( x + 1 <= (x + 1) + ((sum_of_coefficients |.p.|) * ((((x ^2) + 1) * (Product (1 + X))) |^ (degree p))) & (x + 1) + ((sum_of_coefficients |.p.|) * ((((x ^2) + 1) * (Product (1 + X))) |^ (degree p))) < Product h ) by NAT_1:11, XXREAL_0:2;
then A16: x + 1 < Product h by XXREAL_0:2;
defpred S₃[ object , object ] means ( $1 in NAT & $2 in NAT & ( for i, z being Nat st i = $1 & z = $2 holds
( x + 1 < z & ( for j, F being Nat st j in x + 1 & F = (YY . j) . i holds
z,F are_congruent_mod h . (j + 1) ) ) ) );
A17: for i being Nat st i in k holds
ex Y being object st S₃[i,Y]

proof

let i be Nat; :: thesis:
assume i in k ; :: thesis:
deffunc H₁( Nat) -> set = (YY . ($1 -' 1)) . i;
consider X being FinSequence such that
A18: ( len X = x + 1 & ( for k being Nat st k in dom X holds
X . k = H₁(k) ) ) from FINSEQ_1:sch 2();
rng X c= NAT

proof

let y be object ; :: according to TARSKI:def 3 :: thesis:
assume y in rng X ; :: thesis:
then consider x being object such that
A19: ( x in dom X & X . x = y ) by FUNCT_1:def 3;
reconsider x = x as Nat by A19;
X . x = (YY . (x -' 1)) . i by A18, A19;
then X . x in { ((YY . i) . j) where i, j is Nat : S₂[i,j] } ;
then X . x is natural by A8;
hence y in NAT by A19; :: thesis:

end;

then reconsider X = X as FinSequence of NAT by FINSEQ_1:def 4;
consider z being Integer such that
A20: ( 0 <= z & z < Product h ) and
A21: for i being Nat st i in dom X holds
z,X . i are_congruent_mod h . i by INT_6:41, A18, A10;
take Y = z + (Product h); :: thesis:
thus ( i in NAT & Y in NAT ) by A20, ORDINAL1:def 12; :: thesis:
let I, Z be Nat; :: thesis:
assume A22: ( I = i & Z = Y ) ; :: thesis:
Y >= Product h by A20, NAT_1:11;
hence x + 1 < Z by A22, A16, XXREAL_0:2; :: thesis:
let j, F be Nat; :: thesis:
assume A23: ( j in x + 1 & F = (YY . j) . I ) ; :: thesis:
x + 1 = Segm (x + 1) ;
then j < x + 1 by A23, NAT_1:44;
then A24: ( 1 <= j + 1 & j + 1 <= x + 1 ) by NAT_1:11, NAT_1:13;
then A25: z,X . (j + 1) are_congruent_mod h . (j + 1) by A21, A18, FINSEQ_3:25;
j + 1 in dom h by A24, A10, FINSEQ_3:25;
then h . (j + 1) divides (Product h) - 0 by A15, INT_4:32;
then Product h, 0 are_congruent_mod h . (j + 1) by INT_1:def 4;
then A26: Y,(X . (j + 1)) + 0 are_congruent_mod h . (j + 1) by A25, INT_1:16;
X . (j + 1) = (YY . ((j + 1) -' 1)) . i by A18, A24, FINSEQ_3:25;
hence Z,F are_congruent_mod h . (j + 1) by A26, A23, A22, NAT_D:34; :: thesis:

end;

consider YC being XFinSequence such that
A27: ( dom YC = k & ( for i being Nat st i in k holds
S₃[i,YC . i] ) ) from AFINSQ_1:sch 1(A17);
rng YC c= NAT

proof

let y be object ; :: according to TARSKI:def 3 :: thesis:
assume y in rng YC ; :: thesis:
then ex x being object st
( x in dom YC & YC . x = y ) by FUNCT_1:def 3;
hence y in NAT by A27; :: thesis:

end;

then reconsider YC = YC as k -element XFinSequence of NAT by A27, CARD_1:def 7, RELAT_1:def 19;
consider Z being Nat such that
A29: ( Product (1 + ((((x + 1) + ((sum_of_coefficients |.p.|) * ((((x ^2) + 1) * (Product (1 + X))) |^ (degree p)))) !) * (idseq (x + 1)))) = 1 + ((((x + 1) + ((sum_of_coefficients |.p.|) * ((((x ^2) + 1) * (Product (1 + X))) |^ (degree p)))) !) * Z) & ( x + 1 > 0 implies Z > 0 ) ) by Lm1;
reconsider Z1 = Z - 1 as Element of NAT by NAT_1:20, A29;
reconsider K = (x + 1) + ((sum_of_coefficients |.p.|) * ((((x ^2) + 1) * (Product (1 + X))) |^ (degree p))) as Element of NAT by ORDINAL1:def 12;
take YC ; :: thesis:
take Z1 ; :: thesis:
take K ; :: thesis:
thus ( K > x & K >= (sum_of_coefficients |.p.|) * ((((x ^2) + 1) * (Product (1 + X))) |^ (degree p)) ) by NAT_1:11, NAT_1:13, A14; :: thesis:
thus for i being Nat st i in k holds
YC . i > x + 1 by A27; :: thesis:
thus 1 + ((Z1 + 1) * (K !)) = Product (1 + ((K !) * (idseq (x + 1)))) by A29; :: thesis:
A30: for b, c being Element of NAT st b in dom h & c in dom h & b <> c holds
(h . b) gcd (h . c) = 1 by INT_2:def 3, INT_6:def 2;
reconsider E = eval (p,(@ ((<%Z1,x%> ^ X) ^ YC))) as Integer ;
A31: for b being Element of NAT st b in dom h holds
h . b divides E

proof

let b be Element of NAT ; :: thesis:
assume A32: b in dom h ; :: thesis:
A33: h . b = ((K !) * b) + 1 by A32, A11;
( 1 <= b & b <= x + 1 ) by A10, A32, FINSEQ_3:25;
then reconsider b1 = b - 1 as Element of NAT by NAT_1:21;
b1 + 1 <= x + 1 by A10, A32, FINSEQ_3:25;
then b1 < Segm (x + 1) by NAT_1:13;
then A34: b1 in x + 1 by NAT_1:44;
then reconsider YYb = YY . b1 as k -element XFinSequence of NAT by A6;
A35: eval (p,(@ ((<%b1,x%> ^ X) ^ YYb))) = 0 by A34, A6;
for i being Nat st i in (2 + n) + k holds
h . b divides (((<%Z1,x%> ^ X) ^ YC) . i) - (((<%b1,x%> ^ X) ^ YYb) . i)

proof

let i be Nat; :: thesis:
A36: len ((<%Z1,x%> ^ X) ^ YC) = (2 + n) + k by CARD_1:def 7;
A37: ( len <%Z1,x%> = 1 + 1 & len <%b1,x%> = 1 + 1 ) by CARD_1:def 7;
A38: ( len (<%Z1,x%> ^ X) = (len <%Z1,x%>) + (len X) & len (<%b1,x%> ^ X) = (len <%b1,x%>) + (len X) ) by AFINSQ_1:17;
A39: ( len YC = k & k = len YYb ) by CARD_1:def 7;
assume i in (2 + n) + k ; :: thesis:

per cases by A36, AFINSQ_1:20;

suppose A40: i in dom (<%Z1,x%> ^ X) ; :: thesis:

then A41: ( ((<%Z1,x%> ^ X) ^ YC) . i = (<%Z1,x%> ^ X) . i & ((<%b1,x%> ^ X) ^ YYb) . i = (<%b1,x%> ^ X) . i ) by A38, A37, AFINSQ_1:def 3;

per cases by A40, AFINSQ_1:20;

suppose A42: i in dom <%Z1,x%> ; :: thesis:

then A43: i in Segm 2 by CARD_1:def 7;
A44: ( (<%Z1,x%> ^ X) . i = <%Z1,x%> . i & (<%b1,x%> ^ X) . i = <%b1,x%> . i ) by A42, A37, AFINSQ_1:def 3;

per cases by A43, NAT_1:23, NAT_1:44;

suppose i = 0 ; :: thesis:

then A45: ( ((<%Z1,x%> ^ X) ^ YC) . i = Z1 & ((<%b1,x%> ^ X) ^ YYb) . i = b1 ) by A40, A38, A37, AFINSQ_1:def 3, A44;
A46: ((K !) + 1) gcd (K !) = ((b1 * (K !)) + ((K !) + 1)) gcd (K !) by EULER_1:8;
A47: ((K !) + 1) gcd (K !) = 1 by INT_2:def 3, PEPIN:1;
A48: h . b divides Product h by A15, A32, INT_4:32;
A49: (Z1 - b1) * (K !) = (Product (1 + ((K !) * (idseq (x + 1))))) - (h . b) by A29, A33;
h . b divides (Z1 - b1) * (K !) by A48, A49, INT_5:1;
hence h . b divides (((<%Z1,x%> ^ X) ^ YC) . i) - (((<%b1,x%> ^ X) ^ YYb) . i) by A45, A47, INT_2:25, A46, INT_2:def 3, A33; :: thesis:

end;

suppose i = 1 ; :: thesis:

hence h . b divides (((<%Z1,x%> ^ X) ^ YC) . i) - (((<%b1,x%> ^ X) ^ YYb) . i) by INT_2:12, A41, A44; :: thesis:

end;

suppose ex j being Nat st
( j in dom X & i = (len <%Z1,x%>) + j ) ; :: thesis:

then consider j being Nat such that
A50: ( j in dom X & i = 2 + j ) by A37;
( (<%Z1,x%> ^ X) . i = X . j & (<%b1,x%> ^ X) . i = X . j ) by A37, A50, AFINSQ_1:def 3;
hence h . b divides (((<%Z1,x%> ^ X) ^ YC) . i) - (((<%b1,x%> ^ X) ^ YYb) . i) by A41, INT_2:12; :: thesis:

end;

suppose ex j being Nat st
( j in dom YC & i = (len (<%Z1,x%> ^ X)) + j ) ; :: thesis:

then consider j being Nat such that
A51: ( j in dom YC & i = (len (<%Z1,x%> ^ X)) + j ) ;
A52: ((<%Z1,x%> ^ X) ^ YC) . i = YC . j by A51, AFINSQ_1:def 3;
A53: ((<%b1,x%> ^ X) ^ YYb) . i = YYb . j by A39, A37, A38, A51, AFINSQ_1:def 3;
reconsider J = j, YCj = YC . j as Element of NAT by A51;
YC . j,YYb . j are_congruent_mod h . (b1 + 1) by A34, A27, A51;
hence h . b divides (((<%Z1,x%> ^ X) ^ YC) . i) - (((<%b1,x%> ^ X) ^ YYb) . i) by A52, A53, INT_1:def 4; :: thesis:

end;

then h . b divides E - 0 by A32, A35, Th1;
hence h . b divides E ; :: thesis:

end;

Product h divides E

proof

per cases ;

suppose E >= 0 ; :: thesis:

hence Product h divides E by A30, A31, A15, INT_4:38; :: thesis:

end;

suppose E < 0 ; :: thesis:

then reconsider mE = - E as Element of NAT by INT_1:3;
for b being Element of NAT st b in dom h holds
h . b divides mE by A31, INT_2:10;
hence Product h divides E by INT_2:10, A30, A15, INT_4:38; :: thesis:

end;

then Product h divides E - 0 ;
hence eval (p,(@ ((<%Z1,x%> ^ X) ^ YC))), 0 are_congruent_mod 1 + ((Z1 + 1) * (K !)) by A29, INT_1:def 4; :: thesis:
let i be Nat; :: thesis:
assume A54: i in k ; :: thesis:
set YCe = ((YC . i) + 1) + (- (idseq (x + 1)));
A55: ( dom (((YC . i) + 1) + (- (idseq (x + 1)))) = dom (- (idseq (x + 1))) & dom (- (idseq (x + 1))) = dom (idseq (x + 1)) ) by VALUED_1:def 2, VALUED_1:8;
A56: for j being Nat st j in dom (((YC . i) + 1) + (- (idseq (x + 1)))) holds
(((YC . i) + 1) + (- (idseq (x + 1)))) . j = ((YC . i) + 1) - j

proof

let j be Nat; :: thesis:
assume A57: j in dom (((YC . i) + 1) + (- (idseq (x + 1)))) ; :: thesis:
thus (((YC . i) + 1) + (- (idseq (x + 1)))) . j = ((YC . i) + 1) + ((- (idseq (x + 1))) . j) by A57, VALUED_1:def 2
.= ((YC . i) + 1) + (- ((idseq (x + 1)) . j)) by VALUED_1:8
.= ((YC . i) + 1) + (- j) by A57, A55, FINSEQ_2:49
.= ((YC . i) + 1) - j ; :: thesis:

end;

rng (((YC . i) + 1) + (- (idseq (x + 1)))) c= NAT

proof

let b be Integer; :: according to MEMBERED:def 11 :: thesis:
assume b in rng (((YC . i) + 1) + (- (idseq (x + 1)))) ; :: thesis:
then consider a being object such that
A58: ( a in dom (((YC . i) + 1) + (- (idseq (x + 1)))) & (((YC . i) + 1) + (- (idseq (x + 1)))) . a = b ) by FUNCT_1:def 3;
reconsider a = a as Nat by A58;
A59: (((YC . i) + 1) + (- (idseq (x + 1)))) . a = ((YC . i) + 1) - a by A56, A58;
( YC . i > x + 1 & x + 1 >= a ) by A27, A54, A55, A58, FINSEQ_1:1;
then YC . i > a by XXREAL_0:2;
then (YC . i) + 1 > a by NAT_1:13;
then ((YC . i) + 1) - a is Nat by NAT_1:21;
hence b in NAT by A58, A59, ORDINAL1:def 12; :: thesis:

end;

then reconsider YCe = ((YC . i) + 1) + (- (idseq (x + 1))) as FinSequence of NAT by FINSEQ_1:def 4;
reconsider PP = Product YCe as Element of NAT ;
A60: for b being Element of NAT st b in dom h holds
h . b divides PP

proof

let b be Element of NAT ; :: thesis:
assume A61: b in dom h ; :: thesis:
( 1 <= b & b <= x + 1 ) by A61, A10, FINSEQ_3:25;
then reconsider b1 = b - 1 as Nat ;
(YY . b1) . i in { ((YY . i) . j) where i, j is Nat : S₂[i,j] } ;
then reconsider YYb1i = (YY . b1) . i as Nat by A8;
b1 + 1 <= x + 1 by A61, A10, FINSEQ_3:25;
then b1 < Segm (x + 1) by NAT_1:13;
then A62: b1 in x + 1 by NAT_1:44;
then S₁[b1,YY . b1] by A6;
then A63: YYb1i <= x by A54;
YC . i,YYb1i are_congruent_mod h . (b1 + 1) by A62, A27, A54;
then A64: h . b divides (YC . i) - YYb1i by INT_1:def 4;
( 0 + 1 <= YYb1i + 1 & YYb1i + 1 <= x + 1 ) by A63, XREAL_1:7;
then A65: YYb1i + 1 in dom YCe by A55;
then A66: YCe . (YYb1i + 1) = ((YC . i) + 1) - (YYb1i + 1) by A56;
YCe . (YYb1i + 1) divides PP by A65, INT_4:32;
hence h . b divides PP by A66, A64, INT_2:9; :: thesis:

end;

Product h divides PP - 0 by A30, A60, A15, INT_4:38;
hence Product (((YC . i) + 1) + (- (idseq (x + 1)))), 0 are_congruent_mod 1 + ((Z1 + 1) * (K !)) by INT_1:def 4, A29; :: thesis:

end;

given Y being k -element XFinSequence of NAT , Z, K being Element of NAT such that A67: ( K > x & K >= (sum_of_coefficients |.p.|) * ((((x ^2) + 1) * (Product (1 + X))) |^ (degree p)) ) and
A68: for i being Nat st i in k holds
Y . i > x + 1 and
A69: ( 1 + ((Z + 1) * (K !)) = Product (1 + ((K !) * (idseq (x + 1)))) & eval (p,(@ ((<%Z,x%> ^ X) ^ Y))), 0 are_congruent_mod 1 + ((Z + 1) * (K !)) ) and
A70: for i being Nat st i in k holds
Product (((Y . i) + 1) + (- (idseq (x + 1)))), 0 are_congruent_mod 1 + ((Z + 1) * (K !)) ; :: thesis:
let z be Element of NAT ; :: thesis:
assume A71: z <= x ; :: thesis:
set z1 = z + 1;
set K1 = K ! ;
set ZZ = 1 + ((z + 1) * (K !));
A72: 1 + ((z + 1) * (K !)) > 1 + 0 by XREAL_1:8;
consider prim being Element of NAT such that
A73: ( prim divides 1 + ((z + 1) * (K !)) & prim <= 1 + ((z + 1) * (K !)) & prim is prime ) by A72, NAT_4:13;
deffunc H₁( object ) -> Element of omega = (Y . $1) mod prim;
consider Yz being XFinSequence such that
A74: ( len Yz = k & ( for i being Nat st i in k holds
Yz . i = H₁(i) ) ) from AFINSQ_1:sch 2();
rng Yz c= NAT

proof

let y be object ; :: according to TARSKI:def 3 :: thesis:
assume y in rng Yz ; :: thesis:
then consider x being object such that
A75: ( x in dom Yz & Yz . x = y ) by FUNCT_1:def 3;
y = H₁(x) by A74, A75;
hence y in NAT by ORDINAL1:def 12; :: thesis:

end;

then reconsider Yz = Yz as k -element XFinSequence of NAT by A74, RELAT_1:def 19, CARD_1:def 7;
take Yz ; :: thesis:
( 1 <= z + 1 & z + 1 <= x + 1 ) by A71, NAT_1:11, XREAL_1:6;
then A76: z + 1 in Seg (x + 1) ;
K >= x + 1 by A67, NAT_1:13;
then reconsider h = 1 + ((K !) * (idseq (x + 1))) as CR_Sequence by Th2;
rng h c= NAT by VALUED_0:def 6;
then A77: h is FinSequence of NAT by FINSEQ_1:def 4;
A78: ( dom h = dom ((K !) * (idseq (x + 1))) & dom ((K !) * (idseq (x + 1))) = dom (idseq (x + 1)) ) by VALUED_1:def 2, VALUED_1:def 5;
A79: h . (z + 1) = 1 + (((K !) * (idseq (x + 1))) . (z + 1)) by A76, A78, VALUED_1:def 2
.= 1 + ((K !) * ((idseq (x + 1)) . (z + 1))) by A76, A78, VALUED_1:def 5
.= 1 + ((z + 1) * (K !)) by A76, FINSEQ_2:49 ;
1 + ((z + 1) * (K !)) divides 1 + ((Z + 1) * (K !)) by A79, A69, A77, INT_4:32, A76, A78;
then A80: prim divides 1 + ((Z + 1) * (K !)) by A73, INT_2:9;
1 + ((Z + 1) * (K !)) divides (eval (p,(@ ((<%Z,x%> ^ X) ^ Y)))) - 0 by A69, INT_1:def 4;
then A81: prim divides eval (p,(@ ((<%Z,x%> ^ X) ^ Y))) by A80, INT_2:9;
reconsider E1 = eval (p,(@ ((<%Z,x%> ^ X) ^ Y))) as Integer ;
A82: K < prim

proof

assume K >= prim ; :: thesis:
then prim divides (Z + 1) * (K !) by INT_2:2, A73, NEWTON:41;
then prim divides 1 by A80, INT_2:1;
then prim = 1 by INT_2:13;
hence contradiction by A73, INT_2:def 4; :: thesis:

end;

A83: ( len <%z,x%> = 2 & 2 = len <%Z,x%> ) by CARD_1:def 7;
A84: ( len (<%z,x%> ^ X) = 2 + n & 2 + n = len (<%Z,x%> ^ X) ) by CARD_1:def 7;
A85: ( len Y = k & k = len Yz ) by CARD_1:def 7;
A86: len ((<%z,x%> ^ X) ^ Yz) = (2 + k) + n by CARD_1:def 7;
thus for i being Nat st i in k holds
Yz . i <= x :: thesis:

proof

let j be Nat; :: thesis:
assume A87: j in k ; :: thesis:
set YE = ((Y . j) + 1) + (- (idseq (x + 1)));
A88: Yz . j = (Y . j) mod prim by A87, A74;
A89: 1 + ((Z + 1) * (K !)) divides (Product (((Y . j) + 1) + (- (idseq (x + 1))))) - 0 by INT_1:def 4, A70, A87;
A90: ( len (((Y . j) + 1) + (- (idseq (x + 1)))) = len (idseq (x + 1)) & len (idseq (x + 1)) = x + 1 ) by CARD_1:def 7;
A91: for w being Nat st w in dom (((Y . j) + 1) + (- (idseq (x + 1)))) holds
(((Y . j) + 1) + (- (idseq (x + 1)))) . w = ((Y . j) + 1) - w

proof

let w be Nat; :: thesis:
assume A92: w in dom (((Y . j) + 1) + (- (idseq (x + 1)))) ; :: thesis:
then w in dom (- (idseq (x + 1))) by VALUED_1:def 2;
then w in dom (idseq (x + 1)) by VALUED_1:8;
then (idseq (x + 1)) . w = w by FINSEQ_2:49;
then (- (idseq (x + 1))) . w = - w by VALUED_1:8;
then (((Y . j) + 1) + (- (idseq (x + 1)))) . w = ((Y . j) + 1) + (- w) by A92, VALUED_1:def 2;
hence (((Y . j) + 1) + (- (idseq (x + 1)))) . w = ((Y . j) + 1) - w ; :: thesis:

end;

A93: now :: thesis:

let a be Nat; :: thesis:
assume A94: a in dom (((Y . j) + 1) + (- (idseq (x + 1)))) ; :: thesis:
then ( 1 <= a & a <= x + 1 ) by A90, FINSEQ_3:25;
then reconsider a1 = a - 1 as Nat ;
a1 + 1 <= x + 1 by A94, A90, FINSEQ_3:25;
then a1 < x + 1 by NAT_1:13;
then A95: (x + 1) - a1 > 0 by XREAL_1:50;
(((Y . j) + 1) + (- (idseq (x + 1)))) . a = ((Y . j) + 1) - a by A94, A91;
then ((((Y . j) + 1) + (- (idseq (x + 1)))) . a) + a1 > x + 1 by A68, A87;
hence (((Y . j) + 1) + (- (idseq (x + 1)))) . a > 0 by A95, XREAL_1:19; :: thesis:

end;

now :: thesis:

let r be object ; :: thesis:
assume r in rng (((Y . j) + 1) + (- (idseq (x + 1)))) ; :: thesis:
then consider a being object such that
A96: ( a in dom (((Y . j) + 1) + (- (idseq (x + 1)))) & (((Y . j) + 1) + (- (idseq (x + 1)))) . a = r ) by FUNCT_1:def 3;
reconsider a = a as Nat by A96;
(((Y . j) + 1) + (- (idseq (x + 1)))) . a > 0 by A93, A96;
hence r in NAT by A96, INT_1:3; :: thesis:

end;

then A97: ((Y . j) + 1) + (- (idseq (x + 1))) is FinSequence of NAT by FINSEQ_1:def 4, TARSKI:def 3;
((Y . j) + 1) + (- (idseq (x + 1))) is positive-yielding

proof

let r be Real; :: according to PARTFUN3:def 1 :: thesis:
assume r in rng (((Y . j) + 1) + (- (idseq (x + 1)))) ; :: thesis:
then consider a being object such that
A98: ( a in dom (((Y . j) + 1) + (- (idseq (x + 1)))) & (((Y . j) + 1) + (- (idseq (x + 1)))) . a = r ) by FUNCT_1:def 3;
thus not r <= 0 by A93, A98; :: thesis:

end;

then consider w being Nat such that
A99: ( w in dom (((Y . j) + 1) + (- (idseq (x + 1)))) & prim divides (((Y . j) + 1) + (- (idseq (x + 1)))) . w ) by A89, A80, INT_2:9, Th12, A73, A97;
A100: ( 1 <= w & w <= x + 1 ) by A90, A99, FINSEQ_3:25;
then reconsider w1 = w - 1 as Nat ;
prim divides ((Y . j) + 1) - w by A99, A91;
then prim divides (Y . j) - w1 ;
then Yz . j = w1 mod prim by A88, INT_4:23, A73;
then Yz . j < w1 + 1 by NAT_1:13, NEWTON05:11;
then Yz . j < x + 1 by A100, XXREAL_0:2;
hence Yz . j <= x by NAT_1:13; :: thesis:

end;

for i being Nat st i in (2 + k) + n holds
prim divides (((<%Z,x%> ^ X) ^ Y) . i) - (((<%z,x%> ^ X) ^ Yz) . i)

proof

let i be Nat; :: thesis:
assume A101: i in (2 + k) + n ; :: thesis:

per cases by A101, A86, AFINSQ_1:20;

suppose A102: i in dom (<%z,x%> ^ X) ; :: thesis:

then A103: ( ((<%z,x%> ^ X) ^ Yz) . i = (<%z,x%> ^ X) . i & ((<%Z,x%> ^ X) ^ Y) . i = (<%Z,x%> ^ X) . i ) by A84, AFINSQ_1:def 3;

per cases by A102, AFINSQ_1:20;

suppose i in dom <%z,x%> ; :: thesis:

then A104: ( i in Segm 2 & (<%z,x%> ^ X) . i = <%z,x%> . i & (<%Z,x%> ^ X) . i = <%Z,x%> . i ) by A83, AFINSQ_1:def 3;

per cases by A104, NAT_1:23, NAT_1:44;

suppose i = 0 ; :: thesis:

then A105: ( ((<%Z,x%> ^ X) ^ Y) . i = Z & ((<%z,x%> ^ X) ^ Yz) . i = z ) by A102, A84, AFINSQ_1:def 3, A104;
A106: K ! ,prim are_coprime

proof

assume not K ! ,prim are_coprime ; :: thesis:
then A107: (K !) gcd prim <> 1 by INT_2:def 3;
(K !) gcd prim divides prim by INT_2:def 2;
then (K !) gcd prim = prim by A107, A73, INT_2:def 4;
then prim divides K ! by INT_2:def 2;
hence contradiction by A82, NAT_4:19, A73; :: thesis:

end;

prim divides (1 + ((Z + 1) * (K !))) - (1 + ((z + 1) * (K !))) by A80, A73, INT_5:1;
then prim divides (Z - z) * (K !) ;
hence prim divides (((<%Z,x%> ^ X) ^ Y) . i) - (((<%z,x%> ^ X) ^ Yz) . i) by A105, A106, INT_2:25; :: thesis:

end;

suppose i = 1 ; :: thesis:

hence prim divides (((<%Z,x%> ^ X) ^ Y) . i) - (((<%z,x%> ^ X) ^ Yz) . i) by A103, A104, INT_2:12; :: thesis:

end;

suppose ex j being Nat st
( j in dom X & i = (len <%z,x%>) + j ) ; :: thesis:

then consider j being Nat such that
A108: ( j in dom X & i = (len <%z,x%>) + j ) ;
( (<%z,x%> ^ X) . i = X . j & (<%Z,x%> ^ X) . i = X . j ) by A83, A108, AFINSQ_1:def 3;
hence prim divides (((<%Z,x%> ^ X) ^ Y) . i) - (((<%z,x%> ^ X) ^ Yz) . i) by INT_2:12, A103; :: thesis:

end;

suppose ex j being Nat st
( j in dom Yz & i = (len (<%z,x%> ^ X)) + j ) ; :: thesis:

then consider j being Nat such that
A109: ( j in dom Yz & i = (len (<%z,x%> ^ X)) + j ) ;
A110: ( ((<%Z,x%> ^ X) ^ Y) . i = Y . j & ((<%z,x%> ^ X) ^ Yz) . i = Yz . j ) by A84, A85, A109, AFINSQ_1:def 3;
Yz . j = (Y . j) mod prim by A74, A109;
hence prim divides (((<%Z,x%> ^ X) ^ Y) . i) - (((<%z,x%> ^ X) ^ Yz) . i) by A110, A73, PEPIN:8; :: thesis:

end;

then prim divides E1 - (eval (p,(@ ((<%z,x%> ^ X) ^ Yz)))) by A73, Th1;
then prim divides eval (p,(@ ((<%z,x%> ^ X) ^ Yz))) by INT_5:2, A81;
then |.prim.| divides |.(eval (p,(@ ((<%z,x%> ^ X) ^ Yz)))).| by INT_2:16;
then consider m being Nat such that
A111: |.(eval (p,(@ ((<%z,x%> ^ X) ^ Yz)))).| = prim * m by NAT_D:def 3;
A112: x ^2 = x * x by SQUARE_1:def 1;
for i being object st i in dom (@ ((<%z,x%> ^ X) ^ Yz)) holds
|.((@ ((<%z,x%> ^ X) ^ Yz)) . i).| <= ((x ^2) + 1) * (Product (1 + X))

proof

let i be object ; :: thesis:
assume i in dom (@ ((<%z,x%> ^ X) ^ Yz)) ; :: thesis:
then A113: ( i in dom ((<%z,x%> ^ X) ^ Yz) & (<%z,x%> ^ X) ^ Yz = @ ((<%z,x%> ^ X) ^ Yz) ) by HILB10_2:def 1;
reconsider i = i as Nat by A113;

per cases by A113, AFINSQ_1:20;

suppose A114: i in dom (<%z,x%> ^ X) ; :: thesis:

then A115: (@ ((<%z,x%> ^ X) ^ Yz)) . i = (<%z,x%> ^ X) . i by A113, AFINSQ_1:def 3;

per cases by A114, AFINSQ_1:20;

suppose i in dom <%z,x%> ; :: thesis:

then A116: ( i in Segm 2 & (<%z,x%> ^ X) . i = <%z,x%> . i ) by CARD_1:def 7, AFINSQ_1:def 3;
A117: Product (1 + X) >= 1 by NAT_1:14;
x ^2 >= x * 1 by NAT_1:14, A112, XREAL_1:64;
then (x ^2) + 1 >= x + 0 by XREAL_1:7;
then A118: ((x ^2) + 1) * (Product (1 + X)) >= x * 1 by A117, XREAL_1:66;
( i = 0 or i = 1 ) by A116, NAT_1:23, NAT_1:44;
hence |.((@ ((<%z,x%> ^ X) ^ Yz)) . i).| <= ((x ^2) + 1) * (Product (1 + X)) by A118, A71, XXREAL_0:2, A115, A116; :: thesis:

end;

suppose ex j being Nat st
( j in dom X & i = (len <%z,x%>) + j ) ; :: thesis:

then consider j being Nat such that
A119: ( j in dom X & i = (len <%z,x%>) + j ) ;
A120: dom (1 + X) = dom X by VALUED_1:def 2;
then A121: (1 + X) . j <= Product (1 + X) by A119, HILB10_4:11;
(1 + X) . j = 1 + (X . j) by A119, A120, VALUED_1:def 2;
then A122: X . j <= Product (1 + X) by A121, NAT_1:13;
(x ^2) + 1 >= 1 by NAT_1:11;
then 1 * (X . j) <= ((x ^2) + 1) * (Product (1 + X)) by A122, XREAL_1:66;
hence |.((@ ((<%z,x%> ^ X) ^ Yz)) . i).| <= ((x ^2) + 1) * (Product (1 + X)) by A119, AFINSQ_1:def 3, A115; :: thesis:

end;

suppose ex j being Nat st
( j in dom Yz & i = (len (<%z,x%> ^ X)) + j ) ; :: thesis:

then consider j being Nat such that
A123: ( j in dom Yz & i = (len (<%z,x%> ^ X)) + j ) ;
set YE = ((Y . j) + 1) + (- (idseq (x + 1)));
A124: ((<%z,x%> ^ X) ^ Yz) . i = Yz . j by A123, AFINSQ_1:def 3;
A125: Yz . j = (Y . j) mod prim by A123, A74;
A126: 1 + ((Z + 1) * (K !)) divides (Product (((Y . j) + 1) + (- (idseq (x + 1))))) - 0 by INT_1:def 4, A70, A123, A74;
A127: ( len (((Y . j) + 1) + (- (idseq (x + 1)))) = len (idseq (x + 1)) & len (idseq (x + 1)) = x + 1 ) by CARD_1:def 7;
A128: for w being Nat st w in dom (((Y . j) + 1) + (- (idseq (x + 1)))) holds
(((Y . j) + 1) + (- (idseq (x + 1)))) . w = ((Y . j) + 1) - w

proof

let w be Nat; :: thesis:
assume A129: w in dom (((Y . j) + 1) + (- (idseq (x + 1)))) ; :: thesis:
then w in dom (- (idseq (x + 1))) by VALUED_1:def 2;
then w in dom (idseq (x + 1)) by VALUED_1:8;
then (idseq (x + 1)) . w = w by FINSEQ_2:49;
then (- (idseq (x + 1))) . w = - w by VALUED_1:8;
then (((Y . j) + 1) + (- (idseq (x + 1)))) . w = ((Y . j) + 1) + (- w) by A129, VALUED_1:def 2;
hence (((Y . j) + 1) + (- (idseq (x + 1)))) . w = ((Y . j) + 1) - w ; :: thesis:

end;

A130: now :: thesis:

let a be Nat; :: thesis:
assume A131: a in dom (((Y . j) + 1) + (- (idseq (x + 1)))) ; :: thesis:
( 1 <= a & a <= x + 1 ) by A131, A127, FINSEQ_3:25;
then reconsider a1 = a - 1 as Nat ;
a1 + 1 <= x + 1 by A131, A127, FINSEQ_3:25;
then a1 < x + 1 by NAT_1:13;
then A132: (x + 1) - a1 > 0 by XREAL_1:50;
(((Y . j) + 1) + (- (idseq (x + 1)))) . a = ((Y . j) + 1) - a by A131, A128;
then ((((Y . j) + 1) + (- (idseq (x + 1)))) . a) + a1 > x + 1 by A68, A85, A123;
hence (((Y . j) + 1) + (- (idseq (x + 1)))) . a > 0 by A132, XREAL_1:19; :: thesis:

end;

now :: thesis:

let r be object ; :: thesis:
assume r in rng (((Y . j) + 1) + (- (idseq (x + 1)))) ; :: thesis:
then consider a being object such that
A133: ( a in dom (((Y . j) + 1) + (- (idseq (x + 1)))) & (((Y . j) + 1) + (- (idseq (x + 1)))) . a = r ) by FUNCT_1:def 3;
reconsider a = a as Nat by A133;
(((Y . j) + 1) + (- (idseq (x + 1)))) . a > 0 by A130, A133;
hence r in NAT by A133, INT_1:3; :: thesis:

end;

then A134: ((Y . j) + 1) + (- (idseq (x + 1))) is FinSequence of NAT by FINSEQ_1:def 4, TARSKI:def 3;
((Y . j) + 1) + (- (idseq (x + 1))) is positive-yielding

proof

let r be Real; :: according to PARTFUN3:def 1 :: thesis:
assume r in rng (((Y . j) + 1) + (- (idseq (x + 1)))) ; :: thesis:
then consider a being object such that
A135: ( a in dom (((Y . j) + 1) + (- (idseq (x + 1)))) & (((Y . j) + 1) + (- (idseq (x + 1)))) . a = r ) by FUNCT_1:def 3;
thus not r <= 0 by A130, A135; :: thesis:

end;

then consider w being Nat such that
A136: ( w in dom (((Y . j) + 1) + (- (idseq (x + 1)))) & prim divides (((Y . j) + 1) + (- (idseq (x + 1)))) . w ) by A126, A80, INT_2:9, Th12, A73, A134;
A137: ( 1 <= w & w <= x + 1 ) by A127, A136, FINSEQ_3:25;
then reconsider w1 = w - 1 as Nat ;
prim divides ((Y . j) + 1) - w by A136, A128;
then prim divides (Y . j) - w1 ;
then Yz . j = w1 mod prim by A125, INT_4:23, A73;
then Yz . j < w1 + 1 by NAT_1:13, NEWTON05:11;
then A138: Yz . j < x + 1 by A137, XXREAL_0:2;
x ^2 >= x * 1 by NAT_1:14, A112, XREAL_1:64;
then (x ^2) + 1 >= x + 1 by XREAL_1:7;
then A139: Yz . j < (x ^2) + 1 by A138, XXREAL_0:2;
Product (1 + X) >= 1 by NAT_1:14;
then 1 * (Yz . j) <= ((x ^2) + 1) * (Product (1 + X)) by A139, XREAL_1:66;
hence |.((@ ((<%z,x%> ^ X) ^ Yz)) . i).| <= ((x ^2) + 1) * (Product (1 + X)) by A124, A113; :: thesis:

end;

then |.(eval (p,(@ ((<%z,x%> ^ X) ^ Yz)))).| <= (sum_of_coefficients |.p.|) * ((((x ^2) + 1) * (Product (1 + X))) |^ (degree p)) by NAT_1:14, Th10;
then |.(eval (p,(@ ((<%z,x%> ^ X) ^ Yz)))).| <= K by A67, XXREAL_0:2;
then prim * m < prim * 1 by A111, A82, XXREAL_0:2;
then m < 1 by XREAL_1:66;
then m = 0 by NAT_1:14;
hence eval (p,(@ ((<%z,x%> ^ X) ^ Yz))) = 0 by A111; :: thesis: