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