Differentiating,
using
fact
and
fact ,
yields
(
y
f
−
1
(
y
)
−
F
(
f
−
1
(
y
)
)
)
′
=
f
−
1
(
y
)
+
y
1
f
′
(
f
−
1
(
y
)
)
−
f
(
f
−
1
(
y
)
)
1
f
′
(
f
−
1
(
y
)
)
=
f
−
1
(
y
)
.
{\displaystyle {}{\begin{aligned}{\left(yf^{-1}(y)-F{\left(f^{-1}(y)\right)}\right)}'&=f^{-1}(y)+y{\frac {1}{f'(f^{-1}(y))}}-f{\left(f^{-1}(y)\right)}{\frac {1}{f'{\left(f^{-1}(y)\right)}}}\\&=f^{-1}(y).\end{aligned}}}
◻
{\displaystyle \Box }
For this statement, there exists also an easy geometric explanation. When
f
:
[
a
,
b
]
→
R
+
{\displaystyle {}f\colon [a,b]\rightarrow \mathbb {R} _{+}}
is a strictly increasing continuous function
(and therefore induces a bijection between
[
a
,
b
]
{\displaystyle {}[a,b]}
and
[
f
(
a
)
,
f
(
b
)
]
{\displaystyle {}[f(a),f(b)]}
),
then the following relation between the areas holds:
The graph with its inverse function, and the areas relevant for the computation of the integral of the inverse function.
∫
a
b
f
(
s
)
d
s
+
∫
f
(
a
)
f
(
b
)
f
−
1
(
t
)
d
t
=
b
f
(
b
)
−
a
f
(
a
)
,
{\displaystyle {}\int _{a}^{b}f(s)\,ds+\int _{f(a)}^{f(b)}f^{-1}(t)\,dt=bf(b)-af(a)\,,}
or, equivalently,
∫
f
(
a
)
f
(
b
)
f
−
1
(
t
)
d
t
=
b
f
(
b
)
−
a
f
(
a
)
−
∫
a
b
f
(
s
)
d
s
.
{\displaystyle {}\int _{f(a)}^{f(b)}f^{-1}(t)\,dt=bf(b)-af(a)-\int _{a}^{b}f(s)\,ds\,.}
For the primitive function
G
{\displaystyle {}G}
of
f
−
1
{\displaystyle {}f^{-1}}
with starting point
f
(
a
)
{\displaystyle {}f(a)}
, we have, if
F
{\displaystyle {}F}
denotes a primitive function for
f
{\displaystyle {}f}
, the relation
G
(
y
)
=
∫
f
(
a
)
y
f
−
1
(
t
)
d
t
=
∫
f
(
a
)
f
(
f
−
1
(
y
)
)
f
−
1
(
t
)
d
t
=
f
−
1
(
y
)
f
(
f
−
1
(
y
)
)
−
a
f
(
a
)
−
∫
a
f
−
1
(
y
)
f
(
s
)
d
s
=
y
f
−
1
(
y
)
−
a
f
(
a
)
−
F
(
f
−
1
(
y
)
)
+
F
(
a
)
=
y
f
−
1
(
y
)
−
F
(
f
−
1
(
y
)
)
−
a
f
(
a
)
+
F
(
a
)
,
{\displaystyle {}{\begin{aligned}G(y)&=\int _{f(a)}^{y}f^{-1}(t)\,dt\\&=\int _{f(a)}^{f(f^{-1}(y))}f^{-1}(t)\,dt\\&=f^{-1}(y)f(f^{-1}(y))-af(a)-\int _{a}^{f^{-1}(y)}f(s)\,ds\\&=yf^{-1}(y)-af(a)-F(f^{-1}(y))+F(a)\\&=yf^{-1}(y)-F(f^{-1}(y))-af(a)+F(a),\end{aligned}}}
where
−
a
f
(
a
)
+
F
(
a
)
{\displaystyle {}-af(a)+F(a)}
is a constant of integration.