---

Step * 1 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. 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)))
BY
{ ((InstLemma `rem_bounds_1` [⌜N⌝;⌜2⌝]⋅ THENA Auto)
   THEN (GenConcl ⌜(N rem 2) = a ∈ ℕ2⌝⋅ THENA Auto)
   THEN Thin (-1)
   THEN IntSegCases (-1)
   THEN Reduce 0
   THEN Auto) }

---

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.  v  :  \mBbbR{}
6.  rprod(n;m;k.x[k])  =  v
7.  N  :  \mBbbN{}
8.  (m  -  n)  =  N
\mvdash{}  (r0  <  ((if  (N  rem  2  =\msubz{}  0)  then  r1  else  r(-1)  fi    *  r(-1))  *  v))
{}\mRightarrow{}  ((((N  rem  2)  =  1)  {}\mRightarrow{}  (r0  <  v))  \mwedge{}  (((N  rem  2)  =  0)  {}\mRightarrow{}  (v  <  r0)))


By

---

Latex:
((InstLemma  `rem\_bounds\_1`  [\mkleeneopen{}N\mkleeneclose{};\mkleeneopen{}2\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (GenConcl  \mkleeneopen{}(N  rem  2)  =  a\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  Thin  (-1)
  THEN  IntSegCases  (-1)
  THEN  Reduce  0
  THEN  Auto)

---

Home Index