:: Basic Diophantine Relations
:: by Marcin Acewicz and Karol P\kak
::
:: Received June 29, 2018
:: Copyright (c) 2018-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, SUBSET_1, RELAT_1, ORDINAL4, FINSEQ_1, XBOOLE_0,
FUNCT_1, XXREAL_0, TARSKI, NAT_1, INT_1, ARYTM_3, ZFMISC_1, CARD_1,
ORDINAL1, ARYTM_1, PRE_POLY, QC_LANG1, GROUP_1, ALGSTR_0, RLVECT_1,
VECTSP_1, LATTICES, MCART_1, MESFUNC1, RFINSEQ, POLYNOM1, POLYNOM2,
HILBASIS, AFINSQ_1, COMPLEX1, SQUARE_1, NEWTON, PELLS_EQ, HILB10_1,
HILB10_2;
notations TARSKI, XBOOLE_0, SUBSET_1, ZFMISC_1, XTUPLE_0, ORDINAL1, CARD_1,
NUMBERS, RELAT_1, XXREAL_0, XCMPLX_0, FUNCT_1, RELSET_1, XREAL_0, NAT_D,
NAT_1, INT_1, ALGSTR_0, RLVECT_1, VECTSP_1, GROUP_1, RECDEF_1, PRE_POLY,
POLYNOM1, POLYNOM2, HILBASIS, AFINSQ_1, AFINSQ_2, STRUCT_0, POLYNOM7,
COMPLEX1, SQUARE_1, NEWTON, PELLS_EQ, HILB10_1, HILB10_2;
constructors FINSOP_1, NAT_D, RECDEF_1, BINOP_2, RELSET_1, DOMAIN_1, GROUP_4,
ALGSTR_1, VFUNCT_1, POLYNOM2, HILBASIS, AFINSQ_2, POLYNOM7, SQUARE_1,
NEWTON, PELLS_EQ, HILB10_1, HILB10_2;
registrations XBOOLE_0, RELAT_1, FUNCT_1, ORDINAL1, XREAL_0, NAT_1, CARD_1,
VALUED_0, VALUED_1, RELSET_1, INT_1, PEPIN, XTUPLE_0, STRUCT_0, VECTSP_1,
ALGSTR_1, POLYNOM1, PRE_POLY, MEMBERED, POLYNOM2, ALGSTR_0, AFINSQ_2,
NIVEN, HILBASIS, AFINSQ_1, POLYNOM7, PREPOWER, HILB10_2;
requirements NUMERALS, REAL, SUBSET, BOOLE, ARITHM;
definitions TARSKI, RELAT_1, XBOOLE_0;
equalities ORDINAL1, VECTSP_1, HILB10_2;
expansions HILB10_2;
theorems ZFMISC_1, FUNCT_1, NAT_1, INT_1, CARD_1, ORDINAL1, POLYNOM2,
XBOOLE_0, XBOOLE_1, XREAL_1, XXREAL_0, NAT_D, XREAL_0, AFINSQ_1,
HILBASIS, AFINSQ_2, XCMPLX_1, SUBSET_1, POLYNOM7, ABSVALUE, SQUARE_1,
NEWTON03, PELLS_EQ, HILB10_1, HILB10_2;
begin :: Preliminaries
reserve n,m,k for Nat,
p,q for n-element XFinSequence of NAT,
i1,i2,i3,i4,i5,i6 for Element of n,
a,b,c,d,e for Integer;
registration
let X be set, p be INT -valued Series of X, F_Real;
let a be integer Element of F_Real;
cluster a*p -> INT -valued;
coherence
proof
thus rng (a*p) c= INT
proof
let y be object such that
A1: y in rng (a*p);
consider x be object such that
A2: x in dom (a*p) & (a*p).x=y by A1,FUNCT_1:def 3;
reconsider x as bag of X by A2;
(a*p).x = a*(p.x) by POLYNOM7:def 9;
hence thesis by A2,INT_1:def 2;
end;
end;
end;
theorem Th1:
for O be non empty Ordinal, i be Element of O,
L be add-associative right_zeroed
right_complementable well-unital distributive non trivial
doubleLoopStr
for x be Function of O, L holds
eval(1_1(i,L),x) = x.i
proof
let O be non empty Ordinal, i be Element of O,
L be add-associative right_zeroed right_complementable
well-unital distributive non trivial doubleLoopStr;
let x be Function of O, L;
set p = 1_1(i,L);
Support p = {UnitBag i} by HILBASIS:13;
then eval(p, x) = (p.UnitBag i)*eval(UnitBag i,x) by POLYNOM2:19
.= 1_L *eval(UnitBag i,x) by HILBASIS:12
.= eval(UnitBag i,x);
hence thesis by HILBASIS:11;
end;
theorem Th2:
i1 is Element of (n+k)
proof
i1 is Element of Segm(n);
then reconsider I=i1 as Nat;
per cases;
suppose n =0 & k=0;
hence thesis;
end;
suppose A1: n =0 & k>0;
then i1 is empty by SUBSET_1:def 1;
then I in Segm(n+k) by A1,NAT_1:44;
hence thesis;
end;
suppose n<>0;
then I in Segm n;
then I < n <= n+k by NAT_1:11,44;
then I < n+k by XXREAL_0:2;
then I in Segm (n+k) by NAT_1:44;
hence thesis;
end;
end;
theorem Th3:
k < m implies n+k in (n+m)
proof
assume m>k;
then k+n < n+m by XREAL_1:8;
then n+k in Segm (n+m) by NAT_1:44;
hence thesis;
end;
theorem Th4:
for p be (n+k) -element XFinSequence st n<>0 & k <> 0 holds
(p|n).i1 = p.i1
proof
let p be (n+k) -element XFinSequence such that A1:n<>0 and A2:k<>0;
i1 is Element of Segm(n);
then reconsider I=i1 as Nat;
k>0 by A2;then
A3: len p = n+k & n+k > n+0 by CARD_1:def 7,XREAL_1:8;
I in n by A1;
hence thesis by A3,AFINSQ_1:53;
end;
begin :: Basic Diophantine Relations
theorem Th5:
for A be diophantine Subset of n -xtuples_of NAT
for k st k <= n holds
{p|k : p in A} is diophantine Subset of k -xtuples_of NAT
proof
let A be diophantine Subset of n -xtuples_of NAT;
let k such that A1: k <=n;
consider nA be Nat, pA be INT -valued Polynomial of n+nA,F_Real such that
A2: for s be object holds
s in A iff ex x be n-element XFinSequence of NAT,
y be nA-element XFinSequence of NAT st
s=x & eval(pA,@(x^y)) = 0 by HILB10_2:def 6;
set D={p|k where p is n-element XFinSequence of NAT:p in A};
D c= k -xtuples_of NAT
proof
let y be object;
assume y in D;
then consider p be n-element XFinSequence of NAT such that
A3: y=p|k & p in A;
len p = n by CARD_1:def 7;
then len (p|k) = k by A1,AFINSQ_1:54;
then p|k is k-element by CARD_1:def 7;
hence thesis by A3,HILB10_2:def 5;
end;
then reconsider D as Subset of k -xtuples_of NAT;
reconsider nk=n-k as Nat by A1,NAT_1:21;
reconsider P=pA as INT -valued Polynomial of k+(nk+nA),F_Real;
for s be object holds
s in D iff ex x be k-element XFinSequence of NAT,
y be nk+nA-element XFinSequence of NAT st
s=x & eval(P,@(x^y)) = 0
proof
let s be object;
thus s in D implies ex x be k-element XFinSequence of NAT,
y be nk+nA-element XFinSequence of NAT st
s=x & eval(P,@(x^y)) = 0
proof
assume s in D;
then consider p be n-element XFinSequence of NAT such that
A4: s=p|k & p in A;
consider x be n-element XFinSequence of NAT,
y be nA-element XFinSequence of NAT such that
A5: p=x & eval(pA,@(x^y)) = 0 by A4,A2;
A6:x = (x|k)^(x/^k);
A7: len x = n & len y = nA by CARD_1:def 7;
then A8: len (x|k) = k by A1,AFINSQ_1:54;
len (x/^k) = k+nk-'k by A7,AFINSQ_2:def 2
.= nk by NAT_D:34;
then len ((x/^k)^y) = nk+nA by A7,AFINSQ_1:17;
then reconsider X = (x/^k)^y as nk+nA-element XFinSequence of NAT
by CARD_1:def 7;
A9: x^y = (x|k)^X by A6,AFINSQ_1:27;
reconsider xk= x|k as k-element XFinSequence of NAT by A8,CARD_1:def 7;
s=xk by A4,A5;
hence thesis by A9,A5;
end;
given x be k-element XFinSequence of NAT,
y be nk+nA-element XFinSequence of NAT such that
A10: s=x & eval(P,@(x^y)) = 0;
A11:y = (y|nk)^(y/^nk);
A12: len x = k & len y = nk+nA by CARD_1:def 7;
then A13: len (y|nk) = nk by NAT_1:11,AFINSQ_1:54;
A14: len (y/^nk) = nk+nA-'nk by A12,AFINSQ_2:def 2
.= nA by NAT_D:34;
len (x^(y|nk)) = k+nk by A12,A13,AFINSQ_1:17;
then reconsider X = x^(y|nk) as n-element XFinSequence of NAT
by CARD_1:def 7;
reconsider Y=y/^nk as nA-element XFinSequence of NAT
by CARD_1:def 7,A14;
x^y = X^Y by A11,AFINSQ_1:27;
then X in A by A2,A10;
then X|k in D;
hence thesis by A10,A12,AFINSQ_1:57;
end;
hence thesis by HILB10_2:def 6;
end;
theorem Th6:
for a,b,c be Integer,i1,i2 holds
{p: a*p.i1 = b*p.i2+c} is diophantine Subset of n -xtuples_of NAT
proof
let c,a,b be Integer,i1,i2;
set F=F_Real;
reconsider ar=a,br=b,cr = c as integer Element of F by XREAL_0:def 1;
set D = {p: c * p.i1 = a*(p.i2)+b};
D c= n -xtuples_of NAT
proof
let y be object;
assume y in D;
then ex p st
y=p & c*p.i1 = a*(p.i2)+b;
hence thesis by HILB10_2:def 5;
end;
then reconsider D as Subset of n -xtuples_of NAT;
per cases;
suppose n=0;
then D is diophantine Subset of n -xtuples_of NAT;
hence thesis;
end;
suppose A1: n<>0;
set Q= cr*1_1(i1,F) - ar*1_1(i2,F)- br*1_(n,F);
reconsider Q as INT -valued Polynomial of n+0,F_Real;
for s be object holds
s in D iff ex x be n-element XFinSequence of NAT,
y be 0-element XFinSequence of NAT st
s=x & eval(Q,@(x^y)) = 0
proof
let s be object;
thus s in D implies ex x be n-element XFinSequence of NAT,
y be 0-element XFinSequence of NAT st
s=x & eval(Q,@(x^y)) = 0
proof
assume s in D;
then consider p such that
A2: s=p & c* p.i1=a*(p.i2)+b;
reconsider Z=<%>NAT as 0-element XFinSequence of NAT;
take pZ=p,Z;
A3: eval(br*1_(n,F),@p) = br*eval(1_(n,F),@p) by POLYNOM7:29
.= br* 1.F by POLYNOM2:21
.= b;
A4:eval(ar*1_1(i2,F),@p) = ar*eval(1_1(i2,F),@p) by POLYNOM7:29
.= a*(p.i2) by A1,Th1;
A5:eval(cr*1_1(i1,F),@p) = cr*eval(1_1(i1,F),@p) by POLYNOM7:29
.= c*(p.i1) by A1,Th1;
eval(Q,@(p^Z)) =
eval(cr*1_1(i1,F) - ar*1_1(i2,F),@p)- eval(br*1_(n,F),@p)
by POLYNOM2:24
.= eval(cr*1_1(i1,F),@p) - eval(ar*1_1(i2,F),@p)- eval(br*1_(n,F),@p)
by POLYNOM2:24
.= 0 by A2,A3,A4,A5;
hence thesis by A2;
end;
given p be n-element XFinSequence of NAT,
Z be 0-element XFinSequence of NAT such that
A6: s=p & eval(Q,@(p^Z)) = 0;
A7: eval(br*1_(n,F),@p) = br*eval(1_(n,F),@p) by POLYNOM7:29
.= br* 1.F by POLYNOM2:21
.= b;
A8:eval(ar*1_1(i2,F),@p) = ar*eval(1_1(i2,F),@p) by POLYNOM7:29
.= a*(p.i2) by A1,Th1;
A9:
eval(cr*1_1(i1,F),@p) = cr*eval(1_1(i1,F),@p) by POLYNOM7:29
.= c*(p.i1) by A1,Th1;
eval(Q,@(p^Z))
= eval(cr*1_1(i1,F)-ar*1_1(i2,F),@p)- eval(br*1_(n,F),@p) by POLYNOM2:24
.= eval(cr*1_1(i1,F),@p) - eval(ar*1_1(i2,F),@p)- eval(br*1_(n,F),@p)
by POLYNOM2:24
.= c*p.i1 - a*(p.i2) - b by A7,A8,A9;
then c*p.i1 = a*(p.i2)+b by A6;
hence thesis by A6;
end;
then D is diophantine;
hence thesis;
end;
end;
theorem Th7:
for a,b,c,i1,i2 holds
{p: a*p.i1 > b*p.i2+c} is diophantine Subset of n -xtuples_of NAT
proof
let a,b,c be Integer,i1,i2 be Element of n;
set F=F_Real;
set n1=n+1;
set D = {p: a* p.i1 > b*p.i2+c};
D c= n -xtuples_of NAT
proof
let y be object;
assume y in D;
then ex p st y=p & a* p.i1 > b*p.i2+c;
hence thesis by HILB10_2:def 5;
end;
then reconsider D as Subset of n -xtuples_of NAT;
per cases;
suppose n=0;
then D is diophantine Subset of n -xtuples_of NAT;
hence thesis;
end;
suppose A1: n<>0;
A2: n< n1 by NAT_1:13;
n in Segm n1 by A2,NAT_1:44;
then reconsider I=i1,J=i2,N=n as Element of n1 by Th2;
reconsider ar=a,br=b,cr = c+1 as integer Element of F
by XREAL_0:def 1;
set Q=br*1_1(J,F) - ar*1_1(I,F)+1_1(N,F)+cr*1_(n1,F);
reconsider Q as INT -valued Polynomial of n+1,F_Real;
for s be object holds
s in D iff ex x be n-element XFinSequence of NAT,
y be 1-element XFinSequence of NAT st
s=x & eval(Q,@(x^y)) = 0
proof
let s be object;
thus s in D implies ex x be n-element XFinSequence of NAT,
y be 1-element XFinSequence of NAT st
s=x & eval(Q,@(x^y)) = 0
proof
assume s in D;
then consider p such that
A3: s=p & a* p.i1 > b*p.i2+c;
a* p.i1 - (b*p.i2+c) > 0 by A3,XREAL_1:50;
then reconsider pij=a* p.i1 - (b*p.i2+c) as Element of NAT
by INT_1:3;
reconsider pp=pij-1 as Element of NAT by A3,XREAL_1:50,NAT_1:20;
reconsider Z=<%pp%> as 1-element XFinSequence of NAT;
take pZ=p,Z;
set P=@(p^Z);
A4: len p = n by CARD_1:def 7;
A5: P.I = p.i1 & P.J = p.i2 by A4,A1, AFINSQ_1:def 3;
A6:eval(ar*1_1(I,F),P) = ar*eval(1_1(I,F),P) by POLYNOM7:29
.= a*(P.I) by Th1;
A7:eval(br*1_1(J,F),P) = br*eval(1_1(J,F),P) by POLYNOM7:29
.= b*(P.J) by Th1;
A8:eval(cr*1_(n1,F),P) = cr*eval(1_(n1,F),P) by POLYNOM7:29
.= cr*(1.F) by POLYNOM2:21;
A9: eval(1_1(I,F),P) = P.I & eval(1_1(J,F),P) = P.J &
eval(1_1(N,F),P) =P.N & eval(1_(n1,F),P) = 1.F by Th1,POLYNOM2:21;
eval(Q,P) =
eval(br*1_1(J,F) - ar*1_1(I,F)+ 1_1(N,F),P) + eval(cr*1_(n1,F),P)
by POLYNOM2:23
.= eval(br*1_1(J,F) - ar*1_1(I,F),P)+eval(1_1(N,F),P)
+ eval(cr*1_(n1,F),P) by POLYNOM2:23
.= eval(br*1_1(J,F),P) - eval(ar*1_1(I,F),P)+eval(1_1(N,F),P)
+ eval(cr*1_(n1,F),P) by POLYNOM2:24
.= (b*p.i2) - (a*p.i1) +pp+cr by A5,A9,A6,A7,A8
.= 0;
hence thesis by A3;
end;
given p be n-element XFinSequence of NAT,
Z be 1-element XFinSequence of NAT such that
A10: s=p & eval(Q,@(p^Z)) = 0;
set P=@(p^Z);
len p = n by CARD_1:def 7;then
A11: P.I = p.i1 & P.J = p.i2 by A1, AFINSQ_1:def 3;
A12:eval(ar*1_1(I,F),P) = ar*eval(1_1(I,F),P) by POLYNOM7:29
.= a*(P.I) by Th1;
A13:eval(br*1_1(J,F),P) = br*eval(1_1(J,F),P) by POLYNOM7:29
.= b*(P.J) by Th1;
A14:eval(cr*1_(n1,F),P) = cr*eval(1_(n1,F),P) by POLYNOM7:29
.= cr*(1.F) by POLYNOM2:21;
eval(Q,P) =
eval(br*1_1(J,F) - ar*1_1(I,F)+ 1_1(N,F),P) + eval(cr*1_(n1,F),P)
by POLYNOM2:23
.= eval(br*1_1(J,F) - ar*1_1(I,F),P)+eval(1_1(N,F),P) +
eval(cr*1_(n1,F),P) by POLYNOM2:23
.= eval(br*1_1(J,F),P) - eval(ar*1_1(I,F),P)+eval(1_1(N,F),P)
+ eval(cr*1_(n1,F),P) by POLYNOM2:24
.= (b*p.i2) - (a*p.i1) +P.n+cr by Th1,A11,A12,A13,A14;
then (a*p.i1) = ((b*p.i2)+c+1)+P.n by A10;
then A15:(a*p.i1) >= (b*p.i2)+c+1 by XREAL_1:31;
(b*p.i2)+c+1 > (b*p.i2)+c by XREAL_1:29;
then (a*p.i1) > (b*p.i2)+c by A15,XXREAL_0:2;
hence thesis by A10;
end;
then D is diophantine;
hence thesis;
end;
end;
scheme UnionDiophantine{n()->Nat,P,Q[XFinSequence of NAT] }:
{p where p is n()-element XFinSequence of NAT: P[p] or Q[p]}
is diophantine Subset of n() -xtuples_of NAT
provided
A1:{p where p is n()-element XFinSequence of NAT: P[p]}
is diophantine Subset of n() -xtuples_of NAT
and
A2:{p where p is n()-element XFinSequence of NAT: Q[p]}
is diophantine Subset of n() -xtuples_of NAT
proof
reconsider PF={p where p is n()-element XFinSequence of NAT: P[p]} as
diophantine Subset of n() -xtuples_of NAT by A1;
reconsider QF={p where p is n()-element XFinSequence of NAT: Q[p]} as
diophantine Subset of n() -xtuples_of NAT by A2;
set PQ = {p where p is n()-element XFinSequence of NAT: P[p] or Q[p]};
A3: PQ c= PF\/QF
proof
let x be object;
assume x in PQ;
then consider p be n()-element XFinSequence of NAT such that
A4: x =p & (P[p] or Q[p]);
x in PF or x in QF by A4;
hence thesis by XBOOLE_0:def 3;
end;
A5: PF c= PQ
proof
let x be object;
assume x in PF;
then ex p be n()-element XFinSequence of NAT st x =p & P[p];
hence thesis;
end;
QF c= PQ
proof
let x be object;
assume x in QF;
then ex p be n()-element XFinSequence of NAT st x =p & Q[p];
hence thesis;
end;
then PF \/QF c= PQ by A5,XBOOLE_1:8;
hence thesis by A3,XBOOLE_0:def 10;
end;
scheme Eq{n()->Nat,P,Q[object] }:
{p where p is n()-element XFinSequence of NAT: P[p]} =
{q where q is n()-element XFinSequence of NAT: Q[q]}
provided
A1: for p being n()-element XFinSequence of NAT holds P[p] iff Q[p]
proof
set P={p where p is n()-element XFinSequence of NAT: P[p]},
Q={q where q is n()-element XFinSequence of NAT : Q[q]};
thus P c= Q
proof
let x be object such that A2: x in P;
consider p be n()-element XFinSequence of NAT such that A3:x=p&P[p] by A2;
Q[p] by A1,A3;
hence thesis by A3;
end;
let x be object such that A4: x in Q;
consider p be n()-element XFinSequence of NAT such that A5:x= p & Q[p] by A4;
P[p] by A1,A5;
hence thesis by A5;
end;
theorem Th8:
for a,b,c,i1,i2 holds
{p: a*p.i1 >= b*p.i2+c} is diophantine Subset of n -xtuples_of NAT
proof
let a,b,c be Integer,i1,i2 be Element of n;
defpred P[XFinSequence of NAT] means a* $1.i1 > b*$1.i2+c;
defpred Q[XFinSequence of NAT] means a* $1.i1 = b*$1.i2+c;
defpred R[XFinSequence of NAT] means P[$1] or Q[$1];
defpred S[XFinSequence of NAT] means a* $1.i1 >= b*$1.i2+c;
A1:{p: P[p]} is diophantine Subset of n -xtuples_of NAT by Th7;
A2:{p: Q[p]} is diophantine Subset of n -xtuples_of NAT by Th6;
A3: {p: P[p] or Q[p]} is diophantine Subset of n -xtuples_of NAT
from UnionDiophantine(A1,A2);
A4:R[p] iff S[p] by XXREAL_0:1;
{p: R[p]} = {q: S[q]} from Eq(A4);
hence thesis by A3;
end;
theorem Th9:
for a,b,i1,i2,i3 holds
{p: a*p.i1 = b*p.i2*p.i3} is diophantine Subset of n -xtuples_of NAT
proof
let a,b be Integer,i1,i2,i3;
set F=F_Real;
reconsider ar=a,br=b as integer Element of F by XREAL_0:def 1;
set D = {p: a*p.i1 = b*(p.i2) * (p.i3)};
D c= n -xtuples_of NAT
proof
let y be object;
assume y in D;
then ex p st y=p & a*p.i1 = b*(p.i2) * (p.i3);
hence thesis by HILB10_2:def 5;
end;
then reconsider D as Subset of n -xtuples_of NAT;
per cases;
suppose n=0;
then D is diophantine Subset of n -xtuples_of NAT;
hence thesis;
end;
suppose A1: n<>0;
set Q= ar*1_1(i1,F) - br*(1_1(i2,F) *' 1_1(i3,F));
reconsider Q as INT -valued Polynomial of n+0,F_Real;
for s be object holds
s in D iff ex x be n-element XFinSequence of NAT,
y be 0-element XFinSequence of NAT st
s=x & eval(Q,@(x^y)) = 0
proof
let s be object;
thus s in D implies ex x be n-element XFinSequence of NAT,
y be 0-element XFinSequence of NAT st
s=x & eval(Q,@(x^y)) = 0
proof
assume s in D;
then consider p such that
A2: s=p & a * (p.i1)=b*(p.i2) * (p.i3);
reconsider Z=<%>NAT as 0-element XFinSequence of NAT;
take p,Z;
set pZ=p^Z;
A3: eval(1_1(i1,F),@p) = p.i1 &
eval(1_1(i2,F),@p) = p.i2 &
eval(1_1(i3,F),@p) = p.i3 by A1, Th1;
A4:eval(ar*1_1(i1,F),@p) = ar*eval(1_1(i1,F),@p) by POLYNOM7:29
.= a*(p.i1) by A1, Th1;
A5: eval(br*(1_1(i2,F) *' 1_1(i3,F)),@p)
= br*eval(1_1(i2,F) *' 1_1(i3,F),@p) by POLYNOM7:29
.= br*(eval(1_1(i2,F),@p)*eval(1_1(i3,F),@p))
by POLYNOM2:25
.= b*((p.i2)*(p.i3)) by A3;
eval(Q,@(pZ)) =
eval(ar*1_1(i1,F),@p)- eval(br*1_1(i2,F)*' 1_1(i3,F),@p) by POLYNOM2:24
.= 0 by A2,A4,A5;
hence thesis by A2;
end;
given p be n-element XFinSequence of NAT,
Z be 0-element XFinSequence of NAT such that
A6: s=p & eval(Q,@(p^Z)) = 0;
A7: eval(1_1(i1,F),@p) = p.i1 &
eval(1_1(i2,F),@p) = p.i2 &
eval(1_1(i3,F),@p) = p.i3 by A1, Th1;
A8: eval(br*(1_1(i2,F) *' 1_1(i3,F)),@p)
= br*eval(1_1(i2,F) *' 1_1(i3,F),@p) by POLYNOM7:29
.= br*(eval(1_1(i2,F),@p)*eval(1_1(i3,F),@p))
by POLYNOM2:25
.= b*((p.i2)*(p.i3)) by A7;
A9:eval(ar*1_1(i1,F),@p) = ar*eval(1_1(i1,F),@p) by POLYNOM7:29
.= a*(p.i1) by A1, Th1;
set P=p^Z;
eval(Q,@P) =
eval(ar*1_1(i1,F),@p)- eval(br*1_1(i2,F)*' 1_1(i3,F),@p) by POLYNOM2:24
.=a*(p.i1) - (b*((p.i2)*(p.i3))) by A8,A9;
then a*p.i1 = b*(p.i2)*(p.i3) by A6;
hence s in D by A6;
end;
then D is diophantine;
hence thesis;
end;
end;
theorem Th10:
for a,b,c,i1,i2,i3 holds
{p: ex z be Nat st a*p.i1 = b*p.i2+ z*c*p.i3}
is diophantine Subset of n -xtuples_of NAT
proof
let a,b,c be Integer,i1,i2,i3 be Element of n;
set F=F_Real;
set n1=n+1;
set D = {p: ex z be Nat st a*p.i1 = b*p.i2+ z*c*p.i3};
D c= n -xtuples_of NAT
proof
let y be object;
assume y in D;
then ex p st
y=p & ex z be Nat st a*p.i1 = b*p.i2+ z*c*p.i3;
hence thesis by HILB10_2:def 5;
end;
then reconsider D as Subset of n -xtuples_of NAT;
per cases;
suppose n=0;
then D is diophantine Subset of n -xtuples_of NAT;
hence thesis;
end;
suppose A1: n<>0;
A2: n< n1 by NAT_1:13;
n in Segm n1 by A2,NAT_1:44;
then reconsider I=i1,J=i2,K=i3,N=n as Element of n1
by Th2;
reconsider ar=a,br=b,cr = c as integer Element of F by XREAL_0:def 1;
set Q=ar*1_1(I,F) - br*1_1(J,F)-cr*1_1(K,F)*'1_1(N,F);
reconsider Q
as INT -valued Polynomial of n+1,F_Real;
for s be object holds
s in D iff ex x be n-element XFinSequence of NAT,
y be 1-element XFinSequence of NAT st
s=x & eval(Q,@(x^y)) = 0
proof
let s be object;
thus s in D implies ex x be n-element XFinSequence of NAT,
y be 1-element XFinSequence of NAT st
s=x & eval(Q,@(x^y)) = 0
proof
assume s in D;
then consider p such that
A3: s=p & ex z be Nat st a*p.i1 = b*p.i2+ z*c*p.i3;
consider z be Nat such that
A4:a*p.i1 = b*p.i2+ z*c*p.i3 by A3;
reconsider z as Element of NAT by ORDINAL1:def 12;
reconsider Z=<%z%> as 1-element XFinSequence of NAT;
take p,Z;
set P=@(p^Z);
A5: len p = n by CARD_1:def 7;
then
A6: P.I = p.i1 & P.J = p.i2 & P.K = p.i3
by A1, AFINSQ_1:def 3;
A7: eval(1_1(I,F),P) = P.I & eval(1_1(J,F),P) = P.J &
eval(1_1(K,F),P) = P.K & eval(1_1(N,F),P) =P.N &
eval(1_(n1,F),P) = 1.F by Th1,POLYNOM2:21;
A8: eval(cr*(1_1(K,F) *' 1_1(N,F)),P)
= cr*eval(1_1(K,F) *' 1_1(N,F),P) by POLYNOM7:29
.= cr*(eval(1_1(K,F),P)*eval(1_1(N,F),P)) by POLYNOM2:25
.= c*(P.K * P.N) by A7;
eval(Q,P) =
eval(ar*1_1(I,F) - br*1_1(J,F),P) - eval(cr*1_1(K,F)*'1_1(N,F),P)
by POLYNOM2:24
.=eval(ar*1_1(I,F),P)-eval(br*1_1(J,F),P)-eval(cr*1_1(K,F)*'1_1(N,F),P)
by POLYNOM2:24
.=ar*eval(1_1(I,F),P)-eval(br*1_1(J,F),P)-eval(cr*1_1(K,F)*'1_1(N,F),P)
by POLYNOM7:29
.=ar*eval(1_1(I,F),P)-br*eval(1_1(J,F),P)-eval(cr*1_1(K,F)*'1_1(N,F),P)
by POLYNOM7:29
.= ar * P.I - br* P.J - c*P.K * P.N by A7,A8
.= a * (p.i1) - b* (p.i2) - c*(p.i3)*z by A6
.= 0 by A4;
hence thesis by A3;
end;
given p be n-element XFinSequence of NAT,
Z be 1-element XFinSequence of NAT such that
A9: s=p & eval(Q,@(p^Z)) = 0;
set P=@(p^Z);
len p = n by CARD_1:def 7;then
A10: P.I = p.i1 & P.J = p.i2 & P.K = p.i3
by A1, AFINSQ_1:def 3;
A11: eval(1_1(I,F),P) = P.I & eval(1_1(J,F),P) = P.J &
eval(1_1(K,F),P) = P.K & eval(1_1(N,F),P) =P.N &
eval(1_(n1,F),P) = 1.F by Th1,POLYNOM2:21;
A12: eval(cr*(1_1(K,F) *' 1_1(N,F)),P)
= cr*eval(1_1(K,F) *' 1_1(N,F),P) by POLYNOM7:29
.= cr*(eval(1_1(K,F),P)*eval(1_1(N,F),P))
by POLYNOM2:25
.= c*(P.K * P.N) by A11;
eval(Q,P) =
eval(ar*1_1(I,F) - br*1_1(J,F),P) - eval(cr*1_1(K,F)*'1_1(N,F),P)
by POLYNOM2:24
.=eval(ar*1_1(I,F),P)-eval(br*1_1(J,F),P) - eval(cr*1_1(K,F)*'1_1(N,F),P)
by POLYNOM2:24
.= ar*eval(1_1(I,F),P)-eval(br*1_1(J,F),P)-eval(cr*1_1(K,F)*'1_1(N,F),P)
by POLYNOM7:29
.= ar * eval(1_1(I,F),P) - br*eval(1_1(J,F),P) - c*(P.K * P.N)
by A12,POLYNOM7:29
.= a * (p.i1) - b* (p.i2) - c*(p.i3)*(P.N) by A10,A11;
then a*p.i1 = b*p.i2+ (P.N)*c*p.i3 by A9;
hence s in D by A9;
end;
then D is diophantine;
hence thesis;
end;
end;
scheme IntersectionDiophantine{n()->Nat,P,Q[XFinSequence]}:
{p where p is n()-element XFinSequence of NAT: P[p] & Q[p]}
is diophantine Subset of n() -xtuples_of NAT
provided
A1:{p where p is n()-element XFinSequence of NAT: P[p]}
is diophantine Subset of n() -xtuples_of NAT
and
A2:{p where p is n()-element XFinSequence of NAT: Q[p]}
is diophantine Subset of n() -xtuples_of NAT
proof
reconsider PF={p where p is n()-element XFinSequence of NAT: P[p]} as
diophantine Subset of n() -xtuples_of NAT by A1;
reconsider QF={p where p is n()-element XFinSequence of NAT: Q[p]} as
diophantine Subset of n() -xtuples_of NAT by A2;
set PQ = {p where p is n()-element XFinSequence of NAT: P[p] & Q[p]};
A3: PF /\QF c= PQ
proof
let x be object;
assume x in PF /\QF;
then A4: x in PF & x in QF by XBOOLE_0:def 4;
then consider p be n()-element XFinSequence of NAT such that
A5: x =p & P[p] ;
ex p be n()-element XFinSequence of NAT st x =p & Q[p] by A4;
hence thesis by A5;
end;
A6: PQ c= PF
proof
let x be object;
assume x in PQ;
then ex p be n()-element XFinSequence of NAT st x =p &( P[p] & Q[p]);
hence thesis;
end;
PQ c= QF
proof
let x be object;
assume x in PQ;
then ex p be n()-element XFinSequence of NAT st x =p &( P[p] & Q[p]);
hence thesis;
end;
then PQ c= PF /\QF by A6, XBOOLE_1:19;
hence thesis by A3, XBOOLE_0:def 10;
end;
scheme Substitution{P[Nat,Nat,natural object,Nat,Nat,Nat],
F(Nat,Nat,Nat)->natural object}:
for i1,i2,i3,i4,i5 holds {p: P[p.i1,p.i2,F(p.i3,p.i4,p.i5),p.i3,p.i4,p.i5]}
is diophantine Subset of n -xtuples_of NAT
provided
A1: for i1,i2,i3,i4,i5,i6 holds {p: P[p.i1,p.i2,p.i3,p.i4,p.i5,p.i6]}
is diophantine Subset of n -xtuples_of NAT
and
A2:for i1,i2,i3,i4 holds {p: F(p.i1,p.i2,p.i3) = p.i4}
is diophantine Subset of n -xtuples_of NAT
proof
let n,i1,i2,i3,i4,i5;set n1=n+1;
set T={p: P[p.i1,p.i2,F(p.i3,p.i4,p.i5),p.i3,p.i4,p.i5]};
per cases;
suppose A3:n=0;
T c= n -xtuples_of NAT
proof
let x be object;assume x in T;
then ex p be n-element XFinSequence of NAT st
x= p & P[p.i1,p.i2,F(p.i3,p.i4,p.i5),p.i3,p.i4,p.i5];
hence thesis by HILB10_2:def 5;
end;
hence thesis by A3;
end;
suppose A4:n<>0;
A5:n < n1 by NAT_1:13;
then n in Segm n1 by NAT_1:44;
then reconsider I1=i1,I2=i2,I3=i3,I4=i4,I5=i5,N=n as Element of n1 by Th2;
reconsider P = {p where p is n1-element XFinSequence of NAT:
P[p.I1,p.I2,p.N,p.I3,p.I4,p.I5]}
as diophantine Subset of n1 -xtuples_of NAT by A1;
reconsider F = {p where p is n1-element XFinSequence of NAT:
F(p.I3,p.I4,p.I5)=p.N}
as diophantine Subset of n1 -xtuples_of NAT by A2;
reconsider PF=P/\F as Subset of n1 -xtuples_of NAT;
reconsider PFk={p|n where p is n1-element XFinSequence of NAT: p in PF} as
diophantine Subset of n -xtuples_of NAT by Th5,A5;
A6:PFk c= T
proof
let x be object;
assume x in PFk;
then consider p be n1-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 be n1-element XFinSequence of NAT st p=q &
P[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 be n1-element XFinSequence of NAT st
p=q & F(q.I3,q.I4,q.I5)=q.N;
len p = n1 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 thesis by A8,A9,A7;
end;
T c= PFk
proof
let x be object;assume x in T;
then consider p be n-element XFinSequence of NAT such that
A10: x= p & P[p.i1,p.i2,F(p.i3,p.i4,p.i5),p.i3,p.i4,p.i5];
reconsider FF=F(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: pZ|n=p & pZ.n = FF by AFINSQ_1:57;
then p.i1 = pZ.i1 & p.i2 = pZ.i2 & p.i3 = pZ.i3 & p.i4 = pZ.i4 &
p.i5 = pZ.i5 by A4,Th4;
then pZ in F & pZ in P by A10,A11;
then pZ in P/\F by XBOOLE_0:def 4;
hence thesis by A11,A10;
end;
hence thesis by A6,XBOOLE_0:def 10;
end;
end;
scheme SubstitutionInt{P[Nat,Nat,Integer],F(Nat,Nat,Nat)->Integer}:
for i1,i2,i3,i4,i5 holds {p: P[p.i1,p.i2,F(p.i3,p.i4,p.i5)]}
is diophantine Subset of n -xtuples_of NAT
provided
A1: for i1,i2,i3,a holds {p: P[p.i1,p.i2,a*(p.i3)]}
is diophantine Subset of n -xtuples_of NAT
and
A2: for i1,i2,i3,i4,a holds {p: F(p.i1,p.i2,p.i3) = a*(p.i4)}
is diophantine Subset of n -xtuples_of NAT
proof
deffunc AbsF(Nat,Nat,Nat) =|.F($1,$2,$3).|;
defpred plusP[Nat,Nat,natural object,Nat,Nat,Nat] means
P[$1,$2,1*$3] & F($4,$5,$6)>=0;
defpred minusP[Nat,Nat,natural object,Nat,Nat,Nat] means
P[$1,$2,(-1)*$3]&F($4,$5,$6)<=0;
A3: for i1,i2,i3,i4,i5,i6 holds {p: plusP[p.i1,p.i2,p.i3,p.i4,p.i5,p.i6]}
is diophantine Subset of n -xtuples_of NAT
proof
let i1,i2,i3,i4,i5,i6;
set M={p: plusP[p.i1,p.i2,p.i3,p.i4,p.i5,p.i6]};
per cases;
suppose A4:n=0;
M c= n -xtuples_of NAT
proof
let x be object;assume x in M;
then ex p be n-element XFinSequence of NAT st
x= p & plusP[p.i1,p.i2,p.i3,p.i4,p.i5,p.i6];
hence thesis by HILB10_2:def 5;
end;
hence thesis by A4;
end;
suppose A5:n<>0;set n1=n+1;
A6:n < n1 by NAT_1:13;
then n in Segm n1 by NAT_1:44;
then reconsider I1=i1,I2=i2,I3=i3,I4=i4,I5=i5,I6=i6,N=n as Element of n1
by Th2;
defpred pP[XFinSequence of NAT] means P[$1.I1,$1.I2,(1)*($1.I3)];
reconsider P= {p where p is n1-element XFinSequence of NAT: pP[p]}
as diophantine Subset of n1 -xtuples_of NAT by A1;
reconsider F = {p where p is n1-element XFinSequence of NAT:
F(p.I4,p.I5,p.I6)=(1)*p.N}
as diophantine Subset of n1 -xtuples_of NAT by A2;
reconsider PF=P/\F as Subset of n1 -xtuples_of NAT;
reconsider PFk={p|n where p is n1-element XFinSequence of NAT: p in PF}
as diophantine Subset of n -xtuples_of NAT by Th5,A6;
A7:PFk c= M
proof
let x be object;
assume x in PFk;
then consider p be n1-element XFinSequence of NAT such that
A8: x= p|n & p in PF;
p in P by A8,XBOOLE_0:def 4;then
A9: ex q be n1-element XFinSequence of NAT st p=q & pP[q];
p in F by A8,XBOOLE_0:def 4;then
A10: ex q be n1-element XFinSequence of NAT st p=q &
F(q.I4,q.I5,q.I6)=(1)*q.N;
len p = n1 by CARD_1:def 7;then
len (p|n) = n by A6,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 & pn.i6 = p.I6 by A5,Th4;
hence thesis by A8,A9,A10;
end;
M c= PFk
proof
let x be object;assume x in M;
then consider p be n-element XFinSequence of NAT such that
A11: x= p & plusP[p.i1,p.i2,p.i3,p.i4,p.i5,p.i6];
reconsider FF=F(p.i4,p.i5,p.i6) as Element of NAT by A11,INT_1:3;
reconsider Z=<%FF%> as 1-element XFinSequence of NAT;
set pZ=p^Z;
A12: len p = n by CARD_1:def 7;
then A13: pZ|n=p & pZ.n = FF by AFINSQ_1:57;
then p.i1 = pZ.i1 & p.i2 = pZ.i2 & p.i3 = pZ.i3 & p.i4 = pZ.i4 &
p.i5 = pZ.i5 & p.i6 = pZ.i6 by A5,Th4;
then F(pZ.i4,pZ.i5,pZ.i6)=(1)*pZ.n & P[pZ.i1,pZ.i2,(1)*pZ.i3]
by A11;
then pZ in F & pZ in P;
then pZ in P/\F by XBOOLE_0:def 4;
hence thesis by A13,A11;
end;
hence thesis by A7,XBOOLE_0:def 10;
end;
end;
A14: for i1,i2,i3,i4,i5,i6 holds {p: minusP[p.i1,p.i2,p.i3,p.i4,p.i5,p.i6]}
is diophantine Subset of n -xtuples_of NAT
proof
let i1,i2,i3,i4,i5,i6;
set M={p: minusP[p.i1,p.i2,p.i3,p.i4,p.i5,p.i6]};
per cases;
suppose A15:n=0;
M c= n -xtuples_of NAT
proof
let x be object;assume x in M;
then ex p be n-element XFinSequence of NAT st
x= p & minusP[p.i1,p.i2,p.i3,p.i4,p.i5,p.i6];
hence thesis by HILB10_2:def 5;
end;
hence thesis by A15;
end;
suppose A16:n<>0;set n1=n+1;
A17:n < n1 by NAT_1:13;
then n in Segm n1 by NAT_1:44;
then
reconsider I1=i1,I2=i2,I3=i3,I4=i4,I5=i5,I6=i6,N=n as Element of n1
by Th2;
defpred mP[XFinSequence of NAT] means P[$1.I1,$1.I2,(-1)*($1.I3)];
reconsider P= {p where p is n1-element XFinSequence of NAT: mP[p]}
as diophantine Subset of n1 -xtuples_of NAT by A1;
reconsider F = {p where p is n1-element XFinSequence of NAT:
F(p.I4,p.I5,p.I6)=(-1)*p.N}
as diophantine Subset of n1 -xtuples_of NAT by A2;
reconsider PF=P/\F as Subset of n1 -xtuples_of NAT;
reconsider PFk = {p|n where p is n1-element XFinSequence of NAT: p in PF}
as diophantine Subset of n -xtuples_of NAT by Th5,A17;
A18:PFk c= M
proof
let x be object;
assume x in PFk;
then consider p be n1-element XFinSequence of NAT such that
A19: x= p|n & p in PF;
p in P by A19,XBOOLE_0:def 4;then
A20: ex q be n1-element XFinSequence of NAT st p=q & mP[q];
p in F by A19,XBOOLE_0:def 4;then
A21: ex q be n1-element XFinSequence of NAT st p=q &
F(q.I4,q.I5,q.I6)=(-1)*q.N;
len p = n1 by CARD_1:def 7;then
len (p|n) = n by A17,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 & pn.i6 = p.I6 by A16,Th4;
hence thesis by A19,A20,A21;
end;
M c= PFk
proof
let x be object;assume x in M;
then consider p be n-element XFinSequence of NAT such that
A22: x= p & minusP[p.i1,p.i2,p.i3,p.i4,p.i5,p.i6];
reconsider FF=-F(p.i4,p.i5,p.i6) as Element of NAT by A22,INT_1:3;
reconsider Z=<%FF%> as 1-element XFinSequence of NAT;
set pZ=p^Z;
len p = n by CARD_1:def 7;
then A23: pZ|n=p & pZ.n = FF by AFINSQ_1:57;
then p.i1 = pZ.i1 & p.i2 = pZ.i2 & p.i3 = pZ.i3 & p.i4 = pZ.i4 &
p.i5 = pZ.i5 & p.i6 = pZ.i6 by A16,Th4;
then F(pZ.i4,pZ.i5,pZ.i6)=(-1)*pZ.n & P[pZ.i1,pZ.i2,(-1)*pZ.i3]
by A22;
then pZ in F & pZ in P;
then pZ in P/\F by XBOOLE_0:def 4;
hence thesis by A23,A22;
end;
hence thesis by A18,XBOOLE_0:def 10;
end;
end;
A24:
for i1,i2,i3,i4 holds {p: AbsF(p.i1,p.i2,p.i3) = p.i4}
is diophantine Subset of n -xtuples_of NAT
proof
let i1,i2,i3,i4;
defpred plusF[XFinSequence of NAT] means F($1.i1,$1.i2,$1.i3) = 1*($1.i4);
defpred minusF[XFinSequence of NAT] means F($1.i1,$1.i2,$1.i3) =
(-1)*($1.i4);
A25:{p: plusF[p]} is diophantine Subset of n -xtuples_of NAT by A2;
A26:{p: minusF[p]} is diophantine Subset of n -xtuples_of NAT by A2;
A27:{p: plusF[p] or minusF[p]} is diophantine Subset of n -xtuples_of NAT
from UnionDiophantine(A25,A26);
defpred pmF[XFinSequence of NAT] means plusF[$1] or minusF[$1];
defpred absF[XFinSequence of NAT] means AbsF($1.i1,$1.i2,$1.i3) = $1.i4;
A28: for p holds pmF[p] iff absF[p]
proof
let p;
thus pmF[p] implies absF[p]
proof
assume A29:pmF[p];
per cases by A29;
suppose plusF[p];
hence thesis by ABSVALUE:def 1;
end;
suppose minusF[p];
then AbsF(p.i1,p.i2,p.i3) = -((-1)*p.i4) by ABSVALUE:30;
hence thesis;
end;
end;
assume A30: absF[p];
per cases;
suppose F(p.i1,p.i2,p.i3)>=0;
hence thesis by A30,ABSVALUE:def 1;
end;
suppose F(p.i1,p.i2,p.i3)<0;
then AbsF(p.i1,p.i2,p.i3) = - F(p.i1,p.i2,p.i3) by ABSVALUE:def 1;
hence thesis by A30;
end;
end;
{p: pmF[p]}={q: absF[q]} from Eq(A28);
hence thesis by A27;
end;
A31:for i1,i2,i3,i4,i5 holds
{p: plusP[p.i1,p.i2,AbsF(p.i3,p.i4,p.i5),p.i3,p.i4,p.i5]}
is diophantine Subset of n -xtuples_of NAT from Substitution(A3,A24);
A32:for i1,i2,i3,i4,i5 holds
{p: minusP[p.i1,p.i2,AbsF(p.i3,p.i4,p.i5),p.i3,p.i4,p.i5]}
is diophantine Subset of n -xtuples_of NAT from Substitution(A14,A24);
let n,i1,i2,i3,i4,i5;
defpred pP[XFinSequence of NAT] means
plusP[$1.i1,$1.i2,AbsF($1.i3,$1.i4,$1.i5),$1.i3,$1.i4,$1.i5];
defpred mP[XFinSequence of NAT] means
minusP[$1.i1,$1.i2,AbsF($1.i3,$1.i4,$1.i5),$1.i3,$1.i4,$1.i5];
defpred pmP[XFinSequence of NAT] means pP[$1] or mP[$1];
A33: {p: pP[p]} is diophantine Subset of n -xtuples_of NAT by A31;
A34: {p: mP[p]} is diophantine Subset of n -xtuples_of NAT by A32;
A35: {p: pP[p] or mP[p]}
is diophantine Subset of n -xtuples_of NAT from UnionDiophantine(A33,A34);
defpred PF[XFinSequence of NAT] means P[$1.i1,$1.i2,F($1.i3,$1.i4,$1.i5)];
A36: for p holds pmP[p] iff PF[p]
proof
let p;
thus pmP[p] implies PF[p]
proof
assume A37:pP[p] or mP[p];
per cases by A37;
suppose pP[p];
hence thesis by ABSVALUE:def 1;
end;
suppose A38: mP[p];
then AbsF(p.i3,p.i4,p.i5)= - F(p.i3,p.i4,p.i5) by ABSVALUE:30;
hence thesis by A38;
end;
end;
assume A39: PF[p];
per cases;
suppose F(p.i3,p.i4,p.i5)>=0;
hence thesis by A39, ABSVALUE:def 1;
end;
suppose A40: F(p.i3,p.i4,p.i5)<0;
then AbsF(p.i3,p.i4,p.i5)= - F(p.i3,p.i4,p.i5) by ABSVALUE:def 1;
hence thesis by A39,A40;
end;
end;
{p: pmP[p]} ={q: PF[q]} from Eq(A36);
hence thesis by A35;
end;
theorem Th11:
for a,b,c,d,i1,i2,i3 holds
{p: a*p.i1 = b*p.i2+c*p.i3+d} is diophantine Subset of n -xtuples_of NAT
proof
let a,b,c,d be Integer,i1,i2,i3;
set F=F_Real;
reconsider ar=a,br=b,cr = c,dr = d as integer Element of F by XREAL_0:def 1;
set D = {p: a*p.i1 = b*p.i2+c*p.i3+d};
D c= n -xtuples_of NAT
proof
let y be object;
assume y in D;
then ex p st y=p & a*p.i1 = b*p.i2+c*p.i3+d;
hence thesis by HILB10_2:def 5;
end;
then reconsider D as Subset of n -xtuples_of NAT;
per cases;
suppose n=0;
then D is diophantine Subset of n -xtuples_of NAT;
hence thesis;
end;
suppose A1: n<>0;
set Q= ar*1_1(i1,F) - br*1_1(i2,F)- cr*1_1(i3,F) -dr*1_(n,F);
reconsider Q as INT -valued Polynomial of n+0,F_Real;
for s be object holds
s in D iff ex x be n-element XFinSequence of NAT,
y be 0-element XFinSequence of NAT st
s=x & eval(Q,@(x^y)) = 0
proof
let s be object;
thus s in D implies ex x be n-element XFinSequence of NAT,
y be 0-element XFinSequence of NAT st
s=x & eval(Q,@(x^y)) = 0
proof
assume s in D;
then consider p such that
A2: s=p & a*p.i1 = b*p.i2+c*p.i3+d;
reconsider Z=<%>NAT as 0-element XFinSequence of NAT;
take pZ=p,Z;
A3: eval(dr*1_(n,F),@p) = dr*eval(1_(n,F),@p) by POLYNOM7:29
.= dr* 1.F by POLYNOM2:21
.= d;
A4:eval(ar*1_1(i1,F),@p) = ar*eval(1_1(i1,F),@p) by POLYNOM7:29
.= a*(p.i1) by A1,Th1;
A5:eval(br*1_1(i2,F),@p) =
br*eval(1_1(i2,F),@p) by POLYNOM7:29
.= b*(p.i2) by A1,Th1;
A6:eval(cr*1_1(i3,F),@p) =
cr*eval(1_1(i3,F),@p) by POLYNOM7:29
.= c*(p.i3) by A1,Th1;
eval(Q,@(p^Z)) = eval(ar*1_1(i1,F) -
br*1_1(i2,F)- cr*1_1(i3,F),@p) -eval(dr*1_(n,F),@p) by POLYNOM2:24
.= eval(ar*1_1(i1,F) - br*1_1(i2,F),@p)
- eval(cr*1_1(i3,F),@p)-eval(dr*1_(n,F),@p) by POLYNOM2:24
.= eval(ar*1_1(i1,F),@p) - eval(br*1_1(i2,F),@p)
- eval(cr*1_1(i3,F),@p)-eval(dr*1_(n,F),@p) by POLYNOM2:24
.= 0 by A2,A3,A4,A5,A6;
hence thesis by A2;
end;
given p be n-element XFinSequence of NAT,
Z be 0-element XFinSequence of NAT such that
A7: s=p & eval(Q,@(p^Z)) = 0;
A8: eval(dr*1_(n,F),@p) = dr*eval(1_(n,F),@p) by POLYNOM7:29
.= dr* 1.F by POLYNOM2:21
.= d;
A9:eval(ar*1_1(i1,F),@p) = ar*eval(1_1(i1,F),@p) by POLYNOM7:29
.= a*(p.i1) by A1,Th1;
A10:eval(br*1_1(i2,F),@p) =
br*eval(1_1(i2,F),@p) by POLYNOM7:29
.= b*(p.i2) by A1,Th1;
A11:eval(cr*1_1(i3,F),@p) =
cr*eval(1_1(i3,F),@p) by POLYNOM7:29
.= c*(p.i3) by A1,Th1;
eval(Q,@(p^Z))
= eval(ar*1_1(i1,F) - br*1_1(i2,F)- cr*1_1(i3,F),@p)
-eval(dr*1_(n,F),@p) by POLYNOM2:24
.= eval(ar*1_1(i1,F) - br*1_1(i2,F),@p)
- eval(cr*1_1(i3,F),@p)-eval(dr*1_(n,F),@p) by POLYNOM2:24
.= eval(ar*1_1(i1,F),@p) - eval(br*1_1(i2,F),@p)
- eval(cr*1_1(i3,F),@p)-eval(dr*1_(n,F),@p) by POLYNOM2:24
.= a*(p.i1) - b*(p.i2) - c*(p.i3) -d by A8,A9,A10,A11;
then a*p.i1 = b*p.i2+c*p.i3+d by A7;
hence thesis by A7;
end;
then D is diophantine;
hence thesis;
end;
end;
theorem Th12:
for a,i1,i2 holds
{p: p.i1 = a*p.i2} is diophantine Subset of n -xtuples_of NAT
proof
let a be Integer,i1,i2;
defpred P[XFinSequence of NAT] means $1.i1 = a * $1.i2;
defpred Q[XFinSequence of NAT] means 1 * ($1.i1) = a * $1.i2+0;
A1: {p: p.i1 = a*p.i2 } c= {q: 1*q.i1 = a*q.i2+0}
proof
let y be object;
assume y in {p: p.i1 = a*p.i2 };
then consider p be n-element XFinSequence of NAT such that
A2:y=p & p.i1 = a*p.i2;
1*p.i1 = a*p.i2+0 by A2;
hence thesis by A2;
end;
{q: 1*q.i1 = a*q.i2+0} c= {p: p.i1 = a*p.i2 }
proof
let y be object;
assume y in {q: 1*q.i1 = a*q.i2+0};
then ex q be n-element XFinSequence of NAT st
y=q & 1*q.i1 = a*q.i2+0;
hence thesis;
end;
then {q: 1*q.i1 = a*q.i2+0} = {p: p.i1 = a*p.i2 } by A1,XBOOLE_0:def 10;
hence thesis by Th6;
end;
theorem Th13:
for a,b,i1 holds
{p: a* p.i1 = b} is diophantine Subset of n -xtuples_of NAT
proof
let a,b be Integer,i1;
set i2 = the Element of n;
defpred P[XFinSequence of NAT] means a*($1.i1) = b;
defpred Q[XFinSequence of NAT] means a*($1.i1) = 0 * ($1.i2)+b;
A1:for p holds P[p] iff Q[p];
{p: P[p]} = {q:Q[q]} from Eq(A1);
hence thesis by Th6;
end;
theorem Th14:
for a,i1 holds
{p: p.i1 = a} is diophantine Subset of n -xtuples_of NAT
proof
let a be Integer,i1;
set i2 = the Element of n;
defpred P[XFinSequence of NAT] means $1.i1 = a;
defpred Q[XFinSequence of NAT] means 1*($1.i1) = 0 * ($1.i2)+a;
A1:for p holds P[p] iff Q[p];
{p: P[p]} = {q: Q[q]} from Eq(A1);
hence thesis by Th6;
end;
theorem
for a,b,i1,i2 holds
{p: p.i1 = a*p.i2+b} is diophantine Subset of n -xtuples_of NAT
proof
let a,b be Integer,i1,i2;
defpred P[XFinSequence of NAT] means $1.i1 = a * $1.i2 +b;
defpred Q[XFinSequence of NAT] means 1 * ($1.i1) = a * $1.i2+b;
A1:for p holds P[p] iff Q[p];
{p: P[p]} = {q:Q[q]} from Eq(A1);
hence thesis by Th6;
end;
theorem
for a,b,c,i1,i2 holds
{p: a* p.i1 <> b*p.i2+c} is diophantine Subset of n -xtuples_of NAT
proof
let a,b,c be Integer,i1,i2;
defpred P[XFinSequence of NAT] means a* $1.i1 > b*$1.i2+c;
defpred Q[XFinSequence of NAT] means a* $1.i1+(-c) < b*$1.i2;
defpred R[XFinSequence of NAT] means P[$1] or Q[$1];
defpred S[XFinSequence of NAT] means a* $1.i1 <> b*$1.i2+c;
A1:{p: P[p]} is diophantine Subset of n -xtuples_of NAT by Th7;
A2:{p: Q[p]} is diophantine Subset of n -xtuples_of NAT by Th7;
A3: {p: P[p] or Q[p]} is diophantine Subset of n -xtuples_of NAT
from UnionDiophantine(A1,A2);
A4:R[p] iff S[p]
proof
thus R[p] implies S[p];
assume S[p];
then a* p.i1 > b*p.i2+c or a* p.i1 < b*p.i2+c by XXREAL_0:1;
then a* p.i1 > b*p.i2+c or a* p.i1-c < b*p.i2 by XREAL_1:19;
hence thesis;
end;
{p: R[p]} = {q: S[q]} from Eq(A4);
hence thesis by A3;
end;
theorem Th17:
for a,b,i1,i2,i3 holds
{p: a*p.i1 > b*p.i2*p.i3} is diophantine Subset of n -xtuples_of NAT
proof
let a,b,i1,i2,i3;
defpred P[Nat,Nat,Integer] means a*$1 > $3+0;
deffunc F(Nat,Nat,Nat)= b*$2*$3;
defpred P1[XFinSequence of NAT] means a*$1.i1 > b*$1.i2*$1.i3+0;
defpred P2[XFinSequence of NAT] means a*$1.i1 > b*$1.i2*$1.i3;
A1: for n for i1,i2,i3,c holds {p: P[p.i1,p.i2,c*(p.i3)]}
is diophantine Subset of n -xtuples_of NAT by Th7;
A2: for n for i1,i2,i3,i4,c holds {p: F(p.i1,p.i2,p.i3) = c*(p.i4)}
is diophantine Subset of n -xtuples_of NAT by Th9;
A3: for n for i1,i2,i3,i4,i5 holds {p: P[p.i1,p.i2,F(p.i3,p.i4,p.i5)]}
is diophantine Subset of n -xtuples_of NAT from SubstitutionInt(A1,A2);
A4: for p holds P1[p] iff P2[p];
{p: P1[p]} ={q: P2[q]} from Eq(A4);
hence thesis by A3;
end;
theorem Th18:
for a,b,c,i1,i2,i3 holds
{p: a*p.i1 < b*p.i2 + c*p.i3} is diophantine Subset of n -xtuples_of NAT
proof
let a,b,c,i1,i2,i3;
defpred P[Nat,Nat,Integer] means a*$1 +0 < $3;
deffunc F(Nat,Nat,Nat)= b*$2+c*$3+0;
defpred P1[XFinSequence of NAT] means a*$1.i1+0 < b*$1.i2+c* $1.i3+0;
defpred P2[XFinSequence of NAT] means a*$1.i1 < b*$1.i2+c*$1.i3;
A1: for n for i1,i2,i3,d holds {p: P[p.i1,p.i2,d*(p.i3)]}
is diophantine Subset of n -xtuples_of NAT by Th7;
A2: for n for i1,i2,i3,i4,d holds {p: F(p.i1,p.i2,p.i3) = d*(p.i4)}
is diophantine Subset of n -xtuples_of NAT by Th11;
A3:for n for i1,i2,i3,i4,i5 holds {p: P[p.i1,p.i2,F(p.i3,p.i4,p.i5)]}
is diophantine Subset of n -xtuples_of NAT from SubstitutionInt(A1,A2);
A4: for p holds P1[p] iff P2[p];
{p: P1[p]} ={q: P2[q]} from Eq(A4);
hence thesis by A3;
end;
theorem Th19:
for a,b,c,i1,i2,i3 holds
{p: a* p.i1 = b*p.i2-' c*p.i3} is diophantine Subset of n -xtuples_of NAT
proof
let a,b,c be Integer,i1,i2,i3;
defpred P[XFinSequence of NAT] means a*$1.i1 = b*$1.i2+(- c)*$1.i3+0;
defpred Q[XFinSequence of NAT] means b*$1.i2>= c*$1.i3+0;
defpred R[XFinSequence of NAT] means a*$1.i1 = 0*$1.i2*$1.i3;
defpred S[XFinSequence of NAT] means b*$1.i2+0 < c*$1.i3;
defpred PQ[XFinSequence of NAT] means P[$1] & Q[$1];
A1:{p: P[p]} is diophantine Subset of n -xtuples_of NAT by Th11;
A2:{p: Q[p]} is diophantine Subset of n -xtuples_of NAT by Th8;
{p: P[p] & Q[p]} is diophantine Subset of n -xtuples_of NAT
from IntersectionDiophantine(A1,A2);
then A3: {p: PQ[p]} is diophantine Subset of n -xtuples_of NAT;
defpred RS[XFinSequence of NAT] means R[$1] & S[$1];
A4:{p: R[p]} is diophantine Subset of n -xtuples_of NAT by Th9;
A5:{p: S[p]} is diophantine Subset of n -xtuples_of NAT by Th7;
{p: R[p] & S[p]} is diophantine Subset of n -xtuples_of NAT
from IntersectionDiophantine(A4,A5);
then A6: {p: RS[p]} is diophantine Subset of n -xtuples_of NAT;
defpred PQRS[XFinSequence of NAT] means PQ[$1] or RS[$1];
defpred T[XFinSequence of NAT] means a* $1.i1 = b*$1.i2-' c*$1.i3;
A7: {p:PQ[p] or RS[p]} is diophantine Subset of n -xtuples_of NAT
from UnionDiophantine(A3,A6);
A8: PQRS[p] iff T[p]
proof
thus PQRS[p] implies T[p]
proof
assume PQRS[p];
then (a* p.i1 = b*p.i2+(- c)*p.i3+0 & b*p.i2- c*p.i3>=0) or
(a*p.i1 = 0*p.i2*p.i3 & b*p.i2- c*p.i3 < 0) by XREAL_1:48,49;
hence thesis by XREAL_0:def 2;
end;
assume T[p];
then (a* p.i1 = b*p.i2 -c*p.i3+0 & b*p.i2- c*p.i3>=0) or
(a* p.i1 = 0 & b*p.i2- c*p.i3<0) by XREAL_0:def 2;
hence thesis by XREAL_1:48,49;
end;
{p: PQRS[p]} = {q: T[q]} from Eq(A8);
hence thesis by A7;
end;
theorem Th20:
for a,b,c,i1,i2,i3 holds
{p: a* p.i1 = b*p.i2-' c} is diophantine Subset of n -xtuples_of NAT
proof
let a,b,c;
defpred P[Nat,Nat,Integer] means a* $1 = b*$2-' $3;
A1: for n for i1,i2,i3,d holds {p: P[p.i1,p.i2,d*(p.i3)]}
is diophantine Subset of n -xtuples_of NAT by Th19;
deffunc F(Nat,Nat,Nat) = c;
A2: for n for i1,i2,i3,i4,d holds {p: F(p.i1,p.i2,p.i3) = d*(p.i4)}
is diophantine Subset of n -xtuples_of NAT by Th13;
for n for i1,i2,i3,i4,i5 holds {p: P[p.i1,p.i2,F(p.i3,p.i4,p.i5)]}
is diophantine Subset of n -xtuples_of NAT from SubstitutionInt(A1,A2);
hence thesis;
end;
Lm1:
for x,y be Integer
for D be Nat holds x^2 - D*y^2 = 1 iff [x,y] is Pell's_solution of D
proof
let x,y be Integer;
let D be Nat;
A1:[x,y]`1 = x & [x,y]`2 =y;
x in INT & y in INT by INT_1:def 2;
then [x,y] in [:INT,INT:] by ZFMISC_1:87;
hence x^2 - D*y^2 = 1 implies [x,y] is Pell's_solution of D
by A1,PELLS_EQ:def 1;
assume [x,y] is Pell's_solution of D;
hence thesis by PELLS_EQ:def 1,A1;
end;
theorem Th21:
for a,b,c,i1,i2,i3 holds
{p: a*p.i1,b*p.i2 are_congruent_mod c*p.i3}
is diophantine Subset of n -xtuples_of NAT
proof
let a,b,c,i1,i2,i3;
defpred P[XFinSequence of NAT] means ex z be Nat st a*$1.i1
= b*$1.i2+ z*c*$1.i3;
defpred Q[XFinSequence of NAT] means ex z be Nat st b*$1.i2
= a*$1.i1+ z*c*$1.i3;
A1:{p:P[p]} is diophantine Subset of n -xtuples_of NAT by Th10;
A2:{p:Q[p]} is diophantine Subset of n -xtuples_of NAT by Th10;
A3:{p:P[p] or Q[p]}is diophantine Subset of n -xtuples_of NAT
from UnionDiophantine(A1,A2);
set PP={p: a*p.i1,b*p.i2 are_congruent_mod c*p.i3};
A4:PP c= {p:P[p] or Q[p]}
proof
let x be object;
assume x in PP;
then consider p such that
A5:x= p & a*p.i1,b*p.i2 are_congruent_mod c*p.i3;
consider i be Integer such that
A6: (c*p.i3)*i = a*p.i1-b*p.i2 by A5,INT_1:def 5;
per cases;
suppose i>=0;
then reconsider i as Element of NAT by INT_1:3;
a*p.i1=b*p.i2+i*c*p.i3 by A6;
hence thesis by A5;
end;
suppose i<0;
then reconsider I=- i as Element of NAT by INT_1:3;
A7: a*p.i1=b*p.i2+i*c*p.i3 by A6;
a*p.i1=b*p.i2+(-I)*c*p.i3 by A7;
then b*p.i2=a*p.i1+I*c*p.i3;
hence thesis by A5;
end;
end;
{p:P[p] or Q[p]} c= PP
proof
let x be object;
assume x in {p:P[p] or Q[p]};
then consider p such that
A8:x= p & (P[p] or Q[p]);
per cases by A8;
suppose P[p];
then consider z be Nat such that A9: a*p.i1 = b*p.i2+ z*c*p.i3;
z*(c*p.i3) = a*p.i1 - b*p.i2 by A9;
then a*p.i1,b*p.i2 are_congruent_mod c*p.i3 by INT_1:def 5;
hence x in PP by A8;
end;
suppose Q[p];
then consider z be Nat such that A10: b*p.i2 = a*p.i1+ z*c*p.i3;
(-z)*(c*p.i3) = a*p.i1 - b*p.i2 by A10;
then a*p.i1, b*p.i2 are_congruent_mod c*p.i3 by INT_1:def 5;
hence x in PP by A8;
end;
end;
hence thesis by A3,A4,XBOOLE_0:def 10;
end;
theorem Th22:
for a,b,c,i1,i2,i3 holds
{p: [a*p.i1,b*p.i2] is Pell's_solution of (((c*p.i3)^2) -' 1)}
is diophantine Subset of n -xtuples_of NAT
proof
let a,b,c be Integer; let i1,i2,i3;
set n5=n+5;
set WW = {p: [a*p.i1,b*p.i2] is Pell's_solution of (((c*p.i3)^2) -' 1)};
WW c= n -xtuples_of NAT
proof
let y be object;
assume y in WW;
then ex p st
y=p & [a*p.i1,b*p.i2] is Pell's_solution of (((c*p.i3)^2) -' 1);
hence thesis by HILB10_2:def 5;
end;
then reconsider WW as Subset of n -xtuples_of NAT;
per cases;
suppose n=0;
then WW is diophantine Subset of n -xtuples_of NAT;
hence thesis;
end;
suppose A1: n<>0;
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 P[XFinSequence of NAT] means 1* $1.N = a^2*$1.I1*$1.I1;
A2: {p where p is (n+5)-element XFinSequence of NAT:P[p]}
is diophantine Subset of n5 -xtuples_of NAT by Th9;
defpred Q[XFinSequence of NAT] means 1* $1.N1 = c^2*$1.I3*$1.I3;
A3: {p where p is (n+5)-element XFinSequence of NAT:Q[p]}
is diophantine Subset of n5 -xtuples_of NAT by Th9;
defpred R[XFinSequence of NAT] means 1* $1.N2 = 1*$1.N1 -'1;
A4: {p where p is (n+5)-element XFinSequence of NAT:R[p]} is
diophantine Subset of n5 -xtuples_of NAT by Th20;
defpred S[XFinSequence of NAT] means 1* $1.N3 = b^2* $1.I2 * $1.I2;
A5: {p where p is (n+5)-element XFinSequence of NAT:S[p]}
is diophantine Subset of n5 -xtuples_of NAT by Th9;
defpred T[XFinSequence of NAT] means 1* $1.N4 = 1*$1.N2 * $1.N3;
A6: {p where p is (n+5)-element XFinSequence of NAT:T[p]}
is diophantine Subset of n5 -xtuples_of NAT by Th9;
defpred U[XFinSequence of NAT] means 1* $1.N = 1*$1.N4 + 1;
A7: {p where p is (n+5)-element XFinSequence of NAT:U[p]}
is diophantine Subset of n5 -xtuples_of NAT by Th6;
defpred PQ[XFinSequence of NAT] means P[$1] & Q[$1];
defpred PQR[XFinSequence of NAT] means PQ[$1] & R[$1];
defpred PQRS[XFinSequence of NAT] means PQR[$1] & S[$1];
defpred PQRST[XFinSequence of NAT] means PQRS[$1] & T[$1];
defpred PQRSTU[XFinSequence of NAT] means PQRST[$1] & U[$1];
{p where p is (n+5)-element XFinSequence of NAT : P[p] & Q[p]}
is diophantine Subset of n5 -xtuples_of NAT
from IntersectionDiophantine(A2,A3);
then A8: {p where p is (n+5)-element XFinSequence of NAT: PQ[p]}
is diophantine Subset of n5 -xtuples_of NAT;
{p where p is (n+5)-element XFinSequence of NAT : PQ[p] & R[p]}
is diophantine Subset of (n+5) -xtuples_of NAT
from IntersectionDiophantine(A8,A4);
then A9: {p where p is (n+5)-element XFinSequence of NAT: PQR[p]}
is diophantine Subset of n5 -xtuples_of NAT;
{p where p is (n+5)-element XFinSequence of NAT: PQR[p] & S[p]}
is diophantine Subset of n5 -xtuples_of NAT
from IntersectionDiophantine(A9,A5);
then A10: {p where p is (n+5)-element XFinSequence of NAT: PQRS[p]}
is diophantine Subset of n5 -xtuples_of NAT;
{p where p is (n+5)-element XFinSequence of NAT: PQRS[p] & T[p]}
is diophantine Subset of n5 -xtuples_of NAT
from IntersectionDiophantine(A10,A6);
then A11: {p where p is (n+5)-element XFinSequence of NAT : PQRST[p]}
is diophantine Subset of n5 -xtuples_of NAT;
A12: {p where p is (n+5)-element XFinSequence of NAT: PQRST[p] & U[p]}
is diophantine Subset of n5 -xtuples_of NAT
from IntersectionDiophantine(A11,A7);
set DD = {p where p is (n+5)-element XFinSequence of NAT:PQRSTU[p]};
set DDR = {p|n where p is (n+5)-element XFinSequence of NAT:p in DD};
A13: DDR is diophantine Subset of n -xtuples_of NAT by NAT_1:11,Th5,A12;
A14: DDR c= WW
proof
let x be object such that A15: x in DDR;
consider p be (n+5)-element XFinSequence of NAT such that
A16: x=p|n & p in DD by A15;
consider q be (n+5)-element XFinSequence of NAT such that
A17: p=q & PQRSTU[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)^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)^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)^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 thesis by A16;
end;
WW c= DDR
proof
let x be object such that A22: x in WW;
consider p be 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*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*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*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*y2-'1;
set y4 = b^2* p.i2 * p.i2;
set y5 = 1*y3*y4;
reconsider y1,y2,y3,y4,y5 as Element of NAT by ORDINAL1:def 12;
set Y=<%y1%>^<%y2%>^<%y3%>^<%y4%>^<%y5%>;
set PY = p^Y;
A27: len p = n & len Y = 5 by CARD_1:def 7;
A28: PY|n =p by A27,AFINSQ_1:57;
A29: PY.i1= p.i1 by A28,A1,Th4;
A30: PY.i2 = (PY|n).i2 by A1,Th4
.= p.i2 by A27,AFINSQ_1:57;
A31: PY.i3 = (PY|n).i3 by A1,Th4
.= p.i3 by A27,AFINSQ_1:57;
0 in dom Y by A27,AFINSQ_1:66;
then A32:PY.(n+0) = Y.0 by A27,AFINSQ_1:def 3
.= y1 by AFINSQ_1:46;
1 in dom Y by A27,AFINSQ_1:66;
then A33:PY.(n+1) = Y.1 by A27,AFINSQ_1:def 3
.= y2 by AFINSQ_1:46;
2 in dom Y by A27,AFINSQ_1:66;
then A34: PY.(n+2) = Y.2 by A27,AFINSQ_1:def 3
.= y3 by AFINSQ_1:46;
3 in dom Y by A27,AFINSQ_1:66;
then A35: PY.(n+3) = Y.3 by A27,AFINSQ_1:def 3
.= y4 by AFINSQ_1:46;
4 in dom Y by A27,AFINSQ_1:66;
then A36:PY.(n+4) = Y.4 by A27,AFINSQ_1:def 3
.= y5;
y1 - y5=1 by A23,Lm1,A24,A25,A26;
then
y1 = y5+1;
then PQRSTU[PY] by A32,A31,A33,A29,A34,A35,A30,A36;
then PY in DD;
hence thesis by A23,A28;
end;
hence thesis by A13,A14,XBOOLE_0:def 10;
end;
end;
begin :: Main Lemmas
theorem Th23:
for i1,i2,i3 holds
{p: p.i1 = Py(p.i2,p.i3) & p.i2 > 1}
is diophantine Subset of n -xtuples_of NAT
proof
let i1,i2,i3;
set n9=n+9;
set WW = {p: p.i1 = Py(p.i2,p.i3) & p.i2 > 1};
WW c= n -xtuples_of NAT
proof
let y be object;
assume y in WW;
then ex p st
y=p & p.i1 = Py(p.i2,p.i3) & p.i2 > 1;
hence thesis by HILB10_2:def 5;
end;
then reconsider WW as Subset of n -xtuples_of NAT;
per cases;
suppose n=0;
then WW is diophantine Subset of n -xtuples_of NAT;
hence thesis;
end;
suppose A1: n<>0;
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 n9 by Th2,Th3;
defpred P0[XFinSequence of NAT] means 1*$1.I2 > 0*$1.I1 + 1;
A2: {p where p is n9-element XFinSequence of NAT:P0[p]}
is diophantine Subset of n9 -xtuples_of NAT by Th7;
defpred P1[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 n9-element XFinSequence of NAT:P1[p]}
is diophantine Subset of n9 -xtuples_of NAT by Th22;
defpred P2[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 n9-element XFinSequence of NAT:P2[p]}
is diophantine Subset of n9 -xtuples_of NAT by Th22;
defpred P3[XFinSequence of NAT] means 1*$1.N2 >= 1*$1.I1 + 0;
A5: {p where p is n9-element XFinSequence of NAT:P3[p]}
is diophantine Subset of n9 -xtuples_of NAT by Th8;
defpred P4[XFinSequence of NAT] means 1*$1.N3 > 1*$1.I1 + 0;
A6: {p where p is n9-element XFinSequence of NAT:P4[p]}
is diophantine Subset of n9 -xtuples_of NAT by Th7;
defpred P5[XFinSequence of NAT] means 1*$1.I1 >= 1*$1.I3 + 0;
A7: {p where p is n9-element XFinSequence of NAT:P5[p]}
is diophantine Subset of n9 -xtuples_of NAT by Th8;
defpred P6[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 n9-element XFinSequence of NAT:P6[p]}
is diophantine Subset of n9 -xtuples_of NAT by Th22;
defpred P7[XFinSequence of NAT] means
1*$1.N5, 1*$1.I1 are_congruent_mod 1*$1.N1 ;
A9: {p where p is n9-element XFinSequence of NAT:P7[p]}
is diophantine Subset of n9 -xtuples_of NAT by Th21;
defpred PA[XFinSequence of NAT] means 1*$1.N3, 1*$1.I2
are_congruent_mod 1*$1.N1 ;
A10: {p where p is n9-element XFinSequence of NAT:PA[p]}
is diophantine Subset of n9 -xtuples_of NAT by Th21;
defpred PB[XFinSequence of NAT] means 1*$1.N5, 1*$1.I3
are_congruent_mod 1*$1.N6;
A11: {p where p is n9-element XFinSequence of NAT:PB[p]}
is diophantine Subset of n9 -xtuples_of NAT by Th21;
defpred PC[XFinSequence of NAT] means
1*$1.N3, 1*$1.N8 are_congruent_mod 1*$1.N6;
A12: {p where p is n9-element XFinSequence of NAT:PC[p]}
is diophantine Subset of n9 -xtuples_of NAT by Th21;
defpred PD[XFinSequence of NAT] means 1*$1.N2,
0*$1.N3 are_congruent_mod 1*$1.N7;
A13: {p where p is n9-element XFinSequence of NAT:PD[p]}
is diophantine Subset of n9 -xtuples_of NAT by Th21;
defpred PE[XFinSequence of NAT] means 1 = $1.N8;
A14: {p where p is n9-element XFinSequence of NAT:PE[p]}
is diophantine Subset of n9 -xtuples_of NAT by Th14;
defpred PF[XFinSequence of NAT] means 2*$1.I1 = $1.N6;
A15: {p where p is n9-element XFinSequence of NAT:PF[p]}
is diophantine Subset of n9 -xtuples_of NAT by Th12;
defpred PG[XFinSequence of NAT] means 1*$1.I1*$1.I1 = 1*$1.N7;
A16: {p where p is n9-element XFinSequence of NAT:PG[p]}
is diophantine Subset of n9 -xtuples_of NAT by Th9;
defpred P01[XFinSequence of NAT] means P0[$1] & P1[$1];
defpred P23[XFinSequence of NAT] means P2[$1] & P3[$1];
defpred P45[XFinSequence of NAT] means P4[$1] & P5[$1];
defpred P67[XFinSequence of NAT] means P6[$1] & P7[$1];
defpred PAB[XFinSequence of NAT] means PA[$1] & PB[$1];
defpred PCD[XFinSequence of NAT] means PC[$1] & PD[$1];
defpred PEF[XFinSequence of NAT] means PE[$1] & PF[$1];
{p where p is n9-element XFinSequence of NAT : P0[p] & P1[p]}
is diophantine Subset of n9 -xtuples_of NAT
from IntersectionDiophantine(A2,A3);
then A17: {p where p is n9-element XFinSequence of NAT: P01[p]}
is diophantine Subset of n9 -xtuples_of NAT;
{p where p is n9-element XFinSequence of NAT : P2[p] & P3[p]}
is diophantine Subset of n9 -xtuples_of NAT
from IntersectionDiophantine(A4,A5);
then A18: {p where p is n9-element XFinSequence of NAT: P23[p]}
is diophantine Subset of n9 -xtuples_of NAT;
{p where p is n9-element XFinSequence of NAT : P4[p] & P5[p]}
is diophantine Subset of n9 -xtuples_of NAT
from IntersectionDiophantine(A6,A7);
then A19: {p where p is n9-element XFinSequence of NAT: P45[p]}
is diophantine Subset of n9 -xtuples_of NAT;
{p where p is n9-element XFinSequence of NAT : P6[p] & P7[p]}
is diophantine Subset of n9 -xtuples_of NAT
from IntersectionDiophantine(A8,A9);
then A20: {p where p is n9-element XFinSequence of NAT: P67[p]}
is diophantine Subset of n9 -xtuples_of NAT;
{p where p is n9-element XFinSequence of NAT : PA[p] & PB[p]}
is diophantine Subset of n9 -xtuples_of NAT
from IntersectionDiophantine(A10,A11);
then A21: {p where p is n9-element XFinSequence of NAT: PAB[p]}
is diophantine Subset of n9 -xtuples_of NAT;
{p where p is n9-element XFinSequence of NAT : PC[p] & PD[p]}
is diophantine Subset of n9 -xtuples_of NAT
from IntersectionDiophantine(A12,A13);
then A22: {p where p is n9-element XFinSequence of NAT: PCD[p]}
is diophantine Subset of n9 -xtuples_of NAT;
{p where p is n9-element XFinSequence of NAT : PE[p] & PF[p]}
is diophantine Subset of n9 -xtuples_of NAT from
IntersectionDiophantine(A14,A15);
then A23: {p where p is n9-element XFinSequence of NAT: PEF[p]}
is diophantine Subset of n9 -xtuples_of NAT;
defpred P0123[XFinSequence of NAT] means P01[$1] & P23[$1];
defpred P4567[XFinSequence of NAT] means P45[$1] & P67[$1];
defpred PABCD[XFinSequence of NAT] means PAB[$1] & PCD[$1];
defpred PEFG[XFinSequence of NAT] means PEF[$1] & PG[$1];
{p where p is n9-element XFinSequence of NAT : P01[p] & P23[p]}
is diophantine Subset of n9 -xtuples_of NAT
from IntersectionDiophantine(A17,A18);
then A24: {p where p is n9-element XFinSequence of NAT: P0123[p]}
is diophantine Subset of n9 -xtuples_of NAT;
{p where p is n9-element XFinSequence of NAT : P45[p] & P67[p]}
is diophantine Subset of n9 -xtuples_of NAT
from IntersectionDiophantine(A19,A20);
then A25: {p where p is n9-element XFinSequence of NAT: P4567[p]}
is diophantine Subset of n9 -xtuples_of NAT;
{p where p is n9-element XFinSequence of NAT : PAB[p] & PCD[p]}
is diophantine Subset of n9 -xtuples_of NAT
from IntersectionDiophantine(A21,A22);
then A26: {p where p is n9-element XFinSequence of NAT: PABCD[p]}
is diophantine Subset of n9 -xtuples_of NAT;
{p where p is n9-element XFinSequence of NAT : PEF[p] & PG[p]}
is diophantine Subset of n9 -xtuples_of NAT
from IntersectionDiophantine(A23,A16);
then A27: {p where p is n9-element XFinSequence of NAT: PEFG[p]}
is diophantine Subset of n9 -xtuples_of NAT;
defpred P01234567[XFinSequence of NAT] means P0123[$1] & P4567[$1];
defpred PABCDEFG[XFinSequence of NAT] means PABCD[$1] & PEFG[$1];
{p where p is n9-element XFinSequence of NAT : P0123[p] & P4567[p]}
is diophantine Subset of n9 -xtuples_of NAT
from IntersectionDiophantine(A24,A25);
then A28: {p where p is n9-element XFinSequence of NAT: P01234567[p]}
is diophantine Subset of n9 -xtuples_of NAT;
{p where p is n9-element XFinSequence of NAT : PABCD[p] & PEFG[p]}
is diophantine Subset of n9 -xtuples_of NAT
from IntersectionDiophantine(A26,A27);
then A29: {p where p is n9-element XFinSequence of NAT: PABCDEFG[p]}
is diophantine Subset of n9 -xtuples_of NAT;
defpred P01234567ABCDEFG[XFinSequence of NAT] means
P01234567[$1] & PABCDEFG[$1];
A30:{p where p is n9-element XFinSequence of NAT :
P01234567[p] &PABCDEFG[p]}
is diophantine Subset of n9 -xtuples_of NAT
from IntersectionDiophantine(A28,A29);
set DD={p where p is n9-element XFinSequence of NAT: P01234567ABCDEFG[p]};
set DDR = {p|n where p is n9-element XFinSequence of NAT:p in DD};
A31: DDR is diophantine Subset of n -xtuples_of NAT by Th5,A30,NAT_1:11;
A32: DDR c= WW
proof
let o be object such that A33: o in DDR;
consider p be n9-element XFinSequence of NAT such that
A34: o=p|n & p in DD by A33;
consider q be n9-element XFinSequence of NAT such that
A35: p=q & P01234567ABCDEFG[q] by A34;
len p = n9 & n9 >=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 thesis by A34;
end;
WW c= DDR
proof
let o be object such that A37: o in WW;
consider p such that
A38:o=p &p.i1 = Py(p.i2,p.i3) & p.i2 > 1 by A37;
set y = p.i1,a=p.i2,z=p.i3;
consider x,x1,y1,A,x2,y2 be Nat such that
A39: a>1 &
[x,y] is Pell's_solution of (a^2-'1) &
[x1,y1] is Pell's_solution of (a^2-'1)&
y1>=y & A > y & y >= z &
[x2,y2] is Pell's_solution of (A^2-'1) &
y2,y are_congruent_mod x1 &
A,a are_congruent_mod x1 &
y2,z are_congruent_mod 2*y &
A,1 are_congruent_mod 2*y &
y1,0 are_congruent_mod y^2 by A38,HILB10_1:38;
reconsider x,x1,y1,A,x2,y2 as Element of NAT by ORDINAL1:def 12;
reconsider 2y=2*y as Element of NAT;
reconsider yy=y*y 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^Y;
A40: len p = n & len Y = 9 by CARD_1:def 7;
A41: PY|n =p by A40,AFINSQ_1:57;
0 in dom Y by A40,AFINSQ_1:66;
then A42:PY.(n+0) = (Y).0 by A40,AFINSQ_1:def 3
.= x by AFINSQ_1:50;
1 in dom Y by A40,AFINSQ_1:66;
then A43:PY.(n+1) = (Y).1 by A40,AFINSQ_1:def 3
.= x1 by AFINSQ_1:50;
2 in dom Y by A40,AFINSQ_1:66;
then A44:PY.(n+2) = (Y).2 by A40,AFINSQ_1:def 3
.= y1 by AFINSQ_1:50;
3 in dom Y by A40,AFINSQ_1:66;
then A45: PY.(n+3) = Y.3 by A40,AFINSQ_1:def 3
.= A by AFINSQ_1:50;
4 in dom Y by A40,AFINSQ_1:66;
then A46: PY.(n+4) = Y.4 by A40,AFINSQ_1:def 3
.= x2 by AFINSQ_1:50;
5 in dom Y by A40,AFINSQ_1:66;
then A47: PY.(n+5) = Y.5 by A40,AFINSQ_1:def 3
.= y2 by AFINSQ_1:50;
6 in dom Y by A40,AFINSQ_1:66;
then PY.(n+6) = Y.6 by A40,AFINSQ_1:def 3
.= 2y by AFINSQ_1:50;
then A48: PY.N6 = 2*y = 2*PY.I1 by A41,A1,Th4;
7 in dom Y by A40,AFINSQ_1:66;
then A49: PY.(n+7) = Y.7 by A40,AFINSQ_1:def 3
.= yy by AFINSQ_1:50;
8 in dom Y by A40,AFINSQ_1:66;
then A50: PY.(n+8) = Y.8 by A40,AFINSQ_1:def 3
.= Z;
P01234567ABCDEFG[PY] by SQUARE_1:def 1,A39,A42,A45,A46,A47,A1,Th4, A43,
A41,A50,A48,A49,A44;
then PY in DD;
hence thesis by A38,A41;
end;
hence thesis by A31,A32,XBOOLE_0:def 10;
end;
end;
theorem
for i1,i2,i3 holds
{p:p.i2 =(p.i1) |^ (p.i3)} is diophantine Subset of n -xtuples_of NAT
proof
let i1,i2,i3;
set n7=n+7;
set WW = {p: p.i2 =(p.i1) |^ (p.i3)};
WW c= n -xtuples_of NAT
proof
let y be object;
assume y in WW;
then ex p st y=p & p.i2 =(p.i1)|^ (p.i3);
hence thesis by HILB10_2:def 5;
end;
then reconsider WW as Subset of n -xtuples_of NAT;
per cases;
suppose n=0;
then WW is diophantine Subset of n -xtuples_of NAT;
hence thesis;
end;
suppose A1: n<>0;
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 n7 by Th2,Th3;
defpred P0[XFinSequence of NAT] means $1.I1 = 0;
A2: {p where p is n7-element XFinSequence of NAT:P0[p]}
is diophantine Subset of n7 -xtuples_of NAT by Th14;
defpred P1[XFinSequence of NAT] means $1.I1 = 1;
A3: {p where p is n7-element XFinSequence of NAT:P1[p]}
is diophantine Subset of n7 -xtuples_of NAT by Th14;
defpred P2[XFinSequence of NAT] means 1*$1.I1 > 0*$1.I2 + 1;
A4: {p where p is n7-element XFinSequence of NAT:P2[p]}
is diophantine Subset of n7 -xtuples_of NAT by Th7;
defpred P3[XFinSequence of NAT] means $1.I2 = 0;
A5: {p where p is n7-element XFinSequence of NAT:P3[p]}
is diophantine Subset of n7 -xtuples_of NAT by Th14;
defpred P4[XFinSequence of NAT] means $1.I2 = 1;
A6: {p where p is n7-element XFinSequence of NAT:P4[p]}
is diophantine Subset of n7 -xtuples_of NAT by Th14;
defpred P5[XFinSequence of NAT] means $1.I3 = 0;
A7: {p where p is n7-element XFinSequence of NAT:P5[p]}
is diophantine Subset of n7 -xtuples_of NAT by Th14;
defpred P6[XFinSequence of NAT] means 1*$1.I3 > 0*$1.I1 + 0;
A8: {p where p is n7-element XFinSequence of NAT:P6[p]}
is diophantine Subset of n7 -xtuples_of NAT by Th7;
defpred PA[XFinSequence of NAT] means 1*$1.N4 = 1*$1.I3 + 1;
A9: {p where p is n7-element XFinSequence of NAT:PA[p]}
is diophantine Subset of n7 -xtuples_of NAT by Th6;
defpred PB[XFinSequence of NAT] means 1*$1.N5 = 1*$1.N3 * $1.I1;
A10: {p where p is n7-element XFinSequence of NAT:PB[p]}
is diophantine Subset of n7 -xtuples_of NAT by Th9;
defpred PC[XFinSequence of NAT] means $1.N = Py($1.I1,$1.N4) & $1.I1 >1 ;
A11: {p where p is n7-element XFinSequence of NAT:PC[p]}
is diophantine Subset of n7 -xtuples_of NAT by Th23;
defpred PD[XFinSequence of NAT] means 1*$1.N3 > 2 * $1.I3 * $1.N;
A12: {p where p is n7-element XFinSequence of NAT:PD[p]}
is diophantine Subset of n7 -xtuples_of NAT by Th17;
defpred PE[XFinSequence of NAT] means $1.N1 = Py($1.N3,$1.N4)
& $1.N3 > 1;
A13: {p where p is n7-element XFinSequence of NAT:PE[p]}
is diophantine Subset of n7 -xtuples_of NAT by Th23;
defpred PF[XFinSequence of NAT] means $1.N2 = Py($1.N5,$1.N4)
& $1.N5 > 1;
A14: {p where p is n7-element XFinSequence of NAT:PF[p]}
is diophantine Subset of n7 -xtuples_of NAT by Th23;
defpred PG[XFinSequence of NAT] means 1*$1.N6 =1* $1.I2 * $1.N1;
A15: {p where p is n7-element XFinSequence of NAT:PG[p]}
is diophantine Subset of n7 -xtuples_of NAT by Th9;
defpred PH[XFinSequence of NAT] means 1*$1.N6 >= 1*$1.N2 + 0;
A16: {p where p is n7-element XFinSequence of NAT:PH[p]}
is diophantine Subset of n7 -xtuples_of NAT by Th8;
defpred PI[XFinSequence of NAT] means 2*$1.N6 < 1*$1.N1 + 2*$1.N2;
A17: {p where p is n7-element XFinSequence of NAT:PI[p]}
is diophantine Subset of n7 -xtuples_of NAT by Th18;
defpred PJ[XFinSequence of NAT] means 1*$1.N2 >= 1*$1.N6 + 0;
A18: {p where p is n7-element XFinSequence of NAT:PJ[p]}
is diophantine Subset of n7 -xtuples_of NAT by Th8;
defpred PK[XFinSequence of NAT] means (-2)*$1.N6 < 1*$1.N1 + (-2)*$1.N2;
A19: {p where p is n7-element XFinSequence of NAT:PK[p]}
is diophantine Subset of n7 -xtuples_of NAT by Th18;
defpred P45[XFinSequence of NAT] means P4[$1] & P5[$1];
defpred P03[XFinSequence of NAT] means P0[$1] & P3[$1];
defpred P036[XFinSequence of NAT] means P03[$1] & P6[$1];
defpred P14[XFinSequence of NAT] means P1[$1] & P4[$1];
defpred P146[XFinSequence of NAT] means P14[$1] & P6[$1];
defpred P26[XFinSequence of NAT] means P2[$1] & P6[$1];
defpred PHI[XFinSequence of NAT] means PH[$1] & PI[$1];
defpred PJK[XFinSequence of NAT] means PJ[$1] & PK[$1];
{p where p is n7-element XFinSequence of NAT : P4[p] & P5[p]}
is diophantine Subset of n7 -xtuples_of NAT
from IntersectionDiophantine(A6,A7);
then A20: {p where p is n7-element XFinSequence of NAT: P45[p]}
is diophantine Subset of n7 -xtuples_of NAT;
{p where p is n7-element XFinSequence of NAT : P0[p] & P3[p]}
is diophantine Subset of n7 -xtuples_of NAT
from IntersectionDiophantine(A2,A5);
then A21: {p where p is n7-element XFinSequence of NAT: P03[p]}
is diophantine Subset of n7 -xtuples_of NAT;
{p where p is n7-element XFinSequence of NAT : P03[p] & P6[p]}
is diophantine Subset of n7 -xtuples_of NAT
from IntersectionDiophantine(A21,A8);
then A22: {p where p is n7-element XFinSequence of NAT: P036[p]}
is diophantine Subset of n7 -xtuples_of NAT;
{p where p is n7-element XFinSequence of NAT : P1[p] & P4[p]}
is diophantine Subset of n7 -xtuples_of NAT
from IntersectionDiophantine(A3,A6);
then A23: {p where p is n7-element XFinSequence of NAT: P14[p]}
is diophantine Subset of n7 -xtuples_of NAT;
{p where p is n7-element XFinSequence of NAT : P14[p] & P6[p]}
is diophantine Subset of n7 -xtuples_of NAT
from IntersectionDiophantine(A23,A8);
then A24: {p where p is n7-element XFinSequence of NAT: P146[p]}
is diophantine Subset of n7 -xtuples_of NAT;
{p where p is n7-element XFinSequence of NAT : P2[p] & P6[p]}
is diophantine Subset of n7 -xtuples_of NAT
from IntersectionDiophantine(A4,A8);
then A25: {p where p is n7-element XFinSequence of NAT: P26[p]}
is diophantine Subset of n7 -xtuples_of NAT;
{p where p is n7-element XFinSequence of NAT : PH[p] & PI[p]}
is diophantine Subset of n7 -xtuples_of NAT
from IntersectionDiophantine(A16,A17);
then A26: {p where p is n7-element XFinSequence of NAT: PHI[p]}
is diophantine Subset of n7 -xtuples_of NAT;
{p where p is n7-element XFinSequence of NAT : PJ[p] & PK[p]}
is diophantine Subset of n7 -xtuples_of NAT
from IntersectionDiophantine(A18,A19);
then A27: {p where p is n7-element XFinSequence of NAT: PJK[p]}
is diophantine Subset of n7 -xtuples_of NAT;
defpred PHIJK[XFinSequence of NAT] means PHI[$1] or PJK[$1];
{p where p is n7-element XFinSequence of NAT : PHI[p] or PJK[p]}
is diophantine Subset of n7 -xtuples_of NAT from UnionDiophantine(A26,A27);
then A28: {p where p is n7-element XFinSequence of NAT: PHIJK[p]}
is diophantine Subset of n7 -xtuples_of NAT;
defpred P45036[XFinSequence of NAT] means P45[$1] or P036[$1];
{p where p is n7-element XFinSequence of NAT : P45[p] or P036[p]}
is diophantine Subset of n7 -xtuples_of NAT from UnionDiophantine(A20,A22);
then A29: {p where p is n7-element XFinSequence of NAT: P45036[p]}
is diophantine Subset of n7 -xtuples_of NAT;
defpred P45036146[XFinSequence of NAT] means P45036[$1] or P146[$1];
{p where p is n7-element XFinSequence of NAT : P45036[p] or P146[p]}
is diophantine Subset of n7 -xtuples_of NAT from UnionDiophantine(A29,A24);
then A30: {p where p is n7-element XFinSequence of NAT: P45036146[p]}
is diophantine Subset of n7 -xtuples_of NAT;
defpred PAB[XFinSequence of NAT] means PA[$1] & PB[$1];
defpred PCD[XFinSequence of NAT] means PC[$1] & PD[$1];
defpred PCDE[XFinSequence of NAT] means PCD[$1] & PE[$1];
defpred PCDEF[XFinSequence of NAT] means PCDE[$1] & PF[$1];
defpred PCDEFHIJK[XFinSequence of NAT] means PCDEF[$1] & PHIJK[$1];
defpred P26CDEFHIJK[XFinSequence of NAT] means P26[$1] & PCDEFHIJK[$1];
defpred P26CDEFHIJKAB[XFinSequence of NAT] means P26CDEFHIJK[$1] & PAB[$1];
defpred P26CDEFHIJKABG[XFinSequence of NAT] means P26CDEFHIJKAB[$1] &
PG[$1];
{p where p is n7-element XFinSequence of NAT : PA[p] & PB[p]}
is diophantine Subset of n7 -xtuples_of NAT
from IntersectionDiophantine(A9,A10);
then A31: {p where p is n7-element XFinSequence of NAT: PAB[p]}
is diophantine Subset of n7 -xtuples_of NAT;
{p where p is n7-element XFinSequence of NAT : PC[p] & PD[p]}
is diophantine Subset of n7 -xtuples_of NAT
from IntersectionDiophantine(A11,A12);
then A32: {p where p is n7-element XFinSequence of NAT: PCD[p]}
is diophantine Subset of n7 -xtuples_of NAT;
{p where p is n7-element XFinSequence of NAT : PCD[p] & PE[p]}
is diophantine Subset of n7 -xtuples_of NAT
from IntersectionDiophantine(A32,A13);
then A33: {p where p is n7-element XFinSequence of NAT: PCDE[p]}
is diophantine Subset of n7 -xtuples_of NAT;
{p where p is n7-element XFinSequence of NAT : PCDE[p] & PF[p]}
is diophantine Subset of n7 -xtuples_of NAT
from IntersectionDiophantine(A33,A14);
then A34: {p where p is n7-element XFinSequence of NAT: PCDEF[p]}
is diophantine Subset of n7 -xtuples_of NAT;
{p where p is n7-element XFinSequence of NAT : PCDEF[p] & PHIJK[p]}
is diophantine Subset of n7 -xtuples_of NAT
from IntersectionDiophantine(A34,A28);
then A35: {p where p is n7-element XFinSequence of NAT: PCDEFHIJK[p]}
is diophantine Subset of n7 -xtuples_of NAT;
{p where p is n7-element XFinSequence of NAT : P26[p] & PCDEFHIJK[p]}
is diophantine Subset of n7 -xtuples_of NAT
from IntersectionDiophantine(A25,A35);
then A36:
{p where p is n7-element XFinSequence of NAT: P26CDEFHIJK[p]}
is diophantine Subset of n7 -xtuples_of NAT;
{p where p is n7-element XFinSequence of NAT : P26CDEFHIJK[p] & PAB[p]}
is diophantine Subset of n7 -xtuples_of NAT
from IntersectionDiophantine(A36,A31);
then A37: {p where p is n7-element XFinSequence of NAT:
P26CDEFHIJKAB[p]} is diophantine Subset of n7 -xtuples_of NAT;
{p where p is n7-element XFinSequence of NAT : P26CDEFHIJKAB[p] & PG[p]}
is diophantine Subset of n7 -xtuples_of NAT
from IntersectionDiophantine(A37,A15);
then A38: {p where p is n7-element XFinSequence of NAT:
P26CDEFHIJKABG[p]} is diophantine Subset of n7 -xtuples_of NAT;
defpred P4503614626CDEFHIJKABG[XFinSequence of NAT] means
P45036146[$1] or P26CDEFHIJKABG[$1];
A39: {p where p is n7-element XFinSequence of NAT :
P45036146[p] or P26CDEFHIJKABG[p]}
is diophantine Subset of n7 -xtuples_of NAT
from UnionDiophantine(A30, A38);
set DD = {p where p is n7-element XFinSequence of NAT:
P4503614626CDEFHIJKABG[p]};
set DDR = {p|n where p is n7-element XFinSequence of NAT:p in DD};
A40: DDR is diophantine Subset of n -xtuples_of NAT by Th5,A39,NAT_1:11;
A41: DDR c= WW
proof
let o be object such that A42: o in DDR;
consider p be n7-element XFinSequence of NAT such that
A43: o=p|n & p in DD by A42;
consider q be n7-element XFinSequence of NAT such that
A44: p=q & P4503614626CDEFHIJKABG[q] by A43;
len p = n7 & n7 >=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, y = pn.i2, z = pn.i3;
set y1 = p.N,y2 = p.N1,y3 = p.N2,K = p.N3;
A45: x = p.i1 & y = p.i2 & z = p.i3 by A1,Th4;
(y = 1 & z = 0) or
(x = 0 & y = 0 & z > 0) or
(x = 1 & y = 1 & z > 0) or
(x > 1 & z > 0 & ex y1,y2,y3,K be Nat st
y1 = Py(x,z+1) & K > 2*z*y1 & y2 = Py(K,z+1) & y3 = Py(K*x,z+1) &
(0 <= y-y3/y2 <1/2 or 0 <= y3/y2 -y < 1/2))
proof
per cases by A44,A45;
suppose y=1 & z=0;
hence thesis;
end;
suppose x = 0 & y = 0 & z > 0;
hence thesis;
end;
suppose x = 1 & y = 1 & z > 0;
hence thesis;
end;
suppose A46: ((1*x > 0*y + 1) & (1*z > 0*x + 0) & (y1 = Py(x,z+1))
& (1*K > 2*z*y1)
& (y2 = Py(K,z+1))
& (1*y3 = Py(K*x,z+1))
& (( (1*y*y2 >= 1*y3+0) & (2*y*y2 < 1*y2+2*y3)) or
( (1*y3 >= y*y2) & ( (-2)*y*y2 < 1*y2 + (-2)*y3))));
(x > 1 & z > 0 & ex y1,y2,y3,K be Nat st
y1 = Py(x,z+1) & K > 2*z*y1 & y2 = Py(K,z+1) & y3 = Py(K*x,z+1) &
(0 <= y-y3/y2 <1/2 or 0 <= y3/y2 -y < 1/2))
proof
thus x > 1 & z > 0 by A46;
take y1,y2,y3,K;
thus y1 = Py(x,z+1) & K > 2*z*y1 & y2 = Py(K,z+1) &
y3 = Py(K*x,z+1) by A46;
x is non trivial by A46,NEWTON03:def 1;
then y1 >0 & (2*z) >0 by A46,XREAL_1:129,HILB10_1:13;
then 2*z*y1 >0 by XREAL_1:129;
then 2*z*y1 >=1 by NAT_1:14;
then K > 1 by A46,XXREAL_0:2;
then K is non trivial by NEWTON03:def 1;
then
A47: y2 >0 by A46,HILB10_1:13;
per cases by A46;
suppose (y*y2 >= y3) & (2*y*y2 < 1*y2+2*y3 );
then ( y*y2/y2 >= y3/y2) & ( 2*y*y2/y2 < (1*y2 + 2*y3)/y2 )
by A47, XREAL_1:74,72;
then ( y >= y3/y2) & ( 2*y < (1*y2 + 2*y3)/y2 )
by XCMPLX_1:89, A47;
then A48: ( y-y3/y2>= y3/y2 - y3/y2)&(2*y*1 < 1*y2/y2 + 2*y3/y2)
by XREAL_1:9,XCMPLX_1:62;
then ( y-y3/y2>= 0) & (2*y < 1 + 2*y3/y2) by XCMPLX_1:89,A47;
then (2*y/2 < (1 + 2*y3/y2)/2) by XREAL_1:74;
then (y/(2/2) < 1/2 + 2*y3/y2/2 );
then A49: y < 1/2 + 2* y3/ (y2 * 2) by XCMPLX_1:78;
2* y3/ (y2 * 2) = y3/y2 by XCMPLX_1:91;
then (y - y3/y2 < 1/2 + y3/y2 - y3/y2 ) by A49,XREAL_1:9;
hence thesis by A48;
end;
suppose A50: (y3 >= y*y2) & ( (-2)*y*y2 < 1*y2 + (-2)*y3 );
then (y3/y2 >= y*y2/y2) & ( (-2)*y*y2 < 1*y2 + (-2)*y3 )
by XREAL_1:72;
then (y3/y2 >= y) by A47, XCMPLX_1:89;
then A51: ( y3/y2 - y >= y - y) by XREAL_1:9;
( (-2)*y*y2 /y2 < ( 1*y2 + (-2)*y3) /y2 ) by A47,A50, XREAL_1:74;
then ( (-2)*y < ( 1*y2 + (-2)*y3) /y2 ) by A47, XCMPLX_1:89;
then ( (-2)*y < 1*y2/y2 + (-2)*y3 /y2 ) by XCMPLX_1:62;
then ( (-2)*y < 1 + (-2)*y3 /y2 ) by A47, XCMPLX_1:89;
then A52: ( (1 + (-2)*y3 /y2)/ (-2) < (-2)*y/(-2))
by XREAL_1:75;
A53: (-2)*y3/y2/(-2) = (-2)*y3/(y2*(-2)) by XCMPLX_1:78
.= y3/y2 by XCMPLX_1:91;
-1/2 + y3/y2 < y by A52,A53;
then 1/2 > -(y-y3/y2) by XREAL_1:25,20;
hence thesis by A51;
end;
end;
hence thesis;
end;
end;
then pn.i2 =(pn.i1) |^ (pn.i3) by HILB10_1:39;
hence thesis by A43;
end;
WW c= DDR
proof
let o be object such that A54: o in WW;
consider p such that
A55: o=p & p.i2 =(p.i1)|^ (p.i3) by A54;
set x=p.i1,y=p.i2,z=p.i3;
per cases by A55,HILB10_1:39;
suppose A56: (y = 1 & z = 0) or
(x = 0 & y = 0 & z > 0) or
(x = 1 & y = 1 & z > 0);
reconsider Z=0,z1=z+1 as Element of NAT;
set Y=<%Z%>^<%Z%>^<%Z%>^<%Z%>^<%z1%>^<%Z%>^<%Z%>;
set PY = p^Y;
A57: len p = n & len Y = 7 by CARD_1:def 7;
A58: PY|n =p by A57,AFINSQ_1:57;
P45[PY] or P036[PY] or P146[PY] by A56, A58,A1,Th4;
then PY in DD;
hence thesis by A55,A58;
end;
suppose A59: x > 1 & z > 0 & ex y1,y2,y3,K be Nat st
y1 = Py(x,z+1) & K > 2*z*y1 & y2 = Py(K,z+1) & y3 = Py(K*x,z+1) &
(0 <= y-y3/y2 <1/2 or 0 <= y3/y2 -y < 1/2);
then consider y1,y2,y3,K be Nat such that
A60: y1 = Py(x,z+1) & K > 2*z*y1 & y2 = Py(K,z+1) &
y3 = Py(K*x,z+1) &
(0 <= y-y3/y2 <1/2 or 0 <= y3/y2 -y < 1/2);
reconsider y1,y2,y3,K,z1=z+1 as Element of NAT by ORDINAL1:def 12;
reconsider Kx = K*x,yy2=y*y2 as Element of NAT;
set Y=<%y1%>^<%y2%>^<%y3%>^<%K%>^<%z1%>^<%Kx%>^<%yy2%>;
set PY = p^Y;
A61: len p = n & len Y = 7 by CARD_1:def 7;
A62: PY|n =p by A61,AFINSQ_1:57;
4 in dom Y by A61,AFINSQ_1:66;
then A63: PY.(n+4) =Y.4 by A61,AFINSQ_1:def 3
.= z1 by AFINSQ_1:48;
0 in dom Y by A61,AFINSQ_1:66;
then A64: PY.(n+0) = Y.0 by A61,AFINSQ_1:def 3
.= y1 by AFINSQ_1:48;
3 in dom Y by A61,AFINSQ_1:66;
then A65: PY.(n+3) = Y.3 by A61,AFINSQ_1:def 3
.= K by AFINSQ_1:48;
5 in dom Y by A61,AFINSQ_1:66;
then A66:PY.(n+5) = Y.5 by A61,AFINSQ_1:def 3
.= Kx by AFINSQ_1:48;
x is non trivial by A59,NEWTON03:def 1;
then y1 >0 & z >0 by A59,A60, HILB10_1:13;
then z*y1 >0 by XREAL_1:129;
then 2*(z*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 Y by A61,AFINSQ_1:66;
then A69: PY.(n+1) = Y.1 by A61,AFINSQ_1:def 3
.= y2 by AFINSQ_1:48;
A70: K*x > 1 * 1 by A68, A59,XREAL_1:97;
2 in dom Y by A61,AFINSQ_1:66;
then A71: PY.(n+2) = Y.2 by A61,AFINSQ_1:def 3
.= y3 by AFINSQ_1:48;
6 in dom Y by A61,AFINSQ_1:66;
then A72: PY.(n+6) = Y.6 by A61,AFINSQ_1:def 3
.= yy2;
x is non trivial by A59,NEWTON03:def 1;
then y1 >0 & (2*z) >0 by A60,A59,XREAL_1:129,HILB10_1:13;
then 2*z*y1 >0 by XREAL_1:129;
then 2*z*y1 >=1 by NAT_1:14;
then K > 1 by A60,XXREAL_0:2;
then
K is non trivial by NEWTON03:def 1;
then A73: y2 >0 by A60,HILB10_1:13;
PHIJK[PY]
proof
per cases by A60;
suppose A74: ( y-y3/y2>= 0) & (y- y3/y2 < 1/2 );
(y-y3/y2)*y2 >= 0 * y2 by A74;
then y*y2 - y3/y2*y2 >= 0;
then y*y2 - y3/(y2/y2) >= 0 by XCMPLX_1:82;
then y*y2 - y3/1 >=0 by XCMPLX_1:60,A73;
then A75: y*y2 - y3 + y3 >= 0 + y3 by XREAL_1:6;
(y- y3/y2) *y2 < 1/2 *y2 by A74,XREAL_1:68,A73;
then y*y2 -y3/y2 *y2 < 1/2 * y2;
then y*y2 - y3/(y2/y2) < 1/2 * y2 by XCMPLX_1:82;
then y*y2 - y3/1 < 1/2 * y2 by A73, XCMPLX_1:60;
then (y*y2 - y3)*2 < 1/2 * y2 *2 by XREAL_1:68;
then 2*y*y2 - 2*y3 + 2*y3 < 1*y2 + 2*y3 by XREAL_1:6;
hence thesis by A72,A71,A69,A75;
end;
suppose A76: ( y3/y2 - y >= 0) & ( y3/y2 - y < 1/2 );
then y3/y2 - y + y >= 0 + y by XREAL_1:6;
then y3/y2 * y2 >= y*y2 by XREAL_1:64;
then y3/(y2/y2) >= y*y2 by XCMPLX_1:82;
then A77:y3/1 >= y*y2 by A73, XCMPLX_1:60;
(y3/y2 - y) *y2 < 1/2 *y2 by A76,XREAL_1:68,A73;
then y3/y2*y2 - y*y2 < 1/2 * y2;
then y3/(y2/y2) - y*y2 < 1/2 * y2 by XCMPLX_1:82;
then y3/1 - y*y2 < 1/2 * y2 by A73, XCMPLX_1:60;
then (y3 - y*y2 )*2 < 1/2 * y2 *2 by XREAL_1:68;
then -2*y*y2 + 2*y3 - 2*y3 < 1 * y2 - 2*y3 by XREAL_1:14;
hence thesis by A72,A71,A69,A77;
end;
end;
then P26CDEFHIJKABG[PY] by A59,A63,A67,XXREAL_0:2,A65,A71,
A60,A70,A66,A64,A62,A1,Th4,A69,A72;
then PY in DD;
hence thesis by A55,A62;
end;
end;
hence thesis by A40,A41,XBOOLE_0:def 10;
end;
end;