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 ⊢ φ → F ∈ MblFn
itg2i1fseq.2 ⊢ φ → F : ℝ ⟶ 0 +∞
itg2i1fseq.3 ⊢ φ → P : ℕ ⟶ dom ⁡ ∫ 1
itg2i1fseq.4 ⊢ φ → ∀ n ∈ ℕ 0 𝑝 ≤ f P ⁡ n ∧ P ⁡ n ≤ f P ⁡ n + 1
itg2i1fseq.5 ⊢ φ → ∀ x ∈ ℝ n ∈ ℕ ⟼ P ⁡ n ⁡ x ⇝ F ⁡ x
itg2i1fseq.6 ⊢ S = m ∈ ℕ ⟼ ∫ 1 ⁡ P ⁡ m
itg2i1fseq3.7 ⊢ φ → ∫ 2 ⁡ F ∈ ℝ
Assertion itg2i1fseq3 ⊢ φ → S ⇝ ∫ 2 ⁡ F

Proof

Step Hyp Ref Expression
1 itg2i1fseq.1 ⊢ φ → F ∈ MblFn
2 itg2i1fseq.2 ⊢ φ → F : ℝ ⟶ 0 +∞
3 itg2i1fseq.3 ⊢ φ → P : ℕ ⟶ dom ⁡ ∫ 1
4 itg2i1fseq.4 ⊢ φ → ∀ n ∈ ℕ 0 𝑝 ≤ f P ⁡ n ∧ P ⁡ n ≤ f P ⁡ n + 1
5 itg2i1fseq.5 ⊢ φ → ∀ x ∈ ℝ n ∈ ℕ ⟼ P ⁡ n ⁡ x ⇝ F ⁡ x
6 itg2i1fseq.6 ⊢ S = m ∈ ℕ ⟼ ∫ 1 ⁡ P ⁡ m
7 itg2i1fseq3.7 ⊢ φ → ∫ 2 ⁡ F ∈ ℝ
8 icossicc ⊢ 0 +∞ ⊆ 0 +∞
9 fss ⊢ F : ℝ ⟶ 0 +∞ ∧ 0 +∞ ⊆ 0 +∞ → F : ℝ ⟶ 0 +∞
10 2 8 9 sylancl ⊢ φ → F : ℝ ⟶ 0 +∞
11 10 adantr ⊢ φ ∧ k ∈ ℕ → F : ℝ ⟶ 0 +∞
12 3 ffvelcdmda ⊢ φ ∧ k ∈ ℕ → P ⁡ k ∈ dom ⁡ ∫ 1
13 1 2 3 4 5 itg2i1fseqle ⊢ φ ∧ k ∈ ℕ → P ⁡ k ≤ f F
14 itg2ub ⊢ F : ℝ ⟶ 0 +∞ ∧ P ⁡ k ∈ dom ⁡ ∫ 1 ∧ P ⁡ k ≤ f F → ∫ 1 ⁡ P ⁡ k ≤ ∫ 2 ⁡ F
15 11 12 13 14 syl3anc ⊢ φ ∧ k ∈ ℕ → ∫ 1 ⁡ P ⁡ k ≤ ∫ 2 ⁡ F
16 1 2 3 4 5 6 7 15 itg2i1fseq2 ⊢ φ → S ⇝ ∫ 2 ⁡ F