let m1 be Nat; :: thesis: for i1 being Integer
for q being Rational st q = i1 / m1 & m1 <> 0 & i1,m1 are_coprime holds
( i1 = numerator q & m1 = denominator q )
let i1 be Integer; :: thesis: for q being Rational st q = i1 / m1 & m1 <> 0 & i1,m1 are_coprime holds
( i1 = numerator q & m1 = denominator q )
let q be Rational; :: thesis: ( q = i1 / m1 & m1 <> 0 & i1,m1 are_coprime implies ( i1 = numerator q & m1 = denominator q ) )
assume that
A1: q = i1 / m1 and
A2: m1 <> 0 and
A3: i1,m1 are_coprime ; :: thesis: ( i1 = numerator q & m1 = denominator q )
A4: i1 gcd m1 = 1 by A3, INT_2:def 3;
ex m being Nat st
( i1 = (numerator q) * m & m1 = (denominator q) * m ) by A1, A2, RAT_1:27;
then consider m being Nat such that
A5: i1 = m * (numerator q) and
A6: m1 = m * (denominator q) ;
A7: m divides i1 by A5;
A8: m divides m1 by A6;
m divides 1 by A4, A7, A8, INT_2:def 2;
then m = 1 by WSIERP_1:15;
hence ( i1 = numerator q & m1 = denominator q ) by A6, A5; :: thesis: verum