Metamath Proof Explorer

Theorem itg2ge0

Description: The integral of a nonnegative real function is greater than or equal to zero. (Contributed by Mario Carneiro, 28-Jun-2014)

Ref Expression
Assertion itg2ge0 
|- ( F : RR --> ( 0 [,] +oo ) -> 0 <_ ( S.2 ` F ) )

Proof

Step Hyp Ref Expression
1 itg10 
 |-  ( S.1 ` ( RR X. { 0 } ) ) = 0
2 ffvelrn 
 |-  ( ( F : RR --> ( 0 [,] +oo ) /\ y e. RR ) -> ( F ` y ) e. ( 0 [,] +oo ) )
3 0xr 
 |-  0 e. RR*
4 pnfxr 
 |-  +oo e. RR*
5 elicc1 
 |-  ( ( 0 e. RR* /\ +oo e. RR* ) -> ( ( F ` y ) e. ( 0 [,] +oo ) <-> ( ( F ` y ) e. RR* /\ 0 <_ ( F ` y ) /\ ( F ` y ) <_ +oo ) ) )
6 3 4 5 mp2an 
 |-  ( ( F ` y ) e. ( 0 [,] +oo ) <-> ( ( F ` y ) e. RR* /\ 0 <_ ( F ` y ) /\ ( F ` y ) <_ +oo ) )
7 6 simp2bi 
 |-  ( ( F ` y ) e. ( 0 [,] +oo ) -> 0 <_ ( F ` y ) )
8 2 7 syl 
 |-  ( ( F : RR --> ( 0 [,] +oo ) /\ y e. RR ) -> 0 <_ ( F ` y ) )
9 8 ralrimiva 
 |-  ( F : RR --> ( 0 [,] +oo ) -> A. y e. RR 0 <_ ( F ` y ) )
10 0re 
 |-  0 e. RR
11 fnconstg 
 |-  ( 0 e. RR -> ( RR X. { 0 } ) Fn RR )
12 10 11 mp1i 
 |-  ( F : RR --> ( 0 [,] +oo ) -> ( RR X. { 0 } ) Fn RR )
13 ffn 
 |-  ( F : RR --> ( 0 [,] +oo ) -> F Fn RR )
14 reex 
 |-  RR e. _V
15 14 a1i 
 |-  ( F : RR --> ( 0 [,] +oo ) -> RR e. _V )
16 inidm 
 |-  ( RR i^i RR ) = RR
17 c0ex 
 |-  0 e. _V
18 17 fvconst2 
 |-  ( y e. RR -> ( ( RR X. { 0 } ) ` y ) = 0 )
19 18 adantl 
 |-  ( ( F : RR --> ( 0 [,] +oo ) /\ y e. RR ) -> ( ( RR X. { 0 } ) ` y ) = 0 )
20 eqidd 
 |-  ( ( F : RR --> ( 0 [,] +oo ) /\ y e. RR ) -> ( F ` y ) = ( F ` y ) )
21 12 13 15 15 16 19 20 ofrfval 
 |-  ( F : RR --> ( 0 [,] +oo ) -> ( ( RR X. { 0 } ) oR <_ F <-> A. y e. RR 0 <_ ( F ` y ) ) )
22 9 21 mpbird 
 |-  ( F : RR --> ( 0 [,] +oo ) -> ( RR X. { 0 } ) oR <_ F )
23 i1f0 
 |-  ( RR X. { 0 } ) e. dom S.1
24 itg2ub 
 |-  ( ( F : RR --> ( 0 [,] +oo ) /\ ( RR X. { 0 } ) e. dom S.1 /\ ( RR X. { 0 } ) oR <_ F ) -> ( S.1 ` ( RR X. { 0 } ) ) <_ ( S.2 ` F ) )
25 23 24 mp3an2 
 |-  ( ( F : RR --> ( 0 [,] +oo ) /\ ( RR X. { 0 } ) oR <_ F ) -> ( S.1 ` ( RR X. { 0 } ) ) <_ ( S.2 ` F ) )
26 22 25 mpdan 
 |-  ( F : RR --> ( 0 [,] +oo ) -> ( S.1 ` ( RR X. { 0 } ) ) <_ ( S.2 ` F ) )
27 1 26 eqbrtrrid 
 |-  ( F : RR --> ( 0 [,] +oo ) -> 0 <_ ( S.2 ` F ) )