let x be set ; for l being Element of NAT
for m being Integer st x = m / l holds
x in RAT
let l be Element of NAT ; for m being Integer st x = m / l holds
x in RAT
let m be Integer; ( x = m / l implies x in RAT )
A1:
m is Element of INT
by INT_1:def 2;
assume A2:
x = m / l
; x in RAT
then A3:
not x in {[0,0]}
by NUMBERS:def 1, XBOOLE_0:def 5;
per cases
( l = 0 or ex k being Element of NAT st m = k or ( l <> 0 & ( for k being Element of NAT holds m <> k ) ) )
;
suppose that A5:
l <> 0
and A6:
for
k being
Element of
NAT holds
m <> k
;
x in RAT consider k being
Element of
NAT such that A7:
m = - k
by A1, A6, INT_1:def 1;
A8:
k / l = quotient (
k,
l)
by Lm2;
then
k / l in RAT+
;
then reconsider x9 =
k / l as
Element of
REAL+ by ARYTM_2:1;
A9:
0 in {0}
by TARSKI:def 1;
A10:
x = - (k / l)
by A2, A7;
m <> 0
by A6;
then A11:
x9 <> 0
by A2, A5, A10, XCMPLX_1:50;
x =
09 - x9
by A10, Lm3
.=
[0,x9]
by A11, ARYTM_1:19
;
then
x in [:{0},RAT+:]
by A8, A9, ZFMISC_1:87;
then
x in RAT+ \/ [:{0},RAT+:]
by XBOOLE_0:def 3;
hence
x in RAT
by A3, NUMBERS:def 3, XBOOLE_0:def 5;
verum end;