If not equal implies apart, Markov's principle follows

[jkingdon]

If not equal implies apart, Markov's principle follows

[benjub]

Probably the same type of construction as for the omniscience problem of #3757 ? Given a property $P \colon \omega \to 2$, define $x:=\sum_n P_n 2^{-n}$. If $x = 0$, then $\neg \exists n P_n=1$. Therefore, if $\neg\neg \exists n P_n=1$, then $x \neq 0$, so by hypothesis, $x$ is apart from zero, so it is positive (since it is a sum of nonegative numbers, it cannot be negative). Therefore, it is larger than some $2^{-N}$, so there is a natural $n$ (at most $N$) such that $P_n = 1$.