let x be real number ; :: thesis: ( cos x <> 0 implies sin (2 * x) = (2 * (tan x)) / (1 + ((tan x) ^2 )) )
assume A1: cos x <> 0 ; :: thesis: sin (2 * x) = (2 * (tan x)) / (1 + ((tan x) ^2 ))
then A2: (cos x) ^2 <> 0 by SQUARE_1:74;
sin (2 * x) = ((2 * (sin x)) * (cos x)) * 1 by Th5
.= ((2 * (sin x)) * (cos x)) * ((cos x) / (cos x)) by A1, XCMPLX_1:60
.= (((2 * (sin x)) * (cos x)) * (cos x)) / (cos x) by XCMPLX_1:75
.= ((2 * ((cos x) ^2 )) * (sin x)) / (cos x)
.= ((2 * ((cos x) ^2 )) * (tan x)) / 1 by XCMPLX_1:75
.= ((2 * (tan x)) * ((cos x) ^2 )) / (((sin x) ^2 ) + ((cos x) ^2 )) by SIN_COS:32
.= (2 * (tan x)) / ((((sin x) ^2 ) + ((cos x) ^2 )) / ((cos x) ^2 )) by XCMPLX_1:78
.= (2 * (tan x)) / ((((sin x) ^2 ) / ((cos x) ^2 )) + (((cos x) ^2 ) / ((cos x) ^2 ))) by XCMPLX_1:63
.= (2 * (tan x)) / ((((sin x) ^2 ) / ((cos x) ^2 )) + 1) by A2, XCMPLX_1:60
.= (2 * (tan x)) / (((tan x) ^2 ) + 1) by XCMPLX_1:77 ;
hence sin (2 * x) = (2 * (tan x)) / (1 + ((tan x) ^2 )) ; :: thesis: verum