let a, b be Nat; :: thesis: for u being Integer holds (a + (u * b)) gcd b = a gcd b
let u be Integer; :: thesis: (a + (u * b)) gcd b = a gcd b
b divides u * b ;
then A0: b gcd (u * b) = |.b.| by Th3
.= b ;
per cases ( a <> 0 or a = 0 ) ;
suppose a <> 0 ; :: thesis: (a + (u * b)) gcd b = a gcd b
hence (a + (u * b)) gcd b = a gcd b by EULER_1:16; :: thesis: verum
end;
suppose a = 0 ; :: thesis: (a + (u * b)) gcd b = a gcd b
hence (a + (u * b)) gcd b = a gcd b by A0; :: thesis: verum
end;
end;