let x be Real; :: 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:12;
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:75
.= ((((cos x) ^2) / ((cos x) ^2)) - (((sin x) ^2) / ((cos x) ^2))) * ((cos x) ^2) by XCMPLX_1:120
.= (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:76
.= ((1 - ((tan x) ^2)) * ((cos x) ^2)) / (((cos x) ^2) + ((sin x) ^2)) by SIN_COS:29
.= (1 - ((tan x) ^2)) / ((((cos x) ^2) + ((sin x) ^2)) / ((cos x) ^2)) by XCMPLX_1:77
.= (1 - ((tan x) ^2)) / ((((cos x) ^2) / ((cos x) ^2)) + (((sin x) ^2) / ((cos x) ^2))) by XCMPLX_1:62
.= (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:76 ;
hence cos (2 * x) = (1 - ((tan x) ^2)) / (1 + ((tan x) ^2)) ; :: thesis: verum