let p be Rational; :: thesis: for l being Nat holds
( not 1 < l or for m being Integer
for k being Nat holds
( not numerator p = m * l or not denominator p = k * l ) )
assume ex l being Nat st
( 1 < l & ex m being Integer ex k being Nat st
( numerator p = m * l & denominator p = k * l ) ) ; :: thesis: contradiction
then consider l being Nat such that
A1: 1 < l and
A2: ex m being Integer ex k being Nat st
( numerator p = m * l & denominator p = k * l ) ;
consider m being Integer, k being 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, Th12
.= (m / k) * (l / l) by XCMPLX_1:76
.= (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:68;
hence contradiction by A4, A6, A5, Def3; :: thesis: verum