let n be Nat; for i1, i2, i3 being Element of n holds { p where p is n -element XFinSequence of NAT : p . i2 = (p . i1) |^ (p . i3) } 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 . i2 = (p . i1) |^ (p . i3) } is diophantine Subset of (n -xtuples_of NAT)
set n7 = n + 7;
set WW = { p where p is n -element XFinSequence of NAT : p . i2 = (p . i1) |^ (p . i3) } ;
{ p where p is n -element XFinSequence of NAT : p . i2 = (p . i1) |^ (p . i3) } c= n -xtuples_of NAT
then reconsider WW = { p where p is n -element XFinSequence of NAT : p . i2 = (p . i1) |^ (p . i3) } 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 . i2 = (p . i1) |^ (p . i3) } 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 as
Element of
n + 7
by Th2, Th3;
defpred S1[
XFinSequence of
NAT ]
means $1
. I1 = 0 ;
A2:
{ p where p is n + 7 -element XFinSequence of NAT : S1[p] } is
diophantine Subset of
((n + 7) -xtuples_of NAT)
by Th14;
defpred S2[
XFinSequence of
NAT ]
means $1
. I1 = 1;
A3:
{ p where p is n + 7 -element XFinSequence of NAT : S2[p] } is
diophantine Subset of
((n + 7) -xtuples_of NAT)
by Th14;
defpred S3[
XFinSequence of
NAT ]
means 1
* ($1 . I1) > (0 * ($1 . I2)) + 1;
A4:
{ p where p is n + 7 -element XFinSequence of NAT : S3[p] } is
diophantine Subset of
((n + 7) -xtuples_of NAT)
by Th7;
defpred S4[
XFinSequence of
NAT ]
means $1
. I2 = 0 ;
A5:
{ p where p is n + 7 -element XFinSequence of NAT : S4[p] } is
diophantine Subset of
((n + 7) -xtuples_of NAT)
by Th14;
defpred S5[
XFinSequence of
NAT ]
means $1
. I2 = 1;
A6:
{ p where p is n + 7 -element XFinSequence of NAT : S5[p] } is
diophantine Subset of
((n + 7) -xtuples_of NAT)
by Th14;
defpred S6[
XFinSequence of
NAT ]
means $1
. I3 = 0 ;
A7:
{ p where p is n + 7 -element XFinSequence of NAT : S6[p] } is
diophantine Subset of
((n + 7) -xtuples_of NAT)
by Th14;
defpred S7[
XFinSequence of
NAT ]
means 1
* ($1 . I3) > (0 * ($1 . I1)) + 0;
A8:
{ p where p is n + 7 -element XFinSequence of NAT : S7[p] } is
diophantine Subset of
((n + 7) -xtuples_of NAT)
by Th7;
defpred S8[
XFinSequence of
NAT ]
means 1
* ($1 . N4) = (1 * ($1 . I3)) + 1;
A9:
{ p where p is n + 7 -element XFinSequence of NAT : S8[p] } is
diophantine Subset of
((n + 7) -xtuples_of NAT)
by Th6;
defpred S9[
XFinSequence of
NAT ]
means 1
* ($1 . N5) = (1 * ($1 . N3)) * ($1 . I1);
A10:
{ p where p is n + 7 -element XFinSequence of NAT : S9[p] } is
diophantine Subset of
((n + 7) -xtuples_of NAT)
by Th9;
defpred S10[
XFinSequence of
NAT ]
means ( $1
. N = Py (
($1 . I1),
($1 . N4)) & $1
. I1 > 1 );
A11:
{ p where p is n + 7 -element XFinSequence of NAT : S10[p] } is
diophantine Subset of
((n + 7) -xtuples_of NAT)
by Th23;
defpred S11[
XFinSequence of
NAT ]
means 1
* ($1 . N3) > (2 * ($1 . I3)) * ($1 . N);
A12:
{ p where p is n + 7 -element XFinSequence of NAT : S11[p] } is
diophantine Subset of
((n + 7) -xtuples_of NAT)
by Th17;
defpred S12[
XFinSequence of
NAT ]
means ( $1
. N1 = Py (
($1 . N3),
($1 . N4)) & $1
. N3 > 1 );
A13:
{ p where p is n + 7 -element XFinSequence of NAT : S12[p] } is
diophantine Subset of
((n + 7) -xtuples_of NAT)
by Th23;
defpred S13[
XFinSequence of
NAT ]
means ( $1
. N2 = Py (
($1 . N5),
($1 . N4)) & $1
. N5 > 1 );
A14:
{ p where p is n + 7 -element XFinSequence of NAT : S13[p] } is
diophantine Subset of
((n + 7) -xtuples_of NAT)
by Th23;
defpred S14[
XFinSequence of
NAT ]
means 1
* ($1 . N6) = (1 * ($1 . I2)) * ($1 . N1);
A15:
{ p where p is n + 7 -element XFinSequence of NAT : S14[p] } is
diophantine Subset of
((n + 7) -xtuples_of NAT)
by Th9;
defpred S15[
XFinSequence of
NAT ]
means 1
* ($1 . N6) >= (1 * ($1 . N2)) + 0;
A16:
{ p where p is n + 7 -element XFinSequence of NAT : S15[p] } is
diophantine Subset of
((n + 7) -xtuples_of NAT)
by Th8;
defpred S16[
XFinSequence of
NAT ]
means 2
* ($1 . N6) < (1 * ($1 . N1)) + (2 * ($1 . N2));
A17:
{ p where p is n + 7 -element XFinSequence of NAT : S16[p] } is
diophantine Subset of
((n + 7) -xtuples_of NAT)
by Th18;
defpred S17[
XFinSequence of
NAT ]
means 1
* ($1 . N2) >= (1 * ($1 . N6)) + 0;
A18:
{ p where p is n + 7 -element XFinSequence of NAT : S17[p] } is
diophantine Subset of
((n + 7) -xtuples_of NAT)
by Th8;
defpred S18[
XFinSequence of
NAT ]
means (- 2) * ($1 . N6) < (1 * ($1 . N1)) + ((- 2) * ($1 . N2));
A19:
{ p where p is n + 7 -element XFinSequence of NAT : S18[p] } is
diophantine Subset of
((n + 7) -xtuples_of NAT)
by Th18;
defpred S19[
XFinSequence of
NAT ]
means (
S5[$1] &
S6[$1] );
defpred S20[
XFinSequence of
NAT ]
means (
S1[$1] &
S4[$1] );
defpred S21[
XFinSequence of
NAT ]
means (
S20[$1] &
S7[$1] );
defpred S22[
XFinSequence of
NAT ]
means (
S2[$1] &
S5[$1] );
defpred S23[
XFinSequence of
NAT ]
means (
S22[$1] &
S7[$1] );
defpred S24[
XFinSequence of
NAT ]
means (
S3[$1] &
S7[$1] );
defpred S25[
XFinSequence of
NAT ]
means (
S15[$1] &
S16[$1] );
defpred S26[
XFinSequence of
NAT ]
means (
S17[$1] &
S18[$1] );
{ p where p is n + 7 -element XFinSequence of NAT : ( S5[p] & S6[p] ) } is
diophantine Subset of
((n + 7) -xtuples_of NAT)
from HILB10_3:sch 3(A6, A7);
then A20:
{ p where p is n + 7 -element XFinSequence of NAT : S19[p] } is
diophantine Subset of
((n + 7) -xtuples_of NAT)
;
{ p where p is n + 7 -element XFinSequence of NAT : ( S1[p] & S4[p] ) } is
diophantine Subset of
((n + 7) -xtuples_of NAT)
from HILB10_3:sch 3(A2, A5);
then A21:
{ p where p is n + 7 -element XFinSequence of NAT : S20[p] } is
diophantine Subset of
((n + 7) -xtuples_of NAT)
;
{ p where p is n + 7 -element XFinSequence of NAT : ( S20[p] & S7[p] ) } is
diophantine Subset of
((n + 7) -xtuples_of NAT)
from HILB10_3:sch 3(A21, A8);
then A22:
{ p where p is n + 7 -element XFinSequence of NAT : S21[p] } is
diophantine Subset of
((n + 7) -xtuples_of NAT)
;
{ p where p is n + 7 -element XFinSequence of NAT : ( S2[p] & S5[p] ) } is
diophantine Subset of
((n + 7) -xtuples_of NAT)
from HILB10_3:sch 3(A3, A6);
then A23:
{ p where p is n + 7 -element XFinSequence of NAT : S22[p] } is
diophantine Subset of
((n + 7) -xtuples_of NAT)
;
{ p where p is n + 7 -element XFinSequence of NAT : ( S22[p] & S7[p] ) } is
diophantine Subset of
((n + 7) -xtuples_of NAT)
from HILB10_3:sch 3(A23, A8);
then A24:
{ p where p is n + 7 -element XFinSequence of NAT : S23[p] } is
diophantine Subset of
((n + 7) -xtuples_of NAT)
;
{ p where p is n + 7 -element XFinSequence of NAT : ( S3[p] & S7[p] ) } is
diophantine Subset of
((n + 7) -xtuples_of NAT)
from HILB10_3:sch 3(A4, A8);
then A25:
{ p where p is n + 7 -element XFinSequence of NAT : S24[p] } is
diophantine Subset of
((n + 7) -xtuples_of NAT)
;
{ p where p is n + 7 -element XFinSequence of NAT : ( S15[p] & S16[p] ) } is
diophantine Subset of
((n + 7) -xtuples_of NAT)
from HILB10_3:sch 3(A16, A17);
then A26:
{ p where p is n + 7 -element XFinSequence of NAT : S25[p] } is
diophantine Subset of
((n + 7) -xtuples_of NAT)
;
{ p where p is n + 7 -element XFinSequence of NAT : ( S17[p] & S18[p] ) } is
diophantine Subset of
((n + 7) -xtuples_of NAT)
from HILB10_3:sch 3(A18, A19);
then A27:
{ p where p is n + 7 -element XFinSequence of NAT : S26[p] } is
diophantine Subset of
((n + 7) -xtuples_of NAT)
;
defpred S27[
XFinSequence of
NAT ]
means (
S25[$1] or
S26[$1] );
{ p where p is n + 7 -element XFinSequence of NAT : ( S25[p] or S26[p] ) } is
diophantine Subset of
((n + 7) -xtuples_of NAT)
from HILB10_3:sch 1(A26, A27);
then A28:
{ p where p is n + 7 -element XFinSequence of NAT : S27[p] } is
diophantine Subset of
((n + 7) -xtuples_of NAT)
;
defpred S28[
XFinSequence of
NAT ]
means (
S19[$1] or
S21[$1] );
{ p where p is n + 7 -element XFinSequence of NAT : ( S19[p] or S21[p] ) } is
diophantine Subset of
((n + 7) -xtuples_of NAT)
from HILB10_3:sch 1(A20, A22);
then A29:
{ p where p is n + 7 -element XFinSequence of NAT : S28[p] } is
diophantine Subset of
((n + 7) -xtuples_of NAT)
;
defpred S29[
XFinSequence of
NAT ]
means (
S28[$1] or
S23[$1] );
{ p where p is n + 7 -element XFinSequence of NAT : ( S28[p] or S23[p] ) } is
diophantine Subset of
((n + 7) -xtuples_of NAT)
from HILB10_3:sch 1(A29, A24);
then A30:
{ p where p is n + 7 -element XFinSequence of NAT : S29[p] } is
diophantine Subset of
((n + 7) -xtuples_of NAT)
;
defpred S30[
XFinSequence of
NAT ]
means (
S8[$1] &
S9[$1] );
defpred S31[
XFinSequence of
NAT ]
means (
S10[$1] &
S11[$1] );
defpred S32[
XFinSequence of
NAT ]
means (
S31[$1] &
S12[$1] );
defpred S33[
XFinSequence of
NAT ]
means (
S32[$1] &
S13[$1] );
defpred S34[
XFinSequence of
NAT ]
means (
S33[$1] &
S27[$1] );
defpred S35[
XFinSequence of
NAT ]
means (
S24[$1] &
S34[$1] );
defpred S36[
XFinSequence of
NAT ]
means (
S35[$1] &
S30[$1] );
defpred S37[
XFinSequence of
NAT ]
means (
S36[$1] &
S14[$1] );
{ p where p is n + 7 -element XFinSequence of NAT : ( S8[p] & S9[p] ) } is
diophantine Subset of
((n + 7) -xtuples_of NAT)
from HILB10_3:sch 3(A9, A10);
then A31:
{ p where p is n + 7 -element XFinSequence of NAT : S30[p] } is
diophantine Subset of
((n + 7) -xtuples_of NAT)
;
{ p where p is n + 7 -element XFinSequence of NAT : ( S10[p] & S11[p] ) } is
diophantine Subset of
((n + 7) -xtuples_of NAT)
from HILB10_3:sch 3(A11, A12);
then A32:
{ p where p is n + 7 -element XFinSequence of NAT : S31[p] } is
diophantine Subset of
((n + 7) -xtuples_of NAT)
;
{ p where p is n + 7 -element XFinSequence of NAT : ( S31[p] & S12[p] ) } is
diophantine Subset of
((n + 7) -xtuples_of NAT)
from HILB10_3:sch 3(A32, A13);
then A33:
{ p where p is n + 7 -element XFinSequence of NAT : S32[p] } is
diophantine Subset of
((n + 7) -xtuples_of NAT)
;
{ p where p is n + 7 -element XFinSequence of NAT : ( S32[p] & S13[p] ) } is
diophantine Subset of
((n + 7) -xtuples_of NAT)
from HILB10_3:sch 3(A33, A14);
then A34:
{ p where p is n + 7 -element XFinSequence of NAT : S33[p] } is
diophantine Subset of
((n + 7) -xtuples_of NAT)
;
{ p where p is n + 7 -element XFinSequence of NAT : ( S33[p] & S27[p] ) } is
diophantine Subset of
((n + 7) -xtuples_of NAT)
from HILB10_3:sch 3(A34, A28);
then A35:
{ p where p is n + 7 -element XFinSequence of NAT : S34[p] } is
diophantine Subset of
((n + 7) -xtuples_of NAT)
;
{ p where p is n + 7 -element XFinSequence of NAT : ( S24[p] & S34[p] ) } is
diophantine Subset of
((n + 7) -xtuples_of NAT)
from HILB10_3:sch 3(A25, A35);
then A36:
{ p where p is n + 7 -element XFinSequence of NAT : S35[p] } is
diophantine Subset of
((n + 7) -xtuples_of NAT)
;
{ p where p is n + 7 -element XFinSequence of NAT : ( S35[p] & S30[p] ) } is
diophantine Subset of
((n + 7) -xtuples_of NAT)
from HILB10_3:sch 3(A36, A31);
then A37:
{ p where p is n + 7 -element XFinSequence of NAT : S36[p] } is
diophantine Subset of
((n + 7) -xtuples_of NAT)
;
{ p where p is n + 7 -element XFinSequence of NAT : ( S36[p] & S14[p] ) } is
diophantine Subset of
((n + 7) -xtuples_of NAT)
from HILB10_3:sch 3(A37, A15);
then A38:
{ p where p is n + 7 -element XFinSequence of NAT : S37[p] } is
diophantine Subset of
((n + 7) -xtuples_of NAT)
;
defpred S38[
XFinSequence of
NAT ]
means (
S29[$1] or
S37[$1] );
A39:
{ p where p is n + 7 -element XFinSequence of NAT : ( S29[p] or S37[p] ) } is
diophantine Subset of
((n + 7) -xtuples_of NAT)
from HILB10_3:sch 1(A30, A38);
set DD =
{ p where p is n + 7 -element XFinSequence of NAT : S38[p] } ;
set DDR =
{ (p | n) where p is n + 7 -element XFinSequence of NAT : p in { p where p is n + 7 -element XFinSequence of NAT : S38[p] } } ;
A40:
{ (p | n) where p is n + 7 -element XFinSequence of NAT : p in { p where p is n + 7 -element XFinSequence of NAT : S38[p] } } is
diophantine Subset of
(n -xtuples_of NAT)
by Th5, A39, NAT_1:11;
A41:
{ (p | n) where p is n + 7 -element XFinSequence of NAT : p in { p where p is n + 7 -element XFinSequence of NAT : S38[p] } } c= WW
proof
let o be
object ;
TARSKI:def 3 ( not o in { (p | n) where p is n + 7 -element XFinSequence of NAT : p in { p where p is n + 7 -element XFinSequence of NAT : S38[p] } } or o in WW )
assume A42:
o in { (p | n) where p is n + 7 -element XFinSequence of NAT : p in { p where p is n + 7 -element XFinSequence of NAT : S38[p] } }
;
o in WW
consider p being
n + 7
-element XFinSequence of
NAT such that A43:
(
o = p | n &
p in { p where p is n + 7 -element XFinSequence of NAT : S38[p] } )
by A42;
consider q being
n + 7
-element XFinSequence of
NAT such that A44:
(
p = q &
S38[
q] )
by A43;
(
len p = n + 7 &
n + 7
>= 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;
set x =
pn . i1;
set y =
pn . i2;
set z =
pn . i3;
set y1 =
p . N;
set y2 =
p . N1;
set y3 =
p . N2;
set K =
p . N3;
A45:
(
pn . i1 = p . i1 &
pn . i2 = p . i2 &
pn . i3 = p . i3 )
by A1, Th4;
( (
pn . i2 = 1 &
pn . i3 = 0 ) or (
pn . i1 = 0 &
pn . i2 = 0 &
pn . i3 > 0 ) or (
pn . i1 = 1 &
pn . i2 = 1 &
pn . i3 > 0 ) or (
pn . i1 > 1 &
pn . i3 > 0 & ex
y1,
y2,
y3,
K being
Nat st
(
y1 = Py (
(pn . i1),
((pn . i3) + 1)) &
K > (2 * (pn . i3)) * y1 &
y2 = Py (
K,
((pn . i3) + 1)) &
y3 = Py (
(K * (pn . i1)),
((pn . i3) + 1)) & ( (
0 <= (pn . i2) - (y3 / y2) &
(pn . i2) - (y3 / y2) < 1
/ 2 ) or (
0 <= (y3 / y2) - (pn . i2) &
(y3 / y2) - (pn . i2) < 1
/ 2 ) ) ) ) )
proof
per cases
( ( pn . i2 = 1 & pn . i3 = 0 ) or ( pn . i1 = 0 & pn . i2 = 0 & pn . i3 > 0 ) or ( pn . i1 = 1 & pn . i2 = 1 & pn . i3 > 0 ) or ( 1 * (pn . i1) > (0 * (pn . i2)) + 1 & 1 * (pn . i3) > (0 * (pn . i1)) + 0 & p . N = Py ((pn . i1),((pn . i3) + 1)) & 1 * (p . N3) > (2 * (pn . i3)) * (p . N) & p . N1 = Py ((p . N3),((pn . i3) + 1)) & 1 * (p . N2) = Py (((p . N3) * (pn . i1)),((pn . i3) + 1)) & ( ( (1 * (pn . i2)) * (p . N1) >= (1 * (p . N2)) + 0 & (2 * (pn . i2)) * (p . N1) < (1 * (p . N1)) + (2 * (p . N2)) ) or ( 1 * (p . N2) >= (pn . i2) * (p . N1) & ((- 2) * (pn . i2)) * (p . N1) < (1 * (p . N1)) + ((- 2) * (p . N2)) ) ) ) )
by A44, A45;
suppose
(
pn . i2 = 1 &
pn . i3 = 0 )
;
( ( pn . i2 = 1 & pn . i3 = 0 ) or ( pn . i1 = 0 & pn . i2 = 0 & pn . i3 > 0 ) or ( pn . i1 = 1 & pn . i2 = 1 & pn . i3 > 0 ) or ( pn . i1 > 1 & pn . i3 > 0 & ex y1, y2, y3, K being Nat st
( y1 = Py ((pn . i1),((pn . i3) + 1)) & K > (2 * (pn . i3)) * y1 & y2 = Py (K,((pn . i3) + 1)) & y3 = Py ((K * (pn . i1)),((pn . i3) + 1)) & ( ( 0 <= (pn . i2) - (y3 / y2) & (pn . i2) - (y3 / y2) < 1 / 2 ) or ( 0 <= (y3 / y2) - (pn . i2) & (y3 / y2) - (pn . i2) < 1 / 2 ) ) ) ) )hence
( (
pn . i2 = 1 &
pn . i3 = 0 ) or (
pn . i1 = 0 &
pn . i2 = 0 &
pn . i3 > 0 ) or (
pn . i1 = 1 &
pn . i2 = 1 &
pn . i3 > 0 ) or (
pn . i1 > 1 &
pn . i3 > 0 & ex
y1,
y2,
y3,
K being
Nat st
(
y1 = Py (
(pn . i1),
((pn . i3) + 1)) &
K > (2 * (pn . i3)) * y1 &
y2 = Py (
K,
((pn . i3) + 1)) &
y3 = Py (
(K * (pn . i1)),
((pn . i3) + 1)) & ( (
0 <= (pn . i2) - (y3 / y2) &
(pn . i2) - (y3 / y2) < 1
/ 2 ) or (
0 <= (y3 / y2) - (pn . i2) &
(y3 / y2) - (pn . i2) < 1
/ 2 ) ) ) ) )
;
verum end; suppose
(
pn . i1 = 0 &
pn . i2 = 0 &
pn . i3 > 0 )
;
( ( pn . i2 = 1 & pn . i3 = 0 ) or ( pn . i1 = 0 & pn . i2 = 0 & pn . i3 > 0 ) or ( pn . i1 = 1 & pn . i2 = 1 & pn . i3 > 0 ) or ( pn . i1 > 1 & pn . i3 > 0 & ex y1, y2, y3, K being Nat st
( y1 = Py ((pn . i1),((pn . i3) + 1)) & K > (2 * (pn . i3)) * y1 & y2 = Py (K,((pn . i3) + 1)) & y3 = Py ((K * (pn . i1)),((pn . i3) + 1)) & ( ( 0 <= (pn . i2) - (y3 / y2) & (pn . i2) - (y3 / y2) < 1 / 2 ) or ( 0 <= (y3 / y2) - (pn . i2) & (y3 / y2) - (pn . i2) < 1 / 2 ) ) ) ) )hence
( (
pn . i2 = 1 &
pn . i3 = 0 ) or (
pn . i1 = 0 &
pn . i2 = 0 &
pn . i3 > 0 ) or (
pn . i1 = 1 &
pn . i2 = 1 &
pn . i3 > 0 ) or (
pn . i1 > 1 &
pn . i3 > 0 & ex
y1,
y2,
y3,
K being
Nat st
(
y1 = Py (
(pn . i1),
((pn . i3) + 1)) &
K > (2 * (pn . i3)) * y1 &
y2 = Py (
K,
((pn . i3) + 1)) &
y3 = Py (
(K * (pn . i1)),
((pn . i3) + 1)) & ( (
0 <= (pn . i2) - (y3 / y2) &
(pn . i2) - (y3 / y2) < 1
/ 2 ) or (
0 <= (y3 / y2) - (pn . i2) &
(y3 / y2) - (pn . i2) < 1
/ 2 ) ) ) ) )
;
verum end; suppose
(
pn . i1 = 1 &
pn . i2 = 1 &
pn . i3 > 0 )
;
( ( pn . i2 = 1 & pn . i3 = 0 ) or ( pn . i1 = 0 & pn . i2 = 0 & pn . i3 > 0 ) or ( pn . i1 = 1 & pn . i2 = 1 & pn . i3 > 0 ) or ( pn . i1 > 1 & pn . i3 > 0 & ex y1, y2, y3, K being Nat st
( y1 = Py ((pn . i1),((pn . i3) + 1)) & K > (2 * (pn . i3)) * y1 & y2 = Py (K,((pn . i3) + 1)) & y3 = Py ((K * (pn . i1)),((pn . i3) + 1)) & ( ( 0 <= (pn . i2) - (y3 / y2) & (pn . i2) - (y3 / y2) < 1 / 2 ) or ( 0 <= (y3 / y2) - (pn . i2) & (y3 / y2) - (pn . i2) < 1 / 2 ) ) ) ) )hence
( (
pn . i2 = 1 &
pn . i3 = 0 ) or (
pn . i1 = 0 &
pn . i2 = 0 &
pn . i3 > 0 ) or (
pn . i1 = 1 &
pn . i2 = 1 &
pn . i3 > 0 ) or (
pn . i1 > 1 &
pn . i3 > 0 & ex
y1,
y2,
y3,
K being
Nat st
(
y1 = Py (
(pn . i1),
((pn . i3) + 1)) &
K > (2 * (pn . i3)) * y1 &
y2 = Py (
K,
((pn . i3) + 1)) &
y3 = Py (
(K * (pn . i1)),
((pn . i3) + 1)) & ( (
0 <= (pn . i2) - (y3 / y2) &
(pn . i2) - (y3 / y2) < 1
/ 2 ) or (
0 <= (y3 / y2) - (pn . i2) &
(y3 / y2) - (pn . i2) < 1
/ 2 ) ) ) ) )
;
verum end; suppose A46:
( 1
* (pn . i1) > (0 * (pn . i2)) + 1 & 1
* (pn . i3) > (0 * (pn . i1)) + 0 &
p . N = Py (
(pn . i1),
((pn . i3) + 1)) & 1
* (p . N3) > (2 * (pn . i3)) * (p . N) &
p . N1 = Py (
(p . N3),
((pn . i3) + 1)) & 1
* (p . N2) = Py (
((p . N3) * (pn . i1)),
((pn . i3) + 1)) & ( (
(1 * (pn . i2)) * (p . N1) >= (1 * (p . N2)) + 0 &
(2 * (pn . i2)) * (p . N1) < (1 * (p . N1)) + (2 * (p . N2)) ) or ( 1
* (p . N2) >= (pn . i2) * (p . N1) &
((- 2) * (pn . i2)) * (p . N1) < (1 * (p . N1)) + ((- 2) * (p . N2)) ) ) )
;
( ( pn . i2 = 1 & pn . i3 = 0 ) or ( pn . i1 = 0 & pn . i2 = 0 & pn . i3 > 0 ) or ( pn . i1 = 1 & pn . i2 = 1 & pn . i3 > 0 ) or ( pn . i1 > 1 & pn . i3 > 0 & ex y1, y2, y3, K being Nat st
( y1 = Py ((pn . i1),((pn . i3) + 1)) & K > (2 * (pn . i3)) * y1 & y2 = Py (K,((pn . i3) + 1)) & y3 = Py ((K * (pn . i1)),((pn . i3) + 1)) & ( ( 0 <= (pn . i2) - (y3 / y2) & (pn . i2) - (y3 / y2) < 1 / 2 ) or ( 0 <= (y3 / y2) - (pn . i2) & (y3 / y2) - (pn . i2) < 1 / 2 ) ) ) ) )
(
pn . i1 > 1 &
pn . i3 > 0 & ex
y1,
y2,
y3,
K being
Nat st
(
y1 = Py (
(pn . i1),
((pn . i3) + 1)) &
K > (2 * (pn . i3)) * y1 &
y2 = Py (
K,
((pn . i3) + 1)) &
y3 = Py (
(K * (pn . i1)),
((pn . i3) + 1)) & ( (
0 <= (pn . i2) - (y3 / y2) &
(pn . i2) - (y3 / y2) < 1
/ 2 ) or (
0 <= (y3 / y2) - (pn . i2) &
(y3 / y2) - (pn . i2) < 1
/ 2 ) ) ) )
proof
thus
(
pn . i1 > 1 &
pn . i3 > 0 )
by A46;
ex y1, y2, y3, K being Nat st
( y1 = Py ((pn . i1),((pn . i3) + 1)) & K > (2 * (pn . i3)) * y1 & y2 = Py (K,((pn . i3) + 1)) & y3 = Py ((K * (pn . i1)),((pn . i3) + 1)) & ( ( 0 <= (pn . i2) - (y3 / y2) & (pn . i2) - (y3 / y2) < 1 / 2 ) or ( 0 <= (y3 / y2) - (pn . i2) & (y3 / y2) - (pn . i2) < 1 / 2 ) ) )
take
p . N
;
ex y2, y3, K being Nat st
( p . N = Py ((pn . i1),((pn . i3) + 1)) & K > (2 * (pn . i3)) * (p . N) & y2 = Py (K,((pn . i3) + 1)) & y3 = Py ((K * (pn . i1)),((pn . i3) + 1)) & ( ( 0 <= (pn . i2) - (y3 / y2) & (pn . i2) - (y3 / y2) < 1 / 2 ) or ( 0 <= (y3 / y2) - (pn . i2) & (y3 / y2) - (pn . i2) < 1 / 2 ) ) )
take
p . N1
;
ex y3, K being Nat st
( p . N = Py ((pn . i1),((pn . i3) + 1)) & K > (2 * (pn . i3)) * (p . N) & p . N1 = Py (K,((pn . i3) + 1)) & y3 = Py ((K * (pn . i1)),((pn . i3) + 1)) & ( ( 0 <= (pn . i2) - (y3 / (p . N1)) & (pn . i2) - (y3 / (p . N1)) < 1 / 2 ) or ( 0 <= (y3 / (p . N1)) - (pn . i2) & (y3 / (p . N1)) - (pn . i2) < 1 / 2 ) ) )
take
p . N2
;
ex K being Nat st
( p . N = Py ((pn . i1),((pn . i3) + 1)) & K > (2 * (pn . i3)) * (p . N) & p . N1 = Py (K,((pn . i3) + 1)) & p . N2 = Py ((K * (pn . i1)),((pn . i3) + 1)) & ( ( 0 <= (pn . i2) - ((p . N2) / (p . N1)) & (pn . i2) - ((p . N2) / (p . N1)) < 1 / 2 ) or ( 0 <= ((p . N2) / (p . N1)) - (pn . i2) & ((p . N2) / (p . N1)) - (pn . i2) < 1 / 2 ) ) )
take
p . N3
;
( p . N = Py ((pn . i1),((pn . i3) + 1)) & p . N3 > (2 * (pn . i3)) * (p . N) & p . N1 = Py ((p . N3),((pn . i3) + 1)) & p . N2 = Py (((p . N3) * (pn . i1)),((pn . i3) + 1)) & ( ( 0 <= (pn . i2) - ((p . N2) / (p . N1)) & (pn . i2) - ((p . N2) / (p . N1)) < 1 / 2 ) or ( 0 <= ((p . N2) / (p . N1)) - (pn . i2) & ((p . N2) / (p . N1)) - (pn . i2) < 1 / 2 ) ) )
thus
(
p . N = Py (
(pn . i1),
((pn . i3) + 1)) &
p . N3 > (2 * (pn . i3)) * (p . N) &
p . N1 = Py (
(p . N3),
((pn . i3) + 1)) &
p . N2 = Py (
((p . N3) * (pn . i1)),
((pn . i3) + 1)) )
by A46;
( ( 0 <= (pn . i2) - ((p . N2) / (p . N1)) & (pn . i2) - ((p . N2) / (p . N1)) < 1 / 2 ) or ( 0 <= ((p . N2) / (p . N1)) - (pn . i2) & ((p . N2) / (p . N1)) - (pn . i2) < 1 / 2 ) )
not
pn . i1 is
trivial
by A46, NEWTON03:def 1;
then
(
p . N > 0 & 2
* (pn . i3) > 0 )
by A46, XREAL_1:129, HILB10_1:13;
then
(2 * (pn . i3)) * (p . N) > 0
by XREAL_1:129;
then
(2 * (pn . i3)) * (p . N) >= 1
by NAT_1:14;
then
p . N3 > 1
by A46, XXREAL_0:2;
then
not
p . N3 is
trivial
by NEWTON03:def 1;
then A47:
p . N1 > 0
by A46, HILB10_1:13;
per cases
( ( (pn . i2) * (p . N1) >= p . N2 & (2 * (pn . i2)) * (p . N1) < (1 * (p . N1)) + (2 * (p . N2)) ) or ( p . N2 >= (pn . i2) * (p . N1) & ((- 2) * (pn . i2)) * (p . N1) < (1 * (p . N1)) + ((- 2) * (p . N2)) ) )
by A46;
suppose
(
(pn . i2) * (p . N1) >= p . N2 &
(2 * (pn . i2)) * (p . N1) < (1 * (p . N1)) + (2 * (p . N2)) )
;
( ( 0 <= (pn . i2) - ((p . N2) / (p . N1)) & (pn . i2) - ((p . N2) / (p . N1)) < 1 / 2 ) or ( 0 <= ((p . N2) / (p . N1)) - (pn . i2) & ((p . N2) / (p . N1)) - (pn . i2) < 1 / 2 ) )end; suppose A50:
(
p . N2 >= (pn . i2) * (p . N1) &
((- 2) * (pn . i2)) * (p . N1) < (1 * (p . N1)) + ((- 2) * (p . N2)) )
;
( ( 0 <= (pn . i2) - ((p . N2) / (p . N1)) & (pn . i2) - ((p . N2) / (p . N1)) < 1 / 2 ) or ( 0 <= ((p . N2) / (p . N1)) - (pn . i2) & ((p . N2) / (p . N1)) - (pn . i2) < 1 / 2 ) )end;
end; hence
( (
pn . i2 = 1 &
pn . i3 = 0 ) or (
pn . i1 = 0 &
pn . i2 = 0 &
pn . i3 > 0 ) or (
pn . i1 = 1 &
pn . i2 = 1 &
pn . i3 > 0 ) or (
pn . i1 > 1 &
pn . i3 > 0 & ex
y1,
y2,
y3,
K being
Nat st
(
y1 = Py (
(pn . i1),
((pn . i3) + 1)) &
K > (2 * (pn . i3)) * y1 &
y2 = Py (
K,
((pn . i3) + 1)) &
y3 = Py (
(K * (pn . i1)),
((pn . i3) + 1)) & ( (
0 <= (pn . i2) - (y3 / y2) &
(pn . i2) - (y3 / y2) < 1
/ 2 ) or (
0 <= (y3 / y2) - (pn . i2) &
(y3 / y2) - (pn . i2) < 1
/ 2 ) ) ) ) )
;
verum
end;
then
pn . i2 = (pn . i1) |^ (pn . i3)
by HILB10_1:39;
hence
o in WW
by A43;
verum
end;
WW c= { (p | n) where p is n + 7 -element XFinSequence of NAT : p in { p where p is n + 7 -element XFinSequence of NAT : S38[p] } }
proof
let o be
object ;
TARSKI:def 3 ( not o in WW or o in { (p | n) where p is n + 7 -element XFinSequence of NAT : p in { p where p is n + 7 -element XFinSequence of NAT : S38[p] } } )
assume A54:
o in WW
;
o in { (p | n) where p is n + 7 -element XFinSequence of NAT : p in { p where p is n + 7 -element XFinSequence of NAT : S38[p] } }
consider p being
n -element XFinSequence of
NAT such that A55:
(
o = p &
p . i2 = (p . i1) |^ (p . i3) )
by A54;
set x =
p . i1;
set y =
p . i2;
set z =
p . i3;
per cases
( ( p . i2 = 1 & p . i3 = 0 ) or ( p . i1 = 0 & p . i2 = 0 & p . i3 > 0 ) or ( p . i1 = 1 & p . i2 = 1 & p . i3 > 0 ) or ( p . i1 > 1 & p . i3 > 0 & ex y1, y2, y3, K being Nat st
( y1 = Py ((p . i1),((p . i3) + 1)) & K > (2 * (p . i3)) * y1 & y2 = Py (K,((p . i3) + 1)) & y3 = Py ((K * (p . i1)),((p . i3) + 1)) & ( ( 0 <= (p . i2) - (y3 / y2) & (p . i2) - (y3 / y2) < 1 / 2 ) or ( 0 <= (y3 / y2) - (p . i2) & (y3 / y2) - (p . i2) < 1 / 2 ) ) ) ) )
by A55, HILB10_1:39;
suppose A59:
(
p . i1 > 1 &
p . i3 > 0 & ex
y1,
y2,
y3,
K being
Nat st
(
y1 = Py (
(p . i1),
((p . i3) + 1)) &
K > (2 * (p . i3)) * y1 &
y2 = Py (
K,
((p . i3) + 1)) &
y3 = Py (
(K * (p . i1)),
((p . i3) + 1)) & ( (
0 <= (p . i2) - (y3 / y2) &
(p . i2) - (y3 / y2) < 1
/ 2 ) or (
0 <= (y3 / y2) - (p . i2) &
(y3 / y2) - (p . i2) < 1
/ 2 ) ) ) )
;
o in { (p | n) where p is n + 7 -element XFinSequence of NAT : p in { p where p is n + 7 -element XFinSequence of NAT : S38[p] } } then consider y1,
y2,
y3,
K being
Nat such that A60:
(
y1 = Py (
(p . i1),
((p . i3) + 1)) &
K > (2 * (p . i3)) * y1 &
y2 = Py (
K,
((p . i3) + 1)) &
y3 = Py (
(K * (p . i1)),
((p . i3) + 1)) & ( (
0 <= (p . i2) - (y3 / y2) &
(p . i2) - (y3 / y2) < 1
/ 2 ) or (
0 <= (y3 / y2) - (p . i2) &
(y3 / y2) - (p . i2) < 1
/ 2 ) ) )
;
reconsider y1 =
y1,
y2 =
y2,
y3 =
y3,
K =
K,
z1 =
(p . i3) + 1 as
Element of
NAT by ORDINAL1:def 12;
reconsider Kx =
K * (p . i1),
yy2 =
(p . i2) * y2 as
Element of
NAT ;
set Y =
(((((<%y1%> ^ <%y2%>) ^ <%y3%>) ^ <%K%>) ^ <%z1%>) ^ <%Kx%>) ^ <%yy2%>;
set PY =
p ^ ((((((<%y1%> ^ <%y2%>) ^ <%y3%>) ^ <%K%>) ^ <%z1%>) ^ <%Kx%>) ^ <%yy2%>);
A61:
(
len p = n &
len ((((((<%y1%> ^ <%y2%>) ^ <%y3%>) ^ <%K%>) ^ <%z1%>) ^ <%Kx%>) ^ <%yy2%>) = 7 )
by CARD_1:def 7;
A62:
(p ^ ((((((<%y1%> ^ <%y2%>) ^ <%y3%>) ^ <%K%>) ^ <%z1%>) ^ <%Kx%>) ^ <%yy2%>)) | n = p
by A61, AFINSQ_1:57;
4
in dom ((((((<%y1%> ^ <%y2%>) ^ <%y3%>) ^ <%K%>) ^ <%z1%>) ^ <%Kx%>) ^ <%yy2%>)
by A61, AFINSQ_1:66;
then A63:
(p ^ ((((((<%y1%> ^ <%y2%>) ^ <%y3%>) ^ <%K%>) ^ <%z1%>) ^ <%Kx%>) ^ <%yy2%>)) . (n + 4) =
((((((<%y1%> ^ <%y2%>) ^ <%y3%>) ^ <%K%>) ^ <%z1%>) ^ <%Kx%>) ^ <%yy2%>) . 4
by A61, AFINSQ_1:def 3
.=
z1
by AFINSQ_1:48
;
0 in dom ((((((<%y1%> ^ <%y2%>) ^ <%y3%>) ^ <%K%>) ^ <%z1%>) ^ <%Kx%>) ^ <%yy2%>)
by A61, AFINSQ_1:66;
then A64:
(p ^ ((((((<%y1%> ^ <%y2%>) ^ <%y3%>) ^ <%K%>) ^ <%z1%>) ^ <%Kx%>) ^ <%yy2%>)) . (n + 0) =
((((((<%y1%> ^ <%y2%>) ^ <%y3%>) ^ <%K%>) ^ <%z1%>) ^ <%Kx%>) ^ <%yy2%>) . 0
by A61, AFINSQ_1:def 3
.=
y1
by AFINSQ_1:48
;
3
in dom ((((((<%y1%> ^ <%y2%>) ^ <%y3%>) ^ <%K%>) ^ <%z1%>) ^ <%Kx%>) ^ <%yy2%>)
by A61, AFINSQ_1:66;
then A65:
(p ^ ((((((<%y1%> ^ <%y2%>) ^ <%y3%>) ^ <%K%>) ^ <%z1%>) ^ <%Kx%>) ^ <%yy2%>)) . (n + 3) =
((((((<%y1%> ^ <%y2%>) ^ <%y3%>) ^ <%K%>) ^ <%z1%>) ^ <%Kx%>) ^ <%yy2%>) . 3
by A61, AFINSQ_1:def 3
.=
K
by AFINSQ_1:48
;
5
in dom ((((((<%y1%> ^ <%y2%>) ^ <%y3%>) ^ <%K%>) ^ <%z1%>) ^ <%Kx%>) ^ <%yy2%>)
by A61, AFINSQ_1:66;
then A66:
(p ^ ((((((<%y1%> ^ <%y2%>) ^ <%y3%>) ^ <%K%>) ^ <%z1%>) ^ <%Kx%>) ^ <%yy2%>)) . (n + 5) =
((((((<%y1%> ^ <%y2%>) ^ <%y3%>) ^ <%K%>) ^ <%z1%>) ^ <%Kx%>) ^ <%yy2%>) . 5
by A61, AFINSQ_1:def 3
.=
Kx
by AFINSQ_1:48
;
not
p . i1 is
trivial
by A59, NEWTON03:def 1;
then
(
y1 > 0 &
p . i3 > 0 )
by A59, A60, HILB10_1:13;
then
(p . i3) * y1 > 0
by XREAL_1:129;
then
2
* ((p . i3) * y1) >= 2
* 1
by XREAL_1:64, NAT_1:14;
then A67:
K >= 1
+ 1
by XXREAL_0:2, A60;
then A68:
K > 1
by XXREAL_0:2;
1
in dom ((((((<%y1%> ^ <%y2%>) ^ <%y3%>) ^ <%K%>) ^ <%z1%>) ^ <%Kx%>) ^ <%yy2%>)
by A61, AFINSQ_1:66;
then A69:
(p ^ ((((((<%y1%> ^ <%y2%>) ^ <%y3%>) ^ <%K%>) ^ <%z1%>) ^ <%Kx%>) ^ <%yy2%>)) . (n + 1) =
((((((<%y1%> ^ <%y2%>) ^ <%y3%>) ^ <%K%>) ^ <%z1%>) ^ <%Kx%>) ^ <%yy2%>) . 1
by A61, AFINSQ_1:def 3
.=
y2
by AFINSQ_1:48
;
A70:
K * (p . i1) > 1
* 1
by A68, A59, XREAL_1:97;
2
in dom ((((((<%y1%> ^ <%y2%>) ^ <%y3%>) ^ <%K%>) ^ <%z1%>) ^ <%Kx%>) ^ <%yy2%>)
by A61, AFINSQ_1:66;
then A71:
(p ^ ((((((<%y1%> ^ <%y2%>) ^ <%y3%>) ^ <%K%>) ^ <%z1%>) ^ <%Kx%>) ^ <%yy2%>)) . (n + 2) =
((((((<%y1%> ^ <%y2%>) ^ <%y3%>) ^ <%K%>) ^ <%z1%>) ^ <%Kx%>) ^ <%yy2%>) . 2
by A61, AFINSQ_1:def 3
.=
y3
by AFINSQ_1:48
;
6
in dom ((((((<%y1%> ^ <%y2%>) ^ <%y3%>) ^ <%K%>) ^ <%z1%>) ^ <%Kx%>) ^ <%yy2%>)
by A61, AFINSQ_1:66;
then A72:
(p ^ ((((((<%y1%> ^ <%y2%>) ^ <%y3%>) ^ <%K%>) ^ <%z1%>) ^ <%Kx%>) ^ <%yy2%>)) . (n + 6) =
((((((<%y1%> ^ <%y2%>) ^ <%y3%>) ^ <%K%>) ^ <%z1%>) ^ <%Kx%>) ^ <%yy2%>) . 6
by A61, AFINSQ_1:def 3
.=
yy2
by AFINSQ_1:48
;
not
p . i1 is
trivial
by A59, NEWTON03:def 1;
then
(
y1 > 0 & 2
* (p . i3) > 0 )
by A60, A59, XREAL_1:129, HILB10_1:13;
then
(2 * (p . i3)) * y1 > 0
by XREAL_1:129;
then
(2 * (p . i3)) * y1 >= 1
by NAT_1:14;
then
K > 1
by A60, XXREAL_0:2;
then
not
K is
trivial
by NEWTON03:def 1;
then A73:
y2 > 0
by A60, HILB10_1:13;
S27[
p ^ ((((((<%y1%> ^ <%y2%>) ^ <%y3%>) ^ <%K%>) ^ <%z1%>) ^ <%Kx%>) ^ <%yy2%>)]
then
S37[
p ^ ((((((<%y1%> ^ <%y2%>) ^ <%y3%>) ^ <%K%>) ^ <%z1%>) ^ <%Kx%>) ^ <%yy2%>)]
by A59, A63, A67, XXREAL_0:2, A65, A71, A60, A70, A66, A64, A62, A1, Th4, A69, A72;
then
p ^ ((((((<%y1%> ^ <%y2%>) ^ <%y3%>) ^ <%K%>) ^ <%z1%>) ^ <%Kx%>) ^ <%yy2%>) in { p where p is n + 7 -element XFinSequence of NAT : S38[p] }
;
hence
o in { (p | n) where p is n + 7 -element XFinSequence of NAT : p in { p where p is n + 7 -element XFinSequence of NAT : S38[p] } }
by A55, A62;
verum end;
end; hence
{ p where p is n -element XFinSequence of NAT : p . i2 = (p . i1) |^ (p . i3) } is
diophantine Subset of
(n -xtuples_of NAT)
by A40, A41, XBOOLE_0:def 10;
verum end;