---

Step * 1 of Lemma rprod-is-zero


1. n : ℤ
2. m : ℤ
3. x : {n..m + 1-} ⟶ ℝ
4. ∀[i:ℤ]. rprod(n;m;k.x[k]) = (rprod(n;i;k.x[k]) * rprod(i + 1;m;k.x[k])) supposing (i ≤ m) ∧ (n ≤ (i + 1))
5. k : {n..m + 1-}
6. x[k] = r0
7. rprod(n;m;k.x[k]) = (rprod(n;k;k.x[k]) * rprod(k + 1;m;k.x[k]))
⊢ (rprod(n;k;k.x[k]) * rprod(k + 1;m;k.x[k])) = r0
BY
{ ((RW  (AddrC [1;1] (LemmaC `rprod-split-last`)) 0 THENA Auto) THEN RWO "-2" 0 THEN Auto) }

---

Latex:

---

Latex:

1.  n  :  \mBbbZ{}
2.  m  :  \mBbbZ{}
3.  x  :  \{n..m  +  1\msupminus{}\}  {}\mrightarrow{}  \mBbbR{}
4.  \mforall{}[i:\mBbbZ{}]
          rprod(n;m;k.x[k])  =  (rprod(n;i;k.x[k])  *  rprod(i  +  1;m;k.x[k])) 
          supposing  (i  \mleq{}  m)  \mwedge{}  (n  \mleq{}  (i  +  1))
5.  k  :  \{n..m  +  1\msupminus{}\}
6.  x[k]  =  r0
7.  rprod(n;m;k.x[k])  =  (rprod(n;k;k.x[k])  *  rprod(k  +  1;m;k.x[k]))
\mvdash{}  (rprod(n;k;k.x[k])  *  rprod(k  +  1;m;k.x[k]))  =  r0


By

---

Latex:
((RW    (AddrC  [1;1]  (LemmaC  `rprod-split-last`))  0  THENA  Auto)  THEN  RWO  "-2"  0  THEN  Auto)

---

Home Index