let m, n be non zero Nat; :: thesis: ( m,n are_coprime implies number_of_divisors (m * n) = (number_of_divisors m) * (number_of_divisors n) )
assume W1: m,n are_coprime ; :: thesis: number_of_divisors (m * n) = (number_of_divisors m) * (number_of_divisors n)
then AA: Bnumber_of_divisors (m * n) = (Bnumber_of_divisors m) + (Bnumber_of_divisors n) by Th50;
( support (Bnumber_of_divisors m) = support (pfexp m) & support (Bnumber_of_divisors n) = support (pfexp n) ) by BDef;
then KK: support (Bnumber_of_divisors m) misses support (Bnumber_of_divisors n) by W1, NAT_3:44;
hence number_of_divisors (m * n) = (number_of_divisors m) * (number_of_divisors n) by AA, NAT_3:19; :: thesis: verum