Database
BASIC REAL AND COMPLEX ANALYSIS
Integrals
Lebesgue integration
Lesbesgue integral
itgmulc2lem2
Next ⟩
itgmulc2
Metamath Proof Explorer
Ascii
Unicode
Theorem
itgmulc2lem2
Description:
Lemma for
itgmulc2
: real case.
(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
itgmulc2.4
⊢
φ
→
C
∈
ℝ
itgmulc2.5
⊢
φ
∧
x
∈
A
→
B
∈
ℝ
Assertion
itgmulc2lem2
⊢
φ
→
C
∫
A
B
d
x
=
∫
A
C
B
d
x
Proof
Step
Hyp
Ref
Expression
1
itgmulc2.1
⊢
φ
→
C
∈
ℂ
2
itgmulc2.2
⊢
φ
∧
x
∈
A
→
B
∈
V
3
itgmulc2.3
⊢
φ
→
x
∈
A
⟼
B
∈
𝐿
1
4
itgmulc2.4
⊢
φ
→
C
∈
ℝ
5
itgmulc2.5
⊢
φ
∧
x
∈
A
→
B
∈
ℝ
6
4
adantr
⊢
φ
∧
x
∈
A
→
C
∈
ℝ
7
max0sub
⊢
C
∈
ℝ
→
if
0
≤
C
C
0
−
if
0
≤
−
C
−
C
0
=
C
8
6
7
syl
⊢
φ
∧
x
∈
A
→
if
0
≤
C
C
0
−
if
0
≤
−
C
−
C
0
=
C
9
8
oveq1d
⊢
φ
∧
x
∈
A
→
if
0
≤
C
C
0
−
if
0
≤
−
C
−
C
0
B
=
C
B
10
0re
⊢
0
∈
ℝ
11
ifcl
⊢
C
∈
ℝ
∧
0
∈
ℝ
→
if
0
≤
C
C
0
∈
ℝ
12
4
10
11
sylancl
⊢
φ
→
if
0
≤
C
C
0
∈
ℝ
13
12
recnd
⊢
φ
→
if
0
≤
C
C
0
∈
ℂ
14
13
adantr
⊢
φ
∧
x
∈
A
→
if
0
≤
C
C
0
∈
ℂ
15
4
renegcld
⊢
φ
→
−
C
∈
ℝ
16
ifcl
⊢
−
C
∈
ℝ
∧
0
∈
ℝ
→
if
0
≤
−
C
−
C
0
∈
ℝ
17
15
10
16
sylancl
⊢
φ
→
if
0
≤
−
C
−
C
0
∈
ℝ
18
17
recnd
⊢
φ
→
if
0
≤
−
C
−
C
0
∈
ℂ
19
18
adantr
⊢
φ
∧
x
∈
A
→
if
0
≤
−
C
−
C
0
∈
ℂ
20
5
recnd
⊢
φ
∧
x
∈
A
→
B
∈
ℂ
21
14
19
20
subdird
⊢
φ
∧
x
∈
A
→
if
0
≤
C
C
0
−
if
0
≤
−
C
−
C
0
B
=
if
0
≤
C
C
0
B
−
if
0
≤
−
C
−
C
0
B
22
9
21
eqtr3d
⊢
φ
∧
x
∈
A
→
C
B
=
if
0
≤
C
C
0
B
−
if
0
≤
−
C
−
C
0
B
23
22
itgeq2dv
⊢
φ
→
∫
A
C
B
d
x
=
∫
A
if
0
≤
C
C
0
B
−
if
0
≤
−
C
−
C
0
B
d
x
24
12
adantr
⊢
φ
∧
x
∈
A
→
if
0
≤
C
C
0
∈
ℝ
25
24
5
remulcld
⊢
φ
∧
x
∈
A
→
if
0
≤
C
C
0
B
∈
ℝ
26
13
2
3
iblmulc2
⊢
φ
→
x
∈
A
⟼
if
0
≤
C
C
0
B
∈
𝐿
1
27
17
adantr
⊢
φ
∧
x
∈
A
→
if
0
≤
−
C
−
C
0
∈
ℝ
28
27
5
remulcld
⊢
φ
∧
x
∈
A
→
if
0
≤
−
C
−
C
0
B
∈
ℝ
29
18
2
3
iblmulc2
⊢
φ
→
x
∈
A
⟼
if
0
≤
−
C
−
C
0
B
∈
𝐿
1
30
25
26
28
29
itgsub
⊢
φ
→
∫
A
if
0
≤
C
C
0
B
−
if
0
≤
−
C
−
C
0
B
d
x
=
∫
A
if
0
≤
C
C
0
B
d
x
−
∫
A
if
0
≤
−
C
−
C
0
B
d
x
31
ifcl
⊢
B
∈
ℝ
∧
0
∈
ℝ
→
if
0
≤
B
B
0
∈
ℝ
32
5
10
31
sylancl
⊢
φ
∧
x
∈
A
→
if
0
≤
B
B
0
∈
ℝ
33
24
32
remulcld
⊢
φ
∧
x
∈
A
→
if
0
≤
C
C
0
if
0
≤
B
B
0
∈
ℝ
34
5
iblre
⊢
φ
→
x
∈
A
⟼
B
∈
𝐿
1
↔
x
∈
A
⟼
if
0
≤
B
B
0
∈
𝐿
1
∧
x
∈
A
⟼
if
0
≤
−
B
−
B
0
∈
𝐿
1
35
3
34
mpbid
⊢
φ
→
x
∈
A
⟼
if
0
≤
B
B
0
∈
𝐿
1
∧
x
∈
A
⟼
if
0
≤
−
B
−
B
0
∈
𝐿
1
36
35
simpld
⊢
φ
→
x
∈
A
⟼
if
0
≤
B
B
0
∈
𝐿
1
37
13
32
36
iblmulc2
⊢
φ
→
x
∈
A
⟼
if
0
≤
C
C
0
if
0
≤
B
B
0
∈
𝐿
1
38
5
renegcld
⊢
φ
∧
x
∈
A
→
−
B
∈
ℝ
39
ifcl
⊢
−
B
∈
ℝ
∧
0
∈
ℝ
→
if
0
≤
−
B
−
B
0
∈
ℝ
40
38
10
39
sylancl
⊢
φ
∧
x
∈
A
→
if
0
≤
−
B
−
B
0
∈
ℝ
41
24
40
remulcld
⊢
φ
∧
x
∈
A
→
if
0
≤
C
C
0
if
0
≤
−
B
−
B
0
∈
ℝ
42
35
simprd
⊢
φ
→
x
∈
A
⟼
if
0
≤
−
B
−
B
0
∈
𝐿
1
43
13
40
42
iblmulc2
⊢
φ
→
x
∈
A
⟼
if
0
≤
C
C
0
if
0
≤
−
B
−
B
0
∈
𝐿
1
44
33
37
41
43
itgsub
⊢
φ
→
∫
A
if
0
≤
C
C
0
if
0
≤
B
B
0
−
if
0
≤
C
C
0
if
0
≤
−
B
−
B
0
d
x
=
∫
A
if
0
≤
C
C
0
if
0
≤
B
B
0
d
x
−
∫
A
if
0
≤
C
C
0
if
0
≤
−
B
−
B
0
d
x
45
max0sub
⊢
B
∈
ℝ
→
if
0
≤
B
B
0
−
if
0
≤
−
B
−
B
0
=
B
46
5
45
syl
⊢
φ
∧
x
∈
A
→
if
0
≤
B
B
0
−
if
0
≤
−
B
−
B
0
=
B
47
46
oveq2d
⊢
φ
∧
x
∈
A
→
if
0
≤
C
C
0
if
0
≤
B
B
0
−
if
0
≤
−
B
−
B
0
=
if
0
≤
C
C
0
B
48
32
recnd
⊢
φ
∧
x
∈
A
→
if
0
≤
B
B
0
∈
ℂ
49
40
recnd
⊢
φ
∧
x
∈
A
→
if
0
≤
−
B
−
B
0
∈
ℂ
50
14
48
49
subdid
⊢
φ
∧
x
∈
A
→
if
0
≤
C
C
0
if
0
≤
B
B
0
−
if
0
≤
−
B
−
B
0
=
if
0
≤
C
C
0
if
0
≤
B
B
0
−
if
0
≤
C
C
0
if
0
≤
−
B
−
B
0
51
47
50
eqtr3d
⊢
φ
∧
x
∈
A
→
if
0
≤
C
C
0
B
=
if
0
≤
C
C
0
if
0
≤
B
B
0
−
if
0
≤
C
C
0
if
0
≤
−
B
−
B
0
52
51
itgeq2dv
⊢
φ
→
∫
A
if
0
≤
C
C
0
B
d
x
=
∫
A
if
0
≤
C
C
0
if
0
≤
B
B
0
−
if
0
≤
C
C
0
if
0
≤
−
B
−
B
0
d
x
53
5
3
itgreval
⊢
φ
→
∫
A
B
d
x
=
∫
A
if
0
≤
B
B
0
d
x
−
∫
A
if
0
≤
−
B
−
B
0
d
x
54
53
oveq2d
⊢
φ
→
if
0
≤
C
C
0
∫
A
B
d
x
=
if
0
≤
C
C
0
∫
A
if
0
≤
B
B
0
d
x
−
∫
A
if
0
≤
−
B
−
B
0
d
x
55
32
36
itgcl
⊢
φ
→
∫
A
if
0
≤
B
B
0
d
x
∈
ℂ
56
40
42
itgcl
⊢
φ
→
∫
A
if
0
≤
−
B
−
B
0
d
x
∈
ℂ
57
13
55
56
subdid
⊢
φ
→
if
0
≤
C
C
0
∫
A
if
0
≤
B
B
0
d
x
−
∫
A
if
0
≤
−
B
−
B
0
d
x
=
if
0
≤
C
C
0
∫
A
if
0
≤
B
B
0
d
x
−
if
0
≤
C
C
0
∫
A
if
0
≤
−
B
−
B
0
d
x
58
max1
⊢
0
∈
ℝ
∧
C
∈
ℝ
→
0
≤
if
0
≤
C
C
0
59
10
4
58
sylancr
⊢
φ
→
0
≤
if
0
≤
C
C
0
60
max1
⊢
0
∈
ℝ
∧
B
∈
ℝ
→
0
≤
if
0
≤
B
B
0
61
10
5
60
sylancr
⊢
φ
∧
x
∈
A
→
0
≤
if
0
≤
B
B
0
62
13
32
36
12
32
59
61
itgmulc2lem1
⊢
φ
→
if
0
≤
C
C
0
∫
A
if
0
≤
B
B
0
d
x
=
∫
A
if
0
≤
C
C
0
if
0
≤
B
B
0
d
x
63
max1
⊢
0
∈
ℝ
∧
−
B
∈
ℝ
→
0
≤
if
0
≤
−
B
−
B
0
64
10
38
63
sylancr
⊢
φ
∧
x
∈
A
→
0
≤
if
0
≤
−
B
−
B
0
65
13
40
42
12
40
59
64
itgmulc2lem1
⊢
φ
→
if
0
≤
C
C
0
∫
A
if
0
≤
−
B
−
B
0
d
x
=
∫
A
if
0
≤
C
C
0
if
0
≤
−
B
−
B
0
d
x
66
62
65
oveq12d
⊢
φ
→
if
0
≤
C
C
0
∫
A
if
0
≤
B
B
0
d
x
−
if
0
≤
C
C
0
∫
A
if
0
≤
−
B
−
B
0
d
x
=
∫
A
if
0
≤
C
C
0
if
0
≤
B
B
0
d
x
−
∫
A
if
0
≤
C
C
0
if
0
≤
−
B
−
B
0
d
x
67
54
57
66
3eqtrd
⊢
φ
→
if
0
≤
C
C
0
∫
A
B
d
x
=
∫
A
if
0
≤
C
C
0
if
0
≤
B
B
0
d
x
−
∫
A
if
0
≤
C
C
0
if
0
≤
−
B
−
B
0
d
x
68
44
52
67
3eqtr4d
⊢
φ
→
∫
A
if
0
≤
C
C
0
B
d
x
=
if
0
≤
C
C
0
∫
A
B
d
x
69
27
32
remulcld
⊢
φ
∧
x
∈
A
→
if
0
≤
−
C
−
C
0
if
0
≤
B
B
0
∈
ℝ
70
18
32
36
iblmulc2
⊢
φ
→
x
∈
A
⟼
if
0
≤
−
C
−
C
0
if
0
≤
B
B
0
∈
𝐿
1
71
27
40
remulcld
⊢
φ
∧
x
∈
A
→
if
0
≤
−
C
−
C
0
if
0
≤
−
B
−
B
0
∈
ℝ
72
18
40
42
iblmulc2
⊢
φ
→
x
∈
A
⟼
if
0
≤
−
C
−
C
0
if
0
≤
−
B
−
B
0
∈
𝐿
1
73
69
70
71
72
itgsub
⊢
φ
→
∫
A
if
0
≤
−
C
−
C
0
if
0
≤
B
B
0
−
if
0
≤
−
C
−
C
0
if
0
≤
−
B
−
B
0
d
x
=
∫
A
if
0
≤
−
C
−
C
0
if
0
≤
B
B
0
d
x
−
∫
A
if
0
≤
−
C
−
C
0
if
0
≤
−
B
−
B
0
d
x
74
46
oveq2d
⊢
φ
∧
x
∈
A
→
if
0
≤
−
C
−
C
0
if
0
≤
B
B
0
−
if
0
≤
−
B
−
B
0
=
if
0
≤
−
C
−
C
0
B
75
19
48
49
subdid
⊢
φ
∧
x
∈
A
→
if
0
≤
−
C
−
C
0
if
0
≤
B
B
0
−
if
0
≤
−
B
−
B
0
=
if
0
≤
−
C
−
C
0
if
0
≤
B
B
0
−
if
0
≤
−
C
−
C
0
if
0
≤
−
B
−
B
0
76
74
75
eqtr3d
⊢
φ
∧
x
∈
A
→
if
0
≤
−
C
−
C
0
B
=
if
0
≤
−
C
−
C
0
if
0
≤
B
B
0
−
if
0
≤
−
C
−
C
0
if
0
≤
−
B
−
B
0
77
76
itgeq2dv
⊢
φ
→
∫
A
if
0
≤
−
C
−
C
0
B
d
x
=
∫
A
if
0
≤
−
C
−
C
0
if
0
≤
B
B
0
−
if
0
≤
−
C
−
C
0
if
0
≤
−
B
−
B
0
d
x
78
53
oveq2d
⊢
φ
→
if
0
≤
−
C
−
C
0
∫
A
B
d
x
=
if
0
≤
−
C
−
C
0
∫
A
if
0
≤
B
B
0
d
x
−
∫
A
if
0
≤
−
B
−
B
0
d
x
79
18
55
56
subdid
⊢
φ
→
if
0
≤
−
C
−
C
0
∫
A
if
0
≤
B
B
0
d
x
−
∫
A
if
0
≤
−
B
−
B
0
d
x
=
if
0
≤
−
C
−
C
0
∫
A
if
0
≤
B
B
0
d
x
−
if
0
≤
−
C
−
C
0
∫
A
if
0
≤
−
B
−
B
0
d
x
80
max1
⊢
0
∈
ℝ
∧
−
C
∈
ℝ
→
0
≤
if
0
≤
−
C
−
C
0
81
10
15
80
sylancr
⊢
φ
→
0
≤
if
0
≤
−
C
−
C
0
82
18
32
36
17
32
81
61
itgmulc2lem1
⊢
φ
→
if
0
≤
−
C
−
C
0
∫
A
if
0
≤
B
B
0
d
x
=
∫
A
if
0
≤
−
C
−
C
0
if
0
≤
B
B
0
d
x
83
18
40
42
17
40
81
64
itgmulc2lem1
⊢
φ
→
if
0
≤
−
C
−
C
0
∫
A
if
0
≤
−
B
−
B
0
d
x
=
∫
A
if
0
≤
−
C
−
C
0
if
0
≤
−
B
−
B
0
d
x
84
82
83
oveq12d
⊢
φ
→
if
0
≤
−
C
−
C
0
∫
A
if
0
≤
B
B
0
d
x
−
if
0
≤
−
C
−
C
0
∫
A
if
0
≤
−
B
−
B
0
d
x
=
∫
A
if
0
≤
−
C
−
C
0
if
0
≤
B
B
0
d
x
−
∫
A
if
0
≤
−
C
−
C
0
if
0
≤
−
B
−
B
0
d
x
85
78
79
84
3eqtrd
⊢
φ
→
if
0
≤
−
C
−
C
0
∫
A
B
d
x
=
∫
A
if
0
≤
−
C
−
C
0
if
0
≤
B
B
0
d
x
−
∫
A
if
0
≤
−
C
−
C
0
if
0
≤
−
B
−
B
0
d
x
86
73
77
85
3eqtr4d
⊢
φ
→
∫
A
if
0
≤
−
C
−
C
0
B
d
x
=
if
0
≤
−
C
−
C
0
∫
A
B
d
x
87
68
86
oveq12d
⊢
φ
→
∫
A
if
0
≤
C
C
0
B
d
x
−
∫
A
if
0
≤
−
C
−
C
0
B
d
x
=
if
0
≤
C
C
0
∫
A
B
d
x
−
if
0
≤
−
C
−
C
0
∫
A
B
d
x
88
2
3
itgcl
⊢
φ
→
∫
A
B
d
x
∈
ℂ
89
13
18
88
subdird
⊢
φ
→
if
0
≤
C
C
0
−
if
0
≤
−
C
−
C
0
∫
A
B
d
x
=
if
0
≤
C
C
0
∫
A
B
d
x
−
if
0
≤
−
C
−
C
0
∫
A
B
d
x
90
4
7
syl
⊢
φ
→
if
0
≤
C
C
0
−
if
0
≤
−
C
−
C
0
=
C
91
90
oveq1d
⊢
φ
→
if
0
≤
C
C
0
−
if
0
≤
−
C
−
C
0
∫
A
B
d
x
=
C
∫
A
B
d
x
92
87
89
91
3eqtr2d
⊢
φ
→
∫
A
if
0
≤
C
C
0
B
d
x
−
∫
A
if
0
≤
−
C
−
C
0
B
d
x
=
C
∫
A
B
d
x
93
23
30
92
3eqtrrd
⊢
φ
→
C
∫
A
B
d
x
=
∫
A
C
B
d
x