:: Diophantine Sets -- Preliminaries
::  by Karol P\kak
:: 
:: Received May 27, 2019
:: Copyright (c) 2019-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, QC_LANG1, VECTSP_1, POLYNOM1, POLYNOM2, AFINSQ_1,
      NEWTON, HILB10_2, INT_2, PARTFUN3, REAL_1, XCMPLX_0, VALUED_0, FINSEQ_2,
      CARD_3, REALSET1, BINOP_2, FINSOP_1, FUNCOP_1, XREAL_0, RFINSEQ, BINOP_1,
      FUNCT_2;
 notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, RELAT_1, FUNCT_1,
      XCMPLX_0, PARTFUN1, FUNCT_2, BINOP_1, NAT_1, FINSEQ_1, FUNCOP_1,
      VECTSP_1, XXREAL_0, RECDEF_1, POLYNOM1, XREAL_0, INT_1, POLYNOM2,
      AFINSQ_1, AFINSQ_2, NEWTON, HILB10_2, VALUED_0, FINSEQ_2, RVSUM_1,
      VALUED_1, BINOP_2, PARTFUN3, CARD_1, NAT_D, RVSUM_4;
 constructors NAT_D, RECDEF_1, BINOP_2, RELSET_1, GROUP_4, POLYNOM2, AFINSQ_2,
      NEWTON, HILB10_2, WSIERP_1, INT_6, SETWISEO, RVSUM_4;
 registrations XBOOLE_0, RELAT_1, FUNCT_1, ORDINAL1, XREAL_0, NAT_1, CARD_1,
      VALUED_0, VALUED_1, RELSET_1, INT_1, STRUCT_0, VECTSP_1, MEMBERED,
      AFINSQ_1, HILB10_2, XXREAL_0, NUMBERS, XCMPLX_0, NEWTON, NEWTON02, NAT_6,
      FINSEQ_1, FINSEQ_2, RVSUM_1, NEWTON04, MOEBIUS2, EUCLID_9, AFINSQ_2,
      PARTFUN3, BINOP_2, FUNCT_2, RFUNCT_2, RVSUM_4;
 requirements NUMERALS, SUBSET, ARITHM, REAL;


begin :: Product of zero based finite sequences

reserve i,j,n,n1,n2,m,k,l,u for Nat,
        r,r1,r2 for Real,
        x,y for Integer,
        a,b for non trivial Nat,
        F for XFinSequence,
        cF,cF1,cF2 for complex-valued XFinSequence,
        c,c1,c2 for Complex;

registration let c1,c2;
  cluster <%c1,c2%> -> complex-valued;
end;

definition let cF be XFinSequence;  ::: same as XProduct from RVSUM_4
  func Product cF -> Element of COMPLEX equals
:: HILB10_4:def 1
    multcomplex "**" cF;
end;

theorem :: HILB10_4:1
  cF is real-valued implies Product cF = multreal "**" cF;

theorem :: HILB10_4:2
  cF is INT-valued implies Product cF = multint "**" cF;

theorem :: HILB10_4:3
  cF is natural-valued implies Product cF = multnat "**" cF;

registration
  let F be real-valued XFinSequence;
  cluster Product F -> real;
end;

registration
  let F be natural-valued XFinSequence;
  cluster Product F -> natural;
end;

theorem :: HILB10_4:4
  cF = {} implies Product cF = 1;

theorem :: HILB10_4:5
  Product <%c%> = c;

theorem :: HILB10_4:6
  Product <%c1,c2%> = c1 * c2;

theorem :: HILB10_4:7
  Product(cF1^cF2) = Product(cF1) * Product(cF2);

theorem :: HILB10_4:8
  c+ (cF1^cF2) = (c+cF1) ^ (c+cF2);

theorem :: HILB10_4:9
  c1 + <%c2%> = <%c1 + c2%>;

theorem :: HILB10_4:10
  for f1,f2 be XFinSequence,n st n <= len f1 holds
   (f1^f2)/^n = (f1/^n)^f2;

registration let n;
  cluster n-element natural-valued for XFinSequence;
end;

registration
  cluster natural-valued positive-yielding for XFinSequence;
end;

registration
  let R be positive-yielding Relation;
  let X be set;
  cluster R|X -> positive-yielding;
end;

registration
  let X be positive-yielding real-valued XFinSequence;
  cluster Product X -> positive;
end;

theorem :: HILB10_4:11
  for X being natural-valued positive-yielding XFinSequence st
    i in dom X holds X.i <= Product X;

registration
  let X be natural-valued XFinSequence,n be positive Nat;
  cluster n + X -> positive-yielding;
end;

theorem :: HILB10_4:12
  for X1,X2 being natural-valued XFinSequence st len X1=len X2 &
    for n st n in dom X1 holds X1.n <= X2.n holds
      Product X1 <= Product X2;

begin :: Binomial is Diophantin

theorem :: HILB10_4:13
  k <= n implies n choose k <= n|^k;

theorem :: HILB10_4:14
  u > n|^k & n >= k & k > i implies (n choose i)*(u |^i) < (u|^k)/n;

theorem :: HILB10_4:15
  u > n|^k & n >= k implies [\ ((u+1)|^n) / (u|^k) /] mod u = n choose k;

theorem :: HILB10_4:16
  for x,y,z being Nat holds
       x >= z & y = x choose z
  iff
     ex u,v,y1,y2,y3 being Nat st
       y1 = x|^z & y2 = (u+1)|^x & y3 = u|^z &
       u > y1 & v = [\y2/y3/] & y,v are_congruent_mod u & y < u & x >=z;

begin

theorem :: HILB10_4:17
   k >0 & n > (2*k)|^(k+1) implies k! = [\(n|^k) / (n choose k) /];

theorem :: HILB10_4:18
   for x,y being Nat holds
     y = x! iff
  ex n,y1,y2,y3 being Nat st
     y1 = (2*x) |^(x+1) &
     y2 = n|^x &
     y3 = n choose x &
     n > y1 &
     y = [\y2/y3/];

begin :: Diophanticity of selected products

reserve x,y,x1,u,w for Nat;

theorem :: HILB10_4:19
  for x1,w,u being Nat st x1*w,1 are_congruent_mod u
    for x being Nat holds
  Product (1+(x1 * idseq x)), x1|^x * (x!) * ((w+x) choose x)
    are_congruent_mod u;

theorem :: HILB10_4:20
  for x,y,x1 being Nat st x1 >= 1 holds
    y = Product (1+(x1 * idseq x)) iff
      ex u,w,y1,y2,y3,y4,y5 being Nat st
        u > y &
        x1*w, 1 are_congruent_mod u &
        y1 = x1|^x &
        y2 = x! &
        y3 = (w+x) choose x &
        y1*y2*y3, y are_congruent_mod u &
        y4 = 1+x1*x &
        y5 = y4|^x &
        u > y5;

theorem :: HILB10_4:21
  c1 + (n|->c2) = n|->(c1+c2);

theorem :: HILB10_4:22
  for x,y,x1 being Nat st x1 = 0 holds
    y = Product (1+(x1 * idseq x)) iff y = 1;

theorem :: HILB10_4:23
  n >= k implies
    Product ((n+1)+(-idseq k)) = k!*(n choose k);

theorem :: HILB10_4:24
   for y,x1,x2 being Nat holds
     y = Product ( (x2+1)+(-idseq x1)) & x2 > x1
   iff y = x1!*(x2 choose x1) & x2 > x1;

begin :: Selected subsets of zero based finite sequences of NAT
      :: as Diophantine sets

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,d,f for Integer;

theorem :: HILB10_4:25
  for a,b being Nat,i1,i2,i3 holds
    {p: p.i1 = (a*p.i2+b) * p.i3} is diophantine Subset of n -xtuples_of NAT;

theorem :: HILB10_4:26
  for a,i1,i2,i3 holds
    {p: p.i1 = a*p.i2*p.i3} is diophantine Subset of n -xtuples_of NAT;

theorem :: HILB10_4:27
  for A being diophantine Subset of n -xtuples_of NAT
    for k,nk being Nat st k+nk = n holds
       {p/^nk : p in A} is diophantine Subset of k -xtuples_of NAT;

theorem :: HILB10_4:28
  for a,b being Integer,c being Nat, i1,i2,i3 holds
    {p: a*p.i1 = [\ (b*p.i2) / (c*p.i3)/] & (c*p.i3 <> 0) }
  is diophantine Subset of n -xtuples_of NAT;

theorem :: HILB10_4:29
  for i1,i2,i3 st n <> 0 holds {p: p.i1 >= p.i3 & p.i2 = p.i1 choose p.i3}
    is diophantine Subset of n -xtuples_of NAT;

theorem :: HILB10_4:30
  for i1,i2,i3 holds {p: p.i1 >= p.i3 & p.i2 = p.i1 choose p.i3}
     is diophantine Subset of n -xtuples_of NAT;

theorem :: HILB10_4:31
  for i1,i2 st n<>0 holds {p: p.i1 = p.i2!}
    is diophantine Subset of n -xtuples_of NAT;

theorem :: HILB10_4:32
  for i1,i2 holds {p: p.i1 = p.i2!}
    is diophantine Subset of n -xtuples_of NAT;

theorem :: HILB10_4:33
  for n,i1,i2,i3 holds {p: 1+(p.i1+1)*(p.i2!) = p.i3}
    is diophantine Subset of n -xtuples_of NAT;

theorem :: HILB10_4:34
  for i1,i2,i3 st n<>0 holds
    {p: p.i3 = Product (1+((p.i1) * idseq (p.i2))) & p.i1 >= 1}
  is diophantine Subset of n -xtuples_of NAT;

theorem :: HILB10_4:35
  for i1,i2,i3 holds
    {p: p.i3 = Product (1+((p.i1) * idseq (p.i2))) & p.i1 >= 1}
  is diophantine Subset of n -xtuples_of NAT;

theorem :: HILB10_4:36
  for n,i1,i2,i3 holds
    {p: p.i3 = Product (1+((p.i1)! * idseq (1+p.i2)))}
  is diophantine Subset of n -xtuples_of NAT;

theorem :: HILB10_4:37
  for i1,i2,i3 st n<>0 holds
    {p: p.i3 = Product ( (p.i2+1)+(-idseq (p.i1))) & p.i2 > p.i1}
  is diophantine Subset of n -xtuples_of NAT;

theorem :: HILB10_4:38
  for i1,i2,i3 holds
    {p: p.i3 = Product ( (p.i2+1)+(-idseq (p.i1))) & p.i2 > p.i1}
  is diophantine Subset of n -xtuples_of NAT;

theorem :: HILB10_4:39
  for i,n1,n2,n,i1 holds {p: p.i1 = Product (i+((p/^n1) | n2))}
  is diophantine Subset of n -xtuples_of NAT;