Are properties of the imaginary unit assumed or proved?

It does indeed have a proof. But this involves going back to exactly how the complex numbers are defined in the first place.

Let's say for the moment that we're happy with the real numbers and their properties. (Of course, there's a separate question - "how do we construct the reals?" - but let's leave that aside for now.) There are now a number of ways to rigorously define the complex numbers. Here's probably the simplest (although not the most useful): we let $\mathbb{C}$ be the set of ordered pairs $(a, b)$ where $a, b\in\mathbb{R}$, and we define the operations $+$ and $\times$ on $\mathbb{C}$ as follows (intuitively, the pair $(a, b)$ represents the number $a+bi$):

• $(a, b)+(c, d)=(a+b, c+d)$.

• $(a, b)\times (c, d)=(a\times c-b\times d, a\times d+b\times c)$.

Note that on the right hand side of each of those expressions, I'm using the notion of $+$ and $\times$ (and $-$) for real numbers. Arguably, a better way to write this would be

• $(a, b)+_\mathbb{C}(c, d)=(a+_\mathbb{R}b, c+_\mathbb{R}d)$.

• $(a, b)\times_\mathbb{C} (c, d)=(a\times_\mathbb{R} c-_\mathbb{R}b\times_\mathbb{R} d, a\times_\mathbb{R} d+_\mathbb{R}b\times_\mathbb{R} c)$.

That is, I've already defined operations $+_\mathbb{R}, \times_\mathbb{R}, -_\mathbb{R}$ for the reals, and now I'm defining new operations $+_\mathbb{C}, \times_\mathbb{C}$ for the complex numbers. In general, it will always be clear from context which is meant; but it's a good habit when learning this material to get into to clarify things with subscripts whenever we're using both types of operation.

We can use this explicit definition to verify basic claims about complex numbers. For example,

• Check that $(0, 1)\times(0, 1)=(-1, 0)$, and that $(0, 1)$ and $(0, -1)$ are the only complex numbers with this property. We call the former "$i$" (but it doesn't really matter which one we pick).

• Now, we can compute $(0, 1)^3=(0, 1)\times (0, 1)\times (0, 1)=(0, -1)$. This shows that indeed $i^3=-i$.

What about more general claims? For example, I implicitly used the associativity of $\times$ above, in writing out $(0, 1)^3$. We can also use the definition of $\mathbb{C}$ to prove that $\times$ is associative, and more generally that $\mathbb{C}$ is a field). This gets a bit messy; let me give as an example the proof that addition of complex numbers is commutative, which is simpler:

$$(a, b)+_\mathbb{C}(c, d)=(a+_\mathbb{R}c, b+_\mathbb{R}d)=(c+_\mathbb{R}a, d+_\mathbb{R}b)=(c, d)+_\mathbb{C}(a, b).$$

Note how we use (at the second "$=$" sign) the commutativity of $+_\mathbb{R}$; we're building on facts we already know about the reals, to prove facts about the complex numbers, and this is justified because of how the complex numbers are constructed from the reals.

EDIT: Just to tie up a loose end, what did I mean above when I said that this was "not the most useful" way to construct the complex numbers?

Well, it turns out that there is a much more abstract approach we can use, that - while much harder at first - ultimately turns out to be much more mathematically useful. The key point is to notice that essentially the whole point of the complex numbers is to solve a single equation, $x^2=-1$. In some sense, they are what you get when you start with the reals and "fill in" the hole left by that equation.

This suggests that we should look for some tool for doing the following: if $\mathbb{S}$ is some number system (reals, complexes, integers, rationals, quaternions, hyperbolic sedenions, or thing-I-just-made-upions) and $E$ is some equation in $\mathbb{S}$, there should be a way to build a thing like $\mathbb{S}$ but that can also solve $E$. This is really really vague, but ultimately leads to a bunch of ideas in abstract algebra; for example, algebraic extensions of fields. In this context, there's a precise sense in which the complex numbers are the "smallest" number system containing the reals where $x^2=-1$ has a solution, and the relevant notation is $\mathbb{R}[x]/\langle x^2+1\rangle$ - which is probably gibberish right now but down the road you'll see how to view this as a "recipe" for building the complex numbers from the real numbers.

Although those are excellent answers I think the answer is even simpler.

$b^{m}b^{n} = b^{m+n}$ is not a "real number rule" but an "associative binary operation rule".

If we define/construct/invent any set of elements (these could be gumdrops or chess pieces for all we care) and create any operation between to elements ($a*b$ could be "melt the two gumdrops together an make a new one" or "always pick the second chess piece; always") so that:

--$a * b$ for any two elements of the set will result in $c$, also a member of the set and the same $a,b$ combined will always results in the same member $c$ (The term for this is $*$ is a "binary operation".

--If we evaluate $a*b*c*d$ it doesn't matter how we group them. $(a*(b*c))*d$ (where we first do $b*c= e$ and then we do $a*e = f$ and then we do $f*d = g$) will give the same result as $(a*b)*(c*d)$ (where we do $a*b$ and get $h$ and then we do $c*d$ and get $i$ and then we do $h*i$ and get, amazingly, $g$). Or more simply $(a*b)*c = a*(b*c)$. (such an operation is called "associative". An example of something that isn't associative is $(2^3)^2 \ne 2^{(3^2)}$.)

Then if we define as a matter of notation (it's just notation) that if $n\in \mathbb N$ than $a^n := a*a*a*....*a$ where a is operated $n$ times.

If we create such a system, (whether gumdrops, chess pieces, or numbers), then we will always have:

$b^mb^n = (b*.....*b)*(b*.....*b) = (b*....................*b) = b^{m+n}$.

Always.

So this is true for complex numbers. (Assuming we defined what $c*d$ means and that $c*(d*e) = (c*d)*e$).

===

Just to be perverse, let's do this with chess pieces. And define $a*b = b$. Then $(knight*pawn)*bishop = pawn*bishop = bishop$ which is equal to $knight*(pawn*bishop) = knight*bishop = bishop$.

Then $pawn^2*pawn = (pawn*pawn)*pawn=pawn*pawn= pawn; pawn*pawn^2 = pawn*(pawn*pawn) = pawn*pawn = pawn; pawn^3 = pawn*pawn*pawn = pawn*pawn = pawn$.

So $pawn^2pawn=pawn*pawn^2 = pawn^3$.

That was kind of boring.

=====

To go to Noah Schweber's excellent answer. If $i = (0,1)$ and $(a,b)*(c,d)= (ac - bd, ad + bc)$ is the definition of complex numbers then:

-- yes, it is binary. ($(a,b)*(c,d)= (ac - bd, ad + bc)$ results in a real value pair.)

-- yes it is associative. ($(a,b)*[(c,d)*(e,f)] = (a,b)*(ce-df,cf+de)=(a(ce-df)-b(cf+de), b(ce-df) + a(cf+de))=(ace-adf-bcf-bde,bce-bdf+acf+ade)$ while ($[(a,b)*(c,d)]*(e,f) = (ac - bd,bc+ad)*(e,f)=((ac-bd)e-(bc+ad)f,(bc+ad)e + f(bc+ad))=(ace-adf-bcf-bde,bce-bdf+acf+ade)$ so $(a,b)*[(c,d)*(e,f)] = [(a,b)*(c,d)]*(e,f)$.

Then

$(a,b)^3 = (a,b)(a,b)(a,b)=(a^2 - b^2,2ab)(a,b) = (a^3 - 3ab^2,3a^b-b^3)$

$(a,b)^2(a,b) = [(a,b)(a,b)](a,b)=(a^2 - b^2,2ab)(a,b) = (a^3 - 3ab^2,3a^b-b^3)$

$(a,b)(a,b)^2 = (a,b)(a^2 - b^2,2ab)=(a^3 - 3ab^2,3a^b-b^3)$

all equal.

Are properties of the imaginary unit assumed or proved?

Both. The intuitive approach of assuming a solution to a previously unsolvable equation (such as an $i$ solving $i^2= -1$) that satisfies other algebraic properties of the number system, came into use in the 1400-1700's and was later proved to create a consistent number system that works as expected (such as any element of the system with $i$ being uniquely expressible as $x+yi$).

Today the sequence is similar: it is assumed to work in high school, and proved to work at university.