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 = () * w & k = () * w )

let m be Integer; :: thesis: for p being Rational st k <> 0 & p = m / k holds
ex w being Nat st
( m = () * w & k = () * w )

let p be Rational; :: thesis: ( k <> 0 & p = m / k implies ex w being Nat st
( m = () * w & k = () * w ) )

assume that
A1: k <> 0 and
A2: p = m / k ; :: thesis: ex w being Nat st
( m = () * w & k = () * w )

A3: p * k = m by ;
defpred S1[ Nat] means \$1 * () <= k;
A5: for l being Nat st S1[l] holds
l <= k
proof
0 + 1 <= denominator p by NAT_1:13;
then A6: k * 1 <= k * () by NAT_1:4;
let l be Nat; :: thesis: ( S1[l] implies l <= k )
assume A7: l * () <= k ; :: thesis: l <= k
assume not l <= k ; :: thesis: contradiction
then k * () < l * () by XREAL_1:68;
hence contradiction by A7, A6, XXREAL_0:2; :: thesis: verum
end;
A8: 1 * () <= k by A1, A2, Def3;
then A9: ex l1 being Nat st S1[l1] ;
consider l being Nat such that
A10: S1[l] and
A11: for l1 being Nat st S1[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 = () * l & k = () * l )
A12: 0 <> l by ;
then A13: l * () <> 0 by XCMPLX_1:6;
A14: now :: thesis: not l * () < k
assume A15: l * () < k ; :: thesis: contradiction
then 0 + (l * ()) < k ;
then 0 <= k - (l * ()) by XREAL_1:20;
then reconsider x = k - (l * ()) as Element of NAT by INT_1:3;
A16: 0 <> x by A15;
m / k = (() * l) / (l * ()) by ;
then p = (m - (() * l)) / x by ;
then denominator p <= k - (l * ()) by ;
then (l * ()) + (1 * ()) <= k by XREAL_1:19;
then (l + 1) * () <= k ;
then l + 1 <= l by A11;
hence contradiction by NAT_1:13; :: thesis: verum
end;
then k = () * l by ;
hence m = (() / ()) * (() * l) by
.= ((() / ()) * ()) * l
.= () * l by XCMPLX_1:87 ;
:: thesis: k = () * l
thus k = () * l by ; :: thesis: verum