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 () () Unable to load parameter CLASSICAL(Interface:Classical_propositional_calculus)[]+: Unable to load module Interface:Classical_propositional_calculus

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.

Unknown command

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

Unknown command

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

Unknown command

Multiplication distributes over addition.

Unknown command

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

Unknown command

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

Unknown command

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

Unknown command

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.

Unknown command

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

Unknown command

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.

Unknown command

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.

Unknown command

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.

Unknown command

Subtracting a number from itself yields zero.[1]

Unknown command

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

Unknown command

Properties of negation[edit]

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

Unknown command

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

Unknown command

Multiplicative inverse and division[edit]

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

Unknown command

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

Unknown command

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

Unknown command

Order on the reals[edit]

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

Unknown command

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]

Unknown command

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]

Unknown command

Square root[edit]

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

Unknown command

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.

Unknown command

Convenience builders[edit]

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

Unknown command

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