let p, q be Real; (sin . (p + q)) - (sin . p) = (q * (cos . p)) + (q * (Re ((Sum ((q * <i> ) P_dt )) * ((cos . p) + ((sin . p) * <i> )))))
(sin . (p + q)) - (sin . p) =
(sin . (p + q)) - (Im (Sum ((p * <i> ) ExpSeq )))
by Def20
.=
(Im (Sum (((p + q) * <i> ) ExpSeq ))) - (Im (Sum ((p * <i> ) ExpSeq )))
by Def20
.=
Im ((Sum (((p * <i> ) + (q * <i> )) ExpSeq )) - (Sum ((p * <i> ) ExpSeq )))
by COMPLEX1:48
.=
Im (((Sum ((p * <i> ) ExpSeq )) * (q * <i> )) + (((q * <i> ) * (Sum ((q * <i> ) P_dt ))) * (Sum ((p * <i> ) ExpSeq ))))
by Th64
.=
Im ((((cos . p) + ((sin . p) * <i> )) * (q * <i> )) + (((q * <i> ) * (Sum ((q * <i> ) P_dt ))) * (Sum ((p * <i> ) ExpSeq ))))
by Lm3
.=
Im ((((cos . p) + ((sin . p) * <i> )) * (q * <i> )) + (((q * <i> ) * (Sum ((q * <i> ) P_dt ))) * ((cos . p) + ((sin . p) * <i> ))))
by Lm3
.=
(Im ((- (q * (sin . p))) + ((q * (cos . p)) * <i> ))) + (Im (((q * <i> ) * (Sum ((q * <i> ) P_dt ))) * ((cos . p) + ((sin . p) * <i> ))))
by COMPLEX1:19
.=
(q * (cos . p)) + (Im ((q * <i> ) * ((Sum ((q * <i> ) P_dt )) * ((cos . p) + ((sin . p) * <i> )))))
by COMPLEX1:28
.=
(q * (cos . p)) + (q * (Re ((Sum ((q * <i> ) P_dt )) * ((cos . p) + ((sin . p) * <i> )))))
by Lm13
;
hence
(sin . (p + q)) - (sin . p) = (q * (cos . p)) + (q * (Re ((Sum ((q * <i> ) P_dt )) * ((cos . p) + ((sin . p) * <i> )))))
; verum