let r, s, t, u be Real; :: thesis: ( s <> 0 & t <> 0 & r ^2 = ((s ^2) + (t ^2)) - (((2 * s) * t) * u) implies u = (((r ^2) - (s ^2)) - (t ^2)) / (- ((2 * s) * t)) )
assume that
A1: s <> 0 and
A2: t <> 0 and
A3: r ^2 = ((s ^2) + (t ^2)) - (((2 * s) * t) * u) ; :: thesis: u = (((r ^2) - (s ^2)) - (t ^2)) / (- ((2 * s) * t))
((r ^2) - (s ^2)) - (t ^2) = u * (- ((2 * s) * t)) by A3;
hence u = (((r ^2) - (s ^2)) - (t ^2)) / (- ((2 * s) * t)) by A1, A2, XCMPLX_1:89; :: thesis: verum