---

Step * of Lemma increasing-sequence-prop1

∀a:ℕ ⟶ ℕ. (increasing-sequence(a) ⇒ (∀n,m:ℕ.  ((n ≤ m) ⇒ ((a n) ≤ (a m)))))
BY
{ ((UnivCD THENA Auto)
   THEN (Assert ⌜∃k:ℕ. (m = (n + k) ∈ ℤ)⌝⋅ THENA (InstConcl [⌜m - n⌝]⋅ THEN Auto))
   THEN ExRepD
   THEN Eliminate ⌜m⌝⋅
   THEN ThinVar `m') }

1
1. n : ℕ
2. k : ℕ
3. a : ℕ ⟶ ℕ
4. increasing-sequence(a)
5. n ≤ (n + k)
⊢ (a n) ≤ (a (n + k))

---

Latex:

---

Latex:
\mforall{}a:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}.  (increasing-sequence(a)  {}\mRightarrow{}  (\mforall{}n,m:\mBbbN{}.    ((n  \mleq{}  m)  {}\mRightarrow{}  ((a  n)  \mleq{}  (a  m)))))


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  (Assert  \mkleeneopen{}\mexists{}k:\mBbbN{}.  (m  =  (n  +  k))\mkleeneclose{}\mcdot{}  THENA  (InstConcl  [\mkleeneopen{}m  -  n\mkleeneclose{}]\mcdot{}  THEN  Auto))
  THEN  ExRepD
  THEN  Eliminate  \mkleeneopen{}m\mkleeneclose{}\mcdot{}
  THEN  ThinVar  `m')

---

Home Index