let c be Nat; :: thesis: for a, b being Nat st a,b are_coprime holds
c gcd (a * b) = (c gcd a) * (c gcd b)
let a, b be Nat; :: 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)

per cases ( a = 0 or b = 0 or ( a <> 0 & b <> 0 ) ) ;

suppose a = 0 ; :: thesis: c gcd (a * b) = (c gcd a) * (c gcd b)

hence c gcd (a * b) = (c gcd a) * (c gcd b) by A1; :: thesis: verum

end;

suppose b = 0 ; :: thesis: c gcd (a * b) = (c gcd a) * (c gcd b)

hence c gcd (a * b) = (c gcd a) * (c gcd b) by A1; :: thesis: verum

end;

suppose ( a <> 0 & b <> 0 ) ; :: thesis: c gcd (a * b) = (c gcd a) * (c gcd b)

hence c gcd (a * b) = (c gcd a) * (c gcd b) by A1, NAT_5:17; :: thesis: verum

end;

end;