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

Metamath Proof Explorer

Theorem itg2i1fseq3

Description: Special case of itg2i1fseq2 : if the integral of F is a real number, then the standard limit relation holds on the integrals of simple functions approaching F . (Contributed by Mario Carneiro, 17-Aug-2014)

Ref Expression
Hypotheses itg2i1fseq.1 ⊢ ( 𝜑 → 𝐹 ∈ MblFn )
itg2i1fseq.2 ⊢ ( 𝜑 → 𝐹 : ℝ ⟶ ( 0 [,) +∞ ) )
itg2i1fseq.3 ⊢ ( 𝜑 → 𝑃 : ℕ ⟶ dom ∫1 )
itg2i1fseq.4 ⊢ ( 𝜑 → ∀ 𝑛 ∈ ℕ ( 0𝑝 ∘r ≤ ( 𝑃 ‘ 𝑛 ) ∧ ( 𝑃 ‘ 𝑛 ) ∘r ≤ ( 𝑃 ‘ ( 𝑛 + 1 ) ) ) )
itg2i1fseq.5 ⊢ ( 𝜑 → ∀ 𝑥 ∈ ℝ ( 𝑛 ∈ ℕ ↦ ( ( 𝑃 ‘ 𝑛 ) ‘ 𝑥 ) ) ⇝ ( 𝐹 ‘ 𝑥 ) )
itg2i1fseq.6 ⊢ 𝑆 = ( 𝑚 ∈ ℕ ↦ ( ∫1 ‘ ( 𝑃 ‘ 𝑚 ) ) )
itg2i1fseq3.7 ⊢ ( 𝜑 → ( ∫2 ‘ 𝐹 ) ∈ ℝ )
Assertion itg2i1fseq3 ( 𝜑 → 𝑆 ⇝ ( ∫2 ‘ 𝐹 ) )

Proof

Step Hyp Ref Expression
1 itg2i1fseq.1 ⊢ ( 𝜑 → 𝐹 ∈ MblFn )
2 itg2i1fseq.2 ⊢ ( 𝜑 → 𝐹 : ℝ ⟶ ( 0 [,) +∞ ) )
3 itg2i1fseq.3 ⊢ ( 𝜑 → 𝑃 : ℕ ⟶ dom ∫1 )
4 itg2i1fseq.4 ⊢ ( 𝜑 → ∀ 𝑛 ∈ ℕ ( 0𝑝 ∘r ≤ ( 𝑃 ‘ 𝑛 ) ∧ ( 𝑃 ‘ 𝑛 ) ∘r ≤ ( 𝑃 ‘ ( 𝑛 + 1 ) ) ) )
5 itg2i1fseq.5 ⊢ ( 𝜑 → ∀ 𝑥 ∈ ℝ ( 𝑛 ∈ ℕ ↦ ( ( 𝑃 ‘ 𝑛 ) ‘ 𝑥 ) ) ⇝ ( 𝐹 ‘ 𝑥 ) )
6 itg2i1fseq.6 ⊢ 𝑆 = ( 𝑚 ∈ ℕ ↦ ( ∫1 ‘ ( 𝑃 ‘ 𝑚 ) ) )
7 itg2i1fseq3.7 ⊢ ( 𝜑 → ( ∫2 ‘ 𝐹 ) ∈ ℝ )
8 icossicc ⊢ ( 0 [,) +∞ ) ⊆ ( 0 [,] +∞ )
9 fss ⊢ ( ( 𝐹 : ℝ ⟶ ( 0 [,) +∞ ) ∧ ( 0 [,) +∞ ) ⊆ ( 0 [,] +∞ ) ) → 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) )
10 2 8 9 sylancl ⊢ ( 𝜑 → 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) )
11 10 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) )
12 3 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝑃 ‘ 𝑘 ) ∈ dom ∫1 )
13 1 2 3 4 5 itg2i1fseqle ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝑃 ‘ 𝑘 ) ∘r ≤ 𝐹 )
14 itg2ub ⊢ ( ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ ( 𝑃 ‘ 𝑘 ) ∈ dom ∫1 ∧ ( 𝑃 ‘ 𝑘 ) ∘r ≤ 𝐹 ) → ( ∫1 ‘ ( 𝑃 ‘ 𝑘 ) ) ≤ ( ∫2 ‘ 𝐹 ) )
15 11 12 13 14 syl3anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ∫1 ‘ ( 𝑃 ‘ 𝑘 ) ) ≤ ( ∫2 ‘ 𝐹 ) )
16 1 2 3 4 5 6 7 15 itg2i1fseq2 ⊢ ( 𝜑 → 𝑆 ⇝ ( ∫2 ‘ 𝐹 ) )