let n be Nat; :: thesis: for a, b, c being Integer
for i1, i2, i3 being Element of n holds { p where p is n -element XFinSequence of NAT : [(a * (p . i1)),(b * (p . i2))] is Pell's_solution of ((c * (p . i3)) ^2) -' 1 } is diophantine Subset of ()

let a, b, c be Integer; :: thesis: for i1, i2, i3 being Element of n holds { p where p is n -element XFinSequence of NAT : [(a * (p . i1)),(b * (p . i2))] is Pell's_solution of ((c * (p . i3)) ^2) -' 1 } is diophantine Subset of ()
let i1, i2, i3 be Element of n; :: thesis: { p where p is n -element XFinSequence of NAT : [(a * (p . i1)),(b * (p . i2))] is Pell's_solution of ((c * (p . i3)) ^2) -' 1 } is diophantine Subset of ()
set n5 = n + 5;
set WW = { p where p is n -element XFinSequence of NAT : [(a * (p . i1)),(b * (p . i2))] is Pell's_solution of ((c * (p . i3)) ^2) -' 1 } ;
{ p where p is n -element XFinSequence of NAT : [(a * (p . i1)),(b * (p . i2))] is Pell's_solution of ((c * (p . i3)) ^2) -' 1 } c= n -xtuples_of NAT
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in { p where p is n -element XFinSequence of NAT : [(a * (p . i1)),(b * (p . i2))] is Pell's_solution of ((c * (p . i3)) ^2) -' 1 } or y in n -xtuples_of NAT )
assume y in { p where p is n -element XFinSequence of NAT : [(a * (p . i1)),(b * (p . i2))] is Pell's_solution of ((c * (p . i3)) ^2) -' 1 } ; :: thesis:
then ex p being n -element XFinSequence of NAT st
( y = p & [(a * (p . i1)),(b * (p . i2))] is Pell's_solution of ((c * (p . i3)) ^2) -' 1 ) ;
hence y in n -xtuples_of NAT by HILB10_2:def 5; :: thesis: verum
end;
then reconsider WW = { p where p is n -element XFinSequence of NAT : [(a * (p . i1)),(b * (p . i2))] is Pell's_solution of ((c * (p . i3)) ^2) -' 1 } as Subset of () ;
per cases ( n = 0 or n <> 0 ) ;
suppose n = 0 ; :: thesis: { p where p is n -element XFinSequence of NAT : [(a * (p . i1)),(b * (p . i2))] is Pell's_solution of ((c * (p . i3)) ^2) -' 1 } is diophantine Subset of ()
then WW is diophantine Subset of () ;
hence { p where p is n -element XFinSequence of NAT : [(a * (p . i1)),(b * (p . i2))] is Pell's_solution of ((c * (p . i3)) ^2) -' 1 } is diophantine Subset of () ; :: thesis: verum
end;
suppose A1: n <> 0 ; :: thesis: { p where p is n -element XFinSequence of NAT : [(a * (p . i1)),(b * (p . i2))] is Pell's_solution of ((c * (p . i3)) ^2) -' 1 } is diophantine Subset of ()
n = n + 0 ;
then reconsider N = n, I1 = i1, I2 = i2, I3 = i3, N1 = n + 1, N2 = n + 2, N3 = n + 3, N4 = n + 4 as Element of n + 5 by ;
defpred S1[ XFinSequence of NAT ] means 1 * (\$1 . N) = ((a ^2) * (\$1 . I1)) * (\$1 . I1);
A2: { p where p is n + 5 -element XFinSequence of NAT : S1[p] } is diophantine Subset of ((n + 5) -xtuples_of NAT) by Th9;
defpred S2[ XFinSequence of NAT ] means 1 * (\$1 . N1) = ((c ^2) * (\$1 . I3)) * (\$1 . I3);
A3: { p where p is n + 5 -element XFinSequence of NAT : S2[p] } is diophantine Subset of ((n + 5) -xtuples_of NAT) by Th9;
defpred S3[ XFinSequence of NAT ] means 1 * (\$1 . N2) = (1 * (\$1 . N1)) -' 1;
A4: { p where p is n + 5 -element XFinSequence of NAT : S3[p] } is diophantine Subset of ((n + 5) -xtuples_of NAT) by Th20;
defpred S4[ XFinSequence of NAT ] means 1 * (\$1 . N3) = ((b ^2) * (\$1 . I2)) * (\$1 . I2);
A5: { p where p is n + 5 -element XFinSequence of NAT : S4[p] } is diophantine Subset of ((n + 5) -xtuples_of NAT) by Th9;
defpred S5[ XFinSequence of NAT ] means 1 * (\$1 . N4) = (1 * (\$1 . N2)) * (\$1 . N3);
A6: { p where p is n + 5 -element XFinSequence of NAT : S5[p] } is diophantine Subset of ((n + 5) -xtuples_of NAT) by Th9;
defpred S6[ XFinSequence of NAT ] means 1 * (\$1 . N) = (1 * (\$1 . N4)) + 1;
A7: { p where p is n + 5 -element XFinSequence of NAT : S6[p] } is diophantine Subset of ((n + 5) -xtuples_of NAT) by Th6;
defpred S7[ XFinSequence of NAT ] means ( S1[\$1] & S2[\$1] );
defpred S8[ XFinSequence of NAT ] means ( S7[\$1] & S3[\$1] );
defpred S9[ XFinSequence of NAT ] means ( S8[\$1] & S4[\$1] );
defpred S10[ XFinSequence of NAT ] means ( S9[\$1] & S5[\$1] );
defpred S11[ XFinSequence of NAT ] means ( S10[\$1] & S6[\$1] );
{ p where p is n + 5 -element XFinSequence of NAT : ( S1[p] & S2[p] ) } is diophantine Subset of ((n + 5) -xtuples_of NAT) from then A8: { p where p is n + 5 -element XFinSequence of NAT : S7[p] } is diophantine Subset of ((n + 5) -xtuples_of NAT) ;
{ p where p is n + 5 -element XFinSequence of NAT : ( S7[p] & S3[p] ) } is diophantine Subset of ((n + 5) -xtuples_of NAT) from then A9: { p where p is n + 5 -element XFinSequence of NAT : S8[p] } is diophantine Subset of ((n + 5) -xtuples_of NAT) ;
{ p where p is n + 5 -element XFinSequence of NAT : ( S8[p] & S4[p] ) } is diophantine Subset of ((n + 5) -xtuples_of NAT) from then A10: { p where p is n + 5 -element XFinSequence of NAT : S9[p] } is diophantine Subset of ((n + 5) -xtuples_of NAT) ;
{ p where p is n + 5 -element XFinSequence of NAT : ( S9[p] & S5[p] ) } is diophantine Subset of ((n + 5) -xtuples_of NAT) from then A11: { p where p is n + 5 -element XFinSequence of NAT : S10[p] } is diophantine Subset of ((n + 5) -xtuples_of NAT) ;
A12: { p where p is n + 5 -element XFinSequence of NAT : ( S10[p] & S6[p] ) } is diophantine Subset of ((n + 5) -xtuples_of NAT) from set DD = { p where p is n + 5 -element XFinSequence of NAT : S11[p] } ;
set DDR = { (p | n) where p is n + 5 -element XFinSequence of NAT : p in { p where p is n + 5 -element XFinSequence of NAT : S11[p] } } ;
A13: { (p | n) where p is n + 5 -element XFinSequence of NAT : p in { p where p is n + 5 -element XFinSequence of NAT : S11[p] } } is diophantine Subset of () by ;
A14: { (p | n) where p is n + 5 -element XFinSequence of NAT : p in { p where p is n + 5 -element XFinSequence of NAT : S11[p] } } c= WW
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { (p | n) where p is n + 5 -element XFinSequence of NAT : p in { p where p is n + 5 -element XFinSequence of NAT : S11[p] } } or x in WW )
assume A15: x in { (p | n) where p is n + 5 -element XFinSequence of NAT : p in { p where p is n + 5 -element XFinSequence of NAT : S11[p] } } ; :: thesis: x in WW
consider p being n + 5 -element XFinSequence of NAT such that
A16: ( x = p | n & p in { p where p is n + 5 -element XFinSequence of NAT : S11[p] } ) by A15;
consider q being n + 5 -element XFinSequence of NAT such that
A17: ( p = q & S11[q] ) by A16;
( len p = n + 5 & n + 5 >= n ) by ;
then len (p | n) = n by AFINSQ_1:54;
then reconsider pn = p | n as n -element XFinSequence of NAT by CARD_1:def 7;
A18: ( ((b ^2) * (p . I2)) * (p . I2) = (b ^2) * ((p . I2) * (p . I2)) & (b ^2) * ((p . I2) * (p . I2)) = (b ^2) * ((p . I2) ^2) & (b ^2) * ((p . I2) ^2) = (b * (p . I2)) ^2 ) by ;
A19: ( ((a ^2) * (p . I1)) * (p . I1) = (a ^2) * ((p . I1) * (p . I1)) & (a ^2) * ((p . I1) * (p . I1)) = (a ^2) * ((p . I1) ^2) & (a ^2) * ((p . I1) ^2) = (a * (p . I1)) ^2 ) by ;
A20: ( ((c ^2) * (p . I3)) * (p . I3) = (c ^2) * ((p . I3) * (p . I3)) & (c ^2) * ((p . I3) * (p . I3)) = (c ^2) * ((p . I3) ^2) & (c ^2) * ((p . I3) ^2) = (c * (p . I3)) ^2 ) by ;
A21: ( (p | n) . I3 = p . i3 & (p | n) . I2 = p . i2 & (p | n) . I1 = p . i1 ) by ;
(a * (pn . i1)) ^2 = ((((c * (pn . i3)) ^2) -' 1) * ((b * (pn . i2)) ^2)) + 1 by A17, A18, A19, A20, A21;
then ((a * (pn . i1)) ^2) - ((((c * (pn . i3)) ^2) -' 1) * ((b * (pn . i2)) ^2)) = 1 ;
then [(a * (pn . i1)),(b * (pn . i2))] is Pell's_solution of ((c * (pn . i3)) ^2) -' 1 by Lm1;
hence x in WW by A16; :: thesis: verum
end;
WW c= { (p | n) where p is n + 5 -element XFinSequence of NAT : p in { p where p is n + 5 -element XFinSequence of NAT : S11[p] } }
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in WW or x in { (p | n) where p is n + 5 -element XFinSequence of NAT : p in { p where p is n + 5 -element XFinSequence of NAT : S11[p] } } )
assume A22: x in WW ; :: thesis: x in { (p | n) where p is n + 5 -element XFinSequence of NAT : p in { p where p is n + 5 -element XFinSequence of NAT : S11[p] } }
consider p being n -element XFinSequence of NAT such that
A23: ( x = p & [(a * (p . i1)),(b * (p . i2))] is Pell's_solution of ((c * (p . i3)) ^2) -' 1 ) by A22;
A24: ( (a * (p . i1)) ^2 = (a ^2) * ((p . i1) ^2) & (a ^2) * ((p . i1) ^2) = (a ^2) * ((p . i1) * (p . i1)) & (a ^2) * ((p . i1) * (p . i1)) = ((a ^2) * (p . i1)) * (p . i1) ) by ;
A25: ( (b * (p . i2)) ^2 = (b ^2) * ((p . i2) ^2) & (b ^2) * ((p . i2) ^2) = (b ^2) * ((p . i2) * (p . i2)) & (b ^2) * ((p . i2) * (p . i2)) = ((b ^2) * (p . i2)) * (p . i2) ) by ;
A26: ( (c * (p . i3)) ^2 = (c ^2) * ((p . i3) ^2) & (c ^2) * ((p . i3) ^2) = (c ^2) * ((p . i3) * (p . i3)) & (c ^2) * ((p . i3) * (p . i3)) = ((c ^2) * (p . i3)) * (p . i3) ) by ;
set y1 = ((a ^2) * (p . i1)) * (p . i1);
set y2 = ((c ^2) * (p . i3)) * (p . i3);
set y3 = (1 * (((c ^2) * (p . i3)) * (p . i3))) -' 1;
set y4 = ((b ^2) * (p . i2)) * (p . i2);
set y5 = (1 * ((1 * (((c ^2) * (p . i3)) * (p . i3))) -' 1)) * (((b ^2) * (p . i2)) * (p . i2));
reconsider y1 = ((a ^2) * (p . i1)) * (p . i1), y2 = ((c ^2) * (p . i3)) * (p . i3), y3 = (1 * (((c ^2) * (p . i3)) * (p . i3))) -' 1, y4 = ((b ^2) * (p . i2)) * (p . i2), y5 = (1 * ((1 * (((c ^2) * (p . i3)) * (p . i3))) -' 1)) * (((b ^2) * (p . i2)) * (p . i2)) as Element of NAT by ORDINAL1:def 12;
set Y = (((<%y1%> ^ <%y2%>) ^ <%y3%>) ^ <%y4%>) ^ <%y5%>;
set PY = p ^ ((((<%y1%> ^ <%y2%>) ^ <%y3%>) ^ <%y4%>) ^ <%y5%>);
A27: ( len p = n & len ((((<%y1%> ^ <%y2%>) ^ <%y3%>) ^ <%y4%>) ^ <%y5%>) = 5 ) by CARD_1:def 7;
A28: (p ^ ((((<%y1%> ^ <%y2%>) ^ <%y3%>) ^ <%y4%>) ^ <%y5%>)) | n = p by ;
A29: (p ^ ((((<%y1%> ^ <%y2%>) ^ <%y3%>) ^ <%y4%>) ^ <%y5%>)) . i1 = p . i1 by A28, A1, Th4;
A30: (p ^ ((((<%y1%> ^ <%y2%>) ^ <%y3%>) ^ <%y4%>) ^ <%y5%>)) . i2 = ((p ^ ((((<%y1%> ^ <%y2%>) ^ <%y3%>) ^ <%y4%>) ^ <%y5%>)) | n) . i2 by
.= p . i2 by ;
A31: (p ^ ((((<%y1%> ^ <%y2%>) ^ <%y3%>) ^ <%y4%>) ^ <%y5%>)) . i3 = ((p ^ ((((<%y1%> ^ <%y2%>) ^ <%y3%>) ^ <%y4%>) ^ <%y5%>)) | n) . i3 by
.= p . i3 by ;
0 in dom ((((<%y1%> ^ <%y2%>) ^ <%y3%>) ^ <%y4%>) ^ <%y5%>) by ;
then A32: (p ^ ((((<%y1%> ^ <%y2%>) ^ <%y3%>) ^ <%y4%>) ^ <%y5%>)) . (n + 0) = ((((<%y1%> ^ <%y2%>) ^ <%y3%>) ^ <%y4%>) ^ <%y5%>) . 0 by
.= y1 by AFINSQ_1:46 ;
1 in dom ((((<%y1%> ^ <%y2%>) ^ <%y3%>) ^ <%y4%>) ^ <%y5%>) by ;
then A33: (p ^ ((((<%y1%> ^ <%y2%>) ^ <%y3%>) ^ <%y4%>) ^ <%y5%>)) . (n + 1) = ((((<%y1%> ^ <%y2%>) ^ <%y3%>) ^ <%y4%>) ^ <%y5%>) . 1 by
.= y2 by AFINSQ_1:46 ;
2 in dom ((((<%y1%> ^ <%y2%>) ^ <%y3%>) ^ <%y4%>) ^ <%y5%>) by ;
then A34: (p ^ ((((<%y1%> ^ <%y2%>) ^ <%y3%>) ^ <%y4%>) ^ <%y5%>)) . (n + 2) = ((((<%y1%> ^ <%y2%>) ^ <%y3%>) ^ <%y4%>) ^ <%y5%>) . 2 by
.= y3 by AFINSQ_1:46 ;
3 in dom ((((<%y1%> ^ <%y2%>) ^ <%y3%>) ^ <%y4%>) ^ <%y5%>) by ;
then A35: (p ^ ((((<%y1%> ^ <%y2%>) ^ <%y3%>) ^ <%y4%>) ^ <%y5%>)) . (n + 3) = ((((<%y1%> ^ <%y2%>) ^ <%y3%>) ^ <%y4%>) ^ <%y5%>) . 3 by
.= y4 by AFINSQ_1:46 ;
4 in dom ((((<%y1%> ^ <%y2%>) ^ <%y3%>) ^ <%y4%>) ^ <%y5%>) by ;
then A36: (p ^ ((((<%y1%> ^ <%y2%>) ^ <%y3%>) ^ <%y4%>) ^ <%y5%>)) . (n + 4) = ((((<%y1%> ^ <%y2%>) ^ <%y3%>) ^ <%y4%>) ^ <%y5%>) . 4 by
.= y5 by AFINSQ_1:46 ;
y1 - y5 = 1 by A23, Lm1, A24, A25, A26;
then y1 = y5 + 1 ;
then S11[p ^ ((((<%y1%> ^ <%y2%>) ^ <%y3%>) ^ <%y4%>) ^ <%y5%>)] by A32, A31, A33, A29, A34, A35, A30, A36;
then p ^ ((((<%y1%> ^ <%y2%>) ^ <%y3%>) ^ <%y4%>) ^ <%y5%>) in { p where p is n + 5 -element XFinSequence of NAT : S11[p] } ;
hence x in { (p | n) where p is n + 5 -element XFinSequence of NAT : p in { p where p is n + 5 -element XFinSequence of NAT : S11[p] } } by ; :: thesis: verum
end;
hence { p where p is n -element XFinSequence of NAT : [(a * (p . i1)),(b * (p . i2))] is Pell's_solution of ((c * (p . i3)) ^2) -' 1 } is diophantine Subset of () by ; :: thesis: verum
end;
end;