set S = { ].((- (PI / 2)) + (PI * i)),((PI / 2) + (PI * i)).[ where i is Integer : verum } ;
set T = dom tan;
A1: ( dom sin = REAL & dom cos = REAL ) by FUNCT_2:def 1;
then dom tan = REAL /\ (REAL \ (cos " {0})) by RFUNCT_1:def 1;
then A2: dom tan = REAL \ (cos " {0}) by XBOOLE_1:28;
thus dom tan c= union { ].((- (PI / 2)) + (PI * i)),((PI / 2) + (PI * i)).[ where i is Integer : verum } :: according to XBOOLE_0:def 10 :: thesis: union { ].((- (PI / 2)) + (PI * i)),((PI / 2) + (PI * i)).[ where i is Integer : verum } c= dom tan

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in dom tan or x in union { ].((- (PI / 2)) + (PI * i)),((PI / 2) + (PI * i)).[ where i is Integer : verum } )
assume A3: x in dom tan ; :: thesis: x in union { ].((- (PI / 2)) + (PI * i)),((PI / 2) + (PI * i)).[ where i is Integer : verum }
then reconsider x = x as Element of REAL ;
not x in cos " {0} by A2, A3, XBOOLE_0:def 5;
then not cos x in {0} by A1, FUNCT_1:def 7;
then A4: cos x <> 0 by TARSKI:def 1;
set xP = (x - (PI / 2)) / PI;
set E = [\((x - (PI / 2)) / PI)/];
A5: ].((- (PI / 2)) + (PI * ([\((x - (PI / 2)) / PI)/] + 1))),((PI / 2) + (PI * ([\((x - (PI / 2)) / PI)/] + 1))).[ in { ].((- (PI / 2)) + (PI * i)),((PI / 2) + (PI * i)).[ where i is Integer : verum } ;
((x - (PI / 2)) / PI) * PI = x - (PI / 2) by XCMPLX_1:87;
then A6: x = (PI / 2) + (((x - (PI / 2)) / PI) * PI) ;
then A7: [\((x - (PI / 2)) / PI)/] <> (x - (PI / 2)) / PI by Th14, A4;
( [\((x - (PI / 2)) / PI)/] <= (x - (PI / 2)) / PI & (x - (PI / 2)) / PI < [\((x - (PI / 2)) / PI)/] + 1 ) by INT_1:def 6, INT_1:29;
then ( [\((x - (PI / 2)) / PI)/] < (x - (PI / 2)) / PI & (x - (PI / 2)) / PI < [\((x - (PI / 2)) / PI)/] + 1 ) by A7, XXREAL_0:1;
then ( [\((x - (PI / 2)) / PI)/] * PI < ((x - (PI / 2)) / PI) * PI & ((x - (PI / 2)) / PI) * PI < ([\((x - (PI / 2)) / PI)/] + 1) * PI ) by XREAL_1:68;
then ( (PI / 2) + ([\((x - (PI / 2)) / PI)/] * PI) < x & x < (PI / 2) + (([\((x - (PI / 2)) / PI)/] + 1) * PI) ) by A6, XREAL_1:6;
then x in ].((- (PI / 2)) + (PI * ([\((x - (PI / 2)) / PI)/] + 1))),((PI / 2) + (PI * ([\((x - (PI / 2)) / PI)/] + 1))).[ by XXREAL_1:4;
hence x in union { ].((- (PI / 2)) + (PI * i)),((PI / 2) + (PI * i)).[ where i is Integer : verum } by A5, TARSKI:def 4; :: thesis: verum

end;

for X being set st X in { ].((- (PI / 2)) + (PI * i)),((PI / 2) + (PI * i)).[ where i is Integer : verum } holds
X c= dom tan

proof

let X be set ; :: thesis: ( X in { ].((- (PI / 2)) + (PI * i)),((PI / 2) + (PI * i)).[ where i is Integer : verum } implies X c= dom tan )
assume X in { ].((- (PI / 2)) + (PI * i)),((PI / 2) + (PI * i)).[ where i is Integer : verum } ; :: thesis: X c= dom tan
then consider i being Integer such that
A8: X = ].((- (PI / 2)) + (PI * i)),((PI / 2) + (PI * i)).[ ;
A9: X /\ (cos " {0}) = {}

proof

assume X /\ (cos " {0}) <> {} ; :: thesis: contradiction
then consider r being object such that
A10: r in X /\ (cos " {0}) by XBOOLE_0:7;
reconsider r = r as Element of REAL by A10;
r in cos " {0} by A10, XBOOLE_0:def 4;
then A11: cos . r in {0} by FUNCT_1:def 7;
cos . r <> 0

proof

A12: r in X by A10, XBOOLE_0:def 4;
then A13: ( (- (PI / 2)) + (PI * i) < r & r < (PI / 2) + (PI * i) ) by A8, XXREAL_1:4;

per cases ( i is even or i is odd ) ;

suppose i is even ; :: thesis: cos . r <> 0

then consider j being Integer such that
A14: i = 2 * j by INT_1:def 3, ABIAN:def 1;
( - (PI / 2) < r - (PI * i) & r - (PI * i) < PI / 2 ) by A13, XREAL_1:19, XREAL_1:20;
then r - (PI * i) in ].(- (PI / 2)),(PI / 2).[ by XXREAL_1:4;
then cos (r + ((2 * PI) * (- j))) > 0 by A14, COMPTRIG:11;
then cos r > 0 by COMPLEX2:9;
hence cos . r <> 0 ; :: thesis: verum

end;

suppose i is odd ; :: thesis: cos . r <> 0

then consider j being Integer such that
A15: i = (2 * j) + 1 by ABIAN:1;
( ((- (PI / 2)) + PI) + ((2 * PI) * j) < r & r < ((PI / 2) + PI) + ((2 * PI) * j) ) by A12, A8, XXREAL_1:4, A15;
then ( (- (PI / 2)) + PI < r - ((2 * PI) * j) & r - ((2 * PI) * j) < (PI / 2) + PI ) by XREAL_1:19, XREAL_1:20;
then r - ((2 * PI) * j) in ].(PI / 2),((3 / 2) * PI).[ by XXREAL_1:4;
then cos (r + ((2 * PI) * (- j))) < 0 by COMPTRIG:13;
then cos r < 0 by COMPLEX2:9;
hence cos . r <> 0 ; :: thesis: verum

end;

end;

end;

hence contradiction by A11, TARSKI:def 1; :: thesis: verum

end;

X \ (cos " {0}) c= dom tan by A8, A2, XBOOLE_1:33;
hence X c= dom tan by A9, XBOOLE_0:def 7, XBOOLE_1:83; :: thesis: verum

end;

hence union { ].((- (PI / 2)) + (PI * i)),((PI / 2) + (PI * i)).[ where i is Integer : verum } c= dom tan by ZFMISC_1:76; :: thesis: verum