let th be real number ; :: thesis: ( cos . 0 = 1 & sin . 0 = 0 & cos . (- th) = cos . th & sin . (- th) = - (sin . th) )
thus cos . 0 = Re (Sum ((0 * <i> ) ExpSeq )) by Def22
.= 1 by Th10, COMPLEX1:15 ; :: thesis: ( sin . 0 = 0 & cos . (- th) = cos . th & sin . (- th) = - (sin . th) )
thus sin . 0 = Im (Sum ((0 * <i> ) ExpSeq )) by Def20
.= 0 by Th10, COMPLEX1:15 ; :: thesis: ( cos . (- th) = cos . th & sin . (- th) = - (sin . th) )
reconsider th1 = th as Real by XREAL_0:def 1;
thus cos . (- th) = Re (Sum (((- 0 ) + ((- th1) * <i> )) ExpSeq )) by Def22
.= Re (Sum ((- (th1 * <i> )) ExpSeq ))
.= Re ((Sum ((th1 * <i> ) ExpSeq )) *' ) by Lm4
.= Re (((cos . th) + ((sin . th) * <i> )) *' ) by Lm3
.= Re ((cos . th) + ((- (sin . th)) * <i> )) by Lm1
.= cos . th by COMPLEX1:28 ; :: thesis: sin . (- th) = - (sin . th)
thus sin . (- th) = Im (Sum (((- 0 ) + ((- th1) * <i> )) ExpSeq )) by Def20
.= Im (Sum ((- (th1 * <i> )) ExpSeq ))
.= Im ((Sum ((th1 * <i> ) ExpSeq )) *' ) by Lm4
.= Im (((cos . th) + ((sin . th) * <i> )) *' ) by Lm3
.= Im ((cos . th) + ((- (sin . th)) * <i> )) by Lm1
.= - (sin . th) by COMPLEX1:28 ; :: thesis: verum