let x be Real; ( cos x <> 0 implies sin (2 * x) = (2 * (tan x)) / (1 + ((tan x) ^2)) )
assume A1:
cos x <> 0
; sin (2 * x) = (2 * (tan x)) / (1 + ((tan x) ^2))
then A2:
(cos x) ^2 <> 0
by SQUARE_1:12;
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:74
.=
((2 * ((cos x) ^2)) * (sin x)) / (cos x)
.=
((2 * ((cos x) ^2)) * (tan x)) / 1
by XCMPLX_1:74
.=
((2 * (tan x)) * ((cos x) ^2)) / (((sin x) ^2) + ((cos x) ^2))
by SIN_COS:29
.=
(2 * (tan x)) / ((((sin x) ^2) + ((cos x) ^2)) / ((cos x) ^2))
by XCMPLX_1:77
.=
(2 * (tan x)) / ((((sin x) ^2) / ((cos x) ^2)) + (((cos x) ^2) / ((cos x) ^2)))
by XCMPLX_1:62
.=
(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:76
;
hence
sin (2 * x) = (2 * (tan x)) / (1 + ((tan x) ^2))
; verum