set f = tan | ].(- (PI / 2)),(PI / 2).[;
A1: dom ((tan | ].(- (PI / 2)),(PI / 2).[) ") = rng (tan | ].(- (PI / 2)),(PI / 2).[) by FUNCT_1:33
.= tan .: ].(- (PI / 2)),(PI / 2).[ by RELAT_1:115 ;
dom (tan | ].(- (PI / 2)),(PI / 2).[) = (dom tan) /\ ].(- (PI / 2)),(PI / 2).[ by RELAT_1:61;
then A2: ].(- (PI / 2)),(PI / 2).[ c= dom (tan | ].(- (PI / 2)),(PI / 2).[) by Th1, XBOOLE_1:19;
A3: tan | ].(- (PI / 2)),(PI / 2).[ is_differentiable_on ].(- (PI / 2)),(PI / 2).[ by Lm1, FDIFF_2:16;
A4: now :: thesis: for x0 being Real st x0 in ].(- (PI / 2)),(PI / 2).[ holds
0 < diff ((tan | ].(- (PI / 2)),(PI / 2).[),x0)
A5: for x0 being Real st x0 in ].(- (PI / 2)),(PI / 2).[ holds
1 / ((cos . x0) ^2) > 0
proof
let x0 be Real; :: thesis: ( x0 in ].(- (PI / 2)),(PI / 2).[ implies 1 / ((cos . x0) ^2) > 0 )
assume x0 in ].(- (PI / 2)),(PI / 2).[ ; :: thesis: 1 / ((cos . x0) ^2) > 0
then 0 < cos . x0 by COMPTRIG:11;
then (cos . x0) ^2 > 0 ;
then 1 / ((cos . x0) ^2) > 0 / ((cos . x0) ^2) ;
hence 1 / ((cos . x0) ^2) > 0 ; :: thesis: verum
end;
let x0 be Real; :: thesis: ( x0 in ].(- (PI / 2)),(PI / 2).[ implies 0 < diff ((tan | ].(- (PI / 2)),(PI / 2).[),x0) )
assume A6: x0 in ].(- (PI / 2)),(PI / 2).[ ; :: thesis: 0 < diff ((tan | ].(- (PI / 2)),(PI / 2).[),x0)
diff ((tan | ].(- (PI / 2)),(PI / 2).[),x0) = ((tan | ].(- (PI / 2)),(PI / 2).[) `| ].(- (PI / 2)),(PI / 2).[) . x0 by A3, A6, FDIFF_1:def 7
.= (tan `| ].(- (PI / 2)),(PI / 2).[) . x0 by Lm1, FDIFF_2:16
.= diff (tan,x0) by A6, Lm1, FDIFF_1:def 7
.= 1 / ((cos . x0) ^2) by A6, Lm3 ;
hence 0 < diff ((tan | ].(- (PI / 2)),(PI / 2).[),x0) by A6, A5; :: thesis: verum
end;
(tan | ].(- (PI / 2)),(PI / 2).[) | ].(- (PI / 2)),(PI / 2).[ = tan | ].(- (PI / 2)),(PI / 2).[ by RELAT_1:72;
hence arctan is_differentiable_on tan .: ].(- (PI / 2)),(PI / 2).[ by A1, A3, A2, A4, FDIFF_2:48; :: thesis: verum