Metamath Proof Explorer

Theorem itgle

Description: Monotonicity of an integral. (Contributed by Mario Carneiro, 11-Aug-2014)

Ref Expression
Hypotheses itgle.1 ⊢ φ → x ∈ A ⟼ B ∈ 𝐿 1
itgle.2 ⊢ φ → x ∈ A ⟼ C ∈ 𝐿 1
itgle.3 ⊢ φ ∧ x ∈ A → B ∈ ℝ
itgle.4 ⊢ φ ∧ x ∈ A → C ∈ ℝ
itgle.5 ⊢ φ ∧ x ∈ A → B ≤ C
Assertion itgle ⊢ φ → ∫ A B dx ≤ ∫ A C dx

Proof

Step Hyp Ref Expression
1 itgle.1 ⊢ φ → x ∈ A ⟼ B ∈ 𝐿 1
2 itgle.2 ⊢ φ → x ∈ A ⟼ C ∈ 𝐿 1
3 itgle.3 ⊢ φ ∧ x ∈ A → B ∈ ℝ
4 itgle.4 ⊢ φ ∧ x ∈ A → C ∈ ℝ
5 itgle.5 ⊢ φ ∧ x ∈ A → B ≤ C
6 3 iblrelem ⊢ φ → x ∈ A ⟼ B ∈ 𝐿 1 ↔ x ∈ A ⟼ B ∈ MblFn ∧ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ B B 0 ∈ ℝ ∧ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ − B − B 0 ∈ ℝ
7 1 6 mpbid ⊢ φ → x ∈ A ⟼ B ∈ MblFn ∧ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ B B 0 ∈ ℝ ∧ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ − B − B 0 ∈ ℝ
8 7 simp2d ⊢ φ → ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ B B 0 ∈ ℝ
9 4 iblrelem ⊢ φ → x ∈ A ⟼ C ∈ 𝐿 1 ↔ x ∈ A ⟼ C ∈ MblFn ∧ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ C C 0 ∈ ℝ ∧ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ − C − C 0 ∈ ℝ
10 2 9 mpbid ⊢ φ → x ∈ A ⟼ C ∈ MblFn ∧ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ C C 0 ∈ ℝ ∧ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ − C − C 0 ∈ ℝ
11 10 simp3d ⊢ φ → ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ − C − C 0 ∈ ℝ
12 10 simp2d ⊢ φ → ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ C C 0 ∈ ℝ
13 7 simp3d ⊢ φ → ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ − B − B 0 ∈ ℝ
14 3 ad2ant2r ⊢ φ ∧ x ∈ ℝ ∧ x ∈ A ∧ 0 ≤ B → B ∈ ℝ
15 14 rexrd ⊢ φ ∧ x ∈ ℝ ∧ x ∈ A ∧ 0 ≤ B → B ∈ ℝ *
16 simprr ⊢ φ ∧ x ∈ ℝ ∧ x ∈ A ∧ 0 ≤ B → 0 ≤ B
17 elxrge0 ⊢ B ∈ 0 +∞ ↔ B ∈ ℝ * ∧ 0 ≤ B
18 15 16 17 sylanbrc ⊢ φ ∧ x ∈ ℝ ∧ x ∈ A ∧ 0 ≤ B → B ∈ 0 +∞
19 0e0iccpnf ⊢ 0 ∈ 0 +∞
20 19 a1i ⊢ φ ∧ x ∈ ℝ ∧ ¬ x ∈ A ∧ 0 ≤ B → 0 ∈ 0 +∞
21 18 20 ifclda ⊢ φ ∧ x ∈ ℝ → if x ∈ A ∧ 0 ≤ B B 0 ∈ 0 +∞
22 21 fmpttd ⊢ φ → x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ B B 0 : ℝ ⟶ 0 +∞
23 4 ad2ant2r ⊢ φ ∧ x ∈ ℝ ∧ x ∈ A ∧ 0 ≤ C → C ∈ ℝ
24 23 rexrd ⊢ φ ∧ x ∈ ℝ ∧ x ∈ A ∧ 0 ≤ C → C ∈ ℝ *
25 simprr ⊢ φ ∧ x ∈ ℝ ∧ x ∈ A ∧ 0 ≤ C → 0 ≤ C
26 elxrge0 ⊢ C ∈ 0 +∞ ↔ C ∈ ℝ * ∧ 0 ≤ C
27 24 25 26 sylanbrc ⊢ φ ∧ x ∈ ℝ ∧ x ∈ A ∧ 0 ≤ C → C ∈ 0 +∞
28 19 a1i ⊢ φ ∧ x ∈ ℝ ∧ ¬ x ∈ A ∧ 0 ≤ C → 0 ∈ 0 +∞
29 27 28 ifclda ⊢ φ ∧ x ∈ ℝ → if x ∈ A ∧ 0 ≤ C C 0 ∈ 0 +∞
30 29 fmpttd ⊢ φ → x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ C C 0 : ℝ ⟶ 0 +∞
31 0re ⊢ 0 ∈ ℝ
32 max1 ⊢ 0 ∈ ℝ ∧ C ∈ ℝ → 0 ≤ if 0 ≤ C C 0
33 31 4 32 sylancr ⊢ φ ∧ x ∈ A → 0 ≤ if 0 ≤ C C 0
34 ifcl ⊢ C ∈ ℝ ∧ 0 ∈ ℝ → if 0 ≤ C C 0 ∈ ℝ
35 4 31 34 sylancl ⊢ φ ∧ x ∈ A → if 0 ≤ C C 0 ∈ ℝ
36 max2 ⊢ 0 ∈ ℝ ∧ C ∈ ℝ → C ≤ if 0 ≤ C C 0
37 31 4 36 sylancr ⊢ φ ∧ x ∈ A → C ≤ if 0 ≤ C C 0
38 3 4 35 5 37 letrd ⊢ φ ∧ x ∈ A → B ≤ if 0 ≤ C C 0
39 maxle ⊢ 0 ∈ ℝ ∧ B ∈ ℝ ∧ if 0 ≤ C C 0 ∈ ℝ → if 0 ≤ B B 0 ≤ if 0 ≤ C C 0 ↔ 0 ≤ if 0 ≤ C C 0 ∧ B ≤ if 0 ≤ C C 0
40 31 3 35 39 mp3an2i ⊢ φ ∧ x ∈ A → if 0 ≤ B B 0 ≤ if 0 ≤ C C 0 ↔ 0 ≤ if 0 ≤ C C 0 ∧ B ≤ if 0 ≤ C C 0
41 33 38 40 mpbir2and ⊢ φ ∧ x ∈ A → if 0 ≤ B B 0 ≤ if 0 ≤ C C 0
42 iftrue ⊢ x ∈ A → if x ∈ A if 0 ≤ B B 0 0 = if 0 ≤ B B 0
43 42 adantl ⊢ φ ∧ x ∈ A → if x ∈ A if 0 ≤ B B 0 0 = if 0 ≤ B B 0
44 iftrue ⊢ x ∈ A → if x ∈ A if 0 ≤ C C 0 0 = if 0 ≤ C C 0
45 44 adantl ⊢ φ ∧ x ∈ A → if x ∈ A if 0 ≤ C C 0 0 = if 0 ≤ C C 0
46 41 43 45 3brtr4d ⊢ φ ∧ x ∈ A → if x ∈ A if 0 ≤ B B 0 0 ≤ if x ∈ A if 0 ≤ C C 0 0
47 46 ex ⊢ φ → x ∈ A → if x ∈ A if 0 ≤ B B 0 0 ≤ if x ∈ A if 0 ≤ C C 0 0
48 0le0 ⊢ 0 ≤ 0
49 48 a1i ⊢ ¬ x ∈ A → 0 ≤ 0
50 iffalse ⊢ ¬ x ∈ A → if x ∈ A if 0 ≤ B B 0 0 = 0
51 iffalse ⊢ ¬ x ∈ A → if x ∈ A if 0 ≤ C C 0 0 = 0
52 49 50 51 3brtr4d ⊢ ¬ x ∈ A → if x ∈ A if 0 ≤ B B 0 0 ≤ if x ∈ A if 0 ≤ C C 0 0
53 47 52 pm2.61d1 ⊢ φ → if x ∈ A if 0 ≤ B B 0 0 ≤ if x ∈ A if 0 ≤ C C 0 0
54 ifan ⊢ if x ∈ A ∧ 0 ≤ B B 0 = if x ∈ A if 0 ≤ B B 0 0
55 ifan ⊢ if x ∈ A ∧ 0 ≤ C C 0 = if x ∈ A if 0 ≤ C C 0 0
56 53 54 55 3brtr4g ⊢ φ → if x ∈ A ∧ 0 ≤ B B 0 ≤ if x ∈ A ∧ 0 ≤ C C 0
57 56 ralrimivw ⊢ φ → ∀ x ∈ ℝ if x ∈ A ∧ 0 ≤ B B 0 ≤ if x ∈ A ∧ 0 ≤ C C 0
58 reex ⊢ ℝ ∈ V
59 58 a1i ⊢ φ → ℝ ∈ V
60 eqidd ⊢ φ → x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ B B 0 = x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ B B 0
61 eqidd ⊢ φ → x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ C C 0 = x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ C C 0
62 59 21 29 60 61 ofrfval2 ⊢ φ → x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ B B 0 ≤ f x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ C C 0 ↔ ∀ x ∈ ℝ if x ∈ A ∧ 0 ≤ B B 0 ≤ if x ∈ A ∧ 0 ≤ C C 0
63 57 62 mpbird ⊢ φ → x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ B B 0 ≤ f x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ C C 0
64 itg2le ⊢ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ B B 0 : ℝ ⟶ 0 +∞ ∧ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ C C 0 : ℝ ⟶ 0 +∞ ∧ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ B B 0 ≤ f x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ C C 0 → ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ B B 0 ≤ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ C C 0
65 22 30 63 64 syl3anc ⊢ φ → ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ B B 0 ≤ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ C C 0
66 4 renegcld ⊢ φ ∧ x ∈ A → − C ∈ ℝ
67 66 ad2ant2r ⊢ φ ∧ x ∈ ℝ ∧ x ∈ A ∧ 0 ≤ − C → − C ∈ ℝ
68 67 rexrd ⊢ φ ∧ x ∈ ℝ ∧ x ∈ A ∧ 0 ≤ − C → − C ∈ ℝ *
69 simprr ⊢ φ ∧ x ∈ ℝ ∧ x ∈ A ∧ 0 ≤ − C → 0 ≤ − C
70 elxrge0 ⊢ − C ∈ 0 +∞ ↔ − C ∈ ℝ * ∧ 0 ≤ − C
71 68 69 70 sylanbrc ⊢ φ ∧ x ∈ ℝ ∧ x ∈ A ∧ 0 ≤ − C → − C ∈ 0 +∞
72 19 a1i ⊢ φ ∧ x ∈ ℝ ∧ ¬ x ∈ A ∧ 0 ≤ − C → 0 ∈ 0 +∞
73 71 72 ifclda ⊢ φ ∧ x ∈ ℝ → if x ∈ A ∧ 0 ≤ − C − C 0 ∈ 0 +∞
74 73 fmpttd ⊢ φ → x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ − C − C 0 : ℝ ⟶ 0 +∞
75 3 renegcld ⊢ φ ∧ x ∈ A → − B ∈ ℝ
76 75 ad2ant2r ⊢ φ ∧ x ∈ ℝ ∧ x ∈ A ∧ 0 ≤ − B → − B ∈ ℝ
77 76 rexrd ⊢ φ ∧ x ∈ ℝ ∧ x ∈ A ∧ 0 ≤ − B → − B ∈ ℝ *
78 simprr ⊢ φ ∧ x ∈ ℝ ∧ x ∈ A ∧ 0 ≤ − B → 0 ≤ − B
79 elxrge0 ⊢ − B ∈ 0 +∞ ↔ − B ∈ ℝ * ∧ 0 ≤ − B
80 77 78 79 sylanbrc ⊢ φ ∧ x ∈ ℝ ∧ x ∈ A ∧ 0 ≤ − B → − B ∈ 0 +∞
81 19 a1i ⊢ φ ∧ x ∈ ℝ ∧ ¬ x ∈ A ∧ 0 ≤ − B → 0 ∈ 0 +∞
82 80 81 ifclda ⊢ φ ∧ x ∈ ℝ → if x ∈ A ∧ 0 ≤ − B − B 0 ∈ 0 +∞
83 82 fmpttd ⊢ φ → x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ − B − B 0 : ℝ ⟶ 0 +∞
84 max1 ⊢ 0 ∈ ℝ ∧ − B ∈ ℝ → 0 ≤ if 0 ≤ − B − B 0
85 31 75 84 sylancr ⊢ φ ∧ x ∈ A → 0 ≤ if 0 ≤ − B − B 0
86 ifcl ⊢ − B ∈ ℝ ∧ 0 ∈ ℝ → if 0 ≤ − B − B 0 ∈ ℝ
87 75 31 86 sylancl ⊢ φ ∧ x ∈ A → if 0 ≤ − B − B 0 ∈ ℝ
88 3 4 lenegd ⊢ φ ∧ x ∈ A → B ≤ C ↔ − C ≤ − B
89 5 88 mpbid ⊢ φ ∧ x ∈ A → − C ≤ − B
90 max2 ⊢ 0 ∈ ℝ ∧ − B ∈ ℝ → − B ≤ if 0 ≤ − B − B 0
91 31 75 90 sylancr ⊢ φ ∧ x ∈ A → − B ≤ if 0 ≤ − B − B 0
92 66 75 87 89 91 letrd ⊢ φ ∧ x ∈ A → − C ≤ if 0 ≤ − B − B 0
93 maxle ⊢ 0 ∈ ℝ ∧ − C ∈ ℝ ∧ if 0 ≤ − B − B 0 ∈ ℝ → if 0 ≤ − C − C 0 ≤ if 0 ≤ − B − B 0 ↔ 0 ≤ if 0 ≤ − B − B 0 ∧ − C ≤ if 0 ≤ − B − B 0
94 31 66 87 93 mp3an2i ⊢ φ ∧ x ∈ A → if 0 ≤ − C − C 0 ≤ if 0 ≤ − B − B 0 ↔ 0 ≤ if 0 ≤ − B − B 0 ∧ − C ≤ if 0 ≤ − B − B 0
95 85 92 94 mpbir2and ⊢ φ ∧ x ∈ A → if 0 ≤ − C − C 0 ≤ if 0 ≤ − B − B 0
96 iftrue ⊢ x ∈ A → if x ∈ A if 0 ≤ − C − C 0 0 = if 0 ≤ − C − C 0
97 96 adantl ⊢ φ ∧ x ∈ A → if x ∈ A if 0 ≤ − C − C 0 0 = if 0 ≤ − C − C 0
98 iftrue ⊢ x ∈ A → if x ∈ A if 0 ≤ − B − B 0 0 = if 0 ≤ − B − B 0
99 98 adantl ⊢ φ ∧ x ∈ A → if x ∈ A if 0 ≤ − B − B 0 0 = if 0 ≤ − B − B 0
100 95 97 99 3brtr4d ⊢ φ ∧ x ∈ A → if x ∈ A if 0 ≤ − C − C 0 0 ≤ if x ∈ A if 0 ≤ − B − B 0 0
101 100 ex ⊢ φ → x ∈ A → if x ∈ A if 0 ≤ − C − C 0 0 ≤ if x ∈ A if 0 ≤ − B − B 0 0
102 iffalse ⊢ ¬ x ∈ A → if x ∈ A if 0 ≤ − C − C 0 0 = 0
103 iffalse ⊢ ¬ x ∈ A → if x ∈ A if 0 ≤ − B − B 0 0 = 0
104 49 102 103 3brtr4d ⊢ ¬ x ∈ A → if x ∈ A if 0 ≤ − C − C 0 0 ≤ if x ∈ A if 0 ≤ − B − B 0 0
105 101 104 pm2.61d1 ⊢ φ → if x ∈ A if 0 ≤ − C − C 0 0 ≤ if x ∈ A if 0 ≤ − B − B 0 0
106 ifan ⊢ if x ∈ A ∧ 0 ≤ − C − C 0 = if x ∈ A if 0 ≤ − C − C 0 0
107 ifan ⊢ if x ∈ A ∧ 0 ≤ − B − B 0 = if x ∈ A if 0 ≤ − B − B 0 0
108 105 106 107 3brtr4g ⊢ φ → if x ∈ A ∧ 0 ≤ − C − C 0 ≤ if x ∈ A ∧ 0 ≤ − B − B 0
109 108 ralrimivw ⊢ φ → ∀ x ∈ ℝ if x ∈ A ∧ 0 ≤ − C − C 0 ≤ if x ∈ A ∧ 0 ≤ − B − B 0
110 eqidd ⊢ φ → x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ − C − C 0 = x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ − C − C 0
111 eqidd ⊢ φ → x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ − B − B 0 = x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ − B − B 0
112 59 73 82 110 111 ofrfval2 ⊢ φ → x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ − C − C 0 ≤ f x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ − B − B 0 ↔ ∀ x ∈ ℝ if x ∈ A ∧ 0 ≤ − C − C 0 ≤ if x ∈ A ∧ 0 ≤ − B − B 0
113 109 112 mpbird ⊢ φ → x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ − C − C 0 ≤ f x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ − B − B 0
114 itg2le ⊢ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ − C − C 0 : ℝ ⟶ 0 +∞ ∧ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ − B − B 0 : ℝ ⟶ 0 +∞ ∧ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ − C − C 0 ≤ f x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ − B − B 0 → ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ − C − C 0 ≤ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ − B − B 0
115 74 83 113 114 syl3anc ⊢ φ → ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ − C − C 0 ≤ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ − B − B 0
116 8 11 12 13 65 115 le2subd ⊢ φ → ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ B B 0 − ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ − B − B 0 ≤ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ C C 0 − ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ − C − C 0
117 3 1 itgrevallem1 ⊢ φ → ∫ A B dx = ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ B B 0 − ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ − B − B 0
118 4 2 itgrevallem1 ⊢ φ → ∫ A C dx = ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ C C 0 − ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ − C − C 0
119 116 117 118 3brtr4d ⊢ φ → ∫ A B dx ≤ ∫ A C dx