---

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


1. beta : ℕ ⟶ ℕ
2. n0 : finite-nat-seq()
3. x : ℤ
4. 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
7. ¬((beta y) = 0 ∈ ℤ)
8. ¬(∃k:ℕ(x - 1) + 1. (¬((beta k) = 0 ∈ ℤ)))
9. ¬((beta y) = 0 ∈ ℤ)
10. y1 : ℕy
⊢ (beta y1) = 0 ∈ ℤ
BY
{ SupposeNot }

1
1. beta : ℕ ⟶ ℕ
2. n0 : finite-nat-seq()
3. x : ℤ
4. 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
7. ¬((beta y) = 0 ∈ ℤ)
8. ¬(∃k:ℕ(x - 1) + 1. (¬((beta k) = 0 ∈ ℤ)))
9. ¬((beta y) = 0 ∈ ℤ)
10. y1 : ℕy
11. ¬((beta y1) = 0 ∈ ℤ)
⊢ (beta y1) = 0 ∈ ℤ

---

Latex:

---

Latex:

1.  beta  :  \mBbbN{}  {}\mrightarrow{}  \mBbbN{}
2.  n0  :  finite-nat-seq()
3.  x  :  \mBbbZ{}
4.  0  <  x
5.  (\mexists{}y:\mBbbN{}(x  -  1)  +  1.  (\mneg{}((beta  y)  =  0)))
{}\mRightarrow{}  (\mexists{}x1:\mBbbN{}(x  -  1)  +  1.  ((\mneg{}((beta  x1)  =  0))  \mwedge{}  (\mforall{}y:\mBbbN{}x1.  ((beta  y)  =  0))))
6.  y  :  \mBbbN{}x  +  1
7.  \mneg{}((beta  y)  =  0)
8.  \mneg{}(\mexists{}k:\mBbbN{}(x  -  1)  +  1.  (\mneg{}((beta  k)  =  0)))
9.  \mneg{}((beta  y)  =  0)
10.  y1  :  \mBbbN{}y
\mvdash{}  (beta  y1)  =  0


By

---

Latex:
SupposeNot

---

Home Index