let p be G_RAT; :: thesis: ex x, y being G_INTEG st
( y <> 0 & p = x / y )
reconsider Rp = Re p, Ip = Im p as Rational ;
consider m1, n1 being Integer such that
A1: ( n1 > 0 & Rp = m1 / n1 ) by RAT_1:2;
consider m2, n2 being Integer such that
A2: ( n2 > 0 & Ip = m2 / n2 ) by RAT_1:2;
set z = n1 * n2;
( Re (n1 * n2) = n1 * n2 & Im (n1 * n2) = 0 ) by COMPLEX1:def 1, COMPLEX1:def 2;
then A3: ( Re ((n1 * n2) * p) = ((n1 * n2) * Rp) - (0 * Ip) & Im ((n1 * n2) * p) = ((n1 * n2) * Ip) + (Rp * 0) ) by COMPLEX1:9;
A4: Re ((n1 * n2) * p) = ((n1 / n1) * m1) * n2 by A1, A3
.= (1 * m1) * n2 by XCMPLX_1:60, A1
.= m1 * n2 ;
A5: Im ((n1 * n2) * p) = ((n2 / n2) * m2) * n1 by A2, A3
.= (1 * m2) * n1 by XCMPLX_1:60, A2
.= m2 * n1 ;
reconsider x = (n1 * n2) * p as G_INTEG by A4, A5, Lm1;
take x ; :: thesis: ex y being G_INTEG st
( y <> 0 & p = x / y )
take n1 * n2 ; :: thesis: ( n1 * n2 <> 0 & p = x / (n1 * n2) )
x / (n1 * n2) = ((n1 * n2) / (n1 * n2)) * p
.= 1 * p by XCMPLX_1:60, A1, A2
.= p ;
hence ( n1 * n2 <> 0 & p = x / (n1 * n2) ) by A1, A2; :: thesis: verum