prove Eckart-Young-Minsky theorem for Frobinius norm.

I was following the proof on Wikipedia:

$\| A-A_k \|^2_F = \| \sum_{i=k+1}^n \sigma_iu_iv_i^{\top} \|_F^2= \|U \Sigma V^{\top}\|_F^2= \| \Sigma \|_F^2=\sum_{i=k+1}^n \sigma_i^2$.

Notice that applying triangle inequality to the spectral norm of $A$, we get that

if $A=A'+A''$ then $\sigma_1(A) \leq \sigma_1(A')+\sigma_1(A'')$

\ We then have $\sigma_i(A')+\sigma_j(A'')=\sigma_1(A'-A'_{i-1})+\sigma_1(A''-A''_{j-1}) \geq \sigma_1(A-A'_{i-1}-A''_{j-1}) $

Then they said: $\sigma_1(A-A'_{i-1}-A''_{j-1}) \geq \sigma_1(A-A_{i+j-2})$. I got lost here.

here's the proof using von Neumann trace inequality

background
$A = U\Sigma V^*$
$A_k$ has its singular values in a matrix $\Gamma$

in both cases we have the usual ordering $\sigma_1 \geq \sigma_2 \geq ... \geq \sigma_n$ and $\gamma_1 \geq \gamma_2 \geq ... \geq \gamma_n$
$A_k$ being rank k means the first $k$ are positive and the rest are zero for $\Gamma$

notationally it's convenient to bipartition A's singular values so
$\Sigma = \Sigma^{(k)} + \Sigma^{(\gt k)}$
where the $\Sigma^{(k)}$ is defined as being $\Sigma$ except all $\sigma_{j} :=0$ for $j \geq k+1$

the von Neumann trace inequality tells us that
$\big \vert \text{trace}\big(A^*A_k\big)\big \vert \leq \text{trace}\big(\Gamma^T\Sigma \big) = \sigma_1 \gamma_1 + \sigma_2 \gamma_2 + .... + \sigma_k \gamma_k + \sigma_{k+1}0 +... \sigma_{n}0 = \text{trace}\big(\Gamma^T\Sigma^{(k)} \big)$

main argument
The Frobenius norm is unitarily invariant so we can assume WLOG that $A=\Sigma$, so
$\big \Vert \Sigma - A_k\Big \Vert_F^2 $
$= \text{trace}\big(\Sigma^*\Sigma\big) + \text{trace}\big(A_k^*A_k\big) - \text{trace}\big(\Sigma^*A_k\big) - \text{trace}\big(A_k^*\Sigma\big) $
$= \text{trace}\big((\Sigma^{(\gt k)})^T\Sigma^{(\gt k)}\big) + \Big\{\text{trace}\big((\Sigma^{(k)})^T\Sigma^{(k)}\big) + \text{trace}\big(\Gamma^T \Gamma\big) - \Big(\text{trace}\big(\Sigma^*A_k\big) + \text{trace}\big(A_k^*\Sigma\big)\Big)\Big\} $
$\geq \text{trace}\big((\Sigma^{(\gt k)})^T\Sigma^{(\gt k)}\big) + \Big\{\text{trace}\big((\Sigma^{(k)})^T\Sigma^{(k)}\big) + \text{trace}\big(\Gamma^T \Gamma\big) - \big\vert\text{trace}\big(\Sigma^*A_k\big) + \text{trace}\big(A_k^*\Sigma\big)\big\vert\Big\} $
$\geq \text{trace}\big((\Sigma^{(\gt k)})^T\Sigma^{(\gt k)}\big) + \Big\{\text{trace}\big((\Sigma^{(k)})^T\Sigma^{(k)}\big) + \text{trace}\big(\Gamma^T \Gamma\big) - \big \vert \text{trace}\big(\Sigma^*A_k\big) \big \vert - \big \vert\text{trace}\big(A_k^*\Sigma\big) \big \vert\Big\} $
$\geq \text{trace}\big((\Sigma^{(\gt k)})^T\Sigma^{(\gt k)}\big) + \Big\{\text{trace}\big((\Sigma^{(k)})^T\Sigma^{(k)}\big) + \text{trace}\big(\Gamma^T \Gamma\big) - 2\cdot\text{trace}\big(\Gamma^T \Sigma^{(k)}\big) \Big\} $
$= \Big \Vert\Sigma^{(\gt k)}\Big \Vert_F^2 + \Big \Vert \Sigma^{(k)} - \Gamma\Big \Vert_F^2$
$\geq \Big \Vert\Sigma^{(\gt k)}\Big \Vert_F^2$

where the inequalities are triangle inequality twice, then von-neumann trace, then positive definiteness of the (squared) Frobenius norm

this lower bound is met with equality when $A_k = \Gamma = \Sigma^{(k)} $