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: x in RAT

then x in REAL by XREAL_0:def 1;

then A3: not x in {[0,0]} by NUMBERS:def 1, XBOOLE_0:def 5;

reconsider w = w as Element of NAT by ORDINAL1:def 12;

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: x in RAT

then x in REAL by XREAL_0:def 1;

then A3: not x in {[0,0]} by NUMBERS:def 1, XBOOLE_0:def 5;

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 ) ) )
;

end;

suppose
w = 0
; :: thesis: x in RAT

then x =
m * (0 ")
by A2

.= 0 ;

then x in RAT+ \/ [:{0},RAT+:] by Lm1, XBOOLE_0:def 3;

hence x in RAT by A3, NUMBERS:def 3, XBOOLE_0:def 5; :: thesis: verum

end;.= 0 ;

then x in RAT+ \/ [:{0},RAT+:] by Lm1, XBOOLE_0:def 3;

hence x in RAT by A3, NUMBERS:def 3, XBOOLE_0:def 5; :: thesis: verum

suppose
ex k being Nat st m = k
; :: thesis: x in RAT

then consider k being Nat such that

A4: m = k ;

x = quotient (k,w) by A2, A4, Lm2;

then x in RAT+ \/ [:{0},RAT+:] by XBOOLE_0:def 3;

hence x in RAT by A3, NUMBERS:def 3, XBOOLE_0:def 5; :: thesis: verum

end;A4: m = k ;

x = quotient (k,w) by A2, A4, Lm2;

then x in RAT+ \/ [:{0},RAT+:] by XBOOLE_0:def 3;

hence x in RAT by A3, NUMBERS:def 3, XBOOLE_0:def 5; :: thesis: verum

suppose that A5:
w <> 0
and

A6: for k being Nat holds m <> k ; :: thesis: x in RAT

A6: for k being Nat holds m <> k ; :: thesis: x in RAT

consider k being Nat such that

A7: m = - k by A1, A6, INT_1:def 1;

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 {0} by TARSKI:def 1;

A10: x = - (k / w) by A2, A7;

m <> 0 by A6;

then A11: x9 <> 0 by A2, A5, A10, XCMPLX_1:50;

x = Z9 - 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; :: thesis: verum

end;A7: m = - k by A1, A6, INT_1:def 1;

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 {0} by TARSKI:def 1;

A10: x = - (k / w) by A2, A7;

m <> 0 by A6;

then A11: x9 <> 0 by A2, A5, A10, XCMPLX_1:50;

x = Z9 - 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; :: thesis: verum