---

Step * 1 of Lemma rprod-of-negative


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))
BY
{ ((RWO  "rprod-rminus" (-1) THENA Auto)
   THEN MoveToConcl (-1)
   THEN (GenConclTerm ⌜rprod(n;m;k.x[k])⌝⋅ THENA Auto)
   THEN (GenConcl ⌜(m - n) = N ∈ ℕ⌝⋅ THENA Auto)
   THEN (RWO  "rnexp-add<" 0 THENA Auto)
   THEN (RWO  "rnexp1" 0 THENA Auto)
   THEN (RWO "rnexp-minus-one" 0 THENA Auto)) }

1
1. n : ℤ
2. m : ℤ
3. x : {n..m + 1-} ⟶ ℝ
4. [%] : (∀k:{n..m + 1-}. (x[k] < r0)) ∧ (n ≤ m)
5. v : ℝ
6. rprod(n;m;k.x[k]) = v ∈ ℝ
7. N : ℕ
8. (m - n) = N ∈ ℕ
⊢ (r0 < ((if (N rem 2 =z 0) then r1 else r(-1) fi  * r(-1)) * v))
⇒ ((((N rem 2) = 1 ∈ ℤ) ⇒ (r0 < v)) ∧ (((N rem 2) = 0 ∈ ℤ) ⇒ (v < r0)))

---

Latex:

---

Latex:

1.  n  :  \mBbbZ{}
2.  m  :  \mBbbZ{}
3.  x  :  \{n..m  +  1\msupminus{}\}  {}\mrightarrow{}  \mBbbR{}
4.  [\%]  :  (\mforall{}k:\{n..m  +  1\msupminus{}\}.  (x[k]  <  r0))  \mwedge{}  (n  \mleq{}  m)
5.  r0  <  rprod(n;m;k.-(x[k]))
\mvdash{}  (((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))


By

---

Latex:
((RWO    "rprod-rminus"  (-1)  THENA  Auto)
  THEN  MoveToConcl  (-1)
  THEN  (GenConclTerm  \mkleeneopen{}rprod(n;m;k.x[k])\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (GenConcl  \mkleeneopen{}(m  -  n)  =  N\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (RWO    "rnexp-add<"  0  THENA  Auto)
  THEN  (RWO    "rnexp1"  0  THENA  Auto)
  THEN  (RWO  "rnexp-minus-one"  0  THENA  Auto))

---

Home Index