let n, m, k be non zero Nat; ( k = n lcm m implies support (ppf k) = (support (ppf n)) \/ (support (ppf m)) )
assume A1:
k = n lcm m
; support (ppf k) = (support (ppf n)) \/ (support (ppf m))
A2:
support (ppf n) = support (pfexp n)
by NAT_3:def 9;
A3:
(support (pfexp n)) \/ (support (pfexp m)) c= support (max ((pfexp n),(pfexp m)))
A9:
support (ppf m) = support (pfexp m)
by NAT_3:def 9;
A10: support (ppf k) =
support (pfexp k)
by NAT_3:def 9
.=
support (max ((pfexp n),(pfexp m)))
by A1, NAT_3:54
;
then
support (ppf k) c= (support (ppf n)) \/ (support (ppf m))
by A2, A9, NAT_3:18;
hence
support (ppf k) = (support (ppf n)) \/ (support (ppf m))
by A10, A2, A9, A3, XBOOLE_0:def 10; verum