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;
( 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
;
( x + PI in dom tan & x - PI in dom tan & tan . x = tan . (x + PI) )
then
x in (dom sin) /\ ((dom cos) \ (cos " {0}))
by RFUNCT_1:def 1;
then
(
x in dom sin &
x in (dom cos) \ (cos " {0}) )
by XBOOLE_0:def 4;
then
(
x in dom sin &
x in dom cos & not
x in cos " {0} )
by XBOOLE_0:def 5;
then
not
cos . x in {0}
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 {0}
by A2, TARSKI:def 1;
then
(
x + PI in dom sin &
x + PI in dom cos & not
x + PI in cos " {0} )
by FUNCT_1:def 7, SIN_COS:24, XREAL_0:def 1;
then
(
x + PI in dom sin &
x + PI in (dom cos) \ (cos " {0}) )
by XBOOLE_0:def 5;
then A4:
x + PI in (dom sin) /\ ((dom cos) \ (cos " {0}))
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 {0}
by A2, A3, TARSKI:def 1;
then
(
x - PI in dom sin &
x - PI in dom cos & not
x - PI in cos " {0} )
by FUNCT_1:def 7, SIN_COS:24, XREAL_0:def 1;
then
(
x - PI in dom sin &
x - PI in (dom cos) \ (cos " {0}) )
by XBOOLE_0:def 5;
then A5:
x - PI in (dom sin) /\ ((dom cos) \ (cos " {0}))
by XBOOLE_0:def 4;
then
(
x + PI in dom tan &
x - PI in dom tan )
by A4, RFUNCT_1:def 1;
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 A1, RFUNCT_1:def 1
;
hence
(
x + PI in dom tan &
x - PI in dom tan &
tan . x = tan . (x + PI) )
by A4, A5, RFUNCT_1:def 1;
verum
end;
hence
tan is PI -periodic
by Th1; verum