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 Def18
.=
(Re (Sum (((p + q) * <i>) ExpSeq))) - (Re (Sum ((p * <i>) ExpSeq)))
by Def18
.=
Re ((Sum (((p * <i>) + (q * <i>)) ExpSeq)) - (Sum ((p * <i>) ExpSeq)))
by COMPLEX1:19
.=
Re (((Sum ((p * <i>) ExpSeq)) * (q * <i>)) + (((q * <i>) * (Sum ((q * <i>) P_dt))) * (Sum ((p * <i>) ExpSeq))))
by Th58
.=
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:8
.=
(- (q * (sin . p))) + (Re ((q * <i>) * ((Sum ((q * <i>) P_dt)) * ((cos . p) + ((sin . p) * <i>)))))
by COMPLEX1:12
.=
(- (q * (sin . p))) - (q * (Im ((Sum ((q * <i>) P_dt)) * ((cos . p) + ((sin . p) * <i>)))))
by Lm12
;
hence
(cos . (p + q)) - (cos . p) = (- (q * (sin . p))) - (q * (Im ((Sum ((q * <i>) P_dt)) * ((cos . p) + ((sin . p) * <i>)))))
; verum