let k be Element of NAT ; :: thesis: for m being Integer
for p being Rational st p = m / k & k <> 0 & ( for l being Element of NAT holds
( not 1 < l or for m1 being Integer
for k1 being Element of NAT holds
( not m = m1 * l or not k = k1 * l ) ) ) holds
( k = denominator p & m = numerator p )
let m be Integer; :: thesis: for p being Rational st p = m / k & k <> 0 & ( for l being Element of NAT holds
( not 1 < l or for m1 being Integer
for k1 being Element of NAT holds
( not m = m1 * l or not k = k1 * l ) ) ) holds
( k = denominator p & m = numerator p )
let p be Rational; :: thesis: ( p = m / k & k <> 0 & ( for l being Element of NAT holds
( not 1 < l or for m1 being Integer
for k1 being Element of NAT holds
( not m = m1 * l or not k = k1 * l ) ) ) implies ( k = denominator p & m = numerator p ) )
assume A1: ( p = m / k & k <> 0 & ( for l being Element of NAT holds
( not 1 < l or for m1 being Integer
for k1 being Element of NAT holds
( not m = m1 * l or not k = k1 * l ) ) ) ) ; :: thesis: ( k = denominator p & m = numerator p )
then consider l being Element of NAT such that
A2: ( m = (numerator p) * l & k = (denominator p) * l ) by Th60;
A3: l <= 1 by A1, A2;
l <> 0 by A1, A2;
then 0 < l ;
then 0 + 1 <= l by NAT_1:13;
then A4: l = 1 by A3, XXREAL_0:1;
hence k = denominator p by A2; :: thesis: m = numerator p
thus m = numerator p by A2, A4; :: thesis: verum