Journal of Formalized Mathematics
Volume 10, 1998
University of Bialystok
Copyright (c) 1998 Association of Mizar Users

## 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

The terminology and notation used in this paper have been introduced in the following articles [23] [26] [3] [24] [7] [8] [4] [19] [5] [11] [9] [20] [27] [18] [16] [2] [13] [6] [25] [17] [10] [21] [15] [12] [1] [14] [22]

#### 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.