---

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


1. a : ℕ ⟶ ℕ
2. k : ℕ
3. increasing-sequence(a)
4. n : ℕ
5. ¬n + 1 < k
6. n < k
⊢ ((a k) = (a n) ∈ ℕ) ∨ ((a k) = ((a n) + 1) ∈ ℕ)
BY
{ ((Assert ⌜k = (n + 1) ∈ ℕ⌝⋅ THENA Auto) THEN (Eliminate ⌜k⌝⋅ THENA Auto)) }

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

---

Latex:

---

Latex:

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


By

---

Latex:
((Assert  \mkleeneopen{}k  =  (n  +  1)\mkleeneclose{}\mcdot{}  THENA  Auto)  THEN  (Eliminate  \mkleeneopen{}k\mkleeneclose{}\mcdot{}  THENA  Auto))

---

Home Index