environ
vocabularies HIDDEN, 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 HIDDEN, 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;
definitions TARSKI, XBOOLE_0, LATTICES;
theorems NEWTON, ZFMISC_1, LATTICES, FUNCT_1, FUNCT_2, XBOOLE_1, RELAT_1, ORDINAL1, RELSET_1;
schemes BINOP_1, BINOP_2, SUBSET_1;
registrations ORDINAL1, RELSET_1, FINSET_1, XREAL_0, MEMBERED, STRUCT_0, LATTICES;
constructors HIDDEN, PARTFUN1, BINOP_1, FINSET_1, XXREAL_0, NAT_D, MEMBERED, REALSET1, LATTICES, RELSET_1;
requirements HIDDEN, REAL, NUMERALS, SUBSET, BOOLE;
equalities XBOOLE_0, LATTICES, BINOP_1, REALSET1;
expansions TARSKI, LATTICES, BINOP_1;
definition
existence
ex b1 being BinOp of NAT st
for n, m being Nat holds b1 . (m,n) = m gcd n
uniqueness
for b1, b2 being BinOp of NAT st ( for n, m being Nat holds b1 . (m,n) = m gcd n ) & ( for n, m being Nat holds b2 . (m,n) = m gcd n ) holds
b1 = b2
existence
ex b1 being BinOp of NAT st
for n, m being Nat holds b1 . (m,n) = m lcm n
uniqueness
for b1, b2 being BinOp of NAT st ( for n, m being Nat holds b1 . (m,n) = m lcm n ) & ( for n, m being Nat holds b2 . (m,n) = m lcm n ) holds
b1 = b2
end;
Lm1:
for a being Element of Nat_Lattice holds
( 0_NN "/\" a = 0_NN & a "/\" 0_NN = 0_NN )
by NEWTON:51;
theorem
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
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) )
definition
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
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;
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, NEWTON:54;