Theorem fsumrpcl

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

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

Proof

Step	Hyp	Ref	Expression
1		fsumcl.1	|- ( ph -> A e. Fin )
2		fsumrpcl.2	|- ( ph -> A =/= (/) )
3		fsumrpcl.3	|- ( ( ph /\ k e. A ) -> B e. RR+ )
4		rpssre	|- RR+ C_ RR
5		ax-resscn	|- RR C_ CC
6	4 5	sstri	|- RR+ C_ CC
7	6	a1i	|- ( ph -> RR+ C_ CC )
8		rpaddcl	|- ( ( x e. RR+ /\ y e. RR+ ) -> ( x + y ) e. RR+ )
9	8	adantl	|- ( ( ph /\ ( x e. RR+ /\ y e. RR+ ) ) -> ( x + y ) e. RR+ )
10	7 9 1 3 2	fsumcl2lem	|- ( ph -> sum_ k e. A B e. RR+ )