for x being Real st x in dom tan holds
( x + PI in dom tan & x - PI in dom tan & tan . x = tan . (x + PI) )
proof
let x be Real; :: thesis: ( x in dom tan implies ( x + PI in dom tan & x - PI in dom tan & tan . x = tan . (x + PI) ) )
assume A1: x in dom tan ; :: thesis: ( x + PI in dom tan & x - PI in dom tan & tan . x = tan . (x + PI) )
then x in () /\ (() \ ()) by RFUNCT_1:def 1;
then ( x in dom sin & x in () \ () ) by XBOOLE_0:def 4;
then ( x in dom sin & x in dom cos & not x in cos " ) by XBOOLE_0:def 5;
then not cos . x in by FUNCT_1:def 7;
then A2: cos . x <> 0 by TARSKI:def 1;
A3: cos . (x + PI) = - (cos . x) by SIN_COS:78;
then not cos . (x + PI) in by ;
then ( x + PI in dom sin & x + PI in dom cos & not x + PI in cos " ) by ;
then ( x + PI in dom sin & x + PI in () \ () ) by XBOOLE_0:def 5;
then A4: x + PI in () /\ (() \ ()) by XBOOLE_0:def 4;
cos . (x - PI) = cos . ((x - PI) + (2 * PI)) by SIN_COS:78
.= cos . (x + PI) ;
then not cos . (x - PI) in by ;
then ( x - PI in dom sin & x - PI in dom cos & not x - PI in cos " ) by ;
then ( x - PI in dom sin & x - PI in () \ () ) by XBOOLE_0:def 5;
then A5: x - PI in () /\ (() \ ()) by XBOOLE_0:def 4;
then ( x + PI in dom tan & x - PI in dom tan ) by ;
then tan . (x + PI) = (sin . (x + PI)) / (cos . (x + PI)) by RFUNCT_1:def 1
.= (- (sin . x)) / (cos . (x + PI)) by SIN_COS:78
.= (- (sin . x)) / (- (cos . x)) by SIN_COS:78
.= (sin . x) / (cos . x) by XCMPLX_1:191
.= tan . x by ;
hence ( x + PI in dom tan & x - PI in dom tan & tan . x = tan . (x + PI) ) by ; :: thesis: verum
end;
hence tan is PI -periodic by Th1; :: thesis: verum