1: \begin{proof}[Proof of Theorem \ref{TCcommutes}]

2: Consider an $X \in \CycSp_{\geq 0}$ which is $p$-complete.  Since $\TC(X\otimes (-)^{\mathrm{triv}})$ is an exact functor from spectra to spectra with value $\TC(X)$ on $S^0$, we get a natural transformation

3: \[ \TC(X) \otimes (-) \to \TC(X \otimes (-)^{\mathrm{triv}}),\]

4: uniquely characterized by being an equivalence on $S^0$, hence on any finite spectrum.\footnote{This is a standard ``assembly map".  To construct it rigorously, note that left Kan extension of the restriction of the right hand side to finite spectra is uniquely characterized by its value on $S^0$, by the universal property of spectra among presentable stable $\infty$-categories, and therefore identifies with the left hand side.} By Corollary~\ref{geometricreal}, it is also an equivalence on any geometric realization of finite connective spectra, i.e.,

5: for any connective spectrum whose homology groups are finitely generated, e.g.,

6: $H \bb F_p$.

7: So we have shown that, for any $X \in

8: \CycSp_{\geq 0}$ which is $p$-complete, there is a natural equivalence

9: $$\TC(X) \otimes H\mathbb{F}_p \simeq \TC(X \otimes

10: H\mathbb{F}_p^{\mathrm{triv}}).$$

11: 

12: Replacing $X$ with $X/p$, the same conclusion follows for an arbitrary

13: $X \in \CycSp_{\geq 0}$.  Then from Corollary~\ref{Fpcommutecolimit} we deduce that the functor $X

14: \mapsto \TC(X) \otimes H\mathbb{F}_p$ commutes

15: with colimits in $\CycSp_{\geq 0}$. 

16: Hence, given a diagram $I\to\CycSp_{\geq

17: 0}$, the induced map of spectra

18: \begin{equation} \label{TCcolim} \varinjlim_I \TC(X_i) \to \TC(X) \end{equation} 

19: becomes an equivalence after smashing with $H\mathbb{F}_p$. 

20: Since both sides are bounded below mod $p$ by Lemma \ref{connectivity}, it

21: follows that \eqref{TCcolim}

22: is an equivalence after smashing with $S^0/p$.

23: \end{proof}

24: