---

Step * 1 1 of Lemma increasing-baire-eq-from


1. n : ℕ
2. a : ℕ ⟶ ℕ
3. k : ℕ
4. increasing-sequence(a)
5. ¬n + 1 < n + 1
6. n < n + 1
7. k = (n + 1) ∈ ℕ
⊢ ((a (n + 1)) = (a n) ∈ ℕ) ∨ ((a (n + 1)) = ((a n) + 1) ∈ ℕ)
BY
{ (Unfold `increasing-sequence` (-4) THEN Auto) }

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  a  :  \mBbbN{}  {}\mrightarrow{}  \mBbbN{}
3.  k  :  \mBbbN{}
4.  increasing-sequence(a)
5.  \mneg{}n  +  1  <  n  +  1
6.  n  <  n  +  1
7.  k  =  (n  +  1)
\mvdash{}  ((a  (n  +  1))  =  (a  n))  \mvee{}  ((a  (n  +  1))  =  ((a  n)  +  1))


By

---

Latex:
(Unfold  `increasing-sequence`  (-4)  THEN  Auto)

---

Home Index