Interface:Complex numbers

From Wikiproofs
Jump to: navigation, search
Module usage
Parameters
Classical propositional calculus, first-order logic, set theory
Imported by
none yet
Exported by
none yet

This file contains the basic operations on complex numbers: addition, subtraction, square roots, and so on. It also contains a variety of convenience theorems and notations; for a minimal set of theorems/axioms sufficient to define the complex numbers see instead Interface:Complex number axioms.

We build on propositional logic, first-order logic, and set theory.

param (CLASSICAL Interface:Classical_propositional_calculus () ())
param (FIRSTORDER Interface:First-order_logic_with_quantifiability (CLASSICAL) ())
param (SETS Interface:Set_theory (CLASSICAL FIRSTORDER) ())

Complex numbers[edit]

There is a set of complex numbers. As a convention, we tend to use z and w to refer to complex numbers, although using these names does not by itself ensure that a term is a complex number rather than a set of numbers or a relation or something else.

term (object ())
var (object z w s)

The complex numbers are closed under an addition operation, which is commutative and associative.

term (object (+ object object))
stmt (ComplexAdditionClosure () () (((z  ())  (w  ()))  ((z + w)  ())))
stmt (AdditionCommutativity () () (((z  ())  (w  ()))  ((z + w) = (w + z))))
stmt (AdditionAssociativity () () ((((z  ())  (w  ()))  (s  ()))  (((z + w) + s) = (z + (w + s)))))

The complex numbers are closed under a multiplication operation, which is commutative and associative.

term (object (· object object))
stmt (ComplexMultiplicationClosure () () (((z  ())  (w  ()))  ((z · w)  ())))
stmt (MultiplicationCommutativity () () (((z  ())  (w  ()))  ((z · w) = (w · z))))
stmt (MultiplicationAssociativity () () ((((z  ())  (w  ()))  (s  ()))  (((z · w) · s) = (z · (w · s)))))

Multiplication distributes over addition.

stmt (Distributivity () () ((((z  ())  (w  ()))  (s  ()))  ((z · (w + s)) = ((z · w) + (z · s)))))

There is a complex number 1, which serves as a multiplicative identity.

term (object (1))
stmt (MultiplicativeIdentity () () ((z  ())  ((z · (1)) = z)))

There is a complex number 0, not equal to 1, which serves as an additive identity.

term (object (0))
stmt (AdditiveIdentity () () ((z  ())  ((z + (0)) = z)))
stmt (ZeroOne () () ((0)  (1)))

There is a complex number i for the square root of negative one.

term (object (i))
stmt (IComplex () () ((i)  ()))
stmt (ISquared () () ((((i) · (i)) + (1)) = (0)))

Real numbers[edit]

There is a subset of the complex numbers called the real numbers which are closed under addition and multiplication. We conventionally use a, b, and c to refer to real number terms, and x and y for real variables.

term (object ())
var (object a b c)
var (variable x y)
stmt (RealComplex () () (()  ()))
stmt (RealAdditionClosure () () (((a  ())  (b  ()))  ((a + b)  ())))
stmt (RealMultiplicationClosure () () (((a  ())  (b  ()))  ((a · b)  ())))

Any complex number can be written as real and imaginary parts.

stmt (ComplexParts ((x y z)) () ((z  ())  ( x (((value x)  ())  ( y (((value y)  ())  (z = ((value x) + ((i) · (value y))))))))))

Numerical constants[edit]

There is not (yet at least) any particularly convenient way of expressing integers short of defining each one, so here are some of the more commonly used ones.

def ((2) ((1) + (1)))
def ((3) ((2) + (1)))
def ((4) ((3) + (1)))
def ((5) ((4) + (1)))
def ((6) ((5) + (1)))
def ((7) ((6) + (1)))
def ((8) ((7) + (1)))
def ((9) ((8) + (1)))
def ((10) ((9) + (1)))
def ((11) ((10) + (1)))
def ((12) ((11) + (1)))
def ((30) ((3) · (10)))
def ((45) (((4) · (10)) + (5)))
def ((60) ((6) · (10)))
def ((90) ((9) · (10)))
def ((100) ((10) · (10)))
def ((180) ((100) + ((8) · (10))))
def ((360) (((3) · (100)) + (60)))
def ((1000) ((100) · (10)))
def ((1000000) ((1000) · (1000)))

stmt (ZeroReal () () ((0)  ()))
stmt (OneReal () () ((1)  ()))
stmt (TwoReal () () ((2)  ()))
stmt (ThreeReal () () ((3)  ()))
stmt (FourReal () () ((4)  ()))
stmt (FiveReal () () ((5)  ()))
stmt (SixReal () () ((6)  ()))
stmt (SevenReal () () ((7)  ()))
stmt (EightReal () () ((8)  ()))
stmt (NineReal () () ((9)  ()))
stmt (TenReal () () ((10)  ()))
stmt (ElevenReal () () ((11)  ()))
stmt (TwelveReal () () ((12)  ()))
stmt (ThirtyReal () () ((30)  ()))
stmt (FortyFiveReal () () ((45)  ()))
stmt (SixtyReal () () ((60)  ()))
stmt (NinetyReal () () ((90)  ()))
stmt (HundredReal () () ((100)  ()))
stmt (HundredEightyReal () () ((180)  ()))
stmt (ThreeHundredSixtyReal () () ((360)  ()))
stmt (ThousandReal () () ((1000)  ()))
stmt (MillionReal () () ((1000000)  ()))

Additive inverse and subtraction[edit]

Any complex number has an additive inverse, and for a real number the inverse is real. Our notation is - a for the additive inverse of a.

term (object (- object))

stmt (RealAdditiveInverseClosed () () ((z  ())  ((- z)  ())))
stmt (RealAdditiveInverseExists ((x a)) () ((a  ()) 
  ( x (((value x)  ())  ((a + (value x)) = (0))))))

stmt (ComplexAdditiveInverseClosed () () ((z  ())  ((- z)  ())))
stmt (ComplexAdditiveInverse () () ((z  ())  ((z + (- z)) = (0))))

We can subtract any complex (real?) number from another. In case your screen doesn't show it clearly, the minus sign is a different character (longer) than the negation sign above.

term (object ( object object))
stmt (SubtractionClosed () () (((z  ())  (w  ()))  ((z  w)  ())))
stmt (Subtraction () () (((z  ())  (w  ()))  ((z  w) = (z + (- w)))))

Subtracting a number from itself yields zero.[1]

stmt (SubtractionItself () () ((z  ())  ((z  z) = (0))))

The difference between two numbers is zero if and only if they are equal.[2]

stmt (ZeroDifferenceEquality () () (((z  ())  (w  ()))  (((z  w) = (0))  (z = w))))

Properties of negation[edit]

Negation distributes across multiplication in the familiar ways.[3]

stmt (MultiplicationNegativeNegative () () (((z  ())  (w  ()))  (((- z) · (- w)) = (z · w))))

Negating a subtraction is the same as reversing the operands to the subtraction.[4]

stmt (NegativeSubtraction () () (((z  ())  (w  ()))  ((- (z  w)) = (w  z))))

Multiplicative inverse and division[edit]

Every nonzero complex number has a multiplicative inverse.[5]

term (object (/ object object))
stmt (ReciprocalClosed () () (((z  ())  (z  (0)))  (((1) / z)  ())))
stmt (Reciprocal () () (((z  ())  (z  (0)))  ((z · ((1) / z)) = (1))))

The reciprocal of a real number is real. We state this two ways, once with 1 / a and once with .

stmt (RealReciprocalClosed () () (((a  ())  (a  (0)))  (((1) / a)  ())))
stmt (RealReciprocalExists ((x a)) ()
  (((a  ())  (a  (0))) 
    ( x (((value x)  ())  ((a · (value x)) = (1))))))

We can divide any complex number by any nonzero complex number.[6]

stmt (DivisionClosed () () ((((z  ())  (w  ()))  (w  (0))) 
  ((z / w)  ())))
stmt (Division () () ((((z  ())  (w  ()))  (w  (0))) 
  ((z / w) = (z · ((1) / w)))))

Order on the reals[edit]

We define a total order on the reals, which is consistent with addition and multiplication.

term (formula (< object object))
stmt (Trichotomy () () (((a  ())  (b  ()))  ((a < b)  (¬ ((a = b)  (b < a))))))
stmt (Transitivity () () ((((a  ())  (b  ()))  (c  ()))  (((a < b)  (b < c))  (a < c))))
stmt (LessThanAddition () () ((((a  ())  (b  ()))  (c  ()))  ((a < b)  ((c + a) < (c + b)))))
stmt (LessThanMultiplication () () (((a  ())  (b  ()))  ((((0) < a)  ((0) < b))  ((0) < (a · b)))))

def ((> a b) (b < a))
def (( a b) ((a < b)  (a = b)))
def (( a b) (b  a))

Any nonempty set of real numbers which is bounded above has a least upper bound (supremum) which is a real number. This property distinguishes the reals from the rationals. It is this property which causes us to build the reals on top of set theory, instead of just first-order logic, as it involves sets of reals not just individual real numbers. The statement of the axiom is as in metamath (modulo variable renamings and notation changes); the occurence of bound in the second part might better be read as "would-be upper bound" as of course the point is that it can't be less than the supremum and still be an upper bound.[7]

var (object A)
var (variable bound supremum)
stmt (Supremum ((x bound supremum A)) ()
  ((((A  ())
     (A  ()))
     ( bound (((value bound)  ())  
      ( x (((value x)  A)  ((value x) < (value bound)))))))
  
    ( supremum (((value supremum)  ())  (
      ( x (((value x)  A)  (¬ ((value supremum) < (value x)))))  
      ( bound (((value bound)  ())  (((value bound) < (value supremum)) 
        ( x (((value x)  A)  ((value bound) < (value x))))))))))))

Squares and square root[edit]

At least for now, we notate the square of z as z · z. We have not yet developed exponentiation, which might treat z squared as a special case of z to an integer power.

Squares[edit]

The square of a real number is nonnegative.[8]

stmt (RealSquareNonnegative () () ((a  ())  ((0)  (a · a))))

Square root[edit]

We can take the square root of any complex number. The square root of a nonnegative real is real.

term (object ( object))
stmt (SquareRootComplex () () ((z  ())  (( z)  ())))
stmt (SquareRootReal () () (((a  ())  (a  (0)))  (( a)  ())))
stmt (SquareRoot () () ((z  ())  ((( z) · ( z)) = z)))

Builders[edit]

Here we supply builders for each operation.

Although the builders are not interesting unless A0 and so on are complex numbers, we state them without restricting them to complex numbers. However we define the sum of two sets which are not complex numbers, it is no hardship to make that definition obey the builders.

var (object B A0 A1 B0 B1)
stmt (AdditionBuilder () () (((A0 = A1)  (B0 = B1))  ((A0 + B0) = (A1 + B1))))
stmt (SubtractionBuilder () () (((A0 = A1)  (B0 = B1))  ((A0  B0) = (A1  B1))))
stmt (NegativeBuilder () () ((A0 = A1)  ((- A0) = (- A1))))
stmt (MultiplicationBuilder () () (((A0 = A1)  (B0 = B1))  ((A0 · B0) = (A1 · B1))))
stmt (DivisionBuilder () () (((A0 = A1)  (B0 = B1))  ((A0 / B0) = (A1 / B1))))
stmt (SquareRootBuilder () () ((A0 = A1)  (( A0) = ( A1))))

Convenience builders[edit]

The following builders, of course, follow from the ones above.

stmt (buildAddition () ((A0 = A1) (B0 = B1)) ((A0 + B0) = (A1 + B1)))
stmt (buildAdditionLL () ((B0 = B1)) ((A + B0) = (A + B1)))
stmt (buildAdditionRR () ((A0 = A1)) ((A0 + B) = (A1 + B)))
stmt (buildMultiplicationLL () ((B0 = B1)) ((A · B0) = (A · B1)))
stmt (buildMultiplicationRR () ((A0 = A1)) ((A0 · B) = (A1 · B)))

Zeichen 123 - Baustelle, StVO 1992.svg This interface contains statements which are not yet proved, but could be. You can help wikiproofs by creating a proof module which will eventually export this interface. A good starting point would be Interface:Complex number axioms. See Help:Contents if you haven't yet figured out how to edit and write proofs, or ask at WP:TEA if you have any questions.


References[edit]

  1. subid, metamath's set.mm, accessed 2011
  2. subeq0, metamath's set.mm, accessed 2011
  3. mul2neg, metamath's set.mm, accessed 2011
  4. negsubdi2, metamath's set.mm, accessed 2011
  5. reccl, metamath's set.mm, accessed June 9, 2011
  6. divcl, metamath's set.mm, accessed June 9, 2011
  7. axsup
  8. msqge0, metamath's set.mm, accessed April 16, 2012

Interface module parsed successfully