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