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 )

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

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 A4:
r3 * r = r2 * r1
; :: thesis: r3 / r1 = r2 / r
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;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

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