Metamath Proof Explorer

Theorem itggt0cn

Description: itggt0 holds for continuous functions in the absence of ax-cc . (Contributed by Brendan Leahy, 16-Nov-2017)

Ref Expression
Hypotheses itggt0cn.1 
|- ( ph -> X < Y )
itggt0cn.2 
|- ( ph -> ( x e. ( X (,) Y ) |-> B ) e. L^1 )
itggt0cn.3 
|- ( ( ph /\ x e. ( X (,) Y ) ) -> B e. RR+ )
itggt0cn.cn 
|- ( ph -> ( x e. ( X (,) Y ) |-> B ) e. ( ( X (,) Y ) -cn-> CC ) )
Assertion itggt0cn 
|- ( ph -> 0 < S. ( X (,) Y ) B _d x )

Proof

Step Hyp Ref Expression
1 itggt0cn.1 
 |-  ( ph -> X < Y )
2 itggt0cn.2 
 |-  ( ph -> ( x e. ( X (,) Y ) |-> B ) e. L^1 )
3 itggt0cn.3 
 |-  ( ( ph /\ x e. ( X (,) Y ) ) -> B e. RR+ )
4 itggt0cn.cn 
 |-  ( ph -> ( x e. ( X (,) Y ) |-> B ) e. ( ( X (,) Y ) -cn-> CC ) )
5 3 rpred 
 |-  ( ( ph /\ x e. ( X (,) Y ) ) -> B e. RR )
6 3 rpge0d 
 |-  ( ( ph /\ x e. ( X (,) Y ) ) -> 0 <_ B )
7 elrege0 
 |-  ( B e. ( 0 [,) +oo ) <-> ( B e. RR /\ 0 <_ B ) )
8 5 6 7 sylanbrc 
 |-  ( ( ph /\ x e. ( X (,) Y ) ) -> B e. ( 0 [,) +oo ) )
9 0e0icopnf 
 |-  0 e. ( 0 [,) +oo )
10 9 a1i 
 |-  ( ( ph /\ -. x e. ( X (,) Y ) ) -> 0 e. ( 0 [,) +oo ) )
11 8 10 ifclda 
 |-  ( ph -> if ( x e. ( X (,) Y ) , B , 0 ) e. ( 0 [,) +oo ) )
12 11 adantr 
 |-  ( ( ph /\ x e. RR ) -> if ( x e. ( X (,) Y ) , B , 0 ) e. ( 0 [,) +oo ) )
13 12 fmpttd 
 |-  ( ph -> ( x e. RR |-> if ( x e. ( X (,) Y ) , B , 0 ) ) : RR --> ( 0 [,) +oo ) )
14 3 rpgt0d 
 |-  ( ( ph /\ x e. ( X (,) Y ) ) -> 0 < B )
15 elioore 
 |-  ( x e. ( X (,) Y ) -> x e. RR )
16 15 adantl 
 |-  ( ( ph /\ x e. ( X (,) Y ) ) -> x e. RR )
17 iftrue 
 |-  ( x e. ( X (,) Y ) -> if ( x e. ( X (,) Y ) , B , 0 ) = B )
18 17 adantl 
 |-  ( ( ph /\ x e. ( X (,) Y ) ) -> if ( x e. ( X (,) Y ) , B , 0 ) = B )
19 18 3 eqeltrd 
 |-  ( ( ph /\ x e. ( X (,) Y ) ) -> if ( x e. ( X (,) Y ) , B , 0 ) e. RR+ )
20 eqid 
 |-  ( x e. RR |-> if ( x e. ( X (,) Y ) , B , 0 ) ) = ( x e. RR |-> if ( x e. ( X (,) Y ) , B , 0 ) )
21 20 fvmpt2 
 |-  ( ( x e. RR /\ if ( x e. ( X (,) Y ) , B , 0 ) e. RR+ ) -> ( ( x e. RR |-> if ( x e. ( X (,) Y ) , B , 0 ) ) ` x ) = if ( x e. ( X (,) Y ) , B , 0 ) )
22 16 19 21 syl2anc 
 |-  ( ( ph /\ x e. ( X (,) Y ) ) -> ( ( x e. RR |-> if ( x e. ( X (,) Y ) , B , 0 ) ) ` x ) = if ( x e. ( X (,) Y ) , B , 0 ) )
23 22 18 eqtrd 
 |-  ( ( ph /\ x e. ( X (,) Y ) ) -> ( ( x e. RR |-> if ( x e. ( X (,) Y ) , B , 0 ) ) ` x ) = B )
24 14 23 breqtrrd 
 |-  ( ( ph /\ x e. ( X (,) Y ) ) -> 0 < ( ( x e. RR |-> if ( x e. ( X (,) Y ) , B , 0 ) ) ` x ) )
25 24 ralrimiva 
 |-  ( ph -> A. x e. ( X (,) Y ) 0 < ( ( x e. RR |-> if ( x e. ( X (,) Y ) , B , 0 ) ) ` x ) )
26 nfcv 
 |-  F/_ x 0
27 nfcv 
 |-  F/_ x <
28 nffvmpt1 
 |-  F/_ x ( ( x e. RR |-> if ( x e. ( X (,) Y ) , B , 0 ) ) ` y )
29 26 27 28 nfbr 
 |-  F/ x 0 < ( ( x e. RR |-> if ( x e. ( X (,) Y ) , B , 0 ) ) ` y )
30 nfv 
 |-  F/ y 0 < ( ( x e. RR |-> if ( x e. ( X (,) Y ) , B , 0 ) ) ` x )
31 fveq2 
 |-  ( y = x -> ( ( x e. RR |-> if ( x e. ( X (,) Y ) , B , 0 ) ) ` y ) = ( ( x e. RR |-> if ( x e. ( X (,) Y ) , B , 0 ) ) ` x ) )
32 31 breq2d 
 |-  ( y = x -> ( 0 < ( ( x e. RR |-> if ( x e. ( X (,) Y ) , B , 0 ) ) ` y ) <-> 0 < ( ( x e. RR |-> if ( x e. ( X (,) Y ) , B , 0 ) ) ` x ) ) )
33 29 30 32 cbvralw 
 |-  ( A. y e. ( X (,) Y ) 0 < ( ( x e. RR |-> if ( x e. ( X (,) Y ) , B , 0 ) ) ` y ) <-> A. x e. ( X (,) Y ) 0 < ( ( x e. RR |-> if ( x e. ( X (,) Y ) , B , 0 ) ) ` x ) )
34 25 33 sylibr 
 |-  ( ph -> A. y e. ( X (,) Y ) 0 < ( ( x e. RR |-> if ( x e. ( X (,) Y ) , B , 0 ) ) ` y ) )
35 34 r19.21bi 
 |-  ( ( ph /\ y e. ( X (,) Y ) ) -> 0 < ( ( x e. RR |-> if ( x e. ( X (,) Y ) , B , 0 ) ) ` y ) )
36 ioossre 
 |-  ( X (,) Y ) C_ RR
37 resmpt 
 |-  ( ( X (,) Y ) C_ RR -> ( ( x e. RR |-> if ( x e. ( X (,) Y ) , B , 0 ) ) |` ( X (,) Y ) ) = ( x e. ( X (,) Y ) |-> if ( x e. ( X (,) Y ) , B , 0 ) ) )
38 36 37 ax-mp 
 |-  ( ( x e. RR |-> if ( x e. ( X (,) Y ) , B , 0 ) ) |` ( X (,) Y ) ) = ( x e. ( X (,) Y ) |-> if ( x e. ( X (,) Y ) , B , 0 ) )
39 17 mpteq2ia 
 |-  ( x e. ( X (,) Y ) |-> if ( x e. ( X (,) Y ) , B , 0 ) ) = ( x e. ( X (,) Y ) |-> B )
40 38 39 eqtri 
 |-  ( ( x e. RR |-> if ( x e. ( X (,) Y ) , B , 0 ) ) |` ( X (,) Y ) ) = ( x e. ( X (,) Y ) |-> B )
41 40 4 eqeltrid 
 |-  ( ph -> ( ( x e. RR |-> if ( x e. ( X (,) Y ) , B , 0 ) ) |` ( X (,) Y ) ) e. ( ( X (,) Y ) -cn-> CC ) )
42 1 13 35 41 itg2gt0cn 
 |-  ( ph -> 0 < ( S.2 ` ( x e. RR |-> if ( x e. ( X (,) Y ) , B , 0 ) ) ) )
43 5 2 6 itgposval 
 |-  ( ph -> S. ( X (,) Y ) B _d x = ( S.2 ` ( x e. RR |-> if ( x e. ( X (,) Y ) , B , 0 ) ) ) )
44 42 43 breqtrrd 
 |-  ( ph -> 0 < S. ( X (,) Y ) B _d x )