let r be Complex; :: thesis: ( r <> 0 implies ((2 * ((7 / r) |^ 3)) + ((7 / r) * (r - (98 / (r ^2))))) - 7 = 0 )
assume A1: r <> 0 ; :: thesis: ((2 * ((7 / r) |^ 3)) + ((7 / r) * (r - (98 / (r ^2))))) - 7 = 0
A2: (7 / r) |^ 3 = ((7 / r) * (7 / r)) * (7 / r) by POLYEQ_5:2
.= 343 * (((r ") * (r ")) * (r "))
.= 343 * (((r * r) ") * (r ")) by XCMPLX_1:204
.= 343 / ((r * r) * r) by XCMPLX_1:204 ;
A3: (7 / r) * r = 7 by A1, XCMPLX_1:87;
(7 / r) * (98 / (r ^2)) = 686 * ((r ") * ((r * r) "))
.= 686 / ((r * r) * r) by XCMPLX_1:204 ;
hence ((2 * ((7 / r) |^ 3)) + ((7 / r) * (r - (98 / (r ^2))))) - 7 = 0 by A2, A3; :: thesis: verum