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	$⊢ φ \to F \in MblFn$
		itg2i1fseq.2	$⊢ φ \to F : ℝ ⟶ [0, +∞)$
		itg2i1fseq.3	$⊢ φ \to P : ℕ ⟶ dom \int^{1}$
		itg2i1fseq.4	$⊢ φ \to \forall n \in ℕ (0_{𝑝} \leq_{f} P (n) \land P (n) \leq_{f} P (n + 1))$
		itg2i1fseq.5	$⊢ φ \to \forall x \in ℝ (n \in ℕ ⟼ P (n) (x)) ⇝ F (x)$
		itg2i1fseq.6	$⊢ S = (m \in ℕ ⟼ \int^{1} (P (m)))$
		itg2i1fseq3.7	$⊢ φ \to \int^{2} (F) \in ℝ$
	Assertion	itg2i1fseq3	$⊢ φ \to S ⇝ \int^{2} (F)$

Proof

Step	Hyp	Ref	Expression
1		itg2i1fseq.1	$⊢ φ \to F \in MblFn$
2		itg2i1fseq.2	$⊢ φ \to F : ℝ ⟶ [0, +∞)$
3		itg2i1fseq.3	$⊢ φ \to P : ℕ ⟶ dom \int^{1}$
4		itg2i1fseq.4	$⊢ φ \to \forall n \in ℕ (0_{𝑝} \leq_{f} P (n) \land P (n) \leq_{f} P (n + 1))$
5		itg2i1fseq.5	$⊢ φ \to \forall x \in ℝ (n \in ℕ ⟼ P (n) (x)) ⇝ F (x)$
6		itg2i1fseq.6	$⊢ S = (m \in ℕ ⟼ \int^{1} (P (m)))$
7		itg2i1fseq3.7	$⊢ φ \to \int^{2} (F) \in ℝ$
8		icossicc	$⊢ [0, +∞) \subseteq [0, +∞]$
9		fss	$⊢ (F : ℝ ⟶ [0, +∞) \land [0, +∞) \subseteq [0, +∞]) \to F : ℝ ⟶ [0, +∞]$
10	2 8 9	sylancl	$⊢ φ \to F : ℝ ⟶ [0, +∞]$
11	10	adantr	$⊢ (φ \land k \in ℕ) \to F : ℝ ⟶ [0, +∞]$
12	3	ffvelcdmda	$⊢ (φ \land k \in ℕ) \to P (k) \in dom \int^{1}$
13	1 2 3 4 5	itg2i1fseqle	$⊢ (φ \land k \in ℕ) \to P (k) \leq_{f} F$
14		itg2ub	$⊢ (F : ℝ ⟶ [0, +∞] \land P (k) \in dom \int^{1} \land P (k) \leq_{f} F) \to \int^{1} (P (k)) \leq \int^{2} (F)$
15	11 12 13 14	syl3anc	$⊢ (φ \land k \in ℕ) \to \int^{1} (P (k)) \leq \int^{2} (F)$
16	1 2 3 4 5 6 7 15	itg2i1fseq2	$⊢ φ \to S ⇝ \int^{2} (F)$