deffunc H1( Nat, Nat, Nat) -> object = |.F1($1,$2,$3).|;
defpred S1[ Nat, Nat, natural object , Nat, Nat, Nat] means ( P1[$1,$2,1 * $3] & F1($4,$5,$6) >= 0 );
defpred S2[ Nat, Nat, natural object , Nat, Nat, Nat] means ( P1[$1,$2,(- 1) * $3] & F1($4,$5,$6) <= 0 );
A3:
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)
proof
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 : S1[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 : S1[p . i1,p . i2,p . i3,p . i4,p . i5,p . i6] } is diophantine Subset of (n -xtuples_of NAT)
set M =
{ p where p is n -element XFinSequence of NAT : S1[p . i1,p . i2,p . i3,p . i4,p . i5,p . i6] } ;
per cases
( n = 0 or n <> 0 )
;
suppose A4:
n = 0
;
{ p where p is n -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)
{ p where p is n -element XFinSequence of NAT : S1[p . i1,p . i2,p . i3,p . i4,p . i5,p . i6] } c= n -xtuples_of NAT
proof
let x be
object ;
TARSKI:def 3 ( not x in { p where p is n -element XFinSequence of NAT : S1[p . i1,p . i2,p . i3,p . i4,p . i5,p . i6] } or x in n -xtuples_of NAT )
assume
x in { p where p is n -element XFinSequence of NAT : S1[p . i1,p . i2,p . i3,p . i4,p . i5,p . i6] }
;
x in n -xtuples_of NAT
then
ex
p being
n -element XFinSequence of
NAT st
(
x = p &
S1[
p . i1,
p . i2,
p . i3,
p . i4,
p . i5,
p . i6] )
;
hence
x in n -xtuples_of NAT
by HILB10_2:def 5;
verum
end; hence
{ p where p is n -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 A4;
verum end; suppose A5:
n <> 0
;
{ p where p is n -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)set n1 =
n + 1;
A6:
n < n + 1
by NAT_1:13;
then
n in Segm (n + 1)
by NAT_1:44;
then reconsider I1 =
i1,
I2 =
i2,
I3 =
i3,
I4 =
i4,
I5 =
i5,
I6 =
i6,
N =
n as
Element of
n + 1
by Th2;
defpred S3[
XFinSequence of
NAT ]
means P1[$1
. I1,$1
. I2,1
* ($1 . I3)];
reconsider P =
{ p where p is n + 1 -element XFinSequence of NAT : S3[p] } as
diophantine Subset of
((n + 1) -xtuples_of NAT) by A1;
reconsider F =
{ p where p is n + 1 -element XFinSequence of NAT : F1((p . I4),(p . I5),(p . I6)) = 1 * (p . N) } as
diophantine Subset of
((n + 1) -xtuples_of NAT) by A2;
reconsider PF =
P /\ F as
Subset of
((n + 1) -xtuples_of NAT) ;
reconsider PFk =
{ (p | n) where p is n + 1 -element XFinSequence of NAT : p in PF } as
diophantine Subset of
(n -xtuples_of NAT) by Th5, A6;
A7:
PFk c= { p where p is n -element XFinSequence of NAT : S1[p . i1,p . i2,p . i3,p . i4,p . i5,p . i6] }
proof
let x be
object ;
TARSKI:def 3 ( not x in PFk or x in { p where p is n -element XFinSequence of NAT : S1[p . i1,p . i2,p . i3,p . i4,p . i5,p . i6] } )
assume
x in PFk
;
x in { p where p is n -element XFinSequence of NAT : S1[p . i1,p . i2,p . i3,p . i4,p . i5,p . i6] }
then consider p being
n + 1
-element XFinSequence of
NAT such that A8:
(
x = p | n &
p in PF )
;
p in P
by A8, XBOOLE_0:def 4;
then A9:
ex
q being
n + 1
-element XFinSequence of
NAT st
(
p = q &
S3[
q] )
;
p in F
by A8, XBOOLE_0:def 4;
then A10:
ex
q being
n + 1
-element XFinSequence of
NAT st
(
p = q &
F1(
(q . I4),
(q . I5),
(q . I6))
= 1
* (q . N) )
;
len p = n + 1
by CARD_1:def 7;
then
len (p | n) = n
by A6, AFINSQ_1:54;
then reconsider pn =
p | n as
n -element XFinSequence of
NAT by CARD_1:def 7;
(
p . I1 = pn . I1 &
p . I2 = pn . I2 &
p . I3 = pn . I3 &
p . I4 = pn . I4 &
pn . I5 = p . I5 &
pn . i6 = p . I6 )
by A5, Th4;
hence
x in { p where p is n -element XFinSequence of NAT : S1[p . i1,p . i2,p . i3,p . i4,p . i5,p . i6] }
by A8, A9, A10;
verum
end;
{ p where p is n -element XFinSequence of NAT : S1[p . i1,p . i2,p . i3,p . i4,p . i5,p . i6] } c= PFk
proof
let x be
object ;
TARSKI:def 3 ( not x in { p where p is n -element XFinSequence of NAT : S1[p . i1,p . i2,p . i3,p . i4,p . i5,p . i6] } or x in PFk )
assume
x in { p where p is n -element XFinSequence of NAT : S1[p . i1,p . i2,p . i3,p . i4,p . i5,p . i6] }
;
x in PFk
then consider p being
n -element XFinSequence of
NAT such that A11:
(
x = p &
S1[
p . i1,
p . i2,
p . i3,
p . i4,
p . i5,
p . i6] )
;
reconsider FF =
F1(
(p . i4),
(p . i5),
(p . i6)) as
Element of
NAT by A11, INT_1:3;
reconsider Z =
<%FF%> as 1
-element XFinSequence of
NAT ;
set pZ =
p ^ Z;
A12:
len p = n
by CARD_1:def 7;
then A13:
(
(p ^ Z) | n = p &
(p ^ Z) . n = FF )
by AFINSQ_1:57, AFINSQ_1:36;
then
(
p . i1 = (p ^ Z) . i1 &
p . i2 = (p ^ Z) . i2 &
p . i3 = (p ^ Z) . i3 &
p . i4 = (p ^ Z) . i4 &
p . i5 = (p ^ Z) . i5 &
p . i6 = (p ^ Z) . i6 )
by A5, Th4;
then
(
F1(
((p ^ Z) . i4),
((p ^ Z) . i5),
((p ^ Z) . i6))
= 1
* ((p ^ Z) . n) &
P1[
(p ^ Z) . i1,
(p ^ Z) . i2,1
* ((p ^ Z) . i3)] )
by A11, A12, AFINSQ_1:36;
then
(
p ^ Z in F &
p ^ Z in P )
;
then
p ^ Z in P /\ F
by XBOOLE_0:def 4;
hence
x in PFk
by A13, A11;
verum
end; hence
{ p where p is n -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 A7, XBOOLE_0:def 10;
verum end; end;
end;
A14:
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)
proof
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)
set M =
{ p where p is n -element XFinSequence of NAT : S2[p . i1,p . i2,p . i3,p . i4,p . i5,p . i6] } ;
per cases
( n = 0 or n <> 0 )
;
suppose A15:
n = 0
;
{ 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)
{ p where p is n -element XFinSequence of NAT : S2[p . i1,p . i2,p . i3,p . i4,p . i5,p . i6] } c= n -xtuples_of NAT
proof
let x be
object ;
TARSKI:def 3 ( not x in { p where p is n -element XFinSequence of NAT : S2[p . i1,p . i2,p . i3,p . i4,p . i5,p . i6] } or x in n -xtuples_of NAT )
assume
x in { p where p is n -element XFinSequence of NAT : S2[p . i1,p . i2,p . i3,p . i4,p . i5,p . i6] }
;
x in n -xtuples_of NAT
then
ex
p being
n -element XFinSequence of
NAT st
(
x = p &
S2[
p . i1,
p . i2,
p . i3,
p . i4,
p . i5,
p . i6] )
;
hence
x in n -xtuples_of NAT
by HILB10_2:def 5;
verum
end; 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 A15;
verum end; suppose A16:
n <> 0
;
{ 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)set n1 =
n + 1;
A17:
n < n + 1
by NAT_1:13;
then
n in Segm (n + 1)
by NAT_1:44;
then reconsider I1 =
i1,
I2 =
i2,
I3 =
i3,
I4 =
i4,
I5 =
i5,
I6 =
i6,
N =
n as
Element of
n + 1
by Th2;
defpred S3[
XFinSequence of
NAT ]
means P1[$1
. I1,$1
. I2,
(- 1) * ($1 . I3)];
reconsider P =
{ p where p is n + 1 -element XFinSequence of NAT : S3[p] } as
diophantine Subset of
((n + 1) -xtuples_of NAT) by A1;
reconsider F =
{ p where p is n + 1 -element XFinSequence of NAT : F1((p . I4),(p . I5),(p . I6)) = (- 1) * (p . N) } as
diophantine Subset of
((n + 1) -xtuples_of NAT) by A2;
reconsider PF =
P /\ F as
Subset of
((n + 1) -xtuples_of NAT) ;
reconsider PFk =
{ (p | n) where p is n + 1 -element XFinSequence of NAT : p in PF } as
diophantine Subset of
(n -xtuples_of NAT) by Th5, A17;
A18:
PFk c= { p where p is n -element XFinSequence of NAT : S2[p . i1,p . i2,p . i3,p . i4,p . i5,p . i6] }
proof
let x be
object ;
TARSKI:def 3 ( not x in PFk or x in { p where p is n -element XFinSequence of NAT : S2[p . i1,p . i2,p . i3,p . i4,p . i5,p . i6] } )
assume
x in PFk
;
x in { p where p is n -element XFinSequence of NAT : S2[p . i1,p . i2,p . i3,p . i4,p . i5,p . i6] }
then consider p being
n + 1
-element XFinSequence of
NAT such that A19:
(
x = p | n &
p in PF )
;
p in P
by A19, XBOOLE_0:def 4;
then A20:
ex
q being
n + 1
-element XFinSequence of
NAT st
(
p = q &
S3[
q] )
;
p in F
by A19, XBOOLE_0:def 4;
then A21:
ex
q being
n + 1
-element XFinSequence of
NAT st
(
p = q &
F1(
(q . I4),
(q . I5),
(q . I6))
= (- 1) * (q . N) )
;
len p = n + 1
by CARD_1:def 7;
then
len (p | n) = n
by A17, AFINSQ_1:54;
then reconsider pn =
p | n as
n -element XFinSequence of
NAT by CARD_1:def 7;
(
p . I1 = pn . I1 &
p . I2 = pn . I2 &
p . I3 = pn . I3 &
p . I4 = pn . I4 &
pn . I5 = p . I5 &
pn . i6 = p . I6 )
by A16, Th4;
hence
x in { p where p is n -element XFinSequence of NAT : S2[p . i1,p . i2,p . i3,p . i4,p . i5,p . i6] }
by A19, A20, A21;
verum
end;
{ p where p is n -element XFinSequence of NAT : S2[p . i1,p . i2,p . i3,p . i4,p . i5,p . i6] } c= PFk
proof
let x be
object ;
TARSKI:def 3 ( not x in { p where p is n -element XFinSequence of NAT : S2[p . i1,p . i2,p . i3,p . i4,p . i5,p . i6] } or x in PFk )
assume
x in { p where p is n -element XFinSequence of NAT : S2[p . i1,p . i2,p . i3,p . i4,p . i5,p . i6] }
;
x in PFk
then consider p being
n -element XFinSequence of
NAT such that A22:
(
x = p &
S2[
p . i1,
p . i2,
p . i3,
p . i4,
p . i5,
p . i6] )
;
reconsider FF =
- F1(
(p . i4),
(p . i5),
(p . i6)) as
Element of
NAT by A22, INT_1:3;
reconsider Z =
<%FF%> as 1
-element XFinSequence of
NAT ;
set pZ =
p ^ Z;
len p = n
by CARD_1:def 7;
then A23:
(
(p ^ Z) | n = p &
(p ^ Z) . n = FF )
by AFINSQ_1:57, AFINSQ_1:36;
then
(
p . i1 = (p ^ Z) . i1 &
p . i2 = (p ^ Z) . i2 &
p . i3 = (p ^ Z) . i3 &
p . i4 = (p ^ Z) . i4 &
p . i5 = (p ^ Z) . i5 &
p . i6 = (p ^ Z) . i6 )
by A16, Th4;
then
(
F1(
((p ^ Z) . i4),
((p ^ Z) . i5),
((p ^ Z) . i6))
= (- 1) * ((p ^ Z) . n) &
P1[
(p ^ Z) . i1,
(p ^ Z) . i2,
(- 1) * ((p ^ Z) . i3)] )
by A22, A23;
then
(
p ^ Z in F &
p ^ Z in P )
;
then
p ^ Z in P /\ F
by XBOOLE_0:def 4;
hence
x in PFk
by A23, A22;
verum
end; 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 A18, XBOOLE_0:def 10;
verum end; end;
end;
A24:
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)
proof
let n be
Nat;
for i1, i2, i3, i4 being Element of n holds { p where p is n -element XFinSequence of NAT : H1(p . i1,p . i2,p . i3) = p . i4 } is diophantine Subset of (n -xtuples_of NAT)let i1,
i2,
i3,
i4 be
Element of
n;
{ p where p is n -element XFinSequence of NAT : H1(p . i1,p . i2,p . i3) = p . i4 } is diophantine Subset of (n -xtuples_of NAT)
defpred S3[
XFinSequence of
NAT ]
means F1(
($1 . i1),
($1 . i2),
($1 . i3))
= 1
* ($1 . i4);
defpred S4[
XFinSequence of
NAT ]
means F1(
($1 . i1),
($1 . i2),
($1 . i3))
= (- 1) * ($1 . i4);
A25:
{ p where p is n -element XFinSequence of NAT : S3[p] } is
diophantine Subset of
(n -xtuples_of NAT)
by A2;
A26:
{ p where p is n -element XFinSequence of NAT : S4[p] } is
diophantine Subset of
(n -xtuples_of NAT)
by A2;
A27:
{ p where p is n -element XFinSequence of NAT : ( S3[p] or S4[p] ) } is
diophantine Subset of
(n -xtuples_of NAT)
from HILB10_3:sch 1(A25, A26);
defpred S5[
XFinSequence of
NAT ]
means (
S3[$1] or
S4[$1] );
defpred S6[
XFinSequence of
NAT ]
means H1($1
. i1,$1
. i2,$1
. i3)
= $1
. i4;
A28:
for
p being
n -element XFinSequence of
NAT holds
(
S5[
p] iff
S6[
p] )
proof
let p be
n -element XFinSequence of
NAT ;
( S5[p] iff S6[p] )
thus
(
S5[
p] implies
S6[
p] )
( S6[p] implies S5[p] )proof
assume A29:
S5[
p]
;
S6[p]
end;
assume A30:
S6[
p]
;
S5[p]
end;
{ 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(A28);
hence
{ p where p is n -element XFinSequence of NAT : H1(p . i1,p . i2,p . i3) = p . i4 } is
diophantine Subset of
(n -xtuples_of NAT)
by A27;
verum
end;
A31:
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(A3, A24);
A32:
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,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(A14, A24);
let n be Nat; for i1, i2, i3, i4, i5 being Element of n holds { p where p is n -element XFinSequence of NAT : P1[p . i1,p . i2,F1((p . i3),(p . i4),(p . i5))] } is diophantine Subset of (n -xtuples_of NAT)
let i1, i2, i3, i4, i5 be Element of n; { p where p is n -element XFinSequence of NAT : P1[p . i1,p . i2,F1((p . i3),(p . i4),(p . i5))] } is diophantine Subset of (n -xtuples_of NAT)
defpred S3[ XFinSequence of NAT ] means S1[$1 . i1,$1 . i2,H1($1 . i3,$1 . i4,$1 . i5),$1 . i3,$1 . i4,$1 . i5];
defpred S4[ XFinSequence of NAT ] means S2[$1 . i1,$1 . i2,H1($1 . i3,$1 . i4,$1 . i5),$1 . i3,$1 . i4,$1 . i5];
defpred S5[ XFinSequence of NAT ] means ( S3[$1] or S4[$1] );
A33:
{ p where p is n -element XFinSequence of NAT : S3[p] } is diophantine Subset of (n -xtuples_of NAT)
by A31;
A34:
{ p where p is n -element XFinSequence of NAT : S4[p] } is diophantine Subset of (n -xtuples_of NAT)
by A32;
A35:
{ p where p is n -element XFinSequence of NAT : ( S3[p] or S4[p] ) } is diophantine Subset of (n -xtuples_of NAT)
from HILB10_3:sch 1(A33, A34);
defpred S6[ XFinSequence of NAT ] means P1[$1 . i1,$1 . i2,F1(($1 . i3),($1 . i4),($1 . i5))];
A36:
for p being n -element XFinSequence of NAT holds
( S5[p] iff S6[p] )
proof
let p be
n -element XFinSequence of
NAT ;
( S5[p] iff S6[p] )
thus
(
S5[
p] implies
S6[
p] )
( S6[p] implies S5[p] )proof
assume A37:
(
S3[
p] or
S4[
p] )
;
S6[p]
end;
assume A39:
S6[
p]
;
S5[p]
end;
{ 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(A36);
hence
{ p where p is n -element XFinSequence of NAT : P1[p . i1,p . i2,F1((p . i3),(p . i4),(p . i5))] } is diophantine Subset of (n -xtuples_of NAT)
by A35; verum