let x be Real; :: thesis: ( cos (x / 2) <> 0 implies tan (x / 2) = (sin x) / (1 + (cos x)) )
assume cos (x / 2) <> 0 ; :: thesis: tan (x / 2) = (sin x) / (1 + (cos x))
then A1: 2 * (cos (x / 2)) <> 0 ;
(sin x) / (1 + (cos x)) = ((2 * (sin (x / 2))) * (cos (x / 2))) / (1 + (cos (2 * (x / 2)))) by Th5
.= ((2 * (sin (x / 2))) * (cos (x / 2))) / (1 + ((2 * ((cos (x / 2)) ^2)) - 1)) by Th7
.= ((2 * (cos (x / 2))) * (sin (x / 2))) / ((2 * (cos (x / 2))) * (cos (x / 2)))
.= (sin (x / 2)) / (cos (x / 2)) by A1, XCMPLX_1:91 ;
hence tan (x / 2) = (sin x) / (1 + (cos x)) ; :: thesis: verum