:: The Lattice of Natural Numbers and The Sublattice of it.
:: The Set of Prime Numbers
::  by Marek Chmur
::
:: Received April 26, 1991
:: Copyright (c) 1991-2012 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, NAT_1, BINOP_1, FUNCT_1, INT_2, SUBSET_1, ARYTM_3,
      STRUCT_0, XBOOLE_0, LATTICES, ORDINAL1, EQREL_1, PBOOLE, CARD_1, TARSKI,
      XREAL_0, XXREAL_0, QC_LANG1, XCMPLX_0, ZFMISC_1, RELAT_1, REALSET1,
      NAT_LAT, MEMBERED;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, NUMBERS, ORDINAL1, XREAL_0,
      REALSET1, NAT_1, NAT_D, BINOP_1, RELAT_1, FUNCT_1, MEMBERED, XXREAL_0,
      STRUCT_0, LATTICES;
 constructors PARTFUN1, BINOP_1, FINSET_1, XXREAL_0, NAT_D, MEMBERED, REALSET1,
      LATTICES, RELSET_1;
 registrations ORDINAL1, RELSET_1, FINSET_1, XREAL_0, MEMBERED, STRUCT_0,
      LATTICES;
 requirements REAL, NUMERALS, SUBSET, BOOLE;
 definitions TARSKI, XBOOLE_0, LATTICES, BINOP_1, REALSET1, ORDINAL1;
 theorems NEWTON, ZFMISC_1, LATTICES, FUNCT_1, FUNCT_2, XBOOLE_1, RELAT_1,
      ORDINAL1, BINOP_1, RELSET_1;
 schemes BINOP_1, BINOP_2, SUBSET_1;

begin :: Auxiliary Theorems

reserve n,m for Nat;

definition

  func hcflat -> BinOp of NAT means
  :Def1:
  it.(m,n) = m gcd n;
  existence
  proof
    deffunc O(Nat,Nat)= $1 gcd $2;
    consider o being BinOp of NAT such that
A1: for a,b being Element of NAT holds o.(a,b) = O(a,b) from BINOP_1:
    sch 4;
    take o;
    let m,n;
    m in NAT & n in NAT by ORDINAL1:def 12;
    hence thesis by A1;
  end;
  uniqueness
  proof
    let f1,f2 be BinOp of NAT such that
A2: f1.(m,n)=m gcd n and
A3: f2.(m,n)=m gcd n;
    now
      let m,n be Element of NAT;
      thus f1.(m,n) = m gcd n by A2
        .= f2.(m,n) by A3;
    end;
    hence thesis by BINOP_1:2;
  end;
  func lcmlat -> BinOp of NAT means
  :Def2:
  it.(m,n) = m lcm n;
  existence
  proof
    deffunc O(Nat,Nat)= $1 lcm $2;
    consider o being BinOp of NAT such that
A4: for a,b being Element of NAT holds o.(a,b) = O(a,b) from BINOP_1:
    sch 4;
    take o;
    let m,n;
    m in NAT & n in NAT by ORDINAL1:def 12;
    hence thesis by A4;
  end;
  uniqueness
  proof
    let f1,f2 be BinOp of NAT such that
A5: f1.(m,n)=m lcm n and
A6: f2.(m,n)=m lcm n;
    now
      let m,n be Element of NAT;
      thus f1.(m,n) = m lcm n by A5
        .= f2.(m,n) by A6;
    end;
    hence thesis by BINOP_1:2;
  end;
end;

definition
  func Nat_Lattice -> strict non empty LattStr equals
  LattStr(# NAT, lcmlat, hcflat #);
  coherence;
end;

registration
  cluster the carrier of Nat_Lattice -> natural-membered;
  coherence;
end;

reserve p,q,r for Element of Nat_Lattice;

registration
  let p,q;
  identify p"\/"q with p lcm q;
  compatibility by Def2;
  identify p"/\"q with p gcd q;
  compatibility by Def1;
end;

theorem
  p"\/"q =p lcm q;

theorem
  p"/\"q = p gcd q;

theorem
  for a,b being Element of Nat_Lattice st a [= b holds a divides b
proof
  let a,b be Element of Nat_Lattice;
  assume a[=b;
  then a"\/"b=b by LATTICES:def 3;
  hence thesis by NEWTON:44;
end;

definition
  func 0_NN -> Element of Nat_Lattice equals
  1;
  coherence;
  func 1_NN -> Element of Nat_Lattice equals
  0;
  coherence;
end;

theorem
  0_NN=1;

Lm1: for a being Element of Nat_Lattice holds 0_NN"/\"a = 0_NN & a"/\"0_NN =
0_NN by NEWTON:51;

registration
  cluster Nat_Lattice -> Lattice-like;
  coherence
  proof
    thus (for p,q holds p"\/"q = q"\/"p) & (for p,q,r holds p"\/"(q"\/"r) = (p
"\/"q)"\/"r) & (for p,q holds (p"/\"q)"\/"q = q) & (for p,q holds p"/\"q = q
"/\"p) & (for p,q,r holds p"/\"(q"/\"r) = (p"/\"q)"/\"r) & for p,q holds p"/\"(
    p"\/"q) = p by NEWTON:43,48,53,54;
  end;
end;

registration
  cluster Nat_Lattice -> strict;
  coherence;
end;

reserve p,q,r for Element of Nat_Lattice;

registration
  cluster Nat_Lattice -> lower-bounded;
  coherence by Lm1,LATTICES:def 13;
end;

theorem Th5:
  lcmlat.(p,q)=lcmlat.(q,p)
proof
  thus lcmlat.(p,q)=q"\/"p by LATTICES:def 1
    .=lcmlat.(q,p);
end;

theorem Th6:
  hcflat.(q,p)=hcflat.(p,q)
proof
  thus hcflat.(q,p)=p"/\"q by LATTICES:def 2
    .=hcflat.(p,q);
end;

theorem Th7:
  lcmlat.(p,lcmlat.(q,r)) = lcmlat.(lcmlat.(p,q),r)
proof
  set s=q"\/"r;
  thus lcmlat.(p,lcmlat.(q,r))=p"\/"s .=(p"\/"q)"\/"r by NEWTON:43
    .=lcmlat.(lcmlat.(p,q),r);
end;

theorem
  lcmlat.(p,lcmlat.(q,r)) = lcmlat.(lcmlat.(q,p),r) & lcmlat.(p,lcmlat.(
q,r)) = lcmlat.(lcmlat.(p,r),q) & lcmlat.(p,lcmlat.(q,r)) = lcmlat.(lcmlat.(r,q
  ),p) & lcmlat.(p,lcmlat.(q,r)) = lcmlat.(lcmlat.(r,p),q)
proof
  set s=r"\/"q;
  thus lcmlat.(p,lcmlat.(q,r)) =lcmlat.(lcmlat.(p,q),r) by Th7
    .= lcmlat.(lcmlat.(q,p),r) by Th5;
  thus
A1: lcmlat.(p,lcmlat.(q,r)) = lcmlat.(p,lcmlat.(r,q)) by Th5
    .=lcmlat.(lcmlat.(p,r),q) by Th7;
  thus lcmlat.(p,lcmlat.(q,r)) = lcmlat.(p,s) by LATTICES:def 1
    .=lcmlat.(lcmlat.(r,q),p) by Th5;
  thus thesis by A1,Th5;
end;

theorem Th9:
  hcflat.(p,hcflat.(q,r)) = hcflat.(hcflat.(p,q),r)
proof
  set s=q"/\"r;
  thus hcflat.(p,hcflat.(q,r))=p"/\"s .=(p"/\"q)"/\"r by NEWTON:48
    .=hcflat.(hcflat.(p,q),r);
end;

theorem
  hcflat.(p,hcflat.(q,r)) = hcflat.(hcflat.(q,p),r) & hcflat.(p,hcflat.(
q,r)) = hcflat.(hcflat.(p,r),q) & hcflat.(p,hcflat.(q,r)) = hcflat.(hcflat.(r,q
  ),p) & hcflat.(p,hcflat.(q,r)) = hcflat.(hcflat.(r,p),q)
proof
  set s=r"/\"q;
  thus hcflat.(p,hcflat.(q,r)) =hcflat.(hcflat.(p,q),r) by Th9
    .= hcflat.(hcflat.(q,p),r) by Th6;
  thus
A1: hcflat.(p,hcflat.(q,r)) = hcflat.(p,hcflat.(r,q)) by Th6
    .=hcflat.(hcflat.(p,r),q) by Th9;
  thus hcflat.(p,hcflat.(q,r)) = hcflat.(p,s) by LATTICES:def 2
    .=hcflat.(hcflat.(r,q),p) by Th6;
  thus thesis by A1,Th6;
end;

theorem
  hcflat.(q,lcmlat.(q,p))=q & hcflat.(lcmlat.(p,q),q)=q & hcflat.(q,
  lcmlat.(p,q))=q & hcflat.(lcmlat.(q,p),q)=q
proof
  set s=q"\/"p;
  thus
A1: hcflat.(q,lcmlat.(q,p))=q"/\"s .=q by NEWTON:54;
  thus
A2: hcflat.(lcmlat.(p,q),q)=hcflat.(p"\/"q,q) .=q"/\"(q"\/"p) by LATTICES:def 2
    .=q by NEWTON:54;
  thus hcflat.(q,lcmlat.(p,q))=q by A1,Th5;
  thus thesis by A2,Th5;
end;

theorem
  lcmlat.(q,hcflat.(q,p))=q & lcmlat.(hcflat.(p,q),q)=q & lcmlat.(q,
  hcflat.(p,q))=q & lcmlat.(hcflat.(q,p),q)=q
proof
  set r=p"/\"q;
  thus
A1: lcmlat.(q,hcflat.(q,p))=lcmlat.(q,q"/\"p) .=(p"/\"q)"\/"q by LATTICES:def 1
    .=q by NEWTON:53;
  thus
A2: lcmlat.(hcflat.(p,q),q)=r"\/"q .=q by NEWTON:53;
  thus lcmlat.(q,hcflat.(p,q))=q by A1,Th6;
  thus thesis by A2,Th6;
end;

:: NATPLUS

definition

  func NATPLUS -> Subset of NAT means
  :Def6:
  for n being Nat holds n in it iff 0 < n;
  existence
  proof
    defpred P[Nat] means 0 < $1;
    consider X being Subset of NAT such that
A1: for n being Element of NAT holds n in X iff P[n] from SUBSET_1:sch
    3;
    take X;
    let n be Nat;
    thus n in X implies 0 < n by A1;
    n in NAT by ORDINAL1:def 12;
    hence thesis by A1;
  end;
  uniqueness
  proof
    let X, Y be Subset of NAT such that
A2: for n being Nat holds n in X iff 0 < n and
A3: for n being Nat holds n in Y iff 0 < n;
    thus X c= Y
    proof
      let x be set;
      assume
A4:   x in X;
      then reconsider x as Nat;
      0 < x by A2,A4;
      hence thesis by A3;
    end;
    let x be set;
    assume
A5: x in Y;
    then reconsider x as Nat;
    0 < x by A3,A5;
    hence thesis by A2;
  end;
end;

registration
  cluster NATPLUS -> non empty;
  coherence
  proof
    0 < 1;
    hence thesis by Def6;
  end;
end;

definition
  let D be non empty set, S be non empty Subset of D,
      N be non empty Subset of S;
  redefine mode Element of N -> Element of S;
  coherence
  proof
    let x be Element of N;
    thus thesis;
  end;
end;

registration
  let D be Subset of REAL;
  cluster -> real for Element of D;
  coherence;
end;

registration
  let D be Subset of NAT;
  cluster -> real for Element of D;
  coherence;
end;

definition
  mode NatPlus is Element of NATPLUS;
end;

:: LATTICE of NATURAL NUMBERS > 0

definition
  let k be Nat such that
A1: k > 0;
  func @k -> NatPlus equals
  :Def7:
  k;
  coherence by A1,Def6;
end;

registration
  cluster -> natural non zero for NatPlus;
  coherence by Def6;
end;

reserve m,n for NatPlus;

definition

  func hcflatplus -> BinOp of NATPLUS means
  :Def8:
  it.(m,n) = m gcd n;
  existence
  proof
    deffunc O(NatPlus,NatPlus)= @($1 gcd $2);
    consider f being BinOp of NATPLUS such that
A1: for m,n being NatPlus holds f.(m,n)=O(m,n) from BINOP_1:sch 4;
    take f;
    let m,n be NatPlus;
A2: f.(m,n)=@(m gcd n) by A1;
    n>0 by Def6;
    hence thesis by A2,Def7,NEWTON:58;
  end;
  uniqueness
  proof
    deffunc O(NatPlus,NatPlus)= $1 gcd $2;
    thus for o1,o2 being BinOp of NATPLUS st (for a,b being NatPlus
holds o1.(a,b) = O(a,b)) & (for a,b being NatPlus holds o2.(a,b) = O
    (a,b)) holds o1 = o2 from BINOP_2:sch 2;
  end;
  func lcmlatplus -> BinOp of NATPLUS means
  :Def9:
  it.(m,n) = m lcm n;
  existence
  proof
    deffunc O(NatPlus,NatPlus)= @($1 lcm $2);
    consider f being BinOp of NATPLUS such that
A3: for m,n being NatPlus holds f.(m,n)=O(m,n) from BINOP_1:sch 4;
    take f;
    let m,n be NatPlus;
A4: m>0 & n>0 by Def6;
    thus f.(m,n) = O(m,n) by A3
    .= m lcm n by A4,Def7,NEWTON:59;
  end;
  uniqueness
  proof
    deffunc O(NatPlus,NatPlus)= $1 lcm $2;
    thus for o1,o2 being BinOp of NATPLUS st (for a,b being NatPlus
holds o1.(a,b) = O(a,b)) & (for a,b being NatPlus holds o2.(a,b) = O
    (a,b)) holds o1 = o2 from BINOP_2:sch 2;
  end;
end;

definition
  func NatPlus_Lattice -> strict LattStr equals
  LattStr (# NATPLUS, lcmlatplus, hcflatplus #);
  coherence;
end;

registration
  cluster NatPlus_Lattice -> non empty;
  coherence;
end;

definition
  let m be Element of NatPlus_Lattice;
  func @m -> NatPlus equals
  m;
  coherence;
end;

registration
  cluster -> natural non zero for Element of NatPlus_Lattice;
  coherence;
end;

reserve p,q for Element of NatPlus_Lattice;

registration
  let p,q be Element of NatPlus_Lattice;
  identify p"\/"q with p lcm q;
  compatibility by Def9;
  identify p"/\"q with p gcd q;
  compatibility by Def8;
end;

theorem
  p"\/"q =@p lcm @q;

theorem
  p"/\"q = @p gcd @q;

Lm2: ( for a,b being Element of NatPlus_Lattice holds a"\/"b = b"\/"a)& for a,
b,c being Element of NatPlus_Lattice holds a"\/"(b"\/"c) = (a"\/"b)"\/"c by
NEWTON:43;

Lm3: ( for a,b being Element of NatPlus_Lattice holds (a"/\"b)"\/"b = b)& for
a,b being Element of NatPlus_Lattice holds a"/\"b = b"/\"a by NEWTON:53;

Lm4: ( for a,b,c being Element of NatPlus_Lattice holds a"/\"(b"/\"c) = (a"/\"
b)"/\" c)& for a,b being Element of NatPlus_Lattice holds a"/\"(a"\/"b) = a by
NEWTON:48,54;

registration
  cluster NatPlus_Lattice -> join-commutative join-associative
    meet-commutative meet-associative join-absorbing meet-absorbing;
  coherence by Lm2,Lm3,Lm4,LATTICES:def 4,def 5,def 6,def 7,def 8,def 9;
end;

Lm5: now
  let L be Lattice;
  [:the carrier of L, the carrier of L:] = dom (the L_join of L) by
FUNCT_2:def 1;
  hence the L_join of L = (the L_join of L)||the carrier of L by RELAT_1:68;
  [:the carrier of L, the carrier of L:] = dom (the L_meet of L) by
FUNCT_2:def 1;
  hence the L_meet of L = (the L_meet of L)||the carrier of L by RELAT_1:68;
end;

definition
  let L be Lattice;
  mode SubLattice of L -> Lattice means
    :Def12:
    the carrier of it c= the
carrier of L & the L_join of it = (the L_join of L)||the carrier of it & the
    L_meet of it = (the L_meet of L)||the carrier of it;
  existence
  proof
    take L;
    thus thesis by Lm5;
  end;
end;

registration
  let L be Lattice;
  cluster strict for SubLattice of L;
  existence
  proof
    set S = LattStr(#the carrier of L, the L_join of L, the L_meet of L#);
A1: now
      let a,b,c be Element of S;
      reconsider a9 = a, b9 = b, c9 = c as Element of L;
      thus a"\/"(b"\/"c) = a9"\/"(b9"\/"c9)
        .= (a9"\/"b9)"\/"c9 by LATTICES:def 5
        .= (a"\/"b)"\/"c;
    end;
A2: now
      let a,b be Element of S;
      reconsider a9 = a, b9 = b as Element of L;
      thus (a"/\"b)"\/"b = (a9"/\"b9)"\/"b9 .= b by LATTICES:def 8;
    end;
A3: now
      let a,b be Element of S;
      reconsider a9 = a, b9 = b as Element of L;
      thus a"/\"(a"\/"b) = a9"/\"(a9"\/"b9) .=a by LATTICES:def 9;
    end;
A4: now
      let a,b,c be Element of S;
      reconsider a9 = a, b9 = b, c9 = c as Element of L;
      thus a"/\"(b"/\"c) = a9"/\"(b9"/\"c9)
        .= (a9"/\"b9)"/\"c9 by LATTICES:def 7
        .= (a"/\"b)"/\"c;
    end;
A5: for a,b be Element of S, a9,b9 be Element of L st a = a9 & b = b9
    holds a"\/"b = a9"\/"b9 & a"/\"b = a9"/\"b9;
A6: now
      let a,b be Element of S;
      reconsider a9 = a, b9 = b as Element of L;
      thus a"/\"b = b9"/\"a9 by A5
        .= b"/\"a;
    end;
    now
      let a,b be Element of S;
      reconsider a9 = a, b9 = b as Element of L;
      thus a"\/"b = b9"\/"a9 by A5
        .= b"\/"a;
    end;
    then S is join-commutative join-associative meet-absorbing
    meet-commutative meet-associative join-absorbing by A1,A2,A6,A4,A3,
LATTICES:def 4,def 5,def 6,def 7,def 8,def 9;
    then reconsider S as Lattice;
    the L_join of S = (the L_join of L)||the carrier of S & the L_meet of
    S = ( the L_meet of L)||the carrier of S by RELSET_1:19;
    then S is SubLattice of L by Def12;
    hence thesis;
  end;
end;

theorem
  for L being Lattice holds L is SubLattice of L
proof
  let L be Lattice;
  thus the carrier of L c= the carrier of L;
  thus thesis by Lm5;
end;

theorem
  NatPlus_Lattice is SubLattice of Nat_Lattice
proof
A1: for x being set st x in dom hcflatplus holds hcflatplus.x = hcflat.x
  proof
    let x be set;
    assume
A2: x in dom hcflatplus;
    then
A3: x in [:NATPLUS,NATPLUS:] by FUNCT_2:def 1;
    consider y1,y2 being set such that
A4: [y1,y2]=x by A2,RELAT_1:def 1;
    y1 in NATPLUS & y2 in NATPLUS by A3,A4,ZFMISC_1:87;
    then reconsider n=y1,k=y2 as Nat;
A5: hcflat.(n,k) = n gcd k by Def1;
    reconsider n=y1,k=y2 as NatPlus by A3,A4,ZFMISC_1:87;
    hcflatplus.(n,k)= hcflat.(n,k) by A5,Def8;
    hence thesis by A4;
  end;
  dom hcflatplus = [:NATPLUS,NATPLUS:] & dom hcflat = [:NAT,NAT:] by
FUNCT_2:def 1;
  then dom hcflatplus = dom hcflat /\ [:NATPLUS,NATPLUS:] by XBOOLE_1:28
,ZFMISC_1:96;
  then
A6: hcflatplus = hcflat||NATPLUS by A1,FUNCT_1:46;
A7: for x being set st x in dom lcmlatplus holds lcmlatplus.x = lcmlat.x
  proof
    let x be set;
    assume
A8: x in dom lcmlatplus;
    then
A9: x in [:NATPLUS,NATPLUS:] by FUNCT_2:def 1;
    consider y1,y2 being set such that
A10: [y1,y2]=x by A8,RELAT_1:def 1;
    y1 in NATPLUS & y2 in NATPLUS by A9,A10,ZFMISC_1:87;
    then reconsider n=y1,k=y2 as Nat;
A11: lcmlat.(n,k) = n lcm k by Def2;
    reconsider n=y1,k=y2 as NatPlus by A9,A10,ZFMISC_1:87;
    lcmlatplus.(n,k)= lcmlat.(n,k) by A11,Def9;
    hence thesis by A10;
  end;
  dom lcmlatplus = [:NATPLUS,NATPLUS:] & dom lcmlat = [:NAT,NAT:] by
FUNCT_2:def 1;
  then dom lcmlatplus = dom lcmlat /\ [:NATPLUS,NATPLUS:] by XBOOLE_1:28
,ZFMISC_1:96;
  then lcmlatplus = lcmlat||NATPLUS by A7,FUNCT_1:46;
  hence thesis by A6,Def12;
end;