let x be real number ; :: thesis: ( cos x <> 0 implies tan (2 * x) = (2 * (tan x)) / (1 - ((tan x) ^2 )) )
assume A1: cos x <> 0 ; :: thesis: tan (2 * x) = (2 * (tan x)) / (1 - ((tan x) ^2 ))
tan (2 * x) = tan (x + x)
.= ((tan x) + (tan x)) / (1 - ((tan x) * (tan x))) by A1, SIN_COS4:11
.= (2 * (tan x)) / (1 - ((tan x) * (tan x))) ;
hence tan (2 * x) = (2 * (tan x)) / (1 - ((tan x) ^2 )) ; :: thesis: verum