let n, m, k be non zero Nat; :: thesis: ( k = n gcd m implies support (ppf k) = (support (ppf n)) /\ (support (ppf m)) )
assume A1: k = n gcd 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 (ppf m) = support (pfexp m) by NAT_3:def 9;
support (ppf k) = support (pfexp k) by NAT_3:def 9
.= support (min ((pfexp n),(pfexp m))) by A1, NAT_3:53 ;
hence support (ppf k) = (support (ppf n)) /\ (support (ppf m)) by A2, A3, Th10; :: thesis: verum