environ
vocabularies HIDDEN, 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 HIDDEN, 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;
definitions ;
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;
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, CARD_1;
constructors HIDDEN, REAL_1, EUCLID, SQUARE_1, PBOOLE, RFUNCT_1, SIN_COS, FDIFF_9, RELSET_1, COMPLEX1;
requirements HIDDEN, NUMERALS, SUBSET, ARITHM, BOOLE;
equalities VALUED_1, SIN_COS, XCMPLX_0, SQUARE_1, FDIFF_9;
expansions ;
Lm1:
for t, a being Real st t <> 0 holds
REAL --> a is t -periodic
Lm2:
sin is 2 * PI -periodic
by SIN_COS:24, SIN_COS:78, XREAL_0:def 1;
Lm3:
cos is 2 * PI -periodic
by SIN_COS:24, SIN_COS:78, XREAL_0:def 1;
Lm4:
for k being Nat holds sin is (2 * PI) * (k + 1) -periodic
Lm5:
for k being Nat holds cos is (2 * PI) * (k + 1) -periodic
Lm6:
cosec is 2 * PI -periodic
Lm7:
sec is 2 * PI -periodic
Lm8:
for k being Nat holds sec is (2 * PI) * (k + 1) -periodic
Lm9:
for k being Nat holds cosec is (2 * PI) * (k + 1) -periodic
Lm10:
tan is PI -periodic
Lm11:
cot is PI -periodic
Lm12:
for k being Nat holds tan is PI * (k + 1) -periodic
Lm13:
for k being Nat holds cot is PI * (k + 1) -periodic
Lm14:
|.sin.| is PI -periodic
Lm15:
|.cos.| is PI -periodic
Lm16:
for k being Nat holds |.sin.| is PI * (k + 1) -periodic
Lm17:
for k being Nat holds |.cos.| is PI * (k + 1) -periodic
Lm18:
|.sin.| + |.cos.| is PI / 2 -periodic
Lm19:
for k being Nat holds |.sin.| + |.cos.| is (PI / 2) * (k + 1) -periodic
Lm20:
sin ^2 is PI -periodic
Lm21:
cos ^2 is PI -periodic
Lm22:
for k being Nat holds sin ^2 is PI * (k + 1) -periodic
Lm23:
for k being Nat holds cos ^2 is PI * (k + 1) -periodic
Lm24:
sin (#) cos is PI -periodic
Lm25:
for k being Nat holds sin (#) cos is PI * (k + 1) -periodic
Lm26:
for a, b being Real holds b + (a (#) sin) is 2 * PI -periodic
Lm27:
for a, b being Real holds b + (a (#) cos) is 2 * PI -periodic
Lm28:
for a, b being Real
for k being Nat holds b + (a (#) sin) is (2 * PI) * (k + 1) -periodic
Lm29:
for a, b being Real
for k being Nat holds b + (a (#) cos) is (2 * PI) * (k + 1) -periodic