now let y be
set ;
:: thesis: ( ( y in [.(- (PI / 2)),(- (PI / 4)).] implies ex x being set st
( x in dom (arccosec1 | [.(- (sqrt 2)),(- 1).]) & y = (arccosec1 | [.(- (sqrt 2)),(- 1).]) . x ) ) & ( ex x being set st
( x in dom (arccosec1 | [.(- (sqrt 2)),(- 1).]) & y = (arccosec1 | [.(- (sqrt 2)),(- 1).]) . x ) implies y in [.(- (PI / 2)),(- (PI / 4)).] ) )thus
(
y in [.(- (PI / 2)),(- (PI / 4)).] implies ex
x being
set st
(
x in dom (arccosec1 | [.(- (sqrt 2)),(- 1).]) &
y = (arccosec1 | [.(- (sqrt 2)),(- 1).]) . x ) )
:: thesis: ( ex x being set st
( x in dom (arccosec1 | [.(- (sqrt 2)),(- 1).]) & y = (arccosec1 | [.(- (sqrt 2)),(- 1).]) . x ) implies y in [.(- (PI / 2)),(- (PI / 4)).] )proof
assume A1:
y in [.(- (PI / 2)),(- (PI / 4)).]
;
:: thesis: ex x being set st
( x in dom (arccosec1 | [.(- (sqrt 2)),(- 1).]) & y = (arccosec1 | [.(- (sqrt 2)),(- 1).]) . x )
then reconsider y1 =
y as
Real ;
A2:
- (sqrt 2) < - 1
by SQUARE_1:84, XREAL_1:26;
y1 in [.(arccosec1 . (- 1)),(arccosec1 . (- (sqrt 2))).] \/ [.(arccosec1 . (- (sqrt 2))),(arccosec1 . (- 1)).]
by A1, Th75, XBOOLE_0:def 3;
then consider x being
Real such that A3:
x in [.(- (sqrt 2)),(- 1).]
and A4:
y1 = arccosec1 . x
by A2, Th95, Th47, FCONT_2:16;
take
x
;
:: thesis: ( x in dom (arccosec1 | [.(- (sqrt 2)),(- 1).]) & y = (arccosec1 | [.(- (sqrt 2)),(- 1).]) . x )
thus
(
x in dom (arccosec1 | [.(- (sqrt 2)),(- 1).]) &
y = (arccosec1 | [.(- (sqrt 2)),(- 1).]) . x )
by A3, A4, Th47, FUNCT_1:72, RELAT_1:91;
:: thesis: verum
end; thus
( ex
x being
set st
(
x in dom (arccosec1 | [.(- (sqrt 2)),(- 1).]) &
y = (arccosec1 | [.(- (sqrt 2)),(- 1).]) . x ) implies
y in [.(- (PI / 2)),(- (PI / 4)).] )
:: thesis: verumproof
given x being
set such that A5:
x in dom (arccosec1 | [.(- (sqrt 2)),(- 1).])
and A6:
y = (arccosec1 | [.(- (sqrt 2)),(- 1).]) . x
;
:: thesis: y in [.(- (PI / 2)),(- (PI / 4)).]
A7:
dom (arccosec1 | [.(- (sqrt 2)),(- 1).]) = [.(- (sqrt 2)),(- 1).]
by Th47, RELAT_1:91;
reconsider x1 =
x as
Real by A5;
y = arccosec1 . x
by A5, A6, A7, FUNCT_1:72;
hence
y in [.(- (PI / 2)),(- (PI / 4)).]
by A5, A7, Th87;
:: thesis: verum
end; end;
hence
rng (arccosec1 | [.(- (sqrt 2)),(- 1).]) = [.(- (PI / 2)),(- (PI / 4)).]
by FUNCT_1:def 5; :: thesis: verum