let a be Nat; :: thesis: for k being Integer
for q being Rational st q = k / a & a <> 0 & k,a are_coprime holds
( k = numerator q & a = denominator q )
let k be Integer; :: thesis: for q being Rational st q = k / a & a <> 0 & k,a are_coprime holds
( k = numerator q & a = denominator q )
let q be Rational; :: thesis: ( q = k / a & a <> 0 & k,a are_coprime implies ( k = numerator q & a = denominator q ) )
assume that
A1: ( q = k / a & a <> 0 ) and
A2: k,a are_coprime ; :: thesis: ( k = numerator q & a = denominator q )
consider b being Nat such that
A3: ( k = (numerator q) * b & a = (denominator q) * b ) by A1, RAT_1:27;
numerator q, denominator q are_coprime by Th22;
then k gcd a = |.b.| by A3, INT_2:24;
then 1 = |.b.| by A2, INT_2:def 3
.= b by ABSVALUE:def 1 ;
hence ( k = numerator q & a = denominator q ) by A3; :: thesis: verum