itggt0

Description: The integral of a strictly positive function is positive. (Contributed by Mario Carneiro, 30-Aug-2014)

	Ref	Expression
Hypotheses	itggt0.1	\|- ( ph -> 0 < ( vol ` A ) )
	itggt0.2	\|- ( ph -> ( x e. A \|-> B ) e. L^1 )
	itggt0.3	\|- ( ( ph /\ x e. A ) -> B e. RR+ )
Assertion	itggt0	\|- ( ph -> 0 < S. A B _d x )

Proof

Step	Hyp	Ref	Expression
1		itggt0.1	\|- ( ph -> 0 < ( vol ` A ) )
2		itggt0.2	\|- ( ph -> ( x e. A \|-> B ) e. L^1 )
3		itggt0.3	\|- ( ( ph /\ x e. A ) -> B e. RR+ )
4		iblmbf	\|- ( ( x e. A \|-> B ) e. L^1 -> ( x e. A \|-> B ) e. MblFn )
5	2 4	syl	\|- ( ph -> ( x e. A \|-> B ) e. MblFn )
6	5 3	mbfdm2	\|- ( ph -> A e. dom vol )
7	3	rpred	\|- ( ( ph /\ x e. A ) -> B e. RR )
8	3	rpge0d	\|- ( ( ph /\ x e. A ) -> 0 <_ B )
9		elrege0	\|- ( B e. ( 0 [,) +oo ) <-> ( B e. RR /\ 0 <_ B ) )
10	7 8 9	sylanbrc	\|- ( ( ph /\ x e. A ) -> B e. ( 0 [,) +oo ) )
11		0e0icopnf	\|- 0 e. ( 0 [,) +oo )
12	11	a1i	\|- ( ( ph /\ -. x e. A ) -> 0 e. ( 0 [,) +oo ) )
13	10 12	ifclda	\|- ( ph -> if ( x e. A , B , 0 ) e. ( 0 [,) +oo ) )
14	13	adantr	\|- ( ( ph /\ x e. RR ) -> if ( x e. A , B , 0 ) e. ( 0 [,) +oo ) )
15	14	fmpttd	\|- ( ph -> ( x e. RR \|-> if ( x e. A , B , 0 ) ) : RR --> ( 0 [,) +oo ) )
16		mblss	\|- ( A e. dom vol -> A C_ RR )
17	6 16	syl	\|- ( ph -> A C_ RR )
18		rembl	\|- RR e. dom vol
19	18	a1i	\|- ( ph -> RR e. dom vol )
20	13	adantr	\|- ( ( ph /\ x e. A ) -> if ( x e. A , B , 0 ) e. ( 0 [,) +oo ) )
21		eldifn	\|- ( x e. ( RR \ A ) -> -. x e. A )
22	21	adantl	\|- ( ( ph /\ x e. ( RR \ A ) ) -> -. x e. A )
23	22	iffalsed	\|- ( ( ph /\ x e. ( RR \ A ) ) -> if ( x e. A , B , 0 ) = 0 )
24		iftrue	\|- ( x e. A -> if ( x e. A , B , 0 ) = B )
25	24	mpteq2ia	\|- ( x e. A \|-> if ( x e. A , B , 0 ) ) = ( x e. A \|-> B )
26	25 5	eqeltrid	\|- ( ph -> ( x e. A \|-> if ( x e. A , B , 0 ) ) e. MblFn )
27	17 19 20 23 26	mbfss	\|- ( ph -> ( x e. RR \|-> if ( x e. A , B , 0 ) ) e. MblFn )
28	3	rpgt0d	\|- ( ( ph /\ x e. A ) -> 0 < B )
29	17	sselda	\|- ( ( ph /\ x e. A ) -> x e. RR )
30	24	adantl	\|- ( ( ph /\ x e. A ) -> if ( x e. A , B , 0 ) = B )
31	30 3	eqeltrd	\|- ( ( ph /\ x e. A ) -> if ( x e. A , B , 0 ) e. RR+ )
32		eqid	\|- ( x e. RR \|-> if ( x e. A , B , 0 ) ) = ( x e. RR \|-> if ( x e. A , B , 0 ) )
33	32	fvmpt2	\|- ( ( x e. RR /\ if ( x e. A , B , 0 ) e. RR+ ) -> ( ( x e. RR \|-> if ( x e. A , B , 0 ) ) ` x ) = if ( x e. A , B , 0 ) )
34	29 31 33	syl2anc	\|- ( ( ph /\ x e. A ) -> ( ( x e. RR \|-> if ( x e. A , B , 0 ) ) ` x ) = if ( x e. A , B , 0 ) )
35	34 30	eqtrd	\|- ( ( ph /\ x e. A ) -> ( ( x e. RR \|-> if ( x e. A , B , 0 ) ) ` x ) = B )
36	28 35	breqtrrd	\|- ( ( ph /\ x e. A ) -> 0 < ( ( x e. RR \|-> if ( x e. A , B , 0 ) ) ` x ) )
37	36	ralrimiva	\|- ( ph -> A. x e. A 0 < ( ( x e. RR \|-> if ( x e. A , B , 0 ) ) ` x ) )
38		nfcv	\|- F/_ x 0
39		nfcv	\|- F/_ x <
40		nffvmpt1	\|- F/_ x ( ( x e. RR \|-> if ( x e. A , B , 0 ) ) ` y )
41	38 39 40	nfbr	\|- F/ x 0 < ( ( x e. RR \|-> if ( x e. A , B , 0 ) ) ` y )
42		nfv	\|- F/ y 0 < ( ( x e. RR \|-> if ( x e. A , B , 0 ) ) ` x )
43		fveq2	\|- ( y = x -> ( ( x e. RR \|-> if ( x e. A , B , 0 ) ) ` y ) = ( ( x e. RR \|-> if ( x e. A , B , 0 ) ) ` x ) )
44	43	breq2d	\|- ( y = x -> ( 0 < ( ( x e. RR \|-> if ( x e. A , B , 0 ) ) ` y ) <-> 0 < ( ( x e. RR \|-> if ( x e. A , B , 0 ) ) ` x ) ) )
45	41 42 44	cbvralw	\|- ( A. y e. A 0 < ( ( x e. RR \|-> if ( x e. A , B , 0 ) ) ` y ) <-> A. x e. A 0 < ( ( x e. RR \|-> if ( x e. A , B , 0 ) ) ` x ) )
46	37 45	sylibr	\|- ( ph -> A. y e. A 0 < ( ( x e. RR \|-> if ( x e. A , B , 0 ) ) ` y ) )
47	46	r19.21bi	\|- ( ( ph /\ y e. A ) -> 0 < ( ( x e. RR \|-> if ( x e. A , B , 0 ) ) ` y ) )
48	6 1 15 27 47	itg2gt0	\|- ( ph -> 0 < ( S.2 ` ( x e. RR \|-> if ( x e. A , B , 0 ) ) ) )
49	7 2 8	itgposval	\|- ( ph -> S. A B _d x = ( S.2 ` ( x e. RR \|-> if ( x e. A , B , 0 ) ) ) )
50	48 49	breqtrrd	\|- ( ph -> 0 < S. A B _d x )

Metamath Proof Explorer

Theorem itggt0

Proof