let p be Rational; :: thesis: for l being Element of NAT holds
( not 1 < l or for m being Integer
for k being Element of NAT holds
( not numerator p = m * l or not denominator p = k * l ) )
assume ex l being Element of NAT st
( 1 < l & ex m being Integer ex k being Element of NAT st
( numerator p = m * l & denominator p = k * l ) ) ; :: thesis: contradiction
then consider l being Element of NAT such that
A1: 1 < l and
A2: ex m being Integer ex k being Element of NAT st
( numerator p = m * l & denominator p = k * l ) ;
consider m being Integer, k being Element of NAT such that
A3: numerator p = m * l and
A4: denominator p = k * l by A2;
A5: p = (m * l) / (k * l) by A3, A4, Th37
.= (m / k) * (l / l) by XCMPLX_1:77
.= (m / k) * 1 by A1, XCMPLX_1:60
.= m / k ;
A6: k <> 0 by A4, Def3;
then k * 1 < k * l by A1, XREAL_1:70;
hence contradiction by A4, A6, A5, Def3; :: thesis: verum