begin
:: deftheorem Def1 defines -periodic FUNCT_9:def 1 :
for t being real number
for F being Function holds
( F is t -periodic iff ( t <> 0 & ( for x being real number holds
( ( x in dom F implies x + t in dom F ) & ( x + t in dom F implies x in dom F ) & ( x in dom F implies F . x = F . (x + t) ) ) ) ) );
:: deftheorem Def2 defines periodic FUNCT_9:def 2 :
for F being Function holds
( F is periodic iff ex t being real number st F is t -periodic );
theorem Th1:
theorem Ta1:
Lm38:
for t, a being real number st t <> 0 holds
REAL --> a is t -periodic
theorem Ta2:
theorem Trazy:
theorem Ta4:
theorem Th6:
theorem Th7:
theorem Th8:
theorem
theorem Th10:
theorem Th11:
theorem
theorem Th13:
theorem Th14:
theorem
theorem
theorem
theorem
theorem
theorem
Lm1:
sin is 2 * PI -periodic
begin
Lm2:
cos is 2 * PI -periodic
Lmsin:
for k being Nat holds sin is (2 * PI) * (k + 1) -periodic
theorem
Lmcos:
for k being Nat holds cos is (2 * PI) * (k + 1) -periodic
theorem
Lm3:
cosec is 2 * PI -periodic
Lm4:
sec is 2 * PI -periodic
Lmsec:
for k being Nat holds sec is (2 * PI) * (k + 1) -periodic
theorem
Lmcosec:
for k being Nat holds cosec is (2 * PI) * (k + 1) -periodic
theorem
Lm5:
tan is PI -periodic
Lm6:
cot is PI -periodic
Lmtan:
for k being Nat holds tan is PI * (k + 1) -periodic
theorem
Lmcot:
for k being Nat holds cot is PI * (k + 1) -periodic
theorem
Lm7:
|.sin.| is PI -periodic
Lm8:
|.cos.| is PI -periodic
Lmsinm:
for k being Nat holds |.sin.| is PI * (k + 1) -periodic
theorem
Lmcosm:
for k being Nat holds |.cos.| is PI * (k + 1) -periodic
theorem
Lm9:
|.sin.| + |.cos.| is PI / 2 -periodic
Lmsincosm:
for k being Nat holds |.sin.| + |.cos.| is (PI / 2) * (k + 1) -periodic
theorem
Lm10:
sin ^2 is PI -periodic
Lm11:
cos ^2 is PI -periodic
Lmsin2:
for k being Nat holds sin ^2 is PI * (k + 1) -periodic
theorem
Lmcos2:
for k being Nat holds cos ^2 is PI * (k + 1) -periodic
theorem
Lm12:
sin (#) cos is PI -periodic
Lmsincos:
for k being Nat holds sin (#) cos is PI * (k + 1) -periodic
theorem
theorem
canceled;
Lm13:
for b, a being real number holds b + (a (#) sin) is 2 * PI -periodic
Lm14:
for b, a being real number holds b + (a (#) cos) is 2 * PI -periodic
Th34:
for b, a being real number
for k being Nat holds b + (a (#) sin) is (2 * PI) * (k + 1) -periodic
theorem Th35:
theorem
Th36:
for b, a being real number
for k being Nat holds b + (a (#) cos) is (2 * PI) * (k + 1) -periodic
theorem Th37:
theorem
theorem