---

Step * 1 1 1 of Lemma rminimum-split


1. n : ℤ
2. i : ℕ
3. j : ℤ
⊢ ∀X:{n..(n + i + 0) + 2-} ⟶ ℝ. ∀v:ℝ.  (rmin(v;X[n + (0 + i) + 1]) = rmin(v;X[(n + i) + 1]))
BY
{ (Auto THEN Subst' (n + (0 + i) + 1) = ((n + i) + 1) ∈ ℤ 0 THEN Auto)⋅ }

---

Latex:

---

Latex:

1.  n  :  \mBbbZ{}
2.  i  :  \mBbbN{}
3.  j  :  \mBbbZ{}
\mvdash{}  \mforall{}X:\{n..(n  +  i  +  0)  +  2\msupminus{}\}  {}\mrightarrow{}  \mBbbR{}.  \mforall{}v:\mBbbR{}.    (rmin(v;X[n  +  (0  +  i)  +  1])  =  rmin(v;X[(n  +  i)  +  1]))


By

---

Latex:
(Auto  THEN  Subst'  (n  +  (0  +  i)  +  1)  =  ((n  +  i)  +  1)  0  THEN  Auto)\mcdot{}

---

Home Index