---

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


1. beta : ℕ ⟶ ℕ
2. n0 : finite-nat-seq()
3. x : ℕ
4. ∃y:ℕx + 1. (¬((beta y) = 0 ∈ ℤ))
⊢ ∃x1:ℕx + 1. ((¬((beta x1) = 0 ∈ ℤ)) ∧ (∀y:ℕx1. ((beta y) = 0 ∈ ℤ)))
BY
{ (NatInd (-2) THEN (D 0 THENA Auto)) }

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

2
1. beta : ℕ ⟶ ℕ
2. n0 : finite-nat-seq()
3. x : ℤ
4. [%1] : 0 < x
5. (∃y:ℕ(x - 1) + 1. (¬((beta y) = 0 ∈ ℤ)))
⇒ (∃x1:ℕ(x - 1) + 1. ((¬((beta x1) = 0 ∈ ℤ)) ∧ (∀y:ℕx1. ((beta y) = 0 ∈ ℤ))))
6. ∃y:ℕx + 1. (¬((beta y) = 0 ∈ ℤ))
⊢ ∃x1:ℕx + 1. ((¬((beta x1) = 0 ∈ ℤ)) ∧ (∀y:ℕx1. ((beta y) = 0 ∈ ℤ)))

---

Latex:

---

Latex:

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


By

---

Latex:
(NatInd  (-2)  THEN  (D  0  THENA  Auto))

---

Home Index