:: 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 Association of Mizar Users
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 b1 being BinOp of NAT st
for m, n being Nat holds b1 . m,n = m gcd n
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
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 b1 being BinOp of NAT st
for m, n being Nat holds b1 . m,n = m lcm n
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
end;
:: deftheorem NAT_LAT:def 1 :
canceled;
:: deftheorem NAT_LAT:def 2 :
canceled;
:: deftheorem Def3 defines hcflat NAT_LAT:def 3 :
:: deftheorem Def4 defines lcmlat NAT_LAT:def 4 :
:: deftheorem defines Nat_Lattice NAT_LAT:def 5 :
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
theorem :: NAT_LAT:49
theorem :: NAT_LAT:50
canceled;
theorem :: NAT_LAT:51
canceled;
theorem :: NAT_LAT:52
:: deftheorem defines 0_NN NAT_LAT:def 6 :
:: deftheorem defines 1_NN NAT_LAT:def 7 :
theorem :: NAT_LAT:53
canceled;
theorem :: NAT_LAT:54
canceled;
theorem :: NAT_LAT:55
Lm1:
for a being Element of Nat_Lattice holds
( 0_NN "/\" a = 0_NN & a "/\" 0_NN = 0_NN )
by NEWTON:64;
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
theorem Th62: :: NAT_LAT:62
theorem Th63: :: NAT_LAT:63
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 )
theorem Th65: :: NAT_LAT:65
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 )
theorem :: NAT_LAT:67
theorem :: NAT_LAT:68
:: deftheorem NAT_LAT:def 8 :
canceled;
:: deftheorem Def9 defines NATPLUS NAT_LAT:def 9 :
:: deftheorem Def10 defines @ NAT_LAT:def 10 :
for
k being
Nat st
k > 0 holds
@ k = k;
:: deftheorem defines @ NAT_LAT:def 11 :
definition
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 b1 being BinOp of NATPLUS st
for m, n being NatPlus holds b1 . m,n = m gcd n
uniqueness
for b1, b2 being BinOp of NATPLUS st ( for m, n being NatPlus holds b1 . m,n = m gcd n ) & ( for m, n being NatPlus holds b2 . m,n = m gcd n ) holds
b1 = b2
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 b1 being BinOp of NATPLUS st
for m, n being NatPlus holds b1 . m,n = m lcm n
uniqueness
for b1, b2 being BinOp of NATPLUS st ( for m, n being NatPlus holds b1 . m,n = m lcm n ) & ( for m, n being NatPlus holds b2 . m,n = m lcm n ) holds
b1 = b2
end;
:: deftheorem Def12 defines hcflatplus NAT_LAT:def 12 :
:: deftheorem Def13 defines lcmlatplus NAT_LAT:def 13 :
:: deftheorem defines NatPlus_Lattice NAT_LAT:def 14 :
:: deftheorem defines @ NAT_LAT:def 15 :
theorem :: NAT_LAT:69
theorem :: NAT_LAT:70
Lm2:
for a, b being Element of NatPlus_Lattice holds a "\/" b = b "\/" a
;
Lm3:
for a, b, c being Element of NatPlus_Lattice holds a "\/" (b "\/" c) = (a "\/" b) "\/" c
by NEWTON:56;
Lm4:
for a, b being Element of NatPlus_Lattice holds (a "/\" b) "\/" b = b
by NEWTON:66;
Lm5:
for a, b being Element of NatPlus_Lattice holds a "/\" b = b "/\" a
;
Lm6:
for a, b, c being Element of NatPlus_Lattice holds a "/\" (b "/\" c) = (a "/\" b) "/\" c
by NEWTON:61;
Lm7:
for a, b being Element of NatPlus_Lattice holds a "/\" (a "\/" b) = a
by 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, Lm5, Lm6, Lm7, LATTICES:def 4, LATTICES:def 5, LATTICES:def 6, LATTICES:def 7, LATTICES:def 8, LATTICES:def 9;
end;
:: deftheorem Def16 defines SubLattice NAT_LAT:def 16 :
theorem :: NAT_LAT:71
canceled;
theorem :: NAT_LAT:72
canceled;
theorem :: NAT_LAT:73
canceled;
theorem :: NAT_LAT:74
canceled;
theorem :: NAT_LAT:75
theorem :: NAT_LAT:76