---

Step * 1 of Lemma weak-Markov-principle2-alt


1. a : ℕ*
2. c : ℕ ⟶ ℕ
3. ∀i,j:ℕ.  (0 < c i ⇒ 0 < c j ⇒ (i = j ∈ ℤ))
4. x : ℕ
5. ¬((c x) = (0 x) ∈ ℕ)
⊢ ¬(0 = (c x) ∈ ℤ)
BY
{ (RepUR ``nat-star-0`` -1 THEN Auto) }

---

Latex:

---

Latex:

1.  a  :  \mBbbN{}*
2.  c  :  \mBbbN{}  {}\mrightarrow{}  \mBbbN{}
3.  \mforall{}i,j:\mBbbN{}.    (0  <  c  i  {}\mRightarrow{}  0  <  c  j  {}\mRightarrow{}  (i  =  j))
4.  x  :  \mBbbN{}
5.  \mneg{}((c  x)  =  (0  x))
\mvdash{}  \mneg{}(0  =  (c  x))


By

---

Latex:
(RepUR  ``nat-star-0``  -1  THEN  Auto)

---

Home Index