let r be Real; ( arccos is_differentiable_on ].(- 1),1.[ & ( - 1 < r & r < 1 implies diff (arccos,r) = - (1 / (sqrt (1 - (r ^2)))) ) )
set g = arccos | ].(- 1),1.[;
set h = cos | [.0,PI.];
set f = cos | ].0,PI.[;
A1: dom (cos | ].0,PI.[) =
].0,PI.[ /\ REAL
by RELAT_1:61, SIN_COS:24
.=
].0,PI.[
by XBOOLE_1:28
;
set x = arccos . r;
set s = sqrt (1 - (r ^2));
A2:
].(- 1),1.[ c= dom arccos
by Th86, XXREAL_1:25;
A3:
cos is_differentiable_on ].0,PI.[
by FDIFF_1:26, SIN_COS:67;
then A4:
cos | ].0,PI.[ is_differentiable_on ].0,PI.[
by FDIFF_2:16;
A5:
now for x0 being Real st x0 in ].0,PI.[ holds
0 > diff ((cos | ].0,PI.[),x0)let x0 be
Real;
( x0 in ].0,PI.[ implies 0 > diff ((cos | ].0,PI.[),x0) )assume A6:
x0 in ].0,PI.[
;
0 > diff ((cos | ].0,PI.[),x0)A7:
- (- (sin . x0)) > 0
by A6, COMPTRIG:7;
diff (
(cos | ].0,PI.[),
x0) =
((cos | ].0,PI.[) `| ].0,PI.[) . x0
by A4, A6, FDIFF_1:def 7
.=
(cos `| ].0,PI.[) . x0
by A3, FDIFF_2:16
.=
diff (
cos,
x0)
by A3, A6, FDIFF_1:def 7
.=
- (sin . x0)
by SIN_COS:67
;
hence
0 > diff (
(cos | ].0,PI.[),
x0)
by A7;
verum end;
A8: (cos | ].0,PI.[) " =
((cos | [.0,PI.]) | ].0,PI.[) "
by RELAT_1:74, XXREAL_1:25
.=
((cos | [.0,PI.]) ") | ((cos | [.0,PI.]) .: ].0,PI.[)
by RFUNCT_2:17
.=
arccos | ].(- 1),1.[
by Th50, RELAT_1:129, XXREAL_1:25
;
then A9:
( (cos | ].0,PI.[) | ].0,PI.[ = cos | ].0,PI.[ & dom ((cos | ].0,PI.[) ") = ].(- 1),1.[ )
by Th86, RELAT_1:62, RELAT_1:72, XXREAL_1:25;
then A10:
arccos | ].(- 1),1.[ is_differentiable_on ].(- 1),1.[
by A8, A4, A1, A5, FDIFF_2:48;
then
for x being Real st x in ].(- 1),1.[ holds
arccos | ].(- 1),1.[ is_differentiable_in x
by FDIFF_1:9;
hence A11:
arccos is_differentiable_on ].(- 1),1.[
by A2, FDIFF_1:def 6; ( - 1 < r & r < 1 implies diff (arccos,r) = - (1 / (sqrt (1 - (r ^2)))) )
assume A12:
( - 1 < r & r < 1 )
; diff (arccos,r) = - (1 / (sqrt (1 - (r ^2))))
then A13:
r in ].(- 1),1.[
by XXREAL_1:4;
then A14:
(arccos | ].(- 1),1.[) . r = arccos . r
by FUNCT_1:49;
arccos . r = arccos r
;
then
( 0 < arccos . r & arccos . r < PI )
by A12, Th100;
then A15:
arccos . r in ].0,PI.[
by XXREAL_1:4;
then A16: diff ((cos | ].0,PI.[),(arccos . r)) =
((cos | ].0,PI.[) `| ].0,PI.[) . (arccos . r)
by A4, FDIFF_1:def 7
.=
(cos `| ].0,PI.[) . (arccos . r)
by A3, FDIFF_2:16
.=
diff (cos,(arccos . r))
by A3, A15, FDIFF_1:def 7
.=
- (sin . (arccos . r))
by SIN_COS:67
.=
- (sin (arccos r))
by SIN_COS:def 17
.=
- (sqrt (1 - (r ^2)))
by A12, Th104
;
thus diff (arccos,r) =
(arccos `| ].(- 1),1.[) . r
by A11, A13, FDIFF_1:def 7
.=
((arccos | ].(- 1),1.[) `| ].(- 1),1.[) . r
by A11, FDIFF_2:16
.=
diff ((arccos | ].(- 1),1.[),r)
by A10, A13, FDIFF_1:def 7
.=
1 / (- (sqrt (1 - (r ^2))))
by A8, A9, A4, A1, A5, A13, A14, A16, FDIFF_2:48
.=
(- 1) / (sqrt (1 - (r ^2)))
by XCMPLX_1:192
.=
- (1 / (sqrt (1 - (r ^2))))
by XCMPLX_1:187
; verum