---

Step * 1 1 1 of Lemma increasing-sequence-prop1


1. n : ℕ
2. a : ℕ ⟶ ℕ
3. ∀n:ℕ. (((a (n + 1)) = (a n) ∈ ℕ) ∨ ((a (n + 1)) = ((a n) + 1) ∈ ℕ))
4. k : ℤ
5. 0 < k
6. (a n) ≤ (a (n + (k - 1)))
7. ((a (n + k)) = (a (n + (k - 1))) ∈ ℕ) ∨ ((a (n + k)) = ((a (n + (k - 1))) + 1) ∈ ℕ)
⊢ (a n) ≤ (a (n + k))
BY
{ (D (-1) THEN Auto) }

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  a  :  \mBbbN{}  {}\mrightarrow{}  \mBbbN{}
3.  \mforall{}n:\mBbbN{}.  (((a  (n  +  1))  =  (a  n))  \mvee{}  ((a  (n  +  1))  =  ((a  n)  +  1)))
4.  k  :  \mBbbZ{}
5.  0  <  k
6.  (a  n)  \mleq{}  (a  (n  +  (k  -  1)))
7.  ((a  (n  +  k))  =  (a  (n  +  (k  -  1))))  \mvee{}  ((a  (n  +  k))  =  ((a  (n  +  (k  -  1)))  +  1))
\mvdash{}  (a  n)  \mleq{}  (a  (n  +  k))


By

---

Latex:
(D  (-1)  THEN  Auto)

---

Home Index