---

Step * of Lemma weak-Markov-principle2-alt

∀a:ℕ*. ((∀c:ℕ*. ((¬(a = c ∈ ℕ*)) ∨ (¬(0 = c ∈ ℕ*)))) ⇒ (∃n:ℕ. 0 < a n))
BY
{ (InstLemma `weak-Markov-principle2` []
   THEN RepeatFor 2 ((ParallelLast' THENA Auto))
   THEN (D 2 With ⌜c⌝  THENA Auto)
   THEN RepeatFor 2 (ParallelLast)
   THEN Symmetry
   THEN DVar `c'
   THEN EqTypeCD
   THEN Auto
   THEN FunExt
   THEN Auto
   THEN SupposeNot
   THEN D 4
   THEN D 0 With ⌜x⌝ 
   THEN Auto) }

1
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) ∈ ℤ)

---

Latex:

---

Latex:
\mforall{}a:\mBbbN{}*.  ((\mforall{}c:\mBbbN{}*.  ((\mneg{}(a  =  c))  \mvee{}  (\mneg{}(0  =  c))))  {}\mRightarrow{}  (\mexists{}n:\mBbbN{}.  0  <  a  n))


By

---

Latex:
(InstLemma  `weak-Markov-principle2`  []
  THEN  RepeatFor  2  ((ParallelLast'  THENA  Auto))
  THEN  (D  2  With  \mkleeneopen{}c\mkleeneclose{}    THENA  Auto)
  THEN  RepeatFor  2  (ParallelLast)
  THEN  Symmetry
  THEN  DVar  `c'
  THEN  EqTypeCD
  THEN  Auto
  THEN  FunExt
  THEN  Auto
  THEN  SupposeNot
  THEN  D  4
  THEN  D  0  With  \mkleeneopen{}x\mkleeneclose{} 
  THEN  Auto)

---

Home Index