Metamath Proof Explorer

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 
|- ( ( F : RR --> ( 0 [,] +oo ) /\ A e. RR /\ ( S.2 ` F ) <_ A ) -> ( S.2 ` F ) e. RR )

Proof

Step Hyp Ref Expression
1 itg2cl 
 |-  ( F : RR --> ( 0 [,] +oo ) -> ( S.2 ` F ) e. RR* )
2 1 3ad2ant1 
 |-  ( ( F : RR --> ( 0 [,] +oo ) /\ A e. RR /\ ( S.2 ` F ) <_ A ) -> ( S.2 ` F ) e. RR* )
3 simp2 
 |-  ( ( F : RR --> ( 0 [,] +oo ) /\ A e. RR /\ ( S.2 ` F ) <_ A ) -> A e. RR )
4 itg2ge0 
 |-  ( F : RR --> ( 0 [,] +oo ) -> 0 <_ ( S.2 ` F ) )
5 4 3ad2ant1 
 |-  ( ( F : RR --> ( 0 [,] +oo ) /\ A e. RR /\ ( S.2 ` F ) <_ A ) -> 0 <_ ( S.2 ` F ) )
6 simp3 
 |-  ( ( F : RR --> ( 0 [,] +oo ) /\ A e. RR /\ ( S.2 ` F ) <_ A ) -> ( S.2 ` F ) <_ A )
7 xrrege0 
 |-  ( ( ( ( S.2 ` F ) e. RR* /\ A e. RR ) /\ ( 0 <_ ( S.2 ` F ) /\ ( S.2 ` F ) <_ A ) ) -> ( S.2 ` F ) e. RR )
8 2 3 5 6 7 syl22anc 
 |-  ( ( F : RR --> ( 0 [,] +oo ) /\ A e. RR /\ ( S.2 ` F ) <_ A ) -> ( S.2 ` F ) e. RR )