set X = sec .: ].0,(PI / 2).[;
set g1 = arcsec1 | (sec .: ].0,(PI / 2).[);
set f = sec | [.0,(PI / 2).[;
set g = (sec | [.0,(PI / 2).[) | ].0,(PI / 2).[;
A1: (sec | [.0,(PI / 2).[) | ].0,(PI / 2).[ = sec | ].0,(PI / 2).[ by RELAT_1:74, XXREAL_1:22;
A2: dom ((((sec | [.0,(PI / 2).[) | ].0,(PI / 2).[) | ].0,(PI / 2).[) ") = rng (((sec | [.0,(PI / 2).[) | ].0,(PI / 2).[) | ].0,(PI / 2).[) by FUNCT_1:33
.= rng (sec | ].0,(PI / 2).[) by A1, RELAT_1:72
.= sec .: ].0,(PI / 2).[ by RELAT_1:115 ;
A3: (((sec | [.0,(PI / 2).[) | ].0,(PI / 2).[) | ].0,(PI / 2).[) " = ((sec | [.0,(PI / 2).[) | ].0,(PI / 2).[) " by RELAT_1:72
.= arcsec1 | ((sec | [.0,(PI / 2).[) .: ].0,(PI / 2).[) by RFUNCT_2:17
.= arcsec1 | (rng ((sec | [.0,(PI / 2).[) | ].0,(PI / 2).[)) by RELAT_1:115
.= arcsec1 | (rng (sec | ].0,(PI / 2).[)) by RELAT_1:74, XXREAL_1:22
.= arcsec1 | (sec .: ].0,(PI / 2).[) by RELAT_1:115 ;
A4: (sec | [.0,(PI / 2).[) | ].0,(PI / 2).[ is_differentiable_on ].0,(PI / 2).[ by A1, Th5, FDIFF_2:16;
now :: thesis: for x0 being Real st x0 in ].0,(PI / 2).[ holds
diff (((sec | [.0,(PI / 2).[) | ].0,(PI / 2).[),x0) > 0
A5: for x0 being Real st x0 in ].0,(PI / 2).[ holds
(sin . x0) / ((cos . x0) ^2) > 0
proof
let x0 be Real; :: thesis: ( x0 in ].0,(PI / 2).[ implies (sin . x0) / ((cos . x0) ^2) > 0 )
assume A6: x0 in ].0,(PI / 2).[ ; :: thesis: (sin . x0) / ((cos . x0) ^2) > 0
].0,(PI / 2).[ c= ].(- (PI / 2)),(PI / 2).[ by XXREAL_1:46;
then A7: cos . x0 > 0 by A6, COMPTRIG:11;
].0,(PI / 2).[ c= ].0,PI.[ by COMPTRIG:5, XXREAL_1:46;
then sin . x0 > 0 by A6, COMPTRIG:7;
hence (sin . x0) / ((cos . x0) ^2) > 0 by A7; :: thesis: verum
end;
let x0 be Real; :: thesis: ( x0 in ].0,(PI / 2).[ implies diff (((sec | [.0,(PI / 2).[) | ].0,(PI / 2).[),x0) > 0 )
assume A8: x0 in ].0,(PI / 2).[ ; :: thesis: diff (((sec | [.0,(PI / 2).[) | ].0,(PI / 2).[),x0) > 0
diff (((sec | [.0,(PI / 2).[) | ].0,(PI / 2).[),x0) = (((sec | [.0,(PI / 2).[) | ].0,(PI / 2).[) `| ].0,(PI / 2).[) . x0 by A4, A8, FDIFF_1:def 7
.= ((sec | ].0,(PI / 2).[) `| ].0,(PI / 2).[) . x0 by RELAT_1:74, XXREAL_1:22
.= (sec `| ].0,(PI / 2).[) . x0 by Th5, FDIFF_2:16
.= diff (sec,x0) by A8, Th5, FDIFF_1:def 7
.= (sin . x0) / ((cos . x0) ^2) by A8, Th5 ;
hence diff (((sec | [.0,(PI / 2).[) | ].0,(PI / 2).[),x0) > 0 by A8, A5; :: thesis: verum
end;
then A9: arcsec1 | (sec .: ].0,(PI / 2).[) is_differentiable_on sec .: ].0,(PI / 2).[ by A2, A4, A3, Lm21, FDIFF_2:48;
A10: for x being Real st x in sec .: ].0,(PI / 2).[ holds
arcsec1 | (sec .: ].0,(PI / 2).[) is_differentiable_in x
proof
let x be Real; :: thesis: ( x in sec .: ].0,(PI / 2).[ implies arcsec1 | (sec .: ].0,(PI / 2).[) is_differentiable_in x )
assume x in sec .: ].0,(PI / 2).[ ; :: thesis: arcsec1 | (sec .: ].0,(PI / 2).[) is_differentiable_in x
then (arcsec1 | (sec .: ].0,(PI / 2).[)) | (sec .: ].0,(PI / 2).[) is_differentiable_in x by A9, FDIFF_1:def 6;
hence arcsec1 | (sec .: ].0,(PI / 2).[) is_differentiable_in x by RELAT_1:72; :: thesis: verum
end;
sec .: ].0,(PI / 2).[ c= dom arcsec1 by A2, A3, RELAT_1:60;
hence arcsec1 is_differentiable_on sec .: ].0,(PI / 2).[ by A10, FDIFF_1:def 6; :: thesis: verum