---

Step * 1 1 of Lemma rminimum-cases


1. n : ℤ
2. d : ℤ
⊢ ∀x:{n..(n + 0) + 1-} ⟶ ℝ. (¬¬(∃a:{n..(n + 0) + 1-}. ((x[n] = x[a]) ∧ (∀j:{n..(n + 0) + 1-}. (x[a] ≤ x[j])))))
BY
{ (Auto⋅ THEN (RemoveDoubleNegation THENA Auto) THEN InstConcl [⌜n⌝]⋅ THEN Auto THEN Subst' j ~ n 0 THEN Auto) }

---

Latex:

---

Latex:

1.  n  :  \mBbbZ{}
2.  d  :  \mBbbZ{}
\mvdash{}  \mforall{}x:\{n..(n  +  0)  +  1\msupminus{}\}  {}\mrightarrow{}  \mBbbR{}
        (\mneg{}\mneg{}(\mexists{}a:\{n..(n  +  0)  +  1\msupminus{}\}.  ((x[n]  =  x[a])  \mwedge{}  (\mforall{}j:\{n..(n  +  0)  +  1\msupminus{}\}.  (x[a]  \mleq{}  x[j])))))


By

---

Latex:
(Auto\mcdot{}
  THEN  (RemoveDoubleNegation  THENA  Auto)
  THEN  InstConcl  [\mkleeneopen{}n\mkleeneclose{}]\mcdot{}
  THEN  Auto
  THEN  Subst'  j  \msim{}  n  0
  THEN  Auto)

---

Home Index