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