Theorem: Real Part of Integer Power of Complex Number is Harmonic

Let $z \in \C$ be a complex number.
Let $n \in \Z_{>0}$ be a (strictly) positive integer.
Let $z^n$ denote $z$ raised to the $n$th power.
Then the real part $\map \Re {z^n}$ of $z^n$ is a harmonic polynomial.

Proof:
Let $z = x + i y$.
Then:
{{begin-eqn}}
{{eqn | l = z^n
      | r = \paren {\sum_{\substack {0 \mathop \le j \mathop \le n \\ \text {$j$ even} } } \paren {-1}^{j / 2} \dbinom n j x^{n - j} y^j} + i \paren {\sum_{\substack {0 \mathop \le j \mathop \le n \\ \text {$j$ odd} } } \paren {-1}^{\paren {j - 1} / 2} \dbinom n j x^{n - j} y^j}
      | c = Arbitrary Power of Complex Number
}}
{{eqn | ll= \leadsto
      | l = \map \Re {z^n}
      | r = \sum_{\substack {0 \mathop \le j \mathop \le n \\ \text {$j$ even} } } \paren {-1}^{j / 2} \dbinom n j x^{n - j} y^j
      | c = {{Defof|Real Part}}
}}
{{end-eqn}}
Then we have:
{{begin-eqn}}
{{eqn | l = \map {\dfrac \partial {\partial x} } {\map \Re {z^n} }
      | r = \sum_{\substack {0 \mathop \le j \mathop \le n \\ \text {$j$ even} } } \paren {-1}^{j / 2} \dbinom n j \paren {n - j} x^{n - j - 1} y^j
      | c = {{Defof|Partial Derivative}}
}}
{{eqn | ll= \leadsto
      | l = \map {\dfrac {\partial^2} {\partial x^2} } {\map \Re {z^n} }
      | r = \sum_{\substack {0 \mathop \le j \mathop \le n \\ \text {$j$ even} } } \paren {-1}^{j / 2} \dbinom n j \paren {n - j} \paren {n - j - 1} x^{n - j - 2} y^j
      | c = {{Defof|Partial Derivative}}
}}
{{eqn | r = \sum_{\substack {0 \mathop \le j \mathop \le n - 2 \\ \text {$j$ even} } } \paren {-1}^{j / 2} \dbinom n j \paren {n - j} \paren {n - j - 1} x^{n - j - 2} y^j
      | c = as $n - j = 0$ when $j = n$ and $n - j - 1 = 0$ when $j = n - 1$, so terms vanish
}}
{{end-eqn}}
and:
{{begin-eqn}}
{{eqn | l = \map {\dfrac \partial {\partial y} } {\map \Re {z^n} }
      | r = \sum_{\substack {0 \mathop \le j \mathop \le n \\ \text {$j$ even} } } \paren {-1}^{j / 2} \dbinom n j j x^{n - j} y^{j - 1}
      | c = {{Defof|Partial Derivative}}
}}
{{eqn | ll= \leadsto
      | l = \map {\dfrac {\partial^2} {\partial y^2} } {\map \Re {z^n} }
      | r = \sum_{\substack {0 \mathop \le j \mathop \le n \\ \text {$j$ even} } } \paren {-1}^{j / 2} \dbinom n j j \paren {j - 1} x^{n - j} y^{j - 2}
      | c = {{Defof|Partial Derivative}}
}}
{{eqn | r = \sum_{\substack {2 \mathop \le j \mathop \le n \\ \text {$j$ even} } } \paren {-1}^{j / 2} \dbinom n j j \paren {j - 1} x^{n - j} y^{j - 2}
      | c = as terms vanish when $j = 0$ and $j = 1$
}}
{{eqn | r = \sum_{\substack {0 \mathop \le j \mathop \le n - 2 \\ \text {$j$ even} } } \paren {-1}^{\paren {j + 2} / 2} \dbinom n {j + 2} \paren {j + 2} \paren {j + 1} x^{n - j - 2} y^j
      | c = Translation of Index Variable of Summation
}}
{{end-eqn}}
It remains to be shown that for $j \in \set {0, 1, \ldots, n - 2}$ that:
:$\paren {-1}^{j / 2} \dbinom n j \paren {n - j} \paren {n - j - 1} = -\paren {-1}^{\paren {j + 2} / 2} \dbinom n {j + 2} \paren {j + 2} \paren {j + 1}$
First we have that:
{{begin-eqn}}
{{eqn | l = \paren {-1}^{\paren {j + 2} / 2}
      | r = \paren {-1}^{\paren {j / 2} + 1}
      | c = 
}}
{{eqn | r = -\paren {-1}^{j / 2}
      | c = 
}}
{{end-eqn}}
Hence it remains to be shown that:
:$\dbinom n j \paren {n - j} \paren {n - j - 1} = \dbinom n {j + 2} \paren {j + 2} \paren {j + 1}$
We have:
{{begin-eqn}}
{{eqn | l = \dbinom n j \paren {n - j} \paren {n - j - 1}
      | r = \dbinom n {n - j} \paren {n - j} \paren {n - j - 1}
      | c = Symmetry Rule for Binomial Coefficients
}}
{{eqn | r = n \dbinom {n - 1} {n - j - 1} \paren {n - j - 1}
      | c = Factors of Binomial Coefficient
}}
{{eqn | ll= \leadsto
      | n = 1
      | l = \dbinom n j \paren {n - j} \paren {n - j - 1}
      | r = n \paren {n - 1} \dbinom {n - 2} {n - j - 2}
      | c = Factors of Binomial Coefficient
}}
{{end-eqn}}
and:
{{begin-eqn}}
{{eqn | l = \dbinom n {j + 2} \paren {j + 2} \paren {j + 1}
      | r = n \dbinom {n - 1} {j + 1} \paren {j + 1}
      | c = Factors of Binomial Coefficient
}}
{{eqn | r = n \paren {n - 1} \dbinom {n - 2} j
      | c = Factors of Binomial Coefficient
}}
{{eqn | r = n \paren {n - 1} \dbinom {n - 2} {n - j - 2}
      | c = Symmetry Rule for Binomial Coefficients
}}
{{eqn | r = \dbinom n j \paren {n - j} \paren {n - j - 1}
      | c = from $(1)$
}}
{{end-eqn}}
Hence the result.
{{qed}}