let x be Real; :: thesis: ( cos x <> 0 & sin x <> 0 implies ( cosec (2 * x) = ((sec x) * (cosec x)) / 2 & cosec (2 * x) = ((tan x) + (cot x)) / 2 ) )
assume that
A1: cos x <> 0 and
A2: sin x <> 0 ; :: thesis: ( cosec (2 * x) = ((sec x) * (cosec x)) / 2 & cosec (2 * x) = ((tan x) + (cot x)) / 2 )
A3: cosec (2 * x) = 1 / ((2 * (tan x)) / (1 + ((tan x) ^2))) by A1, Th6
.= (1 + ((tan x) ^2)) / (2 * (tan x)) by XCMPLX_1:57
.= ((1 + ((tan x) ^2)) / (tan x)) / 2 by XCMPLX_1:78
.= ((1 / ((sin x) / (cos x))) + (((tan x) ^2) / (tan x))) / 2 by XCMPLX_1:62
.= ((cot x) + (((tan x) * (tan x)) / (tan x))) / 2 by XCMPLX_1:57
.= ((cot x) + (tan x)) / 2 by A1, A2, XCMPLX_1:50, XCMPLX_1:89 ;
cosec (2 * x) = 1 / ((2 * (tan x)) / (1 + ((tan x) ^2))) by A1, Th6
.= (1 + ((tan x) ^2)) / (2 * (tan x)) by XCMPLX_1:57
.= ((sec x) ^2) / (2 * (tan x)) by A1, Th11
.= (((sec x) * (sec x)) / (tan x)) / 2 by XCMPLX_1:78
.= ((sec x) * ((sec x) / ((sin x) / (cos x)))) / 2 by XCMPLX_1:74
.= ((sec x) * (((sec x) * (cos x)) / (sin x))) / 2 by XCMPLX_1:77
.= ((sec x) * (cosec x)) / 2 by A1, XCMPLX_1:106 ;
hence ( cosec (2 * x) = ((sec x) * (cosec x)) / 2 & cosec (2 * x) = ((tan x) + (cot x)) / 2 ) by A3; :: thesis: verum