---

Step * 1 of Lemma rprod-of-positive


1. n : ℤ
2. m : ℤ
3. x : {n..m + 1-} ⟶ ℝ
4. [%] : ∀k:{n..m + 1-}. (r0 < x[k])
5. ∀d:ℕ. (((n + d) ≤ m) ⇒ (r0 < rprod(n;n + d;k.x[k])))
⊢ r0 < rprod(n;m;k.x[k])
BY
{ ((Decide ⌜n ≤ m⌝⋅ THENA Auto) THENL [(InstHyp [⌜m - n⌝] (-2)⋅ THEN Auto); (Unfold `rprod` 0 THEN AutoSplit)]) }

---

Latex:

---

Latex:

1.  n  :  \mBbbZ{}
2.  m  :  \mBbbZ{}
3.  x  :  \{n..m  +  1\msupminus{}\}  {}\mrightarrow{}  \mBbbR{}
4.  [\%]  :  \mforall{}k:\{n..m  +  1\msupminus{}\}.  (r0  <  x[k])
5.  \mforall{}d:\mBbbN{}.  (((n  +  d)  \mleq{}  m)  {}\mRightarrow{}  (r0  <  rprod(n;n  +  d;k.x[k])))
\mvdash{}  r0  <  rprod(n;m;k.x[k])


By

---

Latex:
((Decide  \mkleeneopen{}n  \mleq{}  m\mkleeneclose{}\mcdot{}  THENA  Auto)
  THENL  [(InstHyp  [\mkleeneopen{}m  -  n\mkleeneclose{}]  (-2)\mcdot{}  THEN  Auto);  (Unfold  `rprod`  0  THEN  AutoSplit)]
)

---

Home Index