let x be Real; ( 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 that
A1:
cos x <> 0
and
A2:
sin x <> 0
; ( sec (2 * x) = ((sec x) ^2) / (1 - ((tan x) ^2)) & sec (2 * x) = ((cot x) + (tan x)) / ((cot x) - (tan x)) )
A3: sec (2 * x) =
1 / ((1 - ((tan x) ^2)) / (1 + ((tan x) ^2)))
by A1, 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, A2, XCMPLX_1:50, XCMPLX_1:55
.=
((1 / (tan x)) + (((tan x) ^2) / (tan x))) / ((1 - ((tan x) ^2)) / (tan x))
by XCMPLX_1:62
.=
((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:120
.=
((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, A2, XCMPLX_1:50, XCMPLX_1:89
;
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, A3, XCMPLX_1:50, XCMPLX_1:89; verum