:: 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


begin

definition
func hcflat  ->  BinOp of NAT means :Def1: :: NAT_LAT:def 1
 for m, n being Nat holds it . (m,n) = m gcd n;
existence
 ex b1 being BinOp of NAT st
for m, n being Nat holds b1 . (m,n) = m gcd n
proofend;
uniqueness
 for b1, b2 being BinOp of NAT st ( for m, n being Nat holds b1 . (m,n) = m gcd n ) & ( for m, n being Nat holds b2 . (m,n) = m gcd n ) holds
b1 = b2
proofend;
func lcmlat  ->  BinOp of NAT means :Def2: :: NAT_LAT:def 2
 for m, n being Nat holds it . (m,n) = m lcm n;
existence
 ex b1 being BinOp of NAT st
for m, n being Nat holds b1 . (m,n) = m lcm n
proofend;
uniqueness
 for b1, b2 being BinOp of NAT st ( for m, n being Nat holds b1 . (m,n) = m lcm n ) & ( for m, n being Nat holds b2 . (m,n) = m lcm n ) holds
b1 = b2
proofend;
end;

:: deftheorem Def1 defines hcflat NAT_LAT:def_1_:_
 for b1 being BinOp of NAT holds
( b1 = hcflat iff for m, n being Nat holds b1 . (m,n) = m gcd n );

:: deftheorem Def2 defines lcmlat NAT_LAT:def_2_:_
 for b1 being BinOp of NAT holds
( b1 = lcmlat iff for m, n being Nat holds b1 . (m,n) = m lcm n );

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

:: deftheorem  defines Nat_Lattice NAT_LAT:def_3_:_
 Nat_Lattice = LattStr(# NAT,lcmlat,hcflat #);

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

registration
let p, q be Element of Nat_Lattice;
identifyp "\/" q with p lcm q;
compatibility
 p "\/" q = p lcm q by Def2;
identifyp "/\" q with p gcd q;
compatibility
 p "/\" q = p gcd q by Def1;
end;

theorem :: NAT_LAT:1
for p, q being Element of Nat_Lattice holds p "\/" q = p lcm q ;

theorem :: NAT_LAT:2
for p, q being Element of Nat_Lattice holds p "/\" q = p gcd q ;

theorem :: NAT_LAT:3
for a, b being Element of Nat_Lattice st a [= b holds
a divides b
proofend;

definition
func 0_NN  ->  Element of Nat_Lattice equals :: NAT_LAT:def 4
1;
coherence
 1 is Element of Nat_Lattice ;
func 1_NN  ->  Element of Nat_Lattice equals :: NAT_LAT:def 5
 0 ;
coherence
 0 is Element of Nat_Lattice ;
end;

:: deftheorem  defines 0_NN NAT_LAT:def_4_:_
 0_NN = 1;

:: deftheorem  defines 1_NN NAT_LAT:def_5_:_
 1_NN = 0 ;

theorem :: NAT_LAT:4
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  ->  non empty strict Lattice-like ;
coherence
 Nat_Lattice is Lattice-like
proofend;
end;

registration
cluster Nat_Lattice  ->  non empty strict ;
coherence
 Nat_Lattice is strict ;
end;

registration
cluster Nat_Lattice  ->  non empty strict lower-bounded ;
coherence
 Nat_Lattice is lower-bounded by Lm1, LATTICES:def_13;
end;

theorem Th5: :: NAT_LAT:5
for p, q being Element of Nat_Lattice holds lcmlat . (p,q) = lcmlat . (q,p)
proofend;

theorem Th6: :: NAT_LAT:6
for q, p being Element of Nat_Lattice holds hcflat . (q,p) = hcflat . (p,q)
proofend;

theorem Th7: :: NAT_LAT:7
for p, q, r being Element of Nat_Lattice holds lcmlat . (p,(lcmlat . (q,r))) = lcmlat . ((lcmlat . (p,q)),r)
proofend;

theorem :: NAT_LAT:8
for p, q, r being Element of Nat_Lattice holds
( 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) )
proofend;

theorem Th9: :: NAT_LAT:9
for p, q, r being Element of Nat_Lattice holds hcflat . (p,(hcflat . (q,r))) = hcflat . ((hcflat . (p,q)),r)
proofend;

theorem :: NAT_LAT:10
for p, q, r being Element of Nat_Lattice holds
( 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) )
proofend;

theorem :: NAT_LAT:11
for q, p being Element of Nat_Lattice holds
( hcflat . (q,(lcmlat . (q,p))) = q & hcflat . ((lcmlat . (p,q)),q) = q & hcflat . (q,(lcmlat . (p,q))) = q & hcflat . ((lcmlat . (q,p)),q) = q )
proofend;

theorem :: NAT_LAT:12
for q, p being Element of Nat_Lattice holds
( lcmlat . (q,(hcflat . (q,p))) = q & lcmlat . ((hcflat . (p,q)),q) = q & lcmlat . (q,(hcflat . (p,q))) = q & lcmlat . ((hcflat . (q,p)),q) = q )
proofend;

:: NATPLUS
definition
func NATPLUS  ->  Subset of NAT means :Def6: :: NAT_LAT:def 6
 for n being Nat holds
( n in it iff 0 < n );
existence
 ex b1 being Subset of NAT st
for n being Nat holds
( n in b1 iff 0 < n )
proofend;
uniqueness
 for b1, b2 being Subset of NAT st ( for n being Nat holds
( n in b1 iff 0 < n ) ) &amp; ( for n being Nat holds
( n in b2 iff 0 < n ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def6 defines NATPLUS NAT_LAT:def_6_:_
 for b1 being Subset of NAT holds
( b1 = NATPLUS iff for n being Nat holds
( n in b1 iff 0 < n ) );

registration
cluster NATPLUS  ->  non empty ;
coherence
 not NATPLUS is empty
proofend;
end;

definition
let D be non empty set ;
let S be non empty Subset of D;
let N be non empty Subset of S;
:: original:Element
redefine mode Element of N ->  Element of S;
coherence
 for b1 being Element of N holds b1 is Element of S
proofend;
end;

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

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

definition
mode NatPlus is Element of NATPLUS ;
end;

:: LATTICE of NATURAL NUMBERS > 0
definition
let k be Nat;
assume A1: k > 0 ;
func @ k ->  NatPlus equals :Def7: :: NAT_LAT:def 7
k;
coherence
 k is NatPlus by A1, Def6;
end;

:: deftheorem Def7 defines @ NAT_LAT:def_7_:_
 for k being Nat st k > 0 holds
@ k = k;

registration
cluster  ->  non zero natural for Element of NATPLUS ;
coherence
 for b1 being NatPlus holds
( b1 is natural &amp; not b1 is zero ) by Def6;
end;

definition
func hcflatplus  ->  BinOp of NATPLUS means :Def8: :: NAT_LAT:def 8
 for m, n being NatPlus holds it . (m,n) = m gcd n;
existence
 ex b1 being BinOp of NATPLUS st
for m, n being NatPlus holds b1 . (m,n) = m gcd n
proofend;
uniqueness
 for b1, b2 being BinOp of NATPLUS st ( for m, n being NatPlus holds b1 . (m,n) = m gcd n ) &amp; ( for m, n being NatPlus holds b2 . (m,n) = m gcd n ) holds
b1 = b2
proofend;
func lcmlatplus  ->  BinOp of NATPLUS means :Def9: :: NAT_LAT:def 9
 for m, n being NatPlus holds it . (m,n) = m lcm n;
existence
 ex b1 being BinOp of NATPLUS st
for m, n being NatPlus holds b1 . (m,n) = m lcm n
proofend;
uniqueness
 for b1, b2 being BinOp of NATPLUS st ( for m, n being NatPlus holds b1 . (m,n) = m lcm n ) &amp; ( for m, n being NatPlus holds b2 . (m,n) = m lcm n ) holds
b1 = b2
proofend;
end;

:: deftheorem Def8 defines hcflatplus NAT_LAT:def_8_:_
 for b1 being BinOp of NATPLUS holds
( b1 = hcflatplus iff for m, n being NatPlus holds b1 . (m,n) = m gcd n );

:: deftheorem Def9 defines lcmlatplus NAT_LAT:def_9_:_
 for b1 being BinOp of NATPLUS holds
( b1 = lcmlatplus iff for m, n being NatPlus holds b1 . (m,n) = m lcm n );

definition
func NatPlus_Lattice  ->  strict LattStr  equals :: NAT_LAT:def 10
 LattStr(# NATPLUS,lcmlatplus,hcflatplus #);
coherence
 LattStr(# NATPLUS,lcmlatplus,hcflatplus #) is strict LattStr ;
end;

:: deftheorem  defines NatPlus_Lattice NAT_LAT:def_10_:_
 NatPlus_Lattice = LattStr(# NATPLUS,lcmlatplus,hcflatplus #);

registration
cluster NatPlus_Lattice  ->  non empty strict ;
coherence
 not NatPlus_Lattice is empty ;
end;

definition
let m be Element of NatPlus_Lattice;
func @ m ->  NatPlus equals :: NAT_LAT:def 11
m;
coherence
 m is NatPlus ;
end;

:: deftheorem  defines @ NAT_LAT:def_11_:_
 for m being Element of NatPlus_Lattice holds @ m = m;

registration
cluster  ->  non zero natural for Element of the carrier of NatPlus_Lattice;
coherence
 for b1 being Element of NatPlus_Lattice holds
( b1 is natural &amp; not b1 is zero ) ;
end;

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

theorem :: NAT_LAT:13
for p, q being Element of NatPlus_Lattice holds p "\/" q = (@ p) lcm (@ q) ;

theorem :: NAT_LAT:14
for p, q being Element of NatPlus_Lattice holds p "/\" q = (@ p) gcd (@ q) ;

Lm2:  ( ( for a, b being Element of NatPlus_Lattice holds a "\/" b = b "\/" a ) &amp; ( 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 ) &amp; ( 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 ) &amp; ( for a, b being Element of NatPlus_Lattice holds a "/\" (a "\/" b) = a ) )
by NEWTON:48, NEWTON:54;

registration
cluster NatPlus_Lattice  ->  strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing ;
coherence
 ( NatPlus_Lattice is join-commutative &amp; NatPlus_Lattice is join-associative &amp; NatPlus_Lattice is meet-commutative &amp; NatPlus_Lattice is meet-associative &amp; NatPlus_Lattice is join-absorbing &amp; NatPlus_Lattice is meet-absorbing ) by Lm2, Lm3, Lm4, LATTICES:def_4, LATTICES:def_5, LATTICES:def_6, LATTICES:def_7, LATTICES:def_8, LATTICES:def_9;
end;

Lm5: now__::_thesis:_for_L_being_Lattice_holds_
(_the_L_join_of_L_=_the_L_join_of_L_||_the_carrier_of_L_&amp;_the_L_meet_of_L_=_the_L_meet_of_L_||_the_carrier_of_L_)
let L be Lattice; ::_thesis: ( the L_join of L = the L_join of L || the carrier of L &amp; the L_meet of L = the L_meet of L || the carrier of L )
 [: 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; ::_thesis: the L_meet of L = the L_meet of L || the carrier of L
 [: 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; ::_thesis: verum
end;

definition
let L be Lattice;
mode SubLattice of L ->  Lattice means :Def12: :: NAT_LAT:def 12
( the carrier of it c= the carrier of L &amp; the L_join of it = the L_join of L || the carrier of it &amp; the L_meet of it = the L_meet of L || the carrier of it );
existence
 ex b1 being Lattice st
( the carrier of b1 c= the carrier of L &amp; the L_join of b1 = the L_join of L || the carrier of b1 &amp; the L_meet of b1 = the L_meet of L || the carrier of b1 )
proofend;
end;

:: deftheorem Def12 defines SubLattice NAT_LAT:def_12_:_
 for L, b2 being Lattice holds
( b2 is SubLattice of L iff ( the carrier of b2 c= the carrier of L &amp; the L_join of b2 = the L_join of L || the carrier of b2 &amp; the L_meet of b2 = the L_meet of L || the carrier of b2 ) );

registration
let L be Lattice;
cluster non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like for SubLattice of L;
existence
 ex b1 being SubLattice of L st b1 is strict
proofend;
end;

theorem :: NAT_LAT:15
for L being Lattice holds L is SubLattice of L
proofend;

theorem :: NAT_LAT:16
NatPlus_Lattice is SubLattice of Nat_Lattice
proofend;