Move discussion of 0 to footnote

Thanks to Elias Guisado
https://stacks.math.columbia.edu/tag/05T8#comment-8397

derived.tex

@@ -5392,12 +5392,15 @@ \section{Derived functors on derived categories}
 \end{lemma}
 
 \begin{proof}
-We may add $0$ to $\mathcal{I}$ if necessary. Pick $A \in \mathcal{I}$.
-Let $A[0] \to K^\bullet$ be a quasi-isomorphism with $K^\bullet$
+Pick $A \in \mathcal{I}$. Let $A[0] \to K^\bullet$
+be a quasi-isomorphism with $K^\bullet$
 bounded below. Then we can find a quasi-isomorphism
 $K^\bullet \to I^\bullet$ with $I^\bullet$ bounded below and
 each $I^n \in \mathcal{I}$, see
-Lemma \ref{lemma-subcategory-right-resolution}.
+Lemma \ref{lemma-subcategory-right-resolution}\footnote{By (1)
+we see that $\mathcal{I}$ is nonempty. Pick $P$ in $\mathcal{I}$.
+Then the short exact sequence $0 \to P \to P \to 0 \to 0$ and assumption (2)
+shows that $0$ is in $\mathcal{I}$. Thus the lemma applies.}.
 Hence we see that these resolutions are cofinal in the category
 $A[0]/\text{Qis}^{+}(\mathcal{A})$. To finish the proof it therefore
 suffices to show that for any quasi-isomorphism