Theorem sge0rnre

Description: When sum^ is applied to nonnegative real numbers the range used in its definition is a subset of the reals. (Contributed by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Hypothesis	sge0rnre.1	|- ( ph -> F : X --> ( 0 [,) +oo ) )
Assertion	sge0rnre	|- ( ph -> ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) C_ RR )

Proof

Step	Hyp	Ref	Expression
1		sge0rnre.1	|- ( ph -> F : X --> ( 0 [,) +oo ) )
2		elinel2	|- ( x e. ( ~P X i^i Fin ) -> x e. Fin )
3	2	adantl	|- ( ( ph /\ x e. ( ~P X i^i Fin ) ) -> x e. Fin )
4		rge0ssre	|- ( 0 [,) +oo ) C_ RR
5	1	ad2antrr	|- ( ( ( ph /\ x e. ( ~P X i^i Fin ) ) /\ y e. x ) -> F : X --> ( 0 [,) +oo ) )
6		elinel1	|- ( x e. ( ~P X i^i Fin ) -> x e. ~P X )
7		elpwi	|- ( x e. ~P X -> x C_ X )
8	6 7	syl	|- ( x e. ( ~P X i^i Fin ) -> x C_ X )
9	8	adantr	|- ( ( x e. ( ~P X i^i Fin ) /\ y e. x ) -> x C_ X )
10		simpr	|- ( ( x e. ( ~P X i^i Fin ) /\ y e. x ) -> y e. x )
11	9 10	sseldd	|- ( ( x e. ( ~P X i^i Fin ) /\ y e. x ) -> y e. X )
12	11	adantll	|- ( ( ( ph /\ x e. ( ~P X i^i Fin ) ) /\ y e. x ) -> y e. X )
13	5 12	ffvelrnd	|- ( ( ( ph /\ x e. ( ~P X i^i Fin ) ) /\ y e. x ) -> ( F ` y ) e. ( 0 [,) +oo ) )
14	4 13	sselid	|- ( ( ( ph /\ x e. ( ~P X i^i Fin ) ) /\ y e. x ) -> ( F ` y ) e. RR )
15	3 14	fsumrecl	|- ( ( ph /\ x e. ( ~P X i^i Fin ) ) -> sum_ y e. x ( F ` y ) e. RR )
16	15	ralrimiva	|- ( ph -> A. x e. ( ~P X i^i Fin ) sum_ y e. x ( F ` y ) e. RR )
17		eqid	|- ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) = ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) )
18	17	rnmptss	|- ( A. x e. ( ~P X i^i Fin ) sum_ y e. x ( F ` y ) e. RR -> ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) C_ RR )
19	16 18	syl	|- ( ph -> ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) C_ RR )