:: 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-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, 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, ORDINAL1, NUMBERS, 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; begin :: Auxiliary Theorems reserve n,m for Nat; definition func hcflat -> BinOp of NAT means :: NAT_LAT:def 1 it.(m,n) = m gcd n; func lcmlat -> BinOp of NAT means :: NAT_LAT:def 2 it.(m,n) = m lcm n; end; definition func Nat_Lattice -> strict non empty LattStr equals :: NAT_LAT:def 3 LattStr(# NAT, lcmlat, hcflat #); end; registration cluster the carrier of Nat_Lattice -> natural-membered; end; reserve p,q,r for Element of Nat_Lattice; registration let p,q; identify p"\/"q with p lcm q; identify p"/\"q with p gcd q; end; theorem :: NAT_LAT:1 p"\/"q =p lcm q; theorem :: NAT_LAT:2 p"/\"q = p gcd q; theorem :: NAT_LAT:3 for a,b being Element of Nat_Lattice st a [= b holds a divides b; definition func 0_NN -> Element of Nat_Lattice equals :: NAT_LAT:def 4 1; func 1_NN -> Element of Nat_Lattice equals :: NAT_LAT:def 5 0; end; theorem :: NAT_LAT:4 0_NN=1; registration cluster Nat_Lattice -> Lattice-like; end; registration cluster Nat_Lattice -> strict; end; reserve p,q,r for Element of Nat_Lattice; registration cluster Nat_Lattice -> lower-bounded; end; theorem :: NAT_LAT:5 lcmlat.(p,q)=lcmlat.(q,p); theorem :: NAT_LAT:6 hcflat.(q,p)=hcflat.(p,q); theorem :: NAT_LAT:7 lcmlat.(p,lcmlat.(q,r)) = lcmlat.(lcmlat.(p,q),r); theorem :: NAT_LAT:8 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); theorem :: NAT_LAT:9 hcflat.(p,hcflat.(q,r)) = hcflat.(hcflat.(p,q),r); theorem :: NAT_LAT:10 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); theorem :: NAT_LAT:11 hcflat.(q,lcmlat.(q,p))=q & hcflat.(lcmlat.(p,q),q)=q & hcflat.(q, lcmlat.(p,q))=q & hcflat.(lcmlat.(q,p),q)=q; theorem :: NAT_LAT:12 lcmlat.(q,hcflat.(q,p))=q & lcmlat.(hcflat.(p,q),q)=q & lcmlat.(q, hcflat.(p,q))=q & lcmlat.(hcflat.(q,p),q)=q; :: NATPLUS definition func NATPLUS -> Subset of NAT means :: NAT_LAT:def 6 for n being Nat holds n in it iff 0 < n; end; registration cluster NATPLUS -> non empty; 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; end; registration let D be Subset of REAL; cluster -> real for Element of D; end; registration let D be Subset of NAT; cluster -> real for Element of D; end; definition mode NatPlus is Element of NATPLUS; end; :: LATTICE of NATURAL NUMBERS > 0 definition let k be Nat such that k > 0; func @k -> NatPlus equals :: NAT_LAT:def 7 k; end; registration cluster -> natural non zero for NatPlus; end; reserve m,n for NatPlus; definition func hcflatplus -> BinOp of NATPLUS means :: NAT_LAT:def 8 it.(m,n) = m gcd n; func lcmlatplus -> BinOp of NATPLUS means :: NAT_LAT:def 9 it.(m,n) = m lcm n; end; definition func NatPlus_Lattice -> strict LattStr equals :: NAT_LAT:def 10 LattStr (# NATPLUS, lcmlatplus, hcflatplus #); end; registration cluster NatPlus_Lattice -> non empty; end; definition let m be Element of NatPlus_Lattice; func @m -> NatPlus equals :: NAT_LAT:def 11 m; end; registration cluster -> natural non zero for Element of NatPlus_Lattice; 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; identify p"/\"q with p gcd q; end; theorem :: NAT_LAT:13 p"\/"q =@p lcm @q; theorem :: NAT_LAT:14 p"/\"q = @p gcd @q; registration cluster NatPlus_Lattice -> join-commutative join-associative meet-commutative meet-associative join-absorbing meet-absorbing; end; definition let L be Lattice; mode SubLattice of L -> Lattice means :: NAT_LAT:def 12 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; end; registration let L be Lattice; cluster strict for SubLattice of L; end; theorem :: NAT_LAT:15 for L being Lattice holds L is SubLattice of L; theorem :: NAT_LAT:16 NatPlus_Lattice is SubLattice of Nat_Lattice;