Database
BASIC REAL AND COMPLEX ANALYSIS
Integrals
Lebesgue integration
Lesbesgue integral
iblmulc2
Next ⟩
itgmulc2lem1
Metamath Proof Explorer
Ascii
Unicode
Theorem
iblmulc2
Description:
Multiply an integral by a constant.
(Contributed by
Mario Carneiro
, 25-Aug-2014)
Ref
Expression
Hypotheses
itgmulc2.1
⊢
φ
→
C
∈
ℂ
itgmulc2.2
⊢
φ
∧
x
∈
A
→
B
∈
V
itgmulc2.3
⊢
φ
→
x
∈
A
⟼
B
∈
𝐿
1
Assertion
iblmulc2
⊢
φ
→
x
∈
A
⟼
C
B
∈
𝐿
1
Proof
Step
Hyp
Ref
Expression
1
itgmulc2.1
⊢
φ
→
C
∈
ℂ
2
itgmulc2.2
⊢
φ
∧
x
∈
A
→
B
∈
V
3
itgmulc2.3
⊢
φ
→
x
∈
A
⟼
B
∈
𝐿
1
4
iblmbf
⊢
x
∈
A
⟼
B
∈
𝐿
1
→
x
∈
A
⟼
B
∈
MblFn
5
3
4
syl
⊢
φ
→
x
∈
A
⟼
B
∈
MblFn
6
1
2
5
mbfmulc2
⊢
φ
→
x
∈
A
⟼
C
B
∈
MblFn
7
ifan
⊢
if
x
∈
A
∧
0
≤
ℜ
C
B
i
k
ℜ
C
B
i
k
0
=
if
x
∈
A
if
0
≤
ℜ
C
B
i
k
ℜ
C
B
i
k
0
0
8
1
adantr
⊢
φ
∧
x
∈
A
→
C
∈
ℂ
9
5
2
mbfmptcl
⊢
φ
∧
x
∈
A
→
B
∈
ℂ
10
8
9
mulcld
⊢
φ
∧
x
∈
A
→
C
B
∈
ℂ
11
10
adantlr
⊢
φ
∧
k
∈
0
…
3
∧
x
∈
A
→
C
B
∈
ℂ
12
ax-icn
⊢
i
∈
ℂ
13
ine0
⊢
i
≠
0
14
elfzelz
⊢
k
∈
0
…
3
→
k
∈
ℤ
15
14
ad2antlr
⊢
φ
∧
k
∈
0
…
3
∧
x
∈
A
→
k
∈
ℤ
16
expclz
⊢
i
∈
ℂ
∧
i
≠
0
∧
k
∈
ℤ
→
i
k
∈
ℂ
17
12
13
15
16
mp3an12i
⊢
φ
∧
k
∈
0
…
3
∧
x
∈
A
→
i
k
∈
ℂ
18
expne0i
⊢
i
∈
ℂ
∧
i
≠
0
∧
k
∈
ℤ
→
i
k
≠
0
19
12
13
15
18
mp3an12i
⊢
φ
∧
k
∈
0
…
3
∧
x
∈
A
→
i
k
≠
0
20
11
17
19
divcld
⊢
φ
∧
k
∈
0
…
3
∧
x
∈
A
→
C
B
i
k
∈
ℂ
21
20
recld
⊢
φ
∧
k
∈
0
…
3
∧
x
∈
A
→
ℜ
C
B
i
k
∈
ℝ
22
0re
⊢
0
∈
ℝ
23
ifcl
⊢
ℜ
C
B
i
k
∈
ℝ
∧
0
∈
ℝ
→
if
0
≤
ℜ
C
B
i
k
ℜ
C
B
i
k
0
∈
ℝ
24
21
22
23
sylancl
⊢
φ
∧
k
∈
0
…
3
∧
x
∈
A
→
if
0
≤
ℜ
C
B
i
k
ℜ
C
B
i
k
0
∈
ℝ
25
24
rexrd
⊢
φ
∧
k
∈
0
…
3
∧
x
∈
A
→
if
0
≤
ℜ
C
B
i
k
ℜ
C
B
i
k
0
∈
ℝ
*
26
max1
⊢
0
∈
ℝ
∧
ℜ
C
B
i
k
∈
ℝ
→
0
≤
if
0
≤
ℜ
C
B
i
k
ℜ
C
B
i
k
0
27
22
21
26
sylancr
⊢
φ
∧
k
∈
0
…
3
∧
x
∈
A
→
0
≤
if
0
≤
ℜ
C
B
i
k
ℜ
C
B
i
k
0
28
elxrge0
⊢
if
0
≤
ℜ
C
B
i
k
ℜ
C
B
i
k
0
∈
0
+∞
↔
if
0
≤
ℜ
C
B
i
k
ℜ
C
B
i
k
0
∈
ℝ
*
∧
0
≤
if
0
≤
ℜ
C
B
i
k
ℜ
C
B
i
k
0
29
25
27
28
sylanbrc
⊢
φ
∧
k
∈
0
…
3
∧
x
∈
A
→
if
0
≤
ℜ
C
B
i
k
ℜ
C
B
i
k
0
∈
0
+∞
30
0e0iccpnf
⊢
0
∈
0
+∞
31
30
a1i
⊢
φ
∧
k
∈
0
…
3
∧
¬
x
∈
A
→
0
∈
0
+∞
32
29
31
ifclda
⊢
φ
∧
k
∈
0
…
3
→
if
x
∈
A
if
0
≤
ℜ
C
B
i
k
ℜ
C
B
i
k
0
0
∈
0
+∞
33
32
adantr
⊢
φ
∧
k
∈
0
…
3
∧
x
∈
ℝ
→
if
x
∈
A
if
0
≤
ℜ
C
B
i
k
ℜ
C
B
i
k
0
0
∈
0
+∞
34
7
33
eqeltrid
⊢
φ
∧
k
∈
0
…
3
∧
x
∈
ℝ
→
if
x
∈
A
∧
0
≤
ℜ
C
B
i
k
ℜ
C
B
i
k
0
∈
0
+∞
35
34
fmpttd
⊢
φ
∧
k
∈
0
…
3
→
x
∈
ℝ
⟼
if
x
∈
A
∧
0
≤
ℜ
C
B
i
k
ℜ
C
B
i
k
0
:
ℝ
⟶
0
+∞
36
reex
⊢
ℝ
∈
V
37
36
a1i
⊢
φ
→
ℝ
∈
V
38
1
abscld
⊢
φ
→
C
∈
ℝ
39
38
adantr
⊢
φ
∧
x
∈
ℝ
→
C
∈
ℝ
40
9
abscld
⊢
φ
∧
x
∈
A
→
B
∈
ℝ
41
9
absge0d
⊢
φ
∧
x
∈
A
→
0
≤
B
42
elrege0
⊢
B
∈
0
+∞
↔
B
∈
ℝ
∧
0
≤
B
43
40
41
42
sylanbrc
⊢
φ
∧
x
∈
A
→
B
∈
0
+∞
44
0e0icopnf
⊢
0
∈
0
+∞
45
44
a1i
⊢
φ
∧
¬
x
∈
A
→
0
∈
0
+∞
46
43
45
ifclda
⊢
φ
→
if
x
∈
A
B
0
∈
0
+∞
47
46
adantr
⊢
φ
∧
x
∈
ℝ
→
if
x
∈
A
B
0
∈
0
+∞
48
fconstmpt
⊢
ℝ
×
C
=
x
∈
ℝ
⟼
C
49
48
a1i
⊢
φ
→
ℝ
×
C
=
x
∈
ℝ
⟼
C
50
eqidd
⊢
φ
→
x
∈
ℝ
⟼
if
x
∈
A
B
0
=
x
∈
ℝ
⟼
if
x
∈
A
B
0
51
37
39
47
49
50
offval2
⊢
φ
→
ℝ
×
C
×
f
x
∈
ℝ
⟼
if
x
∈
A
B
0
=
x
∈
ℝ
⟼
C
if
x
∈
A
B
0
52
ovif2
⊢
C
if
x
∈
A
B
0
=
if
x
∈
A
C
B
C
⋅
0
53
8
9
absmuld
⊢
φ
∧
x
∈
A
→
C
B
=
C
B
54
53
ifeq1da
⊢
φ
→
if
x
∈
A
C
B
C
⋅
0
=
if
x
∈
A
C
B
C
⋅
0
55
38
recnd
⊢
φ
→
C
∈
ℂ
56
55
mul01d
⊢
φ
→
C
⋅
0
=
0
57
56
ifeq2d
⊢
φ
→
if
x
∈
A
C
B
C
⋅
0
=
if
x
∈
A
C
B
0
58
54
57
eqtr3d
⊢
φ
→
if
x
∈
A
C
B
C
⋅
0
=
if
x
∈
A
C
B
0
59
52
58
eqtrid
⊢
φ
→
C
if
x
∈
A
B
0
=
if
x
∈
A
C
B
0
60
59
mpteq2dv
⊢
φ
→
x
∈
ℝ
⟼
C
if
x
∈
A
B
0
=
x
∈
ℝ
⟼
if
x
∈
A
C
B
0
61
51
60
eqtrd
⊢
φ
→
ℝ
×
C
×
f
x
∈
ℝ
⟼
if
x
∈
A
B
0
=
x
∈
ℝ
⟼
if
x
∈
A
C
B
0
62
61
fveq2d
⊢
φ
→
∫
2
ℝ
×
C
×
f
x
∈
ℝ
⟼
if
x
∈
A
B
0
=
∫
2
x
∈
ℝ
⟼
if
x
∈
A
C
B
0
63
47
fmpttd
⊢
φ
→
x
∈
ℝ
⟼
if
x
∈
A
B
0
:
ℝ
⟶
0
+∞
64
2
3
iblabs
⊢
φ
→
x
∈
A
⟼
B
∈
𝐿
1
65
40
41
iblpos
⊢
φ
→
x
∈
A
⟼
B
∈
𝐿
1
↔
x
∈
A
⟼
B
∈
MblFn
∧
∫
2
x
∈
ℝ
⟼
if
x
∈
A
B
0
∈
ℝ
66
64
65
mpbid
⊢
φ
→
x
∈
A
⟼
B
∈
MblFn
∧
∫
2
x
∈
ℝ
⟼
if
x
∈
A
B
0
∈
ℝ
67
66
simprd
⊢
φ
→
∫
2
x
∈
ℝ
⟼
if
x
∈
A
B
0
∈
ℝ
68
abscl
⊢
C
∈
ℂ
→
C
∈
ℝ
69
absge0
⊢
C
∈
ℂ
→
0
≤
C
70
elrege0
⊢
C
∈
0
+∞
↔
C
∈
ℝ
∧
0
≤
C
71
68
69
70
sylanbrc
⊢
C
∈
ℂ
→
C
∈
0
+∞
72
1
71
syl
⊢
φ
→
C
∈
0
+∞
73
63
67
72
itg2mulc
⊢
φ
→
∫
2
ℝ
×
C
×
f
x
∈
ℝ
⟼
if
x
∈
A
B
0
=
C
∫
2
x
∈
ℝ
⟼
if
x
∈
A
B
0
74
62
73
eqtr3d
⊢
φ
→
∫
2
x
∈
ℝ
⟼
if
x
∈
A
C
B
0
=
C
∫
2
x
∈
ℝ
⟼
if
x
∈
A
B
0
75
38
67
remulcld
⊢
φ
→
C
∫
2
x
∈
ℝ
⟼
if
x
∈
A
B
0
∈
ℝ
76
74
75
eqeltrd
⊢
φ
→
∫
2
x
∈
ℝ
⟼
if
x
∈
A
C
B
0
∈
ℝ
77
76
adantr
⊢
φ
∧
k
∈
0
…
3
→
∫
2
x
∈
ℝ
⟼
if
x
∈
A
C
B
0
∈
ℝ
78
10
abscld
⊢
φ
∧
x
∈
A
→
C
B
∈
ℝ
79
78
rexrd
⊢
φ
∧
x
∈
A
→
C
B
∈
ℝ
*
80
10
absge0d
⊢
φ
∧
x
∈
A
→
0
≤
C
B
81
elxrge0
⊢
C
B
∈
0
+∞
↔
C
B
∈
ℝ
*
∧
0
≤
C
B
82
79
80
81
sylanbrc
⊢
φ
∧
x
∈
A
→
C
B
∈
0
+∞
83
30
a1i
⊢
φ
∧
¬
x
∈
A
→
0
∈
0
+∞
84
82
83
ifclda
⊢
φ
→
if
x
∈
A
C
B
0
∈
0
+∞
85
84
adantr
⊢
φ
∧
x
∈
ℝ
→
if
x
∈
A
C
B
0
∈
0
+∞
86
85
fmpttd
⊢
φ
→
x
∈
ℝ
⟼
if
x
∈
A
C
B
0
:
ℝ
⟶
0
+∞
87
86
adantr
⊢
φ
∧
k
∈
0
…
3
→
x
∈
ℝ
⟼
if
x
∈
A
C
B
0
:
ℝ
⟶
0
+∞
88
20
releabsd
⊢
φ
∧
k
∈
0
…
3
∧
x
∈
A
→
ℜ
C
B
i
k
≤
C
B
i
k
89
11
17
19
absdivd
⊢
φ
∧
k
∈
0
…
3
∧
x
∈
A
→
C
B
i
k
=
C
B
i
k
90
elfznn0
⊢
k
∈
0
…
3
→
k
∈
ℕ
0
91
90
ad2antlr
⊢
φ
∧
k
∈
0
…
3
∧
x
∈
A
→
k
∈
ℕ
0
92
absexp
⊢
i
∈
ℂ
∧
k
∈
ℕ
0
→
i
k
=
i
k
93
12
91
92
sylancr
⊢
φ
∧
k
∈
0
…
3
∧
x
∈
A
→
i
k
=
i
k
94
absi
⊢
i
=
1
95
94
oveq1i
⊢
i
k
=
1
k
96
1exp
⊢
k
∈
ℤ
→
1
k
=
1
97
15
96
syl
⊢
φ
∧
k
∈
0
…
3
∧
x
∈
A
→
1
k
=
1
98
95
97
eqtrid
⊢
φ
∧
k
∈
0
…
3
∧
x
∈
A
→
i
k
=
1
99
93
98
eqtrd
⊢
φ
∧
k
∈
0
…
3
∧
x
∈
A
→
i
k
=
1
100
99
oveq2d
⊢
φ
∧
k
∈
0
…
3
∧
x
∈
A
→
C
B
i
k
=
C
B
1
101
78
recnd
⊢
φ
∧
x
∈
A
→
C
B
∈
ℂ
102
101
adantlr
⊢
φ
∧
k
∈
0
…
3
∧
x
∈
A
→
C
B
∈
ℂ
103
102
div1d
⊢
φ
∧
k
∈
0
…
3
∧
x
∈
A
→
C
B
1
=
C
B
104
89
100
103
3eqtrd
⊢
φ
∧
k
∈
0
…
3
∧
x
∈
A
→
C
B
i
k
=
C
B
105
88
104
breqtrd
⊢
φ
∧
k
∈
0
…
3
∧
x
∈
A
→
ℜ
C
B
i
k
≤
C
B
106
80
adantlr
⊢
φ
∧
k
∈
0
…
3
∧
x
∈
A
→
0
≤
C
B
107
breq1
⊢
ℜ
C
B
i
k
=
if
0
≤
ℜ
C
B
i
k
ℜ
C
B
i
k
0
→
ℜ
C
B
i
k
≤
C
B
↔
if
0
≤
ℜ
C
B
i
k
ℜ
C
B
i
k
0
≤
C
B
108
breq1
⊢
0
=
if
0
≤
ℜ
C
B
i
k
ℜ
C
B
i
k
0
→
0
≤
C
B
↔
if
0
≤
ℜ
C
B
i
k
ℜ
C
B
i
k
0
≤
C
B
109
107
108
ifboth
⊢
ℜ
C
B
i
k
≤
C
B
∧
0
≤
C
B
→
if
0
≤
ℜ
C
B
i
k
ℜ
C
B
i
k
0
≤
C
B
110
105
106
109
syl2anc
⊢
φ
∧
k
∈
0
…
3
∧
x
∈
A
→
if
0
≤
ℜ
C
B
i
k
ℜ
C
B
i
k
0
≤
C
B
111
iftrue
⊢
x
∈
A
→
if
x
∈
A
if
0
≤
ℜ
C
B
i
k
ℜ
C
B
i
k
0
0
=
if
0
≤
ℜ
C
B
i
k
ℜ
C
B
i
k
0
112
111
adantl
⊢
φ
∧
k
∈
0
…
3
∧
x
∈
A
→
if
x
∈
A
if
0
≤
ℜ
C
B
i
k
ℜ
C
B
i
k
0
0
=
if
0
≤
ℜ
C
B
i
k
ℜ
C
B
i
k
0
113
iftrue
⊢
x
∈
A
→
if
x
∈
A
C
B
0
=
C
B
114
113
adantl
⊢
φ
∧
k
∈
0
…
3
∧
x
∈
A
→
if
x
∈
A
C
B
0
=
C
B
115
110
112
114
3brtr4d
⊢
φ
∧
k
∈
0
…
3
∧
x
∈
A
→
if
x
∈
A
if
0
≤
ℜ
C
B
i
k
ℜ
C
B
i
k
0
0
≤
if
x
∈
A
C
B
0
116
115
ex
⊢
φ
∧
k
∈
0
…
3
→
x
∈
A
→
if
x
∈
A
if
0
≤
ℜ
C
B
i
k
ℜ
C
B
i
k
0
0
≤
if
x
∈
A
C
B
0
117
0le0
⊢
0
≤
0
118
117
a1i
⊢
¬
x
∈
A
→
0
≤
0
119
iffalse
⊢
¬
x
∈
A
→
if
x
∈
A
if
0
≤
ℜ
C
B
i
k
ℜ
C
B
i
k
0
0
=
0
120
iffalse
⊢
¬
x
∈
A
→
if
x
∈
A
C
B
0
=
0
121
118
119
120
3brtr4d
⊢
¬
x
∈
A
→
if
x
∈
A
if
0
≤
ℜ
C
B
i
k
ℜ
C
B
i
k
0
0
≤
if
x
∈
A
C
B
0
122
116
121
pm2.61d1
⊢
φ
∧
k
∈
0
…
3
→
if
x
∈
A
if
0
≤
ℜ
C
B
i
k
ℜ
C
B
i
k
0
0
≤
if
x
∈
A
C
B
0
123
7
122
eqbrtrid
⊢
φ
∧
k
∈
0
…
3
→
if
x
∈
A
∧
0
≤
ℜ
C
B
i
k
ℜ
C
B
i
k
0
≤
if
x
∈
A
C
B
0
124
123
ralrimivw
⊢
φ
∧
k
∈
0
…
3
→
∀
x
∈
ℝ
if
x
∈
A
∧
0
≤
ℜ
C
B
i
k
ℜ
C
B
i
k
0
≤
if
x
∈
A
C
B
0
125
36
a1i
⊢
φ
∧
k
∈
0
…
3
→
ℝ
∈
V
126
85
adantlr
⊢
φ
∧
k
∈
0
…
3
∧
x
∈
ℝ
→
if
x
∈
A
C
B
0
∈
0
+∞
127
eqidd
⊢
φ
∧
k
∈
0
…
3
→
x
∈
ℝ
⟼
if
x
∈
A
∧
0
≤
ℜ
C
B
i
k
ℜ
C
B
i
k
0
=
x
∈
ℝ
⟼
if
x
∈
A
∧
0
≤
ℜ
C
B
i
k
ℜ
C
B
i
k
0
128
eqidd
⊢
φ
∧
k
∈
0
…
3
→
x
∈
ℝ
⟼
if
x
∈
A
C
B
0
=
x
∈
ℝ
⟼
if
x
∈
A
C
B
0
129
125
34
126
127
128
ofrfval2
⊢
φ
∧
k
∈
0
…
3
→
x
∈
ℝ
⟼
if
x
∈
A
∧
0
≤
ℜ
C
B
i
k
ℜ
C
B
i
k
0
≤
f
x
∈
ℝ
⟼
if
x
∈
A
C
B
0
↔
∀
x
∈
ℝ
if
x
∈
A
∧
0
≤
ℜ
C
B
i
k
ℜ
C
B
i
k
0
≤
if
x
∈
A
C
B
0
130
124
129
mpbird
⊢
φ
∧
k
∈
0
…
3
→
x
∈
ℝ
⟼
if
x
∈
A
∧
0
≤
ℜ
C
B
i
k
ℜ
C
B
i
k
0
≤
f
x
∈
ℝ
⟼
if
x
∈
A
C
B
0
131
itg2le
⊢
x
∈
ℝ
⟼
if
x
∈
A
∧
0
≤
ℜ
C
B
i
k
ℜ
C
B
i
k
0
:
ℝ
⟶
0
+∞
∧
x
∈
ℝ
⟼
if
x
∈
A
C
B
0
:
ℝ
⟶
0
+∞
∧
x
∈
ℝ
⟼
if
x
∈
A
∧
0
≤
ℜ
C
B
i
k
ℜ
C
B
i
k
0
≤
f
x
∈
ℝ
⟼
if
x
∈
A
C
B
0
→
∫
2
x
∈
ℝ
⟼
if
x
∈
A
∧
0
≤
ℜ
C
B
i
k
ℜ
C
B
i
k
0
≤
∫
2
x
∈
ℝ
⟼
if
x
∈
A
C
B
0
132
35
87
130
131
syl3anc
⊢
φ
∧
k
∈
0
…
3
→
∫
2
x
∈
ℝ
⟼
if
x
∈
A
∧
0
≤
ℜ
C
B
i
k
ℜ
C
B
i
k
0
≤
∫
2
x
∈
ℝ
⟼
if
x
∈
A
C
B
0
133
itg2lecl
⊢
x
∈
ℝ
⟼
if
x
∈
A
∧
0
≤
ℜ
C
B
i
k
ℜ
C
B
i
k
0
:
ℝ
⟶
0
+∞
∧
∫
2
x
∈
ℝ
⟼
if
x
∈
A
C
B
0
∈
ℝ
∧
∫
2
x
∈
ℝ
⟼
if
x
∈
A
∧
0
≤
ℜ
C
B
i
k
ℜ
C
B
i
k
0
≤
∫
2
x
∈
ℝ
⟼
if
x
∈
A
C
B
0
→
∫
2
x
∈
ℝ
⟼
if
x
∈
A
∧
0
≤
ℜ
C
B
i
k
ℜ
C
B
i
k
0
∈
ℝ
134
35
77
132
133
syl3anc
⊢
φ
∧
k
∈
0
…
3
→
∫
2
x
∈
ℝ
⟼
if
x
∈
A
∧
0
≤
ℜ
C
B
i
k
ℜ
C
B
i
k
0
∈
ℝ
135
134
ralrimiva
⊢
φ
→
∀
k
∈
0
…
3
∫
2
x
∈
ℝ
⟼
if
x
∈
A
∧
0
≤
ℜ
C
B
i
k
ℜ
C
B
i
k
0
∈
ℝ
136
eqidd
⊢
φ
→
x
∈
ℝ
⟼
if
x
∈
A
∧
0
≤
ℜ
C
B
i
k
ℜ
C
B
i
k
0
=
x
∈
ℝ
⟼
if
x
∈
A
∧
0
≤
ℜ
C
B
i
k
ℜ
C
B
i
k
0
137
eqidd
⊢
φ
∧
x
∈
A
→
ℜ
C
B
i
k
=
ℜ
C
B
i
k
138
136
137
10
isibl2
⊢
φ
→
x
∈
A
⟼
C
B
∈
𝐿
1
↔
x
∈
A
⟼
C
B
∈
MblFn
∧
∀
k
∈
0
…
3
∫
2
x
∈
ℝ
⟼
if
x
∈
A
∧
0
≤
ℜ
C
B
i
k
ℜ
C
B
i
k
0
∈
ℝ
139
6
135
138
mpbir2and
⊢
φ
→
x
∈
A
⟼
C
B
∈
𝐿
1