:: 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-2011 Association of Mizar Users

begin

definition

canceled;
canceled;
func hcflat -> BinOp of NAT means :Def3: :: NAT_LAT:def 3
for m, n being Nat holds it . (m,n) = m gcd n;
existence
ex b₁ being BinOp of NAT st
for m, n being Nat holds b₁ . (m,n) = m gcd n

proof end;

uniqueness
for b₁, b₂ being BinOp of NAT st ( for m, n being Nat holds b₁ . (m,n) = m gcd n ) & ( for m, n being Nat holds b₂ . (m,n) = m gcd n ) holds
b₁ = b₂

proof end;

func lcmlat -> BinOp of NAT means :Def4: :: NAT_LAT:def 4
for m, n being Nat holds it . (m,n) = m lcm n;
existence
ex b₁ being BinOp of NAT st
for m, n being Nat holds b₁ . (m,n) = m lcm n

proof end;

uniqueness
for b₁, b₂ being BinOp of NAT st ( for m, n being Nat holds b₁ . (m,n) = m lcm n ) & ( for m, n being Nat holds b₂ . (m,n) = m lcm n ) holds
b₁ = b₂

proof end;

end;

:: deftheorem NAT_LAT:def 1 :
canceled;

:: deftheorem NAT_LAT:def 2 :
canceled;

:: deftheorem Def3 defines hcflat NAT_LAT:def 3 :
for b₁ being BinOp of NAT holds
( b₁ = hcflat iff for m, n being Nat holds b₁ . (m,n) = m gcd n );

:: deftheorem Def4 defines lcmlat NAT_LAT:def 4 :
for b₁ being BinOp of NAT holds
( b₁ = lcmlat iff for m, n being Nat holds b₁ . (m,n) = m lcm n );

definition

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

end;

:: deftheorem defines Nat_Lattice NAT_LAT:def 5 :
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;
identify p "\/" q with p lcm q;
compatibility
p "\/" q = p lcm q by Def4;
identify p "/\" q with p gcd q;
compatibility
p "/\" q = p gcd q by Def3;

end;

theorem :: NAT_LAT:1

canceled;

theorem :: NAT_LAT:2

canceled;

theorem :: NAT_LAT:3

canceled;

theorem :: NAT_LAT:4

canceled;

theorem :: NAT_LAT:5

canceled;

theorem :: NAT_LAT:6

canceled;

theorem :: NAT_LAT:7

canceled;

theorem :: NAT_LAT:8

canceled;

theorem :: NAT_LAT:9

canceled;

theorem :: NAT_LAT:10

canceled;

theorem :: NAT_LAT:11

canceled;

theorem :: NAT_LAT:12

canceled;

theorem :: NAT_LAT:13

canceled;

theorem :: NAT_LAT:14

canceled;

theorem :: NAT_LAT:15

canceled;

theorem :: NAT_LAT:16

canceled;

theorem :: NAT_LAT:17

canceled;

theorem :: NAT_LAT:18

canceled;

theorem :: NAT_LAT:19

canceled;

theorem :: NAT_LAT:20

canceled;

theorem :: NAT_LAT:21

canceled;

theorem :: NAT_LAT:22

canceled;

theorem :: NAT_LAT:23

canceled;

theorem :: NAT_LAT:24

canceled;

theorem :: NAT_LAT:25

canceled;

theorem :: NAT_LAT:26

canceled;

theorem :: NAT_LAT:27

canceled;

theorem :: NAT_LAT:28

canceled;

theorem :: NAT_LAT:29

canceled;

theorem :: NAT_LAT:30

canceled;

theorem :: NAT_LAT:31

canceled;

theorem :: NAT_LAT:32

canceled;

theorem :: NAT_LAT:33

canceled;

theorem :: NAT_LAT:34

canceled;

theorem :: NAT_LAT:35

canceled;

theorem :: NAT_LAT:36

canceled;

theorem :: NAT_LAT:37

canceled;

theorem :: NAT_LAT:38

canceled;

theorem :: NAT_LAT:39

canceled;

theorem :: NAT_LAT:40

canceled;

theorem :: NAT_LAT:41

canceled;

theorem :: NAT_LAT:42

canceled;

theorem :: NAT_LAT:43

canceled;

theorem :: NAT_LAT:44

canceled;

theorem :: NAT_LAT:45

canceled;

theorem :: NAT_LAT:46

canceled;

theorem :: NAT_LAT:47

canceled;

theorem :: NAT_LAT:48

for p, q being Element of Nat_Lattice holds p "\/" q = p lcm q ;

theorem :: NAT_LAT:49

for p, q being Element of Nat_Lattice holds p "/\" q = p gcd q ;

theorem :: NAT_LAT:50

canceled;

theorem :: NAT_LAT:51

canceled;

theorem :: NAT_LAT:52

for a, b being Element of Nat_Lattice st a [= b holds
a divides b

proof end;

definition

func 0_NN -> Element of Nat_Lattice equals :: NAT_LAT:def 6
1;
coherence
1 is Element of Nat_Lattice ;
func 1_NN -> Element of Nat_Lattice equals :: NAT_LAT:def 7
0 ;
coherence
0 is Element of Nat_Lattice ;

end;

:: deftheorem defines 0_NN NAT_LAT:def 6 :
0_NN = 1;

:: deftheorem defines 1_NN NAT_LAT:def 7 :
1_NN = 0 ;

theorem :: NAT_LAT:53

canceled;

theorem :: NAT_LAT:54

canceled;

theorem :: NAT_LAT:55

0_NN = 1 ;

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

registration

cluster Nat_Lattice -> non empty strict Lattice-like ;
coherence
Nat_Lattice is Lattice-like

proof end;

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

canceled;

theorem :: NAT_LAT:57

canceled;

theorem :: NAT_LAT:58

canceled;

theorem :: NAT_LAT:59

canceled;

theorem :: NAT_LAT:60

canceled;

theorem Th61: :: NAT_LAT:61

for p, q being Element of Nat_Lattice holds lcmlat . (p,q) = lcmlat . (q,p)

proof end;

theorem Th62: :: NAT_LAT:62

for q, p being Element of Nat_Lattice holds hcflat . (q,p) = hcflat . (p,q)

proof end;

theorem Th63: :: NAT_LAT:63

for p, q, r being Element of Nat_Lattice holds lcmlat . (p,(lcmlat . (q,r))) = lcmlat . ((lcmlat . (p,q)),r)

proof end;

theorem :: NAT_LAT:64

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

proof end;

theorem Th65: :: NAT_LAT:65

for p, q, r being Element of Nat_Lattice holds hcflat . (p,(hcflat . (q,r))) = hcflat . ((hcflat . (p,q)),r)

proof end;

theorem :: NAT_LAT:66

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

proof end;

theorem :: NAT_LAT:67

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 )

proof end;

theorem :: NAT_LAT:68

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 )

proof end;

definition

canceled;
func NATPLUS -> Subset of NAT means :Def9: :: NAT_LAT:def 9
for n being Nat holds
( n in it iff 0 < n );
existence
ex b₁ being Subset of NAT st
for n being Nat holds
( n in b₁ iff 0 < n )

proof end;

uniqueness
for b₁, b₂ being Subset of NAT st ( for n being Nat holds
( n in b₁ iff 0 < n ) ) & ( for n being Nat holds
( n in b₂ iff 0 < n ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem NAT_LAT:def 8 :
canceled;

:: deftheorem Def9 defines NATPLUS NAT_LAT:def 9 :
for b₁ being Subset of NAT holds
( b₁ = NATPLUS iff for n being Nat holds
( n in b₁ iff 0 < n ) );

registration

cluster NATPLUS -> non empty ;
coherence
not NATPLUS is empty

proof end;

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 b₁ being Element of N holds b₁ is Element of S

proof end;

end;

registration

let D be Subset of REAL;
cluster -> real Element of D;
coherence
for b₁ being Element of D holds b₁ is real ;

end;

registration

let D be Subset of NAT;
cluster -> real Element of D;
coherence
for b₁ being Element of D holds b₁ is real ;

end;

definition

mode NatPlus is Element of NATPLUS ;

end;

definition

let k be Nat;
assume A1: k > 0 ;
func @ k -> NatPlus equals :Def10: :: NAT_LAT:def 10
k;
coherence
k is NatPlus by A1, Def9;

end;

:: deftheorem Def10 defines @ NAT_LAT:def 10 :
for k being Nat st k > 0 holds
@ k = k;

registration

cluster -> non zero natural Element of NATPLUS ;
coherence
for b₁ being NatPlus holds
( b₁ is natural & not b₁ is empty ) by Def9;

end;

definition

canceled;
func hcflatplus -> BinOp of NATPLUS means :Def12: :: NAT_LAT:def 12
for m, n being NatPlus holds it . (m,n) = m gcd n;
existence
ex b₁ being BinOp of NATPLUS st
for m, n being NatPlus holds b₁ . (m,n) = m gcd n

proof end;

uniqueness
for b₁, b₂ being BinOp of NATPLUS st ( for m, n being NatPlus holds b₁ . (m,n) = m gcd n ) & ( for m, n being NatPlus holds b₂ . (m,n) = m gcd n ) holds
b₁ = b₂

proof end;

func lcmlatplus -> BinOp of NATPLUS means :Def13: :: NAT_LAT:def 13
for m, n being NatPlus holds it . (m,n) = m lcm n;
existence
ex b₁ being BinOp of NATPLUS st
for m, n being NatPlus holds b₁ . (m,n) = m lcm n

proof end;

uniqueness
for b₁, b₂ being BinOp of NATPLUS st ( for m, n being NatPlus holds b₁ . (m,n) = m lcm n ) & ( for m, n being NatPlus holds b₂ . (m,n) = m lcm n ) holds
b₁ = b₂

proof end;

end;

:: deftheorem NAT_LAT:def 11 :
canceled;

:: deftheorem Def12 defines hcflatplus NAT_LAT:def 12 :
for b₁ being BinOp of NATPLUS holds
( b₁ = hcflatplus iff for m, n being NatPlus holds b₁ . (m,n) = m gcd n );

:: deftheorem Def13 defines lcmlatplus NAT_LAT:def 13 :
for b₁ being BinOp of NATPLUS holds
( b₁ = lcmlatplus iff for m, n being NatPlus holds b₁ . (m,n) = m lcm n );

definition

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

end;

:: deftheorem defines NatPlus_Lattice NAT_LAT:def 14 :
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 15
m;
coherence
m is NatPlus ;

end;

:: deftheorem defines @ NAT_LAT:def 15 :
for m being Element of NatPlus_Lattice holds @ m = m;

registration

cluster -> non zero natural Element of the carrier of NatPlus_Lattice;
coherence
for b₁ being Element of NatPlus_Lattice holds
( b₁ is natural & not b₁ is empty ) ;

end;

registration

let p, q be Element of NatPlus_Lattice;
identify p "\/" q with p lcm q;
compatibility
p "\/" q = p lcm q by Def13;
identify p "/\" q with p gcd q;
compatibility
p "/\" q = p gcd q by Def12;

end;

theorem :: NAT_LAT:69

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

theorem :: NAT_LAT:70

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

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

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:61, NEWTON:67;

registration

cluster NatPlus_Lattice -> strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing ;
coherence
( NatPlus_Lattice is join-commutative & NatPlus_Lattice is join-associative & NatPlus_Lattice is meet-commutative & NatPlus_Lattice is meet-associative & NatPlus_Lattice is join-absorbing & 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

let L be Lattice; :: thesis: ( the L_join of L = the L_join of L || the carrier of L & 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:97; :: 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:97; :: thesis: verum

end;

definition

let L be Lattice;
mode SubLattice of L -> Lattice means :Def16: :: NAT_LAT:def 16
( 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
ex b₁ being Lattice st
( the carrier of b₁ c= the carrier of L & the L_join of b₁ = the L_join of L || the carrier of b₁ & the L_meet of b₁ = the L_meet of L || the carrier of b₁ )

proof end;

end;

:: deftheorem Def16 defines SubLattice NAT_LAT:def 16 :
for L, b₂ being Lattice holds
( b₂ is SubLattice of L iff ( the carrier of b₂ c= the carrier of L & the L_join of b₂ = the L_join of L || the carrier of b₂ & the L_meet of b₂ = the L_meet of L || the carrier of b₂ ) );

registration

let L be Lattice;
cluster non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like SubLattice of L;
existence
ex b₁ being SubLattice of L st b₁ is strict

proof end;

end;

theorem :: NAT_LAT:71

canceled;

theorem :: NAT_LAT:72

canceled;

theorem :: NAT_LAT:73

canceled;

theorem :: NAT_LAT:74

canceled;

theorem :: NAT_LAT:75

for L being Lattice holds L is SubLattice of L

proof end;

theorem :: NAT_LAT:76

NatPlus_Lattice is SubLattice of Nat_Lattice

proof end;