---

Step * of Lemma rprod-of-negative

∀n,m:ℤ. ∀x:{n..m + 1-} ⟶ ℝ.
  (((m - n rem 2) = 1 ∈ ℤ) ⇒ (r0 < rprod(n;m;k.x[k]))) ∧ (((m - n rem 2) = 0 ∈ ℤ) ⇒ (rprod(n;m;k.x[k]) < r0)) 
  supposing (∀k:{n..m + 1-}. (x[k] < r0)) ∧ (n ≤ m)
BY
{ (Intros
   THEN (InstLemma `rprod-of-positive` [⌜n⌝;⌜m⌝;⌜λ2k.-(x[k])⌝]⋅
         THENA (Auto THEN (Assert x[k] < r0 BY Auto) THEN nRMul ⌜r(-1)⌝ 0⋅ THEN Auto)
         )
   ) }

1
1. n : ℤ
2. m : ℤ
3. x : {n..m + 1-} ⟶ ℝ
4. [%] : (∀k:{n..m + 1-}. (x[k] < r0)) ∧ (n ≤ m)
5. r0 < rprod(n;m;k.-(x[k]))
⊢ (((m - n rem 2) = 1 ∈ ℤ) ⇒ (r0 < rprod(n;m;k.x[k]))) ∧ (((m - n rem 2) = 0 ∈ ℤ) ⇒ (rprod(n;m;k.x[k]) < r0))

---

Latex:

---

Latex:
\mforall{}n,m:\mBbbZ{}.  \mforall{}x:\{n..m  +  1\msupminus{}\}  {}\mrightarrow{}  \mBbbR{}.
    (((m  -  n  rem  2)  =  1)  {}\mRightarrow{}  (r0  <  rprod(n;m;k.x[k])))
    \mwedge{}  (((m  -  n  rem  2)  =  0)  {}\mRightarrow{}  (rprod(n;m;k.x[k])  <  r0)) 
    supposing  (\mforall{}k:\{n..m  +  1\msupminus{}\}.  (x[k]  <  r0))  \mwedge{}  (n  \mleq{}  m)


By

---

Latex:
(Intros
  THEN  (InstLemma  `rprod-of-positive`  [\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}m\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}k.-(x[k])\mkleeneclose{}]\mcdot{}
              THENA  (Auto  THEN  (Assert  x[k]  <  r0  BY  Auto)  THEN  nRMul  \mkleeneopen{}r(-1)\mkleeneclose{}  0\mcdot{}  THEN  Auto)
              )
  )

---

Home Index