let x be object ; :: thesis: ( x in RAT implies ex m, n being Integer st x = m / n )

assume A1: x in RAT ; :: thesis: ex m, n being Integer st x = m / n

assume A1: x in RAT ; :: thesis: ex m, n being Integer st x = m / n

per cases
( x in RAT+ or x in [:{0},RAT+:] )
by A1, NUMBERS:def 3, XBOOLE_0:def 3;

end;

suppose
x in RAT+
; :: thesis: ex m, n being Integer st x = m / n

then reconsider x = x as Element of RAT+ ;

take numerator x ; :: thesis: ex n being Integer st x = (numerator x) / n

take denominator x ; :: thesis: x = (numerator x) / (denominator x)

quotient ((numerator x),(denominator x)) = x by ARYTM_3:39;

hence x = (numerator x) / (denominator x) by Lm2; :: thesis: verum

end;take numerator x ; :: thesis: ex n being Integer st x = (numerator x) / n

take denominator x ; :: thesis: x = (numerator x) / (denominator x)

quotient ((numerator x),(denominator x)) = x by ARYTM_3:39;

hence x = (numerator x) / (denominator x) by Lm2; :: thesis: verum

suppose A2:
x in [:{0},RAT+:]
; :: thesis: ex m, n being Integer st x = m / n

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

consider x1, x2 being object such that

A4: x1 in {0} and

A5: x2 in RAT+ and

A6: x = [x1,x2] by A2, ZFMISC_1:84;

reconsider x2 = x2 as Element of RAT+ by A5;

reconsider x9 = x2 as Element of REAL+ by ARYTM_2:1;

x = [0,x9] by A4, A6, TARSKI:def 1;

then A7: x2 <> 0 by A3, TARSKI:def 1;

take m = - (numerator x2); :: thesis: ex n being Integer st x = m / n

take n = denominator x2; :: thesis: x = m / n

reconsider Z9 = 0 as Element of REAL+ by ARYTM_2:2;

A8: x2 = quotient ((numerator x2),(denominator x2)) by ARYTM_3:39

.= (numerator x2) / n by Lm2 ;

x1 = 0 by A4, TARSKI:def 1;

hence x = Z9 - x9 by A6, A7, ARYTM_1:19

.= - ((numerator x2) / n) by A8, Lm3

.= m / n ;

:: thesis: verum

end;consider x1, x2 being object such that

A4: x1 in {0} and

A5: x2 in RAT+ and

A6: x = [x1,x2] by A2, ZFMISC_1:84;

reconsider x2 = x2 as Element of RAT+ by A5;

reconsider x9 = x2 as Element of REAL+ by ARYTM_2:1;

x = [0,x9] by A4, A6, TARSKI:def 1;

then A7: x2 <> 0 by A3, TARSKI:def 1;

take m = - (numerator x2); :: thesis: ex n being Integer st x = m / n

take n = denominator x2; :: thesis: x = m / n

reconsider Z9 = 0 as Element of REAL+ by ARYTM_2:2;

A8: x2 = quotient ((numerator x2),(denominator x2)) by ARYTM_3:39

.= (numerator x2) / n by Lm2 ;

x1 = 0 by A4, TARSKI:def 1;

hence x = Z9 - x9 by A6, A7, ARYTM_1:19

.= - ((numerator x2) / n) by A8, Lm3

.= m / n ;

:: thesis: verum