Metamath Proof Explorer

Theorem ibladdnclem

Description: Lemma for ibladdnc ; cf ibladdlem , whose fifth hypothesis is rendered unnecessary by the weakened hypotheses of itg2addnc . (Contributed by Brendan Leahy, 31-Oct-2017)

Ref Expression
Hypotheses ibladdnclem.1 ⊢ φ ∧ x ∈ A → B ∈ ℝ
ibladdnclem.2 ⊢ φ ∧ x ∈ A → C ∈ ℝ
ibladdnclem.3 ⊢ φ ∧ x ∈ A → D = B + C
ibladdnclem.4 ⊢ φ → x ∈ A ⟼ B ∈ MblFn
ibladdnclem.6 ⊢ φ → ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ B B 0 ∈ ℝ
ibladdnclem.7 ⊢ φ → ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ C C 0 ∈ ℝ
Assertion ibladdnclem ⊢ φ → ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ D D 0 ∈ ℝ

Proof

Step Hyp Ref Expression
1 ibladdnclem.1 ⊢ φ ∧ x ∈ A → B ∈ ℝ
2 ibladdnclem.2 ⊢ φ ∧ x ∈ A → C ∈ ℝ
3 ibladdnclem.3 ⊢ φ ∧ x ∈ A → D = B + C
4 ibladdnclem.4 ⊢ φ → x ∈ A ⟼ B ∈ MblFn
5 ibladdnclem.6 ⊢ φ → ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ B B 0 ∈ ℝ
6 ibladdnclem.7 ⊢ φ → ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ C C 0 ∈ ℝ
7 ifan ⊢ if x ∈ A ∧ 0 ≤ D D 0 = if x ∈ A if 0 ≤ D D 0 0
8 1 2 readdcld ⊢ φ ∧ x ∈ A → B + C ∈ ℝ
9 3 8 eqeltrd ⊢ φ ∧ x ∈ A → D ∈ ℝ
10 0re ⊢ 0 ∈ ℝ
11 ifcl ⊢ D ∈ ℝ ∧ 0 ∈ ℝ → if 0 ≤ D D 0 ∈ ℝ
12 9 10 11 sylancl ⊢ φ ∧ x ∈ A → if 0 ≤ D D 0 ∈ ℝ
13 12 rexrd ⊢ φ ∧ x ∈ A → if 0 ≤ D D 0 ∈ ℝ *
14 max1 ⊢ 0 ∈ ℝ ∧ D ∈ ℝ → 0 ≤ if 0 ≤ D D 0
15 10 9 14 sylancr ⊢ φ ∧ x ∈ A → 0 ≤ if 0 ≤ D D 0
16 elxrge0 ⊢ if 0 ≤ D D 0 ∈ 0 +∞ ↔ if 0 ≤ D D 0 ∈ ℝ * ∧ 0 ≤ if 0 ≤ D D 0
17 13 15 16 sylanbrc ⊢ φ ∧ x ∈ A → if 0 ≤ D D 0 ∈ 0 +∞
18 0e0iccpnf ⊢ 0 ∈ 0 +∞
19 18 a1i ⊢ φ ∧ ¬ x ∈ A → 0 ∈ 0 +∞
20 17 19 ifclda ⊢ φ → if x ∈ A if 0 ≤ D D 0 0 ∈ 0 +∞
21 20 adantr ⊢ φ ∧ x ∈ ℝ → if x ∈ A if 0 ≤ D D 0 0 ∈ 0 +∞
22 7 21 eqeltrid ⊢ φ ∧ x ∈ ℝ → if x ∈ A ∧ 0 ≤ D D 0 ∈ 0 +∞
23 22 fmpttd ⊢ φ → x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ D D 0 : ℝ ⟶ 0 +∞
24 reex ⊢ ℝ ∈ V
25 24 a1i ⊢ φ → ℝ ∈ V
26 ifan ⊢ if x ∈ A ∧ 0 ≤ B B 0 = if x ∈ A if 0 ≤ B B 0 0
27 ifcl ⊢ B ∈ ℝ ∧ 0 ∈ ℝ → if 0 ≤ B B 0 ∈ ℝ
28 1 10 27 sylancl ⊢ φ ∧ x ∈ A → if 0 ≤ B B 0 ∈ ℝ
29 10 a1i ⊢ φ ∧ ¬ x ∈ A → 0 ∈ ℝ
30 28 29 ifclda ⊢ φ → if x ∈ A if 0 ≤ B B 0 0 ∈ ℝ
31 26 30 eqeltrid ⊢ φ → if x ∈ A ∧ 0 ≤ B B 0 ∈ ℝ
32 31 adantr ⊢ φ ∧ x ∈ ℝ → if x ∈ A ∧ 0 ≤ B B 0 ∈ ℝ
33 ifan ⊢ if x ∈ A ∧ 0 ≤ C C 0 = if x ∈ A if 0 ≤ C C 0 0
34 ifcl ⊢ C ∈ ℝ ∧ 0 ∈ ℝ → if 0 ≤ C C 0 ∈ ℝ
35 2 10 34 sylancl ⊢ φ ∧ x ∈ A → if 0 ≤ C C 0 ∈ ℝ
36 35 29 ifclda ⊢ φ → if x ∈ A if 0 ≤ C C 0 0 ∈ ℝ
37 33 36 eqeltrid ⊢ φ → if x ∈ A ∧ 0 ≤ C C 0 ∈ ℝ
38 37 adantr ⊢ φ ∧ x ∈ ℝ → if x ∈ A ∧ 0 ≤ C C 0 ∈ ℝ
39 eqidd ⊢ φ → x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ B B 0 = x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ B B 0
40 eqidd ⊢ φ → x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ C C 0 = x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ C C 0
41 25 32 38 39 40 offval2 ⊢ φ → 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
42 iftrue ⊢ x ∈ A → if x ∈ A if 0 ≤ B B 0 + if 0 ≤ C C 0 0 = if 0 ≤ B B 0 + if 0 ≤ C C 0
43 ibar ⊢ x ∈ A → 0 ≤ B ↔ x ∈ A ∧ 0 ≤ B
44 43 ifbid ⊢ x ∈ A → if 0 ≤ B B 0 = if x ∈ A ∧ 0 ≤ B B 0
45 ibar ⊢ x ∈ A → 0 ≤ C ↔ x ∈ A ∧ 0 ≤ C
46 45 ifbid ⊢ x ∈ A → if 0 ≤ C C 0 = if x ∈ A ∧ 0 ≤ C C 0
47 44 46 oveq12d ⊢ x ∈ A → if 0 ≤ B B 0 + if 0 ≤ C C 0 = if x ∈ A ∧ 0 ≤ B B 0 + if x ∈ A ∧ 0 ≤ C C 0
48 42 47 eqtr2d ⊢ x ∈ A → if x ∈ A ∧ 0 ≤ B B 0 + if x ∈ A ∧ 0 ≤ C C 0 = if x ∈ A if 0 ≤ B B 0 + if 0 ≤ C C 0 0
49 00id ⊢ 0 + 0 = 0
50 simpl ⊢ x ∈ A ∧ 0 ≤ B → x ∈ A
51 50 con3i ⊢ ¬ x ∈ A → ¬ x ∈ A ∧ 0 ≤ B
52 51 iffalsed ⊢ ¬ x ∈ A → if x ∈ A ∧ 0 ≤ B B 0 = 0
53 simpl ⊢ x ∈ A ∧ 0 ≤ C → x ∈ A
54 53 con3i ⊢ ¬ x ∈ A → ¬ x ∈ A ∧ 0 ≤ C
55 54 iffalsed ⊢ ¬ x ∈ A → if x ∈ A ∧ 0 ≤ C C 0 = 0
56 52 55 oveq12d ⊢ ¬ x ∈ A → if x ∈ A ∧ 0 ≤ B B 0 + if x ∈ A ∧ 0 ≤ C C 0 = 0 + 0
57 iffalse ⊢ ¬ x ∈ A → if x ∈ A if 0 ≤ B B 0 + if 0 ≤ C C 0 0 = 0
58 49 56 57 3eqtr4a ⊢ ¬ x ∈ A → if x ∈ A ∧ 0 ≤ B B 0 + if x ∈ A ∧ 0 ≤ C C 0 = if x ∈ A if 0 ≤ B B 0 + if 0 ≤ C C 0 0
59 48 58 pm2.61i ⊢ if x ∈ A ∧ 0 ≤ B B 0 + if x ∈ A ∧ 0 ≤ C C 0 = if x ∈ A if 0 ≤ B B 0 + if 0 ≤ C C 0 0
60 59 mpteq2i ⊢ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ B B 0 + if x ∈ A ∧ 0 ≤ C C 0 = x ∈ ℝ ⟼ if x ∈ A if 0 ≤ B B 0 + if 0 ≤ C C 0 0
61 41 60 syl6eq ⊢ φ → x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ B B 0 + f x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ C C 0 = x ∈ ℝ ⟼ if x ∈ A if 0 ≤ B B 0 + if 0 ≤ C C 0 0
62 61 fveq2d ⊢ φ → ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ B B 0 + f x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ C C 0 = ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A if 0 ≤ B B 0 + if 0 ≤ C C 0 0
63 4 1 mbfdm2 ⊢ φ → A ∈ dom ⁡ vol
64 mblss ⊢ A ∈ dom ⁡ vol → A ⊆ ℝ
65 63 64 syl ⊢ φ → A ⊆ ℝ
66 rembl ⊢ ℝ ∈ dom ⁡ vol
67 66 a1i ⊢ φ → ℝ ∈ dom ⁡ vol
68 31 adantr ⊢ φ ∧ x ∈ A → if x ∈ A ∧ 0 ≤ B B 0 ∈ ℝ
69 eldifn ⊢ x ∈ ℝ ∖ A → ¬ x ∈ A
70 69 adantl ⊢ φ ∧ x ∈ ℝ ∖ A → ¬ x ∈ A
71 70 intnanrd ⊢ φ ∧ x ∈ ℝ ∖ A → ¬ x ∈ A ∧ 0 ≤ B
72 71 iffalsed ⊢ φ ∧ x ∈ ℝ ∖ A → if x ∈ A ∧ 0 ≤ B B 0 = 0
73 44 mpteq2ia ⊢ x ∈ A ⟼ if 0 ≤ B B 0 = x ∈ A ⟼ if x ∈ A ∧ 0 ≤ B B 0
74 1 4 mbfpos ⊢ φ → x ∈ A ⟼ if 0 ≤ B B 0 ∈ MblFn
75 73 74 eqeltrrid ⊢ φ → x ∈ A ⟼ if x ∈ A ∧ 0 ≤ B B 0 ∈ MblFn
76 65 67 68 72 75 mbfss ⊢ φ → x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ B B 0 ∈ MblFn
77 max1 ⊢ 0 ∈ ℝ ∧ B ∈ ℝ → 0 ≤ if 0 ≤ B B 0
78 10 1 77 sylancr ⊢ φ ∧ x ∈ A → 0 ≤ if 0 ≤ B B 0
79 elrege0 ⊢ if 0 ≤ B B 0 ∈ 0 +∞ ↔ if 0 ≤ B B 0 ∈ ℝ ∧ 0 ≤ if 0 ≤ B B 0
80 28 78 79 sylanbrc ⊢ φ ∧ x ∈ A → if 0 ≤ B B 0 ∈ 0 +∞
81 0e0icopnf ⊢ 0 ∈ 0 +∞
82 81 a1i ⊢ φ ∧ ¬ x ∈ A → 0 ∈ 0 +∞
83 80 82 ifclda ⊢ φ → if x ∈ A if 0 ≤ B B 0 0 ∈ 0 +∞
84 26 83 eqeltrid ⊢ φ → if x ∈ A ∧ 0 ≤ B B 0 ∈ 0 +∞
85 84 adantr ⊢ φ ∧ x ∈ ℝ → if x ∈ A ∧ 0 ≤ B B 0 ∈ 0 +∞
86 85 fmpttd ⊢ φ → x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ B B 0 : ℝ ⟶ 0 +∞
87 max1 ⊢ 0 ∈ ℝ ∧ C ∈ ℝ → 0 ≤ if 0 ≤ C C 0
88 10 2 87 sylancr ⊢ φ ∧ x ∈ A → 0 ≤ if 0 ≤ C C 0
89 elrege0 ⊢ if 0 ≤ C C 0 ∈ 0 +∞ ↔ if 0 ≤ C C 0 ∈ ℝ ∧ 0 ≤ if 0 ≤ C C 0
90 35 88 89 sylanbrc ⊢ φ ∧ x ∈ A → if 0 ≤ C C 0 ∈ 0 +∞
91 90 82 ifclda ⊢ φ → if x ∈ A if 0 ≤ C C 0 0 ∈ 0 +∞
92 33 91 eqeltrid ⊢ φ → if x ∈ A ∧ 0 ≤ C C 0 ∈ 0 +∞
93 92 adantr ⊢ φ ∧ x ∈ ℝ → if x ∈ A ∧ 0 ≤ C C 0 ∈ 0 +∞
94 93 fmpttd ⊢ φ → x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ C C 0 : ℝ ⟶ 0 +∞
95 76 86 5 94 6 itg2addnc ⊢ φ → ∫ 2 ⁡ 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
96 62 95 eqtr3d ⊢ φ → ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A if 0 ≤ B B 0 + if 0 ≤ C C 0 0 = ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ B B 0 + ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ C C 0
97 5 6 readdcld ⊢ φ → ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ B B 0 + ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ C C 0 ∈ ℝ
98 96 97 eqeltrd ⊢ φ → ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A if 0 ≤ B B 0 + if 0 ≤ C C 0 0 ∈ ℝ
99 28 35 readdcld ⊢ φ ∧ x ∈ A → if 0 ≤ B B 0 + if 0 ≤ C C 0 ∈ ℝ
100 99 rexrd ⊢ φ ∧ x ∈ A → if 0 ≤ B B 0 + if 0 ≤ C C 0 ∈ ℝ *
101 28 35 78 88 addge0d ⊢ φ ∧ x ∈ A → 0 ≤ if 0 ≤ B B 0 + if 0 ≤ C C 0
102 elxrge0 ⊢ if 0 ≤ B B 0 + if 0 ≤ C C 0 ∈ 0 +∞ ↔ if 0 ≤ B B 0 + if 0 ≤ C C 0 ∈ ℝ * ∧ 0 ≤ if 0 ≤ B B 0 + if 0 ≤ C C 0
103 100 101 102 sylanbrc ⊢ φ ∧ x ∈ A → if 0 ≤ B B 0 + if 0 ≤ C C 0 ∈ 0 +∞
104 103 19 ifclda ⊢ φ → if x ∈ A if 0 ≤ B B 0 + if 0 ≤ C C 0 0 ∈ 0 +∞
105 104 adantr ⊢ φ ∧ x ∈ ℝ → if x ∈ A if 0 ≤ B B 0 + if 0 ≤ C C 0 0 ∈ 0 +∞
106 105 fmpttd ⊢ φ → x ∈ ℝ ⟼ if x ∈ A if 0 ≤ B B 0 + if 0 ≤ C C 0 0 : ℝ ⟶ 0 +∞
107 max2 ⊢ 0 ∈ ℝ ∧ B ∈ ℝ → B ≤ if 0 ≤ B B 0
108 10 1 107 sylancr ⊢ φ ∧ x ∈ A → B ≤ if 0 ≤ B B 0
109 max2 ⊢ 0 ∈ ℝ ∧ C ∈ ℝ → C ≤ if 0 ≤ C C 0
110 10 2 109 sylancr ⊢ φ ∧ x ∈ A → C ≤ if 0 ≤ C C 0
111 1 2 28 35 108 110 le2addd ⊢ φ ∧ x ∈ A → B + C ≤ if 0 ≤ B B 0 + if 0 ≤ C C 0
112 3 111 eqbrtrd ⊢ φ ∧ x ∈ A → D ≤ if 0 ≤ B B 0 + if 0 ≤ C C 0
113 breq1 ⊢ D = if 0 ≤ D D 0 → D ≤ if 0 ≤ B B 0 + if 0 ≤ C C 0 ↔ if 0 ≤ D D 0 ≤ if 0 ≤ B B 0 + if 0 ≤ C C 0
114 breq1 ⊢ 0 = if 0 ≤ D D 0 → 0 ≤ if 0 ≤ B B 0 + if 0 ≤ C C 0 ↔ if 0 ≤ D D 0 ≤ if 0 ≤ B B 0 + if 0 ≤ C C 0
115 113 114 ifboth ⊢ D ≤ if 0 ≤ B B 0 + if 0 ≤ C C 0 ∧ 0 ≤ if 0 ≤ B B 0 + if 0 ≤ C C 0 → if 0 ≤ D D 0 ≤ if 0 ≤ B B 0 + if 0 ≤ C C 0
116 112 101 115 syl2anc ⊢ φ ∧ x ∈ A → if 0 ≤ D D 0 ≤ if 0 ≤ B B 0 + if 0 ≤ C C 0
117 iftrue ⊢ x ∈ A → if x ∈ A if 0 ≤ D D 0 0 = if 0 ≤ D D 0
118 117 adantl ⊢ φ ∧ x ∈ A → if x ∈ A if 0 ≤ D D 0 0 = if 0 ≤ D D 0
119 42 adantl ⊢ φ ∧ x ∈ A → if x ∈ A if 0 ≤ B B 0 + if 0 ≤ C C 0 0 = if 0 ≤ B B 0 + if 0 ≤ C C 0
120 116 118 119 3brtr4d ⊢ φ ∧ x ∈ A → if x ∈ A if 0 ≤ D D 0 0 ≤ if x ∈ A if 0 ≤ B B 0 + if 0 ≤ C C 0 0
121 120 ex ⊢ φ → x ∈ A → if x ∈ A if 0 ≤ D D 0 0 ≤ if x ∈ A if 0 ≤ B B 0 + if 0 ≤ C C 0 0
122 0le0 ⊢ 0 ≤ 0
123 122 a1i ⊢ ¬ x ∈ A → 0 ≤ 0
124 iffalse ⊢ ¬ x ∈ A → if x ∈ A if 0 ≤ D D 0 0 = 0
125 123 124 57 3brtr4d ⊢ ¬ x ∈ A → if x ∈ A if 0 ≤ D D 0 0 ≤ if x ∈ A if 0 ≤ B B 0 + if 0 ≤ C C 0 0
126 121 125 pm2.61d1 ⊢ φ → if x ∈ A if 0 ≤ D D 0 0 ≤ if x ∈ A if 0 ≤ B B 0 + if 0 ≤ C C 0 0
127 7 126 eqbrtrid ⊢ φ → if x ∈ A ∧ 0 ≤ D D 0 ≤ if x ∈ A if 0 ≤ B B 0 + if 0 ≤ C C 0 0
128 127 ralrimivw ⊢ φ → ∀ x ∈ ℝ if x ∈ A ∧ 0 ≤ D D 0 ≤ if x ∈ A if 0 ≤ B B 0 + if 0 ≤ C C 0 0
129 eqidd ⊢ φ → x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ D D 0 = x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ D D 0
130 eqidd ⊢ φ → x ∈ ℝ ⟼ if x ∈ A if 0 ≤ B B 0 + if 0 ≤ C C 0 0 = x ∈ ℝ ⟼ if x ∈ A if 0 ≤ B B 0 + if 0 ≤ C C 0 0
131 25 22 105 129 130 ofrfval2 ⊢ φ → x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ D D 0 ≤ f x ∈ ℝ ⟼ if x ∈ A if 0 ≤ B B 0 + if 0 ≤ C C 0 0 ↔ ∀ x ∈ ℝ if x ∈ A ∧ 0 ≤ D D 0 ≤ if x ∈ A if 0 ≤ B B 0 + if 0 ≤ C C 0 0
132 128 131 mpbird ⊢ φ → x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ D D 0 ≤ f x ∈ ℝ ⟼ if x ∈ A if 0 ≤ B B 0 + if 0 ≤ C C 0 0
133 itg2le ⊢ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ D D 0 : ℝ ⟶ 0 +∞ ∧ x ∈ ℝ ⟼ if x ∈ A if 0 ≤ B B 0 + if 0 ≤ C C 0 0 : ℝ ⟶ 0 +∞ ∧ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ D D 0 ≤ f x ∈ ℝ ⟼ if x ∈ A if 0 ≤ B B 0 + if 0 ≤ C C 0 0 → ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ D D 0 ≤ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A if 0 ≤ B B 0 + if 0 ≤ C C 0 0
134 23 106 132 133 syl3anc ⊢ φ → ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ D D 0 ≤ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A if 0 ≤ B B 0 + if 0 ≤ C C 0 0
135 itg2lecl ⊢ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ D D 0 : ℝ ⟶ 0 +∞ ∧ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A if 0 ≤ B B 0 + if 0 ≤ C C 0 0 ∈ ℝ ∧ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ D D 0 ≤ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A if 0 ≤ B B 0 + if 0 ≤ C C 0 0 → ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ D D 0 ∈ ℝ
136 23 98 134 135 syl3anc ⊢ φ → ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ D D 0 ∈ ℝ