In [1]:

```
import proveit
# Prepare this notebook for defining the axioms of a theory:
%axioms_notebook # Keep this at the top following 'import proveit'.
from proveit import a, b
from proveit.logic import Forall, Equals, InSet
from proveit.numbers import one, i, Real, Complex, Add, subtract, Neg, Mult, Conjugate
```

In [2]:

```
%begin axioms
```

The imaginary number is defined as a number that squares to -1.

In [3]:

```
imaginary_number_def = Equals(Mult(i, i), Neg(one))
```

In [4]:

```
complex_numbers_def = Forall((a, b), InSet(Add(a, Mult(i, b)), Complex), domain=Real)
```

In [5]:

```
conjugate_def = Forall((a, b), Equals(Conjugate(Add(a, Mult(i, b))),
subtract(a, Mult(i, b))))
```

In [6]:

```
%end axioms
```