Theorem itggt0

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

	Ref	Expression
Hypotheses	itggt0.1	⊢ ( 𝜑 → 0 < ( vol ‘ 𝐴 ) )
	itggt0.2	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ 𝐿1 )
	itggt0.3	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ+ )
Assertion	itggt0	⊢ ( 𝜑 → 0 < ∫ 𝐴 𝐵 d 𝑥 )

Proof

Step	Hyp	Ref	Expression
1		itggt0.1	⊢ ( 𝜑 → 0 < ( vol ‘ 𝐴 ) )
2		itggt0.2	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ 𝐿1 )
3		itggt0.3	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ+ )
4		iblmbf	⊢ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ 𝐿1 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ MblFn )
5	2 4	syl	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ MblFn )
6	5 3	mbfdm2	⊢ ( 𝜑 → 𝐴 ∈ dom vol )
7	3	rpred	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ )
8	3	rpge0d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 0 ≤ 𝐵 )
9		elrege0	⊢ ( 𝐵 ∈ ( 0 [,) +∞ ) ↔ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) )
10	7 8 9	sylanbrc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ( 0 [,) +∞ ) )
11		0e0icopnf	⊢ 0 ∈ ( 0 [,) +∞ )
12	11	a1i	⊢ ( ( 𝜑 ∧ ¬ 𝑥 ∈ 𝐴 ) → 0 ∈ ( 0 [,) +∞ ) )
13	10 12	ifclda	⊢ ( 𝜑 → if ( 𝑥 ∈ 𝐴 , 𝐵 , 0 ) ∈ ( 0 [,) +∞ ) )
14	13	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → if ( 𝑥 ∈ 𝐴 , 𝐵 , 0 ) ∈ ( 0 [,) +∞ ) )
15	14	fmpttd	⊢ ( 𝜑 → ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , 𝐵 , 0 ) ) : ℝ ⟶ ( 0 [,) +∞ ) )
16		mblss	⊢ ( 𝐴 ∈ dom vol → 𝐴 ⊆ ℝ )
17	6 16	syl	⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
18		rembl	⊢ ℝ ∈ dom vol
19	18	a1i	⊢ ( 𝜑 → ℝ ∈ dom vol )
20	13	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → if ( 𝑥 ∈ 𝐴 , 𝐵 , 0 ) ∈ ( 0 [,) +∞ ) )
21		eldifn	⊢ ( 𝑥 ∈ ( ℝ ∖ 𝐴 ) → ¬ 𝑥 ∈ 𝐴 )
22	21	adantl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ℝ ∖ 𝐴 ) ) → ¬ 𝑥 ∈ 𝐴 )
23	22	iffalsed	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ℝ ∖ 𝐴 ) ) → if ( 𝑥 ∈ 𝐴 , 𝐵 , 0 ) = 0 )
24		iftrue	⊢ ( 𝑥 ∈ 𝐴 → if ( 𝑥 ∈ 𝐴 , 𝐵 , 0 ) = 𝐵 )
25	24	mpteq2ia	⊢ ( 𝑥 ∈ 𝐴 ↦ if ( 𝑥 ∈ 𝐴 , 𝐵 , 0 ) ) = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
26	25 5	eqeltrid	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ if ( 𝑥 ∈ 𝐴 , 𝐵 , 0 ) ) ∈ MblFn )
27	17 19 20 23 26	mbfss	⊢ ( 𝜑 → ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , 𝐵 , 0 ) ) ∈ MblFn )
28	3	rpgt0d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 0 < 𝐵 )
29	17	sselda	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ ℝ )
30	24	adantl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → if ( 𝑥 ∈ 𝐴 , 𝐵 , 0 ) = 𝐵 )
31	30 3	eqeltrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → if ( 𝑥 ∈ 𝐴 , 𝐵 , 0 ) ∈ ℝ+ )
32		eqid	⊢ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , 𝐵 , 0 ) ) = ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , 𝐵 , 0 ) )
33	32	fvmpt2	⊢ ( ( 𝑥 ∈ ℝ ∧ if ( 𝑥 ∈ 𝐴 , 𝐵 , 0 ) ∈ ℝ+ ) → ( ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , 𝐵 , 0 ) ) ‘ 𝑥 ) = if ( 𝑥 ∈ 𝐴 , 𝐵 , 0 ) )
34	29 31 33	syl2anc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , 𝐵 , 0 ) ) ‘ 𝑥 ) = if ( 𝑥 ∈ 𝐴 , 𝐵 , 0 ) )
35	34 30	eqtrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , 𝐵 , 0 ) ) ‘ 𝑥 ) = 𝐵 )
36	28 35	breqtrrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 0 < ( ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , 𝐵 , 0 ) ) ‘ 𝑥 ) )
37	36	ralrimiva	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 0 < ( ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , 𝐵 , 0 ) ) ‘ 𝑥 ) )
38		nfcv	⊢ Ⅎ 𝑥 0
39		nfcv	⊢ Ⅎ 𝑥 <
40		nffvmpt1	⊢ Ⅎ 𝑥 ( ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , 𝐵 , 0 ) ) ‘ 𝑦 )
41	38 39 40	nfbr	⊢ Ⅎ 𝑥 0 < ( ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , 𝐵 , 0 ) ) ‘ 𝑦 )
42		nfv	⊢ Ⅎ 𝑦 0 < ( ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , 𝐵 , 0 ) ) ‘ 𝑥 )
43		fveq2	⊢ ( 𝑦 = 𝑥 → ( ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , 𝐵 , 0 ) ) ‘ 𝑦 ) = ( ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , 𝐵 , 0 ) ) ‘ 𝑥 ) )
44	43	breq2d	⊢ ( 𝑦 = 𝑥 → ( 0 < ( ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , 𝐵 , 0 ) ) ‘ 𝑦 ) ↔ 0 < ( ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , 𝐵 , 0 ) ) ‘ 𝑥 ) ) )
45	41 42 44	cbvralw	⊢ ( ∀ 𝑦 ∈ 𝐴 0 < ( ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , 𝐵 , 0 ) ) ‘ 𝑦 ) ↔ ∀ 𝑥 ∈ 𝐴 0 < ( ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , 𝐵 , 0 ) ) ‘ 𝑥 ) )
46	37 45	sylibr	⊢ ( 𝜑 → ∀ 𝑦 ∈ 𝐴 0 < ( ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , 𝐵 , 0 ) ) ‘ 𝑦 ) )
47	46	r19.21bi	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → 0 < ( ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , 𝐵 , 0 ) ) ‘ 𝑦 ) )
48	6 1 15 27 47	itg2gt0	⊢ ( 𝜑 → 0 < ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , 𝐵 , 0 ) ) ) )
49	7 2 8	itgposval	⊢ ( 𝜑 → ∫ 𝐴 𝐵 d 𝑥 = ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , 𝐵 , 0 ) ) ) )
50	48 49	breqtrrd	⊢ ( 𝜑 → 0 < ∫ 𝐴 𝐵 d 𝑥 )