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)),p . i3,p . i4,p . i5] } is diophantine Subset of (n -xtuples_of NAT)
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)),p . i3,p . i4,p . i5] } is diophantine Subset of (n -xtuples_of NAT)
set n1 = n + 1;
set T = { p where p is n -element XFinSequence of NAT : P1[p . i1,p . i2,F1((p . i3),(p . i4),(p . i5)),p . i3,p . i4,p . i5] } ;
per cases ( n = 0 or n <> 0 ) ;
suppose A3: n = 0 ; :: thesis: { p where p is n -element XFinSequence of NAT : P1[p . i1,p . i2,F1((p . i3),(p . i4),(p . i5)),p . i3,p . i4,p . i5] } is diophantine Subset of (n -xtuples_of NAT)
{ p where p is n -element XFinSequence of NAT : P1[p . i1,p . i2,F1((p . i3),(p . i4),(p . i5)),p . i3,p . i4,p . i5] } 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 : P1[p . i1,p . i2,F1((p . i3),(p . i4),(p . i5)),p . i3,p . i4,p . i5] } or x in n -xtuples_of NAT )
assume x in { p where p is n -element XFinSequence of NAT : P1[p . i1,p . i2,F1((p . i3),(p . i4),(p . i5)),p . i3,p . i4,p . i5] } ; :: thesis: x in n -xtuples_of NAT
then ex p being n -element XFinSequence of NAT st
( x = p & P1[p . i1,p . i2,F1((p . i3),(p . i4),(p . i5)),p . i3,p . i4,p . i5] ) ;
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 : P1[p . i1,p . i2,F1((p . i3),(p . i4),(p . i5)),p . i3,p . i4,p . i5] } is diophantine Subset of (n -xtuples_of NAT) by A3; :: thesis: verum
end;
suppose A4: n <> 0 ; :: thesis: { p where p is n -element XFinSequence of NAT : P1[p . i1,p . i2,F1((p . i3),(p . i4),(p . i5)),p . i3,p . i4,p . i5] } is diophantine Subset of (n -xtuples_of NAT)
A5: 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, N = n as Element of n + 1 by Th2;
reconsider P = { p where p is n + 1 -element XFinSequence of NAT : P1[p . I1,p . I2,p . N,p . I3,p . I4,p . I5] } 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 . I3),(p . I4),(p . I5)) = 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, A5;
A6: PFk c= { p where p is n -element XFinSequence of NAT : P1[p . i1,p . i2,F1((p . i3),(p . i4),(p . i5)),p . i3,p . i4,p . i5] }
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 : P1[p . i1,p . i2,F1((p . i3),(p . i4),(p . i5)),p . i3,p . i4,p . i5] } )
assume x in PFk ; :: thesis: x in { p where p is n -element XFinSequence of NAT : P1[p . i1,p . i2,F1((p . i3),(p . i4),(p . i5)),p . i3,p . i4,p . i5] }
then consider p being n + 1 -element XFinSequence of NAT such that
A7: ( x = p | n & p in PF ) ;
p in P by A7, XBOOLE_0:def 4;
then A8: ex q being n + 1 -element XFinSequence of NAT st
( p = q & P1[q . I1,q . I2,q . N,q . I3,q . I4,q . I5] ) ;
p in F by A7, XBOOLE_0:def 4;
then A9: ex q being n + 1 -element XFinSequence of NAT st
( p = q & F1((q . I3),(q . I4),(q . I5)) = q . N ) ;
len p = n + 1 by CARD_1:def 7;
then len (p | n) = n by A5, 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 ) by A4, Th4;
hence x in { p where p is n -element XFinSequence of NAT : P1[p . i1,p . i2,F1((p . i3),(p . i4),(p . i5)),p . i3,p . i4,p . i5] } by A8, A9, A7; :: thesis: verum
end;
{ p where p is n -element XFinSequence of NAT : P1[p . i1,p . i2,F1((p . i3),(p . i4),(p . i5)),p . i3,p . i4,p . i5] } 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 : P1[p . i1,p . i2,F1((p . i3),(p . i4),(p . i5)),p . i3,p . i4,p . i5] } or x in PFk )
assume x in { p where p is n -element XFinSequence of NAT : P1[p . i1,p . i2,F1((p . i3),(p . i4),(p . i5)),p . i3,p . i4,p . i5] } ; :: thesis: x in PFk
then consider p being n -element XFinSequence of NAT such that
A10: ( x = p & P1[p . i1,p . i2,F1((p . i3),(p . i4),(p . i5)),p . i3,p . i4,p . i5] ) ;
reconsider FF = F1((p . i3),(p . i4),(p . i5)) as Element of NAT by ORDINAL1:def 12;
reconsider Z = <%FF%> as 1 -element XFinSequence of NAT ;
set pZ = p ^ Z;
len p = n by CARD_1:def 7;
then A11: ( (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 ) by A4, Th4;
then ( p ^ Z in F & p ^ Z in P ) by A10, A11;
then p ^ Z in P /\ F by XBOOLE_0:def 4;
hence x in PFk by A11, A10; :: thesis: verum
end;
hence { p where p is n -element XFinSequence of NAT : P1[p . i1,p . i2,F1((p . i3),(p . i4),(p . i5)),p . i3,p . i4,p . i5] } is diophantine Subset of (n -xtuples_of NAT) by A6, XBOOLE_0:def 10; :: thesis: verum
end;
end;