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

Metamath Proof Explorer

Theorem isumrecl

Description: The sum of a converging infinite real series is a real number. (Contributed by Mario Carneiro, 24-Apr-2014)

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

Proof

Step Hyp Ref Expression
1 isumrecl.1 
 |-  Z = ( ZZ>= ` M )
2 isumrecl.2 
 |-  ( ph -> M e. ZZ )
3 isumrecl.3 
 |-  ( ( ph /\ k e. Z ) -> ( F ` k ) = A )
4 isumrecl.4 
 |-  ( ( ph /\ k e. Z ) -> A e. RR )
5 isumrecl.5 
 |-  ( ph -> seq M ( + , F ) e. dom ~~> )
6 4 recnd 
 |-  ( ( ph /\ k e. Z ) -> A e. CC )
7 1 2 3 6 5 isumclim2 
 |-  ( ph -> seq M ( + , F ) ~~> sum_ k e. Z A )
8 3 4 eqeltrd 
 |-  ( ( ph /\ k e. Z ) -> ( F ` k ) e. RR )
9 1 2 8 serfre 
 |-  ( ph -> seq M ( + , F ) : Z --> RR )
10 9 ffvelcdmda 
 |-  ( ( ph /\ j e. Z ) -> ( seq M ( + , F ) ` j ) e. RR )
11 1 2 7 10 climrecl 
 |-  ( ph -> sum_ k e. Z A e. RR )