let r, r1, r2, r3 be Real; :: thesis: ( r <> 0 & r1 <> 0 implies ( r3 / r1 = r2 / r iff r3 * r = r2 * r1 ) )
assume that
A1: r <> 0 and
A2: r1 <> 0 ; :: thesis: ( r3 / r1 = r2 / r iff r3 * r = r2 * r1 )
thus ( r3 / r1 = r2 / r implies r3 * r = r2 * r1 ) :: thesis: ( r3 * r = r2 * r1 implies r3 / r1 = r2 / r )

proof

assume A3: r3 / r1 = r2 / r ; :: thesis: r3 * r = r2 * r1
r3 * r = ((r3 / r1) * r1) * r by A2, XCMPLX_1:87
.= ((r2 / r) * r) * r1 by A3
.= r2 * r1 by A1, XCMPLX_1:87 ;
hence r3 * r = r2 * r1 ; :: thesis: verum

end;

assume A4: r3 * r = r2 * r1 ; :: thesis: r3 / r1 = r2 / r
r3 / r1 = (r3 * 1) / r1
.= (r3 * (r * (r "))) / r1 by A1, XCMPLX_0:def 7
.= ((r2 * r1) * (r ")) / r1 by A4, XCMPLX_1:4
.= ((r2 * (r ")) * r1) / r1
.= ((r2 / r) * r1) / r1 by XCMPLX_0:def 9
.= ((r2 / r) * r1) * (r1 ") by XCMPLX_0:def 9
.= (r2 / r) * (r1 * (r1 "))
.= (r2 / r) * 1 by A2, XCMPLX_0:def 7
.= r2 / r ;
hence r3 / r1 = r2 / r ; :: thesis: verum