If complex numbers are merely a definition with defined operations, how come they can help prove properties of real numbers? It is often said that complex numbers were to some degree originally introduced by Rafael Bombelli, who together with Gerolamo Cardano was trying to find solutions to cubic equations.  In one YouTube series titled "Imaginary Numbers are Real", it is mentioned that Bombelli studied equations of the type $x^3=dx+c$, and found
$$x=\sqrt[3]{\frac{d}{2}+\sqrt{\frac{d^2}{4}-\frac{c^2}{27}}} + \sqrt[3]{\frac{d}{2}-\sqrt{\frac{d^2}{4}-\frac{c^2}{27}}}$$
to be one solution. Looking at the equation $x^3=15x+4$ and substituting $d=15,c=4$ one obtains:
$$x=\sqrt[3]{2+\sqrt{-121}}+\sqrt[3]{2-\sqrt{-121}}$$
it is then said that Rafael essentially just assumed that $\sqrt{-1}$ was a normal number with the property that $\sqrt{-1}^2=-1$, and that $\sqrt{-a}=\sqrt{a}*\sqrt{-1}$, and then using some clever algebra and solving a system of equations, managed to eventually cancel out any $\sqrt{-1}$'s, and get:
$$x=4$$
And indeed one can check that $x=4$ is a solution to $x^3=15x+4$. When one introduces a new definition into mathematics, there are obviously certain restrictions, such as the definition having to be consistent with the rest of mathematics. At the end of the day however, it is just a definition, and we get to choose it and it's operations. For example, we could define complex numbers without much reference to the intuitive idea behind "square roots of minus 1" as:
A complex number $z$ is an ordered pair $(a,b)$ of two real numbers $a$ and $b$, often written with the following notational rule
$$(a,b): a+bi $$
plus the following shorthands:
$$\begin{eqnarray}
    && (0,b) & = & bi \\
    && (a,0) & = & a \\
    && (a,1) & = & a & + & i \\
    && (a,-1) & = & a & - & i \\
    && (0,1) & = & i  \\
    && (0,-1) & = - & i \\
    \end{eqnarray}$$
The equality relation $=$ for two complex numbers $z_1, z_2$
is defined as:
$$z_1 = z_2 \equiv (a_1=a_2 \wedge b_1=b_2)  $$
The addition operation $+$ is defined as:
$$z_1+z_2 = (a_1+a_2,b_1+b_2)  $$
The multiplicative operation $\cdot$ is defined as:
$$z_1 \cdot z_2 = (a_1 \cdot a_2 - b_1 \cdot b_2, a_1 \cdot b_2 + b_1 \cdot a_1)$$
Note that setting $a_1=a_2=0$ and $b_1=b_2=1$ and using the notation yields:
$$i \cdot i=(0 \cdot 0 - 1 \cdot 1)+(0 \cdot 1 + 1 \cdot 0)i = -1 $$
This is all fine, and one could define other operations such as raising complex numbers to real powers, real powers to complex numbers, taking logarithms of complex numbers and so on. But if this is merely definition, how do we know we can use it to prove facts about the real numbers as Rafael did? Was it merely intuition and luck on his side that gave him the final correct conclusion?
 A: What you wrote

At the end of the day however, it is just a definition, and we get to choose it and it's operations.

is technically correct. We could, in the same way,
define variants of the complex numbers such as
split-complex numbers
which appear with overa dozen different names. Another variant is the
dual numbers.
These are all mere variant definitions (they only appeared
in the 1800s) and have equal validity in some sense.
Complex numbers were not well understood (not quite "real")
by anyone until around 1800 when it was noticed that the
complex numbers could be identified with the complex plane.
That is, the points in a Cartesian coordinate system
could be interpreted as complex numbers along with
a geometric interpretation of complex addition and complex
multiplication. With this discovery, the complex
numbers were endowed with geometrical meaning and
no longer just an arbitrarily defined extension
of real numbers. There is a lot more to the history
of complex numbers but this is the very brief version.
Your question

But if this is merely definition, how do we know we can use it to prove facts about the real numbers as Rafael did? Was it merely intuition and luck on his side that gave him the final correct conclusion?

is a good one. The answer is mostly based
on the fact that the complex numbers are
the algebraic closure of the real numbers.
What this means is that in order to provide
all polynomials with real coefficients with
roots we need to introduce complex numbers.
From Wikipedia The fundamental theorem of algebra

The fundamental theorem of algebra states that every non-constant single-variable polynomial with complex coefficients has at least one complex root. This includes polynomials with real coefficients, since every real number is a complex number with its imaginary part equal to zero.
Equivalently (by definition), the theorem states that the field of complex numbers is algebraically closed.

We can apparently avoid this by restating
the fundamental theorem as

... it follows from the fundamental theorem of algebra that every non-constant polynomial with real coefficients can be written as a product of polynomials with real coefficients whose degrees are either 1 or 2

and in this version the complex numbers
appear implicitly in complex conjugate
pairs as the roots of the degree 2 factors.
Note that the other two complex number
variants that where mentioned earlier do
not provide any non real roots for
real polynomials.
The Wikipedia articles that I link to have
historical information that may be helpful
for you.
