let a be Integer; :: thesis: for b being non zero Integer holds a / (b gcd a),b / (a gcd b) are_coprime
let b be non zero Integer; :: thesis: a / (b gcd a),b / (a gcd b) are_coprime
consider k, l being Integer such that
A1: ( a = (a gcd b) * k & b = (a gcd b) * l & k,l are_coprime ) by INT_2:23;
( k = a / (a gcd b) & l = b / (a gcd b) ) by A1, XCMPLX_1:89;
hence a / (b gcd a),b / (a gcd b) are_coprime by A1; :: thesis: verum