Trigonometric Functions and Existence of Circle Ratio

Yuguang Yang

Shinshu University, Nagano

Yasunari Shidama

Shinshu University, Nagano

Summary.

In this article, we defined {\em sinus} and {\em cosine} as the real part and the imaginary part of the exponential function on complex, and also give their series expression. Then we proved the differentiablity of {\em sinus}, {\em cosine} and the exponential function of real. Finally, we showed the existence of the circle ratio, and some formulas of {\em sinus}, {\em cosine}.

MML Identifier: SIN_COS

Contents (PDF format)

1. Some Definitions and Properties of Complex Sequence
2. Definition of Exponential Function on Complex
3. Definition of Sinus, Cosine, and Exponential Function on ${\Bbb R}$
4. Differential of Sinus, Cosine, and Exponential Function
5. Existence of Circle Ratio
6. Formulas of Sinus, Cosine

Bibliography

[1] Agnieszka Banachowicz and Anna Winnicka. Complex sequences. Journal of Formalized Mathematics, 5, 1993.

[2] Grzegorz Bancerek. The fundamental properties of natural numbers. Journal of Formalized Mathematics, 1, 1989.

[3] Grzegorz Bancerek. The ordinal numbers. Journal of Formalized Mathematics, 1, 1989.

[4] Czeslaw Bylinski. Functions and their basic properties. Journal of Formalized Mathematics, 1, 1989.

[5] Czeslaw Bylinski. Functions from a set to a set. Journal of Formalized Mathematics, 1, 1989.

[6] Czeslaw Bylinski. The complex numbers. Journal of Formalized Mathematics, 2, 1990.

[7] Library Committee. Introduction to arithmetic. Journal of Formalized Mathematics, Addenda, 2003.

[8] Krzysztof Hryniewiecki. Basic properties of real numbers. Journal of Formalized Mathematics, 1, 1989.

[9] Jaroslaw Kotowicz. Convergent sequences and the limit of sequences. Journal of Formalized Mathematics, 1, 1989.

[10] Jaroslaw Kotowicz. Monotone real sequences. Subsequences. Journal of Formalized Mathematics, 1, 1989.

[11] Jaroslaw Kotowicz. Real sequences and basic operations on them. Journal of Formalized Mathematics, 1, 1989.

[12] Jaroslaw Kotowicz. Partial functions from a domain to the set of real numbers. Journal of Formalized Mathematics, 2, 1990.

[13] Rafal Kwiatek. Factorial and Newton coefficients. Journal of Formalized Mathematics, 2, 1990.

[14] Adam Naumowicz. Conjugate sequences, bounded complex sequences and convergent complex sequences. Journal of Formalized Mathematics, 8, 1996.

[15] Takaya Nishiyama and Yasuho Mizuhara. Binary arithmetics. Journal of Formalized Mathematics, 5, 1993.

[16] Jan Popiolek. Some properties of functions modul and signum. Journal of Formalized Mathematics, 1, 1989.

[17] Konrad Raczkowski. Integer and rational exponents. Journal of Formalized Mathematics, 2, 1990.

[18] Konrad Raczkowski and Andrzej Nedzusiak. Series. Journal of Formalized Mathematics, 3, 1991.

[19] Konrad Raczkowski and Pawel Sadowski. Real function continuity. Journal of Formalized Mathematics, 2, 1990.

[20] Konrad Raczkowski and Pawel Sadowski. Real function differentiability. Journal of Formalized Mathematics, 2, 1990.

[21] Konrad Raczkowski and Pawel Sadowski. Topological properties of subsets in real numbers. Journal of Formalized Mathematics, 2, 1990.

[22] Yasunari Shidama and Artur Kornilowicz. Convergence and the limit of complex sequences. Series. Journal of Formalized Mathematics, 9, 1997.

[23] Andrzej Trybulec. Tarski Grothendieck set theory. Journal of Formalized Mathematics, Axiomatics, 1989.

[24] Andrzej Trybulec. Subsets of real numbers. Journal of Formalized Mathematics, Addenda, 2003.

[25] Andrzej Trybulec and Czeslaw Bylinski. Some properties of real numbers operations: min, max, square, and square root. Journal of Formalized Mathematics, 1, 1989.

[26] Zinaida Trybulec. Properties of subsets. Journal of Formalized Mathematics, 1, 1989.

[27] Edmund Woronowicz. Relations and their basic properties. Journal of Formalized Mathematics, 1, 1989.