for x being Real st x in dom cot holds

( x + PI in dom cot & x - PI in dom cot & cot . x = cot . (x + PI) )

( x + PI in dom cot & x - PI in dom cot & cot . x = cot . (x + PI) )

proof

hence
cot is PI -periodic
by Th1; :: thesis: verum
let x be Real; :: thesis: ( x in dom cot implies ( x + PI in dom cot & x - PI in dom cot & cot . x = cot . (x + PI) ) )

assume A1: x in dom cot ; :: thesis: ( x + PI in dom cot & x - PI in dom cot & cot . x = cot . (x + PI) )

then x in (dom cos) /\ ((dom sin) \ (sin " {0})) by RFUNCT_1:def 1;

then ( x in dom cos & x in (dom sin) \ (sin " {0}) ) by XBOOLE_0:def 4;

then ( x in dom cos & x in dom sin & not x in sin " {0} ) by XBOOLE_0:def 5;

then not sin . x in {0} by FUNCT_1:def 7;

then A2: sin . x <> 0 by TARSKI:def 1;

A3: sin . (x + PI) = - (sin . x) by SIN_COS:78;

then not sin . (x + PI) in {0} by A2, TARSKI:def 1;

then ( x + PI in dom cos & x + PI in dom sin & not x + PI in sin " {0} ) by FUNCT_1:def 7, SIN_COS:24, XREAL_0:def 1;

then ( x + PI in dom cos & x + PI in (dom sin) \ (sin " {0}) ) by XBOOLE_0:def 5;

then A4: x + PI in (dom cos) /\ ((dom sin) \ (sin " {0})) by XBOOLE_0:def 4;

sin . (x - PI) = sin . ((x - PI) + (2 * PI)) by SIN_COS:78

.= sin . (x + PI) ;

then not sin . (x - PI) in {0} by A2, A3, TARSKI:def 1;

then ( x - PI in dom cos & x - PI in dom sin & not x - PI in sin " {0} ) by FUNCT_1:def 7, SIN_COS:24, XREAL_0:def 1;

then ( x - PI in dom cos & x - PI in (dom sin) \ (sin " {0}) ) by XBOOLE_0:def 5;

then A5: x - PI in (dom cos) /\ ((dom sin) \ (sin " {0})) by XBOOLE_0:def 4;

then ( x + PI in dom cot & x - PI in dom cot ) by A4, RFUNCT_1:def 1;

then cot . (x + PI) = (cos . (x + PI)) / (sin . (x + PI)) by RFUNCT_1:def 1

.= (- (cos . x)) / (sin . (x + PI)) by SIN_COS:78

.= (- (cos . x)) / (- (sin . x)) by SIN_COS:78

.= (cos . x) / (sin . x) by XCMPLX_1:191

.= cot . x by A1, RFUNCT_1:def 1 ;

hence ( x + PI in dom cot & x - PI in dom cot & cot . x = cot . (x + PI) ) by A4, A5, RFUNCT_1:def 1; :: thesis: verum

end;assume A1: x in dom cot ; :: thesis: ( x + PI in dom cot & x - PI in dom cot & cot . x = cot . (x + PI) )

then x in (dom cos) /\ ((dom sin) \ (sin " {0})) by RFUNCT_1:def 1;

then ( x in dom cos & x in (dom sin) \ (sin " {0}) ) by XBOOLE_0:def 4;

then ( x in dom cos & x in dom sin & not x in sin " {0} ) by XBOOLE_0:def 5;

then not sin . x in {0} by FUNCT_1:def 7;

then A2: sin . x <> 0 by TARSKI:def 1;

A3: sin . (x + PI) = - (sin . x) by SIN_COS:78;

then not sin . (x + PI) in {0} by A2, TARSKI:def 1;

then ( x + PI in dom cos & x + PI in dom sin & not x + PI in sin " {0} ) by FUNCT_1:def 7, SIN_COS:24, XREAL_0:def 1;

then ( x + PI in dom cos & x + PI in (dom sin) \ (sin " {0}) ) by XBOOLE_0:def 5;

then A4: x + PI in (dom cos) /\ ((dom sin) \ (sin " {0})) by XBOOLE_0:def 4;

sin . (x - PI) = sin . ((x - PI) + (2 * PI)) by SIN_COS:78

.= sin . (x + PI) ;

then not sin . (x - PI) in {0} by A2, A3, TARSKI:def 1;

then ( x - PI in dom cos & x - PI in dom sin & not x - PI in sin " {0} ) by FUNCT_1:def 7, SIN_COS:24, XREAL_0:def 1;

then ( x - PI in dom cos & x - PI in (dom sin) \ (sin " {0}) ) by XBOOLE_0:def 5;

then A5: x - PI in (dom cos) /\ ((dom sin) \ (sin " {0})) by XBOOLE_0:def 4;

then ( x + PI in dom cot & x - PI in dom cot ) by A4, RFUNCT_1:def 1;

then cot . (x + PI) = (cos . (x + PI)) / (sin . (x + PI)) by RFUNCT_1:def 1

.= (- (cos . x)) / (sin . (x + PI)) by SIN_COS:78

.= (- (cos . x)) / (- (sin . x)) by SIN_COS:78

.= (cos . x) / (sin . x) by XCMPLX_1:191

.= cot . x by A1, RFUNCT_1:def 1 ;

hence ( x + PI in dom cot & x - PI in dom cot & cot . x = cot . (x + PI) ) by A4, A5, RFUNCT_1:def 1; :: thesis: verum