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