Metamath Proof Explorer

Theorem fsumrpcl

Description: Closure of a finite sum of positive reals. (Contributed by Mario Carneiro, 3-Jun-2014)

Ref Expression
Hypotheses fsumcl.1 ${⊢}{\phi }\to {A}\in \mathrm{Fin}$
fsumrpcl.2 ${⊢}{\phi }\to {A}\ne \varnothing$
fsumrpcl.3 ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to {B}\in {ℝ}^{+}$
Assertion fsumrpcl ${⊢}{\phi }\to \sum _{{k}\in {A}}{B}\in {ℝ}^{+}$

Proof

Step Hyp Ref Expression
1 fsumcl.1 ${⊢}{\phi }\to {A}\in \mathrm{Fin}$
2 fsumrpcl.2 ${⊢}{\phi }\to {A}\ne \varnothing$
3 fsumrpcl.3 ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to {B}\in {ℝ}^{+}$
4 rpssre ${⊢}{ℝ}^{+}\subseteq ℝ$
5 ax-resscn ${⊢}ℝ\subseteq ℂ$
6 4 5 sstri ${⊢}{ℝ}^{+}\subseteq ℂ$
7 6 a1i ${⊢}{\phi }\to {ℝ}^{+}\subseteq ℂ$
8 rpaddcl ${⊢}\left({x}\in {ℝ}^{+}\wedge {y}\in {ℝ}^{+}\right)\to {x}+{y}\in {ℝ}^{+}$
9 8 adantl ${⊢}\left({\phi }\wedge \left({x}\in {ℝ}^{+}\wedge {y}\in {ℝ}^{+}\right)\right)\to {x}+{y}\in {ℝ}^{+}$
10 7 9 1 3 2 fsumcl2lem ${⊢}{\phi }\to \sum _{{k}\in {A}}{B}\in {ℝ}^{+}$