let n be non zero square-free Nat; Divisors_Lattice n is Boolean
set L = Divisors_Lattice n;
Divisors_Lattice n is complemented
proof
for
b being
Element of
(Divisors_Lattice n) ex
a being
Element of
(Divisors_Lattice n) st
a is_a_complement_of b
proof
let b be
Element of
(Divisors_Lattice n);
ex a being Element of (Divisors_Lattice n) st a is_a_complement_of b
b in the
carrier of
(Divisors_Lattice n)
;
then aa:
b in NatDivisors n
by DivLat;
then A1:
n = b * (n div b)
by NAT_D:3, MOEBIUS1:39;
set a =
n div b;
n div b <> 0
by DivNonZero, aa, MOEBIUS1:39;
then
n div b in NatDivisors n
by MOEBIUS1:39, A1, NAT_D:def 3;
then reconsider a =
n div b as
Element of
(Divisors_Lattice n) by DivLat;
take
a
;
a is_a_complement_of b
reconsider aa =
a,
bb =
b as non
zero Element of
NAT by DivNonZero, aa, MOEBIUS1:39;
S1:
aa,
bb are_coprime
by aa, MOEBIUS1:39, DivRelPrime;
then
a lcm b = n
by A1, INT615;
hence
a is_a_complement_of b
by S1, TopBot;
verum
end;
hence
Divisors_Lattice n is
complemented
;
verum
end;
hence
Divisors_Lattice n is Boolean
; verum