:: Basic Properties of Periodic Functions
:: by Bo Li , Yanhong Men , Dailu Li and Xiquan Liang
::
:: Received October 10, 2009
:: Copyright (c) 2009-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, VALUED_0, FUNCT_1, NAT_1, CARD_1, RELAT_1, ARYTM_3,
ARYTM_1, XBOOLE_0, TARSKI, VALUED_1, COMPLEX1, SQUARE_1, SIN_COS,
PARTFUN1, REAL_1, SIN_COS4, FUNCOP_1, XCMPLX_0, FUNCT_9, INT_1, SUBSET_1;
notations TARSKI, XBOOLE_0, SUBSET_1, COMPLEX1, XCMPLX_0, ORDINAL1, NUMBERS,
XREAL_0, REAL_1, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2, FUNCOP_1, SIN_COS,
VALUED_0, VALUED_1, INT_1, SQUARE_1, FDIFF_9;
constructors REAL_1, EUCLID, SQUARE_1, PBOOLE, RFUNCT_1, SIN_COS, FDIFF_9,
RELSET_1, COMPLEX1;
registrations XXREAL_0, MEMBERED, XCMPLX_0, NUMBERS, VALUED_0, RELAT_1,
VALUED_1, NAT_1, SIN_COS6, FUNCOP_1, XREAL_0, INT_1, SIN_COS, ORDINAL1;
requirements NUMERALS, SUBSET, ARITHM;
equalities VALUED_1, SIN_COS, XCMPLX_0, SQUARE_1, FDIFF_9;
theorems COMPLEX1, XBOOLE_0, XCMPLX_1, VALUED_1, XBOOLE_1, SIN_COS, RFUNCT_1,
FUNCT_1, TARSKI, FUNCOP_1, XREAL_0, INT_1, NAT_1;
schemes NAT_1;
begin :: The Basic Properties of period function
reserve x,t,t1,t2,r,a,b for Real;
reserve F,G for real-valued Function;
reserve k for Nat;
reserve i for non zero Integer;
definition
let t be Real;
let F be Function;
attr F is t-periodic means
t <> 0 & for x holds (x in dom F iff x+t in dom F) &
(x in dom F implies F.x = F.(x+t));
end;
definition
let F be Function;
attr F is periodic means :Def2:
ex t st F is t-periodic;
end;
theorem Th1:
F is t-periodic iff t<>0 &
for x st x in dom F holds x+t in dom F & x-t in dom F & F.x=F.(x+t)
proof
thus F is t-periodic implies t<>0 &
for x st x in dom F holds x+t in dom F & x-t in dom F & F.x=F.(x+t)
proof
assume
A1: F is t-periodic;
for x st x in dom F holds x+t in dom F & x-t in dom F & F.x=F.(x+t)
proof
let x;
assume x in dom F;
then x-t+t in dom F;
hence thesis by A1;
end;
hence thesis by A1;
end;
assume
A2:t<>0 &
for x st x in dom F holds (x+t in dom F & x-t in dom F) & F.x=F.(x+t);
for x holds (x in dom F iff x+t in dom F) &
(x in dom F implies F.x = F.(x+t))
proof
let x;
x in dom F iff x+t in dom F
proof
x+t in dom F implies x in dom F
proof
assume x+t in dom F;
then x+t-t in dom F by A2;
hence thesis;
end;
hence thesis by A2;
end;
hence thesis by A2;
end;
hence thesis by A2;
end;
theorem Th2:
F is t-periodic & G is t-periodic implies F+G is t-periodic
proof
assume that
A1: F is t-periodic and
A2: G is t-periodic;
A3: t<>0 & for x st x in dom F holds (x+t in dom F & x-t in dom F)
& F.x=F.(x+t) by A1,Th1;
for x st x in dom (F + G)
holds (x+t in dom (F + G) & x-t in dom (F + G)) & (F + G).x=(F + G).(x+t)
proof
let x;
assume
A4: x in dom (F + G); then
A5: x in dom F /\ dom G by VALUED_1:def 1;
A6: dom F /\ dom G c= dom F & dom F /\ dom G c= dom G by XBOOLE_1:17;
then
A7: x+t in dom F & x-t in dom F by A1,Th1,A5;
x+t in dom G & x-t in dom G by A2,Th1,A5,A6; then
A8: x+t in dom F /\ dom G & x-t in dom F /\ dom G by A7,XBOOLE_0:def 4;
then
A9: x+t in dom (F + G) & x-t in dom (F + G) by VALUED_1:def 1;
(F + G).x=F.x + G.x by A4,VALUED_1:def 1
.=F.(x+t)+G.x by A1,A5,A6
.=F.(x+t)+G.(x+t) by A2,A5,A6
.=(F + G).(x+t) by A9,VALUED_1:def 1;
hence thesis by A8,VALUED_1:def 1;
end;
hence thesis by A3,Th1;
end;
Lm1:
t <> 0 implies REAL --> a is t -periodic
proof
set F = REAL --> a;
assume t <> 0;
hence t <> 0;
let x;
A1: x in REAL & x+t in REAL by XREAL_0:def 1;
hence x in dom F iff x+t in dom F;
assume x in dom F;
thus F.x = a by A1,FUNCOP_1:7
.= F.(x+t) by A1,FUNCOP_1:7;
end;
theorem Th3:
F is t-periodic & G is t-periodic implies F-G is t-periodic
proof
assume that
A1: F is t-periodic and
A2: G is t-periodic;
A3: t<>0 & for x st x in dom F holds (x+t in dom F & x-t in dom F)
& F.x=F.(x+t) by A1,Th1;
for x st x in dom (F - G)
holds (x+t in dom (F - G) & x-t in dom (F - G)) & (F - G).x=(F - G).(x+t)
proof
let x;
assume
A4: x in dom (F - G); then
A5: x in dom F /\ dom G by VALUED_1:12;
A6: dom F /\ dom G c= dom F & dom F /\ dom G c= dom G by XBOOLE_1:17;
then
A7: x+t in dom F & x-t in dom F by A1,A5,Th1;
x+t in dom G & x-t in dom G by A2,Th1,A5,A6; then
A8: x+t in dom F /\ dom G & x-t in dom F /\ dom G by A7,XBOOLE_0:def 4;
then
A9: x+t in dom (F - G) & x-t in dom (F - G) by VALUED_1:12;
(F - G).x=F.x - G.x by A4,VALUED_1:13
.=F.(x+t)-G.x by A1,A5,A6
.=F.(x+t)-G.(x+t) by A2,A5,A6
.=(F - G).(x+t) by A9,VALUED_1:13;
hence thesis by A8,VALUED_1:12;
end;
hence thesis by A3,Th1;
end;
theorem Th4:
F is t-periodic & G is t-periodic implies F(#)G is t-periodic
proof
assume that
A1: F is t-periodic and
A2: G is t-periodic;
A3: t<>0 & for x st x in dom F holds (x+t in dom F & x-t in dom F)
& F.x=F.(x+t) by A1,Th1;
for x st x in dom (F (#) G) holds
(x+t in dom (F (#) G) & x-t in dom (F (#) G)) & (F (#) G).x=(F (#) G).(x+t)
proof
let x;
assume
A4: x in dom (F (#) G); then
A5: x in dom F /\ dom G by VALUED_1:def 4;
A6: dom F /\ dom G c= dom F & dom F /\ dom G c= dom G by XBOOLE_1:17;
then
A7: x+t in dom F & x-t in dom F by A1,Th1,A5;
x+t in dom G & x-t in dom G by A2,Th1,A5,A6; then
A8: x+t in dom F /\ dom G & x-t in dom F /\ dom G by A7,XBOOLE_0:def 4; then
A9: x+t in dom (F (#) G) & x-t in dom (F (#) G) by VALUED_1:def 4;
(F (#) G).x=F.x * G.x by A4,VALUED_1:def 4
.=F.(x+t)*G.x by A1,A5,A6
.=F.(x+t)*G.(x+t) by A2,A5,A6
.=(F (#) G).(x+t) by A9,VALUED_1:def 4;
hence thesis by A8,VALUED_1:def 4;
end;
hence thesis by A3,Th1;
end;
theorem Th5:
F is t-periodic & G is t-periodic implies F /" G is t-periodic
proof
assume that
A1: F is t-periodic and
A2: G is t-periodic;
A3: t<>0 & for x st x in dom F holds (x+t in dom F & x-t in dom F)
& F.x=F.(x+t) by A1,Th1;
for x st x in dom (F /" G) holds (x+t in dom (F /" G) &
x-t in dom (F /" G)) & (F /" G).x=(F /" G).(x+t)
proof
let x;
assume x in dom (F /" G); then
A4: x in dom F /\ dom G by VALUED_1:16;
A5: dom F /\ dom G c= dom F & dom F /\ dom G c= dom G by XBOOLE_1:17;
then
A6: x+t in dom F & x-t in dom F by A1,Th1,A4;
x+t in dom G & x-t in dom G by A2,Th1,A4,A5;
then
A7: x+t in dom F /\ dom G & x-t in dom F /\ dom G by A6,XBOOLE_0:def 4;
(F /" G).x=F.x / G.x by VALUED_1:17
.=F.(x+t) / G.x by A1,A4,A5
.=F.(x+t) / G.(x+t) by A2,A4,A5
.=(F /" G).(x+t) by VALUED_1:17;
hence thesis by A7,VALUED_1:16;
end;
hence thesis by A3,Th1;
end;
theorem Th6:
F is t-periodic implies -F is t-periodic
proof
assume
A1: F is t-periodic;
then
A2: t<>0 & for x st x in dom F holds (x+t in dom F & x-t in dom F)
& F.x=F.(x+t) by Th1;
for x st x in dom -F holds (x+t in dom -F & x-t in dom -F) &
(-F).x=(-F).(x+t)
proof
let x;
assume x in dom (-F); then
A3: x in dom F by VALUED_1:8;
then
A4: x+t in dom F & x-t in dom F by A1,Th1;
(-F).x=-F.x by VALUED_1:8
.=-F.(x+t) by A1,A3
.=(-F).(x+t) by VALUED_1:8;
hence thesis by A4,VALUED_1:8;
end;
hence thesis by A2,Th1;
end;
theorem Th7:
F is t-periodic implies r (#) F is t-periodic
proof
assume
A1: F is t-periodic;
then A2: t<>0 & for x st x in dom F holds (x+t in dom F & x-t in dom F)
& F.x=F.(x+t) by Th1;
for x st x in dom (r (#) F) holds (x+t in dom (r (#) F)
& x-t in dom (r (#) F)) & (r (#) F).x=(r (#) F).(x+t)
proof
let x;
assume
A3: x in dom (r (#) F); then
A4: x in dom F by VALUED_1:def 5; then
A5: x+t in dom F & x-t in dom F by A1,Th1; then
A6: x+t in dom (r (#) F) & x-t in dom (r (#) F) by VALUED_1:def 5;
(r (#) F).x=r * F.x by A3,VALUED_1:def 5
.=r * F.(x+t) by A1,A4
.=(r (#) F).(x+t) by A6,VALUED_1:def 5;
hence thesis by A5,VALUED_1:def 5;
end;
hence thesis by A2,Th1;
end;
theorem Th8:
F is t-periodic implies r+F is t-periodic
proof
assume
A1: F is t-periodic;
then A2: t<>0 & for x st x in dom F holds (x+t in dom F & x-t in dom F)
& F.x=F.(x+t) by Th1;
for x st x in dom (r+F) holds (x+t in dom (r+F) & x-t in dom (r+F)) &
(r+F).x=(r+F).(x+t)
proof
let x;
assume
A3: x in dom (r+F); then
A4: x in dom F by VALUED_1:def 2; then
A5: x+t in dom F & x-t in dom F by A1,Th1; then
A6: x+t in dom (r + F) & x-t in dom (r + F) by VALUED_1:def 2;
(r+F).x=r + F.x by A3,VALUED_1:def 2
.=r + F.(x+t) by A1,A4
.=(r+F).(x+t) by A6,VALUED_1:def 2;
hence thesis by A5,VALUED_1:def 2;
end;
hence thesis by A2,Th1;
end;
theorem
F is t-periodic implies F-r is t-periodic by Th8;
theorem Th10:
F is t-periodic implies |. F .| is t-periodic
proof
assume
A1: F is t-periodic;
then A2: t<>0 & for x st x in dom F holds (x+t in dom F & x-t in dom F)
& F.x=F.(x+t) by Th1;
for x st x in dom |. F .| holds (x+t in dom |. F .| & x-t in dom |. F .|) &
|. F .|.x=|. F .|.(x+t)
proof
let x;
assume
A3: x in dom |. F .|; then
A4: x in dom F by VALUED_1:def 11; then
A5: x+t in dom F & x-t in dom F by A1,Th1; then
A6: x+t in dom |. F .| & x-t in dom |. F .| by VALUED_1:def 11;
|. F .|.x=|. F.x .| by A3,VALUED_1:def 11
.=|. F.(x+t) .| by A1,A4
.=|. F .|.(x+t) by A6,VALUED_1:def 11;
hence thesis by A5,VALUED_1:def 11;
end;
hence thesis by A2,Th1;
end;
theorem Th11:
F is t-periodic implies F" is t-periodic
proof
assume
A1: F is t-periodic;
then A2: t<>0 & for x st x in dom F holds (x+t in dom F & x-t in dom F)
& F.x=F.(x+t) by Th1;
for x st x in dom (F") holds (x+t in dom (F") & x-t in dom (F")) &
(F").x=(F").(x+t)
proof
let x;
assume
A3: x in dom (F"); then
A4: x in dom F by VALUED_1:def 7; then
A5: x+t in dom F & x-t in dom F by A1,Th1;
then
A6: x+t in dom (F") & x-t in dom (F") by VALUED_1:def 7;
F".x=(F.x)" by A3,VALUED_1:def 7
.=(F.(x+t))" by A1,A4
.=F".(x+t) by A6,VALUED_1:def 7;
hence thesis by A5,VALUED_1:def 7;
end;
hence thesis by A2,Th1;
end;
theorem
F is t-periodic implies F^2 is t-periodic by Th4;
theorem Th13:
F is t-periodic implies for x st x in dom F holds F.x=F.(x-t)
proof
assume
A1: F is t-periodic;
let x;
assume x in dom F; then
x+t in dom F & x-t in dom F by A1,Th1;
then F.(x-t)=F.(x-t+t) by A1
.=F.x;
hence thesis;
end;
theorem Th14:
F is t-periodic implies F is -t -periodic
proof
assume
A1: F is t-periodic;
then A2: -t<>0;
for x st x in dom F holds (x+(-t) in dom F & x-(-t) in dom F) & F.x=F.(x+(-t))
proof
let x;
assume
x in dom F; then
x+t in dom F & x-t in dom F by A1,Th1;
hence thesis by A1,Th13;
end;
hence thesis by A2,Th1;
end;
theorem
F is t1-periodic & F is t2-periodic & t1+t2<>0 implies F is (t1+t2)-periodic
proof
assume
A1:F is t1-periodic & F is t2-periodic & t1+t2<>0;
for x st x in dom F holds (x+(t1+t2) in dom F & x-(t1+t2) in dom F)
& F.x=F.(x+(t1+t2))
proof
let x;
assume
A2: x in dom F; then
x+t1 in dom F & x-t1 in dom F by A1,Th1;
then x+t1+t2 in dom F & x-t1-t2 in dom F
& F.(x+t1)=F.((x+t1)+t2) by A1,Th1;
hence thesis by A1,A2;
end;
hence thesis by A1,Th1;
end;
theorem
F is t1-periodic & F is t2-periodic & t1-t2<>0 implies F is (t1-t2)-periodic
proof
assume
A1: F is t1-periodic & F is t2-periodic & t1-t2<>0;
for x st x in dom F holds (x+(t1-t2) in dom F & x-(t1-t2) in dom F)
& F.x=F.(x+(t1-t2))
proof
let x;
assume
A2: x in dom F; then
x+t1 in dom F & x-t1 in dom F by A1,Th1; then
A3: x+t1-t2 in dom F & x-t1+t2 in dom F by A1,Th1;
A4: x-t2 in dom F by A1,Th1,A2;
then F.(x-t2+t1)=F.(x-t2) by A1
.=F.(x-t2+t2) by A1,A4
.=F.x;
hence thesis by A3;
end;
hence thesis by A1,Th1;
end;
theorem
(t<>0 & for x st x in dom F holds (x+t in dom F & x-t in dom F &
F.(x+t)=F.(x-t))) implies F is (2*t)-periodic & F is periodic
proof
assume that
A1: t<>0 and
A2: for x st x in dom F holds (x+t in dom F & x-t in dom F & F.(x+t)=F.(x-t));
for x st x in dom F holds (x+2*t in dom F & x-2*t in dom F) & F.x=F.(x+2*t)
proof
let x;
assume x in dom F; then
A3: x+t in dom F & x-t in dom F by A2; then
A4: x+t+t in dom F & x-t-t in dom F by A2;
F.(x+2*t)=F.(x+t+t) .=F.(x+t-t) by A2,A3
.=F.x;
hence thesis by A4;
end;
then F is (2*t)-periodic by A1,Th1;
hence thesis;
end;
theorem
(t1+t2<>0 & for x st x in dom F holds (x+t1 in dom F & x-t1 in dom F &
x+t2 in dom F & x-t2 in dom F &
F.(x+t1)=F.(x-t2))) implies F is (t1+t2)-periodic & F is periodic
proof
assume that
A1: t1+t2<>0 and
A2: for x st x in dom F holds (x+t1 in dom F & x-t1 in dom F &
x+t2 in dom F & x-t2 in dom F & F.(x+t1)=F.(x-t2));
for x st x in dom F
holds (x+(t1+t2) in dom F & x-(t1+t2) in dom F) & F.x=F.(x+(t1+t2))
proof
let x;
assume x in dom F; then
A3: x+t1 in dom F & x-t1 in dom F & x+t2 in dom F & x-t2 in dom F by A2;
then
A4: x+t1+t2 in dom F & x-t1-t2 in dom F by A2;
F.(x+(t1+t2))=F.(x+t2+t1) .=F.(x+t2-t2) by A2,A3
.=F.x;
hence thesis by A4;
end;
then F is (t1+t2)-periodic by Th1,A1;
hence thesis;
end;
theorem
(t1-t2<>0 & for x st x in dom F holds (x+t1 in dom F & x-t1 in dom F &
x+t2 in dom F & x-t2 in dom F &
F.(x+t1)=F.(x+t2))) implies F is (t1-t2)-periodic & F is periodic
proof
assume that
A1: t1-t2<>0 and
A2: for x st x in dom F holds (x+t1 in dom F & x-t1 in dom F &
x+t2 in dom F & x-t2 in dom F & F.(x+t1)=F.(x+t2));
for x st x in dom F
holds (x+(t1-t2) in dom F & x-(t1-t2) in dom F) & F.x=F.(x+(t1-t2))
proof
let x;
assume x in dom F; then
A3: x+t1 in dom F & x-t1 in dom F & x+t2 in dom F & x-t2 in dom F by A2;
then
A4: x+t1-t2 in dom F & x-t1+t2 in dom F by A2;
F.(x+(t1-t2))=F.(x-t2+t1) .=F.(x-t2+t2) by A2,A3
.=F.x;
hence thesis by A4;
end;
then F is (t1-t2)-periodic by Th1,A1;
hence thesis;
end;
theorem
(t<>0 & for x st x in dom F holds (x+t in dom F & x-t in dom F &
F.(x+t)=(F.x)")) implies F is (2*t)-periodic & F is periodic
proof
assume that
A1: t<>0 and
A2: for x st x in dom F holds (x+t in dom F & x-t in dom F & F.(x+t)=(F.x)");
for x st x in dom F holds (x+2*t in dom F & x-2*t in dom F) & F.x=F.(x+2*t)
proof
let x;
assume
A3:x in dom F; then
A4: x+t in dom F & x-t in dom F by A2; then
A5: x+t+t in dom F & x-t-t in dom F by A2;
F.(x+2*t)=F.(x+t+t) .=(F.(x+t))" by A2,A4
.=((F.x)")" by A2,A3
.=F.x;
hence thesis by A5;
end;
then F is (2*t)-periodic by A1,Th1;
hence thesis;
end;
Lm2: sin is (2 * PI)-periodic
by SIN_COS:24,SIN_COS:78,XREAL_0:def 1;
registration
cluster periodic real-valued for Function;
existence
by Lm2,Def2;
cluster periodic for PartFunc of REAL, REAL;
existence
proof
take sin;
thus thesis by Lm2;
end;
end;
registration
let t be non zero Real;
cluster REAL --> t -> t-periodic;
coherence by Lm1;
cluster t-periodic real-valued for Function;
existence
proof
take REAL --> t;
thus thesis;
end;
end;
registration
let t be non zero Real;
let F,G be t-periodic real-valued Function;
cluster F + G -> t-periodic;
coherence by Th2;
cluster F - G -> t-periodic;
coherence by Th3;
cluster F (#) G -> t-periodic;
coherence by Th4;
cluster F /" G -> t-periodic;
coherence by Th5;
end;
registration let F be periodic real-valued Function;
cluster -F -> periodic;
coherence
proof
consider t such that
A1: F is t-periodic by Def2;
-F is t-periodic by A1,Th6;
hence thesis;
end;
end;
registration let F be periodic real-valued Function;
let r be Real;
cluster r (#) F -> periodic;
coherence
proof
consider t such that
A1: F is t-periodic by Def2;
r (#) F is t-periodic by A1,Th7;
hence thesis;
end;
cluster r+F -> periodic;
coherence
proof
consider t such that
A2: F is t-periodic by Def2;
r+F is t-periodic by A2,Th8;
hence thesis;
end;
cluster F-r -> periodic;
coherence;
end;
registration let F be periodic real-valued Function;
cluster |. F .| -> periodic;
coherence
proof
consider t such that
A1: F is t-periodic by Def2;
|. F .| is t-periodic by A1,Th10;
hence thesis;
end;
cluster F" -> periodic;
coherence
proof
consider t such that
A2: F is t-periodic by Def2;
F" is t-periodic by A2,Th11;
hence thesis;
end;
cluster F^2 -> periodic;
coherence
proof
consider t such that
A3: F is t-periodic by Def2;
F^2 is t-periodic by A3;
hence thesis;
end;
end;
begin :: Some examples
Lm3:cos is 2 * PI -periodic
by SIN_COS:24,SIN_COS:78,XREAL_0:def 1;
registration
cluster sin -> periodic;
coherence by Lm2;
cluster cos -> periodic;
coherence by Lm3;
end;
Lm4:
sin is 2*PI*(k+1) -periodic
proof
defpred X[Nat] means sin is 2*PI*($1+1) -periodic;
A1: X[0] by Lm2;
A2: for k being Nat st X[k] holds X[k+1]
proof
let k be Nat such that
A3: sin is 2*PI*(k+1) -periodic;
sin is 2*PI*(k+1+1) -periodic
proof
for x st x in dom sin holds sin.x=sin.(x+2*PI*(k+1+1))
proof
let x;
assume
A4: x in dom sin;
sin.(x+2*PI*(k+1))=sin.(x+2*PI*(k+1)+2*PI) by SIN_COS:78;
hence thesis by A3,A4;
end;
then 2*PI*(k+1+1)<>0 & for x st x in dom sin holds
(x+2*PI*(k+1+1) in dom sin & x-2*PI*(k+1+1) in dom sin)
& sin.x=sin.(x+2*PI*(k+1+1)) by SIN_COS:24,XREAL_0:def 1;
hence thesis by Th1;
end;
hence thesis;
end;
for n being Nat holds X[n] from NAT_1:sch 2(A1,A2);
hence thesis;
end;
theorem
sin is (2*PI*i)-periodic
proof
i in INT by INT_1:def 2;
then consider k being Nat such that
A1: i = k or i = - k by INT_1:def 1;
per cases by A1;
suppose i = k;
then ex m being Nat st i = m + 1 by NAT_1:6;
hence thesis by Lm4;
end;
suppose
A2: i = -k;
then consider m being Nat such that
A3: -i = m + 1 by NAT_1:6;
sin is 2*PI*(m+1)-periodic by Lm4;
then sin is -2*PI*(m+1)-periodic by Th14;
hence thesis by A2,A3;
end;
end;
Lm5:
cos is 2*PI*(k+1) -periodic
proof
defpred X[Nat] means cos is 2*PI*($1+1) -periodic;
A1: X[0] by Lm3;
A2: for k being Nat st X[k] holds X[k+1]
proof
let k be Nat such that
A3: cos is 2*PI*(k+1) -periodic;
cos is 2*PI*(k+1+1) -periodic
proof
for x st x in dom cos holds cos.x=cos.(x+2*PI*(k+1+1))
proof
let x;
assume
A4: x in dom cos;
cos.(x+2*PI*(k+1))=cos.(x+2*PI*(k+1)+2*PI) by SIN_COS:78;
hence thesis by A3,A4;
end;
then 2*PI*(k+1+1)<>0 & for x st x in dom cos holds
(x+2*PI*(k+1+1) in dom cos & x-2*PI*(k+1+1) in dom cos) &
cos.x=cos.(x+2*PI*(k+1+1)) by SIN_COS:24, XREAL_0:def 1;
hence thesis by Th1;
end;
hence thesis;
end;
for n being Nat holds X[n] from NAT_1:sch 2(A1,A2);
hence thesis;
end;
theorem
cos is (2*PI*i)-periodic
proof
i in INT by INT_1:def 2;
then consider k being Nat such that
A1: i = k or i = - k by INT_1:def 1;
per cases by A1;
suppose i = k;
then ex m being Nat st i = m + 1 by NAT_1:6;
hence thesis by Lm5;
end;
suppose
A2: i = -k;
then consider m being Nat such that
A3: -i = m + 1 by NAT_1:6;
cos is 2*PI*(m+1)-periodic by Lm5;
then cos is -2*PI*(m+1)-periodic by Th14;
hence thesis by A2,A3;
end;
end;
Lm6: cosec is 2 * PI -periodic
proof
for x st x in dom cosec holds (x+2 * PI in dom cosec & x-2 * PI in dom cosec)
& cosec.x=cosec.(x+2 * PI)
proof
let x;
assume
A1: x in dom cosec;
then x in dom sin \ sin"{0} by RFUNCT_1:def 2;
then x in dom sin & not x in sin"{0} by XBOOLE_0:def 5;
then
A2: not sin.x in {0} by FUNCT_1:def 7;
then sin.x<>0 by TARSKI:def 1;
then sin.(x+2 * PI)<>0 by SIN_COS:78;
then not sin.(x+2 * PI) in {0} by TARSKI:def 1;
then x+2 * PI in dom sin & not x+2 * PI in sin"{0}
by FUNCT_1:def 7,SIN_COS:24,XREAL_0:def 1; then
A3: x+2 * PI in dom sin \ sin"{0} by XBOOLE_0:def 5;
x-2*PI in dom sin by SIN_COS:24,XREAL_0:def 1;
then sin.(x-2 * PI)=sin.(x-2 * PI+2 * PI)
by Lm2;
then x-2 * PI in dom sin & not x-2 * PI in sin"{0}
by A2,FUNCT_1:def 7,SIN_COS:24,XREAL_0:def 1; then
A4: x-2 * PI in dom sin \ sin"{0} by XBOOLE_0:def 5; then
x+2 * PI in dom cosec & x-2 * PI in dom cosec by A3,RFUNCT_1:def 2;
then cosec.(x+2 * PI)=(sin.(x+2 * PI))" by RFUNCT_1:def 2
.=(sin.x)" by SIN_COS:78
.=cosec.x by A1,RFUNCT_1:def 2;
hence thesis by A3,A4,RFUNCT_1:def 2;
end;
hence thesis by Th1;
end;
Lm7: sec is 2 * PI -periodic
proof
for x st x in dom sec holds (x+2 * PI in dom sec & x-2 * PI in dom sec)
& sec.x=sec.(x+2 * PI)
proof
let x;
assume
A1: x in dom sec;
then x in dom cos \ cos"{0} by RFUNCT_1:def 2;
then x in dom cos & not x in cos"{0} by XBOOLE_0:def 5;
then
A2: not cos.x in {0} by FUNCT_1:def 7;
then cos.x<>0 by TARSKI:def 1;
then cos.(x+2 * PI)<>0 by SIN_COS:78;
then not cos.(x+2 * PI) in {0} by TARSKI:def 1;
then x+2 * PI in dom cos & not x+2 * PI in cos"{0}
by FUNCT_1:def 7,SIN_COS:24,XREAL_0:def 1; then
A3: x+2 * PI in dom cos \ cos"{0} by XBOOLE_0:def 5;
x-2 * PI in dom cos by SIN_COS:24,XREAL_0:def 1;
then cos.(x-2 * PI)=cos.(x-2 * PI+2 * PI)
by Lm3;
then x-2 * PI in dom cos & not x-2 * PI in cos"{0}
by A2,FUNCT_1:def 7,SIN_COS:24,XREAL_0:def 1; then
A4: x-2 * PI in dom cos \ cos"{0} by XBOOLE_0:def 5; then
x+2 * PI in dom sec & x-2 * PI in dom sec by A3,RFUNCT_1:def 2;
then sec.(x+2 * PI)=(cos.(x+2 * PI))" by RFUNCT_1:def 2
.=(cos.x)" by SIN_COS:78
.=sec.x by A1,RFUNCT_1:def 2;
hence thesis by A3,A4,RFUNCT_1:def 2;
end;
hence thesis by Th1;
end;
registration
cluster cosec -> periodic;
coherence by Lm6;
cluster sec -> periodic;
coherence by Lm7;
end;
Lm8:
sec is 2*PI*(k+1) -periodic
proof
defpred X[Nat] means sec is 2*PI*($1+1) -periodic;
A1: X[0] by Lm7;
A2: for k being Nat st X[k] holds X[k+1]
proof
let k be Nat such that
A3: sec is 2*PI*(k+1) -periodic;
sec is 2*PI*(k+1+1) -periodic
proof
for x st x in dom sec holds
(x+2*PI*(k+1+1) in dom sec & x-2*PI*(k+1+1) in dom sec) &
sec.x=sec.(x+2*PI*(k+1+1))
proof
let x;
assume x in dom sec; then
A4: x+2*PI*(k+1) in dom sec & x-2*PI*(k+1) in dom sec &
sec.x=sec.(x+2*PI*(k+1)) by A3,Th1;
then x+2*PI*(k+1) in dom cos \ cos"{0} & x-2*PI*(k+1) in dom cos \ cos"{0}
by RFUNCT_1:def 2;
then x+2*PI*(k+1) in dom cos & not x+2*PI*(k+1) in cos"{0}
& x-2*PI*(k+1) in dom cos & not x-2*PI*(k+1) in cos"{0} by XBOOLE_0:def 5;
then
A5: not cos.(x+2*PI*(k+1)) in {0} & not cos.(x-2*PI*(k+1)) in {0}
by FUNCT_1:def 7;
then cos.(x+2*PI*(k+1))<>0 by TARSKI:def 1;
then cos.(x+2*PI*(k+1)+2*PI)<>0 by SIN_COS:78;
then not cos.(x+2*PI*(k+1)+2*PI) in {0} by TARSKI:def 1;
then x+2*PI*(k+1)+2*PI in dom cos & not x+2*PI*(k+1)+2*PI in cos"{0}
by FUNCT_1:def 7,SIN_COS:24,XREAL_0:def 1; then
A6: x+2*PI*(k+1+1) in dom cos \ cos"{0} by XBOOLE_0:def 5;
x-2*PI*(k+1+1) in dom cos
by SIN_COS:24,XREAL_0:def 1;
then cos.(x-2*PI*(k+1+1))= cos.(x-2*PI*(k+1+1)+2*PI)
by Lm3;
then x-2*PI*(k+1+1) in dom cos & not x-2*PI*(k+1+1) in cos"{0}
by A5,FUNCT_1:def 7,SIN_COS:24,XREAL_0:def 1; then
A7: x-2*PI*(k+1+1) in dom cos \ cos"{0} by XBOOLE_0:def 5; then
x+2*PI*(k+1+1) in dom sec & x-2*PI*(k+1+1) in dom sec by A6,RFUNCT_1:def 2;
then sec.(x+2*PI*(k+1+1))=(cos.(x+2*PI*(k+1)+2*PI))" by RFUNCT_1:def 2
.=(cos.(x+2*PI*(k+1)))" by SIN_COS:78
.=sec.x by A4,RFUNCT_1:def 2;
hence thesis by A6,A7,RFUNCT_1:def 2;
end;
hence thesis by Th1;
end;
hence thesis;
end;
for n being Nat holds X[n] from NAT_1:sch 2(A1,A2);
hence thesis;
end;
theorem
sec is (2*PI*i)-periodic
proof
i in INT by INT_1:def 2;
then consider k being Nat such that
A1: i = k or i = - k by INT_1:def 1;
per cases by A1;
suppose i = k;
then ex m being Nat st i = m + 1 by NAT_1:6;
hence thesis by Lm8;
end;
suppose
A2: i = -k;
then consider m being Nat such that
A3: -i = m + 1 by NAT_1:6;
sec is 2*PI*(m+1)-periodic by Lm8;
then sec is -2*PI*(m+1)-periodic by Th14;
hence thesis by A2,A3;
end;
end;
Lm9:
cosec is 2*PI*(k+1) -periodic
proof
defpred X[Nat] means cosec is 2*PI*($1+1) -periodic;
A1: X[0] by Lm6;
A2: for k being Nat st X[k] holds X[k+1]
proof
let k be Nat such that
A3: cosec is 2*PI*(k+1) -periodic;
cosec is 2*PI*(k+1+1) -periodic
proof
for x st x in dom cosec holds
(x+2*PI*(k+1+1) in dom cosec & x-2*PI*(k+1+1) in dom cosec) &
cosec.x=cosec.(x+2*PI*(k+1+1))
proof
let x;
assume x in dom cosec; then
A4: x+2*PI*(k+1) in dom cosec & x-2*PI*(k+1) in dom cosec &
cosec.x=cosec.(x+2*PI*(k+1)) by A3,Th1;
then x+2*PI*(k+1) in dom sin \ sin"{0} & x-2*PI*(k+1) in dom sin \ sin"{0}
by RFUNCT_1:def 2;
then x+2*PI*(k+1) in dom sin & not x+2*PI*(k+1) in sin"{0}
& x-2*PI*(k+1) in dom sin & not x-2*PI*(k+1) in sin"{0} by XBOOLE_0:def 5;
then
A5: not sin.(x+2*PI*(k+1)) in {0} & not sin.(x-2*PI*(k+1)) in {0}
by FUNCT_1:def 7;
then sin.(x+2*PI*(k+1))<>0 by TARSKI:def 1;
then sin.(x+2*PI*(k+1)+2*PI)<>0 by SIN_COS:78;
then not sin.(x+2*PI*(k+1)+2*PI) in {0} by TARSKI:def 1;
then x+2*PI*(k+1)+2*PI in dom sin & not x+2*PI*(k+1)+2*PI in sin"{0}
by FUNCT_1:def 7,SIN_COS:24,XREAL_0:def 1; then
A6: x+2*PI*(k+1+1) in dom sin \ sin"{0} by XBOOLE_0:def 5;
x-2*PI*(k+1+1) in dom sin
by SIN_COS:24,XREAL_0:def 1;
then sin.(x-2*PI*(k+1+1))= sin.(x-2*PI*(k+1+1)+2*PI)
by Lm2;
then x-2*PI*(k+1+1) in dom sin & not x-2*PI*(k+1+1) in sin"{0}
by A5,FUNCT_1:def 7,SIN_COS:24,XREAL_0:def 1; then
A7: x-2*PI*(k+1+1) in dom sin \ sin"{0} by XBOOLE_0:def 5; then
x+2*PI*(k+1+1) in dom cosec & x-2*PI*(k+1+1) in dom cosec
by A6,RFUNCT_1:def 2;
then cosec.(x+2*PI*(k+1+1))=(sin.(x+2*PI*(k+1)+2*PI))" by RFUNCT_1:def 2
.=(sin.(x+2*PI*(k+1)))" by SIN_COS:78
.=cosec.x by A4,RFUNCT_1:def 2;
hence thesis by A6,A7,RFUNCT_1:def 2;
end;
hence thesis by Th1;
end;
hence thesis;
end;
for n being Nat holds X[n] from NAT_1:sch 2(A1,A2);
hence thesis;
end;
theorem
cosec is (2*PI*i)-periodic
proof
i in INT by INT_1:def 2;
then consider k being Nat such that
A1: i = k or i = - k by INT_1:def 1;
per cases by A1;
suppose i = k;
then ex m being Nat st i = m + 1 by NAT_1:6;
hence thesis by Lm9;
end;
suppose
A2: i = -k;
then consider m being Nat such that
A3: -i = m + 1 by NAT_1:6;
cosec is 2*PI*(m+1)-periodic by Lm9;
then cosec is -2*PI*(m+1)-periodic by Th14;
hence thesis by A2,A3;
end;
end;
Lm10: tan is PI -periodic
proof
for x st x in dom tan holds (x+PI in dom tan & x-PI in dom tan)
& tan.x=tan.(x+PI)
proof
let x;
assume
A1: x in dom tan;
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 thesis by A4,A5,RFUNCT_1:def 1;
end;
hence thesis by Th1;
end;
Lm11: cot is PI -periodic
proof
for x st x in dom cot holds (x+PI in dom cot & x-PI in dom cot)
& cot.x=cot.(x+PI)
proof
let x;
assume
A1: x in dom cot;
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 thesis by A4,A5,RFUNCT_1:def 1;
end;
hence thesis by Th1;
end;
registration
cluster tan -> periodic;
coherence by Lm10;
cluster cot -> periodic;
coherence by Lm11;
end;
Lm12:
tan is PI*(k+1) -periodic
proof
defpred X[Nat] means tan is PI*($1+1) -periodic;
A1: X[0] by Lm10;
A2: for k being Nat st X[k] holds X[k+1]
proof
let k be Nat such that
A3: tan is PI*(k+1) -periodic;
tan is PI*(k+1+1) -periodic
proof
for x st x in dom tan holds
(x+PI*(k+1+1) in dom tan & x-PI*(k+1+1) in dom tan) &
tan.x=tan.(x+PI*(k+1+1))
proof
let x;
assume x in dom tan; then
A4: x+PI*(k+1) in dom tan & x-PI*(k+1) in dom tan &
tan.x=tan.(x+PI*(k+1)) by A3,Th1;
then x+PI*(k+1) in dom sin /\ (dom cos \ cos"{0})
& x-PI*(k+1) in dom sin /\ (dom cos \ cos"{0}) by RFUNCT_1:def 1;
then x+PI*(k+1) in dom sin & x+PI*(k+1) in dom cos \ cos"{0} &
x-PI*(k+1) in dom sin & x-PI*(k+1) in dom cos \ cos"{0} by XBOOLE_0:def 4;
then x+PI*(k+1) in dom sin & x+PI*(k+1) in dom cos
& not x+PI*(k+1) in cos"{0} & x-PI*(k+1) in dom sin & x-PI*(k+1) in dom cos
& not x-PI*(k+1) in cos"{0} by XBOOLE_0:def 5;
then not cos.(x+PI*(k+1)) in {0} & not cos.(x-PI*(k+1)) in {0}
by FUNCT_1:def 7;
then
A5: cos.(x+PI*(k+1))<>0 & cos.(x-PI*(k+1))<>0 by TARSKI:def 1;
cos.(x+PI*(k+1)+PI)=-cos.(x+PI*(k+1)) by SIN_COS:78;
then not cos.(x+PI*(k+1)+PI) in {0} by A5,TARSKI:def 1;
then x+PI*(k+1)+PI in dom sin & x+PI*(k+1)+PI in dom cos
& not x+PI*(k+1)+PI in cos"{0} by FUNCT_1:def 7,SIN_COS:24,XREAL_0:def 1;
then x+PI*(k+1)+PI in dom sin & x+PI*(k+1)+PI in dom cos \ cos"{0}
by XBOOLE_0:def 5;
then
A6: x+PI*(k+1)+PI in dom sin /\ (dom cos \ cos"{0}) by XBOOLE_0:def 4;
cos.(x-PI*(k+1+1)+PI)=-cos.(x-PI*(k+1+1)) by SIN_COS:78;
then cos.(x-PI*(k+1+1))=-cos.(x-PI*(k+1));
then not cos.(x-PI*(k+1+1)) in {0} by A5,TARSKI:def 1;
then x-PI*(k+1+1) in dom sin & x-PI*(k+1+1) in dom cos &
not x-PI*(k+1+1) in cos"{0} by FUNCT_1:def 7,SIN_COS:24,XREAL_0:def 1;
then x-PI*(k+1+1) in dom sin & x-PI*(k+1+1) in dom cos \ cos"{0}
by XBOOLE_0:def 5; then
A7:x-PI*(k+1+1) in dom sin /\ (dom cos \ cos"{0}) by XBOOLE_0:def 4; then
x+PI*(k+1+1) in dom tan & x-PI*(k+1+1) in dom tan by A6,RFUNCT_1:def 1;
then tan.(x+PI*(k+1+1))
=(sin.(x+PI*(k+1)+PI))/(cos.(x+PI*(k+1)+PI)) by RFUNCT_1:def 1
.=(-sin.(x+PI*(k+1)))/(cos.(x+PI*(k+1)+PI)) by SIN_COS:78
.=(-sin.(x+PI*(k+1)))/(-cos.(x+PI*(k+1))) by SIN_COS:78
.=sin.(x+PI*(k+1))/cos.(x+PI*(k+1)) by XCMPLX_1:191
.=tan.x by A4,RFUNCT_1:def 1;
hence thesis by A7,A6,RFUNCT_1:def 1;
end;
hence thesis by Th1;
end;
hence thesis;
end;
for n being Nat holds X[n] from NAT_1:sch 2(A1,A2);
hence thesis;
end;
theorem
tan is (PI*i)-periodic
proof
i in INT by INT_1:def 2;
then consider k being Nat such that
A1: i = k or i = - k by INT_1:def 1;
per cases by A1;
suppose i = k;
then ex m being Nat st i = m + 1 by NAT_1:6;
hence thesis by Lm12;
end;
suppose
A2: i = -k;
then consider m being Nat such that
A3: -i = m + 1 by NAT_1:6;
tan is PI*(m+1)-periodic by Lm12;
then tan is -PI*(m+1)-periodic by Th14;
hence thesis by A2,A3;
end;
end;
Lm13:
cot is PI*(k+1) -periodic
proof
defpred X[Nat] means cot is PI*($1+1) -periodic;
A1: X[0] by Lm11;
A2: for k being Nat st X[k] holds X[k+1]
proof
let k be Nat such that
A3: cot is PI*(k+1) -periodic;
cot is PI*(k+1+1) -periodic
proof
for x 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;
assume x in dom cot; 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 thesis by A7,A6,RFUNCT_1:def 1;
end;
hence thesis by Th1;
end;
hence thesis;
end;
for n being Nat holds X[n] from NAT_1:sch 2(A1,A2);
hence thesis;
end;
theorem
cot is (PI*i)-periodic
proof
i in INT by INT_1:def 2;
then consider k being Nat such that
A1: i = k or i = - k by INT_1:def 1;
per cases by A1;
suppose i = k;
then ex m being Nat st i = m + 1 by NAT_1:6;
hence thesis by Lm13;
end;
suppose
A2: i = -k;
then consider m being Nat such that
A3: -i = m + 1 by NAT_1:6;
cot is PI*(m+1)-periodic by Lm13;
then cot is -PI*(m+1)-periodic by Th14;
hence thesis by A2,A3;
end;
end;
Lm14: |. sin .| is PI-periodic
proof
for x st x in dom |. sin .| holds (x+PI in dom |. sin .|
& x-PI in dom |. sin .|) & |. sin .|.x=|. sin .|.(x+PI)
proof
let x;
assume
A1: x in dom |. sin .|;
A2: x+PI in dom sin & x-PI in dom sin by SIN_COS:24,XREAL_0:def 1; then
x+PI in dom |. sin .| & x-PI in dom |. sin .| by VALUED_1:def 11;
then |. sin .|.(x+PI)=|. sin(x+PI) .| by VALUED_1:def 11
.=|. -sin.x .| by SIN_COS:78
.=|. sin.x .| by COMPLEX1:52
.=|. sin .|.x by A1,VALUED_1:def 11;
hence thesis by A2,VALUED_1:def 11;
end;
hence thesis by Th1;
end;
Lm15:|. cos .| is PI-periodic
proof
for x st x in dom |. cos .| holds (x+PI in dom |. cos .|
& x-PI in dom |. cos .|) & |. cos .|.x=|. cos .|.(x+PI)
proof
let x; assume
A1: x in dom |. cos .|;
A2: x+PI in dom cos & x-PI in dom cos by SIN_COS:24,XREAL_0:def 1; then
x+PI in dom |. cos .| & x-PI in dom |. cos .| by VALUED_1:def 11;
then |. cos .|.(x+PI)=|. cos(x+PI) .| by VALUED_1:def 11
.=|. -cos.x .| by SIN_COS:78
.=|. cos.x .| by COMPLEX1:52
.=|. cos .|.x by A1,VALUED_1:def 11;
hence thesis by A2,VALUED_1:def 11;
end;
hence thesis by Th1;
end;
Lm16:
|. sin .| is PI*(k+1) -periodic
proof
defpred X[Nat] means |. sin .| is PI*($1+1) -periodic;
A1: X[0] by Lm14;
A2: for k being Nat st X[k] holds X[k+1]
proof
let k be Nat such that
A3: |. sin .| is PI*(k+1) -periodic;
|. sin .| is PI*(k+1+1) -periodic
proof
for x st x in dom |. sin .| holds (x+PI*(k+1+1) in dom |. sin .| &
x-PI*(k+1+1) in dom |. sin .|) & |. sin .|.x=|. sin .|.(x+PI*(k+1+1))
proof
let x;
assume
A4: x in dom |. sin .|; then
A5:x+PI*(k+1) in dom |. sin .| & x-PI*(k+1) in dom |. sin .| by A3,Th1;
A6:x+PI*(k+1+1) in dom sin & x-PI*(k+1+1) in dom sin
by SIN_COS:24,XREAL_0:def 1;
then x+PI*(k+1+1) in dom |. sin .| & x-PI*(k+1+1) in dom |. sin .|
by VALUED_1:def 11;
then |. sin .|.(x+PI*(k+1+1))=|. sin.(x+PI*(k+1)+PI) .| by VALUED_1:def 11
.=|. -sin.(x+PI*(k+1)) .| by SIN_COS:78
.=|. sin.(x+PI*(k+1)) .| by COMPLEX1:52
.=|. sin .|.(x+PI*(k+1)) by A5,VALUED_1:def 11;
hence thesis by A3,A4,A6,VALUED_1:def 11;
end;
hence thesis by Th1;
end;
hence thesis;
end;
for n being Nat holds X[n] from NAT_1:sch 2(A1,A2);
hence thesis;
end;
theorem
|. sin .| is (PI*i)-periodic
proof
i in INT by INT_1:def 2;
then consider k being Nat such that
A1: i = k or i = - k by INT_1:def 1;
per cases by A1;
suppose i = k;
then ex m being Nat st i = m + 1 by NAT_1:6;
hence thesis by Lm16;
end;
suppose
A2: i = -k;
then consider m being Nat such that
A3: -i = m + 1 by NAT_1:6;
|. sin .| is PI*(m+1)-periodic by Lm16;
then |. sin .| is -PI*(m+1)-periodic by Th14;
hence thesis by A2,A3;
end;
end;
Lm17:
|. cos .| is PI*(k+1) -periodic
proof
defpred X[Nat] means |. cos .| is PI*($1+1) -periodic;
A1: X[0] by Lm15;
A2: for k being Nat st X[k] holds X[k+1]
proof
let k be Nat such that
A3: |. cos .| is PI*(k+1) -periodic;
|. cos .| is PI*(k+1+1) -periodic
proof
for x st x in dom |. cos .| holds (x+PI*(k+1+1) in dom |. cos .| &
x-PI*(k+1+1) in dom |. cos .|) & |. cos .|.x=|. cos .|.(x+PI*(k+1+1))
proof
let x;
assume
A4: x in dom |. cos .|; then
A5:x+PI*(k+1) in dom |. cos .| & x-PI*(k+1) in dom |. cos .| by A3,Th1;
A6:x+PI*(k+1+1) in dom cos & x-PI*(k+1+1) in dom cos
by SIN_COS:24,XREAL_0:def 1;
then x+PI*(k+1+1) in dom |. cos .| & x-PI*(k+1+1) in dom |. cos .|
by VALUED_1:def 11;
then |. cos .|.(x+PI*(k+1+1))=|. cos.(x+PI*(k+1)+PI) .| by VALUED_1:def 11
.=|. -cos.(x+PI*(k+1)) .| by SIN_COS:78
.=|. cos.(x+PI*(k+1)) .| by COMPLEX1:52
.=|. cos .|.(x+PI*(k+1)) by A5,VALUED_1:def 11;
hence thesis by A3,A4,A6,VALUED_1:def 11;
end;
hence thesis by Th1;
end;
hence thesis;
end;
for n being Nat holds X[n] from NAT_1:sch 2(A1,A2);
hence thesis;
end;
theorem
|. cos .| is (PI*i)-periodic
proof
i in INT by INT_1:def 2;
then consider k being Nat such that
A1: i = k or i = - k by INT_1:def 1;
per cases by A1;
suppose i = k;
then ex m being Nat st i = m + 1 by NAT_1:6;
hence thesis by Lm17;
end;
suppose
A2: i = -k;
then consider m being Nat such that
A3: -i = m + 1 by NAT_1:6;
|. cos .| is PI*(m+1)-periodic by Lm17;
then |. cos .| is -PI*(m+1)-periodic by Th14;
hence thesis by A2,A3;
end;
end;
Lm18:|. sin .| + |. cos .| is PI/2 -periodic
proof
for x st x in dom(|. sin .| + |. cos .|) holds
(x+PI/2 in dom(|. sin .| + |. cos .|) & x-PI/2 in dom(|. sin .| + |. cos .|))
& (|. sin .| + |. cos .|).x=(|. sin .| + |. cos .|).(x+PI/2)
proof
let x;
assume
A1: x in dom(|. sin .| + |. cos .|);
A2: dom(|. sin .| + |. cos .|)=REAL & dom |. sin .|=REAL & dom |. cos .|=REAL
proof
A3: dom(|. sin .| + |. cos .|)=dom |. sin .| /\ dom |. cos .|
by VALUED_1:def 1;
dom |. sin .|=REAL & dom |. cos .|=REAL by SIN_COS:24,VALUED_1:def 11;
hence thesis by A3;
end;
then
(|. sin .| + |. cos .|).(x+PI/2)=|. sin .|.(x+PI/2)+|. cos .|.(x+PI/2)
by VALUED_1:def 1,XREAL_0:def 1
.=|. sin.(x+PI/2) .|+|. cos .|.(x+PI/2) by A2,VALUED_1:def 11,XREAL_0:def 1
.=|. sin.(x+PI/2) .|+|. cos.(x+PI/2) .| by A2,VALUED_1:def 11,XREAL_0:def 1
.=|. cos.x .|+|. cos.(x+PI/2) .| by SIN_COS:78
.=|. cos.x .|+|. -sin.x .| by SIN_COS:78
.=|. cos.x .|+|. sin.x .| by COMPLEX1:52
.=|. cos .|.x +|. sin.x .| by A1,A2,VALUED_1:def 11
.=|. cos .|.x+|. sin .|.x by A1,A2,VALUED_1:def 11
.=(|. sin .| + |. cos .|).x by A1,VALUED_1:def 1;
hence thesis by A2,XREAL_0:def 1;
end;
hence thesis by Th1;
end;
Lm19:
|. sin .| + |. cos .| is (PI/2)*(k+1) -periodic
proof
defpred X[Nat] means |. sin .| + |. cos .| is (PI/2)*($1+1) -periodic;
A1: X[0] by Lm18;
A2: for k being Nat st X[k] holds X[k+1]
proof
let k be Nat such that
A3: |. sin .| + |. cos .| is (PI/2)*(k+1) -periodic;
A4: dom(|. sin .| + |. cos .|)=REAL & dom |. sin .|=REAL & dom |. cos .|=REAL
proof
A5: dom(|. sin .| + |. cos .|)=dom |. sin .| /\ dom |. cos .|
by VALUED_1:def 1;
dom |. sin .|=REAL & dom |. cos .|=REAL by SIN_COS:24,VALUED_1:def 11;
hence thesis by A5;
end;
|. sin .| + |. cos .| is (PI/2)*(k+1+1) -periodic
proof
for x st x in dom (|. sin .| + |. cos .|) holds (x+(PI/2)*(k+1+1) in
dom (|. sin .| + |. cos .|) & x-(PI/2)*(k+1+1) in dom (|. sin .| + |. cos .|))
& (|. sin .| + |. cos .|).x=(|. sin .| + |. cos .|).(x+(PI/2)*(k+1+1))
proof
let x;
assume
x in dom (|. sin .| + |. cos .|);
(|. sin .| + |. cos .|).(x+(PI/2)*(k+1+1))
=|. sin .|.(x+(PI/2)*(k+1+1))+|. cos .|.(x+(PI/2)*(k+1+1))
by A4,VALUED_1:def 1,XREAL_0:def 1
.=|. sin.(x+(PI/2)*(k+1+1)) .|+|. cos .|.(x+(PI/2)*(k+1+1))
by A4,VALUED_1:def 11,XREAL_0:def 1
.=|. sin.(x+(PI/2)*(k+1)+PI/2) .|+|. cos.(x+(PI/2)*(k+1)+PI/2) .|
by A4,VALUED_1:def 11,XREAL_0:def 1
.=|. cos.(x+(PI/2)*(k+1)) .|+|. cos.(x+(PI/2)*(k+1)+PI/2) .|
by SIN_COS:78
.=|. cos.(x+(PI/2)*(k+1)) .|+|. -sin.(x+(PI/2)*(k+1)) .| by SIN_COS:78
.=|. cos.(x+(PI/2)*(k+1)) .|+|. sin.(x+(PI/2)*(k+1)) .| by COMPLEX1:52
.=|. cos .|.(x+(PI/2)*(k+1)) +|. sin.(x+(PI/2)*(k+1)) .|
by A4,VALUED_1:def 11,XREAL_0:def 1
.=|. cos .|.(x+(PI/2)*(k+1))+|. sin .|.(x+(PI/2)*(k+1))
by A4,VALUED_1:def 11,XREAL_0:def 1
.=(|. sin .| + |. cos .|).(x+(PI/2)*(k+1)) by A4,VALUED_1:def 1,XREAL_0:def 1;
hence thesis by A3,A4,XREAL_0:def 1;
end;
hence thesis by Th1;
end;
hence thesis;
end;
for n being Nat holds X[n] from NAT_1:sch 2(A1,A2);
hence thesis;
end;
theorem
|. sin .| + |. cos .| is (PI/2*i)-periodic
proof
i in INT by INT_1:def 2;
then consider k being Nat such that
A1: i = k or i = - k by INT_1:def 1;
per cases by A1;
suppose i = k;
then ex m being Nat st i = m + 1 by NAT_1:6;
hence thesis by Lm19;
end;
suppose
A2: i = -k;
then consider m being Nat such that
A3: -i = m + 1 by NAT_1:6;
|. sin .| + |. cos .| is PI/2*(m+1)-periodic by Lm19;
then |. sin .| + |. cos .| is -PI/2*(m+1)-periodic by Th14;
hence thesis by A2,A3;
end;
end;
Lm20: sin^2 is PI-periodic
proof
for x st x in dom(sin^2) holds (x+PI in dom(sin^2)
& x-PI in dom(sin^2)) & (sin^2).x=(sin^2).(x+PI)
proof
let x;
assume x in dom(sin^2);
A1: x+PI in dom sin & x-PI in dom sin by SIN_COS:24,XREAL_0:def 1;
(sin^2).(x+PI)=(sin(x+PI))^2 by VALUED_1:11
.=(-sin.x)^2 by SIN_COS:78
.=(sin.x)^2
.=(sin^2).x by VALUED_1:11;
hence thesis by A1,VALUED_1:11;
end;
hence thesis by Th1;
end;
Lm21:cos^2 is PI-periodic
proof
for x st x in dom(cos^2) holds (x+PI in dom(cos^2)
& x-PI in dom(cos^2)) & (cos^2).x=(cos^2).(x+PI)
proof
let x;
assume x in dom(cos^2);
A1: x+PI in dom cos & x-PI in dom cos by SIN_COS:24,XREAL_0:def 1;
(cos^2).(x+PI)=(cos(x+PI))^2 by VALUED_1:11
.=(-cos.x)^2 by SIN_COS:78
.=(cos.x)^2
.=(cos^2).x by VALUED_1:11;
hence thesis by A1,VALUED_1:11;
end;
hence thesis by Th1;
end;
Lm22:
sin^2 is PI*(k+1) -periodic
proof
defpred X[Nat] means sin^2 is PI*($1+1) -periodic;
A1: X[0] by Lm20;
A2: for k being Nat st X[k] holds X[k+1]
proof
let k be Nat such that
A3: sin^2 is PI*(k+1) -periodic;
sin^2 is PI*(k+1+1) -periodic
proof
for x st x in dom(sin^2) holds (x+PI*(k+1+1) in dom(sin^2) &
x-PI*(k+1+1) in dom(sin^2)) & (sin^2).x=(sin^2).(x+PI*(k+1+1))
proof
let x;
assume
A4: x in dom(sin^2);
A5:x+PI*(k+1+1) in dom sin & x-PI*(k+1+1) in dom sin
by SIN_COS:24,XREAL_0:def 1;
(sin^2).(x+PI*(k+1+1))=(sin.(x+PI*(k+1)+PI))^2 by VALUED_1:11
.=(-sin.(x+PI*(k+1)))^2by SIN_COS:78
.=(sin.(x+PI*(k+1)))^2
.=(sin^2).(x+PI*(k+1)) by VALUED_1:11;
hence thesis by A3,A4,A5,VALUED_1:11;
end;
hence thesis by Th1;
end;
hence thesis;
end;
for n being Nat holds X[n] from NAT_1:sch 2(A1,A2);
hence thesis;
end;
theorem
sin^2 is (PI*i)-periodic
proof
i in INT by INT_1:def 2;
then consider k being Nat such that
A1: i = k or i = - k by INT_1:def 1;
per cases by A1;
suppose i = k;
then ex m being Nat st i = m + 1 by NAT_1:6;
hence thesis by Lm22;
end;
suppose
A2: i = -k;
then consider m being Nat such that
A3: -i = m + 1 by NAT_1:6;
sin^2 is PI*(m+1)-periodic by Lm22;
then sin^2 is -PI*(m+1)-periodic by Th14;
hence thesis by A2,A3;
end;
end;
Lm23:
cos^2 is PI*(k+1) -periodic
proof
defpred X[Nat] means cos^2 is PI*($1+1) -periodic;
A1: X[0] by Lm21;
A2: for k being Nat st X[k] holds X[k+1]
proof
let k be Nat such that
A3: cos^2 is PI*(k+1) -periodic;
cos^2 is PI*(k+1+1) -periodic
proof
for x st x in dom(cos^2) holds (x+PI*(k+1+1) in dom(cos^2) &
x-PI*(k+1+1) in dom(cos^2)) & (cos^2).x=(cos^2).(x+PI*(k+1+1))
proof
let x;
assume
A4: x in dom(cos^2);
A5:x+PI*(k+1+1) in dom cos & x-PI*(k+1+1) in dom cos
by SIN_COS:24,XREAL_0:def 1;
(cos^2).(x+PI*(k+1+1))=(cos.(x+PI*(k+1)+PI))^2 by VALUED_1:11
.=(-cos.(x+PI*(k+1)))^2 by SIN_COS:78
.=(cos.(x+PI*(k+1)))^2
.=(cos^2).(x+PI*(k+1)) by VALUED_1:11;
hence thesis by A3,A4,A5,VALUED_1:11;
end;
hence thesis by Th1;
end;
hence thesis;
end;
for n being Nat holds X[n] from NAT_1:sch 2(A1,A2);
hence thesis;
end;
theorem
cos^2 is (PI*i)-periodic
proof
i in INT by INT_1:def 2;
then consider k being Nat such that
A1: i = k or i = - k by INT_1:def 1;
per cases by A1;
suppose i = k;
then ex m being Nat st i = m + 1 by NAT_1:6;
hence thesis by Lm23;
end;
suppose
A2: i = -k;
then consider m being Nat such that
A3: -i = m + 1 by NAT_1:6;
cos^2 is PI*(m+1)-periodic by Lm23;
then cos^2 is -PI*(m+1)-periodic by Th14;
hence thesis by A2,A3;
end;
end;
Lm24:sin (#) cos is PI-periodic
proof
for x st x in dom(sin (#) cos) holds (x+PI in dom(sin (#) cos)
& x-PI in dom(sin (#) cos)) & (sin (#) cos).x=(sin (#) cos).(x+PI)
proof
let x;
assume
A1: x in dom(sin (#) cos);
A2: x+PI in dom sin /\ dom cos & x-PI in dom sin /\ dom cos
by SIN_COS:24,XREAL_0:def 1; then
x+PI in dom(sin (#) cos) & x-PI in dom(sin (#) cos) by VALUED_1:def 4;
then (sin (#) cos).(x+PI)=sin.(x+PI) * cos.(x+PI) by VALUED_1:def 4
.=(-sin.x) * cos.(x+PI) by SIN_COS:78
.=(-sin.x) * (-cos.x) by SIN_COS:78
.=sin.x * cos.x
.=(sin (#) cos).x by A1,VALUED_1:def 4;
hence thesis by A2,VALUED_1:def 4;
end;
hence thesis by Th1;
end;
Lm25:
sin (#) cos is PI*(k+1) -periodic
proof
defpred X[Nat] means sin (#) cos is PI*($1+1) -periodic;
A1: X[0] by Lm24;
A2: for k being Nat st X[k] holds X[k+1]
proof
let k be Nat such that
A3: sin (#) cos is PI*(k+1) -periodic;
sin (#) cos is PI*(k+1+1) -periodic
proof
for x st x in dom(sin (#) cos) holds (x+PI*(k+1+1) in dom(sin (#) cos)
& x-PI*(k+1+1) in dom(sin (#) cos)) &
(sin (#) cos).x=(sin (#) cos).(x+PI*(k+1+1))
proof
let x;
assume
A4: x in dom(sin (#) cos); then
A5:x+PI*(k+1) in dom(sin (#) cos) & x-PI*(k+1) in dom(sin (#) cos) by A3,Th1;
A6:x+PI*(k+1+1) in dom cos /\ dom sin &
x-PI*(k+1+1) in dom cos /\ dom sin by SIN_COS:24,XREAL_0:def 1;
then x+PI*(k+1+1) in dom(sin (#) cos) &
x-PI*(k+1+1) in dom(sin (#) cos) by VALUED_1:def 4;
then (sin (#) cos).(x+PI*(k+1+1))
=(sin.(x+PI*(k+1)+PI)) * (cos.(x+PI*(k+1)+PI)) by VALUED_1:def 4
.=(-sin.(x+PI*(k+1))) * (cos.(x+PI*(k+1)+PI)) by SIN_COS:78
.=(-sin.(x+PI*(k+1))) * (-cos.(x+PI*(k+1))) by SIN_COS:78
.=(sin.(x+PI*(k+1))) * (cos.(x+PI*(k+1)))
.=(sin (#) cos).(x+PI*(k+1)) by A5,VALUED_1:def 4;
hence thesis by A3,A4,A6,VALUED_1:def 4;
end;
hence thesis by Th1;
end;
hence thesis;
end;
for n being Nat holds X[n] from NAT_1:sch 2(A1,A2);
hence thesis;
end;
theorem
sin (#) cos is (PI*i)-periodic
proof
i in INT by INT_1:def 2;
then consider k being Nat such that
A1: i = k or i = - k by INT_1:def 1;
per cases by A1;
suppose i = k;
then ex m being Nat st i = m + 1 by NAT_1:6;
hence thesis by Lm25;
end;
suppose
A2: i = -k;
then consider m being Nat such that
A3: -i = m + 1 by NAT_1:6;
sin(#)cos is PI*(m+1)-periodic by Lm25;
then sin(#)cos is -PI*(m+1)-periodic by Th14;
hence thesis by A2,A3;
end;
end;
Lm26: b + a (#) sin is 2*PI-periodic
proof
for x st x in dom(b + a (#) sin) holds (x+2*PI in dom(b + a (#) sin)
& x-2*PI in dom(b + a (#) sin)) & (b + a (#) sin).x=(b + a (#) sin).(x+2*PI)
proof
let x;
assume x in dom(b + a (#) sin);
x in REAL by XREAL_0:def 1;
then
A1: x in dom(a (#) sin) by SIN_COS:24,VALUED_1:def 5; then
A2: x in dom(b + a (#) sin) & x in dom(b + a (#) sin) by VALUED_1:def 2;
x+2*PI in dom sin & x-2*PI in dom sin by SIN_COS:24,XREAL_0:def 1; then
A3: x+2*PI in dom(a (#) sin) & x-2*PI in dom(a (#) sin) by VALUED_1:def 5;
then
x+2*PI in dom(b + a (#) sin) & x-2*PI in dom(b + a (#) sin)
by VALUED_1:def 2;
then
(b + a (#) sin).(x+2*PI) =b + (a (#) sin).(x+2*PI) by VALUED_1:def 2
.=b + a * sin.(x+2*PI) by A3,VALUED_1:def 5
.=b + a * sin.x by SIN_COS:78
.=b + (a (#) sin).x by A1,VALUED_1:def 5
.=(b + a (#) sin).x by A2,VALUED_1:def 2;
hence thesis by A3,VALUED_1:def 2;
end;
hence thesis by Th1;
end;
Lm27:b + a (#) cos is 2*PI -periodic
proof
for x st x in dom(b + a (#) cos) holds (x+2*PI in dom(b + a (#) cos)
& x-2*PI in dom(b + a (#) cos)) & (b + a (#) cos).x=(b + a (#) cos).(x+2*PI)
proof
let x;
assume x in dom(b + a (#) cos);
x in REAL by XREAL_0:def 1;
then
A1: x in dom(a (#) cos) by SIN_COS:24,VALUED_1:def 5; then
A2: x in dom(b + a (#) cos) & x in dom(b + a (#) cos) by VALUED_1:def 2;
x+2*PI in dom cos & x-2*PI in dom cos by SIN_COS:24,XREAL_0:def 1; then
A3: x+2*PI in dom(a (#) cos) & x-2*PI in dom(a (#) cos) by VALUED_1:def 5;
then
x+2*PI in dom(b + a (#) cos) & x-2*PI in dom(b + a (#) cos)
by VALUED_1:def 2;
then
(b + a (#) cos).(x+2*PI) =b + (a (#) cos).(x+2*PI) by VALUED_1:def 2
.=b + a * cos.(x+2*PI) by A3,VALUED_1:def 5
.=b + a * cos.x by SIN_COS:78
.=b + (a (#) cos).x by A1,VALUED_1:def 5
.=(b + a (#) cos).x by A2,VALUED_1:def 2;
hence thesis by A3,VALUED_1:def 2;
end;
hence thesis by Th1;
end;
Lm28:
b + a (#) sin is 2*PI*(k+1) -periodic
proof
defpred X[Nat] means b + a (#) sin is 2*PI*($1+1) -periodic;
A1: X[0] by Lm26;
A2: for k being Nat st X[k] holds X[k+1]
proof
let k be Nat such that
A3: b + a (#) sin is 2*PI*(k+1) -periodic;
b + a (#) sin is 2*PI*(k+1+1) -periodic
proof
for x st x in dom(b + a (#) sin) holds (x+2*PI*(k+1+1) in dom(b + a (#) sin) &
x-2*PI*(k+1+1) in dom(b + a (#) sin)) &
(b + a (#) sin).x=(b + a (#) sin).(x+2*PI*(k+1+1))
proof
let x;
assume x in dom(b + a (#) sin);
x in REAL by XREAL_0:def 1;
then x in dom(a (#) sin) by SIN_COS:24,VALUED_1:def 5; then
A4: x in dom(b + a (#) sin) by VALUED_1:def 2;
x+2*PI*(k+1+1) in dom sin & x-2*PI*(k+1+1) in dom sin &
x+2*PI*(k+1) in dom sin & x-2*PI*(k+1) in dom sin
by SIN_COS:24,XREAL_0:def 1; then
A5: x+2*PI*(k+1+1) in dom(a (#) sin) & x-2*PI*(k+1+1) in dom(a (#) sin) &
x+2*PI*(k+1) in dom(a (#) sin) & x-2*PI*(k+1) in dom(a (#) sin)
by VALUED_1:def 5; then
A6: x+2*PI*(k+1+1) in dom(b + a (#) sin)
& x-2*PI*(k+1+1) in dom(b + a (#) sin) & x+2*PI*(k+1) in dom(b + a (#) sin)
& x-2*PI*(k+1) in dom(b + a (#) sin) by VALUED_1:def 2;
then (b + a (#) sin).(x+2*PI*(k+1+1))
=b + (a (#) sin).(x+2*PI*(k+1+1)) by VALUED_1:def 2
.=b + a * sin.(x+2*PI*(k+1)+2*PI) by A5,VALUED_1:def 5
.=b + a * sin.(x+2*PI*(k+1)) by SIN_COS:78
.=b + (a (#) sin).(x+2*PI*(k+1)) by A5,VALUED_1:def 5
.=(b + a (#) sin).(x+2*PI*(k+1)) by A6,VALUED_1:def 2;
hence thesis by A3,A5,A4,VALUED_1:def 2;
end;
hence thesis by Th1;
end;
hence thesis;
end;
for n being Nat holds X[n] from NAT_1:sch 2(A1,A2);
hence thesis;
end;
theorem Th33:
b + a (#) sin is (2*PI*i)-periodic
proof
i in INT by INT_1:def 2;
then consider k being Nat such that
A1: i = k or i = - k by INT_1:def 1;
per cases by A1;
suppose i = k;
then ex m being Nat st i = m + 1 by NAT_1:6;
hence thesis by Lm28;
end;
suppose
A2: i = -k;
then consider m being Nat such that
A3: -i = m + 1 by NAT_1:6;
b+a(#)sin is 2*PI*(m+1)-periodic by Lm28;
then b+a(#)sin is -2*PI*(m+1)-periodic by Th14;
hence thesis by A2,A3;
end;
end;
theorem
a (#) sin - b is (2*PI*i)-periodic by Th33;
Lm29:
b + a (#) cos is 2*PI*(k+1) -periodic
proof
defpred X[Nat] means b + a (#) cos is 2*PI*($1+1) -periodic;
A1: X[0] by Lm27;
A2: for k being Nat st X[k] holds X[k+1]
proof
let k be Nat such that
A3: b + a (#) cos is 2*PI*(k+1) -periodic;
b + a (#) cos is 2*PI*(k+1+1) -periodic
proof
for x st x in dom(b + a (#) cos) holds (x+2*PI*(k+1+1) in dom(b + a (#) cos) &
x-2*PI*(k+1+1) in dom(b + a (#) cos)) &
(b + a (#) cos).x=(b + a (#) cos).(x+2*PI*(k+1+1))
proof
let x;
assume x in dom(b + a (#) cos);
x in REAL by XREAL_0:def 1;
then x in dom(a (#) cos) by SIN_COS:24,VALUED_1:def 5;then
A4: x in dom(b + a (#) cos) by VALUED_1:def 2;
x+2*PI*(k+1+1) in dom cos & x-2*PI*(k+1+1) in dom cos &
x+2*PI*(k+1) in dom cos & x-2*PI*(k+1) in dom cos
by SIN_COS:24,XREAL_0:def 1; then
A5: x+2*PI*(k+1+1) in dom(a (#) cos) & x-2*PI*(k+1+1) in dom(a (#) cos) &
x+2*PI*(k+1) in dom(a (#) cos) & x-2*PI*(k+1) in dom(a (#) cos)
by VALUED_1:def 5; then
A6: x+2*PI*(k+1+1) in dom(b + a (#) cos)
& x-2*PI*(k+1+1) in dom(b + a (#) cos) & x+2*PI*(k+1) in dom(b + a (#) cos)
& x-2*PI*(k+1) in dom(b + a (#) cos) by VALUED_1:def 2;
then (b + a (#) cos).(x+2*PI*(k+1+1))
=b + (a (#) cos).(x+2*PI*(k+1+1)) by VALUED_1:def 2
.=b + a * cos.(x+2*PI*(k+1)+2*PI) by A5,VALUED_1:def 5
.=b + a * cos.(x+2*PI*(k+1)) by SIN_COS:78
.=b + (a (#) cos).(x+2*PI*(k+1)) by A5,VALUED_1:def 5
.=(b + a (#) cos).(x+2*PI*(k+1)) by A6,VALUED_1:def 2;
hence thesis by A3,A5,A4,VALUED_1:def 2;
end;
hence thesis by Th1;
end;
hence thesis;
end;
for n being Nat holds X[n] from NAT_1:sch 2(A1,A2);
hence thesis;
end;
theorem Th35:
b + a (#) cos is (2*PI*i)-periodic
proof
i in INT by INT_1:def 2;
then consider k being Nat such that
A1: i = k or i = - k by INT_1:def 1;
per cases by A1;
suppose i = k;
then ex m being Nat st i = m + 1 by NAT_1:6;
hence thesis by Lm29;
end;
suppose
A2: i = -k;
then consider m being Nat such that
A3: -i = m + 1 by NAT_1:6;
b+a(#)cos is 2*PI*(m+1)-periodic by Lm29;
then b+a(#)cos is -2*PI*(m+1)-periodic by Th14;
hence thesis by A2,A3;
end;
end;
theorem
a (#) cos - b is (2*PI*i)-periodic by Th35;
theorem
t <> 0 implies REAL --> a is t -periodic by Lm1;
registration
let a;
cluster REAL --> a -> periodic;
coherence
proof
take 1;
thus thesis by Lm1;
end;
end;
registration
let t be non zero Real;
cluster t-periodic for Function of REAL,REAL;
existence
proof
take REAL --> the Element of REAL;
thus thesis by Lm1;
end;
end;