let x be set ; ( x in [.(PI / 4),((3 / 4) * PI).] implies cot . x in [.(- 1),1.] )
A1:
(PI / 4) * 3 > PI / 4
by XREAL_1:155;
assume
x in [.(PI / 4),((3 / 4) * PI).]
; cot . x in [.(- 1),1.]
then
x in ].(PI / 4),((3 / 4) * PI).[ \/ {(PI / 4),((3 / 4) * PI)}
by A1, XXREAL_1:128;
then A2:
( x in ].(PI / 4),((3 / 4) * PI).[ or x in {(PI / 4),((3 / 4) * PI)} )
by XBOOLE_0:def 3;
per cases
( x in ].(PI / 4),((3 / 4) * PI).[ or x = PI / 4 or x = (3 / 4) * PI )
by A2, TARSKI:def 2;
suppose A3:
x in ].(PI / 4),((3 / 4) * PI).[
;
cot . x in [.(- 1),1.]then
x in { s where s is Real : ( PI / 4 < s & s < (3 / 4) * PI ) }
by RCOMP_1:def 2;
then A4:
ex
s being
Real st
(
s = x &
PI / 4
< s &
s < (3 / 4) * PI )
;
A5:
[.(PI / 4),((3 / 4) * PI).] c= ].0,PI.[
by Lm9, Lm10, XXREAL_2:def 12;
then A6:
cot | [.(PI / 4),((3 / 4) * PI).] is
decreasing
by Th8, RFUNCT_2:29;
x in { s where s is Real : ( PI / 4 < s & s < (3 / 4) * PI ) }
by A3, RCOMP_1:def 2;
then A7:
ex
s being
Real st
(
s = x &
PI / 4
< s &
s < (3 / 4) * PI )
;
A8:
].(PI / 4),((3 / 4) * PI).[ c= [.(PI / 4),((3 / 4) * PI).]
by XXREAL_1:25;
A9:
[.(PI / 4),((3 / 4) * PI).] /\ (dom cot) = [.(PI / 4),((3 / 4) * PI).]
by A5, Th2, XBOOLE_1:1, XBOOLE_1:28;
(3 / 4) * PI in { s where s is Real : ( PI / 4 <= s & s <= (3 / 4) * PI ) }
by A1;
then
(3 / 4) * PI in [.(PI / 4),((3 / 4) * PI).] /\ (dom cot)
by A9, RCOMP_1:def 1;
then A10:
- 1
< cot . x
by A3, A6, A9, A8, A7, Th18, RFUNCT_2:21;
PI / 4
in { s where s is Real : ( PI / 4 <= s & s <= (3 / 4) * PI ) }
by A1;
then
PI / 4
in [.(PI / 4),((3 / 4) * PI).] /\ (dom cot)
by A9, RCOMP_1:def 1;
then
cot . x < 1
by A3, A6, A9, A8, A4, Th18, RFUNCT_2:21;
then
cot . x in { s where s is Real : ( - 1 < s & s < 1 ) }
by A10;
then A11:
cot . x in ].(- 1),1.[
by RCOMP_1:def 2;
].(- 1),1.[ c= [.(- 1),1.]
by XXREAL_1:25;
hence
cot . x in [.(- 1),1.]
by A11;
verum end;