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
( ( for i being Nat st i in k holds
y . i <= x ) & 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
( ( for i being Nat st i in k holds
y . i <= x ) & 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
( ( for i being Nat st i in k holds
y . i <= x ) & 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) + 2 < ((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) ) 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 by HILB10_3:3;
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)))) * ((0 * ($1 . i0)) + 1)) |^ ((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, HILB10_3:5, NAT_1:11;
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 A13, A14; :: 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 A15, HILB10_4:23;
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 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 )
then (1 + n) + i in { ((1 + n) + i) where i is Nat : i in k } ;
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 . i0 = (1 * ($1 . ZERO)) + 1;
A24: { 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:15;
defpred S5[ XFinSequence of NAT ] means 1 + ((($1 . i3) + 1) * (($1 . i1) !)) = $1 . i2;
A25: { 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)))));
A26: { 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 A27: { 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] );
A28: { 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] );
A29: { 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(A28, A4);
 defpred S10[ XFinSequence of NAT ] means ( S9[$1] & S4[$1] );
A30: { 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(A29, A24);
 defpred S11[ XFinSequence of NAT ] means ( S10[$1] & S5[$1] );
A31: { 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(A30, A25);
 defpred S12[ XFinSequence of NAT ] means ( S11[$1] & S6[$1] );
A32: { 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(A31, A26);
 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] } ;
A33: { 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(A32, A27);
 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 A34: { (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 A33, 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
( ( for i being Nat st i in k holds
y . i <= $1 . 0 ) & 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
A35: ( s = h & S14[h] ) ;
set X = h /^ 1;
( len h = n + 1 & n + 1 >= 1 ) by NAT_1:11, CARD_1:def 7;
then A36: len (h /^ 1) = (n + 1) -' 1 by AFINSQ_2:def 2;
then A37: len (h /^ 1) = n by NAT_D:34;
reconsider X = h /^ 1 as n -element XFinSequence of NAT by A36, NAT_D:34, CARD_1:def 7;
set x = h . 0;
set e = (h . 0) + 1;
for z being Element of NAT st z <= h . 0 holds
ex y being k -element XFinSequence of NAT st
( ( for i being Nat st i in k holds
y . i <= h . 0 ) & 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
( ( for i being Nat st i in k holds
y . i <= h . 0 ) & eval (p,(@ ((<%z,(h . 0)%> ^ X) ^ y))) = 0 ) )
assume A38: z <= h . 0 ; :: thesis: ex y being k -element XFinSequence of NAT st
( ( for i being Nat st i in k holds
y . i <= h . 0 ) & eval (p,(@ ((<%z,(h . 0)%> ^ X) ^ y))) = 0 )
consider y being k -element XFinSequence of NAT such that
A39: for X1 being n -element XFinSequence of NAT st X1 = h /^ 1 holds
( ( for i being Nat st i in k holds
y . i <= h . 0 ) & eval (p,(@ ((<%z,(h . 0)%> ^ X1) ^ y))) = 0 ) by A38, A35;
X = h /^ 1 ;
then ( ( for i being Nat st i in k holds
y . i <= h . 0 ) & eval (p,(@ ((<%z,(h . 0)%> ^ X) ^ y))) = 0 ) by A39;
hence ex y being k -element XFinSequence of NAT st
( ( for i being Nat st i in k holds
y . i <= h . 0 ) & eval (p,(@ ((<%z,(h . 0)%> ^ X) ^ y))) = 0 ) ; :: thesis: verum
end;
then consider Y being k -element XFinSequence of NAT , Z, K being Element of NAT such that
A40: ( K > h . 0 & K >= (sum_of_coefficients |.p.|) * (((((h . 0) ^2) + 1) * (Product (1 + X))) |^ (degree p)) ) and
A41: for i being Nat st i in k holds
Y . i > (h . 0) + 1 and
A42: 1 + ((Z + 1) * (K !)) = Product (1 + ((K !) * (idseq ((h . 0) + 1)))) and
A43: eval (p,(@ ((<%Z,(h . 0)%> ^ X) ^ Y))), 0 are_congruent_mod 1 + ((Z + 1) * (K !)) and
A44: for i being Nat st i in k holds
Product (((Y . i) + 1) + (- (idseq ((h . 0) + 1)))), 0 are_congruent_mod 1 + ((Z + 1) * (K !)) by Th17;
set xXY = (<%(h . 0)%> ^ X) ^ Y;
set E = ((<%((h . 0) + 1)%> ^ <%K%>) ^ <%(1 + ((Z + 1) * (K !)))%>) ^ <%Z%>;
set H = ((<%(h . 0)%> ^ X) ^ Y) ^ (((<%((h . 0) + 1)%> ^ <%K%>) ^ <%(1 + ((Z + 1) * (K !)))%>) ^ <%Z%>);
0 in Segm 1 by NAT_1:44;
then A45: ( 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 A46: (((<%(h . 0)%> ^ X) ^ Y) ^ (((<%((h . 0) + 1)%> ^ <%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, A45
.= <%(h . 0)%> . 0 by AFINSQ_1:def 3, A45 ;
((<%(h . 0)%> ^ X) ^ Y) ^ (((<%((h . 0) + 1)%> ^ <%K%>) ^ <%(1 + ((Z + 1) * (K !)))%>) ^ <%Z%>) = (<%(h . 0)%> ^ (X ^ Y)) ^ (((<%((h . 0) + 1)%> ^ <%K%>) ^ <%(1 + ((Z + 1) * (K !)))%>) ^ <%Z%>) by AFINSQ_1:27
.= <%(h . 0)%> ^ ((X ^ Y) ^ (((<%((h . 0) + 1)%> ^ <%K%>) ^ <%(1 + ((Z + 1) * (K !)))%>) ^ <%Z%>)) by AFINSQ_1:27 ;
then A47: (((<%(h . 0)%> ^ X) ^ Y) ^ (((<%((h . 0) + 1)%> ^ <%K%>) ^ <%(1 + ((Z + 1) * (K !)))%>) ^ <%Z%>)) /^ 1 = (X ^ Y) ^ (((<%((h . 0) + 1)%> ^ <%K%>) ^ <%(1 + ((Z + 1) * (K !)))%>) ^ <%Z%>) by A45, AFINSQ_2:12
.= X ^ (Y ^ (((<%((h . 0) + 1)%> ^ <%K%>) ^ <%(1 + ((Z + 1) * (K !)))%>) ^ <%Z%>)) by AFINSQ_1:27 ;
A48: len ((<%(h . 0)%> ^ X) ^ Y) = (1 + n) + k by CARD_1:def 7;
A49: len (((<%((h . 0) + 1)%> ^ <%K%>) ^ <%(1 + ((Z + 1) * (K !)))%>) ^ <%Z%>) = 4 by CARD_1:def 7;
0 in dom (((<%((h . 0) + 1)%> ^ <%K%>) ^ <%(1 + ((Z + 1) * (K !)))%>) ^ <%Z%>) by AFINSQ_1:66;
then A50: (((<%(h . 0)%> ^ X) ^ Y) ^ (((<%((h . 0) + 1)%> ^ <%K%>) ^ <%(1 + ((Z + 1) * (K !)))%>) ^ <%Z%>)) . (((1 + n) + k) + 0) = (((<%((h . 0) + 1)%> ^ <%K%>) ^ <%(1 + ((Z + 1) * (K !)))%>) ^ <%Z%>) . 0 by A48, AFINSQ_1:def 3
.= (h . 0) + 1 by AFINSQ_1:45 ;
1 in dom (((<%((h . 0) + 1)%> ^ <%K%>) ^ <%(1 + ((Z + 1) * (K !)))%>) ^ <%Z%>) by A49, AFINSQ_1:66;
then A51: (((<%(h . 0)%> ^ X) ^ Y) ^ (((<%((h . 0) + 1)%> ^ <%K%>) ^ <%(1 + ((Z + 1) * (K !)))%>) ^ <%Z%>)) . (((1 + n) + k) + 1) = (((<%((h . 0) + 1)%> ^ <%K%>) ^ <%(1 + ((Z + 1) * (K !)))%>) ^ <%Z%>) . 1 by A48, AFINSQ_1:def 3
.= K by AFINSQ_1:45 ;
2 in dom (((<%((h . 0) + 1)%> ^ <%K%>) ^ <%(1 + ((Z + 1) * (K !)))%>) ^ <%Z%>) by A49, AFINSQ_1:66;
then A52: (((<%(h . 0)%> ^ X) ^ Y) ^ (((<%((h . 0) + 1)%> ^ <%K%>) ^ <%(1 + ((Z + 1) * (K !)))%>) ^ <%Z%>)) . (((1 + n) + k) + 2) = (((<%((h . 0) + 1)%> ^ <%K%>) ^ <%(1 + ((Z + 1) * (K !)))%>) ^ <%Z%>) . 2 by A48, AFINSQ_1:def 3
.= 1 + ((Z + 1) * (K !)) by AFINSQ_1:45 ;
3 in dom (((<%((h . 0) + 1)%> ^ <%K%>) ^ <%(1 + ((Z + 1) * (K !)))%>) ^ <%Z%>) by A49, AFINSQ_1:66;
then A53: (((<%(h . 0)%> ^ X) ^ Y) ^ (((<%((h . 0) + 1)%> ^ <%K%>) ^ <%(1 + ((Z + 1) * (K !)))%>) ^ <%Z%>)) . (((1 + n) + k) + 3) = (((<%((h . 0) + 1)%> ^ <%K%>) ^ <%(1 + ((Z + 1) * (K !)))%>) ^ <%Z%>) . 3 by A48, AFINSQ_1:def 3
.= Z by AFINSQ_1:45 ;
A54: for i being Nat st i in k holds
(((<%(h . 0)%> ^ X) ^ Y) ^ (((<%((h . 0) + 1)%> ^ <%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) ^ (((<%((h . 0) + 1)%> ^ <%K%>) ^ <%(1 + ((Z + 1) * (K !)))%>) ^ <%Z%>)) . ((1 + n) + i) = Y . i )
assume A55: i in k ; :: thesis: (((<%(h . 0)%> ^ X) ^ Y) ^ (((<%((h . 0) + 1)%> ^ <%K%>) ^ <%(1 + ((Z + 1) * (K !)))%>) ^ <%Z%>)) . ((1 + n) + i) = Y . i
A56: ( 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, A55;
hence (((<%(h . 0)%> ^ X) ^ Y) ^ (((<%((h . 0) + 1)%> ^ <%K%>) ^ <%(1 + ((Z + 1) * (K !)))%>) ^ <%Z%>)) . ((1 + n) + i) = ((<%(h . 0)%> ^ X) ^ Y) . ((1 + n) + i) by AFINSQ_1:def 3
.= Y . i by A56, A55, AFINSQ_1:def 3 ;
:: thesis: verum
end;
A57: for i being Nat st i in k holds
(((<%(h . 0)%> ^ X) ^ Y) ^ (((<%((h . 0) + 1)%> ^ <%K%>) ^ <%(1 + ((Z + 1) * (K !)))%>) ^ <%Z%>)) . ((1 + n) + i) > (((<%(h . 0)%> ^ X) ^ Y) ^ (((<%((h . 0) + 1)%> ^ <%K%>) ^ <%(1 + ((Z + 1) * (K !)))%>) ^ <%Z%>)) . ((1 + n) + k)
proof
let i be Nat; :: thesis: ( i in k implies (((<%(h . 0)%> ^ X) ^ Y) ^ (((<%((h . 0) + 1)%> ^ <%K%>) ^ <%(1 + ((Z + 1) * (K !)))%>) ^ <%Z%>)) . ((1 + n) + i) > (((<%(h . 0)%> ^ X) ^ Y) ^ (((<%((h . 0) + 1)%> ^ <%K%>) ^ <%(1 + ((Z + 1) * (K !)))%>) ^ <%Z%>)) . ((1 + n) + k) )
assume A58: i in k ; :: thesis: (((<%(h . 0)%> ^ X) ^ Y) ^ (((<%((h . 0) + 1)%> ^ <%K%>) ^ <%(1 + ((Z + 1) * (K !)))%>) ^ <%Z%>)) . ((1 + n) + i) > (((<%(h . 0)%> ^ X) ^ Y) ^ (((<%((h . 0) + 1)%> ^ <%K%>) ^ <%(1 + ((Z + 1) * (K !)))%>) ^ <%Z%>)) . ((1 + n) + k)
(((<%(h . 0)%> ^ X) ^ Y) ^ (((<%((h . 0) + 1)%> ^ <%K%>) ^ <%(1 + ((Z + 1) * (K !)))%>) ^ <%Z%>)) . ((1 + n) + i) = Y . i by A58, A54;
hence (((<%(h . 0)%> ^ X) ^ Y) ^ (((<%((h . 0) + 1)%> ^ <%K%>) ^ <%(1 + ((Z + 1) * (K !)))%>) ^ <%Z%>)) . ((1 + n) + i) > (((<%(h . 0)%> ^ X) ^ Y) ^ (((<%((h . 0) + 1)%> ^ <%K%>) ^ <%(1 + ((Z + 1) * (K !)))%>) ^ <%Z%>)) . ((1 + n) + k) by A50, A41, A58; :: thesis: verum
end;
A59: for Y being (2 + n) + k -element XFinSequence of NAT st Y = <%((((<%(h . 0)%> ^ X) ^ Y) ^ (((<%((h . 0) + 1)%> ^ <%K%>) ^ <%(1 + ((Z + 1) * (K !)))%>) ^ <%Z%>)) . (((1 + n) + k) + 3))%> ^ ((((<%(h . 0)%> ^ X) ^ Y) ^ (((<%((h . 0) + 1)%> ^ <%K%>) ^ <%(1 + ((Z + 1) * (K !)))%>) ^ <%Z%>)) | ((1 + n) + k)) holds
eval (p,(@ Y)), 0 are_congruent_mod (((<%(h . 0)%> ^ X) ^ Y) ^ (((<%((h . 0) + 1)%> ^ <%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) ^ (((<%((h . 0) + 1)%> ^ <%K%>) ^ <%(1 + ((Z + 1) * (K !)))%>) ^ <%Z%>)) . (((1 + n) + k) + 3))%> ^ ((((<%(h . 0)%> ^ X) ^ Y) ^ (((<%((h . 0) + 1)%> ^ <%K%>) ^ <%(1 + ((Z + 1) * (K !)))%>) ^ <%Z%>)) | ((1 + n) + k)) implies eval (p,(@ YY)), 0 are_congruent_mod (((<%(h . 0)%> ^ X) ^ Y) ^ (((<%((h . 0) + 1)%> ^ <%K%>) ^ <%(1 + ((Z + 1) * (K !)))%>) ^ <%Z%>)) . (((1 + n) + k) + 2) )
assume A60: YY = <%((((<%(h . 0)%> ^ X) ^ Y) ^ (((<%((h . 0) + 1)%> ^ <%K%>) ^ <%(1 + ((Z + 1) * (K !)))%>) ^ <%Z%>)) . (((1 + n) + k) + 3))%> ^ ((((<%(h . 0)%> ^ X) ^ Y) ^ (((<%((h . 0) + 1)%> ^ <%K%>) ^ <%(1 + ((Z + 1) * (K !)))%>) ^ <%Z%>)) | ((1 + n) + k)) ; :: thesis: eval (p,(@ YY)), 0 are_congruent_mod (((<%(h . 0)%> ^ X) ^ Y) ^ (((<%((h . 0) + 1)%> ^ <%K%>) ^ <%(1 + ((Z + 1) * (K !)))%>) ^ <%Z%>)) . (((1 + n) + k) + 2)
YY = <%((((<%(h . 0)%> ^ X) ^ Y) ^ (((<%((h . 0) + 1)%> ^ <%K%>) ^ <%(1 + ((Z + 1) * (K !)))%>) ^ <%Z%>)) . (((1 + n) + k) + 3))%> ^ ((<%(h . 0)%> ^ X) ^ Y) by A48, AFINSQ_1:57, A60
.= <%Z%> ^ (<%(h . 0)%> ^ (X ^ Y)) by A53, AFINSQ_1:27
.= (<%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) ^ (((<%((h . 0) + 1)%> ^ <%K%>) ^ <%(1 + ((Z + 1) * (K !)))%>) ^ <%Z%>)) . (((1 + n) + k) + 2) by A52, A43; :: thesis: verum
end;
A61: for i being Nat st i in k holds
Product ((((((<%(h . 0)%> ^ X) ^ Y) ^ (((<%((h . 0) + 1)%> ^ <%K%>) ^ <%(1 + ((Z + 1) * (K !)))%>) ^ <%Z%>)) . ((1 + n) + i)) + 1) + (- (idseq ((((<%(h . 0)%> ^ X) ^ Y) ^ (((<%((h . 0) + 1)%> ^ <%K%>) ^ <%(1 + ((Z + 1) * (K !)))%>) ^ <%Z%>)) . ((1 + n) + k))))), 0 are_congruent_mod (((<%(h . 0)%> ^ X) ^ Y) ^ (((<%((h . 0) + 1)%> ^ <%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) ^ (((<%((h . 0) + 1)%> ^ <%K%>) ^ <%(1 + ((Z + 1) * (K !)))%>) ^ <%Z%>)) . ((1 + n) + i)) + 1) + (- (idseq ((((<%(h . 0)%> ^ X) ^ Y) ^ (((<%((h . 0) + 1)%> ^ <%K%>) ^ <%(1 + ((Z + 1) * (K !)))%>) ^ <%Z%>)) . ((1 + n) + k))))), 0 are_congruent_mod (((<%(h . 0)%> ^ X) ^ Y) ^ (((<%((h . 0) + 1)%> ^ <%K%>) ^ <%(1 + ((Z + 1) * (K !)))%>) ^ <%Z%>)) . (((1 + n) + k) + 2) )
assume A62: i in k ; :: thesis: Product ((((((<%(h . 0)%> ^ X) ^ Y) ^ (((<%((h . 0) + 1)%> ^ <%K%>) ^ <%(1 + ((Z + 1) * (K !)))%>) ^ <%Z%>)) . ((1 + n) + i)) + 1) + (- (idseq ((((<%(h . 0)%> ^ X) ^ Y) ^ (((<%((h . 0) + 1)%> ^ <%K%>) ^ <%(1 + ((Z + 1) * (K !)))%>) ^ <%Z%>)) . ((1 + n) + k))))), 0 are_congruent_mod (((<%(h . 0)%> ^ X) ^ Y) ^ (((<%((h . 0) + 1)%> ^ <%K%>) ^ <%(1 + ((Z + 1) * (K !)))%>) ^ <%Z%>)) . (((1 + n) + k) + 2)
then (((<%(h . 0)%> ^ X) ^ Y) ^ (((<%((h . 0) + 1)%> ^ <%K%>) ^ <%(1 + ((Z + 1) * (K !)))%>) ^ <%Z%>)) . ((1 + n) + i) = Y . i by A54;
hence Product ((((((<%(h . 0)%> ^ X) ^ Y) ^ (((<%((h . 0) + 1)%> ^ <%K%>) ^ <%(1 + ((Z + 1) * (K !)))%>) ^ <%Z%>)) . ((1 + n) + i)) + 1) + (- (idseq ((((<%(h . 0)%> ^ X) ^ Y) ^ (((<%((h . 0) + 1)%> ^ <%K%>) ^ <%(1 + ((Z + 1) * (K !)))%>) ^ <%Z%>)) . ((1 + n) + k))))), 0 are_congruent_mod (((<%(h . 0)%> ^ X) ^ Y) ^ (((<%((h . 0) + 1)%> ^ <%K%>) ^ <%(1 + ((Z + 1) * (K !)))%>) ^ <%Z%>)) . (((1 + n) + k) + 2) by A50, A52, A44, A62; :: thesis: verum
end;
A63: S1[((<%(h . 0)%> ^ X) ^ Y) ^ (((<%((h . 0) + 1)%> ^ <%K%>) ^ <%(1 + ((Z + 1) * (K !)))%>) ^ <%Z%>)] by A46, A51, A40;
A64: S2[((<%(h . 0)%> ^ X) ^ Y) ^ (((<%((h . 0) + 1)%> ^ <%K%>) ^ <%(1 + ((Z + 1) * (K !)))%>) ^ <%Z%>)] by A46, A47, A37, AFINSQ_1:57, A51, A40;
S3[((<%(h . 0)%> ^ X) ^ Y) ^ (((<%((h . 0) + 1)%> ^ <%K%>) ^ <%(1 + ((Z + 1) * (K !)))%>) ^ <%Z%>)] by A57, A61;
then ((<%(h . 0)%> ^ X) ^ Y) ^ (((<%((h . 0) + 1)%> ^ <%K%>) ^ <%(1 + ((Z + 1) * (K !)))%>) ^ <%Z%>) in { q where q is ((1 + n) + k) + 4 -element XFinSequence of NAT : S13[q] } by A63, A64, A46, A50, A51, A52, A53, A42, A59;
then A66: (((<%(h . 0)%> ^ X) ^ Y) ^ (((<%((h . 0) + 1)%> ^ <%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) ^ (((<%((h . 0) + 1)%> ^ <%K%>) ^ <%(1 + ((Z + 1) * (K !)))%>) ^ <%Z%>)) | (n + 1) = ((<%(h . 0)%> ^ X) ^ Y) | (n + 1) & len (<%(h . 0)%> ^ X) = 1 + n ) by NAT_1:11, A48, AFINSQ_1:58, CARD_1:def 7;
then (((<%(h . 0)%> ^ X) ^ Y) ^ (((<%((h . 0) + 1)%> ^ <%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 A35, A66, 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
A67: ( 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
A68: H = x and
A69: S13[H] by A67;
A70: ( ((1 + n) + k) + 4 >= (1 + n) + k & len H = ((1 + n) + k) + 4 ) by NAT_1:11, CARD_1:def 7;
then A71: len (H | ((1 + n) + k)) = (1 + n) + k by AFINSQ_1:54;
then A72: len ((H | ((1 + n) + k)) /^ (n + 1)) = ((1 + n) + k) -' (n + 1) by AFINSQ_2:def 2;
then A73: 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 A72, CARD_1:def 7, NAT_D:34;
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 ;
A74: 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 A75: 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, A75;
then reconsider X = (H /^ 1) | n as n -element XFinSequence of NAT by CARD_1:def 7;
A76: 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 A77: i in k ; :: thesis: Y . i = H . ((1 + n) + i)
then i in Segm k ;
then (1 + n) + i < Segm ((1 + n) + k) by NAT_1:44, XREAL_1:8;
then (H | ((1 + n) + k)) . ((n + 1) + i) = H . ((n + 1) + i) by NAT_1:44, FUNCT_1:49;
hence Y . i = H . ((1 + n) + i) by A77, A73, AFINSQ_2:def 2; :: thesis: verum
end;
A78: for i being Nat st i in k holds
Y . i > x + 1
proof
let i be Nat; :: thesis: ( i in k implies Y . i > x + 1 )
assume A79: i in k ; :: thesis: Y . i > x + 1
Y . i = H . ((1 + n) + i) by A79, A76;
hence Y . i > x + 1 by A79, A69; :: thesis: verum
end;
len <%Z%> = 1 by CARD_1:def 7;
then len (<%Z%> ^ (H | ((1 + n) + k))) = 1 + ((1 + n) + k) by A71, 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 aa: (H | ((1 + n) + k)) | (n + 1) = H | (n + 1) by RELAT_1:74;
A81: ( (1 + 1) -' 1 = 1 & (n + 2) -' 2 = n ) by NAT_D:34;
n + 1 <= (n + 1) + (k + 4) by NAT_1:11;
then A82: (H /^ ((1 + 1) -' 1)) | (((n + 1) + 1) -' (1 + 1)) = mid (H,(1 + 1),(n + 1)) by A70, AFINSQ_2:15
.= (H | (n + 1)) /^ ((1 + 1) -' 1) by AFINSQ_2:def 3 ;
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 H | ((1 + n) + k) = (<%x%> ^ X) ^ Y by aa, A82, A81;
then ZY = <%Z%> ^ (<%x%> ^ (X ^ Y)) by AFINSQ_1:27
.= (<%Z%> ^ <%x%>) ^ (X ^ Y) by AFINSQ_1:27
.= (<%Z,x%> ^ X) ^ Y by AFINSQ_1:27 ;
then A83: eval (p,(@ ((<%Z,x%> ^ X) ^ Y))), 0 are_congruent_mod 1 + ((Z + 1) * (K !)) by A69;
A84: for i being Nat st i in k holds
Product (((Y . i) + 1) + (- (idseq (x + 1)))), 0 are_congruent_mod 1 + ((Z + 1) * (K !))
proof
let i be Nat; :: thesis: ( i in k implies Product (((Y . i) + 1) + (- (idseq (x + 1)))), 0 are_congruent_mod 1 + ((Z + 1) * (K !)) )
assume A85: i in k ; :: thesis: Product (((Y . i) + 1) + (- (idseq (x + 1)))), 0 are_congruent_mod 1 + ((Z + 1) * (K !))
then Y . i = H . ((n + 1) + i) by A76;
hence Product (((Y . i) + 1) + (- (idseq (x + 1)))), 0 are_congruent_mod 1 + ((Z + 1) * (K !)) by A85, A69; :: thesis: verum
end;
n + 1 <= (n + 1) + (k + 4) by NAT_1:11;
then len (H | (n + 1)) = n + 1 by AFINSQ_1:54, A74;
then reconsider F = H | (n + 1) as n + 1 -element XFinSequence of NAT by CARD_1:def 7;
0 < len F ;
then A86: F . 0 = H . 0 by AFINSQ_1:66, FUNCT_1:47;
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
( ( for i being Nat st i in k holds
y . i <= F . 0 ) & 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
( ( for i being Nat st i in k holds
y . i <= F . 0 ) & eval (p,(@ ((<%z,(F . 0)%> ^ X1) ^ y))) = 0 ) )
assume 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
( ( for i being Nat st i in k holds
y . i <= F . 0 ) & eval (p,(@ ((<%z,(F . 0)%> ^ X1) ^ y))) = 0 )
then consider y being k -element XFinSequence of NAT such that
A88: ( ( for i being Nat st i in k holds
y . i <= x ) & eval (p,(@ ((<%z,x%> ^ X) ^ y))) = 0 ) by A86, A84, Th17, A69, A78, A83;
take y ; :: thesis: for X1 being n -element XFinSequence of NAT st X1 = F /^ 1 holds
( ( for i being Nat st i in k holds
y . i <= F . 0 ) & eval (p,(@ ((<%z,(F . 0)%> ^ X1) ^ y))) = 0 )
let X1 be n -element XFinSequence of NAT ; :: thesis: ( X1 = F /^ 1 implies ( ( for i being Nat st i in k holds
y . i <= F . 0 ) & eval (p,(@ ((<%z,(F . 0)%> ^ X1) ^ y))) = 0 ) )
assume X1 = F /^ 1 ; :: thesis: ( ( for i being Nat st i in k holds
y . i <= F . 0 ) & eval (p,(@ ((<%z,(F . 0)%> ^ X1) ^ y))) = 0 )
hence ( ( for i being Nat st i in k holds
y . i <= F . 0 ) & eval (p,(@ ((<%z,(F . 0)%> ^ X1) ^ y))) = 0 ) by A88, A86, A82, A81; :: thesis: verum
end;
hence s in { X where X is n + 1 -element XFinSequence of NAT : S14[X] } by A68, A67; :: thesis: verum
end;
then A89: { 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] } } ;
A90: { (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 HILB10_4:27, A89, A34;
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
( ( for i being Nat st i in k holds
y . i <= x ) & 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
( ( for i being Nat st i in k holds
y . i <= x ) & 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
( ( for i being Nat st i in k holds
y . i <= x ) & 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
( ( for i being Nat st i in k holds
y . i <= x ) & 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
( ( for i being Nat st i in k holds
y . i <= x ) & eval (p,(@ ((<%z,x%> ^ X) ^ y))) = 0 ) }
then consider xS being n + 1 -element XFinSequence of NAT such that
A91: ( s = xS /^ 1 & xS in { X where X is n + 1 -element XFinSequence of NAT : S14[X] } ) ;
A92: ex w being n + 1 -element XFinSequence of NAT st
( xS = w & S14[w] ) by A91;
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
( ( for i being Nat st i in k holds
y . i <= x ) & 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
( ( for i being Nat st i in k holds
y . i <= x ) & 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
( ( for i being Nat st i in k holds
y . i <= x ) & eval (p,(@ ((<%z,x%> ^ S) ^ y))) = 0 ) )
assume A93: z <= x ; :: thesis: 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%> ^ S) ^ y))) = 0 )
consider y being k -element XFinSequence of NAT such that
A94: for X1 being n -element XFinSequence of NAT st X1 = xS /^ 1 holds
( ( for i being Nat st i in k holds
y . i <= x ) & eval (p,(@ ((<%z,(xS . 0)%> ^ X1) ^ y))) = 0 ) by A92, A93;
take y ; :: thesis: ( ( for i being Nat st i in k holds
y . i <= x ) & eval (p,(@ ((<%z,x%> ^ S) ^ y))) = 0 )
S = xS /^ 1 ;
hence ( ( for i being Nat st i in k holds
y . i <= x ) & eval (p,(@ ((<%z,x%> ^ S) ^ y))) = 0 ) by A94; :: 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
( ( for i being Nat st i in k holds
y . i <= x ) & eval (p,(@ ((<%z,x%> ^ X) ^ y))) = 0 ) } by A91; :: 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
( ( for i being Nat st i in k holds
y . i <= x ) & 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
A95: ( 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
( ( for i being Nat st i in k holds
y . i <= x ) & eval (p,(@ ((<%z,x%> ^ S) ^ y))) = 0 ) ) ;
consider x being Element of NAT such that
A96: 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%> ^ S) ^ y))) = 0 ) by A95;
set xS = <%x%> ^ S;
len <%x%> = 1 by CARD_1:def 7;
then A97: (<%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
( ( for i being Nat st i in k holds
y . i <= (<%x%> ^ S) . 0 ) & eval (p,(@ ((<%z,((<%x%> ^ S) . 0)%> ^ X1) ^ y))) = 0 ) )
assume A98: 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
( ( for i being Nat st i in k holds
y . i <= (<%x%> ^ S) . 0 ) & eval (p,(@ ((<%z,((<%x%> ^ S) . 0)%> ^ X1) ^ y))) = 0 )
(<%x%> ^ S) . 0 = x by AFINSQ_1:35;
then consider y being k -element XFinSequence of NAT such that
A99: ( ( for i being Nat st i in k holds
y . i <= (<%x%> ^ S) . 0 ) & eval (p,(@ ((<%z,x%> ^ S) ^ y))) = 0 ) by A96, A98;
take y ; :: thesis: for X1 being n -element XFinSequence of NAT st X1 = (<%x%> ^ S) /^ 1 holds
( ( for i being Nat st i in k holds
y . i <= (<%x%> ^ S) . 0 ) & eval (p,(@ ((<%z,((<%x%> ^ S) . 0)%> ^ X1) ^ y))) = 0 )
thus for X1 being n -element XFinSequence of NAT st X1 = (<%x%> ^ S) /^ 1 holds
( ( for i being Nat st i in k holds
y . i <= (<%x%> ^ S) . 0 ) & eval (p,(@ ((<%z,((<%x%> ^ S) . 0)%> ^ X1) ^ y))) = 0 ) by A97, AFINSQ_1:35, A99; :: 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 A97, A95; :: 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
( ( for i being Nat st i in k holds
y . i <= x ) & eval (p,(@ ((<%z,x%> ^ X) ^ y))) = 0 ) } is diophantine Subset of (n -xtuples_of NAT) by A90, TARSKI:2; :: thesis: verum