let n be Nat; 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 (n -xtuples_of NAT)
let a, b, c be 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 (n -xtuples_of NAT)
let i1, i2, i3 be Element of n; { 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 -xtuples_of NAT)
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
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 (n -xtuples_of NAT) ;
per cases
( n = 0 or n <> 0 )
;
suppose A1:
n <> 0
;
{ 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 -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 as
Element of
n + 5
by Th2, Th3;
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 HILB10_3:sch 3(A2, A3);
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 HILB10_3:sch 3(A8, A4);
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 HILB10_3:sch 3(A9, A5);
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 HILB10_3:sch 3(A10, A6);
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 HILB10_3:sch 3(A11, A7);
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
(n -xtuples_of NAT)
by NAT_1:11, Th5, A12;
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 ;
TARSKI:def 3 ( 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] } }
;
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 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;
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 SQUARE_1:def 1, SQUARE_1:9;
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 SQUARE_1:def 1, SQUARE_1:9;
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 SQUARE_1:def 1, SQUARE_1:9;
A21:
(
(p | n) . I3 = p . i3 &
(p | n) . I2 = p . i2 &
(p | n) . I1 = p . i1 )
by A1, Th4;
(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;
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 ;
TARSKI:def 3 ( 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
;
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 SQUARE_1:def 1, SQUARE_1:9;
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 SQUARE_1:def 1, SQUARE_1:9;
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 SQUARE_1:def 1, SQUARE_1:9;
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 A27, AFINSQ_1:57;
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 A1, Th4
.=
p . i2
by A27, AFINSQ_1:57
;
A31:
(p ^ ((((<%y1%> ^ <%y2%>) ^ <%y3%>) ^ <%y4%>) ^ <%y5%>)) . i3 =
((p ^ ((((<%y1%> ^ <%y2%>) ^ <%y3%>) ^ <%y4%>) ^ <%y5%>)) | n) . i3
by A1, Th4
.=
p . i3
by A27, AFINSQ_1:57
;
0 in dom ((((<%y1%> ^ <%y2%>) ^ <%y3%>) ^ <%y4%>) ^ <%y5%>)
by A27, AFINSQ_1:66;
then A32:
(p ^ ((((<%y1%> ^ <%y2%>) ^ <%y3%>) ^ <%y4%>) ^ <%y5%>)) . (n + 0) =
((((<%y1%> ^ <%y2%>) ^ <%y3%>) ^ <%y4%>) ^ <%y5%>) . 0
by A27, AFINSQ_1:def 3
.=
y1
by AFINSQ_1:46
;
1
in dom ((((<%y1%> ^ <%y2%>) ^ <%y3%>) ^ <%y4%>) ^ <%y5%>)
by A27, AFINSQ_1:66;
then A33:
(p ^ ((((<%y1%> ^ <%y2%>) ^ <%y3%>) ^ <%y4%>) ^ <%y5%>)) . (n + 1) =
((((<%y1%> ^ <%y2%>) ^ <%y3%>) ^ <%y4%>) ^ <%y5%>) . 1
by A27, AFINSQ_1:def 3
.=
y2
by AFINSQ_1:46
;
2
in dom ((((<%y1%> ^ <%y2%>) ^ <%y3%>) ^ <%y4%>) ^ <%y5%>)
by A27, AFINSQ_1:66;
then A34:
(p ^ ((((<%y1%> ^ <%y2%>) ^ <%y3%>) ^ <%y4%>) ^ <%y5%>)) . (n + 2) =
((((<%y1%> ^ <%y2%>) ^ <%y3%>) ^ <%y4%>) ^ <%y5%>) . 2
by A27, AFINSQ_1:def 3
.=
y3
by AFINSQ_1:46
;
3
in dom ((((<%y1%> ^ <%y2%>) ^ <%y3%>) ^ <%y4%>) ^ <%y5%>)
by A27, AFINSQ_1:66;
then A35:
(p ^ ((((<%y1%> ^ <%y2%>) ^ <%y3%>) ^ <%y4%>) ^ <%y5%>)) . (n + 3) =
((((<%y1%> ^ <%y2%>) ^ <%y3%>) ^ <%y4%>) ^ <%y5%>) . 3
by A27, AFINSQ_1:def 3
.=
y4
by AFINSQ_1:46
;
4
in dom ((((<%y1%> ^ <%y2%>) ^ <%y3%>) ^ <%y4%>) ^ <%y5%>)
by A27, AFINSQ_1:66;
then A36:
(p ^ ((((<%y1%> ^ <%y2%>) ^ <%y3%>) ^ <%y4%>) ^ <%y5%>)) . (n + 4) =
((((<%y1%> ^ <%y2%>) ^ <%y3%>) ^ <%y4%>) ^ <%y5%>) . 4
by A27, AFINSQ_1:def 3
.=
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 A23, A28;
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
(n -xtuples_of NAT)
by A13, A14, XBOOLE_0:def 10;
verum end;