let x be set ; :: thesis: ( x in [.(- 1),1.] implies arccot . x in [.(PI / 4),((3 / 4) * PI ).] )
assume x in [.(- 1),1.] ; :: thesis: arccot . x in [.(PI / 4),((3 / 4) * PI ).]
then x in ].(- 1),1.[ \/ {(- 1),1} by XXREAL_1:128;
then A1: ( x in ].(- 1),1.[ or x in {(- 1),1} ) by XBOOLE_0:def 3;
per cases ( x in ].(- 1),1.[ or x = - 1 or x = 1 ) by A1, TARSKI:def 2;
suppose A2: x in ].(- 1),1.[ ; :: thesis: arccot . x in [.(PI / 4),((3 / 4) * PI ).]
A4: - 1 in [.(- 1),1.] by XXREAL_1:1;
A5: [.(- 1),1.] /\ (dom arccot ) = [.(- 1),1.] by Th22, XBOOLE_1:28;
A7: ].(- 1),1.[ c= [.(- 1),1.] by XXREAL_1:25;
x in { s where s is Real : ( - 1 < s & s < 1 ) } by A2, RCOMP_1:def 2;
then A8: ex s being Real st
( s = x & - 1 < s & s < 1 ) ;
then A9: (3 / 4) * PI > arccot . x by A2, A4, A5, A7, Th36, Th46, RFUNCT_2:44;
1 in [.(- 1),1.] /\ (dom arccot ) by A5, XXREAL_1:1;
then arccot . x > PI / 4 by A2, A5, A7, A8, Th38, Th46, RFUNCT_2:44;
hence arccot . x in [.(PI / 4),((3 / 4) * PI ).] by A9, XXREAL_1:1; :: thesis: verum
end;
suppose A10: x = - 1 ; :: thesis: arccot . x in [.(PI / 4),((3 / 4) * PI ).]
PI in ].0 ,4.[ by SIN_COS:def 32;
then PI > 0 by XXREAL_1:4;
then PI / 4 > 0 / 4 by XREAL_1:76;
then PI / 4 < (PI / 4) * 3 by XREAL_1:157;
hence arccot . x in [.(PI / 4),((3 / 4) * PI ).] by A10, Th36, XXREAL_1:1; :: thesis: verum
end;
suppose A11: x = 1 ; :: thesis: arccot . x in [.(PI / 4),((3 / 4) * PI ).]
PI in ].0 ,4.[ by SIN_COS:def 32;
then PI > 0 by XXREAL_1:4;
then PI / 4 > 0 / 4 by XREAL_1:76;
then PI / 4 < (PI / 4) * 3 by XREAL_1:157;
hence arccot . x in [.(PI / 4),((3 / 4) * PI ).] by A11, Th38, XXREAL_1:1; :: thesis: verum
end;
end;