This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ‘ 𝐴 ) )
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 𝑥 )