---

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


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
7. ¬((beta y) = 0 ∈ ℤ)
⊢ ∃x1:ℕx + 1. ((¬((beta x1) = 0 ∈ ℤ)) ∧ (∀y:ℕx1. ((beta y) = 0 ∈ ℤ)))
BY
{ ((InstLemma `dec-exists-int-seg` [⌜0⌝;⌜(x - 1) + 1⌝;⌜λ2y.¬((beta y) = 0 ∈ ℤ)⌝]⋅ THENA Auto) THEN D (-1)) }

1
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
7. ¬((beta y) = 0 ∈ ℤ)
8. ∃k:ℕ(x - 1) + 1. (¬((beta k) = 0 ∈ ℤ))
⊢ ∃x1:ℕx + 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
7. ¬((beta y) = 0 ∈ ℤ)
8. ¬(∃k:ℕ(x - 1) + 1. (¬((beta k) = 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  :  \mBbbZ{}
4.  [\%1]  :  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)
\mvdash{}  \mexists{}x1:\mBbbN{}x  +  1.  ((\mneg{}((beta  x1)  =  0))  \mwedge{}  (\mforall{}y:\mBbbN{}x1.  ((beta  y)  =  0)))


By

---

Latex:
((InstLemma  `dec-exists-int-seg`  [\mkleeneopen{}0\mkleeneclose{};\mkleeneopen{}(x  -  1)  +  1\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}y.\mneg{}((beta  y)  =  0)\mkleeneclose{}]\mcdot{}  THENA  Auto)  THEN  D  (-1))

---

Home Index