Projective complexes model the bounded above derived category

Every bounded-above projective complex is K-projective. The no-roof theorem and the fully faithful bounded embedding identify its Hom in $K$ with Hom in $D^{-}$. This proves full faithfulness, including the zero complex.

Enough projectives gives objectwise replacements under the stated choice hypothesis; here $p_X$ are supplied simultaneously. Put $R(X)=P_X$. For $u:X\to Y$ in $D^{-}$, full faithfulness gives a unique homotopy class $R(u):P_X\to P_Y$ with $Q(R(u))=Q(p_Y{)}^{-1}uQ(p_X)$. Uniqueness gives identity and composition laws. The maps $Q(p_X)$ and their unique lifts provide the natural isomorphisms for a quasi-inverse.

Finite sums of projectives are projective by lifting their component maps. Hence shifts and cones of maps of bounded-above projectives stay in the model. Its cone triangulation is the restricted one from $K$; the inclusion is exact. A triangle transported by $R$ is isomorphic to a model cone triangle: lift its first arrow, take its cone, and use TR3 plus the two-isomorphism argument to compare completions. Thus the equivalence is exact. Its Hom sets are the ordinary homotopy-class quotients of sets of complex maps.