let r be Real; :: thesis: ( - 1 <= r & r <= 1 implies diff (arctan,r) = 1 / (1 + (r ^2)) )
set g = arctan ;
set f = tan | ].(- (PI / 2)),(PI / 2).[;
set x = arctan . r;
assume that
A1: - 1 <= r and
A2: r <= 1 ; :: thesis: diff (arctan,r) = 1 / (1 + (r ^2))
A3: ((sin . (arctan . r)) ^2) + ((cos . (arctan . r)) ^2) = 1 by SIN_COS:28;
A4: tan | ].(- (PI / 2)),(PI / 2).[ is_differentiable_on ].(- (PI / 2)),(PI / 2).[ by Lm1, FDIFF_2:16;
A5: now :: thesis: for x0 being Real st x0 in ].(- (PI / 2)),(PI / 2).[ holds
0 < diff ((tan | ].(- (PI / 2)),(PI / 2).[),x0)
A6: 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 A7: 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 A4, A7, FDIFF_1:def 7
.= (tan `| ].(- (PI / 2)),(PI / 2).[) . x0 by Lm1, FDIFF_2:16
.= diff (tan,x0) by A7, Lm1, FDIFF_1:def 7
.= 1 / ((cos . x0) ^2) by A7, Lm3 ;
hence 0 < diff ((tan | ].(- (PI / 2)),(PI / 2).[),x0) by A7, A6; :: thesis: verum
end;
A8: r in [.(- 1),1.] by A1, A2, XXREAL_1:1;
then A9: arctan . r in [.(- (PI / 4)),(PI / 4).] by Th49;
arctan . r = arctan r ;
then A10: r = tan (arctan . r) by A1, A2, Th51
.= (sin (arctan . r)) / (cos (arctan . r)) by SIN_COS4:def 1 ;
dom (tan | ].(- (PI / 2)),(PI / 2).[) = (dom tan) /\ ].(- (PI / 2)),(PI / 2).[ by RELAT_1:61;
then A11: ].(- (PI / 2)),(PI / 2).[ c= dom (tan | ].(- (PI / 2)),(PI / 2).[) by Th1, XBOOLE_1:19;
A12: (tan | ].(- (PI / 2)),(PI / 2).[) | ].(- (PI / 2)),(PI / 2).[ = tan | ].(- (PI / 2)),(PI / 2).[ by RELAT_1:72;
A13: [.(- (PI / 4)),(PI / 4).] c= ].(- (PI / 2)),(PI / 2).[ by Lm7, Lm8, XXREAL_2:def 12;
then cos (arctan . r) <> 0 by A9, COMPTRIG:11;
then r * (cos (arctan . r)) = sin (arctan . r) by A10, XCMPLX_1:87;
then A14: 1 = ((cos (arctan . r)) ^2) * ((r ^2) + 1) by A3;
tan | ].(- (PI / 2)),(PI / 2).[ is_differentiable_on ].(- (PI / 2)),(PI / 2).[ by Lm1, FDIFF_2:16;
then diff ((tan | ].(- (PI / 2)),(PI / 2).[),(arctan . r)) = ((tan | ].(- (PI / 2)),(PI / 2).[) `| ].(- (PI / 2)),(PI / 2).[) . (arctan . r) by A9, A13, FDIFF_1:def 7
.= (tan `| ].(- (PI / 2)),(PI / 2).[) . (arctan . r) by Lm1, FDIFF_2:16
.= diff (tan,(arctan . r)) by A9, A13, Lm1, FDIFF_1:def 7
.= 1 / ((cos (arctan . r)) ^2) by A9, A13, Lm3 ;
then diff (arctan,r) = 1 / (1 / ((cos (arctan . r)) ^2)) by A8, A4, A5, A12, A11, Th23, FDIFF_2:48
.= 1 / ((r ^2) + 1) by A14, XCMPLX_1:73 ;
hence diff (arctan,r) = 1 / (1 + (r ^2)) ; :: thesis: verum