let k, n1, n2, i, j, l, m be Nat; for n being Nat
for i1, i2, i3, i4 being Element of n st n1 + n2 <= n holds
{ p where p is b1 -element XFinSequence of NAT : p . i1 >= k * ((((((p . i2) ^2) + 1) * (Product (1 + ((p /^ n1) | n2)))) * ((l * (p . i3)) + m)) |^ ((i * (p . i4)) + j)) } is diophantine Subset of (n -xtuples_of NAT)
deffunc H1( Nat, Nat, Nat) -> set = $1 |^ $2;
A1:
for n being Nat
for i1, i2, i3, i4 being Element of n holds { p where p is b1 -element XFinSequence of NAT : H1(p . i1,p . i2,p . i3) = p . i4 } is diophantine Subset of (n -xtuples_of NAT)
by HILB10_3:24;
defpred S1[ Nat, Nat, natural object , Nat, Nat, Nat] means 1 * $1 >= (k * $3) + 0;
A2:
for n being Nat
for i1, i2, i3, i4, i5, i6 being Element of n holds { p where p is b1 -element XFinSequence of NAT : S1[p . i1,p . i2,p . i3,p . i4,p . i5,p . i6] } is diophantine Subset of (n -xtuples_of NAT)
by HILB10_3:8;
A3:
for n being Nat
for i1, i2, i3, i4, i5 being Element of n holds { p where p is b1 -element XFinSequence of NAT : S1[p . i1,p . i2,H1(p . i3,p . i4,p . i5),p . i3,p . i4,p . i5] } is diophantine Subset of (n -xtuples_of NAT)
from HILB10_3:sch 4(A2, A1);
deffunc H2( Nat, Nat, Nat) -> set = (i * $1) + j;
A4:
for n being Nat
for i1, i2, i3, i4 being Element of n holds { p where p is b1 -element XFinSequence of NAT : H2(p . i1,p . i2,p . i3) = p . i4 } is diophantine Subset of (n -xtuples_of NAT)
by HILB10_3:15;
defpred S2[ Nat, Nat, natural object , Nat, Nat, Nat] means $1 >= k * ($2 |^ $3);
A5:
now for n being Nat
for i1, i2, i3, i4, i5, i6 being Element of n holds { p where p is b1 -element XFinSequence of NAT : S2[p . i1,p . i2,p . i3,p . i4,p . i5,p . i6] } is diophantine Subset of (n -xtuples_of NAT)let n be
Nat;
for i1, i2, i3, i4, i5, i6 being Element of n holds { p where p is n -element XFinSequence of NAT : S2[p . i1,p . i2,p . i3,p . i4,p . i5,p . i6] } is diophantine Subset of (n -xtuples_of NAT)let i1,
i2,
i3,
i4,
i5,
i6 be
Element of
n;
{ p where p is n -element XFinSequence of NAT : S2[p . i1,p . i2,p . i3,p . i4,p . i5,p . i6] } is diophantine Subset of (n -xtuples_of NAT)defpred S3[
XFinSequence of
NAT ]
means S1[$1
. i1,$1
. i2,
($1 . i2) |^ ($1 . i3),$1
. i4,$1
. i5,$1
. i6];
defpred S4[
XFinSequence of
NAT ]
means S2[$1
. i1,$1
. i2,$1
. i3,$1
. i4,$1
. i5,$1
. i6];
A6:
for
p being
n -element XFinSequence of
NAT holds
(
S3[
p] iff
S4[
p] )
;
{ p where p is n -element XFinSequence of NAT : S3[p] } = { q where q is n -element XFinSequence of NAT : S4[q] }
from HILB10_3:sch 2(A6);
hence
{ p where p is n -element XFinSequence of NAT : S2[p . i1,p . i2,p . i3,p . i4,p . i5,p . i6] } is
diophantine Subset of
(n -xtuples_of NAT)
by A3;
verum end;
A7:
for n being Nat
for i1, i2, i3, i4, i5 being Element of n holds { p where p is b1 -element XFinSequence of NAT : S2[p . i1,p . i2,H2(p . i3,p . i4,p . i5),p . i3,p . i4,p . i5] } is diophantine Subset of (n -xtuples_of NAT)
from HILB10_3:sch 4(A5, A4);
deffunc H3( Nat, Nat, Nat) -> set = (1 * $1) * $2;
A8:
for n being Nat
for i1, i2, i3, i4 being Element of n holds { p where p is b1 -element XFinSequence of NAT : H3(p . i1,p . i2,p . i3) = p . i4 } is diophantine Subset of (n -xtuples_of NAT)
by HILB10_4:26;
defpred S3[ Nat, Nat, natural object , Nat, Nat, Nat] means $1 >= k * ($3 |^ ((i * $2) + j));
A9:
for n being Nat
for i1, i3, i2, i4, i5, i6 being Element of n holds { p where p is b1 -element XFinSequence of NAT : S3[p . i1,p . i3,p . i2,p . i4,p . i5,p . i6] } is diophantine Subset of (n -xtuples_of NAT)
by A7;
A10:
for n being Nat
for i1, i2, i3, i4, i5 being Element of n holds { p where p is b1 -element XFinSequence of NAT : S3[p . i1,p . i2,H3(p . i3,p . i4,p . i5),p . i3,p . i4,p . i5] } is diophantine Subset of (n -xtuples_of NAT)
from HILB10_3:sch 4(A9, A8);
defpred S4[ Nat, Nat, natural object , Nat, Nat, Nat] means $1 >= k * (($6 * $3) |^ ((i * $2) + j));
A11:
now for n being Nat
for i1, i2, i4, i5, i6, i3 being Element of n holds { p where p is b1 -element XFinSequence of NAT : S4[p . i1,p . i2,p . i4,p . i5,p . i6,p . i3] } is diophantine Subset of (n -xtuples_of NAT)let n be
Nat;
for i1, i2, i4, i5, i6, i3 being Element of n holds { p where p is n -element XFinSequence of NAT : S4[p . i1,p . i2,p . i4,p . i5,p . i6,p . i3] } is diophantine Subset of (n -xtuples_of NAT)let i1,
i2,
i4,
i5,
i6,
i3 be
Element of
n;
{ p where p is n -element XFinSequence of NAT : S4[p . i1,p . i2,p . i4,p . i5,p . i6,p . i3] } is diophantine Subset of (n -xtuples_of NAT)defpred S5[
XFinSequence of
NAT ]
means S3[$1
. i1,$1
. i2,
(1 * ($1 . i3)) * ($1 . i4),$1
. i4,$1
. i5,$1
. i5];
defpred S6[
XFinSequence of
NAT ]
means S4[$1
. i1,$1
. i2,$1
. i4,$1
. i5,$1
. i6,$1
. i3];
A12:
for
p being
n -element XFinSequence of
NAT holds
(
S5[
p] iff
S6[
p] )
;
{ p where p is n -element XFinSequence of NAT : S5[p] } = { q where q is n -element XFinSequence of NAT : S6[q] }
from HILB10_3:sch 2(A12);
hence
{ p where p is n -element XFinSequence of NAT : S4[p . i1,p . i2,p . i4,p . i5,p . i6,p . i3] } is
diophantine Subset of
(n -xtuples_of NAT)
by A10;
verum end;
A13:
for n being Nat
for i1, i2, i3, i4, i5 being Element of n holds { p where p is b1 -element XFinSequence of NAT : S4[p . i1,p . i2,H3(p . i3,p . i4,p . i5),p . i3,p . i4,p . i5] } is diophantine Subset of (n -xtuples_of NAT)
from HILB10_3:sch 4(A11, A8);
deffunc H4( Nat, Nat, Nat) -> Element of omega = (1 * $1) + 1;
A14:
for n being Nat
for i1, i2, i3, i4 being Element of n holds { p where p is b1 -element XFinSequence of NAT : H4(p . i1,p . i2,p . i3) = p . i4 } is diophantine Subset of (n -xtuples_of NAT)
by HILB10_3:15;
defpred S5[ Nat, Nat, natural object , Nat, Nat, Nat] means $1 >= k * ((($3 * $5) * $6) |^ ((i * $2) + j));
A15:
now for n being Nat
for i1, i2, i4, i3, i5, i6 being Element of n holds { p where p is b1 -element XFinSequence of NAT : S5[p . i1,p . i2,p . i4,p . i3,p . i5,p . i6] } is diophantine Subset of (n -xtuples_of NAT)let n be
Nat;
for i1, i2, i4, i3, i5, i6 being Element of n holds { p where p is n -element XFinSequence of NAT : S5[p . i1,p . i2,p . i4,p . i3,p . i5,p . i6] } is diophantine Subset of (n -xtuples_of NAT)let i1,
i2,
i4,
i3,
i5,
i6 be
Element of
n;
{ p where p is n -element XFinSequence of NAT : S5[p . i1,p . i2,p . i4,p . i3,p . i5,p . i6] } is diophantine Subset of (n -xtuples_of NAT)defpred S6[
XFinSequence of
NAT ]
means S4[$1
. i1,$1
. i2,
(1 * ($1 . i4)) * ($1 . i5),$1
. i4,$1
. i5,$1
. i6];
defpred S7[
XFinSequence of
NAT ]
means S5[$1
. i1,$1
. i2,$1
. i4,$1
. i3,$1
. i5,$1
. i6];
A16:
for
p being
n -element XFinSequence of
NAT holds
(
S6[
p] iff
S7[
p] )
;
{ p where p is n -element XFinSequence of NAT : S6[p] } = { q where q is n -element XFinSequence of NAT : S7[q] }
from HILB10_3:sch 2(A16);
hence
{ p where p is n -element XFinSequence of NAT : S5[p . i1,p . i2,p . i4,p . i3,p . i5,p . i6] } is
diophantine Subset of
(n -xtuples_of NAT)
by A13;
verum end;
A17:
for n being Nat
for i1, i2, i3, i4, i5 being Element of n holds { p where p is b1 -element XFinSequence of NAT : S5[p . i1,p . i2,H4(p . i3,p . i4,p . i5),p . i3,p . i4,p . i5] } is diophantine Subset of (n -xtuples_of NAT)
from HILB10_3:sch 4(A15, A14);
deffunc H5( Nat, Nat, Nat) -> set = (l * $1) + m;
A18:
for n being Nat
for i1, i2, i3, i4 being Element of n holds { p where p is b1 -element XFinSequence of NAT : H5(p . i1,p . i2,p . i3) = p . i4 } is diophantine Subset of (n -xtuples_of NAT)
by HILB10_3:15;
defpred S6[ Nat, Nat, natural object , Nat, Nat, Nat] means $1 >= k * ((($3 * $5) * ($6 + 1)) |^ ((i * $2) + j));
A19:
now for n being Nat
for i1, i2, i6, i4, i5, i3 being Element of n holds { p where p is b1 -element XFinSequence of NAT : S6[p . i1,p . i2,p . i6,p . i4,p . i5,p . i3] } is diophantine Subset of (n -xtuples_of NAT)let n be
Nat;
for i1, i2, i6, i4, i5, i3 being Element of n holds { p where p is n -element XFinSequence of NAT : S6[p . i1,p . i2,p . i6,p . i4,p . i5,p . i3] } is diophantine Subset of (n -xtuples_of NAT)let i1,
i2,
i6,
i4,
i5,
i3 be
Element of
n;
{ p where p is n -element XFinSequence of NAT : S6[p . i1,p . i2,p . i6,p . i4,p . i5,p . i3] } is diophantine Subset of (n -xtuples_of NAT)defpred S7[
XFinSequence of
NAT ]
means S5[$1
. i1,$1
. i2,
(1 * ($1 . i3)) + 1,$1
. i4,$1
. i5,$1
. i6];
defpred S8[
XFinSequence of
NAT ]
means S6[$1
. i1,$1
. i2,$1
. i6,$1
. i4,$1
. i5,$1
. i3];
A20:
for
p being
n -element XFinSequence of
NAT holds
(
S7[
p] iff
S8[
p] )
;
{ p where p is n -element XFinSequence of NAT : S7[p] } = { q where q is n -element XFinSequence of NAT : S8[q] }
from HILB10_3:sch 2(A20);
hence
{ p where p is n -element XFinSequence of NAT : S6[p . i1,p . i2,p . i6,p . i4,p . i5,p . i3] } is
diophantine Subset of
(n -xtuples_of NAT)
by A17;
verum end;
A21:
for n being Nat
for i1, i2, i3, i4, i5 being Element of n holds { p where p is b1 -element XFinSequence of NAT : S6[p . i1,p . i2,H5(p . i3,p . i4,p . i5),p . i3,p . i4,p . i5] } is diophantine Subset of (n -xtuples_of NAT)
from HILB10_3:sch 4(A19, A18);
defpred S7[ Nat, Nat, natural object , Nat, Nat, Nat] means $1 >= k * (((($3 + 1) * $5) * ((l * $6) + m)) |^ ((i * $2) + j));
deffunc H6( Nat, Nat, Nat) -> set = (1 * $1) * $1;
A22:
for n being Nat
for i1, i2, i3, i4 being Element of n holds { p where p is b1 -element XFinSequence of NAT : H6(p . i1,p . i2,p . i3) = p . i4 } is diophantine Subset of (n -xtuples_of NAT)
by HILB10_4:26;
A23:
now for n being Nat
for i1, i2, i6, i4, i5, i3 being Element of n holds { p where p is b1 -element XFinSequence of NAT : S7[p . i1,p . i2,p . i6,p . i4,p . i5,p . i3] } is diophantine Subset of (n -xtuples_of NAT)let n be
Nat;
for i1, i2, i6, i4, i5, i3 being Element of n holds { p where p is n -element XFinSequence of NAT : S7[p . i1,p . i2,p . i6,p . i4,p . i5,p . i3] } is diophantine Subset of (n -xtuples_of NAT)let i1,
i2,
i6,
i4,
i5,
i3 be
Element of
n;
{ p where p is n -element XFinSequence of NAT : S7[p . i1,p . i2,p . i6,p . i4,p . i5,p . i3] } is diophantine Subset of (n -xtuples_of NAT)defpred S8[
XFinSequence of
NAT ]
means S6[$1
. i1,$1
. i2,
(l * ($1 . i3)) + m,$1
. i4,$1
. i5,$1
. i6];
defpred S9[
XFinSequence of
NAT ]
means S7[$1
. i1,$1
. i2,$1
. i6,$1
. i4,$1
. i5,$1
. i3];
A24:
for
p being
n -element XFinSequence of
NAT holds
(
S8[
p] iff
S9[
p] )
;
{ p where p is n -element XFinSequence of NAT : S8[p] } = { q where q is n -element XFinSequence of NAT : S9[q] }
from HILB10_3:sch 2(A24);
hence
{ p where p is n -element XFinSequence of NAT : S7[p . i1,p . i2,p . i6,p . i4,p . i5,p . i3] } is
diophantine Subset of
(n -xtuples_of NAT)
by A21;
verum end;
A25:
for n being Nat
for i1, i2, i3, i4, i5 being Element of n holds { p where p is b1 -element XFinSequence of NAT : S7[p . i1,p . i2,H6(p . i3,p . i4,p . i5),p . i3,p . i4,p . i5] } is diophantine Subset of (n -xtuples_of NAT)
from HILB10_3:sch 4(A23, A22);
let n be Nat; for i1, i2, i3, i4 being Element of n st n1 + n2 <= n holds
{ p where p is n -element XFinSequence of NAT : p . i1 >= k * ((((((p . i2) ^2) + 1) * (Product (1 + ((p /^ n1) | n2)))) * ((l * (p . i3)) + m)) |^ ((i * (p . i4)) + j)) } is diophantine Subset of (n -xtuples_of NAT)
let i1, i2, i3, i4 be Element of n; ( n1 + n2 <= n implies { p where p is n -element XFinSequence of NAT : p . i1 >= k * ((((((p . i2) ^2) + 1) * (Product (1 + ((p /^ n1) | n2)))) * ((l * (p . i3)) + m)) |^ ((i * (p . i4)) + j)) } is diophantine Subset of (n -xtuples_of NAT) )
assume A26:
n1 + n2 <= n
; { p where p is n -element XFinSequence of NAT : p . i1 >= k * ((((((p . i2) ^2) + 1) * (Product (1 + ((p /^ n1) | n2)))) * ((l * (p . i3)) + m)) |^ ((i * (p . i4)) + j)) } is diophantine Subset of (n -xtuples_of NAT)
set X = n + 1;
A27:
n < n + 1
by NAT_1:13;
then
n in Segm (n + 1)
by NAT_1:44;
then reconsider N = n, I1 = i1, I2 = i2, I3 = i3, I4 = i4 as Element of n + 1 by HILB10_3:2;
defpred S8[ XFinSequence of NAT ] means $1 . I1 >= k * ((((((1 * ($1 . I2)) * ($1 . I2)) + 1) * ($1 . N)) * ((l * ($1 . I3)) + m)) |^ ((i * ($1 . I4)) + j));
A28:
{ p where p is n + 1 -element XFinSequence of NAT : S8[p] } is diophantine Subset of ((n + 1) -xtuples_of NAT)
by A25;
defpred S9[ XFinSequence of NAT ] means $1 . N = Product (1 + (($1 /^ n1) | n2));
A29:
{ p where p is n + 1 -element XFinSequence of NAT : S9[p] } is diophantine Subset of ((n + 1) -xtuples_of NAT)
by HILB10_4:39;
set PQ = { p where p is n + 1 -element XFinSequence of NAT : ( S8[p] & S9[p] ) } ;
A30:
{ p where p is n + 1 -element XFinSequence of NAT : ( S8[p] & S9[p] ) } is diophantine Subset of ((n + 1) -xtuples_of NAT)
from HILB10_3:sch 3(A28, A29);
set PQr = { (p | n) where p is n + 1 -element XFinSequence of NAT : p in { p where p is n + 1 -element XFinSequence of NAT : ( S8[p] & S9[p] ) } } ;
defpred S10[ XFinSequence of NAT ] means $1 . i1 >= k * (((((($1 . i2) ^2) + 1) * (Product (1 + (($1 /^ n1) | n2)))) * ((l * ($1 . i3)) + m)) |^ ((i * ($1 . i4)) + j));
set S = { p where p is n -element XFinSequence of NAT : S10[p] } ;
A31:
{ (p | n) where p is n + 1 -element XFinSequence of NAT : p in { p where p is n + 1 -element XFinSequence of NAT : ( S8[p] & S9[p] ) } } is diophantine Subset of (n -xtuples_of NAT)
by HILB10_3:5, A27, A30;
A32:
n1 <= n1 + n2
by NAT_1:11;
A33:
n -' n1 = n - n1
by A32, A26, XXREAL_0:2, XREAL_1:233;
A34:
n2 <= n - n1
by A26, XREAL_1:19;
{ p where p is n -element XFinSequence of NAT : S10[p] } c= n -xtuples_of NAT
then reconsider S = { p where p is n -element XFinSequence of NAT : S10[p] } as Subset of (n -xtuples_of NAT) ;
per cases
( n = 0 or n <> 0 )
;
suppose A35:
n <> 0
;
{ p where p is n -element XFinSequence of NAT : p . i1 >= k * ((((((p . i2) ^2) + 1) * (Product (1 + ((p /^ n1) | n2)))) * ((l * (p . i3)) + m)) |^ ((i * (p . i4)) + j)) } is diophantine Subset of (n -xtuples_of NAT)A36:
S c= { (p | n) where p is n + 1 -element XFinSequence of NAT : p in { p where p is n + 1 -element XFinSequence of NAT : ( S8[p] & S9[p] ) } }
proof
let y be
object ;
TARSKI:def 3 ( not y in S or y in { (p | n) where p is n + 1 -element XFinSequence of NAT : p in { p where p is n + 1 -element XFinSequence of NAT : ( S8[p] & S9[p] ) } } )
assume
y in S
;
y in { (p | n) where p is n + 1 -element XFinSequence of NAT : p in { p where p is n + 1 -element XFinSequence of NAT : ( S8[p] & S9[p] ) } }
then consider p being
n -element XFinSequence of
NAT such that A37:
(
y = p &
S10[
p] )
;
A38:
len p = n
by CARD_1:def 7;
then A39:
len (p /^ n1) >= n2
by A34, A33, AFINSQ_2:def 2;
reconsider P =
Product (1 + ((p /^ n1) | n2)) as
Element of
NAT by ORDINAL1:def 12;
reconsider pP =
p ^ <%P%> as
n + 1
-element XFinSequence of
NAT ;
A40:
pP | n = p
by A38, AFINSQ_1:57;
A41:
pP . N = P
by A38, AFINSQ_1:36;
A42:
(
pP . I1 = p . i1 &
pP . I2 = p . i2 &
pP . I3 = p . i3 &
pP . I4 = p . i4 )
by A35, A40, HILB10_3:4;
A43:
(pP /^ n1) | n2 =
((p /^ n1) ^ <%P%>) | n2
by HILB10_4:10, A38, A32, A26, XXREAL_0:2
.=
(p /^ n1) | n2
by AFINSQ_1:58, A39
;
(
S8[
pP] &
S9[
pP] )
by A43, A42, A41, A37, SQUARE_1:def 1;
then
pP in { p where p is n + 1 -element XFinSequence of NAT : ( S8[p] & S9[p] ) }
;
hence
y in { (p | n) where p is n + 1 -element XFinSequence of NAT : p in { p where p is n + 1 -element XFinSequence of NAT : ( S8[p] & S9[p] ) } }
by A37, A40;
verum
end;
{ (p | n) where p is n + 1 -element XFinSequence of NAT : p in { p where p is n + 1 -element XFinSequence of NAT : ( S8[p] & S9[p] ) } } c= S
proof
let y be
object ;
TARSKI:def 3 ( not y in { (p | n) where p is n + 1 -element XFinSequence of NAT : p in { p where p is n + 1 -element XFinSequence of NAT : ( S8[p] & S9[p] ) } } or y in S )
assume
y in { (p | n) where p is n + 1 -element XFinSequence of NAT : p in { p where p is n + 1 -element XFinSequence of NAT : ( S8[p] & S9[p] ) } }
;
y in S
then consider pP being
n + 1
-element XFinSequence of
NAT such that A44:
(
y = pP | n &
pP in { p where p is n + 1 -element XFinSequence of NAT : ( S8[p] & S9[p] ) } )
;
A45:
ex
q being
n + 1
-element XFinSequence of
NAT st
(
pP = q &
S8[
q] &
S9[
q] )
by A44;
A46:
len pP = n + 1
by CARD_1:def 7;
then A47:
len (pP | n) = n
by A27, AFINSQ_1:54;
then reconsider p =
pP | n as
n -element XFinSequence of
NAT by CARD_1:def 7;
A48:
len (p /^ n1) >= n2
by A34, A33, A47, AFINSQ_2:def 2;
set P =
Product (1 + ((p /^ n1) | n2));
A49:
pP = p ^ <%(pP . n)%>
by A46, AFINSQ_1:56;
A50:
(pP /^ n1) | n2 =
((p /^ n1) ^ <%(pP . n)%>) | n2
by A49, HILB10_4:10, A47, A32, A26, XXREAL_0:2
.=
(p /^ n1) | n2
by AFINSQ_1:58, A48
;
A51:
(
pP . I1 = p . i1 &
pP . I2 = p . i2 &
pP . I3 = p . i3 &
pP . I4 = p . i4 )
by A35, HILB10_3:4;
(p . i2) * (p . i2) = (p . i2) ^2
by SQUARE_1:def 1;
hence
y in S
by A44, A50, A51, A45;
verum
end; hence
{ p where p is n -element XFinSequence of NAT : p . i1 >= k * ((((((p . i2) ^2) + 1) * (Product (1 + ((p /^ n1) | n2)))) * ((l * (p . i3)) + m)) |^ ((i * (p . i4)) + j)) } is
diophantine Subset of
(n -xtuples_of NAT)
by A31, A36, XBOOLE_0:def 10;
verum end;