let x be Real; ( sin (x / 2) <> 0 & cos (x / 2) <> 0 & 1 - ((tan (x / 2)) ^2) <> 0 & not cosec (x / 2) = sqrt ((2 * (sec x)) / ((sec x) - 1)) implies cosec (x / 2) = - (sqrt ((2 * (sec x)) / ((sec x) - 1))) )
assume that
A1:
sin (x / 2) <> 0
and
A2:
cos (x / 2) <> 0
and
A3:
1 - ((tan (x / 2)) ^2) <> 0
; ( cosec (x / 2) = sqrt ((2 * (sec x)) / ((sec x) - 1)) or cosec (x / 2) = - (sqrt ((2 * (sec x)) / ((sec x) - 1))) )
set b = (sec (x / 2)) ^2 ;
set a = 1 - ((tan (x / 2)) ^2);
A4: ((sec (x / 2)) ^2) - (1 - ((tan (x / 2)) ^2)) =
(1 + ((tan (x / 2)) ^2)) - (1 - ((tan (x / 2)) ^2))
by A2, Th11
.=
2 * ((tan (x / 2)) ^2)
;
sqrt ((2 * (sec x)) / ((sec x) - 1)) =
sqrt ((2 * (((sec (x / 2)) ^2) / (1 - ((tan (x / 2)) ^2)))) / ((sec (2 * (x / 2))) - 1))
by A1, A2, Th13
.=
sqrt ((2 * (((sec (x / 2)) ^2) / (1 - ((tan (x / 2)) ^2)))) / ((((sec (x / 2)) ^2) / (1 - ((tan (x / 2)) ^2))) - 1))
by A1, A2, Th13
;
then A5: sqrt ((2 * (sec x)) / ((sec x) - 1)) =
sqrt (((2 * (((sec (x / 2)) ^2) / (1 - ((tan (x / 2)) ^2)))) * (1 - ((tan (x / 2)) ^2))) / (((((sec (x / 2)) ^2) / (1 - ((tan (x / 2)) ^2))) - 1) * (1 - ((tan (x / 2)) ^2))))
by A3, XCMPLX_1:91
.=
sqrt ((2 * ((((sec (x / 2)) ^2) / (1 - ((tan (x / 2)) ^2))) * (1 - ((tan (x / 2)) ^2)))) / (((((sec (x / 2)) ^2) / (1 - ((tan (x / 2)) ^2))) * (1 - ((tan (x / 2)) ^2))) - (1 * (1 - ((tan (x / 2)) ^2)))))
.=
sqrt ((2 * ((((sec (x / 2)) ^2) / (1 - ((tan (x / 2)) ^2))) * (1 - ((tan (x / 2)) ^2)))) / (((sec (x / 2)) ^2) - (1 - ((tan (x / 2)) ^2))))
by A3, XCMPLX_1:87
.=
sqrt ((2 * ((sec (x / 2)) ^2)) / (2 * ((tan (x / 2)) ^2)))
by A3, A4, XCMPLX_1:87
.=
sqrt (((sec (x / 2)) ^2) / ((tan (x / 2)) ^2))
by XCMPLX_1:91
.=
sqrt (((sec (x / 2)) / (tan (x / 2))) ^2)
by XCMPLX_1:76
.=
sqrt ((cosec (x / 2)) ^2)
by A2, Th1
.=
|.(cosec (x / 2)).|
by COMPLEX1:72
;