let a, b, c be Integer; :: thesis: ( a,b are_coprime implies c gcd (a * b) = (c gcd a) * (c gcd b) )
assume A1: a,b are_coprime ; :: thesis: c gcd (a * b) = (c gcd a) * (c gcd b)
reconsider k = |.a.|, l = |.b.|, m = |.c.| as Nat ;
A2: k,l are_coprime by A1, INT_2:34;
|.a.| * |.b.| = |.(a * b).| by COMPLEX1:65;
then ( c gcd (a * b) = m gcd (k * l) & c gcd a = m gcd k & c gcd b = m gcd l ) by INT_2:34;
hence c gcd (a * b) = (c gcd a) * (c gcd b) by A2, NAT517; :: thesis: verum