---

Step * 1 1 1 1 of Lemma gamma-neighbourhood-prop2


1. beta : ℕ ⟶ ℕ
2. n0 : finite-nat-seq()
3. ∃y:ℕ0 + 1. (¬((beta y) = 0 ∈ ℤ))
⊢ ∃x1:ℕ0 + 1. ((¬((beta x1) = 0 ∈ ℤ)) ∧ (∀y:ℕx1. ((beta y) = 0 ∈ ℤ)))
BY
{ (ExRepD THEN (Assert ⌜y = 0 ∈ ℤ⌝⋅ THENA Auto) THEN InstConcl [⌜0⌝]⋅ THEN Auto) }

---

Latex:

---

Latex:

1.  beta  :  \mBbbN{}  {}\mrightarrow{}  \mBbbN{}
2.  n0  :  finite-nat-seq()
3.  \mexists{}y:\mBbbN{}0  +  1.  (\mneg{}((beta  y)  =  0))
\mvdash{}  \mexists{}x1:\mBbbN{}0  +  1.  ((\mneg{}((beta  x1)  =  0))  \mwedge{}  (\mforall{}y:\mBbbN{}x1.  ((beta  y)  =  0)))


By

---

Latex:
(ExRepD  THEN  (Assert  \mkleeneopen{}y  =  0\mkleeneclose{}\mcdot{}  THENA  Auto)  THEN  InstConcl  [\mkleeneopen{}0\mkleeneclose{}]\mcdot{}  THEN  Auto)

---

Home Index