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