let m, n be non zero Nat; :: thesis: ( m,n are_coprime implies card (NatDivisors (m * n)) = (card (NatDivisors m)) * (card (NatDivisors n)) )
assume m,n are_coprime ; :: thesis: card (NatDivisors (m * n)) = (card (NatDivisors m)) * (card (NatDivisors n))
then A1: #divs (m * n) = (#divs m) * (#divs n) by DivsMulti;
( #divs (m * n) = card (NatDivisors (m * n)) & #divs m = card (NatDivisors m) & #divs n = card (NatDivisors n) ) by ThDivs;
hence card (NatDivisors (m * n)) = (card (NatDivisors m)) * (card (NatDivisors n)) by A1; :: thesis: verum