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;