Metamath Proof Explorer

Theorem ibladdlem

Description: Lemma for ibladd . (Contributed by Mario Carneiro, 17-Aug-2014)

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

Proof

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