Theorem 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	$$⊢\left(F:ℝ⟶\left[0,\mathrm{+\infty }\right]\wedge A\in ℝ\wedge {\int }^2\left(F\right)\le A\right)\to {\int }^2\left(F\right)\in ℝ$$

Proof

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