complex1 http://www.openmath.org/cd/complex1.ocd 2003-04-01 2001-03-12 2 0 official quant1 relation1 arith1 nums1 transc1 logic1 set1 setname1 alg1 This CD is intended to be `compatible' with the MathML view of operations on and constructors for complex numbers. complex_cartesian This symbol represents a constructor function for complex numbers specified as the Cartesian coordinates of the relevant point on the complex plane. It takes two arguments, the first is a number x to denote the real part and the second a number y to denote the imaginary part of the complex number x + i y. (Where i is the square root of -1.) for all x,y | complex_cartesian(x,y) = x + iy real This represents the real part of a complex number for all x,y | x = real(x+iy) imaginary This represents the imaginary part of a complex number for all x,y | y = imaginary(x+iy) complex_polar This symbol represents a constructor function for complex numbers specified as the polar coordinates of the relevant point on the complex plane. It takes two arguments, the first is a nonnegative number r to denote the magnitude and the second a number theta (given in radians) to denote the argument of the complex number r e^(i theta). (i and e are defined as in this CD). for all r,a | complex_polar(r,a) = r*e^(a*i) for all x,y,r,a | (r sin a = y and r cos a = x) implies (complex_polar(r,a) = complex_cartesian(x,y) for all x | if a is a real number and k is an integer then complex_polar(x,a) = complex_polar(x,a+2*pi*k) 2 i = complex_polar(1,pi/2) 2 argument This symbol represents the unary function which returns the argument of a complex number, viz. the angle which a straight line drawn from the number to zero makes with the Real line (measured anti-clockwise). The argument to the symbol is the complex number whos argument is being taken. for all r,a | argument(complex_polar(r,a)=a) the argument of x+i*y = tan(y/x) conjugate A unary operator representing the complex conjugate of its argument. if a is a complex number then (conjugate(a) + a) is a real number