Theorem isumneg

Description: Negation of a converging sum. (Contributed by Glauco Siliprandi, 29-Jun-2017)

	Ref	Expression
Hypotheses	isumneg.1	|- Z = ( ZZ>= ` M )
	isumneg.2	|- ( ph -> M e. ZZ )
	isumneg.3	|- ( ph -> sum_ k e. Z A e. CC )
	isumneg.4	|- ( ( ph /\ k e. Z ) -> ( F ` k ) = A )
	isumneg.5	|- ( ( ph /\ k e. Z ) -> A e. CC )
	isumneg.6	|- ( ph -> seq M ( + , F ) e. dom ~~> )
Assertion	isumneg	|- ( ph -> sum_ k e. Z -u A = -u sum_ k e. Z A )

Proof

Step	Hyp	Ref	Expression
1		isumneg.1	|- Z = ( ZZ>= ` M )
2		isumneg.2	|- ( ph -> M e. ZZ )
3		isumneg.3	|- ( ph -> sum_ k e. Z A e. CC )
4		isumneg.4	|- ( ( ph /\ k e. Z ) -> ( F ` k ) = A )
5		isumneg.5	|- ( ( ph /\ k e. Z ) -> A e. CC )
6		isumneg.6	|- ( ph -> seq M ( + , F ) e. dom ~~> )
7	5	mulm1d	|- ( ( ph /\ k e. Z ) -> ( -u 1 x. A ) = -u A )
8	7	eqcomd	|- ( ( ph /\ k e. Z ) -> -u A = ( -u 1 x. A ) )
9	8	sumeq2dv	|- ( ph -> sum_ k e. Z -u A = sum_ k e. Z ( -u 1 x. A ) )
10		1cnd	|- ( ph -> 1 e. CC )
11	10	negcld	|- ( ph -> -u 1 e. CC )
12	1 2 4 5 6 11	isummulc2	|- ( ph -> ( -u 1 x. sum_ k e. Z A ) = sum_ k e. Z ( -u 1 x. A ) )
13	3	mulm1d	|- ( ph -> ( -u 1 x. sum_ k e. Z A ) = -u sum_ k e. Z A )
14	9 12 13	3eqtr2d	|- ( ph -> sum_ k e. Z -u A = -u sum_ k e. Z A )