---

Step * of Lemma weak-Markov-principle-alt

∀a,b:ℕ ⟶ ℕ.  ((∀c:ℕ ⟶ ℕ. ((¬(a = c ∈ (ℕ ⟶ ℕ))) ∨ (¬(b = c ∈ (ℕ ⟶ ℕ))))) ⇒ (∃n:ℕ. (¬((a n) = (b n) ∈ ℤ))))
BY
{ xxx(Auto
      THEN Assert ⌜∀c:ℕ ⟶ ℕ
                     ∃i:ℕ. (((i = 0 ∈ ℤ) ⇒ (¬(a = c ∈ (ℕ ⟶ ℕ)))) ∧ ((¬(i = 0 ∈ ℤ)) ⇒ (¬(b = c ∈ (ℕ ⟶ ℕ)))))⌝⋅
      )xxx }

1
.....assertion..... 
1. a : ℕ ⟶ ℕ
2. b : ℕ ⟶ ℕ
3. ∀c:ℕ ⟶ ℕ. ((¬(a = c ∈ (ℕ ⟶ ℕ))) ∨ (¬(b = c ∈ (ℕ ⟶ ℕ))))
⊢ ∀c:ℕ ⟶ ℕ. ∃i:ℕ. (((i = 0 ∈ ℤ) ⇒ (¬(a = c ∈ (ℕ ⟶ ℕ)))) ∧ ((¬(i = 0 ∈ ℤ)) ⇒ (¬(b = c ∈ (ℕ ⟶ ℕ)))))

2
1. a : ℕ ⟶ ℕ
2. b : ℕ ⟶ ℕ
3. ∀c:ℕ ⟶ ℕ. ((¬(a = c ∈ (ℕ ⟶ ℕ))) ∨ (¬(b = c ∈ (ℕ ⟶ ℕ))))
4. ∀c:ℕ ⟶ ℕ. ∃i:ℕ. (((i = 0 ∈ ℤ) ⇒ (¬(a = c ∈ (ℕ ⟶ ℕ)))) ∧ ((¬(i = 0 ∈ ℤ)) ⇒ (¬(b = c ∈ (ℕ ⟶ ℕ)))))
⊢ ∃n:ℕ. (¬((a n) = (b n) ∈ ℤ))

---

Latex:

---

Latex:
\mforall{}a,b:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}.    ((\mforall{}c:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}.  ((\mneg{}(a  =  c))  \mvee{}  (\mneg{}(b  =  c))))  {}\mRightarrow{}  (\mexists{}n:\mBbbN{}.  (\mneg{}((a  n)  =  (b  n)))))


By

---

Latex:
xxx(Auto  THEN  Assert  \mkleeneopen{}\mforall{}c:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}.  \mexists{}i:\mBbbN{}.  (((i  =  0)  {}\mRightarrow{}  (\mneg{}(a  =  c)))  \mwedge{}  ((\mneg{}(i  =  0))  {}\mRightarrow{}  (\mneg{}(b  =  c))))\mkleeneclose{}\mcdot{})xxx

---

Home Index