This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )