let x be Real; :: thesis: ( sin . x > 0 & cos . x < 1 & cos . x > - 1 implies (sin . x) / ((1 + (cos . x)) #R (1 / 2)) = (1 - (cos . x)) #R (1 / 2) )
assume that
A1: sin . x > 0 and
A2: cos . x < 1 and
A3: cos . x > - 1 ; :: thesis: (sin . x) / ((1 + (cos . x)) #R (1 / 2)) = (1 - (cos . x)) #R (1 / 2)
A4: 1 + (cos . x) > 1 + (- 1) by A3, XREAL_1:8;
1 - (cos . x) > 1 - 1 by A2, XREAL_1:15;
then A5: (1 - (cos . x)) * (1 + (cos . x)) > 0 by A4, XREAL_1:129;
(sin . x) / ((1 + (cos . x)) #R (1 / 2)) = (((1 - (cos . x)) * (1 + (cos . x))) #R (1 / 2)) / ((1 + (cos . x)) #R (1 / 2)) by A1, Lm3
.= (((1 - (cos . x)) * (1 + (cos . x))) / (1 + (cos . x))) #R (1 / 2) by A4, A5, PREPOWER:80
.= (1 - (cos . x)) #R (1 / 2) by A4, XCMPLX_1:89 ;
hence (sin . x) / ((1 + (cos . x)) #R (1 / 2)) = (1 - (cos . x)) #R (1 / 2) ; :: thesis: verum