---

Step * of Lemma rprod-rminus

∀n,m:ℤ. ∀x:{n..m + 1-} ⟶ ℝ.  rprod(n;m;k.-(x[k])) = (r(-1)^(m - n) + 1 * rprod(n;m;k.x[k])) supposing n ≤ m
BY
{ (Intros
   THEN ((Assert ∀d:ℕ. (((n + d) ≤ m) ⇒ (rprod(n;n + d;k.-(x[k])) = (r(-1)^d + 1 * rprod(n;n + d;k.x[k])))) BY
                InductionOnNat)
        THENM (InstHyp [⌜m - n⌝] (-1)⋅ THEN Auto THEN Subst' n + (m - n) ~ m -1 THEN Auto)
        )
   ) }

1
.....aux..... 
1. n : ℤ
2. m : ℤ
3. x : {n..m + 1-} ⟶ ℝ
4. n ≤ m
5. d : ℤ
⊢ ((n + 0) ≤ m) ⇒ (rprod(n;n + 0;k.-(x[k])) = (r(-1)^0 + 1 * rprod(n;n + 0;k.x[k])))

2
.....aux..... 
1. n : ℤ
2. m : ℤ
3. x : {n..m + 1-} ⟶ ℝ
4. n ≤ m
5. d : ℤ
6. 0 < d
7. ((n + (d - 1)) ≤ m) ⇒ (rprod(n;n + (d - 1);k.-(x[k])) = (r(-1)^(d - 1) + 1 * rprod(n;n + (d - 1);k.x[k])))
⊢ ((n + d) ≤ m) ⇒ (rprod(n;n + d;k.-(x[k])) = (r(-1)^d + 1 * rprod(n;n + d;k.x[k])))

---

Latex:

---

Latex:
\mforall{}n,m:\mBbbZ{}.  \mforall{}x:\{n..m  +  1\msupminus{}\}  {}\mrightarrow{}  \mBbbR{}.
    rprod(n;m;k.-(x[k]))  =  (r(-1)\^{}(m  -  n)  +  1  *  rprod(n;m;k.x[k]))  supposing  n  \mleq{}  m


By

---

Latex:
(Intros
  THEN  ((Assert  \mforall{}d:\mBbbN{}
                                  (((n  +  d)  \mleq{}  m)
                                  {}\mRightarrow{}  (rprod(n;n  +  d;k.-(x[k]))  =  (r(-1)\^{}d  +  1  *  rprod(n;n  +  d;k.x[k]))))  BY
                            InductionOnNat)
            THENM  (InstHyp  [\mkleeneopen{}m  -  n\mkleeneclose{}]  (-1)\mcdot{}  THEN  Auto  THEN  Subst'  n  +  (m  -  n)  \msim{}  m  -1  THEN  Auto)
            )
  )

---

Home Index