Metamath Proof Explorer

Theorem itgless

Description: Expand the integral of a nonnegative function. (Contributed by Mario Carneiro, 31-Aug-2014)

Ref Expression
Hypotheses itgless.1 ⊢ ( 𝜑 → 𝐴 ⊆ 𝐵 )
itgless.2 ⊢ ( 𝜑 → 𝐴 ∈ dom vol )
itgless.3 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝐶 ∈ ℝ )
itgless.4 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 0 ≤ 𝐶 )
itgless.5 ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) ∈ 𝐿1 )
Assertion itgless ( 𝜑 → ∫ 𝐴 𝐶 d 𝑥 ≤ ∫ 𝐵 𝐶 d 𝑥 )

Proof

Step Hyp Ref Expression
1 itgless.1 ⊢ ( 𝜑 → 𝐴 ⊆ 𝐵 )
2 itgless.2 ⊢ ( 𝜑 → 𝐴 ∈ dom vol )
3 itgless.3 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝐶 ∈ ℝ )
4 itgless.4 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 0 ≤ 𝐶 )
5 itgless.5 ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) ∈ 𝐿1 )
6 itgss2 ⊢ ( 𝐴 ⊆ 𝐵 → ∫ 𝐴 𝐶 d 𝑥 = ∫ 𝐵 if ( 𝑥 ∈ 𝐴 , 𝐶 , 0 ) d 𝑥 )
7 1 6 syl ⊢ ( 𝜑 → ∫ 𝐴 𝐶 d 𝑥 = ∫ 𝐵 if ( 𝑥 ∈ 𝐴 , 𝐶 , 0 ) d 𝑥 )
8 iblmbf ⊢ ( ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) ∈ 𝐿1 → ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) ∈ MblFn )
9 5 8 syl ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) ∈ MblFn )
10 9 3 mbfdm2 ⊢ ( 𝜑 → 𝐵 ∈ dom vol )
11 1 sselda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ 𝐵 )
12 11 3 syldan ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ ℝ )
13 0re ⊢ 0 ∈ ℝ
14 ifcl ⊢ ( ( 𝐶 ∈ ℝ ∧ 0 ∈ ℝ ) → if ( 𝑥 ∈ 𝐴 , 𝐶 , 0 ) ∈ ℝ )
15 12 13 14 sylancl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → if ( 𝑥 ∈ 𝐴 , 𝐶 , 0 ) ∈ ℝ )
16 eldifn ⊢ ( 𝑥 ∈ ( 𝐵 ∖ 𝐴 ) → ¬ 𝑥 ∈ 𝐴 )
17 16 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐵 ∖ 𝐴 ) ) → ¬ 𝑥 ∈ 𝐴 )
18 17 iffalsed ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐵 ∖ 𝐴 ) ) → if ( 𝑥 ∈ 𝐴 , 𝐶 , 0 ) = 0 )
19 iftrue ⊢ ( 𝑥 ∈ 𝐴 → if ( 𝑥 ∈ 𝐴 , 𝐶 , 0 ) = 𝐶 )
20 19 mpteq2ia ⊢ ( 𝑥 ∈ 𝐴 ↦ if ( 𝑥 ∈ 𝐴 , 𝐶 , 0 ) ) = ( 𝑥 ∈ 𝐴 ↦ 𝐶 )
21 1 2 3 5 iblss ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ∈ 𝐿1 )
22 20 21 eqeltrid ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ if ( 𝑥 ∈ 𝐴 , 𝐶 , 0 ) ) ∈ 𝐿1 )
23 1 10 15 18 22 iblss2 ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 ∈ 𝐴 , 𝐶 , 0 ) ) ∈ 𝐿1 )
24 3 13 14 sylancl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → if ( 𝑥 ∈ 𝐴 , 𝐶 , 0 ) ∈ ℝ )
25 3 leidd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝐶 ≤ 𝐶 )
26 breq1 ⊢ ( 𝐶 = if ( 𝑥 ∈ 𝐴 , 𝐶 , 0 ) → ( 𝐶 ≤ 𝐶 ↔ if ( 𝑥 ∈ 𝐴 , 𝐶 , 0 ) ≤ 𝐶 ) )
27 breq1 ⊢ ( 0 = if ( 𝑥 ∈ 𝐴 , 𝐶 , 0 ) → ( 0 ≤ 𝐶 ↔ if ( 𝑥 ∈ 𝐴 , 𝐶 , 0 ) ≤ 𝐶 ) )
28 26 27 ifboth ⊢ ( ( 𝐶 ≤ 𝐶 ∧ 0 ≤ 𝐶 ) → if ( 𝑥 ∈ 𝐴 , 𝐶 , 0 ) ≤ 𝐶 )
29 25 4 28 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → if ( 𝑥 ∈ 𝐴 , 𝐶 , 0 ) ≤ 𝐶 )
30 23 5 24 3 29 itgle ⊢ ( 𝜑 → ∫ 𝐵 if ( 𝑥 ∈ 𝐴 , 𝐶 , 0 ) d 𝑥 ≤ ∫ 𝐵 𝐶 d 𝑥 )
31 7 30 eqbrtrd ⊢ ( 𝜑 → ∫ 𝐴 𝐶 d 𝑥 ≤ ∫ 𝐵 𝐶 d 𝑥 )