let n, m, k be non zero Nat; :: 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 n) = support (pfexp n) by NAT_3:def 9;
A3: (support (pfexp n)) \/ (support (pfexp m)) c= support (max ((pfexp n),(pfexp m)))
proof
let x be object ; :: 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 A4: 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 A4, XBOOLE_0:def 3;
suppose A5: x in support (pfexp n) ; :: thesis: x in support (max ((pfexp n),(pfexp m)))
A6: (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;
(pfexp n) . x <> 0 by A5, PRE_POLY:def 7;
then 0 < (pfexp n) . x ;
hence x in support (max ((pfexp n),(pfexp m))) by A6, PRE_POLY:def 7; :: thesis: verum
end;
suppose A7: x in support (pfexp m) ; :: thesis: x in support (max ((pfexp n),(pfexp m)))
A8: (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;
(pfexp m) . x <> 0 by A7, PRE_POLY:def 7;
then 0 < (pfexp m) . x ;
hence x in support (max ((pfexp n),(pfexp m))) by A8, PRE_POLY:def 7; :: thesis: verum
end;
end;
end;
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; :: thesis: verum