---

Step * 2 1 of Lemma rminimum-positive


1. n : ℤ
2. d : ℤ
3. [%1] : 0 < d
4. ∀x:{n..(n + (d - 1)) + 1-} ⟶ ℝ
     ((∀i:{n..(n + (d - 1)) + 1-}. (r0 < (x i))) ⇒ (r0 < primrec(d - 1;x n;λi,s. rmin(s;x (n + i + 1)))))
5. x : {n..(n + d) + 1-} ⟶ ℝ
6. ∀i:{n..(n + d) + 1-}. (r0 < (x i))
⊢ r0 < rmin(primrec(d - 1;x n;λi,s. rmin(s;x (n + i + 1)));x (n + (d - 1) + 1))
BY
{ (BLemma `rmin_strict_ub` THEN Auto) }

---

Latex:

---

Latex:

1.  n  :  \mBbbZ{}
2.  d  :  \mBbbZ{}
3.  [\%1]  :  0  <  d
4.  \mforall{}x:\{n..(n  +  (d  -  1))  +  1\msupminus{}\}  {}\mrightarrow{}  \mBbbR{}
          ((\mforall{}i:\{n..(n  +  (d  -  1))  +  1\msupminus{}\}.  (r0  <  (x  i)))
          {}\mRightarrow{}  (r0  <  primrec(d  -  1;x  n;\mlambda{}i,s.  rmin(s;x  (n  +  i  +  1)))))
5.  x  :  \{n..(n  +  d)  +  1\msupminus{}\}  {}\mrightarrow{}  \mBbbR{}
6.  \mforall{}i:\{n..(n  +  d)  +  1\msupminus{}\}.  (r0  <  (x  i))
\mvdash{}  r0  <  rmin(primrec(d  -  1;x  n;\mlambda{}i,s.  rmin(s;x  (n  +  i  +  1)));x  (n  +  (d  -  1)  +  1))


By

---

Latex:
(BLemma  `rmin\_strict\_ub`  THEN  Auto)

---

Home Index