Metamath Proof Explorer


Theorem fsumrecl

Description: Closure of a finite sum of reals. (Contributed by NM, 9-Nov-2005) (Revised by Mario Carneiro, 22-Apr-2014)

Ref Expression
Hypotheses fsumcl.1
|- ( ph -> A e. Fin )
fsumrecl.2
|- ( ( ph /\ k e. A ) -> B e. RR )
Assertion fsumrecl
|- ( ph -> sum_ k e. A B e. RR )

Proof

Step Hyp Ref Expression
1 fsumcl.1
 |-  ( ph -> A e. Fin )
2 fsumrecl.2
 |-  ( ( ph /\ k e. A ) -> B e. RR )
3 ax-resscn
 |-  RR C_ CC
4 3 a1i
 |-  ( ph -> RR C_ CC )
5 readdcl
 |-  ( ( x e. RR /\ y e. RR ) -> ( x + y ) e. RR )
6 5 adantl
 |-  ( ( ph /\ ( x e. RR /\ y e. RR ) ) -> ( x + y ) e. RR )
7 0red
 |-  ( ph -> 0 e. RR )
8 4 6 1 2 7 fsumcllem
 |-  ( ph -> sum_ k e. A B e. RR )