now let y be
set ;
:: thesis: ( ( y in [.(PI / 4),((3 / 4) * PI ).] implies ex x being set st
( x in dom (arccot | [.(- 1),1.]) & y = (arccot | [.(- 1),1.]) . x ) ) & ( ex x being set st
( x in dom (arccot | [.(- 1),1.]) & y = (arccot | [.(- 1),1.]) . x ) implies y in [.(PI / 4),((3 / 4) * PI ).] ) )thus
(
y in [.(PI / 4),((3 / 4) * PI ).] implies ex
x being
set st
(
x in dom (arccot | [.(- 1),1.]) &
y = (arccot | [.(- 1),1.]) . x ) )
:: thesis: ( ex x being set st
( x in dom (arccot | [.(- 1),1.]) & y = (arccot | [.(- 1),1.]) . x ) implies y in [.(PI / 4),((3 / 4) * PI ).] )proof
assume A1:
y in [.(PI / 4),((3 / 4) * PI ).]
;
:: thesis: ex x being set st
( x in dom (arccot | [.(- 1),1.]) & y = (arccot | [.(- 1),1.]) . x )
then reconsider y1 =
y as
Real ;
y1 in [.(arccot . 1),(arccot . (- 1)).] \/ [.(arccot . (- 1)),(arccot . 1).]
by A1, Th36, Th38, XBOOLE_0:def 3;
then consider x being
Real such that A3:
x in [.(- 1),1.]
and A4:
y1 = arccot . x
by Th52, Th22, FCONT_2:16;
take
x
;
:: thesis: ( x in dom (arccot | [.(- 1),1.]) & y = (arccot | [.(- 1),1.]) . x )
thus
(
x in dom (arccot | [.(- 1),1.]) &
y = (arccot | [.(- 1),1.]) . x )
by A3, A4, Th22, FUNCT_1:72, RELAT_1:91;
:: thesis: verum
end; thus
( ex
x being
set st
(
x in dom (arccot | [.(- 1),1.]) &
y = (arccot | [.(- 1),1.]) . x ) implies
y in [.(PI / 4),((3 / 4) * PI ).] )
:: thesis: verumproof
given x being
set such that A6:
x in dom (arccot | [.(- 1),1.])
and A7:
y = (arccot | [.(- 1),1.]) . x
;
:: thesis: y in [.(PI / 4),((3 / 4) * PI ).]
A8:
dom (arccot | [.(- 1),1.]) = [.(- 1),1.]
by Th22, RELAT_1:91;
reconsider x1 =
x as
Real by A6;
y = arccot . x
by A6, A7, A8, FUNCT_1:72;
hence
y in [.(PI / 4),((3 / 4) * PI ).]
by A6, A8, Th48;
:: thesis: verum
end; end;
hence
rng (arccot | [.(- 1),1.]) = [.(PI / 4),((3 / 4) * PI ).]
by FUNCT_1:def 5; :: thesis: verum