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_{1}[ Nat] means $1 * (denominator p) <= k;

A5: for l being Nat st S_{1}[l] holds

l <= k

then A9: ex l1 being Nat st S_{1}[l1]
;

consider l being Nat such that

A10: S_{1}[l]
and

A11: for l1 being Nat st S_{1}[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;

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

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

A5: for l being Nat st S

l <= k

proof

A8:
1 * (denominator p) <= k
by A1, A2, Def3;
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_{1}[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;then A6: k * 1 <= k * (denominator p) by NAT_1:4;

let l be Nat; :: thesis: ( S

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

then A9: ex l1 being Nat st S

consider l being Nat such that

A10: S

A11: for l1 being Nat st S

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

then
k = (denominator p) * l
by A10, XXREAL_0:1;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 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

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