let n, m, k be non empty natural number ; :: thesis: ( k = n lcm m implies support (ppf k) = (support (ppf n)) \/ (support (ppf m)) )
assume A1: k = n lcm m ; :: thesis: support (ppf k) = (support (ppf n)) \/ (support (ppf m))
A2: support (ppf k) = support (pfexp k) by NAT_3:def 9
.= support (max (pfexp n),(pfexp m)) by A1, NAT_3:54 ;
A3: support (ppf n) = support (pfexp n) by NAT_3:def 9;
A4: support (ppf m) = support (pfexp m) by NAT_3:def 9;
A5: support (ppf k) c= (support (ppf n)) \/ (support (ppf m)) by A2, A3, A4, NAT_3:18;
(support (pfexp n)) \/ (support (pfexp m)) c= support (max (pfexp n),(pfexp m))

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in (support (pfexp n)) \/ (support (pfexp m)) or x in support (max (pfexp n),(pfexp m)) )
assume A6: x in (support (pfexp n)) \/ (support (pfexp m)) ; :: thesis: x in support (max (pfexp n),(pfexp m))

per cases ( x in support (pfexp n) or x in support (pfexp m) ) by A6, XBOOLE_0:def 3;

suppose x in support (pfexp n) ; :: thesis: x in support (max (pfexp n),(pfexp m))

then (pfexp n) . x <> 0 by POLYNOM1:def 7;
then A7: 0 < (pfexp n) . x ;
(pfexp n) . x <= (max (pfexp n),(pfexp m)) . x

proof

per cases ( (pfexp n) . x <= (pfexp m) . x or (pfexp n) . x > (pfexp m) . x ) ;

suppose (pfexp n) . x <= (pfexp m) . x ; :: thesis: (pfexp n) . x <= (max (pfexp n),(pfexp m)) . x

hence (pfexp n) . x <= (max (pfexp n),(pfexp m)) . x by NAT_3:def 4; :: thesis: verum

end;

suppose (pfexp n) . x > (pfexp m) . x ; :: thesis: (pfexp n) . x <= (max (pfexp n),(pfexp m)) . x

hence (pfexp n) . x <= (max (pfexp n),(pfexp m)) . x by NAT_3:def 4; :: thesis: verum

end;

end;

end;

hence x in support (max (pfexp n),(pfexp m)) by A7, POLYNOM1:def 7; :: thesis: verum

end;

suppose x in support (pfexp m) ; :: thesis: x in support (max (pfexp n),(pfexp m))

then (pfexp m) . x <> 0 by POLYNOM1:def 7;
then A8: 0 < (pfexp m) . x ;
(pfexp m) . x <= (max (pfexp n),(pfexp m)) . x

proof

per cases ( (pfexp n) . x <= (pfexp m) . x or (pfexp n) . x > (pfexp m) . x ) ;

suppose (pfexp n) . x <= (pfexp m) . x ; :: thesis: (pfexp m) . x <= (max (pfexp n),(pfexp m)) . x

hence (pfexp m) . x <= (max (pfexp n),(pfexp m)) . x by NAT_3:def 4; :: thesis: verum

end;

suppose (pfexp n) . x > (pfexp m) . x ; :: thesis: (pfexp m) . x <= (max (pfexp n),(pfexp m)) . x

hence (pfexp m) . x <= (max (pfexp n),(pfexp m)) . x by NAT_3:def 4; :: thesis: verum

end;

end;

end;

hence x in support (max (pfexp n),(pfexp m)) by A8, POLYNOM1:def 7; :: thesis: verum

end;

end;

end;

hence support (ppf k) = (support (ppf n)) \/ (support (ppf m)) by A2, A3, A4, A5, XBOOLE_0:def 10; :: thesis: verum