itg2lcl

Description: The set of lower sums is a set of extended reals. (Contributed by Mario Carneiro, 28-Jun-2014)

		Ref	Expression
	Hypothesis	itg2val.1	$⊢ L = \{x \| \exists g \in dom \int^{1} (g \leq_{f} F \land x = \int^{1} (g))\}$
	Assertion	itg2lcl	$⊢ L \subseteq ℝ^{*}$

Step	Hyp	Ref	Expression
1		itg2val.1	$⊢ L = \{x \| \exists g \in dom \int^{1} (g \leq_{f} F \land x = \int^{1} (g))\}$
2		itg1cl	$⊢ g \in dom \int^{1} \to \int^{1} (g) \in ℝ$
3	2	rexrd	$⊢ g \in dom \int^{1} \to \int^{1} (g) \in ℝ^{*}$
4		simpr	$⊢ (g \leq_{f} F \land x = \int^{1} (g)) \to x = \int^{1} (g)$
5	4	eleq1d	$⊢ (g \leq_{f} F \land x = \int^{1} (g)) \to (x \in ℝ^{} \leftrightarrow \int^{1} (g) \in ℝ^{})$
6	3 5	syl5ibrcom	$⊢ g \in dom \int^{1} \to ((g \leq_{f} F \land x = \int^{1} (g)) \to x \in ℝ^{*})$
7	6	rexlimiv	$⊢ \exists g \in dom \int^{1} (g \leq_{f} F \land x = \int^{1} (g)) \to x \in ℝ^{*}$
8	7	abssi	$⊢ \{x \| \exists g \in dom \int^{1} (g \leq_{f} F \land x = \int^{1} (g))\} \subseteq ℝ^{*}$
9	1 8	eqsstri	$⊢ L \subseteq ℝ^{*}$

Metamath Proof Explorer