let a, b, c, d be Real; :: thesis: ( a <> 0 & b <> 0 & a * d = b * c implies ex e being Real st
( e = d / b & e = c / a & c = e * a & d = e * b ) )
assume that
A1: a <> 0 and
A2: b <> 0 and
A3: a * d = b * c ; :: thesis: ex e being Real st
( e = d / b & e = c / a & c = e * a & d = e * b )
A4: c = (a * d) / b by A2, A3, XCMPLX_1:89
.= (d / b) * a by XCMPLX_1:74 ;
A5: d = (b * c) / a by A1, A3, XCMPLX_1:89
.= (c / a) * b by XCMPLX_1:74 ;
d / b = ((d / b) * a) / a by A1, XCMPLX_1:89
.= (b * c) / (b * a) by A3, XCMPLX_1:83
.= (b / b) / (a / c) by XCMPLX_1:84
.= 1 / (a / c) by A2, XCMPLX_1:60
.= c / a by XCMPLX_1:57 ;
hence ex e being Real st
( e = d / b & e = c / a & c = e * a & d = e * b ) by A4, A5; :: thesis: verum