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