itg2lecl

Description: If an S.2 integral is bounded above, then it is real. (Contributed by Mario Carneiro, 28-Jun-2014)

		Ref	Expression
	Assertion	itg2lecl	$⊢ (F : ℝ ⟶ [0, +∞] \land A \in ℝ \land \int^{2} (F) \leq A) \to \int^{2} (F) \in ℝ$

Step	Hyp	Ref	Expression
1		itg2cl	$⊢ F : ℝ ⟶ [0, +∞] \to \int^{2} (F) \in ℝ^{*}$
2	1	3ad2ant1	$⊢ (F : ℝ ⟶ [0, +∞] \land A \in ℝ \land \int^{2} (F) \leq A) \to \int^{2} (F) \in ℝ^{*}$
3		simp2	$⊢ (F : ℝ ⟶ [0, +∞] \land A \in ℝ \land \int^{2} (F) \leq A) \to A \in ℝ$
4		itg2ge0	$⊢ F : ℝ ⟶ [0, +∞] \to 0 \leq \int^{2} (F)$
5	4	3ad2ant1	$⊢ (F : ℝ ⟶ [0, +∞] \land A \in ℝ \land \int^{2} (F) \leq A) \to 0 \leq \int^{2} (F)$
6		simp3	$⊢ (F : ℝ ⟶ [0, +∞] \land A \in ℝ \land \int^{2} (F) \leq A) \to \int^{2} (F) \leq A$
7		xrrege0	$⊢ ((\int^{2} (F) \in ℝ^{*} \land A \in ℝ) \land (0 \leq \int^{2} (F) \land \int^{2} (F) \leq A)) \to \int^{2} (F) \in ℝ$
8	2 3 5 6 7	syl22anc	$⊢ (F : ℝ ⟶ [0, +∞] \land A \in ℝ \land \int^{2} (F) \leq A) \to \int^{2} (F) \in ℝ$

Metamath Proof Explorer