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