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 ⊢ φ → A ⊆ B
itgless.2 ⊢ φ → A ∈ dom ⁡ vol
itgless.3 ⊢ φ ∧ x ∈ B → C ∈ ℝ
itgless.4 ⊢ φ ∧ x ∈ B → 0 ≤ C
itgless.5 ⊢ φ → x ∈ B ⟼ C ∈ 𝐿 1
Assertion itgless ⊢ φ → ∫ A C dx ≤ ∫ B C dx

Proof

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