set L = NatPlus_Lattice ;
set C = NatDivisors n;
set LJ = the L_join of NatPlus_Lattice || (NatDivisors n);
set LM = the L_meet of NatPlus_Lattice || (NatDivisors n);
A0: NatDivisors n c= the carrier of NatPlus_Lattice by NAT_LAT:def 6, NAT_LAT:def 10;
dom the L_join of NatPlus_Lattice = [: the carrier of NatPlus_Lattice, the carrier of NatPlus_Lattice:] by FUNCT_2:def 1;
then A1: dom ( the L_join of NatPlus_Lattice || (NatDivisors n)) = [:(NatDivisors n),(NatDivisors n):] by RELAT_1:62, A0, ZFMISC_1:96;
rng ( the L_join of NatPlus_Lattice || (NatDivisors n)) c= NatDivisors n
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng ( the L_join of NatPlus_Lattice || (NatDivisors n)) or y in NatDivisors n )
assume y in rng ( the L_join of NatPlus_Lattice || (NatDivisors n)) ; :: thesis: y in NatDivisors n
then consider x being object such that
B1: ( x in dom ( the L_join of NatPlus_Lattice || (NatDivisors n)) & y = ( the L_join of NatPlus_Lattice || (NatDivisors n)) . x ) by FUNCT_1:def 3;
consider x1, x2 being object such that
B2: ( x1 in NatDivisors n & x2 in NatDivisors n & x = [x1,x2] ) by ZFMISC_1:def 2, A1, B1;
reconsider xx1 = x1, xx2 = x2 as Nat by B2;
reconsider xx1 = xx1, xx2 = xx2 as NatPlus by B2, NAT_LAT:def 6;
y = lcmlatplus . (x1,x2) by NAT_LAT:def 10, B1, A1, B2, FUNCT_1:49;
then y = xx1 lcm xx2 by NAT_LAT:def 9;
hence y in NatDivisors n by LCMDiv, B2; :: thesis: verum
end;
then reconsider LJ = the L_join of NatPlus_Lattice || (NatDivisors n) as BinOp of (NatDivisors n) by FUNCT_2:2, A1;
dom the L_meet of NatPlus_Lattice = [: the carrier of NatPlus_Lattice, the carrier of NatPlus_Lattice:] by FUNCT_2:def 1;
then A1: dom ( the L_meet of NatPlus_Lattice || (NatDivisors n)) = [:(NatDivisors n),(NatDivisors n):] by RELAT_1:62, A0, ZFMISC_1:96;
rng ( the L_meet of NatPlus_Lattice || (NatDivisors n)) c= NatDivisors n
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng ( the L_meet of NatPlus_Lattice || (NatDivisors n)) or y in NatDivisors n )
assume y in rng ( the L_meet of NatPlus_Lattice || (NatDivisors n)) ; :: thesis: y in NatDivisors n
then consider x being object such that
B1: ( x in dom ( the L_meet of NatPlus_Lattice || (NatDivisors n)) & y = ( the L_meet of NatPlus_Lattice || (NatDivisors n)) . x ) by FUNCT_1:def 3;
consider x1, x2 being object such that
B2: ( x1 in NatDivisors n & x2 in NatDivisors n & x = [x1,x2] ) by ZFMISC_1:def 2, A1, B1;
reconsider xx1 = x1, xx2 = x2 as Nat by B2;
reconsider xx1 = xx1, xx2 = xx2 as NatPlus by B2, NAT_LAT:def 6;
y = hcflatplus . (x1,x2) by NAT_LAT:def 10, B1, A1, B2, FUNCT_1:49;
then y = xx1 gcd xx2 by NAT_LAT:def 8;
hence y in NatDivisors n by GCDDiv, B2; :: thesis: verum
end;
then reconsider LM = the L_meet of NatPlus_Lattice || (NatDivisors n) as BinOp of (NatDivisors n) by FUNCT_2:2, A1;
set DD = LattStr(# (NatDivisors n),LJ,LM #);
reconsider DD = LattStr(# (NatDivisors n),LJ,LM #) as non empty LattStr ;
SS: for a, b being Element of DD
for aa, bb being Nat st a = aa & b = bb holds
LJ . (a,b) = aa lcm bb
proof
let a, b be Element of DD; :: thesis: for aa, bb being Nat st a = aa & b = bb holds
LJ . (a,b) = aa lcm bb
let aa, bb be Nat; :: thesis: ( a = aa & b = bb implies LJ . (a,b) = aa lcm bb )
assume Z1: ( a = aa & b = bb ) ; :: thesis: LJ . (a,b) = aa lcm bb
reconsider a1 = a, b1 = b as NatPlus by NAT_LAT:def 6;
thus LJ . (a,b) = lcmlatplus . (a,b) by NAT_LAT:def 10, ZFMISC_1:87, FUNCT_1:49
.= a1 lcm b1 by NAT_LAT:def 9
.= aa lcm bb by Z1 ; :: thesis: verum
end;
ss: for a, b being Element of DD
for aa, bb being Nat st a = aa & b = bb holds
LM . (a,b) = aa gcd bb
proof
let a, b be Element of DD; :: thesis: for aa, bb being Nat st a = aa & b = bb holds
LM . (a,b) = aa gcd bb
let aa, bb be Nat; :: thesis: ( a = aa & b = bb implies LM . (a,b) = aa gcd bb )
assume Z1: ( a = aa & b = bb ) ; :: thesis: LM . (a,b) = aa gcd bb
reconsider a1 = a, b1 = b as NatPlus by NAT_LAT:def 6;
thus LM . (a,b) = hcflatplus . (a,b) by NAT_LAT:def 10, ZFMISC_1:87, FUNCT_1:49
.= a1 gcd b1 by NAT_LAT:def 8
.= aa gcd bb by Z1 ; :: thesis: verum
end;
set LL = the L_join of NatPlus_Lattice;
d3: LJ is commutative by CutComm, DivInPlus, NAT_LAT:def 10;
set ll = the L_meet of NatPlus_Lattice;
d2: LM is commutative by CutComm, NAT_LAT:def 10, DivInPlus;
d4: LM is associative by CutAssoc, NAT_LAT:def 10, DivInPlus;
d5: LJ is associative by CutAssoc, NAT_LAT:def 10, DivInPlus;
for a, b being Element of DD holds a "/\" (a "\/" b) = a
proof
let a, b be Element of DD; :: thesis: a "/\" (a "\/" b) = a
reconsider aa = a, bb = b as Nat ;
[a,b] in [:(NatDivisors n),(NatDivisors n):] by ZFMISC_1:87;
then reconsider jj = LJ . (a,b) as Element of DD by FUNCT_2:5;
reconsider lj = jj as Nat ;
thus a "/\" (a "\/" b) = aa gcd lj by ss
.= aa gcd (aa lcm bb) by SS
.= a by NEWTON:54 ; :: thesis: verum
end;
then D1: DD is join-absorbing ;
for a, b being Element of DD holds (a "/\" b) "\/" b = b
proof
let a, b be Element of DD; :: thesis: (a "/\" b) "\/" b = b
reconsider aa = a, bb = b as Nat ;
[a,b] in [:(NatDivisors n),(NatDivisors n):] by ZFMISC_1:87;
then reconsider jj = LM . (a,b) as Element of DD by FUNCT_2:5;
reconsider lj = jj as Nat ;
thus (a "/\" b) "\/" b = lj lcm bb by SS
.= (aa gcd bb) lcm bb by ss
.= b by NEWTON:53 ; :: thesis: verum
end;
then DD is meet-absorbing ;
then DD is SubLattice of NatPlus_Lattice by DivInPlus, NAT_LAT:def 10, NAT_LAT:def 12, D1, d2, d3, d4, d5;
hence ex b1 being strict SubLattice of NatPlus_Lattice st the carrier of b1 = NatDivisors n ; :: thesis: verum