let n, k be Nat; :: thesis: for p being INT -valued Polynomial of ((2 + n) + k),F_Real holds { X where X is n -element XFinSequence of NAT : ex x being Element of NAT st
for z being Element of NAT st z <= x holds
ex y being k -element XFinSequence of NAT st eval (p,(@ ((<%z,x%> ^ X) ^ y))) = 0 } is diophantine Subset of (n -xtuples_of NAT)
let p be INT -valued Polynomial of ((2 + n) + k),F_Real; :: thesis: { X where X is n -element XFinSequence of NAT : ex x being Element of NAT st
for z being Element of NAT st z <= x holds
ex y being k -element XFinSequence of NAT st eval (p,(@ ((<%z,x%> ^ X) ^ y))) = 0 } is diophantine Subset of (n -xtuples_of NAT)
set X0 = { X where X is n -element XFinSequence of NAT : ex x being Element of NAT st
for z being Element of NAT st z <= x holds
ex y being k -element XFinSequence of NAT st eval (p,(@ ((<%z,x%> ^ X) ^ y))) = 0 } ;
set NK = (1 + n) + k;
set sum = sum_of_coefficients |.p.|;
set Deg = degree p;
A1: ( 0 < ((1 + n) + k) + 4 & ((1 + n) + k) + 0 < ((1 + n) + k) + 4 & ((1 + n) + k) + 1 < ((1 + n) + k) + 4 & ((1 + n) + k) + 2 < ((1 + n) + k) + 4 & ((1 + n) + k) + 3 < ((1 + n) + k) + 4 ) by XREAL_1:8;
then ( 0 in Segm (((1 + n) + k) + 4) & ((1 + n) + k) + 0 in Segm (((1 + n) + k) + 4) & ((1 + n) + k) + 1 in Segm (((1 + n) + k) + 4) & ((1 + n) + k) + 2 in Segm (((1 + n) + k) + 4) & ((1 + n) + k) + 3 in Segm (((1 + n) + k) + 4) ) by NAT_1:44;
then reconsider ZERO = 0 , i0 = (1 + n) + k, i1 = ((1 + n) + k) + 1, i2 = ((1 + n) + k) + 2, i3 = ((1 + n) + k) + 3 as Element of ((1 + n) + k) + 4 ;
defpred S1[ XFinSequence of NAT ] means 1 * ($1 . i1) > (1 * ($1 . ZERO)) + 0;
A2: { q where q is ((1 + n) + k) + 4 -element XFinSequence of NAT : S1[q] } is diophantine Subset of ((((1 + n) + k) + 4) -xtuples_of NAT) by HILB10_3:7;
defpred S2[ XFinSequence of NAT ] means $1 . i1 >= (sum_of_coefficients |.p.|) * (((((($1 . ZERO) ^2) + 1) * (Product (1 + (($1 /^ 1) | n)))) * ((1 * ($1 . i0)) + 0)) |^ ((0 * ($1 . i0)) + (degree p)));
1 + n <= (1 + n) + k by NAT_1:11;
then A3: { q where q is ((1 + n) + k) + 4 -element XFinSequence of NAT : S2[q] } is diophantine Subset of ((((1 + n) + k) + 4) -xtuples_of NAT) by Th11, A1, XXREAL_0:2;
defpred S3[ XFinSequence of NAT ] means for i being Nat st i in k holds
( $1 . ((1 + n) + i) > $1 . i0 & Product ((($1 . ((1 + n) + i)) + 1) + (- (idseq ($1 . i0)))), 0 are_congruent_mod $1 . i2 );
A4: { q where q is ((1 + n) + k) + 4 -element XFinSequence of NAT : S3[q] } is diophantine Subset of ((((1 + n) + k) + 4) -xtuples_of NAT)
proof
defpred S4[ Nat, Nat, Nat, Nat] means ( Product (($1 + 1) + (- (idseq $2))), 0 are_congruent_mod $3 & $1 > $2 );
A5: for i1, i2, i3, i4 being Element of ((1 + n) + k) + 4 holds { q where q is ((1 + n) + k) + 4 -element XFinSequence of NAT : S4[q . i1,q . i2,q . i3,q . i4] } is diophantine Subset of ((((1 + n) + k) + 4) -xtuples_of NAT)
proof
let i1, i2, i3, i4 be Element of ((1 + n) + k) + 4; :: thesis: { q where q is ((1 + n) + k) + 4 -element XFinSequence of NAT : S4[q . i1,q . i2,q . i3,q . i4] } is diophantine Subset of ((((1 + n) + k) + 4) -xtuples_of NAT)
set NK5 = (((1 + n) + k) + 4) + 1;
A6: (((1 + n) + k) + 4) + 0 < (((1 + n) + k) + 4) + 1 by NAT_1:13;
then ((1 + n) + k) + 4 in Segm ((((1 + n) + k) + 4) + 1) by NAT_1:44;
then reconsider I1 = i1, I2 = i2, I3 = i3, I4 = i4, M0 = ((1 + n) + k) + 4 as Element of (((1 + n) + k) + 4) + 1 by HILB10_3:2;
defpred S5[ XFinSequence of NAT ] means ( $1 . M0 = Product ((($1 . I1) + 1) + (- (idseq ($1 . I2)))) & $1 . I1 > $1 . I2 );
A7: { q where q is (((1 + n) + k) + 4) + 1 -element XFinSequence of NAT : S5[q] } is diophantine Subset of (((((1 + n) + k) + 4) + 1) -xtuples_of NAT) by HILB10_4:38;
defpred S6[ XFinSequence of NAT ] means 1 * ($1 . M0),0 * ($1 . I4) are_congruent_mod 1 * ($1 . I3);
A8: { q where q is (((1 + n) + k) + 4) + 1 -element XFinSequence of NAT : S6[q] } is diophantine Subset of (((((1 + n) + k) + 4) + 1) -xtuples_of NAT) by HILB10_3:21;
set GH = { q where q is (((1 + n) + k) + 4) + 1 -element XFinSequence of NAT : ( S5[q] & S6[q] ) } ;
set GHr = { (q | (((1 + n) + k) + 4)) where q is (((1 + n) + k) + 4) + 1 -element XFinSequence of NAT : q in { q where q is (((1 + n) + k) + 4) + 1 -element XFinSequence of NAT : ( S5[q] & S6[q] ) } } ;
set QQ = { q where q is ((1 + n) + k) + 4 -element XFinSequence of NAT : S4[q . i1,q . i2,q . i3,q . i4] } ;
A9: { q where q is (((1 + n) + k) + 4) + 1 -element XFinSequence of NAT : ( S5[q] & S6[q] ) } is diophantine Subset of (((((1 + n) + k) + 4) + 1) -xtuples_of NAT) from HILB10_3:sch 3(A7, A8);
 A10: { (q | (((1 + n) + k) + 4)) where q is (((1 + n) + k) + 4) + 1 -element XFinSequence of NAT : q in { q where q is (((1 + n) + k) + 4) + 1 -element XFinSequence of NAT : ( S5[q] & S6[q] ) } } is diophantine Subset of ((((1 + n) + k) + 4) -xtuples_of NAT) by A9, NAT_1:11, HILB10_3:5;
A11: { (q | (((1 + n) + k) + 4)) where q is (((1 + n) + k) + 4) + 1 -element XFinSequence of NAT : q in { q where q is (((1 + n) + k) + 4) + 1 -element XFinSequence of NAT : ( S5[q] & S6[q] ) } } c= { q where q is ((1 + n) + k) + 4 -element XFinSequence of NAT : S4[q . i1,q . i2,q . i3,q . i4] }
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in { (q | (((1 + n) + k) + 4)) where q is (((1 + n) + k) + 4) + 1 -element XFinSequence of NAT : q in { q where q is (((1 + n) + k) + 4) + 1 -element XFinSequence of NAT : ( S5[q] & S6[q] ) } } or y in { q where q is ((1 + n) + k) + 4 -element XFinSequence of NAT : S4[q . i1,q . i2,q . i3,q . i4] } )
assume A12: y in { (q | (((1 + n) + k) + 4)) where q is (((1 + n) + k) + 4) + 1 -element XFinSequence of NAT : q in { q where q is (((1 + n) + k) + 4) + 1 -element XFinSequence of NAT : ( S5[q] & S6[q] ) } } ; :: thesis: y in { q where q is ((1 + n) + k) + 4 -element XFinSequence of NAT : S4[q . i1,q . i2,q . i3,q . i4] }
consider q being (((1 + n) + k) + 4) + 1 -element XFinSequence of NAT such that
A13: ( y = q | (((1 + n) + k) + 4) & q in { q where q is (((1 + n) + k) + 4) + 1 -element XFinSequence of NAT : ( S5[q] & S6[q] ) } ) by A12;
A14: ex w being (((1 + n) + k) + 4) + 1 -element XFinSequence of NAT st
( w = q & S5[w] & S6[w] ) by A13;
len q = (((1 + n) + k) + 4) + 1 by CARD_1:def 7;
then len (q | (((1 + n) + k) + 4)) = ((1 + n) + k) + 4 by A6, AFINSQ_1:54;
then reconsider Q = q | (((1 + n) + k) + 4) as ((1 + n) + k) + 4 -element XFinSequence of NAT by CARD_1:def 7;
( Q . i1 = q . I1 & Q . i2 = q . I2 & Q . i3 = q . I3 & Q . i4 = q . I4 ) by HILB10_3:4;
hence y in { q where q is ((1 + n) + k) + 4 -element XFinSequence of NAT : S4[q . i1,q . i2,q . i3,q . i4] } by A14, A13; :: thesis: verum
end;
{ q where q is ((1 + n) + k) + 4 -element XFinSequence of NAT : S4[q . i1,q . i2,q . i3,q . i4] } c= { (q | (((1 + n) + k) + 4)) where q is (((1 + n) + k) + 4) + 1 -element XFinSequence of NAT : q in { q where q is (((1 + n) + k) + 4) + 1 -element XFinSequence of NAT : ( S5[q] & S6[q] ) } }
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in { q where q is ((1 + n) + k) + 4 -element XFinSequence of NAT : S4[q . i1,q . i2,q . i3,q . i4] } or y in { (q | (((1 + n) + k) + 4)) where q is (((1 + n) + k) + 4) + 1 -element XFinSequence of NAT : q in { q where q is (((1 + n) + k) + 4) + 1 -element XFinSequence of NAT : ( S5[q] & S6[q] ) } } )
assume y in { q where q is ((1 + n) + k) + 4 -element XFinSequence of NAT : S4[q . i1,q . i2,q . i3,q . i4] } ; :: thesis: y in { (q | (((1 + n) + k) + 4)) where q is (((1 + n) + k) + 4) + 1 -element XFinSequence of NAT : q in { q where q is (((1 + n) + k) + 4) + 1 -element XFinSequence of NAT : ( S5[q] & S6[q] ) } }
then consider q being ((1 + n) + k) + 4 -element XFinSequence of NAT such that
A15: ( y = q & S4[q . i1,q . i2,q . i3,q . i4] ) ;
Product (((q . i1) + 1) + (- (idseq (q . i2)))) = ((q . i2) !) * ((q . i1) choose (q . i2)) by HILB10_4:23, A15;
then reconsider P = Product (((q . i1) + 1) + (- (idseq (q . i2)))) as Element of NAT ;
set qP = q ^ <%P%>;
A16: len q = ((1 + n) + k) + 4 by CARD_1:def 7;
A17: (q ^ <%P%>) | (((1 + n) + k) + 4) = q by A16, AFINSQ_1:57;
( (q ^ <%P%>) . i1 = q . i1 & (q ^ <%P%>) . i2 = q . i2 & (q ^ <%P%>) . i3 = q . i3 ) by A17, HILB10_3:4;
then ( S5[q ^ <%P%>] & S6[q ^ <%P%>] ) by A16, AFINSQ_1:36, A15;
then q ^ <%P%> in { q where q is (((1 + n) + k) + 4) + 1 -element XFinSequence of NAT : ( S5[q] & S6[q] ) } ;
hence y in { (q | (((1 + n) + k) + 4)) where q is (((1 + n) + k) + 4) + 1 -element XFinSequence of NAT : q in { q where q is (((1 + n) + k) + 4) + 1 -element XFinSequence of NAT : ( S5[q] & S6[q] ) } } by A15, A17; :: thesis: verum
end;
hence { q where q is ((1 + n) + k) + 4 -element XFinSequence of NAT : S4[q . i1,q . i2,q . i3,q . i4] } is diophantine Subset of ((((1 + n) + k) + 4) -xtuples_of NAT) by A10, A11, XBOOLE_0:def 10; :: thesis: verum
end;
set SN = { ((1 + n) + i) where i is Nat : i in k } ;
A18: { ((1 + n) + i) where i is Nat : i in k } c= Segm (((1 + n) + k) + 4)
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { ((1 + n) + i) where i is Nat : i in k } or x in Segm (((1 + n) + k) + 4) )
assume x in { ((1 + n) + i) where i is Nat : i in k } ; :: thesis: x in Segm (((1 + n) + k) + 4)
then consider i being Nat such that
A19: ( x = (1 + n) + i & i in k ) ;
i in Segm k by A19;
then i + 0 < k + 4 by NAT_1:44, XREAL_1:8;
then (1 + n) + (i + 0) < (1 + n) + (k + 4) by XREAL_1:8;
hence x in Segm (((1 + n) + k) + 4) by A19, NAT_1:44; :: thesis: verum
end;
set PP = { p where p is ((1 + n) + k) + 4 -element XFinSequence of NAT : for i being Nat st i in { ((1 + n) + i) where i is Nat : i in k } holds
S4[p . i,p . i0,p . i2,p . i2] } ;
for i2, i3, i4 being Element of ((1 + n) + k) + 4 holds { p where p is ((1 + n) + k) + 4 -element XFinSequence of NAT : for i being Nat st i in { ((1 + n) + i) where i is Nat : i in k } holds
S4[p . i,p . i2,p . i3,p . i4] } is diophantine Subset of ((((1 + n) + k) + 4) -xtuples_of NAT) from HILB10_5:sch 2(A5, A18);
 then A20: { p where p is ((1 + n) + k) + 4 -element XFinSequence of NAT : for i being Nat st i in { ((1 + n) + i) where i is Nat : i in k } holds
S4[p . i,p . i0,p . i2,p . i2] } is diophantine Subset of ((((1 + n) + k) + 4) -xtuples_of NAT) ;
set QQ = { q where q is ((1 + n) + k) + 4 -element XFinSequence of NAT : S3[q] } ;
A21: { q where q is ((1 + n) + k) + 4 -element XFinSequence of NAT : S3[q] } c= { p where p is ((1 + n) + k) + 4 -element XFinSequence of NAT : for i being Nat st i in { ((1 + n) + i) where i is Nat : i in k } holds
S4[p . i,p . i0,p . i2,p . i2] }
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { q where q is ((1 + n) + k) + 4 -element XFinSequence of NAT : S3[q] } or x in { p where p is ((1 + n) + k) + 4 -element XFinSequence of NAT : for i being Nat st i in { ((1 + n) + i) where i is Nat : i in k } holds
S4[p . i,p . i0,p . i2,p . i2] } )
assume x in { q where q is ((1 + n) + k) + 4 -element XFinSequence of NAT : S3[q] } ; :: thesis: x in { p where p is ((1 + n) + k) + 4 -element XFinSequence of NAT : for i being Nat st i in { ((1 + n) + i) where i is Nat : i in k } holds
S4[p . i,p . i0,p . i2,p . i2] }
then consider p being ((1 + n) + k) + 4 -element XFinSequence of NAT such that
A22: ( x = p & S3[p] ) ;
for i being Nat st i in { ((1 + n) + i) where i is Nat : i in k } holds
S4[p . i,p . i0,p . i2,p . i2]
proof
let i be Nat; :: thesis: ( i in { ((1 + n) + i) where i is Nat : i in k } implies S4[p . i,p . i0,p . i2,p . i2] )
assume i in { ((1 + n) + i) where i is Nat : i in k } ; :: thesis: S4[p . i,p . i0,p . i2,p . i2]
then ex j being Nat st
( i = (1 + n) + j & j in k ) ;
hence S4[p . i,p . i0,p . i2,p . i2] by A22; :: thesis: verum
end;
hence x in { p where p is ((1 + n) + k) + 4 -element XFinSequence of NAT : for i being Nat st i in { ((1 + n) + i) where i is Nat : i in k } holds
S4[p . i,p . i0,p . i2,p . i2] } by A22; :: thesis: verum
end;
{ p where p is ((1 + n) + k) + 4 -element XFinSequence of NAT : for i being Nat st i in { ((1 + n) + i) where i is Nat : i in k } holds
S4[p . i,p . i0,p . i2,p . i2] } c= { q where q is ((1 + n) + k) + 4 -element XFinSequence of NAT : S3[q] }
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { p where p is ((1 + n) + k) + 4 -element XFinSequence of NAT : for i being Nat st i in { ((1 + n) + i) where i is Nat : i in k } holds
S4[p . i,p . i0,p . i2,p . i2] } or x in { q where q is ((1 + n) + k) + 4 -element XFinSequence of NAT : S3[q] } )
assume x in { p where p is ((1 + n) + k) + 4 -element XFinSequence of NAT : for i being Nat st i in { ((1 + n) + i) where i is Nat : i in k } holds
S4[p . i,p . i0,p . i2,p . i2] } ; :: thesis: x in { q where q is ((1 + n) + k) + 4 -element XFinSequence of NAT : S3[q] }
then consider p being ((1 + n) + k) + 4 -element XFinSequence of NAT such that
A23: ( x = p & ( for i being Nat st i in { ((1 + n) + i) where i is Nat : i in k } holds
S4[p . i,p . i0,p . i2,p . i2] ) ) ;
S3[p]
proof
let i be Nat; :: thesis: ( i in k implies ( p . ((1 + n) + i) > p . i0 & Product (((p . ((1 + n) + i)) + 1) + (- (idseq (p . i0)))), 0 are_congruent_mod p . i2 ) )
assume A24: i in k ; :: thesis: ( p . ((1 + n) + i) > p . i0 & Product (((p . ((1 + n) + i)) + 1) + (- (idseq (p . i0)))), 0 are_congruent_mod p . i2 )
(1 + n) + i in { ((1 + n) + i) where i is Nat : i in k } by A24;
hence ( p . ((1 + n) + i) > p . i0 & Product (((p . ((1 + n) + i)) + 1) + (- (idseq (p . i0)))), 0 are_congruent_mod p . i2 ) by A23; :: thesis: verum
end;
hence x in { q where q is ((1 + n) + k) + 4 -element XFinSequence of NAT : S3[q] } by A23; :: thesis: verum
end;
hence { q where q is ((1 + n) + k) + 4 -element XFinSequence of NAT : S3[q] } is diophantine Subset of ((((1 + n) + k) + 4) -xtuples_of NAT) by A20, XBOOLE_0:def 10, A21; :: thesis: verum
end;
defpred S4[ XFinSequence of NAT ] means 1 * ($1 . i0) > (1 * ($1 . ZERO)) + 0;
A25: { q where q is ((1 + n) + k) + 4 -element XFinSequence of NAT : S4[q] } is diophantine Subset of ((((1 + n) + k) + 4) -xtuples_of NAT) by HILB10_3:7;
defpred S5[ XFinSequence of NAT ] means 1 + ((($1 . i3) + 1) * (($1 . i1) !)) = $1 . i2;
A26: { q where q is ((1 + n) + k) + 4 -element XFinSequence of NAT : S5[q] } is diophantine Subset of ((((1 + n) + k) + 4) -xtuples_of NAT) by HILB10_4:33;
defpred S6[ XFinSequence of NAT ] means $1 . i2 = Product (1 + ((($1 . i1) !) * (idseq (1 + ($1 . ZERO)))));
A27: { q where q is ((1 + n) + k) + 4 -element XFinSequence of NAT : S6[q] } is diophantine Subset of ((((1 + n) + k) + 4) -xtuples_of NAT) by HILB10_4:36;
reconsider R = p as INT -valued Polynomial of (1 + ((1 + n) + k)),F_Real ;
defpred S7[ XFinSequence of NAT ] means for Y being 1 + ((1 + n) + k) -element XFinSequence of NAT st Y = <%($1 . i3)%> ^ ($1 | ((1 + n) + k)) holds
eval (R,(@ Y)), 0 are_congruent_mod $1 . i2;
((1 + n) + k) + 0 < ((1 + n) + k) + 3 by XREAL_1:8;
then ( ((1 + n) + k) + 1 <= ((1 + n) + k) + 4 & (1 + n) + k in Segm i3 ) by XREAL_1:8, NAT_1:44;
then A28: { q where q is ((1 + n) + k) + 4 -element XFinSequence of NAT : S7[q] } is diophantine Subset of ((((1 + n) + k) + 4) -xtuples_of NAT) by Th15;
defpred S8[ XFinSequence of NAT ] means ( S1[$1] & S2[$1] );
A29: { q where q is ((1 + n) + k) + 4 -element XFinSequence of NAT : S8[q] } is diophantine Subset of ((((1 + n) + k) + 4) -xtuples_of NAT) from HILB10_3:sch 3(A2, A3);
 defpred S9[ XFinSequence of NAT ] means ( S8[$1] & S3[$1] );
A30: { q where q is ((1 + n) + k) + 4 -element XFinSequence of NAT : S9[q] } is diophantine Subset of ((((1 + n) + k) + 4) -xtuples_of NAT) from HILB10_3:sch 3(A29, A4);
 defpred S10[ XFinSequence of NAT ] means ( S9[$1] & S4[$1] );
A31: { q where q is ((1 + n) + k) + 4 -element XFinSequence of NAT : S10[q] } is diophantine Subset of ((((1 + n) + k) + 4) -xtuples_of NAT) from HILB10_3:sch 3(A30, A25);
 defpred S11[ XFinSequence of NAT ] means ( S10[$1] & S5[$1] );
A32: { q where q is ((1 + n) + k) + 4 -element XFinSequence of NAT : S11[q] } is diophantine Subset of ((((1 + n) + k) + 4) -xtuples_of NAT) from HILB10_3:sch 3(A31, A26);
 defpred S12[ XFinSequence of NAT ] means ( S11[$1] & S6[$1] );
A33: { q where q is ((1 + n) + k) + 4 -element XFinSequence of NAT : S12[q] } is diophantine Subset of ((((1 + n) + k) + 4) -xtuples_of NAT) from HILB10_3:sch 3(A32, A27);
 defpred S13[ XFinSequence of NAT ] means ( S12[$1] & S7[$1] );
set X3 = { q where q is ((1 + n) + k) + 4 -element XFinSequence of NAT : S13[q] } ;
A34: { q where q is ((1 + n) + k) + 4 -element XFinSequence of NAT : S13[q] } is diophantine Subset of ((((1 + n) + k) + 4) -xtuples_of NAT) from HILB10_3:sch 3(A33, A28);
 set X2 = { (X | (n + 1)) where X is ((1 + n) + k) + 4 -element XFinSequence of NAT : X in { q where q is ((1 + n) + k) + 4 -element XFinSequence of NAT : S13[q] } } ;
n + 1 <= (1 + n) + (k + 4) by NAT_1:11;
then A35: { (X | (n + 1)) where X is ((1 + n) + k) + 4 -element XFinSequence of NAT : X in { q where q is ((1 + n) + k) + 4 -element XFinSequence of NAT : S13[q] } } is diophantine Subset of ((n + 1) -xtuples_of NAT) by A34, HILB10_3:5;
defpred S14[ XFinSequence of NAT ] means for z being Element of NAT st z <= $1 . 0 holds
ex y being k -element XFinSequence of NAT st
for X1 being n -element XFinSequence of NAT st X1 = $1 /^ 1 holds
eval (p,(@ ((<%z,($1 . 0)%> ^ X1) ^ y))) = 0 ;
set X1 = { X where X is n + 1 -element XFinSequence of NAT : S14[X] } ;
for s being object holds
( s in { X where X is n + 1 -element XFinSequence of NAT : S14[X] } iff s in { (X | (n + 1)) where X is ((1 + n) + k) + 4 -element XFinSequence of NAT : X in { q where q is ((1 + n) + k) + 4 -element XFinSequence of NAT : S13[q] } } )
proof
let s be object ; :: thesis: ( s in { X where X is n + 1 -element XFinSequence of NAT : S14[X] } iff s in { (X | (n + 1)) where X is ((1 + n) + k) + 4 -element XFinSequence of NAT : X in { q where q is ((1 + n) + k) + 4 -element XFinSequence of NAT : S13[q] } } )
thus ( s in { X where X is n + 1 -element XFinSequence of NAT : S14[X] } implies s in { (X | (n + 1)) where X is ((1 + n) + k) + 4 -element XFinSequence of NAT : X in { q where q is ((1 + n) + k) + 4 -element XFinSequence of NAT : S13[q] } } ) :: thesis: ( s in { (X | (n + 1)) where X is ((1 + n) + k) + 4 -element XFinSequence of NAT : X in { q where q is ((1 + n) + k) + 4 -element XFinSequence of NAT : S13[q] } } implies s in { X where X is n + 1 -element XFinSequence of NAT : S14[X] } )
proof
assume s in { X where X is n + 1 -element XFinSequence of NAT : S14[X] } ; :: thesis: s in { (X | (n + 1)) where X is ((1 + n) + k) + 4 -element XFinSequence of NAT : X in { q where q is ((1 + n) + k) + 4 -element XFinSequence of NAT : S13[q] } }
then consider h being n + 1 -element XFinSequence of NAT such that
A36: ( s = h & S14[h] ) ;
set X = h /^ 1;
( len h = n + 1 & n + 1 >= 1 ) by NAT_1:11, CARD_1:def 7;
then A37: len (h /^ 1) = (n + 1) -' 1 by AFINSQ_2:def 2;
then A38: len (h /^ 1) = n by NAT_D:34;
reconsider X = h /^ 1 as n -element XFinSequence of NAT by A37, NAT_D:34, CARD_1:def 7;
set x = h . 0;
for z being Element of NAT st z <= h . 0 holds
ex y being k -element XFinSequence of NAT st eval (p,(@ ((<%z,(h . 0)%> ^ X) ^ y))) = 0
proof
let z be Element of NAT ; :: thesis: ( z <= h . 0 implies ex y being k -element XFinSequence of NAT st eval (p,(@ ((<%z,(h . 0)%> ^ X) ^ y))) = 0 )
assume A39: z <= h . 0 ; :: thesis: ex y being k -element XFinSequence of NAT st eval (p,(@ ((<%z,(h . 0)%> ^ X) ^ y))) = 0
consider y being k -element XFinSequence of NAT such that
A40: for X1 being n -element XFinSequence of NAT st X1 = h /^ 1 holds
eval (p,(@ ((<%z,(h . 0)%> ^ X1) ^ y))) = 0 by A39, A36;
eval (p,(@ ((<%z,(h . 0)%> ^ X) ^ y))) = 0 by A40;
hence ex y being k -element XFinSequence of NAT st eval (p,(@ ((<%z,(h . 0)%> ^ X) ^ y))) = 0 ; :: thesis: verum
end;
then consider Y being k -element XFinSequence of NAT , Z, e, K being Element of NAT such that
A41: ( K > h . 0 & K >= (sum_of_coefficients |.p.|) * ((((((h . 0) ^2) + 1) * (Product (1 + X))) * e) |^ (degree p)) ) and
A42: for i being Nat st i in k holds
Y . i > e and
A43: e > h . 0 and
A44: 1 + ((Z + 1) * (K !)) = Product (1 + ((K !) * (idseq ((h . 0) + 1)))) and
A45: eval (p,(@ ((<%Z,(h . 0)%> ^ X) ^ Y))), 0 are_congruent_mod 1 + ((Z + 1) * (K !)) and
A46: for i being Nat st i in k holds
Product (((Y . i) + 1) + (- (idseq e))), 0 are_congruent_mod 1 + ((Z + 1) * (K !)) by Th16;
set xXY = (<%(h . 0)%> ^ X) ^ Y;
set E = ((<%e%> ^ <%K%>) ^ <%(1 + ((Z + 1) * (K !)))%>) ^ <%Z%>;
set H = ((<%(h . 0)%> ^ X) ^ Y) ^ (((<%e%> ^ <%K%>) ^ <%(1 + ((Z + 1) * (K !)))%>) ^ <%Z%>);
0 in Segm 1 by NAT_1:44;
then A47: ( 0 in dom <%(h . 0)%> & len <%(h . 0)%> = 1 & dom <%(h . 0)%> c= dom (<%(h . 0)%> ^ X) ) by AFINSQ_1:21, AFINSQ_1:33;
then ( 0 in dom (<%(h . 0)%> ^ X) & dom (<%(h . 0)%> ^ X) c= dom ((<%(h . 0)%> ^ X) ^ Y) ) by AFINSQ_1:21;
then A48: (((<%(h . 0)%> ^ X) ^ Y) ^ (((<%e%> ^ <%K%>) ^ <%(1 + ((Z + 1) * (K !)))%>) ^ <%Z%>)) . 0 = ((<%(h . 0)%> ^ X) ^ Y) . 0 by AFINSQ_1:def 3
.= (<%(h . 0)%> ^ X) . 0 by AFINSQ_1:def 3, A47
.= <%(h . 0)%> . 0 by AFINSQ_1:def 3, A47 ;
((<%(h . 0)%> ^ X) ^ Y) ^ (((<%e%> ^ <%K%>) ^ <%(1 + ((Z + 1) * (K !)))%>) ^ <%Z%>) = (<%(h . 0)%> ^ (X ^ Y)) ^ (((<%e%> ^ <%K%>) ^ <%(1 + ((Z + 1) * (K !)))%>) ^ <%Z%>) by AFINSQ_1:27
.= <%(h . 0)%> ^ ((X ^ Y) ^ (((<%e%> ^ <%K%>) ^ <%(1 + ((Z + 1) * (K !)))%>) ^ <%Z%>)) by AFINSQ_1:27 ;
then A49: (((<%(h . 0)%> ^ X) ^ Y) ^ (((<%e%> ^ <%K%>) ^ <%(1 + ((Z + 1) * (K !)))%>) ^ <%Z%>)) /^ 1 = (X ^ Y) ^ (((<%e%> ^ <%K%>) ^ <%(1 + ((Z + 1) * (K !)))%>) ^ <%Z%>) by A47, AFINSQ_2:12
.= X ^ (Y ^ (((<%e%> ^ <%K%>) ^ <%(1 + ((Z + 1) * (K !)))%>) ^ <%Z%>)) by AFINSQ_1:27 ;
A50: len ((<%(h . 0)%> ^ X) ^ Y) = (1 + n) + k by CARD_1:def 7;
then A51: (((<%(h . 0)%> ^ X) ^ Y) ^ (((<%e%> ^ <%K%>) ^ <%(1 + ((Z + 1) * (K !)))%>) ^ <%Z%>)) | ((1 + n) + k) = (<%(h . 0)%> ^ X) ^ Y by AFINSQ_1:57;
A52: len (((<%e%> ^ <%K%>) ^ <%(1 + ((Z + 1) * (K !)))%>) ^ <%Z%>) = 4 by CARD_1:def 7;
0 in dom (((<%e%> ^ <%K%>) ^ <%(1 + ((Z + 1) * (K !)))%>) ^ <%Z%>) by AFINSQ_1:66;
then A53: (((<%(h . 0)%> ^ X) ^ Y) ^ (((<%e%> ^ <%K%>) ^ <%(1 + ((Z + 1) * (K !)))%>) ^ <%Z%>)) . (((1 + n) + k) + 0) = (((<%e%> ^ <%K%>) ^ <%(1 + ((Z + 1) * (K !)))%>) ^ <%Z%>) . 0 by A50, AFINSQ_1:def 3
.= e by AFINSQ_1:45 ;
1 in dom (((<%e%> ^ <%K%>) ^ <%(1 + ((Z + 1) * (K !)))%>) ^ <%Z%>) by A52, AFINSQ_1:66;
then A54: (((<%(h . 0)%> ^ X) ^ Y) ^ (((<%e%> ^ <%K%>) ^ <%(1 + ((Z + 1) * (K !)))%>) ^ <%Z%>)) . (((1 + n) + k) + 1) = (((<%e%> ^ <%K%>) ^ <%(1 + ((Z + 1) * (K !)))%>) ^ <%Z%>) . 1 by A50, AFINSQ_1:def 3
.= K by AFINSQ_1:45 ;
2 in dom (((<%e%> ^ <%K%>) ^ <%(1 + ((Z + 1) * (K !)))%>) ^ <%Z%>) by A52, AFINSQ_1:66;
then A55: (((<%(h . 0)%> ^ X) ^ Y) ^ (((<%e%> ^ <%K%>) ^ <%(1 + ((Z + 1) * (K !)))%>) ^ <%Z%>)) . (((1 + n) + k) + 2) = (((<%e%> ^ <%K%>) ^ <%(1 + ((Z + 1) * (K !)))%>) ^ <%Z%>) . 2 by A50, AFINSQ_1:def 3
.= 1 + ((Z + 1) * (K !)) by AFINSQ_1:45 ;
3 in dom (((<%e%> ^ <%K%>) ^ <%(1 + ((Z + 1) * (K !)))%>) ^ <%Z%>) by A52, AFINSQ_1:66;
then A56: (((<%(h . 0)%> ^ X) ^ Y) ^ (((<%e%> ^ <%K%>) ^ <%(1 + ((Z + 1) * (K !)))%>) ^ <%Z%>)) . (((1 + n) + k) + 3) = (((<%e%> ^ <%K%>) ^ <%(1 + ((Z + 1) * (K !)))%>) ^ <%Z%>) . 3 by A50, AFINSQ_1:def 3
.= Z by AFINSQ_1:45 ;
A57: for i being Nat st i in k holds
(((<%(h . 0)%> ^ X) ^ Y) ^ (((<%e%> ^ <%K%>) ^ <%(1 + ((Z + 1) * (K !)))%>) ^ <%Z%>)) . ((1 + n) + i) = Y . i
proof
let i be Nat; :: thesis: ( i in k implies (((<%(h . 0)%> ^ X) ^ Y) ^ (((<%e%> ^ <%K%>) ^ <%(1 + ((Z + 1) * (K !)))%>) ^ <%Z%>)) . ((1 + n) + i) = Y . i )
assume A58: i in k ; :: thesis: (((<%(h . 0)%> ^ X) ^ Y) ^ (((<%e%> ^ <%K%>) ^ <%(1 + ((Z + 1) * (K !)))%>) ^ <%Z%>)) . ((1 + n) + i) = Y . i
A59: ( len Y = k & len (<%(h . 0)%> ^ X) = 1 + n ) by CARD_1:def 7;
then (1 + n) + i in dom ((<%(h . 0)%> ^ X) ^ Y) by AFINSQ_1:23, A58;
hence (((<%(h . 0)%> ^ X) ^ Y) ^ (((<%e%> ^ <%K%>) ^ <%(1 + ((Z + 1) * (K !)))%>) ^ <%Z%>)) . ((1 + n) + i) = ((<%(h . 0)%> ^ X) ^ Y) . ((1 + n) + i) by AFINSQ_1:def 3
.= Y . i by A59, A58, AFINSQ_1:def 3 ;
:: thesis: verum
end;
A60: for i being Nat st i in k holds
(((<%(h . 0)%> ^ X) ^ Y) ^ (((<%e%> ^ <%K%>) ^ <%(1 + ((Z + 1) * (K !)))%>) ^ <%Z%>)) . ((1 + n) + i) > (((<%(h . 0)%> ^ X) ^ Y) ^ (((<%e%> ^ <%K%>) ^ <%(1 + ((Z + 1) * (K !)))%>) ^ <%Z%>)) . ((1 + n) + k)
proof
let i be Nat; :: thesis: ( i in k implies (((<%(h . 0)%> ^ X) ^ Y) ^ (((<%e%> ^ <%K%>) ^ <%(1 + ((Z + 1) * (K !)))%>) ^ <%Z%>)) . ((1 + n) + i) > (((<%(h . 0)%> ^ X) ^ Y) ^ (((<%e%> ^ <%K%>) ^ <%(1 + ((Z + 1) * (K !)))%>) ^ <%Z%>)) . ((1 + n) + k) )
assume A61: i in k ; :: thesis: (((<%(h . 0)%> ^ X) ^ Y) ^ (((<%e%> ^ <%K%>) ^ <%(1 + ((Z + 1) * (K !)))%>) ^ <%Z%>)) . ((1 + n) + i) > (((<%(h . 0)%> ^ X) ^ Y) ^ (((<%e%> ^ <%K%>) ^ <%(1 + ((Z + 1) * (K !)))%>) ^ <%Z%>)) . ((1 + n) + k)
(((<%(h . 0)%> ^ X) ^ Y) ^ (((<%e%> ^ <%K%>) ^ <%(1 + ((Z + 1) * (K !)))%>) ^ <%Z%>)) . ((1 + n) + i) = Y . i by A61, A57;
hence (((<%(h . 0)%> ^ X) ^ Y) ^ (((<%e%> ^ <%K%>) ^ <%(1 + ((Z + 1) * (K !)))%>) ^ <%Z%>)) . ((1 + n) + i) > (((<%(h . 0)%> ^ X) ^ Y) ^ (((<%e%> ^ <%K%>) ^ <%(1 + ((Z + 1) * (K !)))%>) ^ <%Z%>)) . ((1 + n) + k) by A53, A42, A61; :: thesis: verum
end;
A62: for Y being (2 + n) + k -element XFinSequence of NAT st Y = <%((((<%(h . 0)%> ^ X) ^ Y) ^ (((<%e%> ^ <%K%>) ^ <%(1 + ((Z + 1) * (K !)))%>) ^ <%Z%>)) . (((1 + n) + k) + 3))%> ^ ((((<%(h . 0)%> ^ X) ^ Y) ^ (((<%e%> ^ <%K%>) ^ <%(1 + ((Z + 1) * (K !)))%>) ^ <%Z%>)) | ((1 + n) + k)) holds
eval (p,(@ Y)), 0 are_congruent_mod (((<%(h . 0)%> ^ X) ^ Y) ^ (((<%e%> ^ <%K%>) ^ <%(1 + ((Z + 1) * (K !)))%>) ^ <%Z%>)) . (((1 + n) + k) + 2)
proof
let YY be (2 + n) + k -element XFinSequence of NAT ; :: thesis: ( YY = <%((((<%(h . 0)%> ^ X) ^ Y) ^ (((<%e%> ^ <%K%>) ^ <%(1 + ((Z + 1) * (K !)))%>) ^ <%Z%>)) . (((1 + n) + k) + 3))%> ^ ((((<%(h . 0)%> ^ X) ^ Y) ^ (((<%e%> ^ <%K%>) ^ <%(1 + ((Z + 1) * (K !)))%>) ^ <%Z%>)) | ((1 + n) + k)) implies eval (p,(@ YY)), 0 are_congruent_mod (((<%(h . 0)%> ^ X) ^ Y) ^ (((<%e%> ^ <%K%>) ^ <%(1 + ((Z + 1) * (K !)))%>) ^ <%Z%>)) . (((1 + n) + k) + 2) )
assume A63: YY = <%((((<%(h . 0)%> ^ X) ^ Y) ^ (((<%e%> ^ <%K%>) ^ <%(1 + ((Z + 1) * (K !)))%>) ^ <%Z%>)) . (((1 + n) + k) + 3))%> ^ ((((<%(h . 0)%> ^ X) ^ Y) ^ (((<%e%> ^ <%K%>) ^ <%(1 + ((Z + 1) * (K !)))%>) ^ <%Z%>)) | ((1 + n) + k)) ; :: thesis: eval (p,(@ YY)), 0 are_congruent_mod (((<%(h . 0)%> ^ X) ^ Y) ^ (((<%e%> ^ <%K%>) ^ <%(1 + ((Z + 1) * (K !)))%>) ^ <%Z%>)) . (((1 + n) + k) + 2)
YY = <%Z%> ^ (<%(h . 0)%> ^ (X ^ Y)) by A56, AFINSQ_1:27, A51, A63
.= (<%Z%> ^ <%(h . 0)%>) ^ (X ^ Y) by AFINSQ_1:27
.= (<%Z,(h . 0)%> ^ X) ^ Y by AFINSQ_1:27 ;
hence eval (p,(@ YY)), 0 are_congruent_mod (((<%(h . 0)%> ^ X) ^ Y) ^ (((<%e%> ^ <%K%>) ^ <%(1 + ((Z + 1) * (K !)))%>) ^ <%Z%>)) . (((1 + n) + k) + 2) by A45, A55; :: thesis: verum
end;
A64: for i being Nat st i in k holds
Product ((((((<%(h . 0)%> ^ X) ^ Y) ^ (((<%e%> ^ <%K%>) ^ <%(1 + ((Z + 1) * (K !)))%>) ^ <%Z%>)) . ((1 + n) + i)) + 1) + (- (idseq ((((<%(h . 0)%> ^ X) ^ Y) ^ (((<%e%> ^ <%K%>) ^ <%(1 + ((Z + 1) * (K !)))%>) ^ <%Z%>)) . ((1 + n) + k))))), 0 are_congruent_mod (((<%(h . 0)%> ^ X) ^ Y) ^ (((<%e%> ^ <%K%>) ^ <%(1 + ((Z + 1) * (K !)))%>) ^ <%Z%>)) . (((1 + n) + k) + 2)
proof
let i be Nat; :: thesis: ( i in k implies Product ((((((<%(h . 0)%> ^ X) ^ Y) ^ (((<%e%> ^ <%K%>) ^ <%(1 + ((Z + 1) * (K !)))%>) ^ <%Z%>)) . ((1 + n) + i)) + 1) + (- (idseq ((((<%(h . 0)%> ^ X) ^ Y) ^ (((<%e%> ^ <%K%>) ^ <%(1 + ((Z + 1) * (K !)))%>) ^ <%Z%>)) . ((1 + n) + k))))), 0 are_congruent_mod (((<%(h . 0)%> ^ X) ^ Y) ^ (((<%e%> ^ <%K%>) ^ <%(1 + ((Z + 1) * (K !)))%>) ^ <%Z%>)) . (((1 + n) + k) + 2) )
assume A65: i in k ; :: thesis: Product ((((((<%(h . 0)%> ^ X) ^ Y) ^ (((<%e%> ^ <%K%>) ^ <%(1 + ((Z + 1) * (K !)))%>) ^ <%Z%>)) . ((1 + n) + i)) + 1) + (- (idseq ((((<%(h . 0)%> ^ X) ^ Y) ^ (((<%e%> ^ <%K%>) ^ <%(1 + ((Z + 1) * (K !)))%>) ^ <%Z%>)) . ((1 + n) + k))))), 0 are_congruent_mod (((<%(h . 0)%> ^ X) ^ Y) ^ (((<%e%> ^ <%K%>) ^ <%(1 + ((Z + 1) * (K !)))%>) ^ <%Z%>)) . (((1 + n) + k) + 2)
(((<%(h . 0)%> ^ X) ^ Y) ^ (((<%e%> ^ <%K%>) ^ <%(1 + ((Z + 1) * (K !)))%>) ^ <%Z%>)) . ((1 + n) + i) = Y . i by A65, A57;
hence Product ((((((<%(h . 0)%> ^ X) ^ Y) ^ (((<%e%> ^ <%K%>) ^ <%(1 + ((Z + 1) * (K !)))%>) ^ <%Z%>)) . ((1 + n) + i)) + 1) + (- (idseq ((((<%(h . 0)%> ^ X) ^ Y) ^ (((<%e%> ^ <%K%>) ^ <%(1 + ((Z + 1) * (K !)))%>) ^ <%Z%>)) . ((1 + n) + k))))), 0 are_congruent_mod (((<%(h . 0)%> ^ X) ^ Y) ^ (((<%e%> ^ <%K%>) ^ <%(1 + ((Z + 1) * (K !)))%>) ^ <%Z%>)) . (((1 + n) + k) + 2) by A53, A55, A46, A65; :: thesis: verum
end;
A66: S1[((<%(h . 0)%> ^ X) ^ Y) ^ (((<%e%> ^ <%K%>) ^ <%(1 + ((Z + 1) * (K !)))%>) ^ <%Z%>)] by A48, A54, A41;
A67: S2[((<%(h . 0)%> ^ X) ^ Y) ^ (((<%e%> ^ <%K%>) ^ <%(1 + ((Z + 1) * (K !)))%>) ^ <%Z%>)] by A48, A49, A38, AFINSQ_1:57, A53, A54, A41;
A68: S3[((<%(h . 0)%> ^ X) ^ Y) ^ (((<%e%> ^ <%K%>) ^ <%(1 + ((Z + 1) * (K !)))%>) ^ <%Z%>)] by A60, A64;
((<%(h . 0)%> ^ X) ^ Y) ^ (((<%e%> ^ <%K%>) ^ <%(1 + ((Z + 1) * (K !)))%>) ^ <%Z%>) in { q where q is ((1 + n) + k) + 4 -element XFinSequence of NAT : S13[q] } by A66, A67, A68, A53, A43, A56, A48, A54, A55, A44, A62;
then A69: (((<%(h . 0)%> ^ X) ^ Y) ^ (((<%e%> ^ <%K%>) ^ <%(1 + ((Z + 1) * (K !)))%>) ^ <%Z%>)) | (n + 1) in { (X | (n + 1)) where X is ((1 + n) + k) + 4 -element XFinSequence of NAT : X in { q where q is ((1 + n) + k) + 4 -element XFinSequence of NAT : S13[q] } } ;
( (((<%(h . 0)%> ^ X) ^ Y) ^ (((<%e%> ^ <%K%>) ^ <%(1 + ((Z + 1) * (K !)))%>) ^ <%Z%>)) | (n + 1) = ((<%(h . 0)%> ^ X) ^ Y) | (n + 1) & len (<%(h . 0)%> ^ X) = 1 + n ) by NAT_1:11, A50, AFINSQ_1:58, CARD_1:def 7;
then (((<%(h . 0)%> ^ X) ^ Y) ^ (((<%e%> ^ <%K%>) ^ <%(1 + ((Z + 1) * (K !)))%>) ^ <%Z%>)) | (n + 1) = <%(h . 0)%> ^ X by AFINSQ_1:57;
hence s in { (X | (n + 1)) where X is ((1 + n) + k) + 4 -element XFinSequence of NAT : X in { q where q is ((1 + n) + k) + 4 -element XFinSequence of NAT : S13[q] } } by A36, A69, NUMERAL2:2; :: thesis: verum
end;
assume s in { (X | (n + 1)) where X is ((1 + n) + k) + 4 -element XFinSequence of NAT : X in { q where q is ((1 + n) + k) + 4 -element XFinSequence of NAT : S13[q] } } ; :: thesis: s in { X where X is n + 1 -element XFinSequence of NAT : S14[X] }
then consider x being ((1 + n) + k) + 4 -element XFinSequence of NAT such that
A70: ( s = x | (n + 1) & x in { q where q is ((1 + n) + k) + 4 -element XFinSequence of NAT : S13[q] } ) ;
consider H being ((1 + n) + k) + 4 -element XFinSequence of NAT such that
A71: H = x and
A72: S13[H] by A70;
A73: ( ((1 + n) + k) + 4 >= (1 + n) + k & len H = ((1 + n) + k) + 4 ) by NAT_1:11, CARD_1:def 7;
then A74: len (H | ((1 + n) + k)) = (1 + n) + k by AFINSQ_1:54;
then A75: len ((H | ((1 + n) + k)) /^ (n + 1)) = ((1 + n) + k) -' (n + 1) by AFINSQ_2:def 2;
then A76: len ((H | ((1 + n) + k)) /^ (n + 1)) = k by NAT_D:34;
reconsider Y = (H | ((1 + n) + k)) /^ (n + 1) as k -element XFinSequence of NAT by A75, NAT_D:34, CARD_1:def 7;
reconsider x = H . 0, e = H . ((1 + n) + k), K = H . (((1 + n) + k) + 1), Z = H . (((1 + n) + k) + 3) as Element of NAT ;
A77: len H = (((1 + n) + k) + 3) + 1 by CARD_1:def 7;
then len (H /^ 1) = ((((1 + n) + k) + 3) + 1) -' 1 by AFINSQ_2:def 2;
then A78: len (H /^ 1) = ((1 + n) + k) + 3 by NAT_D:34;
((1 + k) + 3) + n >= n by NAT_1:11;
then len ((H /^ 1) | n) = n by AFINSQ_1:54, A78;
then reconsider X = (H /^ 1) | n as n -element XFinSequence of NAT by CARD_1:def 7;
A79: for i being Nat st i in k holds
Y . i = H . ((1 + n) + i)
proof
let i be Nat; :: thesis: ( i in k implies Y . i = H . ((1 + n) + i) )
assume A80: i in k ; :: thesis: Y . i = H . ((1 + n) + i)
A81: Y . i = (H | ((1 + n) + k)) . ((n + 1) + i) by A80, A76, AFINSQ_2:def 2;
i in Segm k by A80;
then (1 + n) + i < Segm ((1 + n) + k) by XREAL_1:8, NAT_1:44;
hence Y . i = H . ((1 + n) + i) by A81, NAT_1:44, FUNCT_1:49; :: thesis: verum
end;
A82: for i being Nat st i in k holds
Y . i > e
proof
let i be Nat; :: thesis: ( i in k implies Y . i > e )
assume A83: i in k ; :: thesis: Y . i > e
Y . i = H . ((1 + n) + i) by A83, A79;
hence Y . i > e by A83, A72; :: thesis: verum
end;
len <%Z%> = 1 by CARD_1:def 7;
then len (<%Z%> ^ (H | ((1 + n) + k))) = 1 + ((1 + n) + k) by A74, AFINSQ_1:17;
then reconsider ZY = <%Z%> ^ (H | ((1 + n) + k)) as (2 + n) + k -element XFinSequence of NAT by CARD_1:def 7;
Segm (n + 1) c= Segm ((1 + n) + k) by NAT_1:11, NAT_1:39;
then (H | ((1 + n) + k)) | (n + 1) = H | (n + 1) by RELAT_1:74;
then A84: H | ((1 + n) + k) = (H | (n + 1)) ^ Y ;
A85: ( (1 + 1) -' 1 = 1 & (n + 2) -' 2 = n ) by NAT_D:34;
n + 1 <= (n + 1) + (k + 4) by NAT_1:11;
then A86: (H /^ ((1 + 1) -' 1)) | (((n + 1) + 1) -' (1 + 1)) = mid (H,(1 + 1),(n + 1)) by A73, AFINSQ_2:15
.= (H | (n + 1)) /^ ((1 + 1) -' 1) by AFINSQ_2:def 3 ;
A87: H | (n + 1) = ((H | (n + 1)) | 1) ^ ((H /^ 1) | n) by A85, A86;
Segm 1 c= Segm (n + 1) by NAT_1:11, NAT_1:39;
then (H | (n + 1)) | 1 = H | 1 by RELAT_1:74
.= <%(H . 0)%> by NUMERAL2:1 ;
then ZY = <%Z%> ^ (<%x%> ^ (X ^ Y)) by A84, A87, AFINSQ_1:27
.= (<%Z%> ^ <%x%>) ^ (X ^ Y) by AFINSQ_1:27
.= (<%Z,x%> ^ X) ^ Y by AFINSQ_1:27 ;
then A88: eval (p,(@ ((<%Z,x%> ^ X) ^ Y))), 0 are_congruent_mod 1 + ((Z + 1) * (K !)) by A72;
A89: for i being Nat st i in k holds
Product (((Y . i) + 1) + (- (idseq e))), 0 are_congruent_mod 1 + ((Z + 1) * (K !))
proof
let i be Nat; :: thesis: ( i in k implies Product (((Y . i) + 1) + (- (idseq e))), 0 are_congruent_mod 1 + ((Z + 1) * (K !)) )
assume A90: i in k ; :: thesis: Product (((Y . i) + 1) + (- (idseq e))), 0 are_congruent_mod 1 + ((Z + 1) * (K !))
then Y . i = H . ((n + 1) + i) by A79;
hence Product (((Y . i) + 1) + (- (idseq e))), 0 are_congruent_mod 1 + ((Z + 1) * (K !)) by A90, A72; :: thesis: verum
end;
n + 1 <= (n + 1) + (k + 4) by NAT_1:11;
then len (H | (n + 1)) = n + 1 by AFINSQ_1:54, A77;
then reconsider F = H | (n + 1) as n + 1 -element XFinSequence of NAT by CARD_1:def 7;
A91: 0 < len F ;
then A92: F . 0 = H . 0 by FUNCT_1:47, AFINSQ_1:66;
for z being Element of NAT st z <= F . 0 holds
ex y being k -element XFinSequence of NAT st
for X1 being n -element XFinSequence of NAT st X1 = F /^ 1 holds
eval (p,(@ ((<%z,(F . 0)%> ^ X1) ^ y))) = 0
proof
let z be Element of NAT ; :: thesis: ( z <= F . 0 implies ex y being k -element XFinSequence of NAT st
for X1 being n -element XFinSequence of NAT st X1 = F /^ 1 holds
eval (p,(@ ((<%z,(F . 0)%> ^ X1) ^ y))) = 0 )
assume A93: z <= F . 0 ; :: thesis: ex y being k -element XFinSequence of NAT st
for X1 being n -element XFinSequence of NAT st X1 = F /^ 1 holds
eval (p,(@ ((<%z,(F . 0)%> ^ X1) ^ y))) = 0
consider y being k -element XFinSequence of NAT such that
A94: eval (p,(@ ((<%z,x%> ^ X) ^ y))) = 0 by A93, A92, A89, Th16, A72, A82, A88;
take y ; :: thesis: for X1 being n -element XFinSequence of NAT st X1 = F /^ 1 holds
eval (p,(@ ((<%z,(F . 0)%> ^ X1) ^ y))) = 0
let X1 be n -element XFinSequence of NAT ; :: thesis: ( X1 = F /^ 1 implies eval (p,(@ ((<%z,(F . 0)%> ^ X1) ^ y))) = 0 )
assume X1 = F /^ 1 ; :: thesis: eval (p,(@ ((<%z,(F . 0)%> ^ X1) ^ y))) = 0
hence eval (p,(@ ((<%z,(F . 0)%> ^ X1) ^ y))) = 0 by A94, A91, FUNCT_1:47, AFINSQ_1:66, A86, A85; :: thesis: verum
end;
hence s in { X where X is n + 1 -element XFinSequence of NAT : S14[X] } by A71, A70; :: thesis: verum
end;
then A95: { X where X is n + 1 -element XFinSequence of NAT : S14[X] } = { (X | (n + 1)) where X is ((1 + n) + k) + 4 -element XFinSequence of NAT : X in { q where q is ((1 + n) + k) + 4 -element XFinSequence of NAT : S13[q] } } by TARSKI:2;
set Y1 = { (X /^ 1) where X is n + 1 -element XFinSequence of NAT : X in { X where X is n + 1 -element XFinSequence of NAT : S14[X] } } ;
A96: { (X /^ 1) where X is n + 1 -element XFinSequence of NAT : X in { X where X is n + 1 -element XFinSequence of NAT : S14[X] } } is diophantine Subset of (n -xtuples_of NAT) by A95, A35, HILB10_4:27;
for s being object holds
( s in { (X /^ 1) where X is n + 1 -element XFinSequence of NAT : X in { X where X is n + 1 -element XFinSequence of NAT : S14[X] } } iff s in { X where X is n -element XFinSequence of NAT : ex x being Element of NAT st
for z being Element of NAT st z <= x holds
ex y being k -element XFinSequence of NAT st eval (p,(@ ((<%z,x%> ^ X) ^ y))) = 0 } )
proof
let s be object ; :: thesis: ( s in { (X /^ 1) where X is n + 1 -element XFinSequence of NAT : X in { X where X is n + 1 -element XFinSequence of NAT : S14[X] } } iff s in { X where X is n -element XFinSequence of NAT : ex x being Element of NAT st
for z being Element of NAT st z <= x holds
ex y being k -element XFinSequence of NAT st eval (p,(@ ((<%z,x%> ^ X) ^ y))) = 0 } )
thus ( s in { (X /^ 1) where X is n + 1 -element XFinSequence of NAT : X in { X where X is n + 1 -element XFinSequence of NAT : S14[X] } } implies s in { X where X is n -element XFinSequence of NAT : ex x being Element of NAT st
for z being Element of NAT st z <= x holds
ex y being k -element XFinSequence of NAT st eval (p,(@ ((<%z,x%> ^ X) ^ y))) = 0 } ) :: thesis: ( s in { X where X is n -element XFinSequence of NAT : ex x being Element of NAT st
for z being Element of NAT st z <= x holds
ex y being k -element XFinSequence of NAT st eval (p,(@ ((<%z,x%> ^ X) ^ y))) = 0 } implies s in { (X /^ 1) where X is n + 1 -element XFinSequence of NAT : X in { X where X is n + 1 -element XFinSequence of NAT : S14[X] } } )
proof
assume s in { (X /^ 1) where X is n + 1 -element XFinSequence of NAT : X in { X where X is n + 1 -element XFinSequence of NAT : S14[X] } } ; :: thesis: s in { X where X is n -element XFinSequence of NAT : ex x being Element of NAT st
for z being Element of NAT st z <= x holds
ex y being k -element XFinSequence of NAT st eval (p,(@ ((<%z,x%> ^ X) ^ y))) = 0 }
then consider xS being n + 1 -element XFinSequence of NAT such that
A97: ( s = xS /^ 1 & xS in { X where X is n + 1 -element XFinSequence of NAT : S14[X] } ) ;
A98: ex w being n + 1 -element XFinSequence of NAT st
( xS = w & S14[w] ) by A97;
len xS = n + 1 by CARD_1:def 7;
then len (xS /^ 1) = (n + 1) -' 1 by AFINSQ_2:def 2;
then reconsider S = xS /^ 1 as n -element XFinSequence of NAT by NAT_D:34, CARD_1:def 7;
ex x being Element of NAT st
for z being Element of NAT st z <= x holds
ex y being k -element XFinSequence of NAT st eval (p,(@ ((<%z,x%> ^ S) ^ y))) = 0
proof
take x = xS . 0; :: thesis: for z being Element of NAT st z <= x holds
ex y being k -element XFinSequence of NAT st eval (p,(@ ((<%z,x%> ^ S) ^ y))) = 0
let z be Element of NAT ; :: thesis: ( z <= x implies ex y being k -element XFinSequence of NAT st eval (p,(@ ((<%z,x%> ^ S) ^ y))) = 0 )
assume A99: z <= x ; :: thesis: ex y being k -element XFinSequence of NAT st eval (p,(@ ((<%z,x%> ^ S) ^ y))) = 0
consider y being k -element XFinSequence of NAT such that
A100: for X1 being n -element XFinSequence of NAT st X1 = xS /^ 1 holds
eval (p,(@ ((<%z,(xS . 0)%> ^ X1) ^ y))) = 0 by A98, A99;
eval (p,(@ ((<%z,x%> ^ S) ^ y))) = 0 by A100;
hence ex y being k -element XFinSequence of NAT st eval (p,(@ ((<%z,x%> ^ S) ^ y))) = 0 ; :: thesis: verum
end;
hence s in { X where X is n -element XFinSequence of NAT : ex x being Element of NAT st
for z being Element of NAT st z <= x holds
ex y being k -element XFinSequence of NAT st eval (p,(@ ((<%z,x%> ^ X) ^ y))) = 0 } by A97; :: thesis: verum
end;
assume s in { X where X is n -element XFinSequence of NAT : ex x being Element of NAT st
for z being Element of NAT st z <= x holds
ex y being k -element XFinSequence of NAT st eval (p,(@ ((<%z,x%> ^ X) ^ y))) = 0 } ; :: thesis: s in { (X /^ 1) where X is n + 1 -element XFinSequence of NAT : X in { X where X is n + 1 -element XFinSequence of NAT : S14[X] } }
then consider S being n -element XFinSequence of NAT such that
A101: ( s = S & ex x being Element of NAT st
for z being Element of NAT st z <= x holds
ex y being k -element XFinSequence of NAT st eval (p,(@ ((<%z,x%> ^ S) ^ y))) = 0 ) ;
consider x being Element of NAT such that
A102: for z being Element of NAT st z <= x holds
ex y being k -element XFinSequence of NAT st eval (p,(@ ((<%z,x%> ^ S) ^ y))) = 0 by A101;
set xS = <%x%> ^ S;
A103: len <%x%> = 1 by CARD_1:def 7;
then A104: (<%x%> ^ S) /^ 1 = S by AFINSQ_2:12;
S14[<%x%> ^ S]
proof
let z be Element of NAT ; :: thesis: ( z <= (<%x%> ^ S) . 0 implies ex y being k -element XFinSequence of NAT st
for X1 being n -element XFinSequence of NAT st X1 = (<%x%> ^ S) /^ 1 holds
eval (p,(@ ((<%z,((<%x%> ^ S) . 0)%> ^ X1) ^ y))) = 0 )
assume A105: z <= (<%x%> ^ S) . 0 ; :: thesis: ex y being k -element XFinSequence of NAT st
for X1 being n -element XFinSequence of NAT st X1 = (<%x%> ^ S) /^ 1 holds
eval (p,(@ ((<%z,((<%x%> ^ S) . 0)%> ^ X1) ^ y))) = 0
A106: (<%x%> ^ S) . 0 = x by AFINSQ_1:35;
then consider y being k -element XFinSequence of NAT such that
A107: eval (p,(@ ((<%z,x%> ^ S) ^ y))) = 0 by A102, A105;
take y ; :: thesis: for X1 being n -element XFinSequence of NAT st X1 = (<%x%> ^ S) /^ 1 holds
eval (p,(@ ((<%z,((<%x%> ^ S) . 0)%> ^ X1) ^ y))) = 0
thus for X1 being n -element XFinSequence of NAT st X1 = (<%x%> ^ S) /^ 1 holds
eval (p,(@ ((<%z,((<%x%> ^ S) . 0)%> ^ X1) ^ y))) = 0 by AFINSQ_2:12, A103, A106, A107; :: thesis: verum
end;
then <%x%> ^ S in { X where X is n + 1 -element XFinSequence of NAT : S14[X] } ;
hence s in { (X /^ 1) where X is n + 1 -element XFinSequence of NAT : X in { X where X is n + 1 -element XFinSequence of NAT : S14[X] } } by A104, A101; :: thesis: verum
end;
hence { X where X is n -element XFinSequence of NAT : ex x being Element of NAT st
for z being Element of NAT st z <= x holds
ex y being k -element XFinSequence of NAT st eval (p,(@ ((<%z,x%> ^ X) ^ y))) = 0 } is diophantine Subset of (n -xtuples_of NAT) by A96, TARSKI:2; :: thesis: verum