let x be Real; for f being PartFunc of REAL,REAL st f is_differentiable_in x & f . x > - 1 & f . x < 1 holds
( arctan * f is_differentiable_in x & diff ((arctan * f),x) = (diff (f,x)) / (1 + ((f . x) ^2)) )
let f be PartFunc of REAL,REAL; ( f is_differentiable_in x & f . x > - 1 & f . x < 1 implies ( arctan * f is_differentiable_in x & diff ((arctan * f),x) = (diff (f,x)) / (1 + ((f . x) ^2)) ) )
assume that
A1:
f is_differentiable_in x
and
A2:
f . x > - 1
and
A3:
f . x < 1
; ( arctan * f is_differentiable_in x & diff ((arctan * f),x) = (diff (f,x)) / (1 + ((f . x) ^2)) )
f . x in ].(- 1),1.[
by A2, A3, XXREAL_1:4;
then A4:
arctan is_differentiable_in f . x
by Th73, FDIFF_1:9;
then diff ((arctan * f),x) =
(diff (arctan,(f . x))) * (diff (f,x))
by A1, FDIFF_2:13
.=
(diff (f,x)) * (1 / (1 + ((f . x) ^2)))
by A2, A3, Th75
.=
(diff (f,x)) / (1 + ((f . x) ^2))
;
hence
( arctan * f is_differentiable_in x & diff ((arctan * f),x) = (diff (f,x)) / (1 + ((f . x) ^2)) )
by A1, A4, FDIFF_2:13; verum