let x be real number ; :: thesis: ( cos x <> 0 & sin x <> 0 implies ( sec (2 * x) = ((sec x) ^2 ) / (1 - ((tan x) ^2 )) & sec (2 * x) = ((cot x) + (tan x)) / ((cot x) - (tan x)) ) )
assume A1: ( cos x <> 0 & sin x <> 0 ) ; :: thesis: ( sec (2 * x) = ((sec x) ^2 ) / (1 - ((tan x) ^2 )) & sec (2 * x) = ((cot x) + (tan x)) / ((cot x) - (tan x)) )
then A2: sec (2 * x) = 1 / ((1 - ((tan x) ^2 )) / (1 + ((tan x) ^2 ))) by Th8
.= (1 + ((tan x) ^2 )) / (1 - ((tan x) ^2 )) by XCMPLX_1:57
.= ((sec x) ^2 ) / (1 - ((tan x) ^2 )) by A1, Th11 ;
then sec (2 * x) = (1 + ((tan x) ^2 )) / (1 - ((tan x) ^2 )) by A1, Th11
.= ((1 + ((tan x) ^2 )) / (tan x)) / ((1 - ((tan x) ^2 )) / (tan x)) by A1, XCMPLX_1:50, XCMPLX_1:55
.= ((1 / (tan x)) + (((tan x) ^2 ) / (tan x))) / ((1 - ((tan x) ^2 )) / (tan x)) by XCMPLX_1:63
.= ((cot x) + (((tan x) ^2 ) / (tan x))) / ((1 - ((tan x) ^2 )) / (tan x)) by XCMPLX_1:57
.= ((cot x) + (((tan x) ^2 ) / (tan x))) / ((1 / (tan x)) - (((tan x) ^2 ) / (tan x))) by XCMPLX_1:121
.= ((cot x) + (((tan x) * (tan x)) / (tan x))) / ((cot x) - (((tan x) ^2 ) / (tan x))) by XCMPLX_1:57
.= ((cot x) + (tan x)) / ((cot x) - (((tan x) * (tan x)) / (tan x))) by A1, XCMPLX_1:50, XCMPLX_1:90 ;
hence ( sec (2 * x) = ((sec x) ^2 ) / (1 - ((tan x) ^2 )) & sec (2 * x) = ((cot x) + (tan x)) / ((cot x) - (tan x)) ) by A1, A2, XCMPLX_1:50, XCMPLX_1:90; :: thesis: verum