:: Basic Diophantine Relations :: by Marcin Acewicz and Karol P\kak :: :: Received June 29, 2018 :: Copyright (c) 2018-2021 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; 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; end; theorem :: HILB10_3:1 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; theorem :: HILB10_3:2 i1 is Element of (n+k); theorem :: HILB10_3:3 k < m implies n+k in (n+m); theorem :: HILB10_3:4 for p be (n+k) -element XFinSequence st n<>0 & k <> 0 holds (p|n).i1 = p.i1; begin :: Basic Diophantine Relations theorem :: HILB10_3:5 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; theorem :: HILB10_3:6 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; theorem :: HILB10_3:7 for a,b,c,i1,i2 holds {p: a*p.i1 > b*p.i2+c} is diophantine Subset of n -xtuples_of NAT; scheme :: HILB10_3:sch 1 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 {p where p is n()-element XFinSequence of NAT: P[p]} is diophantine Subset of n() -xtuples_of NAT and {p where p is n()-element XFinSequence of NAT: Q[p]} is diophantine Subset of n() -xtuples_of NAT; scheme :: HILB10_3:sch 2 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 for p being n()-element XFinSequence of NAT holds P[p] iff Q[p]; theorem :: HILB10_3:8 for a,b,c,i1,i2 holds {p: a*p.i1 >= b*p.i2+c} is diophantine Subset of n -xtuples_of NAT; theorem :: HILB10_3:9 for a,b,i1,i2,i3 holds {p: a*p.i1 = b*p.i2*p.i3} is diophantine Subset of n -xtuples_of NAT; theorem :: HILB10_3:10 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; scheme :: HILB10_3:sch 3 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 {p where p is n()-element XFinSequence of NAT: P[p]} is diophantine Subset of n() -xtuples_of NAT and {p where p is n()-element XFinSequence of NAT: Q[p]} is diophantine Subset of n() -xtuples_of NAT; scheme :: HILB10_3:sch 4 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 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 for i1,i2,i3,i4 holds {p: F(p.i1,p.i2,p.i3) = p.i4} is diophantine Subset of n -xtuples_of NAT; scheme :: HILB10_3:sch 5 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 for i1,i2,i3,a holds {p: P[p.i1,p.i2,a*(p.i3)]} is diophantine Subset of n -xtuples_of NAT and 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; theorem :: HILB10_3:11 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; theorem :: HILB10_3:12 for a,i1,i2 holds {p: p.i1 = a*p.i2} is diophantine Subset of n -xtuples_of NAT; theorem :: HILB10_3:13 for a,b,i1 holds {p: a* p.i1 = b} is diophantine Subset of n -xtuples_of NAT; theorem :: HILB10_3:14 for a,i1 holds {p: p.i1 = a} is diophantine Subset of n -xtuples_of NAT; theorem :: HILB10_3:15 for a,b,i1,i2 holds {p: p.i1 = a*p.i2+b} is diophantine Subset of n -xtuples_of NAT; theorem :: HILB10_3:16 for a,b,c,i1,i2 holds {p: a* p.i1 <> b*p.i2+c} is diophantine Subset of n -xtuples_of NAT; theorem :: HILB10_3:17 for a,b,i1,i2,i3 holds {p: a*p.i1 > b*p.i2*p.i3} is diophantine Subset of n -xtuples_of NAT; theorem :: HILB10_3:18 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; theorem :: HILB10_3:19 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; theorem :: HILB10_3:20 for a,b,c,i1,i2,i3 holds {p: a* p.i1 = b*p.i2-' c} is diophantine Subset of n -xtuples_of NAT; theorem :: HILB10_3:21 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; theorem :: HILB10_3:22 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; begin :: Main Lemmas theorem :: HILB10_3:23 for i1,i2,i3 holds {p: p.i1 = Py(p.i2,p.i3) & p.i2 > 1} is diophantine Subset of n -xtuples_of NAT; theorem :: HILB10_3:24 for i1,i2,i3 holds {p:p.i2 =(p.i1) |^ (p.i3)} is diophantine Subset of n -xtuples_of NAT;