Metamath Proof Explorer

Theorem itg1ge0a

Description: The integral of an almost positive simple function is positive. (Contributed by Mario Carneiro, 11-Aug-2014)

Ref Expression
Hypotheses itg10a.1 
|- ( ph -> F e. dom S.1 )
itg10a.2 
|- ( ph -> A C_ RR )
itg10a.3 
|- ( ph -> ( vol* ` A ) = 0 )
itg1ge0a.4 
|- ( ( ph /\ x e. ( RR \ A ) ) -> 0 <_ ( F ` x ) )
Assertion itg1ge0a 
|- ( ph -> 0 <_ ( S.1 ` F ) )

Proof

Step Hyp Ref Expression
1 itg10a.1 
 |-  ( ph -> F e. dom S.1 )
2 itg10a.2 
 |-  ( ph -> A C_ RR )
3 itg10a.3 
 |-  ( ph -> ( vol* ` A ) = 0 )
4 itg1ge0a.4 
 |-  ( ( ph /\ x e. ( RR \ A ) ) -> 0 <_ ( F ` x ) )
5 i1frn 
 |-  ( F e. dom S.1 -> ran F e. Fin )
6 1 5 syl 
 |-  ( ph -> ran F e. Fin )
7 difss 
 |-  ( ran F \ { 0 } ) C_ ran F
8 ssfi 
 |-  ( ( ran F e. Fin /\ ( ran F \ { 0 } ) C_ ran F ) -> ( ran F \ { 0 } ) e. Fin )
9 6 7 8 sylancl 
 |-  ( ph -> ( ran F \ { 0 } ) e. Fin )
10 i1ff 
 |-  ( F e. dom S.1 -> F : RR --> RR )
11 1 10 syl 
 |-  ( ph -> F : RR --> RR )
12 11 frnd 
 |-  ( ph -> ran F C_ RR )
13 12 ssdifssd 
 |-  ( ph -> ( ran F \ { 0 } ) C_ RR )
14 13 sselda 
 |-  ( ( ph /\ k e. ( ran F \ { 0 } ) ) -> k e. RR )
15 i1fima2sn 
 |-  ( ( F e. dom S.1 /\ k e. ( ran F \ { 0 } ) ) -> ( vol ` ( `' F " { k } ) ) e. RR )
16 1 15 sylan 
 |-  ( ( ph /\ k e. ( ran F \ { 0 } ) ) -> ( vol ` ( `' F " { k } ) ) e. RR )
17 14 16 remulcld 
 |-  ( ( ph /\ k e. ( ran F \ { 0 } ) ) -> ( k x. ( vol ` ( `' F " { k } ) ) ) e. RR )
18 0le0 
 |-  0 <_ 0
19 i1fima 
 |-  ( F e. dom S.1 -> ( `' F " { k } ) e. dom vol )
20 1 19 syl 
 |-  ( ph -> ( `' F " { k } ) e. dom vol )
21 mblvol 
 |-  ( ( `' F " { k } ) e. dom vol -> ( vol ` ( `' F " { k } ) ) = ( vol* ` ( `' F " { k } ) ) )
22 20 21 syl 
 |-  ( ph -> ( vol ` ( `' F " { k } ) ) = ( vol* ` ( `' F " { k } ) ) )
23 22 ad2antrr 
 |-  ( ( ( ph /\ k e. ( ran F \ { 0 } ) ) /\ k < 0 ) -> ( vol ` ( `' F " { k } ) ) = ( vol* ` ( `' F " { k } ) ) )
24 11 ffnd 
 |-  ( ph -> F Fn RR )
25 fniniseg 
 |-  ( F Fn RR -> ( x e. ( `' F " { k } ) <-> ( x e. RR /\ ( F ` x ) = k ) ) )
26 24 25 syl 
 |-  ( ph -> ( x e. ( `' F " { k } ) <-> ( x e. RR /\ ( F ` x ) = k ) ) )
27 26 ad2antrr 
 |-  ( ( ( ph /\ k e. ( ran F \ { 0 } ) ) /\ k < 0 ) -> ( x e. ( `' F " { k } ) <-> ( x e. RR /\ ( F ` x ) = k ) ) )
28 simprl 
 |-  ( ( ( ph /\ k e. ( ran F \ { 0 } ) ) /\ ( x e. RR /\ ( F ` x ) = k ) ) -> x e. RR )
29 eldif 
 |-  ( x e. ( RR \ A ) <-> ( x e. RR /\ -. x e. A ) )
30 4 ex 
 |-  ( ph -> ( x e. ( RR \ A ) -> 0 <_ ( F ` x ) ) )
31 30 ad2antrr 
 |-  ( ( ( ph /\ k e. ( ran F \ { 0 } ) ) /\ ( x e. RR /\ ( F ` x ) = k ) ) -> ( x e. ( RR \ A ) -> 0 <_ ( F ` x ) ) )
32 simprr 
 |-  ( ( ( ph /\ k e. ( ran F \ { 0 } ) ) /\ ( x e. RR /\ ( F ` x ) = k ) ) -> ( F ` x ) = k )
33 32 breq2d 
 |-  ( ( ( ph /\ k e. ( ran F \ { 0 } ) ) /\ ( x e. RR /\ ( F ` x ) = k ) ) -> ( 0 <_ ( F ` x ) <-> 0 <_ k ) )
34 0red 
 |-  ( ( ( ph /\ k e. ( ran F \ { 0 } ) ) /\ ( x e. RR /\ ( F ` x ) = k ) ) -> 0 e. RR )
35 14 adantr 
 |-  ( ( ( ph /\ k e. ( ran F \ { 0 } ) ) /\ ( x e. RR /\ ( F ` x ) = k ) ) -> k e. RR )
36 34 35 lenltd 
 |-  ( ( ( ph /\ k e. ( ran F \ { 0 } ) ) /\ ( x e. RR /\ ( F ` x ) = k ) ) -> ( 0 <_ k <-> -. k < 0 ) )
37 33 36 bitrd 
 |-  ( ( ( ph /\ k e. ( ran F \ { 0 } ) ) /\ ( x e. RR /\ ( F ` x ) = k ) ) -> ( 0 <_ ( F ` x ) <-> -. k < 0 ) )
38 31 37 sylibd 
 |-  ( ( ( ph /\ k e. ( ran F \ { 0 } ) ) /\ ( x e. RR /\ ( F ` x ) = k ) ) -> ( x e. ( RR \ A ) -> -. k < 0 ) )
39 29 38 biimtrrid 
 |-  ( ( ( ph /\ k e. ( ran F \ { 0 } ) ) /\ ( x e. RR /\ ( F ` x ) = k ) ) -> ( ( x e. RR /\ -. x e. A ) -> -. k < 0 ) )
40 28 39 mpand 
 |-  ( ( ( ph /\ k e. ( ran F \ { 0 } ) ) /\ ( x e. RR /\ ( F ` x ) = k ) ) -> ( -. x e. A -> -. k < 0 ) )
41 40 con4d 
 |-  ( ( ( ph /\ k e. ( ran F \ { 0 } ) ) /\ ( x e. RR /\ ( F ` x ) = k ) ) -> ( k < 0 -> x e. A ) )
42 41 impancom 
 |-  ( ( ( ph /\ k e. ( ran F \ { 0 } ) ) /\ k < 0 ) -> ( ( x e. RR /\ ( F ` x ) = k ) -> x e. A ) )
43 27 42 sylbid 
 |-  ( ( ( ph /\ k e. ( ran F \ { 0 } ) ) /\ k < 0 ) -> ( x e. ( `' F " { k } ) -> x e. A ) )
44 43 ssrdv 
 |-  ( ( ( ph /\ k e. ( ran F \ { 0 } ) ) /\ k < 0 ) -> ( `' F " { k } ) C_ A )
45 2 ad2antrr 
 |-  ( ( ( ph /\ k e. ( ran F \ { 0 } ) ) /\ k < 0 ) -> A C_ RR )
46 3 ad2antrr 
 |-  ( ( ( ph /\ k e. ( ran F \ { 0 } ) ) /\ k < 0 ) -> ( vol* ` A ) = 0 )
47 ovolssnul 
 |-  ( ( ( `' F " { k } ) C_ A /\ A C_ RR /\ ( vol* ` A ) = 0 ) -> ( vol* ` ( `' F " { k } ) ) = 0 )
48 44 45 46 47 syl3anc 
 |-  ( ( ( ph /\ k e. ( ran F \ { 0 } ) ) /\ k < 0 ) -> ( vol* ` ( `' F " { k } ) ) = 0 )
49 23 48 eqtrd 
 |-  ( ( ( ph /\ k e. ( ran F \ { 0 } ) ) /\ k < 0 ) -> ( vol ` ( `' F " { k } ) ) = 0 )
50 49 oveq2d 
 |-  ( ( ( ph /\ k e. ( ran F \ { 0 } ) ) /\ k < 0 ) -> ( k x. ( vol ` ( `' F " { k } ) ) ) = ( k x. 0 ) )
51 14 recnd 
 |-  ( ( ph /\ k e. ( ran F \ { 0 } ) ) -> k e. CC )
52 51 adantr 
 |-  ( ( ( ph /\ k e. ( ran F \ { 0 } ) ) /\ k < 0 ) -> k e. CC )
53 52 mul01d 
 |-  ( ( ( ph /\ k e. ( ran F \ { 0 } ) ) /\ k < 0 ) -> ( k x. 0 ) = 0 )
54 50 53 eqtrd 
 |-  ( ( ( ph /\ k e. ( ran F \ { 0 } ) ) /\ k < 0 ) -> ( k x. ( vol ` ( `' F " { k } ) ) ) = 0 )
55 18 54 breqtrrid 
 |-  ( ( ( ph /\ k e. ( ran F \ { 0 } ) ) /\ k < 0 ) -> 0 <_ ( k x. ( vol ` ( `' F " { k } ) ) ) )
56 14 adantr 
 |-  ( ( ( ph /\ k e. ( ran F \ { 0 } ) ) /\ 0 <_ k ) -> k e. RR )
57 16 adantr 
 |-  ( ( ( ph /\ k e. ( ran F \ { 0 } ) ) /\ 0 <_ k ) -> ( vol ` ( `' F " { k } ) ) e. RR )
58 simpr 
 |-  ( ( ( ph /\ k e. ( ran F \ { 0 } ) ) /\ 0 <_ k ) -> 0 <_ k )
59 20 ad2antrr 
 |-  ( ( ( ph /\ k e. ( ran F \ { 0 } ) ) /\ 0 <_ k ) -> ( `' F " { k } ) e. dom vol )
60 mblss 
 |-  ( ( `' F " { k } ) e. dom vol -> ( `' F " { k } ) C_ RR )
61 59 60 syl 
 |-  ( ( ( ph /\ k e. ( ran F \ { 0 } ) ) /\ 0 <_ k ) -> ( `' F " { k } ) C_ RR )
62 ovolge0 
 |-  ( ( `' F " { k } ) C_ RR -> 0 <_ ( vol* ` ( `' F " { k } ) ) )
63 61 62 syl 
 |-  ( ( ( ph /\ k e. ( ran F \ { 0 } ) ) /\ 0 <_ k ) -> 0 <_ ( vol* ` ( `' F " { k } ) ) )
64 22 ad2antrr 
 |-  ( ( ( ph /\ k e. ( ran F \ { 0 } ) ) /\ 0 <_ k ) -> ( vol ` ( `' F " { k } ) ) = ( vol* ` ( `' F " { k } ) ) )
65 63 64 breqtrrd 
 |-  ( ( ( ph /\ k e. ( ran F \ { 0 } ) ) /\ 0 <_ k ) -> 0 <_ ( vol ` ( `' F " { k } ) ) )
66 56 57 58 65 mulge0d 
 |-  ( ( ( ph /\ k e. ( ran F \ { 0 } ) ) /\ 0 <_ k ) -> 0 <_ ( k x. ( vol ` ( `' F " { k } ) ) ) )
67 0red 
 |-  ( ( ph /\ k e. ( ran F \ { 0 } ) ) -> 0 e. RR )
68 55 66 14 67 ltlecasei 
 |-  ( ( ph /\ k e. ( ran F \ { 0 } ) ) -> 0 <_ ( k x. ( vol ` ( `' F " { k } ) ) ) )
69 9 17 68 fsumge0 
 |-  ( ph -> 0 <_ sum_ k e. ( ran F \ { 0 } ) ( k x. ( vol ` ( `' F " { k } ) ) ) )
70 itg1val 
 |-  ( F e. dom S.1 -> ( S.1 ` F ) = sum_ k e. ( ran F \ { 0 } ) ( k x. ( vol ` ( `' F " { k } ) ) ) )
71 1 70 syl 
 |-  ( ph -> ( S.1 ` F ) = sum_ k e. ( ran F \ { 0 } ) ( k x. ( vol ` ( `' F " { k } ) ) ) )
72 69 71 breqtrrd 
 |-  ( ph -> 0 <_ ( S.1 ` F ) )