let x be real number ; :: thesis: ( cos x <> 0 implies cos (2 * x) = (1 - ((tan x) ^2)) / (1 + ((tan x) ^2)) )
assume cos x <> 0 ; :: thesis: cos (2 * x) = (1 - ((tan x) ^2)) / (1 + ((tan x) ^2))
then A1: (cos x) ^2 <> 0 by SQUARE_1:74;
cos (2 * x) = (((cos x) ^2) - ((sin x) ^2)) * 1 by Th7
.= (((cos x) ^2) - ((sin x) ^2)) * (((cos x) ^2) / ((cos x) ^2)) by A1, XCMPLX_1:60
.= ((((cos x) ^2) - ((sin x) ^2)) / ((cos x) ^2)) * ((cos x) ^2) by XCMPLX_1:76
.= ((((cos x) ^2) / ((cos x) ^2)) - (((sin x) ^2) / ((cos x) ^2))) * ((cos x) ^2) by XCMPLX_1:121
.= (1 - (((sin x) ^2) / ((cos x) ^2))) * ((cos x) ^2) by A1, XCMPLX_1:60
.= ((1 - ((tan x) ^2)) * ((cos x) ^2)) / 1 by XCMPLX_1:77
.= ((1 - ((tan x) ^2)) * ((cos x) ^2)) / (((cos x) ^2) + ((sin x) ^2)) by SIN_COS:32
.= (1 - ((tan x) ^2)) / ((((cos x) ^2) + ((sin x) ^2)) / ((cos x) ^2)) by XCMPLX_1:78
.= (1 - ((tan x) ^2)) / ((((cos x) ^2) / ((cos x) ^2)) + (((sin x) ^2) / ((cos x) ^2))) by XCMPLX_1:63
.= (1 - ((tan x) ^2)) / (1 + (((sin x) ^2) / ((cos x) ^2))) by A1, XCMPLX_1:60
.= (1 - ((tan x) ^2)) / (1 + ((tan x) ^2)) by XCMPLX_1:77 ;
hence cos (2 * x) = (1 - ((tan x) ^2)) / (1 + ((tan x) ^2)) ; :: thesis: verum