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