---

Step * 1 1 of Lemma rmaximum_ub


1. k : ℤ
2. n : ℤ
3. d : ℤ
⊢ ∀x:{n..(n + 0) + 1-} ⟶ ℝ. ((n ≤ k) ⇒ (k ≤ (n + 0)) ⇒ (x[k] ≤ x[n]))
BY
{ (Auto THEN Subst' k ~ n 0 THEN Auto)⋅ }

---

Latex:

---

Latex:

1.  k  :  \mBbbZ{}
2.  n  :  \mBbbZ{}
3.  d  :  \mBbbZ{}
\mvdash{}  \mforall{}x:\{n..(n  +  0)  +  1\msupminus{}\}  {}\mrightarrow{}  \mBbbR{}.  ((n  \mleq{}  k)  {}\mRightarrow{}  (k  \mleq{}  (n  +  0))  {}\mRightarrow{}  (x[k]  \mleq{}  x[n]))


By

---

Latex:
(Auto  THEN  Subst'  k  \msim{}  n  0  THEN  Auto)\mcdot{}

---

Home Index