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