set P = PI / 2;
set I = ].(- (PI / 2)),(PI / 2).[;
REAL c= rng (tan | ].(- (PI / 2)),(PI / 2).[)
proof
let r be object ; :: according to TARSKI:def 3 :: thesis: ( not r in REAL or r in rng (tan | ].(- (PI / 2)),(PI / 2).[) )
assume r in REAL ; :: thesis: r in rng (tan | ].(- (PI / 2)),(PI / 2).[)
then reconsider r = r as Real ;
per cases ( r > 0 or r < 0 or r = 0 ) ;
suppose A1: r > 0 ; :: thesis: r in rng (tan | ].(- (PI / 2)),(PI / 2).[)
then consider s being Real such that
A2: ( 0 <= s & s < PI / 2 & tan . s = r ) by Lm3;
s in dom tan by A1, A2, FUNCT_1:def 2;
hence r in rng (tan | ].(- (PI / 2)),(PI / 2).[) by XXREAL_1:4, A2, FUNCT_1:50; :: thesis: verum
end;
suppose A3: r < 0 ; :: thesis: r in rng (tan | ].(- (PI / 2)),(PI / 2).[)
then consider s being Real such that
A4: ( 0 <= s & s < PI / 2 & tan . s = - r ) by Lm3;
A5: s in dom tan by A3, A4, FUNCT_1:def 2;
A6: ( dom sin = REAL & dom cos = REAL ) by FUNCT_2:def 1;
then dom tan = REAL /\ (REAL \ (cos " {0})) by RFUNCT_1:def 1;
then s in REAL \ (cos " {0}) by A5, XBOOLE_0:def 4;
then ( s in REAL & not s in cos " {0} ) by XBOOLE_0:def 5;
then not cos . s in {0} by A6, FUNCT_1:def 7;
then ( cos . s <> 0 & cos . s = cos . (- s) ) by TARSKI:def 1, SIN_COS:30;
then ( tan . s = tan s & tan . (- s) = tan (- s) & - (tan s) = tan (- s) ) by SIN_COS9:15, SIN_COS4:1;
then A7: ( - s in dom tan & tan . (- s) = r ) by A3, A4, FUNCT_1:def 2;
( PI / 2 > - s & - s > - (PI / 2) ) by A4, XREAL_1:24;
hence r in rng (tan | ].(- (PI / 2)),(PI / 2).[) by A7, FUNCT_1:50, XXREAL_1:4; :: thesis: verum
end;
end;
end;
hence rng (tan | ].(- (PI / 2)),(PI / 2).[) = REAL by XBOOLE_0:def 10; :: thesis: verum