[proofplan]
We first check that $\mathfrak a+\mathfrak b$ is an ideal by using the ideal property of $\mathfrak a$ and $\mathfrak b$ separately on each summand. To prove solvability, we compare the derived series of $\mathfrak a+\mathfrak b$ with the quotient by $\mathfrak a$. The quotient $(\mathfrak a+\mathfrak b)/\mathfrak a$ is a homomorphic image of the solvable Lie algebra $\mathfrak b$, so enough derived steps place the derived series of $\mathfrak a+\mathfrak b$ inside $\mathfrak a$; the solvability of $\mathfrak a$ then kills the remaining derived series.
[/proofplan]
[step:Show that the sum is an ideal of $\mathfrak g$]
Let $\mathfrak s:=\mathfrak a+\mathfrak b$. Since $\mathfrak a$ and $\mathfrak b$ are vector subspaces of $\mathfrak g$, their sum $\mathfrak s$ is a vector subspace of $\mathfrak g$.
We prove that $\mathfrak s$ is an ideal. Let $x\in\mathfrak g$ and let $y\in\mathfrak s$. By definition of $\mathfrak s$, there exist $u\in\mathfrak a$ and $v\in\mathfrak b$ such that $y=u+v$. Since $\mathfrak a\trianglelefteq\mathfrak g$ and $\mathfrak b\trianglelefteq\mathfrak g$, we have $[x,u]\in\mathfrak a$ and $[x,v]\in\mathfrak b$. Bilinearity of the Lie bracket gives
\begin{align*}
[x,y]=[x,u+v]=[x,u]+[x,v]\in\mathfrak a+\mathfrak b=\mathfrak s.
\end{align*}
Thus $[\mathfrak g,\mathfrak s]\subseteq\mathfrak s$, so $\mathfrak s\trianglelefteq\mathfrak g$.
[/step]
[step:Define the derived series and choose vanishing stages for $\mathfrak a$ and $\mathfrak b$]
For any Lie algebra $\mathfrak h$, define its derived series $(\mathfrak h^{(r)})_{r\geq 0}$ by
\begin{align*}
\mathfrak h^{(0)}&:=\mathfrak h,\\
\mathfrak h^{(r+1)}&:=[\mathfrak h^{(r)},\mathfrak h^{(r)}]\qquad\text{for every }r\geq 0.
\end{align*}
Here $[\mathfrak u,\mathfrak v]$ denotes the vector subspace spanned by all brackets $[u,v]$ with $u\in\mathfrak u$ and $v\in\mathfrak v$.
Since $\mathfrak a$ and $\mathfrak b$ are solvable, there exist integers $m,n\geq 0$ such that
\begin{align*}
\mathfrak a^{(m)}=0,
\qquad
\mathfrak b^{(n)}=0.
\end{align*}
[/step]
[step:Use the quotient by $\mathfrak a$ to force the derived series into $\mathfrak a$]
Let
\begin{align*}
\pi:\mathfrak s&\to \mathfrak s/\mathfrak a\\
x&\mapsto x+\mathfrak a
\end{align*}
be the quotient Lie algebra homomorphism. Since $\mathfrak a\trianglelefteq\mathfrak s$, this quotient Lie algebra is well-defined. Define the kernel of $\pi$ by
\begin{align*}
\ker\pi:=\{x\in\mathfrak s: \pi(x)=0+\mathfrak a\}.
\end{align*}
We claim that $(\mathfrak s/\mathfrak a)^{(n)}=0$. Indeed, define
\begin{align*}
\varphi:\mathfrak b&\to \mathfrak s/\mathfrak a\\
v&\mapsto v+\mathfrak a.
\end{align*}
This is a Lie algebra homomorphism because it is the restriction of $\pi$ to $\mathfrak b$. It is surjective: if $u+v\in\mathfrak s$ with $u\in\mathfrak a$ and $v\in\mathfrak b$, then
\begin{align*}
(u+v)+\mathfrak a=v+\mathfrak a=\varphi(v).
\end{align*}
For every Lie algebra homomorphism $\psi:\mathfrak h\to\mathfrak q$ and every $r\geq 0$, induction on $r$ gives
\begin{align*}
\psi(\mathfrak h^{(r)})=\psi(\mathfrak h)^{(r)}
\end{align*}
whenever $\psi$ is surjective. Applying this to $\varphi$ gives
\begin{align*}
(\mathfrak s/\mathfrak a)^{(n)}
=\varphi(\mathfrak b)^{(n)}
=\varphi(\mathfrak b^{(n)})
=\varphi(0)
=0.
\end{align*}
Now $\pi$ is surjective, so the same derived-series compatibility gives
\begin{align*}
\pi(\mathfrak s^{(n)})=(\mathfrak s/\mathfrak a)^{(n)}=0.
\end{align*}
Therefore $\mathfrak s^{(n)}\subseteq\ker\pi=\mathfrak a$.
[guided]
The purpose of passing to the quotient by $\mathfrak a$ is to isolate the contribution of $\mathfrak b$. Define the quotient homomorphism
\begin{align*}
\pi:\mathfrak s&\to \mathfrak s/\mathfrak a\\
x&\mapsto x+\mathfrak a.
\end{align*}
This map is defined because $\mathfrak a$ is an ideal of $\mathfrak s$: since $\mathfrak a\trianglelefteq\mathfrak g$ and $\mathfrak s\subseteq\mathfrak g$, we have $[\mathfrak s,\mathfrak a]\subseteq[\mathfrak g,\mathfrak a]\subseteq\mathfrak a$. Define the kernel of $\pi$ by
\begin{align*}
\ker\pi:=\{x\in\mathfrak s: \pi(x)=0+\mathfrak a\}.
\end{align*}
Now define
\begin{align*}
\varphi:\mathfrak b&\to \mathfrak s/\mathfrak a\\
v&\mapsto v+\mathfrak a.
\end{align*}
This is a Lie algebra homomorphism because for $v_1,v_2\in\mathfrak b$,
\begin{align*}
\varphi([v_1,v_2])
=[v_1,v_2]+\mathfrak a
=[v_1+\mathfrak a,v_2+\mathfrak a]
=[\varphi(v_1),\varphi(v_2)].
\end{align*}
It is surjective because every element of $\mathfrak s/\mathfrak a$ has the form $(u+v)+\mathfrak a$ with $u\in\mathfrak a$ and $v\in\mathfrak b$, and this coset equals $v+\mathfrak a=\varphi(v)$.
We also need the standard compatibility between surjective homomorphisms and derived series. Let $\psi:\mathfrak h\to\mathfrak q$ be a surjective Lie algebra homomorphism. We prove by induction that
\begin{align*}
\psi(\mathfrak h^{(r)})=\mathfrak q^{(r)}
\end{align*}
for every $r\geq 0$. For $r=0$, this is exactly surjectivity: $\psi(\mathfrak h)=\mathfrak q$. If the equality holds for $r$, then bracket preservation and bilinearity give
\begin{align*}
\psi(\mathfrak h^{(r+1)})
&=\psi([\mathfrak h^{(r)},\mathfrak h^{(r)}])\\
&=[\psi(\mathfrak h^{(r)}),\psi(\mathfrak h^{(r)})]\\
&=[\mathfrak q^{(r)},\mathfrak q^{(r)}]\\
&=\mathfrak q^{(r+1)}.
\end{align*}
Applying this result to the surjective homomorphism $\varphi:\mathfrak b\to\mathfrak s/\mathfrak a$ yields
\begin{align*}
(\mathfrak s/\mathfrak a)^{(n)}
=\varphi(\mathfrak b)^{(n)}
=\varphi(\mathfrak b^{(n)})
=\varphi(0)
=0.
\end{align*}
Finally apply the same compatibility to the quotient map $\pi:\mathfrak s\to\mathfrak s/\mathfrak a$. Since $(\mathfrak s/\mathfrak a)^{(n)}=0$, we get
\begin{align*}
\pi(\mathfrak s^{(n)})=(\mathfrak s/\mathfrak a)^{(n)}=0.
\end{align*}
Thus every element of $\mathfrak s^{(n)}$ lies in $\ker\pi=\mathfrak a$, so $\mathfrak s^{(n)}\subseteq\mathfrak a$.
[/guided]
[/step]
[step:Take the remaining derived steps inside $\mathfrak a$]
We prove by induction on $r\geq 0$ that
\begin{align*}
\mathfrak s^{(n+r)}\subseteq\mathfrak a^{(r)}.
\end{align*}
For $r=0$, this is the inclusion $\mathfrak s^{(n)}\subseteq\mathfrak a$ proved above. Suppose $\mathfrak s^{(n+r)}\subseteq\mathfrak a^{(r)}$. Then
\begin{align*}
\mathfrak s^{(n+r+1)}
&=[\mathfrak s^{(n+r)},\mathfrak s^{(n+r)}]\\
&\subseteq[\mathfrak a^{(r)},\mathfrak a^{(r)}]\\
&=\mathfrak a^{(r+1)}.
\end{align*}
Thus the induction is complete. Taking $r=m$ gives
\begin{align*}
\mathfrak s^{(n+m)}\subseteq\mathfrak a^{(m)}=0.
\end{align*}
Therefore $\mathfrak s^{(n+m)}=0$, so $\mathfrak s=\mathfrak a+\mathfrak b$ is solvable. Combined with the first step, $\mathfrak a+\mathfrak b$ is a solvable ideal of $\mathfrak g$.
[/step]
