Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Brendan Leahy
ftc1anclem4
Next ⟩
ftc1anclem5
Metamath Proof Explorer
Ascii
Unicode
Theorem
ftc1anclem4
Description:
Lemma for
ftc1anc
.
(Contributed by
Brendan Leahy
, 17-Jun-2018)
Ref
Expression
Assertion
ftc1anclem4
⊢
F
∈
dom
∫
1
∧
G
∈
𝐿
1
∧
G
:
ℝ
⟶
ℝ
→
∫
2
t
∈
ℝ
⟼
G
t
−
F
t
∈
ℝ
Proof
Step
Hyp
Ref
Expression
1
ffvelrn
⊢
G
:
ℝ
⟶
ℝ
∧
t
∈
ℝ
→
G
t
∈
ℝ
2
1
recnd
⊢
G
:
ℝ
⟶
ℝ
∧
t
∈
ℝ
→
G
t
∈
ℂ
3
i1ff
⊢
F
∈
dom
∫
1
→
F
:
ℝ
⟶
ℝ
4
3
ffvelrnda
⊢
F
∈
dom
∫
1
∧
t
∈
ℝ
→
F
t
∈
ℝ
5
4
recnd
⊢
F
∈
dom
∫
1
∧
t
∈
ℝ
→
F
t
∈
ℂ
6
subcl
⊢
G
t
∈
ℂ
∧
F
t
∈
ℂ
→
G
t
−
F
t
∈
ℂ
7
2
5
6
syl2anr
⊢
F
∈
dom
∫
1
∧
t
∈
ℝ
∧
G
:
ℝ
⟶
ℝ
∧
t
∈
ℝ
→
G
t
−
F
t
∈
ℂ
8
7
anandirs
⊢
F
∈
dom
∫
1
∧
G
:
ℝ
⟶
ℝ
∧
t
∈
ℝ
→
G
t
−
F
t
∈
ℂ
9
8
abscld
⊢
F
∈
dom
∫
1
∧
G
:
ℝ
⟶
ℝ
∧
t
∈
ℝ
→
G
t
−
F
t
∈
ℝ
10
9
rexrd
⊢
F
∈
dom
∫
1
∧
G
:
ℝ
⟶
ℝ
∧
t
∈
ℝ
→
G
t
−
F
t
∈
ℝ
*
11
8
absge0d
⊢
F
∈
dom
∫
1
∧
G
:
ℝ
⟶
ℝ
∧
t
∈
ℝ
→
0
≤
G
t
−
F
t
12
elxrge0
⊢
G
t
−
F
t
∈
0
+∞
↔
G
t
−
F
t
∈
ℝ
*
∧
0
≤
G
t
−
F
t
13
10
11
12
sylanbrc
⊢
F
∈
dom
∫
1
∧
G
:
ℝ
⟶
ℝ
∧
t
∈
ℝ
→
G
t
−
F
t
∈
0
+∞
14
13
fmpttd
⊢
F
∈
dom
∫
1
∧
G
:
ℝ
⟶
ℝ
→
t
∈
ℝ
⟼
G
t
−
F
t
:
ℝ
⟶
0
+∞
15
14
3adant2
⊢
F
∈
dom
∫
1
∧
G
∈
𝐿
1
∧
G
:
ℝ
⟶
ℝ
→
t
∈
ℝ
⟼
G
t
−
F
t
:
ℝ
⟶
0
+∞
16
reex
⊢
ℝ
∈
V
17
16
a1i
⊢
F
∈
dom
∫
1
∧
G
∈
𝐿
1
∧
G
:
ℝ
⟶
ℝ
→
ℝ
∈
V
18
fvexd
⊢
F
∈
dom
∫
1
∧
G
∈
𝐿
1
∧
G
:
ℝ
⟶
ℝ
∧
t
∈
ℝ
→
G
t
∈
V
19
fvexd
⊢
F
∈
dom
∫
1
∧
G
∈
𝐿
1
∧
G
:
ℝ
⟶
ℝ
∧
t
∈
ℝ
→
F
t
∈
V
20
eqidd
⊢
F
∈
dom
∫
1
∧
G
∈
𝐿
1
∧
G
:
ℝ
⟶
ℝ
→
t
∈
ℝ
⟼
G
t
=
t
∈
ℝ
⟼
G
t
21
eqidd
⊢
F
∈
dom
∫
1
∧
G
∈
𝐿
1
∧
G
:
ℝ
⟶
ℝ
→
t
∈
ℝ
⟼
F
t
=
t
∈
ℝ
⟼
F
t
22
17
18
19
20
21
offval2
⊢
F
∈
dom
∫
1
∧
G
∈
𝐿
1
∧
G
:
ℝ
⟶
ℝ
→
t
∈
ℝ
⟼
G
t
+
f
t
∈
ℝ
⟼
F
t
=
t
∈
ℝ
⟼
G
t
+
F
t
23
22
fveq2d
⊢
F
∈
dom
∫
1
∧
G
∈
𝐿
1
∧
G
:
ℝ
⟶
ℝ
→
∫
2
t
∈
ℝ
⟼
G
t
+
f
t
∈
ℝ
⟼
F
t
=
∫
2
t
∈
ℝ
⟼
G
t
+
F
t
24
id
⊢
G
:
ℝ
⟶
ℝ
→
G
:
ℝ
⟶
ℝ
25
24
feqmptd
⊢
G
:
ℝ
⟶
ℝ
→
G
=
t
∈
ℝ
⟼
G
t
26
absf
⊢
abs
:
ℂ
⟶
ℝ
27
26
a1i
⊢
G
:
ℝ
⟶
ℝ
→
abs
:
ℂ
⟶
ℝ
28
27
feqmptd
⊢
G
:
ℝ
⟶
ℝ
→
abs
=
x
∈
ℂ
⟼
x
29
fveq2
⊢
x
=
G
t
→
x
=
G
t
30
2
25
28
29
fmptco
⊢
G
:
ℝ
⟶
ℝ
→
abs
∘
G
=
t
∈
ℝ
⟼
G
t
31
30
adantl
⊢
G
∈
𝐿
1
∧
G
:
ℝ
⟶
ℝ
→
abs
∘
G
=
t
∈
ℝ
⟼
G
t
32
iblmbf
⊢
G
∈
𝐿
1
→
G
∈
MblFn
33
ftc1anclem1
⊢
G
:
ℝ
⟶
ℝ
∧
G
∈
MblFn
→
abs
∘
G
∈
MblFn
34
32
33
sylan2
⊢
G
:
ℝ
⟶
ℝ
∧
G
∈
𝐿
1
→
abs
∘
G
∈
MblFn
35
34
ancoms
⊢
G
∈
𝐿
1
∧
G
:
ℝ
⟶
ℝ
→
abs
∘
G
∈
MblFn
36
31
35
eqeltrrd
⊢
G
∈
𝐿
1
∧
G
:
ℝ
⟶
ℝ
→
t
∈
ℝ
⟼
G
t
∈
MblFn
37
36
3adant1
⊢
F
∈
dom
∫
1
∧
G
∈
𝐿
1
∧
G
:
ℝ
⟶
ℝ
→
t
∈
ℝ
⟼
G
t
∈
MblFn
38
2
abscld
⊢
G
:
ℝ
⟶
ℝ
∧
t
∈
ℝ
→
G
t
∈
ℝ
39
2
absge0d
⊢
G
:
ℝ
⟶
ℝ
∧
t
∈
ℝ
→
0
≤
G
t
40
elrege0
⊢
G
t
∈
0
+∞
↔
G
t
∈
ℝ
∧
0
≤
G
t
41
38
39
40
sylanbrc
⊢
G
:
ℝ
⟶
ℝ
∧
t
∈
ℝ
→
G
t
∈
0
+∞
42
41
fmpttd
⊢
G
:
ℝ
⟶
ℝ
→
t
∈
ℝ
⟼
G
t
:
ℝ
⟶
0
+∞
43
42
3ad2ant3
⊢
F
∈
dom
∫
1
∧
G
∈
𝐿
1
∧
G
:
ℝ
⟶
ℝ
→
t
∈
ℝ
⟼
G
t
:
ℝ
⟶
0
+∞
44
iftrue
⊢
t
∈
ℝ
→
if
t
∈
ℝ
G
t
0
=
G
t
45
44
mpteq2ia
⊢
t
∈
ℝ
⟼
if
t
∈
ℝ
G
t
0
=
t
∈
ℝ
⟼
G
t
46
45
fveq2i
⊢
∫
2
t
∈
ℝ
⟼
if
t
∈
ℝ
G
t
0
=
∫
2
t
∈
ℝ
⟼
G
t
47
1
adantll
⊢
G
∈
𝐿
1
∧
G
:
ℝ
⟶
ℝ
∧
t
∈
ℝ
→
G
t
∈
ℝ
48
simpr
⊢
G
∈
𝐿
1
∧
G
:
ℝ
⟶
ℝ
→
G
:
ℝ
⟶
ℝ
49
48
feqmptd
⊢
G
∈
𝐿
1
∧
G
:
ℝ
⟶
ℝ
→
G
=
t
∈
ℝ
⟼
G
t
50
simpl
⊢
G
∈
𝐿
1
∧
G
:
ℝ
⟶
ℝ
→
G
∈
𝐿
1
51
49
50
eqeltrrd
⊢
G
∈
𝐿
1
∧
G
:
ℝ
⟶
ℝ
→
t
∈
ℝ
⟼
G
t
∈
𝐿
1
52
47
51
36
iblabsnc
⊢
G
∈
𝐿
1
∧
G
:
ℝ
⟶
ℝ
→
t
∈
ℝ
⟼
G
t
∈
𝐿
1
53
38
adantll
⊢
G
∈
𝐿
1
∧
G
:
ℝ
⟶
ℝ
∧
t
∈
ℝ
→
G
t
∈
ℝ
54
39
adantll
⊢
G
∈
𝐿
1
∧
G
:
ℝ
⟶
ℝ
∧
t
∈
ℝ
→
0
≤
G
t
55
53
54
iblpos
⊢
G
∈
𝐿
1
∧
G
:
ℝ
⟶
ℝ
→
t
∈
ℝ
⟼
G
t
∈
𝐿
1
↔
t
∈
ℝ
⟼
G
t
∈
MblFn
∧
∫
2
t
∈
ℝ
⟼
if
t
∈
ℝ
G
t
0
∈
ℝ
56
52
55
mpbid
⊢
G
∈
𝐿
1
∧
G
:
ℝ
⟶
ℝ
→
t
∈
ℝ
⟼
G
t
∈
MblFn
∧
∫
2
t
∈
ℝ
⟼
if
t
∈
ℝ
G
t
0
∈
ℝ
57
56
simprd
⊢
G
∈
𝐿
1
∧
G
:
ℝ
⟶
ℝ
→
∫
2
t
∈
ℝ
⟼
if
t
∈
ℝ
G
t
0
∈
ℝ
58
46
57
eqeltrrid
⊢
G
∈
𝐿
1
∧
G
:
ℝ
⟶
ℝ
→
∫
2
t
∈
ℝ
⟼
G
t
∈
ℝ
59
58
3adant1
⊢
F
∈
dom
∫
1
∧
G
∈
𝐿
1
∧
G
:
ℝ
⟶
ℝ
→
∫
2
t
∈
ℝ
⟼
G
t
∈
ℝ
60
5
abscld
⊢
F
∈
dom
∫
1
∧
t
∈
ℝ
→
F
t
∈
ℝ
61
5
absge0d
⊢
F
∈
dom
∫
1
∧
t
∈
ℝ
→
0
≤
F
t
62
elrege0
⊢
F
t
∈
0
+∞
↔
F
t
∈
ℝ
∧
0
≤
F
t
63
60
61
62
sylanbrc
⊢
F
∈
dom
∫
1
∧
t
∈
ℝ
→
F
t
∈
0
+∞
64
63
fmpttd
⊢
F
∈
dom
∫
1
→
t
∈
ℝ
⟼
F
t
:
ℝ
⟶
0
+∞
65
64
3ad2ant1
⊢
F
∈
dom
∫
1
∧
G
∈
𝐿
1
∧
G
:
ℝ
⟶
ℝ
→
t
∈
ℝ
⟼
F
t
:
ℝ
⟶
0
+∞
66
iftrue
⊢
t
∈
ℝ
→
if
t
∈
ℝ
F
t
0
=
F
t
67
66
mpteq2ia
⊢
t
∈
ℝ
⟼
if
t
∈
ℝ
F
t
0
=
t
∈
ℝ
⟼
F
t
68
67
fveq2i
⊢
∫
2
t
∈
ℝ
⟼
if
t
∈
ℝ
F
t
0
=
∫
2
t
∈
ℝ
⟼
F
t
69
3
feqmptd
⊢
F
∈
dom
∫
1
→
F
=
t
∈
ℝ
⟼
F
t
70
i1fibl
⊢
F
∈
dom
∫
1
→
F
∈
𝐿
1
71
69
70
eqeltrrd
⊢
F
∈
dom
∫
1
→
t
∈
ℝ
⟼
F
t
∈
𝐿
1
72
26
a1i
⊢
F
∈
dom
∫
1
→
abs
:
ℂ
⟶
ℝ
73
72
feqmptd
⊢
F
∈
dom
∫
1
→
abs
=
x
∈
ℂ
⟼
x
74
fveq2
⊢
x
=
F
t
→
x
=
F
t
75
5
69
73
74
fmptco
⊢
F
∈
dom
∫
1
→
abs
∘
F
=
t
∈
ℝ
⟼
F
t
76
i1fmbf
⊢
F
∈
dom
∫
1
→
F
∈
MblFn
77
ftc1anclem1
⊢
F
:
ℝ
⟶
ℝ
∧
F
∈
MblFn
→
abs
∘
F
∈
MblFn
78
3
76
77
syl2anc
⊢
F
∈
dom
∫
1
→
abs
∘
F
∈
MblFn
79
75
78
eqeltrrd
⊢
F
∈
dom
∫
1
→
t
∈
ℝ
⟼
F
t
∈
MblFn
80
4
71
79
iblabsnc
⊢
F
∈
dom
∫
1
→
t
∈
ℝ
⟼
F
t
∈
𝐿
1
81
60
61
iblpos
⊢
F
∈
dom
∫
1
→
t
∈
ℝ
⟼
F
t
∈
𝐿
1
↔
t
∈
ℝ
⟼
F
t
∈
MblFn
∧
∫
2
t
∈
ℝ
⟼
if
t
∈
ℝ
F
t
0
∈
ℝ
82
80
81
mpbid
⊢
F
∈
dom
∫
1
→
t
∈
ℝ
⟼
F
t
∈
MblFn
∧
∫
2
t
∈
ℝ
⟼
if
t
∈
ℝ
F
t
0
∈
ℝ
83
82
simprd
⊢
F
∈
dom
∫
1
→
∫
2
t
∈
ℝ
⟼
if
t
∈
ℝ
F
t
0
∈
ℝ
84
68
83
eqeltrrid
⊢
F
∈
dom
∫
1
→
∫
2
t
∈
ℝ
⟼
F
t
∈
ℝ
85
84
3ad2ant1
⊢
F
∈
dom
∫
1
∧
G
∈
𝐿
1
∧
G
:
ℝ
⟶
ℝ
→
∫
2
t
∈
ℝ
⟼
F
t
∈
ℝ
86
37
43
59
65
85
itg2addnc
⊢
F
∈
dom
∫
1
∧
G
∈
𝐿
1
∧
G
:
ℝ
⟶
ℝ
→
∫
2
t
∈
ℝ
⟼
G
t
+
f
t
∈
ℝ
⟼
F
t
=
∫
2
t
∈
ℝ
⟼
G
t
+
∫
2
t
∈
ℝ
⟼
F
t
87
23
86
eqtr3d
⊢
F
∈
dom
∫
1
∧
G
∈
𝐿
1
∧
G
:
ℝ
⟶
ℝ
→
∫
2
t
∈
ℝ
⟼
G
t
+
F
t
=
∫
2
t
∈
ℝ
⟼
G
t
+
∫
2
t
∈
ℝ
⟼
F
t
88
59
85
readdcld
⊢
F
∈
dom
∫
1
∧
G
∈
𝐿
1
∧
G
:
ℝ
⟶
ℝ
→
∫
2
t
∈
ℝ
⟼
G
t
+
∫
2
t
∈
ℝ
⟼
F
t
∈
ℝ
89
87
88
eqeltrd
⊢
F
∈
dom
∫
1
∧
G
∈
𝐿
1
∧
G
:
ℝ
⟶
ℝ
→
∫
2
t
∈
ℝ
⟼
G
t
+
F
t
∈
ℝ
90
readdcl
⊢
G
t
∈
ℝ
∧
F
t
∈
ℝ
→
G
t
+
F
t
∈
ℝ
91
38
60
90
syl2anr
⊢
F
∈
dom
∫
1
∧
t
∈
ℝ
∧
G
:
ℝ
⟶
ℝ
∧
t
∈
ℝ
→
G
t
+
F
t
∈
ℝ
92
91
anandirs
⊢
F
∈
dom
∫
1
∧
G
:
ℝ
⟶
ℝ
∧
t
∈
ℝ
→
G
t
+
F
t
∈
ℝ
93
92
rexrd
⊢
F
∈
dom
∫
1
∧
G
:
ℝ
⟶
ℝ
∧
t
∈
ℝ
→
G
t
+
F
t
∈
ℝ
*
94
38
adantll
⊢
F
∈
dom
∫
1
∧
G
:
ℝ
⟶
ℝ
∧
t
∈
ℝ
→
G
t
∈
ℝ
95
60
adantlr
⊢
F
∈
dom
∫
1
∧
G
:
ℝ
⟶
ℝ
∧
t
∈
ℝ
→
F
t
∈
ℝ
96
39
adantll
⊢
F
∈
dom
∫
1
∧
G
:
ℝ
⟶
ℝ
∧
t
∈
ℝ
→
0
≤
G
t
97
61
adantlr
⊢
F
∈
dom
∫
1
∧
G
:
ℝ
⟶
ℝ
∧
t
∈
ℝ
→
0
≤
F
t
98
94
95
96
97
addge0d
⊢
F
∈
dom
∫
1
∧
G
:
ℝ
⟶
ℝ
∧
t
∈
ℝ
→
0
≤
G
t
+
F
t
99
elxrge0
⊢
G
t
+
F
t
∈
0
+∞
↔
G
t
+
F
t
∈
ℝ
*
∧
0
≤
G
t
+
F
t
100
93
98
99
sylanbrc
⊢
F
∈
dom
∫
1
∧
G
:
ℝ
⟶
ℝ
∧
t
∈
ℝ
→
G
t
+
F
t
∈
0
+∞
101
100
fmpttd
⊢
F
∈
dom
∫
1
∧
G
:
ℝ
⟶
ℝ
→
t
∈
ℝ
⟼
G
t
+
F
t
:
ℝ
⟶
0
+∞
102
101
3adant2
⊢
F
∈
dom
∫
1
∧
G
∈
𝐿
1
∧
G
:
ℝ
⟶
ℝ
→
t
∈
ℝ
⟼
G
t
+
F
t
:
ℝ
⟶
0
+∞
103
abs2dif2
⊢
G
t
∈
ℂ
∧
F
t
∈
ℂ
→
G
t
−
F
t
≤
G
t
+
F
t
104
2
5
103
syl2anr
⊢
F
∈
dom
∫
1
∧
t
∈
ℝ
∧
G
:
ℝ
⟶
ℝ
∧
t
∈
ℝ
→
G
t
−
F
t
≤
G
t
+
F
t
105
104
anandirs
⊢
F
∈
dom
∫
1
∧
G
:
ℝ
⟶
ℝ
∧
t
∈
ℝ
→
G
t
−
F
t
≤
G
t
+
F
t
106
105
ralrimiva
⊢
F
∈
dom
∫
1
∧
G
:
ℝ
⟶
ℝ
→
∀
t
∈
ℝ
G
t
−
F
t
≤
G
t
+
F
t
107
16
a1i
⊢
F
∈
dom
∫
1
∧
G
:
ℝ
⟶
ℝ
→
ℝ
∈
V
108
eqidd
⊢
F
∈
dom
∫
1
∧
G
:
ℝ
⟶
ℝ
→
t
∈
ℝ
⟼
G
t
−
F
t
=
t
∈
ℝ
⟼
G
t
−
F
t
109
eqidd
⊢
F
∈
dom
∫
1
∧
G
:
ℝ
⟶
ℝ
→
t
∈
ℝ
⟼
G
t
+
F
t
=
t
∈
ℝ
⟼
G
t
+
F
t
110
107
9
92
108
109
ofrfval2
⊢
F
∈
dom
∫
1
∧
G
:
ℝ
⟶
ℝ
→
t
∈
ℝ
⟼
G
t
−
F
t
≤
f
t
∈
ℝ
⟼
G
t
+
F
t
↔
∀
t
∈
ℝ
G
t
−
F
t
≤
G
t
+
F
t
111
106
110
mpbird
⊢
F
∈
dom
∫
1
∧
G
:
ℝ
⟶
ℝ
→
t
∈
ℝ
⟼
G
t
−
F
t
≤
f
t
∈
ℝ
⟼
G
t
+
F
t
112
111
3adant2
⊢
F
∈
dom
∫
1
∧
G
∈
𝐿
1
∧
G
:
ℝ
⟶
ℝ
→
t
∈
ℝ
⟼
G
t
−
F
t
≤
f
t
∈
ℝ
⟼
G
t
+
F
t
113
itg2le
⊢
t
∈
ℝ
⟼
G
t
−
F
t
:
ℝ
⟶
0
+∞
∧
t
∈
ℝ
⟼
G
t
+
F
t
:
ℝ
⟶
0
+∞
∧
t
∈
ℝ
⟼
G
t
−
F
t
≤
f
t
∈
ℝ
⟼
G
t
+
F
t
→
∫
2
t
∈
ℝ
⟼
G
t
−
F
t
≤
∫
2
t
∈
ℝ
⟼
G
t
+
F
t
114
15
102
112
113
syl3anc
⊢
F
∈
dom
∫
1
∧
G
∈
𝐿
1
∧
G
:
ℝ
⟶
ℝ
→
∫
2
t
∈
ℝ
⟼
G
t
−
F
t
≤
∫
2
t
∈
ℝ
⟼
G
t
+
F
t
115
itg2lecl
⊢
t
∈
ℝ
⟼
G
t
−
F
t
:
ℝ
⟶
0
+∞
∧
∫
2
t
∈
ℝ
⟼
G
t
+
F
t
∈
ℝ
∧
∫
2
t
∈
ℝ
⟼
G
t
−
F
t
≤
∫
2
t
∈
ℝ
⟼
G
t
+
F
t
→
∫
2
t
∈
ℝ
⟼
G
t
−
F
t
∈
ℝ
116
15
89
114
115
syl3anc
⊢
F
∈
dom
∫
1
∧
G
∈
𝐿
1
∧
G
:
ℝ
⟶
ℝ
→
∫
2
t
∈
ℝ
⟼
G
t
−
F
t
∈
ℝ