Metamath Proof Explorer

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⁡A
itggt0.2 ⊢φ→x∈A⟼B∈𝐿1
itggt0.3 ⊢φ∧x∈A→B∈ℝ+
Assertion itggt0 ⊢φ→0<∫ABdx

Proof

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