let x be Real; :: 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:7
.= (2 * (tan x)) / (1 - ((tan x) * (tan x))) ;
hence tan (2 * x) = (2 * (tan x)) / (1 - ((tan x) ^2)) ; :: thesis: verum