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

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