:: 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-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, 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;
definitions TARSKI, XBOOLE_0, LATTICES;
equalities XBOOLE_0, LATTICES, BINOP_1, REALSET1;
expansions TARSKI, LATTICES, BINOP_1;
theorems NEWTON, ZFMISC_1, LATTICES, FUNCT_1, FUNCT_2, XBOOLE_1, RELAT_1,
ORDINAL1, 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;
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;
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
by NEWTON:44;
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;
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
by A2,A3;
let x be object;
assume
A4: x in Y;
then reconsider x as Nat;
0 < x by A3,A4;
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; :: redefines Element (SUBSET_1, definition)
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;
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;
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 object st x in dom hcflatplus holds hcflatplus.x = hcflat.x
proof
let x be object;
assume
A2: x in dom hcflatplus;
then
A3: x in [:NATPLUS,NATPLUS:] by FUNCT_2:def 1;
consider y1,y2 being object 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 object st x in dom lcmlatplus holds lcmlatplus.x = lcmlat.x
proof
let x be object;
assume
A8: x in dom lcmlatplus;
then
A9: x in [:NATPLUS,NATPLUS:] by FUNCT_2:def 1;
consider y1,y2 being object 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;