let n be Nat; for i1, i2, i3 being Element of n holds { p where p is n -element XFinSequence of NAT : ( p . i1 = Py ((p . i2),(p . i3)) & p . i2 > 1 ) } is diophantine Subset of (n -xtuples_of NAT)
let i1, i2, i3 be Element of n; { p where p is n -element XFinSequence of NAT : ( p . i1 = Py ((p . i2),(p . i3)) & p . i2 > 1 ) } is diophantine Subset of (n -xtuples_of NAT)
set n9 = n + 9;
set WW = { p where p is n -element XFinSequence of NAT : ( p . i1 = Py ((p . i2),(p . i3)) & p . i2 > 1 ) } ;
{ p where p is n -element XFinSequence of NAT : ( p . i1 = Py ((p . i2),(p . i3)) & p . i2 > 1 ) } c= n -xtuples_of NAT
then reconsider WW = { p where p is n -element XFinSequence of NAT : ( p . i1 = Py ((p . i2),(p . i3)) & p . i2 > 1 ) } as Subset of (n -xtuples_of NAT) ;
per cases
( n = 0 or n <> 0 )
;
suppose A1:
n <> 0
;
{ p where p is n -element XFinSequence of NAT : ( p . i1 = Py ((p . i2),(p . i3)) & p . i2 > 1 ) } is diophantine Subset of (n -xtuples_of NAT)
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,
N5 =
n + 5,
N6 =
n + 6,
N7 =
n + 7,
N8 =
n + 8 as
Element of
n + 9
by Th2, Th3;
defpred S1[
XFinSequence of
NAT ]
means 1
* ($1 . I2) > (0 * ($1 . I1)) + 1;
A2:
{ p where p is n + 9 -element XFinSequence of NAT : S1[p] } is
diophantine Subset of
((n + 9) -xtuples_of NAT)
by Th7;
defpred S2[
XFinSequence of
NAT ]
means [(1 * ($1 . N)),(1 * ($1 . I1))] is
Pell's_solution of
((1 * ($1 . I2)) ^2) -' 1;
A3:
{ p where p is n + 9 -element XFinSequence of NAT : S2[p] } is
diophantine Subset of
((n + 9) -xtuples_of NAT)
by Th22;
defpred S3[
XFinSequence of
NAT ]
means [(1 * ($1 . N1)),(1 * ($1 . N2))] is
Pell's_solution of
((1 * ($1 . I2)) ^2) -' 1;
A4:
{ p where p is n + 9 -element XFinSequence of NAT : S3[p] } is
diophantine Subset of
((n + 9) -xtuples_of NAT)
by Th22;
defpred S4[
XFinSequence of
NAT ]
means 1
* ($1 . N2) >= (1 * ($1 . I1)) + 0;
A5:
{ p where p is n + 9 -element XFinSequence of NAT : S4[p] } is
diophantine Subset of
((n + 9) -xtuples_of NAT)
by Th8;
defpred S5[
XFinSequence of
NAT ]
means 1
* ($1 . N3) > (1 * ($1 . I1)) + 0;
A6:
{ p where p is n + 9 -element XFinSequence of NAT : S5[p] } is
diophantine Subset of
((n + 9) -xtuples_of NAT)
by Th7;
defpred S6[
XFinSequence of
NAT ]
means 1
* ($1 . I1) >= (1 * ($1 . I3)) + 0;
A7:
{ p where p is n + 9 -element XFinSequence of NAT : S6[p] } is
diophantine Subset of
((n + 9) -xtuples_of NAT)
by Th8;
defpred S7[
XFinSequence of
NAT ]
means [(1 * ($1 . N4)),(1 * ($1 . N5))] is
Pell's_solution of
((1 * ($1 . N3)) ^2) -' 1;
A8:
{ p where p is n + 9 -element XFinSequence of NAT : S7[p] } is
diophantine Subset of
((n + 9) -xtuples_of NAT)
by Th22;
defpred S8[
XFinSequence of
NAT ]
means 1
* ($1 . N5),1
* ($1 . I1) are_congruent_mod 1
* ($1 . N1);
A9:
{ p where p is n + 9 -element XFinSequence of NAT : S8[p] } is
diophantine Subset of
((n + 9) -xtuples_of NAT)
by Th21;
defpred S9[
XFinSequence of
NAT ]
means 1
* ($1 . N3),1
* ($1 . I2) are_congruent_mod 1
* ($1 . N1);
A10:
{ p where p is n + 9 -element XFinSequence of NAT : S9[p] } is
diophantine Subset of
((n + 9) -xtuples_of NAT)
by Th21;
defpred S10[
XFinSequence of
NAT ]
means 1
* ($1 . N5),1
* ($1 . I3) are_congruent_mod 1
* ($1 . N6);
A11:
{ p where p is n + 9 -element XFinSequence of NAT : S10[p] } is
diophantine Subset of
((n + 9) -xtuples_of NAT)
by Th21;
defpred S11[
XFinSequence of
NAT ]
means 1
* ($1 . N3),1
* ($1 . N8) are_congruent_mod 1
* ($1 . N6);
A12:
{ p where p is n + 9 -element XFinSequence of NAT : S11[p] } is
diophantine Subset of
((n + 9) -xtuples_of NAT)
by Th21;
defpred S12[
XFinSequence of
NAT ]
means 1
* ($1 . N2),
0 * ($1 . N3) are_congruent_mod 1
* ($1 . N7);
A13:
{ p where p is n + 9 -element XFinSequence of NAT : S12[p] } is
diophantine Subset of
((n + 9) -xtuples_of NAT)
by Th21;
defpred S13[
XFinSequence of
NAT ]
means 1
= $1
. N8;
A14:
{ p where p is n + 9 -element XFinSequence of NAT : S13[p] } is
diophantine Subset of
((n + 9) -xtuples_of NAT)
by Th14;
defpred S14[
XFinSequence of
NAT ]
means 2
* ($1 . I1) = $1
. N6;
A15:
{ p where p is n + 9 -element XFinSequence of NAT : S14[p] } is
diophantine Subset of
((n + 9) -xtuples_of NAT)
by Th12;
defpred S15[
XFinSequence of
NAT ]
means (1 * ($1 . I1)) * ($1 . I1) = 1
* ($1 . N7);
A16:
{ p where p is n + 9 -element XFinSequence of NAT : S15[p] } is
diophantine Subset of
((n + 9) -xtuples_of NAT)
by Th9;
defpred S16[
XFinSequence of
NAT ]
means (
S1[$1] &
S2[$1] );
defpred S17[
XFinSequence of
NAT ]
means (
S3[$1] &
S4[$1] );
defpred S18[
XFinSequence of
NAT ]
means (
S5[$1] &
S6[$1] );
defpred S19[
XFinSequence of
NAT ]
means (
S7[$1] &
S8[$1] );
defpred S20[
XFinSequence of
NAT ]
means (
S9[$1] &
S10[$1] );
defpred S21[
XFinSequence of
NAT ]
means (
S11[$1] &
S12[$1] );
defpred S22[
XFinSequence of
NAT ]
means (
S13[$1] &
S14[$1] );
{ p where p is n + 9 -element XFinSequence of NAT : ( S1[p] & S2[p] ) } is
diophantine Subset of
((n + 9) -xtuples_of NAT)
from HILB10_3:sch 3(A2, A3);
then A17:
{ p where p is n + 9 -element XFinSequence of NAT : S16[p] } is
diophantine Subset of
((n + 9) -xtuples_of NAT)
;
{ p where p is n + 9 -element XFinSequence of NAT : ( S3[p] & S4[p] ) } is
diophantine Subset of
((n + 9) -xtuples_of NAT)
from HILB10_3:sch 3(A4, A5);
then A18:
{ p where p is n + 9 -element XFinSequence of NAT : S17[p] } is
diophantine Subset of
((n + 9) -xtuples_of NAT)
;
{ p where p is n + 9 -element XFinSequence of NAT : ( S5[p] & S6[p] ) } is
diophantine Subset of
((n + 9) -xtuples_of NAT)
from HILB10_3:sch 3(A6, A7);
then A19:
{ p where p is n + 9 -element XFinSequence of NAT : S18[p] } is
diophantine Subset of
((n + 9) -xtuples_of NAT)
;
{ p where p is n + 9 -element XFinSequence of NAT : ( S7[p] & S8[p] ) } is
diophantine Subset of
((n + 9) -xtuples_of NAT)
from HILB10_3:sch 3(A8, A9);
then A20:
{ p where p is n + 9 -element XFinSequence of NAT : S19[p] } is
diophantine Subset of
((n + 9) -xtuples_of NAT)
;
{ p where p is n + 9 -element XFinSequence of NAT : ( S9[p] & S10[p] ) } is
diophantine Subset of
((n + 9) -xtuples_of NAT)
from HILB10_3:sch 3(A10, A11);
then A21:
{ p where p is n + 9 -element XFinSequence of NAT : S20[p] } is
diophantine Subset of
((n + 9) -xtuples_of NAT)
;
{ p where p is n + 9 -element XFinSequence of NAT : ( S11[p] & S12[p] ) } is
diophantine Subset of
((n + 9) -xtuples_of NAT)
from HILB10_3:sch 3(A12, A13);
then A22:
{ p where p is n + 9 -element XFinSequence of NAT : S21[p] } is
diophantine Subset of
((n + 9) -xtuples_of NAT)
;
{ p where p is n + 9 -element XFinSequence of NAT : ( S13[p] & S14[p] ) } is
diophantine Subset of
((n + 9) -xtuples_of NAT)
from HILB10_3:sch 3(A14, A15);
then A23:
{ p where p is n + 9 -element XFinSequence of NAT : S22[p] } is
diophantine Subset of
((n + 9) -xtuples_of NAT)
;
defpred S23[
XFinSequence of
NAT ]
means (
S16[$1] &
S17[$1] );
defpred S24[
XFinSequence of
NAT ]
means (
S18[$1] &
S19[$1] );
defpred S25[
XFinSequence of
NAT ]
means (
S20[$1] &
S21[$1] );
defpred S26[
XFinSequence of
NAT ]
means (
S22[$1] &
S15[$1] );
{ p where p is n + 9 -element XFinSequence of NAT : ( S16[p] & S17[p] ) } is
diophantine Subset of
((n + 9) -xtuples_of NAT)
from HILB10_3:sch 3(A17, A18);
then A24:
{ p where p is n + 9 -element XFinSequence of NAT : S23[p] } is
diophantine Subset of
((n + 9) -xtuples_of NAT)
;
{ p where p is n + 9 -element XFinSequence of NAT : ( S18[p] & S19[p] ) } is
diophantine Subset of
((n + 9) -xtuples_of NAT)
from HILB10_3:sch 3(A19, A20);
then A25:
{ p where p is n + 9 -element XFinSequence of NAT : S24[p] } is
diophantine Subset of
((n + 9) -xtuples_of NAT)
;
{ p where p is n + 9 -element XFinSequence of NAT : ( S20[p] & S21[p] ) } is
diophantine Subset of
((n + 9) -xtuples_of NAT)
from HILB10_3:sch 3(A21, A22);
then A26:
{ p where p is n + 9 -element XFinSequence of NAT : S25[p] } is
diophantine Subset of
((n + 9) -xtuples_of NAT)
;
{ p where p is n + 9 -element XFinSequence of NAT : ( S22[p] & S15[p] ) } is
diophantine Subset of
((n + 9) -xtuples_of NAT)
from HILB10_3:sch 3(A23, A16);
then A27:
{ p where p is n + 9 -element XFinSequence of NAT : S26[p] } is
diophantine Subset of
((n + 9) -xtuples_of NAT)
;
defpred S27[
XFinSequence of
NAT ]
means (
S23[$1] &
S24[$1] );
defpred S28[
XFinSequence of
NAT ]
means (
S25[$1] &
S26[$1] );
{ p where p is n + 9 -element XFinSequence of NAT : ( S23[p] & S24[p] ) } is
diophantine Subset of
((n + 9) -xtuples_of NAT)
from HILB10_3:sch 3(A24, A25);
then A28:
{ p where p is n + 9 -element XFinSequence of NAT : S27[p] } is
diophantine Subset of
((n + 9) -xtuples_of NAT)
;
{ p where p is n + 9 -element XFinSequence of NAT : ( S25[p] & S26[p] ) } is
diophantine Subset of
((n + 9) -xtuples_of NAT)
from HILB10_3:sch 3(A26, A27);
then A29:
{ p where p is n + 9 -element XFinSequence of NAT : S28[p] } is
diophantine Subset of
((n + 9) -xtuples_of NAT)
;
defpred S29[
XFinSequence of
NAT ]
means (
S27[$1] &
S28[$1] );
A30:
{ p where p is n + 9 -element XFinSequence of NAT : ( S27[p] & S28[p] ) } is
diophantine Subset of
((n + 9) -xtuples_of NAT)
from HILB10_3:sch 3(A28, A29);
set DD =
{ p where p is n + 9 -element XFinSequence of NAT : S29[p] } ;
set DDR =
{ (p | n) where p is n + 9 -element XFinSequence of NAT : p in { p where p is n + 9 -element XFinSequence of NAT : S29[p] } } ;
A31:
{ (p | n) where p is n + 9 -element XFinSequence of NAT : p in { p where p is n + 9 -element XFinSequence of NAT : S29[p] } } is
diophantine Subset of
(n -xtuples_of NAT)
by Th5, A30, NAT_1:11;
A32:
{ (p | n) where p is n + 9 -element XFinSequence of NAT : p in { p where p is n + 9 -element XFinSequence of NAT : S29[p] } } c= WW
proof
let o be
object ;
TARSKI:def 3 ( not o in { (p | n) where p is n + 9 -element XFinSequence of NAT : p in { p where p is n + 9 -element XFinSequence of NAT : S29[p] } } or o in WW )
assume A33:
o in { (p | n) where p is n + 9 -element XFinSequence of NAT : p in { p where p is n + 9 -element XFinSequence of NAT : S29[p] } }
;
o in WW
consider p being
n + 9
-element XFinSequence of
NAT such that A34:
(
o = p | n &
p in { p where p is n + 9 -element XFinSequence of NAT : S29[p] } )
by A33;
consider q being
n + 9
-element XFinSequence of
NAT such that A35:
(
p = q &
S29[
q] )
by A34;
(
len p = n + 9 &
n + 9
>= n )
by CARD_1:def 7, NAT_1:11;
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;
A36:
(
pn . I3 = p . i3 &
pn . I2 = p . i2 &
(p | n) . I1 = p . i1 )
by A1, Th4;
( 1
* (p . I2) > (0 * (p . I1)) + 1 &
[(1 * (p . N)),(1 * (p . I1))] is
Pell's_solution of
((1 * (p . I2)) ^2) -' 1 &
[(1 * (p . N1)),(1 * (p . N2))] is
Pell's_solution of
((1 * (p . I2)) ^2) -' 1 & 1
* (p . N2) >= (1 * (p . I1)) + 0 & 1
* (p . N3) > (1 * (p . I1)) + 0 & 1
* (p . I1) >= (1 * (p . I3)) + 0 &
[(1 * (p . N4)),(1 * (p . N5))] is
Pell's_solution of
((1 * (p . N3)) ^2) -' 1 & 1
* (p . N5),1
* (p . I1) are_congruent_mod 1
* (p . N1) & 1
* (p . N3),1
* (p . I2) are_congruent_mod 1
* (p . N1) & 1
* (p . N5),1
* (p . I3) are_congruent_mod 1
* (2 * (p . I1)) & 1
* (p . N3),1
* 1
are_congruent_mod 1
* (2 * (p . I1)) & 1
* (p . N2),
0 * (p . N3) are_congruent_mod (p . I1) ^2 )
by SQUARE_1:def 1, A35;
then
(
pn . i1 = Py (
(pn . i2),
(pn . i3)) &
pn . i2 > 1 )
by HILB10_1:38, A36;
hence
o in WW
by A34;
verum
end;
WW c= { (p | n) where p is n + 9 -element XFinSequence of NAT : p in { p where p is n + 9 -element XFinSequence of NAT : S29[p] } }
proof
let o be
object ;
TARSKI:def 3 ( not o in WW or o in { (p | n) where p is n + 9 -element XFinSequence of NAT : p in { p where p is n + 9 -element XFinSequence of NAT : S29[p] } } )
assume A37:
o in WW
;
o in { (p | n) where p is n + 9 -element XFinSequence of NAT : p in { p where p is n + 9 -element XFinSequence of NAT : S29[p] } }
consider p being
n -element XFinSequence of
NAT such that A38:
(
o = p &
p . i1 = Py (
(p . i2),
(p . i3)) &
p . i2 > 1 )
by A37;
set y =
p . i1;
set a =
p . i2;
set z =
p . i3;
consider x,
x1,
y1,
A,
x2,
y2 being
Nat such that A39:
(
p . i2 > 1 &
[x,(p . i1)] is
Pell's_solution of
((p . i2) ^2) -' 1 &
[x1,y1] is
Pell's_solution of
((p . i2) ^2) -' 1 &
y1 >= p . i1 &
A > p . i1 &
p . i1 >= p . i3 &
[x2,y2] is
Pell's_solution of
(A ^2) -' 1 &
y2,
p . i1 are_congruent_mod x1 &
A,
p . i2 are_congruent_mod x1 &
y2,
p . i3 are_congruent_mod 2
* (p . i1) &
A,1
are_congruent_mod 2
* (p . i1) &
y1,
0 are_congruent_mod (p . i1) ^2 )
by A38, HILB10_1:38;
reconsider x =
x,
x1 =
x1,
y1 =
y1,
A =
A,
x2 =
x2,
y2 =
y2 as
Element of
NAT by ORDINAL1:def 12;
reconsider 2y = 2
* (p . i1) as
Element of
NAT ;
reconsider yy =
(p . i1) * (p . i1) as
Element of
NAT ;
reconsider Z = 1 as
Element of
NAT ;
set Y =
(((((((<%x%> ^ <%x1%>) ^ <%y1%>) ^ <%A%>) ^ <%x2%>) ^ <%y2%>) ^ <%2y%>) ^ <%yy%>) ^ <%Z%>;
set PY =
p ^ ((((((((<%x%> ^ <%x1%>) ^ <%y1%>) ^ <%A%>) ^ <%x2%>) ^ <%y2%>) ^ <%2y%>) ^ <%yy%>) ^ <%Z%>);
A40:
(
len p = n &
len ((((((((<%x%> ^ <%x1%>) ^ <%y1%>) ^ <%A%>) ^ <%x2%>) ^ <%y2%>) ^ <%2y%>) ^ <%yy%>) ^ <%Z%>) = 9 )
by CARD_1:def 7;
A41:
(p ^ ((((((((<%x%> ^ <%x1%>) ^ <%y1%>) ^ <%A%>) ^ <%x2%>) ^ <%y2%>) ^ <%2y%>) ^ <%yy%>) ^ <%Z%>)) | n = p
by A40, AFINSQ_1:57;
0 in dom ((((((((<%x%> ^ <%x1%>) ^ <%y1%>) ^ <%A%>) ^ <%x2%>) ^ <%y2%>) ^ <%2y%>) ^ <%yy%>) ^ <%Z%>)
by A40, AFINSQ_1:66;
then A42:
(p ^ ((((((((<%x%> ^ <%x1%>) ^ <%y1%>) ^ <%A%>) ^ <%x2%>) ^ <%y2%>) ^ <%2y%>) ^ <%yy%>) ^ <%Z%>)) . (n + 0) =
((((((((<%x%> ^ <%x1%>) ^ <%y1%>) ^ <%A%>) ^ <%x2%>) ^ <%y2%>) ^ <%2y%>) ^ <%yy%>) ^ <%Z%>) . 0
by A40, AFINSQ_1:def 3
.=
x
by AFINSQ_1:50
;
1
in dom ((((((((<%x%> ^ <%x1%>) ^ <%y1%>) ^ <%A%>) ^ <%x2%>) ^ <%y2%>) ^ <%2y%>) ^ <%yy%>) ^ <%Z%>)
by A40, AFINSQ_1:66;
then A43:
(p ^ ((((((((<%x%> ^ <%x1%>) ^ <%y1%>) ^ <%A%>) ^ <%x2%>) ^ <%y2%>) ^ <%2y%>) ^ <%yy%>) ^ <%Z%>)) . (n + 1) =
((((((((<%x%> ^ <%x1%>) ^ <%y1%>) ^ <%A%>) ^ <%x2%>) ^ <%y2%>) ^ <%2y%>) ^ <%yy%>) ^ <%Z%>) . 1
by A40, AFINSQ_1:def 3
.=
x1
by AFINSQ_1:50
;
2
in dom ((((((((<%x%> ^ <%x1%>) ^ <%y1%>) ^ <%A%>) ^ <%x2%>) ^ <%y2%>) ^ <%2y%>) ^ <%yy%>) ^ <%Z%>)
by A40, AFINSQ_1:66;
then A44:
(p ^ ((((((((<%x%> ^ <%x1%>) ^ <%y1%>) ^ <%A%>) ^ <%x2%>) ^ <%y2%>) ^ <%2y%>) ^ <%yy%>) ^ <%Z%>)) . (n + 2) =
((((((((<%x%> ^ <%x1%>) ^ <%y1%>) ^ <%A%>) ^ <%x2%>) ^ <%y2%>) ^ <%2y%>) ^ <%yy%>) ^ <%Z%>) . 2
by A40, AFINSQ_1:def 3
.=
y1
by AFINSQ_1:50
;
3
in dom ((((((((<%x%> ^ <%x1%>) ^ <%y1%>) ^ <%A%>) ^ <%x2%>) ^ <%y2%>) ^ <%2y%>) ^ <%yy%>) ^ <%Z%>)
by A40, AFINSQ_1:66;
then A45:
(p ^ ((((((((<%x%> ^ <%x1%>) ^ <%y1%>) ^ <%A%>) ^ <%x2%>) ^ <%y2%>) ^ <%2y%>) ^ <%yy%>) ^ <%Z%>)) . (n + 3) =
((((((((<%x%> ^ <%x1%>) ^ <%y1%>) ^ <%A%>) ^ <%x2%>) ^ <%y2%>) ^ <%2y%>) ^ <%yy%>) ^ <%Z%>) . 3
by A40, AFINSQ_1:def 3
.=
A
by AFINSQ_1:50
;
4
in dom ((((((((<%x%> ^ <%x1%>) ^ <%y1%>) ^ <%A%>) ^ <%x2%>) ^ <%y2%>) ^ <%2y%>) ^ <%yy%>) ^ <%Z%>)
by A40, AFINSQ_1:66;
then A46:
(p ^ ((((((((<%x%> ^ <%x1%>) ^ <%y1%>) ^ <%A%>) ^ <%x2%>) ^ <%y2%>) ^ <%2y%>) ^ <%yy%>) ^ <%Z%>)) . (n + 4) =
((((((((<%x%> ^ <%x1%>) ^ <%y1%>) ^ <%A%>) ^ <%x2%>) ^ <%y2%>) ^ <%2y%>) ^ <%yy%>) ^ <%Z%>) . 4
by A40, AFINSQ_1:def 3
.=
x2
by AFINSQ_1:50
;
5
in dom ((((((((<%x%> ^ <%x1%>) ^ <%y1%>) ^ <%A%>) ^ <%x2%>) ^ <%y2%>) ^ <%2y%>) ^ <%yy%>) ^ <%Z%>)
by A40, AFINSQ_1:66;
then A47:
(p ^ ((((((((<%x%> ^ <%x1%>) ^ <%y1%>) ^ <%A%>) ^ <%x2%>) ^ <%y2%>) ^ <%2y%>) ^ <%yy%>) ^ <%Z%>)) . (n + 5) =
((((((((<%x%> ^ <%x1%>) ^ <%y1%>) ^ <%A%>) ^ <%x2%>) ^ <%y2%>) ^ <%2y%>) ^ <%yy%>) ^ <%Z%>) . 5
by A40, AFINSQ_1:def 3
.=
y2
by AFINSQ_1:50
;
6
in dom ((((((((<%x%> ^ <%x1%>) ^ <%y1%>) ^ <%A%>) ^ <%x2%>) ^ <%y2%>) ^ <%2y%>) ^ <%yy%>) ^ <%Z%>)
by A40, AFINSQ_1:66;
then (p ^ ((((((((<%x%> ^ <%x1%>) ^ <%y1%>) ^ <%A%>) ^ <%x2%>) ^ <%y2%>) ^ <%2y%>) ^ <%yy%>) ^ <%Z%>)) . (n + 6) =
((((((((<%x%> ^ <%x1%>) ^ <%y1%>) ^ <%A%>) ^ <%x2%>) ^ <%y2%>) ^ <%2y%>) ^ <%yy%>) ^ <%Z%>) . 6
by A40, AFINSQ_1:def 3
.=
2y
by AFINSQ_1:50
;
then A48:
(
(p ^ ((((((((<%x%> ^ <%x1%>) ^ <%y1%>) ^ <%A%>) ^ <%x2%>) ^ <%y2%>) ^ <%2y%>) ^ <%yy%>) ^ <%Z%>)) . N6 = 2
* (p . i1) & 2
* (p . i1) = 2
* ((p ^ ((((((((<%x%> ^ <%x1%>) ^ <%y1%>) ^ <%A%>) ^ <%x2%>) ^ <%y2%>) ^ <%2y%>) ^ <%yy%>) ^ <%Z%>)) . I1) )
by A41, A1, Th4;
7
in dom ((((((((<%x%> ^ <%x1%>) ^ <%y1%>) ^ <%A%>) ^ <%x2%>) ^ <%y2%>) ^ <%2y%>) ^ <%yy%>) ^ <%Z%>)
by A40, AFINSQ_1:66;
then A49:
(p ^ ((((((((<%x%> ^ <%x1%>) ^ <%y1%>) ^ <%A%>) ^ <%x2%>) ^ <%y2%>) ^ <%2y%>) ^ <%yy%>) ^ <%Z%>)) . (n + 7) =
((((((((<%x%> ^ <%x1%>) ^ <%y1%>) ^ <%A%>) ^ <%x2%>) ^ <%y2%>) ^ <%2y%>) ^ <%yy%>) ^ <%Z%>) . 7
by A40, AFINSQ_1:def 3
.=
yy
by AFINSQ_1:50
;
8
in dom ((((((((<%x%> ^ <%x1%>) ^ <%y1%>) ^ <%A%>) ^ <%x2%>) ^ <%y2%>) ^ <%2y%>) ^ <%yy%>) ^ <%Z%>)
by A40, AFINSQ_1:66;
then A50:
(p ^ ((((((((<%x%> ^ <%x1%>) ^ <%y1%>) ^ <%A%>) ^ <%x2%>) ^ <%y2%>) ^ <%2y%>) ^ <%yy%>) ^ <%Z%>)) . (n + 8) =
((((((((<%x%> ^ <%x1%>) ^ <%y1%>) ^ <%A%>) ^ <%x2%>) ^ <%y2%>) ^ <%2y%>) ^ <%yy%>) ^ <%Z%>) . 8
by A40, AFINSQ_1:def 3
.=
Z
by AFINSQ_1:50
;
S29[
p ^ ((((((((<%x%> ^ <%x1%>) ^ <%y1%>) ^ <%A%>) ^ <%x2%>) ^ <%y2%>) ^ <%2y%>) ^ <%yy%>) ^ <%Z%>)]
by SQUARE_1:def 1, A39, A42, A45, A46, A47, A1, Th4, A43, A41, A50, A48, A49, A44;
then
p ^ ((((((((<%x%> ^ <%x1%>) ^ <%y1%>) ^ <%A%>) ^ <%x2%>) ^ <%y2%>) ^ <%2y%>) ^ <%yy%>) ^ <%Z%>) in { p where p is n + 9 -element XFinSequence of NAT : S29[p] }
;
hence
o in { (p | n) where p is n + 9 -element XFinSequence of NAT : p in { p where p is n + 9 -element XFinSequence of NAT : S29[p] } }
by A38, A41;
verum
end; hence
{ p where p is n -element XFinSequence of NAT : ( p . i1 = Py ((p . i2),(p . i3)) & p . i2 > 1 ) } is
diophantine Subset of
(n -xtuples_of NAT)
by A31, A32, XBOOLE_0:def 10;
verum end;