---

Step * 1 1 1 1 1 1 1 1 2 of Lemma finite-partition-property


1. g : ℕ ⟶ ℤ
2. k : ℤ
3. [%1] : 0 < k
4. (∀i:ℕk - 1. ∃n:ℕ. (¬(∃m:ℕ. (n < m ∧ ((g m) = i ∈ ℤ))))) ⇒ (∃n:ℕ. ∀i:ℕk - 1. (¬(∃m:ℕ. (n < m ∧ ((g m) = i ∈ ℤ)))))
5. ∀i:ℕk. ∃n:ℕ. (¬(∃m:ℕ. (n < m ∧ ((g m) = i ∈ ℤ))))
⊢ ∃n:ℕ. ∀i:ℕk. (¬(∃m:ℕ. (n < m ∧ ((g m) = i ∈ ℤ))))
BY
{ ((D (-2) THENA (Auto THEN BHyp (-2) THEN Auto)) THEN D -1) }

1
1. g : ℕ ⟶ ℤ
2. k : ℤ
3. [%1] : 0 < k
4. ∀i:ℕk. ∃n:ℕ. (¬(∃m:ℕ. (n < m ∧ ((g m) = i ∈ ℤ))))
5. n : ℕ
6. ∀i:ℕk - 1. (¬(∃m:ℕ. (n < m ∧ ((g m) = i ∈ ℤ))))
⊢ ∃n:ℕ. ∀i:ℕk. (¬(∃m:ℕ. (n < m ∧ ((g m) = i ∈ ℤ))))

---

Latex:

---

Latex:

1.  g  :  \mBbbN{}  {}\mrightarrow{}  \mBbbZ{}
2.  k  :  \mBbbZ{}
3.  [\%1]  :  0  <  k
4.  (\mforall{}i:\mBbbN{}k  -  1.  \mexists{}n:\mBbbN{}.  (\mneg{}(\mexists{}m:\mBbbN{}.  (n  <  m  \mwedge{}  ((g  m)  =  i)))))
{}\mRightarrow{}  (\mexists{}n:\mBbbN{}.  \mforall{}i:\mBbbN{}k  -  1.  (\mneg{}(\mexists{}m:\mBbbN{}.  (n  <  m  \mwedge{}  ((g  m)  =  i)))))
5.  \mforall{}i:\mBbbN{}k.  \mexists{}n:\mBbbN{}.  (\mneg{}(\mexists{}m:\mBbbN{}.  (n  <  m  \mwedge{}  ((g  m)  =  i))))
\mvdash{}  \mexists{}n:\mBbbN{}.  \mforall{}i:\mBbbN{}k.  (\mneg{}(\mexists{}m:\mBbbN{}.  (n  <  m  \mwedge{}  ((g  m)  =  i))))


By

---

Latex:
((D  (-2)  THENA  (Auto  THEN  BHyp  (-2)  THEN  Auto))  THEN  D  -1)

---

Home Index