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
per cases ( x in RAT+ or x in [:{0},RAT+:] ) by A1, NUMBERS:def 3, XBOOLE_0:def 3;
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;
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;
end;