let x be object ; :: thesis: for w being Nat
for m being Integer st x = m / w holds
x in RAT

let w be Nat; :: thesis: for m being Integer st x = m / w holds
x in RAT

let m be Integer; :: thesis: ( x = m / w implies x in RAT )
reconsider Z9 = 0 as Element of REAL+ by ARYTM_2:2;
A1: m is Element of INT by INT_1:def 2;
assume A2: x = m / w ; :: thesis:
then x in REAL by XREAL_0:def 1;
then A3: not x in by ;
reconsider w = w as Element of NAT by ORDINAL1:def 12;
per cases ( w = 0 or ex k being Nat st m = k or ( w <> 0 & ( for k being Nat holds m <> k ) ) ) ;
suppose w = 0 ; :: thesis:
then x = m * () by A2
.= 0 ;
then x in RAT+ \/ by ;
hence x in RAT by ; :: thesis: verum
end;
suppose ex k being Nat st m = k ; :: thesis:
then consider k being Nat such that
A4: m = k ;
x = quotient (k,w) by A2, A4, Lm2;
then x in RAT+ \/ by XBOOLE_0:def 3;
hence x in RAT by ; :: thesis: verum
end;
suppose that A5: w <> 0 and
A6: for k being Nat holds m <> k ; :: thesis:
consider k being Nat such that
A7: m = - k by ;
A8: k / w = quotient (k,w) by Lm2;
then k / w in RAT+ ;
then reconsider x9 = k / w as Element of REAL+ by ARYTM_2:1;
A9: 0 in by TARSKI:def 1;
A10: x = - (k / w) by A2, A7;
m <> 0 by A6;
then A11: x9 <> 0 by ;
x = Z9 - x9 by
.= [0,x9] by ;
then x in by ;
then x in RAT+ \/ by XBOOLE_0:def 3;
hence x in RAT by ; :: thesis: verum
end;
end;