let a, b be Nat; :: thesis: ( a is even & a gcd b = 1 implies a gcd (2 * b) = 2 )
assume A1: ( a is even & a gcd b = 1 ) ; :: thesis: a gcd (2 * b) = 2
a,b are_coprime by A1;
then a gcd (b * 2) = a gcd 2 by INT_6:19;
hence a gcd (2 * b) = 2 by A1, NEWTON:49; :: thesis: verum