Journal of Formalized Mathematics
Volume 12, 2000
University of Bialystok
Copyright (c) 2000 Association of Mizar Users

Trigonometric Form of Complex Numbers


Robert Milewski
University of Bialystok

MML Identifier: COMPTRIG

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

Contents (PDF format)

  1. Preliminaries
  2. Sinus and Cosinus Properties
  3. Argument of Complex Number

Bibliography

[1] Grzegorz Bancerek. The ordinal numbers. Journal of Formalized Mathematics, 1, 1989.
[2] Czeslaw Bylinski. Binary operations. Journal of Formalized Mathematics, 1, 1989.
[3] Czeslaw Bylinski. Functions and their basic properties. Journal of Formalized Mathematics, 1, 1989.
[4] Czeslaw Bylinski. Partial functions. Journal of Formalized Mathematics, 1, 1989.
[5] Czeslaw Bylinski. The complex numbers. Journal of Formalized Mathematics, 2, 1990.
[6] Krzysztof Hryniewiecki. Basic properties of real numbers. Journal of Formalized Mathematics, 1, 1989.
[7] Jaroslaw Kotowicz. Real sequences and basic operations on them. Journal of Formalized Mathematics, 1, 1989.
[8] Jaroslaw Kotowicz. Properties of real functions. Journal of Formalized Mathematics, 2, 1990.
[9] Eugeniusz Kusak, Wojciech Leonczuk, and Michal Muzalewski. Abelian groups, fields and vector spaces. Journal of Formalized Mathematics, 1, 1989.
[10] Anna Justyna Milewska. The field of complex numbers. Journal of Formalized Mathematics, 12, 2000.
[11] Anna Justyna Milewska. The Hahn Banach theorem in the vector space over the field of complex numbers. Journal of Formalized Mathematics, 12, 2000.
[12] Jan Popiolek. Some properties of functions modul and signum. Journal of Formalized Mathematics, 1, 1989.
[13] Konrad Raczkowski and Andrzej Nedzusiak. Real exponents and logarithms. Journal of Formalized Mathematics, 2, 1990.
[14] Konrad Raczkowski and Pawel Sadowski. Real function continuity. Journal of Formalized Mathematics, 2, 1990.
[15] Konrad Raczkowski and Pawel Sadowski. Topological properties of subsets in real numbers. Journal of Formalized Mathematics, 2, 1990.
[16] Andrzej Trybulec. Tarski Grothendieck set theory. Journal of Formalized Mathematics, Axiomatics, 1989.
[17] Andrzej Trybulec. Subsets of real numbers. Journal of Formalized Mathematics, Addenda, 2003.
[18] Andrzej Trybulec and Czeslaw Bylinski. Some properties of real numbers operations: min, max, square, and square root. Journal of Formalized Mathematics, 1, 1989.
[19] Wojciech A. Trybulec. Vectors in real linear space. Journal of Formalized Mathematics, 1, 1989.
[20] Wojciech A. Trybulec. Groups. Journal of Formalized Mathematics, 2, 1990.
[21] Zinaida Trybulec. Properties of subsets. Journal of Formalized Mathematics, 1, 1989.
[22] Edmund Woronowicz. Relations and their basic properties. Journal of Formalized Mathematics, 1, 1989.
[23] Yuguang Yang and Yasunari Shidama. Trigonometric functions and existence of circle ratio. Journal of Formalized Mathematics, 10, 1998.

Received July 21, 2000

[ Download a postscript version, MML identifier index, Mizar home page]