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 ()
proof
let n be Nat; :: thesis: 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 ()
let i1, i2, i3, i4, i5, i6 be Element of n; :: thesis: { 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 ()
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 ; :: thesis: { 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 ()
{ 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 ; :: according to TARSKI:def 3 :: thesis: ( 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] } ; :: thesis:
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; :: thesis: 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 () by A4; :: thesis: verum
end;
suppose A5: n <> 0 ; :: thesis: { 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 ()
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 () by ;
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 ; :: according to TARSKI:def 3 :: thesis: ( 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 ; :: thesis: 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 ;
then A9: ex q being n + 1 -element XFinSequence of NAT st
( p = q & S3[q] ) ;
p in F by ;
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 ;
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 ;
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; :: thesis: 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 ; :: according to TARSKI:def 3 :: thesis: ( 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] } ; :: thesis: 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 ;
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 ;
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 ;
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 ;
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 ; :: thesis: 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 () by ; :: thesis: 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 ()
proof
let n be Nat; :: thesis: 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 ()
let i1, i2, i3, i4, i5, i6 be Element of n; :: thesis: { 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 ()
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 ; :: thesis: { 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 ()
{ 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 ; :: according to TARSKI:def 3 :: thesis: ( 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] } ; :: thesis:
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; :: thesis: 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 () by A15; :: thesis: verum
end;
suppose A16: n <> 0 ; :: thesis: { 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 ()
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 () by ;
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 ; :: according to TARSKI:def 3 :: thesis: ( 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 ; :: thesis: 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 ;
then A20: ex q being n + 1 -element XFinSequence of NAT st
( p = q & S3[q] ) ;
p in F by ;
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 ;
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 ;
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 ; :: thesis: 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 ; :: according to TARSKI:def 3 :: thesis: ( 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] } ; :: thesis: 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 ;
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 ;
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 ;
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 ;
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 ; :: thesis: 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 () by ; :: thesis: 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 ()
proof
let n be Nat; :: thesis: 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 ()
let i1, i2, i3, i4 be Element of n; :: thesis: { p where p is n -element XFinSequence of NAT : H1(p . i1,p . i2,p . i3) = p . i4 } is diophantine Subset of ()
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 () by A2;
A26: { p where p is n -element XFinSequence of NAT : S4[p] } is diophantine Subset of () by A2;
A27: { p where p is n -element XFinSequence of NAT : ( S3[p] or S4[p] ) } is diophantine Subset of () from 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 ; :: thesis: ( S5[p] iff S6[p] )
thus ( S5[p] implies S6[p] ) :: thesis: ( S6[p] implies S5[p] ) assume A30: S6[p] ; :: thesis: S5[p]
per cases ( F1((p . i1),(p . i2),(p . i3)) >= 0 or F1((p . i1),(p . i2),(p . i3)) < 0 ) ;
suppose F1((p . i1),(p . i2),(p . i3)) >= 0 ; :: thesis: S5[p]
end;
suppose F1((p . i1),(p . i2),(p . i3)) < 0 ; :: thesis: S5[p]
then H1(p . i1,p . i2,p . i3) = - F1((p . i1),(p . i2),(p . i3)) by ABSVALUE:def 1;
hence S5[p] by A30; :: thesis: verum
end;
end;
end;
{ p where p is n -element XFinSequence of NAT : S5[p] } = { q where q is n -element XFinSequence of NAT : S6[q] } from hence { p where p is n -element XFinSequence of NAT : H1(p . i1,p . i2,p . i3) = p . i4 } is diophantine Subset of () by A27; :: thesis: 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 () from 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 () from let n be Nat; :: thesis: 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 ()
let i1, i2, i3, i4, i5 be Element of n; :: thesis: { 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 ()
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 () by A31;
A34: { p where p is n -element XFinSequence of NAT : S4[p] } is diophantine Subset of () by A32;
A35: { p where p is n -element XFinSequence of NAT : ( S3[p] or S4[p] ) } is diophantine Subset of () from 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 ; :: thesis: ( S5[p] iff S6[p] )
thus ( S5[p] implies S6[p] ) :: thesis: ( S6[p] implies S5[p] )
proof end;
assume A39: S6[p] ; :: thesis: S5[p]
per cases ( F1((p . i3),(p . i4),(p . i5)) >= 0 or F1((p . i3),(p . i4),(p . i5)) < 0 ) ;
suppose F1((p . i3),(p . i4),(p . i5)) >= 0 ; :: thesis: S5[p]
end;
suppose A40: F1((p . i3),(p . i4),(p . i5)) < 0 ; :: thesis: S5[p]
then H1(p . i3,p . i4,p . i5) = - F1((p . i3),(p . i4),(p . i5)) by ABSVALUE:def 1;
hence S5[p] by A39, A40; :: thesis: verum
end;
end;
end;
{ p where p is n -element XFinSequence of NAT : S5[p] } = { q where q is n -element XFinSequence of NAT : S6[q] } from 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 () by A35; :: thesis: verum