This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 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 ⊢ 𝐿 = { 𝑥 ∣ ∃ 𝑔 ∈ dom ∫1 ( 𝑔 ∘r ≤ 𝐹 ∧ 𝑥 = ( ∫1 ‘ 𝑔 ) ) }
Assertion itg2lcl 𝐿 ⊆ ℝ*

Proof

Step Hyp Ref Expression
1 itg2val.1 ⊢ 𝐿 = { 𝑥 ∣ ∃ 𝑔 ∈ dom ∫1 ( 𝑔 ∘r ≤ 𝐹 ∧ 𝑥 = ( ∫1 ‘ 𝑔 ) ) }
2 itg1cl ⊢ ( 𝑔 ∈ dom ∫1 → ( ∫1 ‘ 𝑔 ) ∈ ℝ )
3 2 rexrd ⊢ ( 𝑔 ∈ dom ∫1 → ( ∫1 ‘ 𝑔 ) ∈ ℝ* )
4 simpr ⊢ ( ( 𝑔 ∘r ≤ 𝐹 ∧ 𝑥 = ( ∫1 ‘ 𝑔 ) ) → 𝑥 = ( ∫1 ‘ 𝑔 ) )
5 4 eleq1d ⊢ ( ( 𝑔 ∘r ≤ 𝐹 ∧ 𝑥 = ( ∫1 ‘ 𝑔 ) ) → ( 𝑥 ∈ ℝ* ↔ ( ∫1 ‘ 𝑔 ) ∈ ℝ* ) )
6 3 5 syl5ibrcom ⊢ ( 𝑔 ∈ dom ∫1 → ( ( 𝑔 ∘r ≤ 𝐹 ∧ 𝑥 = ( ∫1 ‘ 𝑔 ) ) → 𝑥 ∈ ℝ* ) )
7 6 rexlimiv ⊢ ( ∃ 𝑔 ∈ dom ∫1 ( 𝑔 ∘r ≤ 𝐹 ∧ 𝑥 = ( ∫1 ‘ 𝑔 ) ) → 𝑥 ∈ ℝ* )
8 7 abssi ⊢ { 𝑥 ∣ ∃ 𝑔 ∈ dom ∫1 ( 𝑔 ∘r ≤ 𝐹 ∧ 𝑥 = ( ∫1 ‘ 𝑔 ) ) } ⊆ ℝ*
9 1 8 eqsstri ⊢ 𝐿 ⊆ ℝ*