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 ⊢φ→∫ABdx≤∫ACdx

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∈ℝ⟼ifx∈A∧0≤BB0∈ℝ∧∫2⁡x∈ℝ⟼ifx∈A∧0≤−B−B0∈ℝ
7 1 6 mpbid ⊢φ→x∈A⟼B∈MblFn∧∫2⁡x∈ℝ⟼ifx∈A∧0≤BB0∈ℝ∧∫2⁡x∈ℝ⟼ifx∈A∧0≤−B−B0∈ℝ
8 7 simp2d ⊢φ→∫2⁡x∈ℝ⟼ifx∈A∧0≤BB0∈ℝ
9 4 iblrelem ⊢φ→x∈A⟼C∈𝐿1↔x∈A⟼C∈MblFn∧∫2⁡x∈ℝ⟼ifx∈A∧0≤CC0∈ℝ∧∫2⁡x∈ℝ⟼ifx∈A∧0≤−C−C0∈ℝ
10 2 9 mpbid ⊢φ→x∈A⟼C∈MblFn∧∫2⁡x∈ℝ⟼ifx∈A∧0≤CC0∈ℝ∧∫2⁡x∈ℝ⟼ifx∈A∧0≤−C−C0∈ℝ
11 10 simp3d ⊢φ→∫2⁡x∈ℝ⟼ifx∈A∧0≤−C−C0∈ℝ
12 10 simp2d ⊢φ→∫2⁡x∈ℝ⟼ifx∈A∧0≤CC0∈ℝ
13 7 simp3d ⊢φ→∫2⁡x∈ℝ⟼ifx∈A∧0≤−B−B0∈ℝ
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∈ℝ→ifx∈A∧0≤BB0∈0+∞
22 21 fmpttd ⊢φ→x∈ℝ⟼ifx∈A∧0≤BB0:ℝ⟶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∈ℝ→ifx∈A∧0≤CC0∈0+∞
30 29 fmpttd ⊢φ→x∈ℝ⟼ifx∈A∧0≤CC0:ℝ⟶0+∞
31 0re ⊢0∈ℝ
32 max1 ⊢0∈ℝ∧C∈ℝ→0≤if0≤CC0
33 31 4 32 sylancr ⊢φ∧x∈A→0≤if0≤CC0
34 ifcl ⊢C∈ℝ∧0∈ℝ→if0≤CC0∈ℝ
35 4 31 34 sylancl ⊢φ∧x∈A→if0≤CC0∈ℝ
36 max2 ⊢0∈ℝ∧C∈ℝ→C≤if0≤CC0
37 31 4 36 sylancr ⊢φ∧x∈A→C≤if0≤CC0
38 3 4 35 5 37 letrd ⊢φ∧x∈A→B≤if0≤CC0
39 maxle ⊢0∈ℝ∧B∈ℝ∧if0≤CC0∈ℝ→if0≤BB0≤if0≤CC0↔0≤if0≤CC0∧B≤if0≤CC0
40 31 3 35 39 mp3an2i ⊢φ∧x∈A→if0≤BB0≤if0≤CC0↔0≤if0≤CC0∧B≤if0≤CC0
41 33 38 40 mpbir2and ⊢φ∧x∈A→if0≤BB0≤if0≤CC0
42 iftrue ⊢x∈A→ifx∈Aif0≤BB00=if0≤BB0
43 42 adantl ⊢φ∧x∈A→ifx∈Aif0≤BB00=if0≤BB0
44 iftrue ⊢x∈A→ifx∈Aif0≤CC00=if0≤CC0
45 44 adantl ⊢φ∧x∈A→ifx∈Aif0≤CC00=if0≤CC0
46 41 43 45 3brtr4d ⊢φ∧x∈A→ifx∈Aif0≤BB00≤ifx∈Aif0≤CC00
47 46 ex ⊢φ→x∈A→ifx∈Aif0≤BB00≤ifx∈Aif0≤CC00
48 0le0 ⊢0≤0
49 48 a1i ⊢¬x∈A→0≤0
50 iffalse ⊢¬x∈A→ifx∈Aif0≤BB00=0
51 iffalse ⊢¬x∈A→ifx∈Aif0≤CC00=0
52 49 50 51 3brtr4d ⊢¬x∈A→ifx∈Aif0≤BB00≤ifx∈Aif0≤CC00
53 47 52 pm2.61d1 ⊢φ→ifx∈Aif0≤BB00≤ifx∈Aif0≤CC00
54 ifan ⊢ifx∈A∧0≤BB0=ifx∈Aif0≤BB00
55 ifan ⊢ifx∈A∧0≤CC0=ifx∈Aif0≤CC00
56 53 54 55 3brtr4g ⊢φ→ifx∈A∧0≤BB0≤ifx∈A∧0≤CC0
57 56 ralrimivw ⊢φ→∀x∈ℝifx∈A∧0≤BB0≤ifx∈A∧0≤CC0
58 reex ⊢ℝ∈V
59 58 a1i ⊢φ→ℝ∈V
60 eqidd ⊢φ→x∈ℝ⟼ifx∈A∧0≤BB0=x∈ℝ⟼ifx∈A∧0≤BB0
61 eqidd ⊢φ→x∈ℝ⟼ifx∈A∧0≤CC0=x∈ℝ⟼ifx∈A∧0≤CC0
62 59 21 29 60 61 ofrfval2 ⊢φ→x∈ℝ⟼ifx∈A∧0≤BB0≤fx∈ℝ⟼ifx∈A∧0≤CC0↔∀x∈ℝifx∈A∧0≤BB0≤ifx∈A∧0≤CC0
63 57 62 mpbird ⊢φ→x∈ℝ⟼ifx∈A∧0≤BB0≤fx∈ℝ⟼ifx∈A∧0≤CC0
64 itg2le ⊢x∈ℝ⟼ifx∈A∧0≤BB0:ℝ⟶0+∞∧x∈ℝ⟼ifx∈A∧0≤CC0:ℝ⟶0+∞∧x∈ℝ⟼ifx∈A∧0≤BB0≤fx∈ℝ⟼ifx∈A∧0≤CC0→∫2⁡x∈ℝ⟼ifx∈A∧0≤BB0≤∫2⁡x∈ℝ⟼ifx∈A∧0≤CC0
65 22 30 63 64 syl3anc ⊢φ→∫2⁡x∈ℝ⟼ifx∈A∧0≤BB0≤∫2⁡x∈ℝ⟼ifx∈A∧0≤CC0
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∈ℝ→ifx∈A∧0≤−C−C0∈0+∞
74 73 fmpttd ⊢φ→x∈ℝ⟼ifx∈A∧0≤−C−C0:ℝ⟶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∈ℝ→ifx∈A∧0≤−B−B0∈0+∞
83 82 fmpttd ⊢φ→x∈ℝ⟼ifx∈A∧0≤−B−B0:ℝ⟶0+∞
84 max1 ⊢0∈ℝ∧−B∈ℝ→0≤if0≤−B−B0
85 31 75 84 sylancr ⊢φ∧x∈A→0≤if0≤−B−B0
86 ifcl ⊢−B∈ℝ∧0∈ℝ→if0≤−B−B0∈ℝ
87 75 31 86 sylancl ⊢φ∧x∈A→if0≤−B−B0∈ℝ
88 3 4 lenegd ⊢φ∧x∈A→B≤C↔−C≤−B
89 5 88 mpbid ⊢φ∧x∈A→−C≤−B
90 max2 ⊢0∈ℝ∧−B∈ℝ→−B≤if0≤−B−B0
91 31 75 90 sylancr ⊢φ∧x∈A→−B≤if0≤−B−B0
92 66 75 87 89 91 letrd ⊢φ∧x∈A→−C≤if0≤−B−B0
93 maxle ⊢0∈ℝ∧−C∈ℝ∧if0≤−B−B0∈ℝ→if0≤−C−C0≤if0≤−B−B0↔0≤if0≤−B−B0∧−C≤if0≤−B−B0
94 31 66 87 93 mp3an2i ⊢φ∧x∈A→if0≤−C−C0≤if0≤−B−B0↔0≤if0≤−B−B0∧−C≤if0≤−B−B0
95 85 92 94 mpbir2and ⊢φ∧x∈A→if0≤−C−C0≤if0≤−B−B0
96 iftrue ⊢x∈A→ifx∈Aif0≤−C−C00=if0≤−C−C0
97 96 adantl ⊢φ∧x∈A→ifx∈Aif0≤−C−C00=if0≤−C−C0
98 iftrue ⊢x∈A→ifx∈Aif0≤−B−B00=if0≤−B−B0
99 98 adantl ⊢φ∧x∈A→ifx∈Aif0≤−B−B00=if0≤−B−B0
100 95 97 99 3brtr4d ⊢φ∧x∈A→ifx∈Aif0≤−C−C00≤ifx∈Aif0≤−B−B00
101 100 ex ⊢φ→x∈A→ifx∈Aif0≤−C−C00≤ifx∈Aif0≤−B−B00
102 iffalse ⊢¬x∈A→ifx∈Aif0≤−C−C00=0
103 iffalse ⊢¬x∈A→ifx∈Aif0≤−B−B00=0
104 49 102 103 3brtr4d ⊢¬x∈A→ifx∈Aif0≤−C−C00≤ifx∈Aif0≤−B−B00
105 101 104 pm2.61d1 ⊢φ→ifx∈Aif0≤−C−C00≤ifx∈Aif0≤−B−B00
106 ifan ⊢ifx∈A∧0≤−C−C0=ifx∈Aif0≤−C−C00
107 ifan ⊢ifx∈A∧0≤−B−B0=ifx∈Aif0≤−B−B00
108 105 106 107 3brtr4g ⊢φ→ifx∈A∧0≤−C−C0≤ifx∈A∧0≤−B−B0
109 108 ralrimivw ⊢φ→∀x∈ℝifx∈A∧0≤−C−C0≤ifx∈A∧0≤−B−B0
110 eqidd ⊢φ→x∈ℝ⟼ifx∈A∧0≤−C−C0=x∈ℝ⟼ifx∈A∧0≤−C−C0
111 eqidd ⊢φ→x∈ℝ⟼ifx∈A∧0≤−B−B0=x∈ℝ⟼ifx∈A∧0≤−B−B0
112 59 73 82 110 111 ofrfval2 ⊢φ→x∈ℝ⟼ifx∈A∧0≤−C−C0≤fx∈ℝ⟼ifx∈A∧0≤−B−B0↔∀x∈ℝifx∈A∧0≤−C−C0≤ifx∈A∧0≤−B−B0
113 109 112 mpbird ⊢φ→x∈ℝ⟼ifx∈A∧0≤−C−C0≤fx∈ℝ⟼ifx∈A∧0≤−B−B0
114 itg2le ⊢x∈ℝ⟼ifx∈A∧0≤−C−C0:ℝ⟶0+∞∧x∈ℝ⟼ifx∈A∧0≤−B−B0:ℝ⟶0+∞∧x∈ℝ⟼ifx∈A∧0≤−C−C0≤fx∈ℝ⟼ifx∈A∧0≤−B−B0→∫2⁡x∈ℝ⟼ifx∈A∧0≤−C−C0≤∫2⁡x∈ℝ⟼ifx∈A∧0≤−B−B0
115 74 83 113 114 syl3anc ⊢φ→∫2⁡x∈ℝ⟼ifx∈A∧0≤−C−C0≤∫2⁡x∈ℝ⟼ifx∈A∧0≤−B−B0
116 8 11 12 13 65 115 le2subd ⊢φ→∫2⁡x∈ℝ⟼ifx∈A∧0≤BB0−∫2⁡x∈ℝ⟼ifx∈A∧0≤−B−B0≤∫2⁡x∈ℝ⟼ifx∈A∧0≤CC0−∫2⁡x∈ℝ⟼ifx∈A∧0≤−C−C0
117 3 1 itgrevallem1 ⊢φ→∫ABdx=∫2⁡x∈ℝ⟼ifx∈A∧0≤BB0−∫2⁡x∈ℝ⟼ifx∈A∧0≤−B−B0
118 4 2 itgrevallem1 ⊢φ→∫ACdx=∫2⁡x∈ℝ⟼ifx∈A∧0≤CC0−∫2⁡x∈ℝ⟼ifx∈A∧0≤−C−C0
119 116 117 118 3brtr4d ⊢φ→∫ABdx≤∫ACdx