let a be Nat; :: thesis: for k being Integer
for q being Rational st q <> 0 & q = k / a & a <> 0 & k,a are_relative_prime holds
( k = numerator q & a = denominator q )
let k be Integer; :: thesis: for q being Rational st q <> 0 & q = k / a & a <> 0 & k,a are_relative_prime holds
( k = numerator q & a = denominator q )
let q be Rational; :: thesis: ( q <> 0 & q = k / a & a <> 0 & k,a are_relative_prime implies ( k = numerator q & a = denominator q ) )
X: a in NAT by ORDINAL1:def 13;
assume A1: ( q <> 0 & q = k / a & a <> 0 & k,a are_relative_prime ) ; :: thesis: ( k = numerator q & a = denominator q )
then consider b being Element of NAT such that
A2: ( k = (numerator q) * b & a = (denominator q) * b ) by X, RAT_1:60;
numerator q, denominator q are_relative_prime by Th29;
then k gcd a = abs b by A2, INT_2:39;
then 1 = abs b by A1, INT_2:def 4
.= b by ABSVALUE:def 1 ;
hence ( k = numerator q & a = denominator q ) by A2; :: thesis: verum