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 A2, XREAL_1:17;
A5: 1 + (cos . x) > 1 + (- 1) by A3, XREAL_1:10;
then A6: (1 - (cos . x)) * (1 + (cos . x)) > 0 by A4, XREAL_1:131;
(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 A5, A6, PREPOWER:94
.= (1 - (cos . x)) #R (1 / 2) by A5, XCMPLX_1:90 ;
hence (sin . x) / ((1 + (cos . x)) #R (1 / 2)) = (1 - (cos . x)) #R (1 / 2) ; :: thesis: verum