let k be Nat; cot is PI * (k + 1) -periodic
defpred S1[ Nat] means cot is PI * ($1 + 1) -periodic ;
A1:
S1[ 0 ]
by Lm11;
A2:
for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be
Nat;
( S1[k] implies S1[k + 1] )
assume A3:
cot is
PI * (k + 1) -periodic
;
S1[k + 1]
cot is
PI * ((k + 1) + 1) -periodic
proof
for
x being
Real st
x in dom cot holds
(
x + (PI * ((k + 1) + 1)) in dom cot &
x - (PI * ((k + 1) + 1)) in dom cot &
cot . x = cot . (x + (PI * ((k + 1) + 1))) )
proof
let x be
Real;
( x in dom cot implies ( x + (PI * ((k + 1) + 1)) in dom cot & x - (PI * ((k + 1) + 1)) in dom cot & cot . x = cot . (x + (PI * ((k + 1) + 1))) ) )
assume
x in dom cot
;
( x + (PI * ((k + 1) + 1)) in dom cot & x - (PI * ((k + 1) + 1)) in dom cot & cot . x = cot . (x + (PI * ((k + 1) + 1))) )
then A4:
(
x + (PI * (k + 1)) in dom cot &
x - (PI * (k + 1)) in dom cot &
cot . x = cot . (x + (PI * (k + 1))) )
by A3, Th1;
then
(
x + (PI * (k + 1)) in (dom cos) /\ ((dom sin) \ (sin " {0})) &
x - (PI * (k + 1)) in (dom cos) /\ ((dom sin) \ (sin " {0})) )
by RFUNCT_1:def 1;
then
(
x + (PI * (k + 1)) in dom cos &
x + (PI * (k + 1)) in (dom sin) \ (sin " {0}) &
x - (PI * (k + 1)) in dom cos &
x - (PI * (k + 1)) in (dom sin) \ (sin " {0}) )
by XBOOLE_0:def 4;
then
(
x + (PI * (k + 1)) in dom cos &
x + (PI * (k + 1)) in dom sin & not
x + (PI * (k + 1)) in sin " {0} &
x - (PI * (k + 1)) in dom cos &
x - (PI * (k + 1)) in dom sin & not
x - (PI * (k + 1)) in sin " {0} )
by XBOOLE_0:def 5;
then
( not
sin . (x + (PI * (k + 1))) in {0} & not
sin . (x - (PI * (k + 1))) in {0} )
by FUNCT_1:def 7;
then A5:
(
sin . (x + (PI * (k + 1))) <> 0 &
sin . (x - (PI * (k + 1))) <> 0 )
by TARSKI:def 1;
sin . ((x + (PI * (k + 1))) + PI) = - (sin . (x + (PI * (k + 1))))
by SIN_COS:78;
then
not
sin . ((x + (PI * (k + 1))) + PI) in {0}
by A5, TARSKI:def 1;
then
(
(x + (PI * (k + 1))) + PI in dom cos &
(x + (PI * (k + 1))) + PI in dom sin & not
(x + (PI * (k + 1))) + PI in sin " {0} )
by FUNCT_1:def 7, SIN_COS:24, XREAL_0:def 1;
then
(
(x + (PI * (k + 1))) + PI in dom cos &
(x + (PI * (k + 1))) + PI in (dom sin) \ (sin " {0}) )
by XBOOLE_0:def 5;
then A6:
(x + (PI * (k + 1))) + PI in (dom cos) /\ ((dom sin) \ (sin " {0}))
by XBOOLE_0:def 4;
sin . ((x - (PI * ((k + 1) + 1))) + PI) = - (sin . (x - (PI * ((k + 1) + 1))))
by SIN_COS:78;
then
sin . (x - (PI * ((k + 1) + 1))) = - (sin . (x - (PI * (k + 1))))
;
then
not
sin . (x - (PI * ((k + 1) + 1))) in {0}
by A5, TARSKI:def 1;
then
(
x - (PI * ((k + 1) + 1)) in dom cos &
x - (PI * ((k + 1) + 1)) in dom sin & not
x - (PI * ((k + 1) + 1)) in sin " {0} )
by FUNCT_1:def 7, SIN_COS:24, XREAL_0:def 1;
then
(
x - (PI * ((k + 1) + 1)) in dom cos &
x - (PI * ((k + 1) + 1)) in (dom sin) \ (sin " {0}) )
by XBOOLE_0:def 5;
then A7:
x - (PI * ((k + 1) + 1)) in (dom cos) /\ ((dom sin) \ (sin " {0}))
by XBOOLE_0:def 4;
then
(
x + (PI * ((k + 1) + 1)) in dom cot &
x - (PI * ((k + 1) + 1)) in dom cot )
by A6, RFUNCT_1:def 1;
then cot . (x + (PI * ((k + 1) + 1))) =
(cos . ((x + (PI * (k + 1))) + PI)) / (sin . ((x + (PI * (k + 1))) + PI))
by RFUNCT_1:def 1
.=
(- (cos . (x + (PI * (k + 1))))) / (sin . ((x + (PI * (k + 1))) + PI))
by SIN_COS:78
.=
(- (cos . (x + (PI * (k + 1))))) / (- (sin . (x + (PI * (k + 1)))))
by SIN_COS:78
.=
(cos . (x + (PI * (k + 1)))) / (sin . (x + (PI * (k + 1))))
by XCMPLX_1:191
.=
cot . x
by A4, RFUNCT_1:def 1
;
hence
(
x + (PI * ((k + 1) + 1)) in dom cot &
x - (PI * ((k + 1) + 1)) in dom cot &
cot . x = cot . (x + (PI * ((k + 1) + 1))) )
by A7, A6, RFUNCT_1:def 1;
verum
end;
hence
cot is
PI * ((k + 1) + 1) -periodic
by Th1;
verum
end;
hence
S1[
k + 1]
;
verum
end;
for n being Nat holds S1[n]
from NAT_1:sch 2(A1, A2);
hence
cot is PI * (k + 1) -periodic
; verum