let k be Nat; :: thesis: for m being Integer
for p being Rational st k <> 0 & p = m / k holds
ex w being Nat st
( m = (numerator p) * w & k = (denominator p) * w )
let m be Integer; :: thesis: for p being Rational st k <> 0 & p = m / k holds
ex w being Nat st
( m = (numerator p) * w & k = (denominator p) * w )
let p be Rational; :: thesis: ( k <> 0 & p = m / k implies ex w being Nat st
( m = (numerator p) * w & k = (denominator p) * w ) )
assume that
A1: k <> 0 and
A2: p = m / k ; :: thesis: ex w being Nat st
( m = (numerator p) * w & k = (denominator p) * w )
A3: p * k = m by A1, A2, XCMPLX_1:87;
defpred S₁[ Nat] means $1 * (denominator p) <= k;
A5: for l being Nat st S₁[l] holds
l <= k

proof

0 + 1 <= denominator p by NAT_1:13;
then A6: k * 1 <= k * (denominator p) by NAT_1:4;
let l be Nat; :: thesis: ( S₁[l] implies l <= k )
assume A7: l * (denominator p) <= k ; :: thesis: l <= k
assume not l <= k ; :: thesis: contradiction
then k * (denominator p) < l * (denominator p) by XREAL_1:68;
hence contradiction by A7, A6, XXREAL_0:2; :: thesis: verum

end;

A8: 1 * (denominator p) <= k by A1, A2, Def3;
then A9: ex l1 being Nat st S₁[l1] ;
consider l being Nat such that
A10: S₁[l] and
A11: for l1 being Nat st S₁[l1] holds
l1 <= l from NAT_1:sch 6(A5, A9);
reconsider l = l as Element of NAT by ORDINAL1:def 12;
take l ; :: thesis: ( m = (numerator p) * l & k = (denominator p) * l )
A12: 0 <> l by A8, A11;
then A13: l * (denominator p) <> 0 by XCMPLX_1:6;

A14: now :: thesis: not l * (denominator p) < k

assume A15: l * (denominator p) < k ; :: thesis: contradiction
then 0 + (l * (denominator p)) < k ;
then 0 <= k - (l * (denominator p)) by XREAL_1:20;
then reconsider x = k - (l * (denominator p)) as Element of NAT by INT_1:3;
A16: 0 <> x by A15;
m / k = ((numerator p) * l) / (l * (denominator p)) by A2, A12, Th23;
then p = (m - ((numerator p) * l)) / x by A2, A13, A15, XCMPLX_1:123;
then denominator p <= k - (l * (denominator p)) by A16, Def3;
then (l * (denominator p)) + (1 * (denominator p)) <= k by XREAL_1:19;
then (l + 1) * (denominator p) <= k ;
then l + 1 <= l by A11;
hence contradiction by NAT_1:13; :: thesis: verum

end;

then k = (denominator p) * l by A10, XXREAL_0:1;
hence m = ((numerator p) / (denominator p)) * ((denominator p) * l) by A3, Th12
.= (((numerator p) / (denominator p)) * (denominator p)) * l
.= (numerator p) * l by XCMPLX_1:87 ;
:: thesis: k = (denominator p) * l
thus k = (denominator p) * l by A10, A14, XXREAL_0:1; :: thesis: verum