Database
BASIC REAL AND COMPLEX ANALYSIS
Integrals
Lebesgue integration
Lesbesgue integral
mbfi1fseqlem3
Next ⟩
mbfi1fseqlem4
Metamath Proof Explorer
Ascii
Unicode
Theorem
mbfi1fseqlem3
Description:
Lemma for
mbfi1fseq
.
(Contributed by
Mario Carneiro
, 16-Aug-2014)
Ref
Expression
Hypotheses
mbfi1fseq.1
⊢
φ
→
F
∈
MblFn
mbfi1fseq.2
⊢
φ
→
F
:
ℝ
⟶
0
+∞
mbfi1fseq.3
⊢
J
=
m
∈
ℕ
,
y
∈
ℝ
⟼
F
y
2
m
2
m
mbfi1fseq.4
⊢
G
=
m
∈
ℕ
⟼
x
∈
ℝ
⟼
if
x
∈
−
m
m
if
m
J
x
≤
m
m
J
x
m
0
Assertion
mbfi1fseqlem3
⊢
φ
∧
A
∈
ℕ
→
G
A
:
ℝ
⟶
ran
m
∈
0
…
A
2
A
⟼
m
2
A
Proof
Step
Hyp
Ref
Expression
1
mbfi1fseq.1
⊢
φ
→
F
∈
MblFn
2
mbfi1fseq.2
⊢
φ
→
F
:
ℝ
⟶
0
+∞
3
mbfi1fseq.3
⊢
J
=
m
∈
ℕ
,
y
∈
ℝ
⟼
F
y
2
m
2
m
4
mbfi1fseq.4
⊢
G
=
m
∈
ℕ
⟼
x
∈
ℝ
⟼
if
x
∈
−
m
m
if
m
J
x
≤
m
m
J
x
m
0
5
1
2
3
4
mbfi1fseqlem2
⊢
A
∈
ℕ
→
G
A
=
x
∈
ℝ
⟼
if
x
∈
−
A
A
if
A
J
x
≤
A
A
J
x
A
0
6
5
adantl
⊢
φ
∧
A
∈
ℕ
→
G
A
=
x
∈
ℝ
⟼
if
x
∈
−
A
A
if
A
J
x
≤
A
A
J
x
A
0
7
rge0ssre
⊢
0
+∞
⊆
ℝ
8
simpr
⊢
m
∈
ℕ
∧
y
∈
ℝ
→
y
∈
ℝ
9
ffvelcdm
⊢
F
:
ℝ
⟶
0
+∞
∧
y
∈
ℝ
→
F
y
∈
0
+∞
10
2
8
9
syl2an
⊢
φ
∧
m
∈
ℕ
∧
y
∈
ℝ
→
F
y
∈
0
+∞
11
7
10
sselid
⊢
φ
∧
m
∈
ℕ
∧
y
∈
ℝ
→
F
y
∈
ℝ
12
2nn
⊢
2
∈
ℕ
13
nnnn0
⊢
m
∈
ℕ
→
m
∈
ℕ
0
14
nnexpcl
⊢
2
∈
ℕ
∧
m
∈
ℕ
0
→
2
m
∈
ℕ
15
12
13
14
sylancr
⊢
m
∈
ℕ
→
2
m
∈
ℕ
16
15
ad2antrl
⊢
φ
∧
m
∈
ℕ
∧
y
∈
ℝ
→
2
m
∈
ℕ
17
16
nnred
⊢
φ
∧
m
∈
ℕ
∧
y
∈
ℝ
→
2
m
∈
ℝ
18
11
17
remulcld
⊢
φ
∧
m
∈
ℕ
∧
y
∈
ℝ
→
F
y
2
m
∈
ℝ
19
reflcl
⊢
F
y
2
m
∈
ℝ
→
F
y
2
m
∈
ℝ
20
18
19
syl
⊢
φ
∧
m
∈
ℕ
∧
y
∈
ℝ
→
F
y
2
m
∈
ℝ
21
20
16
nndivred
⊢
φ
∧
m
∈
ℕ
∧
y
∈
ℝ
→
F
y
2
m
2
m
∈
ℝ
22
21
ralrimivva
⊢
φ
→
∀
m
∈
ℕ
∀
y
∈
ℝ
F
y
2
m
2
m
∈
ℝ
23
3
fmpo
⊢
∀
m
∈
ℕ
∀
y
∈
ℝ
F
y
2
m
2
m
∈
ℝ
↔
J
:
ℕ
×
ℝ
⟶
ℝ
24
22
23
sylib
⊢
φ
→
J
:
ℕ
×
ℝ
⟶
ℝ
25
fovcdm
⊢
J
:
ℕ
×
ℝ
⟶
ℝ
∧
A
∈
ℕ
∧
x
∈
ℝ
→
A
J
x
∈
ℝ
26
24
25
syl3an1
⊢
φ
∧
A
∈
ℕ
∧
x
∈
ℝ
→
A
J
x
∈
ℝ
27
26
3expa
⊢
φ
∧
A
∈
ℕ
∧
x
∈
ℝ
→
A
J
x
∈
ℝ
28
nnre
⊢
A
∈
ℕ
→
A
∈
ℝ
29
28
ad2antlr
⊢
φ
∧
A
∈
ℕ
∧
x
∈
ℝ
→
A
∈
ℝ
30
nnnn0
⊢
A
∈
ℕ
→
A
∈
ℕ
0
31
nnexpcl
⊢
2
∈
ℕ
∧
A
∈
ℕ
0
→
2
A
∈
ℕ
32
12
30
31
sylancr
⊢
A
∈
ℕ
→
2
A
∈
ℕ
33
32
ad2antlr
⊢
φ
∧
A
∈
ℕ
∧
x
∈
ℝ
→
2
A
∈
ℕ
34
nnre
⊢
2
A
∈
ℕ
→
2
A
∈
ℝ
35
nngt0
⊢
2
A
∈
ℕ
→
0
<
2
A
36
34
35
jca
⊢
2
A
∈
ℕ
→
2
A
∈
ℝ
∧
0
<
2
A
37
33
36
syl
⊢
φ
∧
A
∈
ℕ
∧
x
∈
ℝ
→
2
A
∈
ℝ
∧
0
<
2
A
38
lemul1
⊢
A
J
x
∈
ℝ
∧
A
∈
ℝ
∧
2
A
∈
ℝ
∧
0
<
2
A
→
A
J
x
≤
A
↔
A
J
x
2
A
≤
A
2
A
39
27
29
37
38
syl3anc
⊢
φ
∧
A
∈
ℕ
∧
x
∈
ℝ
→
A
J
x
≤
A
↔
A
J
x
2
A
≤
A
2
A
40
39
biimpa
⊢
φ
∧
A
∈
ℕ
∧
x
∈
ℝ
∧
A
J
x
≤
A
→
A
J
x
2
A
≤
A
2
A
41
simpr
⊢
m
=
A
∧
y
=
x
→
y
=
x
42
41
fveq2d
⊢
m
=
A
∧
y
=
x
→
F
y
=
F
x
43
simpl
⊢
m
=
A
∧
y
=
x
→
m
=
A
44
43
oveq2d
⊢
m
=
A
∧
y
=
x
→
2
m
=
2
A
45
42
44
oveq12d
⊢
m
=
A
∧
y
=
x
→
F
y
2
m
=
F
x
2
A
46
45
fveq2d
⊢
m
=
A
∧
y
=
x
→
F
y
2
m
=
F
x
2
A
47
46
44
oveq12d
⊢
m
=
A
∧
y
=
x
→
F
y
2
m
2
m
=
F
x
2
A
2
A
48
ovex
⊢
F
x
2
A
2
A
∈
V
49
47
3
48
ovmpoa
⊢
A
∈
ℕ
∧
x
∈
ℝ
→
A
J
x
=
F
x
2
A
2
A
50
49
ad4ant23
⊢
φ
∧
A
∈
ℕ
∧
x
∈
ℝ
∧
A
J
x
≤
A
→
A
J
x
=
F
x
2
A
2
A
51
50
oveq1d
⊢
φ
∧
A
∈
ℕ
∧
x
∈
ℝ
∧
A
J
x
≤
A
→
A
J
x
2
A
=
F
x
2
A
2
A
2
A
52
2
adantr
⊢
φ
∧
A
∈
ℕ
→
F
:
ℝ
⟶
0
+∞
53
52
ffvelcdmda
⊢
φ
∧
A
∈
ℕ
∧
x
∈
ℝ
→
F
x
∈
0
+∞
54
elrege0
⊢
F
x
∈
0
+∞
↔
F
x
∈
ℝ
∧
0
≤
F
x
55
53
54
sylib
⊢
φ
∧
A
∈
ℕ
∧
x
∈
ℝ
→
F
x
∈
ℝ
∧
0
≤
F
x
56
55
simpld
⊢
φ
∧
A
∈
ℕ
∧
x
∈
ℝ
→
F
x
∈
ℝ
57
33
nnred
⊢
φ
∧
A
∈
ℕ
∧
x
∈
ℝ
→
2
A
∈
ℝ
58
56
57
remulcld
⊢
φ
∧
A
∈
ℕ
∧
x
∈
ℝ
→
F
x
2
A
∈
ℝ
59
33
nnnn0d
⊢
φ
∧
A
∈
ℕ
∧
x
∈
ℝ
→
2
A
∈
ℕ
0
60
59
nn0ge0d
⊢
φ
∧
A
∈
ℕ
∧
x
∈
ℝ
→
0
≤
2
A
61
mulge0
⊢
F
x
∈
ℝ
∧
0
≤
F
x
∧
2
A
∈
ℝ
∧
0
≤
2
A
→
0
≤
F
x
2
A
62
55
57
60
61
syl12anc
⊢
φ
∧
A
∈
ℕ
∧
x
∈
ℝ
→
0
≤
F
x
2
A
63
flge0nn0
⊢
F
x
2
A
∈
ℝ
∧
0
≤
F
x
2
A
→
F
x
2
A
∈
ℕ
0
64
58
62
63
syl2anc
⊢
φ
∧
A
∈
ℕ
∧
x
∈
ℝ
→
F
x
2
A
∈
ℕ
0
65
64
adantr
⊢
φ
∧
A
∈
ℕ
∧
x
∈
ℝ
∧
A
J
x
≤
A
→
F
x
2
A
∈
ℕ
0
66
65
nn0cnd
⊢
φ
∧
A
∈
ℕ
∧
x
∈
ℝ
∧
A
J
x
≤
A
→
F
x
2
A
∈
ℂ
67
33
adantr
⊢
φ
∧
A
∈
ℕ
∧
x
∈
ℝ
∧
A
J
x
≤
A
→
2
A
∈
ℕ
68
67
nncnd
⊢
φ
∧
A
∈
ℕ
∧
x
∈
ℝ
∧
A
J
x
≤
A
→
2
A
∈
ℂ
69
67
nnne0d
⊢
φ
∧
A
∈
ℕ
∧
x
∈
ℝ
∧
A
J
x
≤
A
→
2
A
≠
0
70
66
68
69
divcan1d
⊢
φ
∧
A
∈
ℕ
∧
x
∈
ℝ
∧
A
J
x
≤
A
→
F
x
2
A
2
A
2
A
=
F
x
2
A
71
51
70
eqtrd
⊢
φ
∧
A
∈
ℕ
∧
x
∈
ℝ
∧
A
J
x
≤
A
→
A
J
x
2
A
=
F
x
2
A
72
71
65
eqeltrd
⊢
φ
∧
A
∈
ℕ
∧
x
∈
ℝ
∧
A
J
x
≤
A
→
A
J
x
2
A
∈
ℕ
0
73
nn0uz
⊢
ℕ
0
=
ℤ
≥
0
74
72
73
eleqtrdi
⊢
φ
∧
A
∈
ℕ
∧
x
∈
ℝ
∧
A
J
x
≤
A
→
A
J
x
2
A
∈
ℤ
≥
0
75
nnmulcl
⊢
A
∈
ℕ
∧
2
A
∈
ℕ
→
A
2
A
∈
ℕ
76
32
75
mpdan
⊢
A
∈
ℕ
→
A
2
A
∈
ℕ
77
76
ad2antlr
⊢
φ
∧
A
∈
ℕ
∧
x
∈
ℝ
→
A
2
A
∈
ℕ
78
77
adantr
⊢
φ
∧
A
∈
ℕ
∧
x
∈
ℝ
∧
A
J
x
≤
A
→
A
2
A
∈
ℕ
79
78
nnzd
⊢
φ
∧
A
∈
ℕ
∧
x
∈
ℝ
∧
A
J
x
≤
A
→
A
2
A
∈
ℤ
80
elfz5
⊢
A
J
x
2
A
∈
ℤ
≥
0
∧
A
2
A
∈
ℤ
→
A
J
x
2
A
∈
0
…
A
2
A
↔
A
J
x
2
A
≤
A
2
A
81
74
79
80
syl2anc
⊢
φ
∧
A
∈
ℕ
∧
x
∈
ℝ
∧
A
J
x
≤
A
→
A
J
x
2
A
∈
0
…
A
2
A
↔
A
J
x
2
A
≤
A
2
A
82
40
81
mpbird
⊢
φ
∧
A
∈
ℕ
∧
x
∈
ℝ
∧
A
J
x
≤
A
→
A
J
x
2
A
∈
0
…
A
2
A
83
oveq1
⊢
m
=
A
J
x
2
A
→
m
2
A
=
A
J
x
2
A
2
A
84
eqid
⊢
m
∈
0
…
A
2
A
⟼
m
2
A
=
m
∈
0
…
A
2
A
⟼
m
2
A
85
ovex
⊢
A
J
x
2
A
2
A
∈
V
86
83
84
85
fvmpt
⊢
A
J
x
2
A
∈
0
…
A
2
A
→
m
∈
0
…
A
2
A
⟼
m
2
A
A
J
x
2
A
=
A
J
x
2
A
2
A
87
82
86
syl
⊢
φ
∧
A
∈
ℕ
∧
x
∈
ℝ
∧
A
J
x
≤
A
→
m
∈
0
…
A
2
A
⟼
m
2
A
A
J
x
2
A
=
A
J
x
2
A
2
A
88
27
adantr
⊢
φ
∧
A
∈
ℕ
∧
x
∈
ℝ
∧
A
J
x
≤
A
→
A
J
x
∈
ℝ
89
88
recnd
⊢
φ
∧
A
∈
ℕ
∧
x
∈
ℝ
∧
A
J
x
≤
A
→
A
J
x
∈
ℂ
90
89
68
69
divcan4d
⊢
φ
∧
A
∈
ℕ
∧
x
∈
ℝ
∧
A
J
x
≤
A
→
A
J
x
2
A
2
A
=
A
J
x
91
87
90
eqtrd
⊢
φ
∧
A
∈
ℕ
∧
x
∈
ℝ
∧
A
J
x
≤
A
→
m
∈
0
…
A
2
A
⟼
m
2
A
A
J
x
2
A
=
A
J
x
92
elfznn0
⊢
m
∈
0
…
A
2
A
→
m
∈
ℕ
0
93
92
nn0red
⊢
m
∈
0
…
A
2
A
→
m
∈
ℝ
94
32
adantl
⊢
φ
∧
A
∈
ℕ
→
2
A
∈
ℕ
95
nndivre
⊢
m
∈
ℝ
∧
2
A
∈
ℕ
→
m
2
A
∈
ℝ
96
93
94
95
syl2anr
⊢
φ
∧
A
∈
ℕ
∧
m
∈
0
…
A
2
A
→
m
2
A
∈
ℝ
97
96
fmpttd
⊢
φ
∧
A
∈
ℕ
→
m
∈
0
…
A
2
A
⟼
m
2
A
:
0
…
A
2
A
⟶
ℝ
98
97
ffnd
⊢
φ
∧
A
∈
ℕ
→
m
∈
0
…
A
2
A
⟼
m
2
A
Fn
0
…
A
2
A
99
98
adantr
⊢
φ
∧
A
∈
ℕ
∧
x
∈
ℝ
→
m
∈
0
…
A
2
A
⟼
m
2
A
Fn
0
…
A
2
A
100
99
adantr
⊢
φ
∧
A
∈
ℕ
∧
x
∈
ℝ
∧
A
J
x
≤
A
→
m
∈
0
…
A
2
A
⟼
m
2
A
Fn
0
…
A
2
A
101
fnfvelrn
⊢
m
∈
0
…
A
2
A
⟼
m
2
A
Fn
0
…
A
2
A
∧
A
J
x
2
A
∈
0
…
A
2
A
→
m
∈
0
…
A
2
A
⟼
m
2
A
A
J
x
2
A
∈
ran
m
∈
0
…
A
2
A
⟼
m
2
A
102
100
82
101
syl2anc
⊢
φ
∧
A
∈
ℕ
∧
x
∈
ℝ
∧
A
J
x
≤
A
→
m
∈
0
…
A
2
A
⟼
m
2
A
A
J
x
2
A
∈
ran
m
∈
0
…
A
2
A
⟼
m
2
A
103
91
102
eqeltrrd
⊢
φ
∧
A
∈
ℕ
∧
x
∈
ℝ
∧
A
J
x
≤
A
→
A
J
x
∈
ran
m
∈
0
…
A
2
A
⟼
m
2
A
104
77
nnnn0d
⊢
φ
∧
A
∈
ℕ
∧
x
∈
ℝ
→
A
2
A
∈
ℕ
0
105
104
73
eleqtrdi
⊢
φ
∧
A
∈
ℕ
∧
x
∈
ℝ
→
A
2
A
∈
ℤ
≥
0
106
eluzfz2
⊢
A
2
A
∈
ℤ
≥
0
→
A
2
A
∈
0
…
A
2
A
107
105
106
syl
⊢
φ
∧
A
∈
ℕ
∧
x
∈
ℝ
→
A
2
A
∈
0
…
A
2
A
108
oveq1
⊢
m
=
A
2
A
→
m
2
A
=
A
2
A
2
A
109
ovex
⊢
A
2
A
2
A
∈
V
110
108
84
109
fvmpt
⊢
A
2
A
∈
0
…
A
2
A
→
m
∈
0
…
A
2
A
⟼
m
2
A
A
2
A
=
A
2
A
2
A
111
107
110
syl
⊢
φ
∧
A
∈
ℕ
∧
x
∈
ℝ
→
m
∈
0
…
A
2
A
⟼
m
2
A
A
2
A
=
A
2
A
2
A
112
29
recnd
⊢
φ
∧
A
∈
ℕ
∧
x
∈
ℝ
→
A
∈
ℂ
113
33
nncnd
⊢
φ
∧
A
∈
ℕ
∧
x
∈
ℝ
→
2
A
∈
ℂ
114
33
nnne0d
⊢
φ
∧
A
∈
ℕ
∧
x
∈
ℝ
→
2
A
≠
0
115
112
113
114
divcan4d
⊢
φ
∧
A
∈
ℕ
∧
x
∈
ℝ
→
A
2
A
2
A
=
A
116
111
115
eqtrd
⊢
φ
∧
A
∈
ℕ
∧
x
∈
ℝ
→
m
∈
0
…
A
2
A
⟼
m
2
A
A
2
A
=
A
117
fnfvelrn
⊢
m
∈
0
…
A
2
A
⟼
m
2
A
Fn
0
…
A
2
A
∧
A
2
A
∈
0
…
A
2
A
→
m
∈
0
…
A
2
A
⟼
m
2
A
A
2
A
∈
ran
m
∈
0
…
A
2
A
⟼
m
2
A
118
99
107
117
syl2anc
⊢
φ
∧
A
∈
ℕ
∧
x
∈
ℝ
→
m
∈
0
…
A
2
A
⟼
m
2
A
A
2
A
∈
ran
m
∈
0
…
A
2
A
⟼
m
2
A
119
116
118
eqeltrrd
⊢
φ
∧
A
∈
ℕ
∧
x
∈
ℝ
→
A
∈
ran
m
∈
0
…
A
2
A
⟼
m
2
A
120
119
adantr
⊢
φ
∧
A
∈
ℕ
∧
x
∈
ℝ
∧
¬
A
J
x
≤
A
→
A
∈
ran
m
∈
0
…
A
2
A
⟼
m
2
A
121
103
120
ifclda
⊢
φ
∧
A
∈
ℕ
∧
x
∈
ℝ
→
if
A
J
x
≤
A
A
J
x
A
∈
ran
m
∈
0
…
A
2
A
⟼
m
2
A
122
eluzfz1
⊢
A
2
A
∈
ℤ
≥
0
→
0
∈
0
…
A
2
A
123
105
122
syl
⊢
φ
∧
A
∈
ℕ
∧
x
∈
ℝ
→
0
∈
0
…
A
2
A
124
oveq1
⊢
m
=
0
→
m
2
A
=
0
2
A
125
ovex
⊢
0
2
A
∈
V
126
124
84
125
fvmpt
⊢
0
∈
0
…
A
2
A
→
m
∈
0
…
A
2
A
⟼
m
2
A
0
=
0
2
A
127
123
126
syl
⊢
φ
∧
A
∈
ℕ
∧
x
∈
ℝ
→
m
∈
0
…
A
2
A
⟼
m
2
A
0
=
0
2
A
128
nncn
⊢
2
A
∈
ℕ
→
2
A
∈
ℂ
129
nnne0
⊢
2
A
∈
ℕ
→
2
A
≠
0
130
128
129
div0d
⊢
2
A
∈
ℕ
→
0
2
A
=
0
131
33
130
syl
⊢
φ
∧
A
∈
ℕ
∧
x
∈
ℝ
→
0
2
A
=
0
132
127
131
eqtrd
⊢
φ
∧
A
∈
ℕ
∧
x
∈
ℝ
→
m
∈
0
…
A
2
A
⟼
m
2
A
0
=
0
133
fnfvelrn
⊢
m
∈
0
…
A
2
A
⟼
m
2
A
Fn
0
…
A
2
A
∧
0
∈
0
…
A
2
A
→
m
∈
0
…
A
2
A
⟼
m
2
A
0
∈
ran
m
∈
0
…
A
2
A
⟼
m
2
A
134
99
123
133
syl2anc
⊢
φ
∧
A
∈
ℕ
∧
x
∈
ℝ
→
m
∈
0
…
A
2
A
⟼
m
2
A
0
∈
ran
m
∈
0
…
A
2
A
⟼
m
2
A
135
132
134
eqeltrrd
⊢
φ
∧
A
∈
ℕ
∧
x
∈
ℝ
→
0
∈
ran
m
∈
0
…
A
2
A
⟼
m
2
A
136
121
135
ifcld
⊢
φ
∧
A
∈
ℕ
∧
x
∈
ℝ
→
if
x
∈
−
A
A
if
A
J
x
≤
A
A
J
x
A
0
∈
ran
m
∈
0
…
A
2
A
⟼
m
2
A
137
6
136
fmpt3d
⊢
φ
∧
A
∈
ℕ
→
G
A
:
ℝ
⟶
ran
m
∈
0
…
A
2
A
⟼
m
2
A