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	ffvelrnda	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝑃 ‘ 𝑘 ) ∈ 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 ‘ 𝐹 ) )