Database
BASIC REAL AND COMPLEX ANALYSIS
Integrals
Lebesgue integration
Lesbesgue integral
itg2cnlem2
Next ⟩
itg2cn
Metamath Proof Explorer
Ascii
Unicode
Theorem
itg2cnlem2
Description:
Lemma for
itgcn
.
(Contributed by
Mario Carneiro
, 31-Aug-2014)
Ref
Expression
Hypotheses
itg2cn.1
⊢
φ
→
F
:
ℝ
⟶
0
+∞
itg2cn.2
⊢
φ
→
F
∈
MblFn
itg2cn.3
⊢
φ
→
∫
2
F
∈
ℝ
itg2cn.4
⊢
φ
→
C
∈
ℝ
+
itg2cn.5
⊢
φ
→
M
∈
ℕ
itg2cn.6
⊢
φ
→
¬
∫
2
x
∈
ℝ
⟼
if
F
x
≤
M
F
x
0
≤
∫
2
F
−
C
2
Assertion
itg2cnlem2
⊢
φ
→
∃
d
∈
ℝ
+
∀
u
∈
dom
vol
vol
u
<
d
→
∫
2
x
∈
ℝ
⟼
if
x
∈
u
F
x
0
<
C
Proof
Step
Hyp
Ref
Expression
1
itg2cn.1
⊢
φ
→
F
:
ℝ
⟶
0
+∞
2
itg2cn.2
⊢
φ
→
F
∈
MblFn
3
itg2cn.3
⊢
φ
→
∫
2
F
∈
ℝ
4
itg2cn.4
⊢
φ
→
C
∈
ℝ
+
5
itg2cn.5
⊢
φ
→
M
∈
ℕ
6
itg2cn.6
⊢
φ
→
¬
∫
2
x
∈
ℝ
⟼
if
F
x
≤
M
F
x
0
≤
∫
2
F
−
C
2
7
4
rphalfcld
⊢
φ
→
C
2
∈
ℝ
+
8
5
nnrpd
⊢
φ
→
M
∈
ℝ
+
9
7
8
rpdivcld
⊢
φ
→
C
2
M
∈
ℝ
+
10
simprl
⊢
φ
∧
u
∈
dom
vol
∧
vol
u
<
C
2
M
→
u
∈
dom
vol
11
2
adantr
⊢
φ
∧
u
∈
dom
vol
∧
vol
u
<
C
2
M
→
F
∈
MblFn
12
rge0ssre
⊢
0
+∞
⊆
ℝ
13
fss
⊢
F
:
ℝ
⟶
0
+∞
∧
0
+∞
⊆
ℝ
→
F
:
ℝ
⟶
ℝ
14
1
12
13
sylancl
⊢
φ
→
F
:
ℝ
⟶
ℝ
15
14
adantr
⊢
φ
∧
u
∈
dom
vol
∧
vol
u
<
C
2
M
→
F
:
ℝ
⟶
ℝ
16
mbfima
⊢
F
∈
MblFn
∧
F
:
ℝ
⟶
ℝ
→
F
-1
M
+∞
∈
dom
vol
17
11
15
16
syl2anc
⊢
φ
∧
u
∈
dom
vol
∧
vol
u
<
C
2
M
→
F
-1
M
+∞
∈
dom
vol
18
inmbl
⊢
u
∈
dom
vol
∧
F
-1
M
+∞
∈
dom
vol
→
u
∩
F
-1
M
+∞
∈
dom
vol
19
10
17
18
syl2anc
⊢
φ
∧
u
∈
dom
vol
∧
vol
u
<
C
2
M
→
u
∩
F
-1
M
+∞
∈
dom
vol
20
difmbl
⊢
u
∈
dom
vol
∧
F
-1
M
+∞
∈
dom
vol
→
u
∖
F
-1
M
+∞
∈
dom
vol
21
10
17
20
syl2anc
⊢
φ
∧
u
∈
dom
vol
∧
vol
u
<
C
2
M
→
u
∖
F
-1
M
+∞
∈
dom
vol
22
inass
⊢
u
∩
F
-1
M
+∞
∩
u
∖
F
-1
M
+∞
=
u
∩
F
-1
M
+∞
∩
u
∖
F
-1
M
+∞
23
disjdif
⊢
F
-1
M
+∞
∩
u
∖
F
-1
M
+∞
=
∅
24
23
ineq2i
⊢
u
∩
F
-1
M
+∞
∩
u
∖
F
-1
M
+∞
=
u
∩
∅
25
in0
⊢
u
∩
∅
=
∅
26
22
24
25
3eqtri
⊢
u
∩
F
-1
M
+∞
∩
u
∖
F
-1
M
+∞
=
∅
27
26
fveq2i
⊢
vol
*
u
∩
F
-1
M
+∞
∩
u
∖
F
-1
M
+∞
=
vol
*
∅
28
ovol0
⊢
vol
*
∅
=
0
29
27
28
eqtri
⊢
vol
*
u
∩
F
-1
M
+∞
∩
u
∖
F
-1
M
+∞
=
0
30
29
a1i
⊢
φ
∧
u
∈
dom
vol
∧
vol
u
<
C
2
M
→
vol
*
u
∩
F
-1
M
+∞
∩
u
∖
F
-1
M
+∞
=
0
31
inundif
⊢
u
∩
F
-1
M
+∞
∪
u
∖
F
-1
M
+∞
=
u
32
31
eqcomi
⊢
u
=
u
∩
F
-1
M
+∞
∪
u
∖
F
-1
M
+∞
33
32
a1i
⊢
φ
∧
u
∈
dom
vol
∧
vol
u
<
C
2
M
→
u
=
u
∩
F
-1
M
+∞
∪
u
∖
F
-1
M
+∞
34
mblss
⊢
u
∈
dom
vol
→
u
⊆
ℝ
35
10
34
syl
⊢
φ
∧
u
∈
dom
vol
∧
vol
u
<
C
2
M
→
u
⊆
ℝ
36
35
sselda
⊢
φ
∧
u
∈
dom
vol
∧
vol
u
<
C
2
M
∧
x
∈
u
→
x
∈
ℝ
37
1
adantr
⊢
φ
∧
u
∈
dom
vol
∧
vol
u
<
C
2
M
→
F
:
ℝ
⟶
0
+∞
38
37
ffvelrnda
⊢
φ
∧
u
∈
dom
vol
∧
vol
u
<
C
2
M
∧
x
∈
ℝ
→
F
x
∈
0
+∞
39
elrege0
⊢
F
x
∈
0
+∞
↔
F
x
∈
ℝ
∧
0
≤
F
x
40
38
39
sylib
⊢
φ
∧
u
∈
dom
vol
∧
vol
u
<
C
2
M
∧
x
∈
ℝ
→
F
x
∈
ℝ
∧
0
≤
F
x
41
40
simpld
⊢
φ
∧
u
∈
dom
vol
∧
vol
u
<
C
2
M
∧
x
∈
ℝ
→
F
x
∈
ℝ
42
41
rexrd
⊢
φ
∧
u
∈
dom
vol
∧
vol
u
<
C
2
M
∧
x
∈
ℝ
→
F
x
∈
ℝ
*
43
40
simprd
⊢
φ
∧
u
∈
dom
vol
∧
vol
u
<
C
2
M
∧
x
∈
ℝ
→
0
≤
F
x
44
elxrge0
⊢
F
x
∈
0
+∞
↔
F
x
∈
ℝ
*
∧
0
≤
F
x
45
42
43
44
sylanbrc
⊢
φ
∧
u
∈
dom
vol
∧
vol
u
<
C
2
M
∧
x
∈
ℝ
→
F
x
∈
0
+∞
46
36
45
syldan
⊢
φ
∧
u
∈
dom
vol
∧
vol
u
<
C
2
M
∧
x
∈
u
→
F
x
∈
0
+∞
47
eqid
⊢
x
∈
ℝ
⟼
if
x
∈
u
∩
F
-1
M
+∞
F
x
0
=
x
∈
ℝ
⟼
if
x
∈
u
∩
F
-1
M
+∞
F
x
0
48
eqid
⊢
x
∈
ℝ
⟼
if
x
∈
u
∖
F
-1
M
+∞
F
x
0
=
x
∈
ℝ
⟼
if
x
∈
u
∖
F
-1
M
+∞
F
x
0
49
eqid
⊢
x
∈
ℝ
⟼
if
x
∈
u
F
x
0
=
x
∈
ℝ
⟼
if
x
∈
u
F
x
0
50
0e0iccpnf
⊢
0
∈
0
+∞
51
ifcl
⊢
F
x
∈
0
+∞
∧
0
∈
0
+∞
→
if
x
∈
u
∩
F
-1
M
+∞
F
x
0
∈
0
+∞
52
45
50
51
sylancl
⊢
φ
∧
u
∈
dom
vol
∧
vol
u
<
C
2
M
∧
x
∈
ℝ
→
if
x
∈
u
∩
F
-1
M
+∞
F
x
0
∈
0
+∞
53
52
fmpttd
⊢
φ
∧
u
∈
dom
vol
∧
vol
u
<
C
2
M
→
x
∈
ℝ
⟼
if
x
∈
u
∩
F
-1
M
+∞
F
x
0
:
ℝ
⟶
0
+∞
54
3
adantr
⊢
φ
∧
u
∈
dom
vol
∧
vol
u
<
C
2
M
→
∫
2
F
∈
ℝ
55
icossicc
⊢
0
+∞
⊆
0
+∞
56
fss
⊢
F
:
ℝ
⟶
0
+∞
∧
0
+∞
⊆
0
+∞
→
F
:
ℝ
⟶
0
+∞
57
37
55
56
sylancl
⊢
φ
∧
u
∈
dom
vol
∧
vol
u
<
C
2
M
→
F
:
ℝ
⟶
0
+∞
58
41
leidd
⊢
φ
∧
u
∈
dom
vol
∧
vol
u
<
C
2
M
∧
x
∈
ℝ
→
F
x
≤
F
x
59
breq1
⊢
F
x
=
if
x
∈
u
∩
F
-1
M
+∞
F
x
0
→
F
x
≤
F
x
↔
if
x
∈
u
∩
F
-1
M
+∞
F
x
0
≤
F
x
60
breq1
⊢
0
=
if
x
∈
u
∩
F
-1
M
+∞
F
x
0
→
0
≤
F
x
↔
if
x
∈
u
∩
F
-1
M
+∞
F
x
0
≤
F
x
61
59
60
ifboth
⊢
F
x
≤
F
x
∧
0
≤
F
x
→
if
x
∈
u
∩
F
-1
M
+∞
F
x
0
≤
F
x
62
58
43
61
syl2anc
⊢
φ
∧
u
∈
dom
vol
∧
vol
u
<
C
2
M
∧
x
∈
ℝ
→
if
x
∈
u
∩
F
-1
M
+∞
F
x
0
≤
F
x
63
62
ralrimiva
⊢
φ
∧
u
∈
dom
vol
∧
vol
u
<
C
2
M
→
∀
x
∈
ℝ
if
x
∈
u
∩
F
-1
M
+∞
F
x
0
≤
F
x
64
reex
⊢
ℝ
∈
V
65
64
a1i
⊢
φ
∧
u
∈
dom
vol
∧
vol
u
<
C
2
M
→
ℝ
∈
V
66
eqidd
⊢
φ
∧
u
∈
dom
vol
∧
vol
u
<
C
2
M
→
x
∈
ℝ
⟼
if
x
∈
u
∩
F
-1
M
+∞
F
x
0
=
x
∈
ℝ
⟼
if
x
∈
u
∩
F
-1
M
+∞
F
x
0
67
37
feqmptd
⊢
φ
∧
u
∈
dom
vol
∧
vol
u
<
C
2
M
→
F
=
x
∈
ℝ
⟼
F
x
68
65
52
41
66
67
ofrfval2
⊢
φ
∧
u
∈
dom
vol
∧
vol
u
<
C
2
M
→
x
∈
ℝ
⟼
if
x
∈
u
∩
F
-1
M
+∞
F
x
0
≤
f
F
↔
∀
x
∈
ℝ
if
x
∈
u
∩
F
-1
M
+∞
F
x
0
≤
F
x
69
63
68
mpbird
⊢
φ
∧
u
∈
dom
vol
∧
vol
u
<
C
2
M
→
x
∈
ℝ
⟼
if
x
∈
u
∩
F
-1
M
+∞
F
x
0
≤
f
F
70
itg2le
⊢
x
∈
ℝ
⟼
if
x
∈
u
∩
F
-1
M
+∞
F
x
0
:
ℝ
⟶
0
+∞
∧
F
:
ℝ
⟶
0
+∞
∧
x
∈
ℝ
⟼
if
x
∈
u
∩
F
-1
M
+∞
F
x
0
≤
f
F
→
∫
2
x
∈
ℝ
⟼
if
x
∈
u
∩
F
-1
M
+∞
F
x
0
≤
∫
2
F
71
53
57
69
70
syl3anc
⊢
φ
∧
u
∈
dom
vol
∧
vol
u
<
C
2
M
→
∫
2
x
∈
ℝ
⟼
if
x
∈
u
∩
F
-1
M
+∞
F
x
0
≤
∫
2
F
72
itg2lecl
⊢
x
∈
ℝ
⟼
if
x
∈
u
∩
F
-1
M
+∞
F
x
0
:
ℝ
⟶
0
+∞
∧
∫
2
F
∈
ℝ
∧
∫
2
x
∈
ℝ
⟼
if
x
∈
u
∩
F
-1
M
+∞
F
x
0
≤
∫
2
F
→
∫
2
x
∈
ℝ
⟼
if
x
∈
u
∩
F
-1
M
+∞
F
x
0
∈
ℝ
73
53
54
71
72
syl3anc
⊢
φ
∧
u
∈
dom
vol
∧
vol
u
<
C
2
M
→
∫
2
x
∈
ℝ
⟼
if
x
∈
u
∩
F
-1
M
+∞
F
x
0
∈
ℝ
74
ifcl
⊢
F
x
∈
0
+∞
∧
0
∈
0
+∞
→
if
x
∈
u
∖
F
-1
M
+∞
F
x
0
∈
0
+∞
75
45
50
74
sylancl
⊢
φ
∧
u
∈
dom
vol
∧
vol
u
<
C
2
M
∧
x
∈
ℝ
→
if
x
∈
u
∖
F
-1
M
+∞
F
x
0
∈
0
+∞
76
75
fmpttd
⊢
φ
∧
u
∈
dom
vol
∧
vol
u
<
C
2
M
→
x
∈
ℝ
⟼
if
x
∈
u
∖
F
-1
M
+∞
F
x
0
:
ℝ
⟶
0
+∞
77
breq1
⊢
F
x
=
if
x
∈
u
∖
F
-1
M
+∞
F
x
0
→
F
x
≤
F
x
↔
if
x
∈
u
∖
F
-1
M
+∞
F
x
0
≤
F
x
78
breq1
⊢
0
=
if
x
∈
u
∖
F
-1
M
+∞
F
x
0
→
0
≤
F
x
↔
if
x
∈
u
∖
F
-1
M
+∞
F
x
0
≤
F
x
79
77
78
ifboth
⊢
F
x
≤
F
x
∧
0
≤
F
x
→
if
x
∈
u
∖
F
-1
M
+∞
F
x
0
≤
F
x
80
58
43
79
syl2anc
⊢
φ
∧
u
∈
dom
vol
∧
vol
u
<
C
2
M
∧
x
∈
ℝ
→
if
x
∈
u
∖
F
-1
M
+∞
F
x
0
≤
F
x
81
80
ralrimiva
⊢
φ
∧
u
∈
dom
vol
∧
vol
u
<
C
2
M
→
∀
x
∈
ℝ
if
x
∈
u
∖
F
-1
M
+∞
F
x
0
≤
F
x
82
eqidd
⊢
φ
∧
u
∈
dom
vol
∧
vol
u
<
C
2
M
→
x
∈
ℝ
⟼
if
x
∈
u
∖
F
-1
M
+∞
F
x
0
=
x
∈
ℝ
⟼
if
x
∈
u
∖
F
-1
M
+∞
F
x
0
83
65
75
41
82
67
ofrfval2
⊢
φ
∧
u
∈
dom
vol
∧
vol
u
<
C
2
M
→
x
∈
ℝ
⟼
if
x
∈
u
∖
F
-1
M
+∞
F
x
0
≤
f
F
↔
∀
x
∈
ℝ
if
x
∈
u
∖
F
-1
M
+∞
F
x
0
≤
F
x
84
81
83
mpbird
⊢
φ
∧
u
∈
dom
vol
∧
vol
u
<
C
2
M
→
x
∈
ℝ
⟼
if
x
∈
u
∖
F
-1
M
+∞
F
x
0
≤
f
F
85
itg2le
⊢
x
∈
ℝ
⟼
if
x
∈
u
∖
F
-1
M
+∞
F
x
0
:
ℝ
⟶
0
+∞
∧
F
:
ℝ
⟶
0
+∞
∧
x
∈
ℝ
⟼
if
x
∈
u
∖
F
-1
M
+∞
F
x
0
≤
f
F
→
∫
2
x
∈
ℝ
⟼
if
x
∈
u
∖
F
-1
M
+∞
F
x
0
≤
∫
2
F
86
76
57
84
85
syl3anc
⊢
φ
∧
u
∈
dom
vol
∧
vol
u
<
C
2
M
→
∫
2
x
∈
ℝ
⟼
if
x
∈
u
∖
F
-1
M
+∞
F
x
0
≤
∫
2
F
87
itg2lecl
⊢
x
∈
ℝ
⟼
if
x
∈
u
∖
F
-1
M
+∞
F
x
0
:
ℝ
⟶
0
+∞
∧
∫
2
F
∈
ℝ
∧
∫
2
x
∈
ℝ
⟼
if
x
∈
u
∖
F
-1
M
+∞
F
x
0
≤
∫
2
F
→
∫
2
x
∈
ℝ
⟼
if
x
∈
u
∖
F
-1
M
+∞
F
x
0
∈
ℝ
88
76
54
86
87
syl3anc
⊢
φ
∧
u
∈
dom
vol
∧
vol
u
<
C
2
M
→
∫
2
x
∈
ℝ
⟼
if
x
∈
u
∖
F
-1
M
+∞
F
x
0
∈
ℝ
89
19
21
30
33
46
47
48
49
73
88
itg2split
⊢
φ
∧
u
∈
dom
vol
∧
vol
u
<
C
2
M
→
∫
2
x
∈
ℝ
⟼
if
x
∈
u
F
x
0
=
∫
2
x
∈
ℝ
⟼
if
x
∈
u
∩
F
-1
M
+∞
F
x
0
+
∫
2
x
∈
ℝ
⟼
if
x
∈
u
∖
F
-1
M
+∞
F
x
0
90
4
adantr
⊢
φ
∧
u
∈
dom
vol
∧
vol
u
<
C
2
M
→
C
∈
ℝ
+
91
90
rphalfcld
⊢
φ
∧
u
∈
dom
vol
∧
vol
u
<
C
2
M
→
C
2
∈
ℝ
+
92
91
rpred
⊢
φ
∧
u
∈
dom
vol
∧
vol
u
<
C
2
M
→
C
2
∈
ℝ
93
ifcl
⊢
F
x
∈
0
+∞
∧
0
∈
0
+∞
→
if
x
∈
F
-1
M
+∞
F
x
0
∈
0
+∞
94
45
50
93
sylancl
⊢
φ
∧
u
∈
dom
vol
∧
vol
u
<
C
2
M
∧
x
∈
ℝ
→
if
x
∈
F
-1
M
+∞
F
x
0
∈
0
+∞
95
94
fmpttd
⊢
φ
∧
u
∈
dom
vol
∧
vol
u
<
C
2
M
→
x
∈
ℝ
⟼
if
x
∈
F
-1
M
+∞
F
x
0
:
ℝ
⟶
0
+∞
96
breq1
⊢
F
x
=
if
x
∈
F
-1
M
+∞
F
x
0
→
F
x
≤
F
x
↔
if
x
∈
F
-1
M
+∞
F
x
0
≤
F
x
97
breq1
⊢
0
=
if
x
∈
F
-1
M
+∞
F
x
0
→
0
≤
F
x
↔
if
x
∈
F
-1
M
+∞
F
x
0
≤
F
x
98
96
97
ifboth
⊢
F
x
≤
F
x
∧
0
≤
F
x
→
if
x
∈
F
-1
M
+∞
F
x
0
≤
F
x
99
58
43
98
syl2anc
⊢
φ
∧
u
∈
dom
vol
∧
vol
u
<
C
2
M
∧
x
∈
ℝ
→
if
x
∈
F
-1
M
+∞
F
x
0
≤
F
x
100
99
ralrimiva
⊢
φ
∧
u
∈
dom
vol
∧
vol
u
<
C
2
M
→
∀
x
∈
ℝ
if
x
∈
F
-1
M
+∞
F
x
0
≤
F
x
101
eqidd
⊢
φ
∧
u
∈
dom
vol
∧
vol
u
<
C
2
M
→
x
∈
ℝ
⟼
if
x
∈
F
-1
M
+∞
F
x
0
=
x
∈
ℝ
⟼
if
x
∈
F
-1
M
+∞
F
x
0
102
65
94
45
101
67
ofrfval2
⊢
φ
∧
u
∈
dom
vol
∧
vol
u
<
C
2
M
→
x
∈
ℝ
⟼
if
x
∈
F
-1
M
+∞
F
x
0
≤
f
F
↔
∀
x
∈
ℝ
if
x
∈
F
-1
M
+∞
F
x
0
≤
F
x
103
100
102
mpbird
⊢
φ
∧
u
∈
dom
vol
∧
vol
u
<
C
2
M
→
x
∈
ℝ
⟼
if
x
∈
F
-1
M
+∞
F
x
0
≤
f
F
104
itg2le
⊢
x
∈
ℝ
⟼
if
x
∈
F
-1
M
+∞
F
x
0
:
ℝ
⟶
0
+∞
∧
F
:
ℝ
⟶
0
+∞
∧
x
∈
ℝ
⟼
if
x
∈
F
-1
M
+∞
F
x
0
≤
f
F
→
∫
2
x
∈
ℝ
⟼
if
x
∈
F
-1
M
+∞
F
x
0
≤
∫
2
F
105
95
57
103
104
syl3anc
⊢
φ
∧
u
∈
dom
vol
∧
vol
u
<
C
2
M
→
∫
2
x
∈
ℝ
⟼
if
x
∈
F
-1
M
+∞
F
x
0
≤
∫
2
F
106
itg2lecl
⊢
x
∈
ℝ
⟼
if
x
∈
F
-1
M
+∞
F
x
0
:
ℝ
⟶
0
+∞
∧
∫
2
F
∈
ℝ
∧
∫
2
x
∈
ℝ
⟼
if
x
∈
F
-1
M
+∞
F
x
0
≤
∫
2
F
→
∫
2
x
∈
ℝ
⟼
if
x
∈
F
-1
M
+∞
F
x
0
∈
ℝ
107
95
54
105
106
syl3anc
⊢
φ
∧
u
∈
dom
vol
∧
vol
u
<
C
2
M
→
∫
2
x
∈
ℝ
⟼
if
x
∈
F
-1
M
+∞
F
x
0
∈
ℝ
108
0red
⊢
φ
∧
u
∈
dom
vol
∧
vol
u
<
C
2
M
∧
x
∈
ℝ
→
0
∈
ℝ
109
elinel2
⊢
x
∈
u
∩
F
-1
M
+∞
→
x
∈
F
-1
M
+∞
110
109
a1i
⊢
φ
∧
u
∈
dom
vol
∧
vol
u
<
C
2
M
∧
x
∈
ℝ
→
x
∈
u
∩
F
-1
M
+∞
→
x
∈
F
-1
M
+∞
111
ifle
⊢
F
x
∈
ℝ
∧
0
∈
ℝ
∧
0
≤
F
x
∧
x
∈
u
∩
F
-1
M
+∞
→
x
∈
F
-1
M
+∞
→
if
x
∈
u
∩
F
-1
M
+∞
F
x
0
≤
if
x
∈
F
-1
M
+∞
F
x
0
112
41
108
43
110
111
syl31anc
⊢
φ
∧
u
∈
dom
vol
∧
vol
u
<
C
2
M
∧
x
∈
ℝ
→
if
x
∈
u
∩
F
-1
M
+∞
F
x
0
≤
if
x
∈
F
-1
M
+∞
F
x
0
113
112
ralrimiva
⊢
φ
∧
u
∈
dom
vol
∧
vol
u
<
C
2
M
→
∀
x
∈
ℝ
if
x
∈
u
∩
F
-1
M
+∞
F
x
0
≤
if
x
∈
F
-1
M
+∞
F
x
0
114
65
52
94
66
101
ofrfval2
⊢
φ
∧
u
∈
dom
vol
∧
vol
u
<
C
2
M
→
x
∈
ℝ
⟼
if
x
∈
u
∩
F
-1
M
+∞
F
x
0
≤
f
x
∈
ℝ
⟼
if
x
∈
F
-1
M
+∞
F
x
0
↔
∀
x
∈
ℝ
if
x
∈
u
∩
F
-1
M
+∞
F
x
0
≤
if
x
∈
F
-1
M
+∞
F
x
0
115
113
114
mpbird
⊢
φ
∧
u
∈
dom
vol
∧
vol
u
<
C
2
M
→
x
∈
ℝ
⟼
if
x
∈
u
∩
F
-1
M
+∞
F
x
0
≤
f
x
∈
ℝ
⟼
if
x
∈
F
-1
M
+∞
F
x
0
116
itg2le
⊢
x
∈
ℝ
⟼
if
x
∈
u
∩
F
-1
M
+∞
F
x
0
:
ℝ
⟶
0
+∞
∧
x
∈
ℝ
⟼
if
x
∈
F
-1
M
+∞
F
x
0
:
ℝ
⟶
0
+∞
∧
x
∈
ℝ
⟼
if
x
∈
u
∩
F
-1
M
+∞
F
x
0
≤
f
x
∈
ℝ
⟼
if
x
∈
F
-1
M
+∞
F
x
0
→
∫
2
x
∈
ℝ
⟼
if
x
∈
u
∩
F
-1
M
+∞
F
x
0
≤
∫
2
x
∈
ℝ
⟼
if
x
∈
F
-1
M
+∞
F
x
0
117
53
95
115
116
syl3anc
⊢
φ
∧
u
∈
dom
vol
∧
vol
u
<
C
2
M
→
∫
2
x
∈
ℝ
⟼
if
x
∈
u
∩
F
-1
M
+∞
F
x
0
≤
∫
2
x
∈
ℝ
⟼
if
x
∈
F
-1
M
+∞
F
x
0
118
67
fveq2d
⊢
φ
∧
u
∈
dom
vol
∧
vol
u
<
C
2
M
→
∫
2
F
=
∫
2
x
∈
ℝ
⟼
F
x
119
cmmbl
⊢
F
-1
M
+∞
∈
dom
vol
→
ℝ
∖
F
-1
M
+∞
∈
dom
vol
120
17
119
syl
⊢
φ
∧
u
∈
dom
vol
∧
vol
u
<
C
2
M
→
ℝ
∖
F
-1
M
+∞
∈
dom
vol
121
disjdif
⊢
F
-1
M
+∞
∩
ℝ
∖
F
-1
M
+∞
=
∅
122
121
fveq2i
⊢
vol
*
F
-1
M
+∞
∩
ℝ
∖
F
-1
M
+∞
=
vol
*
∅
123
122
28
eqtri
⊢
vol
*
F
-1
M
+∞
∩
ℝ
∖
F
-1
M
+∞
=
0
124
123
a1i
⊢
φ
∧
u
∈
dom
vol
∧
vol
u
<
C
2
M
→
vol
*
F
-1
M
+∞
∩
ℝ
∖
F
-1
M
+∞
=
0
125
undif2
⊢
F
-1
M
+∞
∪
ℝ
∖
F
-1
M
+∞
=
F
-1
M
+∞
∪
ℝ
126
mblss
⊢
F
-1
M
+∞
∈
dom
vol
→
F
-1
M
+∞
⊆
ℝ
127
17
126
syl
⊢
φ
∧
u
∈
dom
vol
∧
vol
u
<
C
2
M
→
F
-1
M
+∞
⊆
ℝ
128
ssequn1
⊢
F
-1
M
+∞
⊆
ℝ
↔
F
-1
M
+∞
∪
ℝ
=
ℝ
129
127
128
sylib
⊢
φ
∧
u
∈
dom
vol
∧
vol
u
<
C
2
M
→
F
-1
M
+∞
∪
ℝ
=
ℝ
130
125
129
eqtr2id
⊢
φ
∧
u
∈
dom
vol
∧
vol
u
<
C
2
M
→
ℝ
=
F
-1
M
+∞
∪
ℝ
∖
F
-1
M
+∞
131
eqid
⊢
x
∈
ℝ
⟼
if
x
∈
F
-1
M
+∞
F
x
0
=
x
∈
ℝ
⟼
if
x
∈
F
-1
M
+∞
F
x
0
132
eqid
⊢
x
∈
ℝ
⟼
if
x
∈
ℝ
∖
F
-1
M
+∞
F
x
0
=
x
∈
ℝ
⟼
if
x
∈
ℝ
∖
F
-1
M
+∞
F
x
0
133
iftrue
⊢
x
∈
ℝ
→
if
x
∈
ℝ
F
x
0
=
F
x
134
133
mpteq2ia
⊢
x
∈
ℝ
⟼
if
x
∈
ℝ
F
x
0
=
x
∈
ℝ
⟼
F
x
135
134
eqcomi
⊢
x
∈
ℝ
⟼
F
x
=
x
∈
ℝ
⟼
if
x
∈
ℝ
F
x
0
136
ifcl
⊢
F
x
∈
0
+∞
∧
0
∈
0
+∞
→
if
x
∈
ℝ
∖
F
-1
M
+∞
F
x
0
∈
0
+∞
137
45
50
136
sylancl
⊢
φ
∧
u
∈
dom
vol
∧
vol
u
<
C
2
M
∧
x
∈
ℝ
→
if
x
∈
ℝ
∖
F
-1
M
+∞
F
x
0
∈
0
+∞
138
137
fmpttd
⊢
φ
∧
u
∈
dom
vol
∧
vol
u
<
C
2
M
→
x
∈
ℝ
⟼
if
x
∈
ℝ
∖
F
-1
M
+∞
F
x
0
:
ℝ
⟶
0
+∞
139
breq1
⊢
F
x
=
if
x
∈
ℝ
∖
F
-1
M
+∞
F
x
0
→
F
x
≤
F
x
↔
if
x
∈
ℝ
∖
F
-1
M
+∞
F
x
0
≤
F
x
140
breq1
⊢
0
=
if
x
∈
ℝ
∖
F
-1
M
+∞
F
x
0
→
0
≤
F
x
↔
if
x
∈
ℝ
∖
F
-1
M
+∞
F
x
0
≤
F
x
141
139
140
ifboth
⊢
F
x
≤
F
x
∧
0
≤
F
x
→
if
x
∈
ℝ
∖
F
-1
M
+∞
F
x
0
≤
F
x
142
58
43
141
syl2anc
⊢
φ
∧
u
∈
dom
vol
∧
vol
u
<
C
2
M
∧
x
∈
ℝ
→
if
x
∈
ℝ
∖
F
-1
M
+∞
F
x
0
≤
F
x
143
142
ralrimiva
⊢
φ
∧
u
∈
dom
vol
∧
vol
u
<
C
2
M
→
∀
x
∈
ℝ
if
x
∈
ℝ
∖
F
-1
M
+∞
F
x
0
≤
F
x
144
eqidd
⊢
φ
∧
u
∈
dom
vol
∧
vol
u
<
C
2
M
→
x
∈
ℝ
⟼
if
x
∈
ℝ
∖
F
-1
M
+∞
F
x
0
=
x
∈
ℝ
⟼
if
x
∈
ℝ
∖
F
-1
M
+∞
F
x
0
145
65
137
45
144
67
ofrfval2
⊢
φ
∧
u
∈
dom
vol
∧
vol
u
<
C
2
M
→
x
∈
ℝ
⟼
if
x
∈
ℝ
∖
F
-1
M
+∞
F
x
0
≤
f
F
↔
∀
x
∈
ℝ
if
x
∈
ℝ
∖
F
-1
M
+∞
F
x
0
≤
F
x
146
143
145
mpbird
⊢
φ
∧
u
∈
dom
vol
∧
vol
u
<
C
2
M
→
x
∈
ℝ
⟼
if
x
∈
ℝ
∖
F
-1
M
+∞
F
x
0
≤
f
F
147
itg2le
⊢
x
∈
ℝ
⟼
if
x
∈
ℝ
∖
F
-1
M
+∞
F
x
0
:
ℝ
⟶
0
+∞
∧
F
:
ℝ
⟶
0
+∞
∧
x
∈
ℝ
⟼
if
x
∈
ℝ
∖
F
-1
M
+∞
F
x
0
≤
f
F
→
∫
2
x
∈
ℝ
⟼
if
x
∈
ℝ
∖
F
-1
M
+∞
F
x
0
≤
∫
2
F
148
138
57
146
147
syl3anc
⊢
φ
∧
u
∈
dom
vol
∧
vol
u
<
C
2
M
→
∫
2
x
∈
ℝ
⟼
if
x
∈
ℝ
∖
F
-1
M
+∞
F
x
0
≤
∫
2
F
149
itg2lecl
⊢
x
∈
ℝ
⟼
if
x
∈
ℝ
∖
F
-1
M
+∞
F
x
0
:
ℝ
⟶
0
+∞
∧
∫
2
F
∈
ℝ
∧
∫
2
x
∈
ℝ
⟼
if
x
∈
ℝ
∖
F
-1
M
+∞
F
x
0
≤
∫
2
F
→
∫
2
x
∈
ℝ
⟼
if
x
∈
ℝ
∖
F
-1
M
+∞
F
x
0
∈
ℝ
150
138
54
148
149
syl3anc
⊢
φ
∧
u
∈
dom
vol
∧
vol
u
<
C
2
M
→
∫
2
x
∈
ℝ
⟼
if
x
∈
ℝ
∖
F
-1
M
+∞
F
x
0
∈
ℝ
151
17
120
124
130
45
131
132
135
107
150
itg2split
⊢
φ
∧
u
∈
dom
vol
∧
vol
u
<
C
2
M
→
∫
2
x
∈
ℝ
⟼
F
x
=
∫
2
x
∈
ℝ
⟼
if
x
∈
F
-1
M
+∞
F
x
0
+
∫
2
x
∈
ℝ
⟼
if
x
∈
ℝ
∖
F
-1
M
+∞
F
x
0
152
118
151
eqtrd
⊢
φ
∧
u
∈
dom
vol
∧
vol
u
<
C
2
M
→
∫
2
F
=
∫
2
x
∈
ℝ
⟼
if
x
∈
F
-1
M
+∞
F
x
0
+
∫
2
x
∈
ℝ
⟼
if
x
∈
ℝ
∖
F
-1
M
+∞
F
x
0
153
eldif
⊢
x
∈
ℝ
∖
F
-1
M
+∞
↔
x
∈
ℝ
∧
¬
x
∈
F
-1
M
+∞
154
153
baib
⊢
x
∈
ℝ
→
x
∈
ℝ
∖
F
-1
M
+∞
↔
¬
x
∈
F
-1
M
+∞
155
154
adantl
⊢
φ
∧
u
∈
dom
vol
∧
vol
u
<
C
2
M
∧
x
∈
ℝ
→
x
∈
ℝ
∖
F
-1
M
+∞
↔
¬
x
∈
F
-1
M
+∞
156
1
ffnd
⊢
φ
→
F
Fn
ℝ
157
156
ad2antrr
⊢
φ
∧
u
∈
dom
vol
∧
vol
u
<
C
2
M
∧
x
∈
ℝ
→
F
Fn
ℝ
158
elpreima
⊢
F
Fn
ℝ
→
x
∈
F
-1
M
+∞
↔
x
∈
ℝ
∧
F
x
∈
M
+∞
159
157
158
syl
⊢
φ
∧
u
∈
dom
vol
∧
vol
u
<
C
2
M
∧
x
∈
ℝ
→
x
∈
F
-1
M
+∞
↔
x
∈
ℝ
∧
F
x
∈
M
+∞
160
41
biantrurd
⊢
φ
∧
u
∈
dom
vol
∧
vol
u
<
C
2
M
∧
x
∈
ℝ
→
M
<
F
x
↔
F
x
∈
ℝ
∧
M
<
F
x
161
5
nnred
⊢
φ
→
M
∈
ℝ
162
161
ad2antrr
⊢
φ
∧
u
∈
dom
vol
∧
vol
u
<
C
2
M
∧
x
∈
ℝ
→
M
∈
ℝ
163
162
rexrd
⊢
φ
∧
u
∈
dom
vol
∧
vol
u
<
C
2
M
∧
x
∈
ℝ
→
M
∈
ℝ
*
164
elioopnf
⊢
M
∈
ℝ
*
→
F
x
∈
M
+∞
↔
F
x
∈
ℝ
∧
M
<
F
x
165
163
164
syl
⊢
φ
∧
u
∈
dom
vol
∧
vol
u
<
C
2
M
∧
x
∈
ℝ
→
F
x
∈
M
+∞
↔
F
x
∈
ℝ
∧
M
<
F
x
166
simpr
⊢
φ
∧
u
∈
dom
vol
∧
vol
u
<
C
2
M
∧
x
∈
ℝ
→
x
∈
ℝ
167
166
biantrurd
⊢
φ
∧
u
∈
dom
vol
∧
vol
u
<
C
2
M
∧
x
∈
ℝ
→
F
x
∈
M
+∞
↔
x
∈
ℝ
∧
F
x
∈
M
+∞
168
160
165
167
3bitr2d
⊢
φ
∧
u
∈
dom
vol
∧
vol
u
<
C
2
M
∧
x
∈
ℝ
→
M
<
F
x
↔
x
∈
ℝ
∧
F
x
∈
M
+∞
169
162
41
ltnled
⊢
φ
∧
u
∈
dom
vol
∧
vol
u
<
C
2
M
∧
x
∈
ℝ
→
M
<
F
x
↔
¬
F
x
≤
M
170
159
168
169
3bitr2rd
⊢
φ
∧
u
∈
dom
vol
∧
vol
u
<
C
2
M
∧
x
∈
ℝ
→
¬
F
x
≤
M
↔
x
∈
F
-1
M
+∞
171
170
con1bid
⊢
φ
∧
u
∈
dom
vol
∧
vol
u
<
C
2
M
∧
x
∈
ℝ
→
¬
x
∈
F
-1
M
+∞
↔
F
x
≤
M
172
155
171
bitrd
⊢
φ
∧
u
∈
dom
vol
∧
vol
u
<
C
2
M
∧
x
∈
ℝ
→
x
∈
ℝ
∖
F
-1
M
+∞
↔
F
x
≤
M
173
172
ifbid
⊢
φ
∧
u
∈
dom
vol
∧
vol
u
<
C
2
M
∧
x
∈
ℝ
→
if
x
∈
ℝ
∖
F
-1
M
+∞
F
x
0
=
if
F
x
≤
M
F
x
0
174
173
mpteq2dva
⊢
φ
∧
u
∈
dom
vol
∧
vol
u
<
C
2
M
→
x
∈
ℝ
⟼
if
x
∈
ℝ
∖
F
-1
M
+∞
F
x
0
=
x
∈
ℝ
⟼
if
F
x
≤
M
F
x
0
175
174
fveq2d
⊢
φ
∧
u
∈
dom
vol
∧
vol
u
<
C
2
M
→
∫
2
x
∈
ℝ
⟼
if
x
∈
ℝ
∖
F
-1
M
+∞
F
x
0
=
∫
2
x
∈
ℝ
⟼
if
F
x
≤
M
F
x
0
176
6
adantr
⊢
φ
∧
u
∈
dom
vol
∧
vol
u
<
C
2
M
→
¬
∫
2
x
∈
ℝ
⟼
if
F
x
≤
M
F
x
0
≤
∫
2
F
−
C
2
177
175
176
eqnbrtrd
⊢
φ
∧
u
∈
dom
vol
∧
vol
u
<
C
2
M
→
¬
∫
2
x
∈
ℝ
⟼
if
x
∈
ℝ
∖
F
-1
M
+∞
F
x
0
≤
∫
2
F
−
C
2
178
54
92
resubcld
⊢
φ
∧
u
∈
dom
vol
∧
vol
u
<
C
2
M
→
∫
2
F
−
C
2
∈
ℝ
179
178
150
ltnled
⊢
φ
∧
u
∈
dom
vol
∧
vol
u
<
C
2
M
→
∫
2
F
−
C
2
<
∫
2
x
∈
ℝ
⟼
if
x
∈
ℝ
∖
F
-1
M
+∞
F
x
0
↔
¬
∫
2
x
∈
ℝ
⟼
if
x
∈
ℝ
∖
F
-1
M
+∞
F
x
0
≤
∫
2
F
−
C
2
180
177
179
mpbird
⊢
φ
∧
u
∈
dom
vol
∧
vol
u
<
C
2
M
→
∫
2
F
−
C
2
<
∫
2
x
∈
ℝ
⟼
if
x
∈
ℝ
∖
F
-1
M
+∞
F
x
0
181
54
92
150
ltsubadd2d
⊢
φ
∧
u
∈
dom
vol
∧
vol
u
<
C
2
M
→
∫
2
F
−
C
2
<
∫
2
x
∈
ℝ
⟼
if
x
∈
ℝ
∖
F
-1
M
+∞
F
x
0
↔
∫
2
F
<
C
2
+
∫
2
x
∈
ℝ
⟼
if
x
∈
ℝ
∖
F
-1
M
+∞
F
x
0
182
180
181
mpbid
⊢
φ
∧
u
∈
dom
vol
∧
vol
u
<
C
2
M
→
∫
2
F
<
C
2
+
∫
2
x
∈
ℝ
⟼
if
x
∈
ℝ
∖
F
-1
M
+∞
F
x
0
183
152
182
eqbrtrrd
⊢
φ
∧
u
∈
dom
vol
∧
vol
u
<
C
2
M
→
∫
2
x
∈
ℝ
⟼
if
x
∈
F
-1
M
+∞
F
x
0
+
∫
2
x
∈
ℝ
⟼
if
x
∈
ℝ
∖
F
-1
M
+∞
F
x
0
<
C
2
+
∫
2
x
∈
ℝ
⟼
if
x
∈
ℝ
∖
F
-1
M
+∞
F
x
0
184
107
92
150
ltadd1d
⊢
φ
∧
u
∈
dom
vol
∧
vol
u
<
C
2
M
→
∫
2
x
∈
ℝ
⟼
if
x
∈
F
-1
M
+∞
F
x
0
<
C
2
↔
∫
2
x
∈
ℝ
⟼
if
x
∈
F
-1
M
+∞
F
x
0
+
∫
2
x
∈
ℝ
⟼
if
x
∈
ℝ
∖
F
-1
M
+∞
F
x
0
<
C
2
+
∫
2
x
∈
ℝ
⟼
if
x
∈
ℝ
∖
F
-1
M
+∞
F
x
0
185
183
184
mpbird
⊢
φ
∧
u
∈
dom
vol
∧
vol
u
<
C
2
M
→
∫
2
x
∈
ℝ
⟼
if
x
∈
F
-1
M
+∞
F
x
0
<
C
2
186
73
107
92
117
185
lelttrd
⊢
φ
∧
u
∈
dom
vol
∧
vol
u
<
C
2
M
→
∫
2
x
∈
ℝ
⟼
if
x
∈
u
∩
F
-1
M
+∞
F
x
0
<
C
2
187
161
adantr
⊢
φ
∧
u
∈
dom
vol
∧
vol
u
<
C
2
M
→
M
∈
ℝ
188
mblvol
⊢
u
∈
dom
vol
→
vol
u
=
vol
*
u
189
10
188
syl
⊢
φ
∧
u
∈
dom
vol
∧
vol
u
<
C
2
M
→
vol
u
=
vol
*
u
190
9
rpred
⊢
φ
→
C
2
M
∈
ℝ
191
190
adantr
⊢
φ
∧
u
∈
dom
vol
∧
vol
u
<
C
2
M
→
C
2
M
∈
ℝ
192
ovolcl
⊢
u
⊆
ℝ
→
vol
*
u
∈
ℝ
*
193
35
192
syl
⊢
φ
∧
u
∈
dom
vol
∧
vol
u
<
C
2
M
→
vol
*
u
∈
ℝ
*
194
191
rexrd
⊢
φ
∧
u
∈
dom
vol
∧
vol
u
<
C
2
M
→
C
2
M
∈
ℝ
*
195
simprr
⊢
φ
∧
u
∈
dom
vol
∧
vol
u
<
C
2
M
→
vol
u
<
C
2
M
196
189
195
eqbrtrrd
⊢
φ
∧
u
∈
dom
vol
∧
vol
u
<
C
2
M
→
vol
*
u
<
C
2
M
197
193
194
196
xrltled
⊢
φ
∧
u
∈
dom
vol
∧
vol
u
<
C
2
M
→
vol
*
u
≤
C
2
M
198
ovollecl
⊢
u
⊆
ℝ
∧
C
2
M
∈
ℝ
∧
vol
*
u
≤
C
2
M
→
vol
*
u
∈
ℝ
199
35
191
197
198
syl3anc
⊢
φ
∧
u
∈
dom
vol
∧
vol
u
<
C
2
M
→
vol
*
u
∈
ℝ
200
189
199
eqeltrd
⊢
φ
∧
u
∈
dom
vol
∧
vol
u
<
C
2
M
→
vol
u
∈
ℝ
201
187
200
remulcld
⊢
φ
∧
u
∈
dom
vol
∧
vol
u
<
C
2
M
→
M
vol
u
∈
ℝ
202
187
rexrd
⊢
φ
∧
u
∈
dom
vol
∧
vol
u
<
C
2
M
→
M
∈
ℝ
*
203
5
adantr
⊢
φ
∧
u
∈
dom
vol
∧
vol
u
<
C
2
M
→
M
∈
ℕ
204
203
nnnn0d
⊢
φ
∧
u
∈
dom
vol
∧
vol
u
<
C
2
M
→
M
∈
ℕ
0
205
204
nn0ge0d
⊢
φ
∧
u
∈
dom
vol
∧
vol
u
<
C
2
M
→
0
≤
M
206
elxrge0
⊢
M
∈
0
+∞
↔
M
∈
ℝ
*
∧
0
≤
M
207
202
205
206
sylanbrc
⊢
φ
∧
u
∈
dom
vol
∧
vol
u
<
C
2
M
→
M
∈
0
+∞
208
ifcl
⊢
M
∈
0
+∞
∧
0
∈
0
+∞
→
if
x
∈
u
M
0
∈
0
+∞
209
207
50
208
sylancl
⊢
φ
∧
u
∈
dom
vol
∧
vol
u
<
C
2
M
→
if
x
∈
u
M
0
∈
0
+∞
210
209
adantr
⊢
φ
∧
u
∈
dom
vol
∧
vol
u
<
C
2
M
∧
x
∈
ℝ
→
if
x
∈
u
M
0
∈
0
+∞
211
210
fmpttd
⊢
φ
∧
u
∈
dom
vol
∧
vol
u
<
C
2
M
→
x
∈
ℝ
⟼
if
x
∈
u
M
0
:
ℝ
⟶
0
+∞
212
eldifn
⊢
x
∈
u
∖
F
-1
M
+∞
→
¬
x
∈
F
-1
M
+∞
213
212
adantl
⊢
φ
∧
u
∈
dom
vol
∧
vol
u
<
C
2
M
∧
x
∈
u
∖
F
-1
M
+∞
→
¬
x
∈
F
-1
M
+∞
214
difssd
⊢
φ
∧
u
∈
dom
vol
∧
vol
u
<
C
2
M
→
u
∖
F
-1
M
+∞
⊆
u
215
214
sselda
⊢
φ
∧
u
∈
dom
vol
∧
vol
u
<
C
2
M
∧
x
∈
u
∖
F
-1
M
+∞
→
x
∈
u
216
36
170
syldan
⊢
φ
∧
u
∈
dom
vol
∧
vol
u
<
C
2
M
∧
x
∈
u
→
¬
F
x
≤
M
↔
x
∈
F
-1
M
+∞
217
215
216
syldan
⊢
φ
∧
u
∈
dom
vol
∧
vol
u
<
C
2
M
∧
x
∈
u
∖
F
-1
M
+∞
→
¬
F
x
≤
M
↔
x
∈
F
-1
M
+∞
218
217
con1bid
⊢
φ
∧
u
∈
dom
vol
∧
vol
u
<
C
2
M
∧
x
∈
u
∖
F
-1
M
+∞
→
¬
x
∈
F
-1
M
+∞
↔
F
x
≤
M
219
213
218
mpbid
⊢
φ
∧
u
∈
dom
vol
∧
vol
u
<
C
2
M
∧
x
∈
u
∖
F
-1
M
+∞
→
F
x
≤
M
220
iftrue
⊢
x
∈
u
∖
F
-1
M
+∞
→
if
x
∈
u
∖
F
-1
M
+∞
F
x
0
=
F
x
221
220
adantl
⊢
φ
∧
u
∈
dom
vol
∧
vol
u
<
C
2
M
∧
x
∈
u
∖
F
-1
M
+∞
→
if
x
∈
u
∖
F
-1
M
+∞
F
x
0
=
F
x
222
215
iftrued
⊢
φ
∧
u
∈
dom
vol
∧
vol
u
<
C
2
M
∧
x
∈
u
∖
F
-1
M
+∞
→
if
x
∈
u
M
0
=
M
223
219
221
222
3brtr4d
⊢
φ
∧
u
∈
dom
vol
∧
vol
u
<
C
2
M
∧
x
∈
u
∖
F
-1
M
+∞
→
if
x
∈
u
∖
F
-1
M
+∞
F
x
0
≤
if
x
∈
u
M
0
224
iffalse
⊢
¬
x
∈
u
∖
F
-1
M
+∞
→
if
x
∈
u
∖
F
-1
M
+∞
F
x
0
=
0
225
224
adantl
⊢
φ
∧
u
∈
dom
vol
∧
vol
u
<
C
2
M
∧
¬
x
∈
u
∖
F
-1
M
+∞
→
if
x
∈
u
∖
F
-1
M
+∞
F
x
0
=
0
226
0le0
⊢
0
≤
0
227
breq2
⊢
M
=
if
x
∈
u
M
0
→
0
≤
M
↔
0
≤
if
x
∈
u
M
0
228
breq2
⊢
0
=
if
x
∈
u
M
0
→
0
≤
0
↔
0
≤
if
x
∈
u
M
0
229
227
228
ifboth
⊢
0
≤
M
∧
0
≤
0
→
0
≤
if
x
∈
u
M
0
230
205
226
229
sylancl
⊢
φ
∧
u
∈
dom
vol
∧
vol
u
<
C
2
M
→
0
≤
if
x
∈
u
M
0
231
230
adantr
⊢
φ
∧
u
∈
dom
vol
∧
vol
u
<
C
2
M
∧
¬
x
∈
u
∖
F
-1
M
+∞
→
0
≤
if
x
∈
u
M
0
232
225
231
eqbrtrd
⊢
φ
∧
u
∈
dom
vol
∧
vol
u
<
C
2
M
∧
¬
x
∈
u
∖
F
-1
M
+∞
→
if
x
∈
u
∖
F
-1
M
+∞
F
x
0
≤
if
x
∈
u
M
0
233
223
232
pm2.61dan
⊢
φ
∧
u
∈
dom
vol
∧
vol
u
<
C
2
M
→
if
x
∈
u
∖
F
-1
M
+∞
F
x
0
≤
if
x
∈
u
M
0
234
233
ralrimivw
⊢
φ
∧
u
∈
dom
vol
∧
vol
u
<
C
2
M
→
∀
x
∈
ℝ
if
x
∈
u
∖
F
-1
M
+∞
F
x
0
≤
if
x
∈
u
M
0
235
eqidd
⊢
φ
∧
u
∈
dom
vol
∧
vol
u
<
C
2
M
→
x
∈
ℝ
⟼
if
x
∈
u
M
0
=
x
∈
ℝ
⟼
if
x
∈
u
M
0
236
65
75
210
82
235
ofrfval2
⊢
φ
∧
u
∈
dom
vol
∧
vol
u
<
C
2
M
→
x
∈
ℝ
⟼
if
x
∈
u
∖
F
-1
M
+∞
F
x
0
≤
f
x
∈
ℝ
⟼
if
x
∈
u
M
0
↔
∀
x
∈
ℝ
if
x
∈
u
∖
F
-1
M
+∞
F
x
0
≤
if
x
∈
u
M
0
237
234
236
mpbird
⊢
φ
∧
u
∈
dom
vol
∧
vol
u
<
C
2
M
→
x
∈
ℝ
⟼
if
x
∈
u
∖
F
-1
M
+∞
F
x
0
≤
f
x
∈
ℝ
⟼
if
x
∈
u
M
0
238
itg2le
⊢
x
∈
ℝ
⟼
if
x
∈
u
∖
F
-1
M
+∞
F
x
0
:
ℝ
⟶
0
+∞
∧
x
∈
ℝ
⟼
if
x
∈
u
M
0
:
ℝ
⟶
0
+∞
∧
x
∈
ℝ
⟼
if
x
∈
u
∖
F
-1
M
+∞
F
x
0
≤
f
x
∈
ℝ
⟼
if
x
∈
u
M
0
→
∫
2
x
∈
ℝ
⟼
if
x
∈
u
∖
F
-1
M
+∞
F
x
0
≤
∫
2
x
∈
ℝ
⟼
if
x
∈
u
M
0
239
76
211
237
238
syl3anc
⊢
φ
∧
u
∈
dom
vol
∧
vol
u
<
C
2
M
→
∫
2
x
∈
ℝ
⟼
if
x
∈
u
∖
F
-1
M
+∞
F
x
0
≤
∫
2
x
∈
ℝ
⟼
if
x
∈
u
M
0
240
elrege0
⊢
M
∈
0
+∞
↔
M
∈
ℝ
∧
0
≤
M
241
187
205
240
sylanbrc
⊢
φ
∧
u
∈
dom
vol
∧
vol
u
<
C
2
M
→
M
∈
0
+∞
242
itg2const
⊢
u
∈
dom
vol
∧
vol
u
∈
ℝ
∧
M
∈
0
+∞
→
∫
2
x
∈
ℝ
⟼
if
x
∈
u
M
0
=
M
vol
u
243
10
200
241
242
syl3anc
⊢
φ
∧
u
∈
dom
vol
∧
vol
u
<
C
2
M
→
∫
2
x
∈
ℝ
⟼
if
x
∈
u
M
0
=
M
vol
u
244
239
243
breqtrd
⊢
φ
∧
u
∈
dom
vol
∧
vol
u
<
C
2
M
→
∫
2
x
∈
ℝ
⟼
if
x
∈
u
∖
F
-1
M
+∞
F
x
0
≤
M
vol
u
245
203
nngt0d
⊢
φ
∧
u
∈
dom
vol
∧
vol
u
<
C
2
M
→
0
<
M
246
ltmuldiv2
⊢
vol
u
∈
ℝ
∧
C
2
∈
ℝ
∧
M
∈
ℝ
∧
0
<
M
→
M
vol
u
<
C
2
↔
vol
u
<
C
2
M
247
200
92
187
245
246
syl112anc
⊢
φ
∧
u
∈
dom
vol
∧
vol
u
<
C
2
M
→
M
vol
u
<
C
2
↔
vol
u
<
C
2
M
248
195
247
mpbird
⊢
φ
∧
u
∈
dom
vol
∧
vol
u
<
C
2
M
→
M
vol
u
<
C
2
249
88
201
92
244
248
lelttrd
⊢
φ
∧
u
∈
dom
vol
∧
vol
u
<
C
2
M
→
∫
2
x
∈
ℝ
⟼
if
x
∈
u
∖
F
-1
M
+∞
F
x
0
<
C
2
250
73
88
92
92
186
249
lt2addd
⊢
φ
∧
u
∈
dom
vol
∧
vol
u
<
C
2
M
→
∫
2
x
∈
ℝ
⟼
if
x
∈
u
∩
F
-1
M
+∞
F
x
0
+
∫
2
x
∈
ℝ
⟼
if
x
∈
u
∖
F
-1
M
+∞
F
x
0
<
C
2
+
C
2
251
89
250
eqbrtrd
⊢
φ
∧
u
∈
dom
vol
∧
vol
u
<
C
2
M
→
∫
2
x
∈
ℝ
⟼
if
x
∈
u
F
x
0
<
C
2
+
C
2
252
90
rpcnd
⊢
φ
∧
u
∈
dom
vol
∧
vol
u
<
C
2
M
→
C
∈
ℂ
253
252
2halvesd
⊢
φ
∧
u
∈
dom
vol
∧
vol
u
<
C
2
M
→
C
2
+
C
2
=
C
254
251
253
breqtrd
⊢
φ
∧
u
∈
dom
vol
∧
vol
u
<
C
2
M
→
∫
2
x
∈
ℝ
⟼
if
x
∈
u
F
x
0
<
C
255
254
expr
⊢
φ
∧
u
∈
dom
vol
→
vol
u
<
C
2
M
→
∫
2
x
∈
ℝ
⟼
if
x
∈
u
F
x
0
<
C
256
255
ralrimiva
⊢
φ
→
∀
u
∈
dom
vol
vol
u
<
C
2
M
→
∫
2
x
∈
ℝ
⟼
if
x
∈
u
F
x
0
<
C
257
breq2
⊢
d
=
C
2
M
→
vol
u
<
d
↔
vol
u
<
C
2
M
258
257
rspceaimv
⊢
C
2
M
∈
ℝ
+
∧
∀
u
∈
dom
vol
vol
u
<
C
2
M
→
∫
2
x
∈
ℝ
⟼
if
x
∈
u
F
x
0
<
C
→
∃
d
∈
ℝ
+
∀
u
∈
dom
vol
vol
u
<
d
→
∫
2
x
∈
ℝ
⟼
if
x
∈
u
F
x
0
<
C
259
9
256
258
syl2anc
⊢
φ
→
∃
d
∈
ℝ
+
∀
u
∈
dom
vol
vol
u
<
d
→
∫
2
x
∈
ℝ
⟼
if
x
∈
u
F
x
0
<
C