---

Step * of Lemma rprod-split

∀[n,m:ℤ]. ∀[x:{n..m + 1-} ⟶ ℝ]. ∀[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))
BY
{ Assert ⌜∀d:ℕ
            ∀[n:ℤ]. ∀[x:{n..(n + d) + 1-} ⟶ ℝ]. ∀[i:ℤ].
              rprod(n;n + d;k.x[k]) = (rprod(n;i;k.x[k]) * rprod(i + 1;n + d;k.x[k])) 
              supposing (i ≤ (n + d)) ∧ (n ≤ (i + 1))⌝⋅ }

1
.....assertion..... 
∀d:ℕ
  ∀[n:ℤ]. ∀[x:{n..(n + d) + 1-} ⟶ ℝ]. ∀[i:ℤ].
    rprod(n;n + d;k.x[k]) = (rprod(n;i;k.x[k]) * rprod(i + 1;n + d;k.x[k])) supposing (i ≤ (n + d)) ∧ (n ≤ (i + 1))

2
1. ∀d:ℕ
     ∀[n:ℤ]. ∀[x:{n..(n + d) + 1-} ⟶ ℝ]. ∀[i:ℤ].
       rprod(n;n + d;k.x[k]) = (rprod(n;i;k.x[k]) * rprod(i + 1;n + d;k.x[k])) supposing (i ≤ (n + d)) ∧ (n ≤ (i + 1))
⊢ ∀[n,m:ℤ]. ∀[x:{n..m + 1-} ⟶ ℝ]. ∀[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))

---

Latex:

---

Latex:
\mforall{}[n,m:\mBbbZ{}].  \mforall{}[x:\{n..m  +  1\msupminus{}\}  {}\mrightarrow{}  \mBbbR{}].  \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))


By

---

Latex:
Assert  \mkleeneopen{}\mforall{}d:\mBbbN{}
                    \mforall{}[n:\mBbbZ{}].  \mforall{}[x:\{n..(n  +  d)  +  1\msupminus{}\}  {}\mrightarrow{}  \mBbbR{}].  \mforall{}[i:\mBbbZ{}].
                        rprod(n;n  +  d;k.x[k])  =  (rprod(n;i;k.x[k])  *  rprod(i  +  1;n  +  d;k.x[k])) 
                        supposing  (i  \mleq{}  (n  +  d))  \mwedge{}  (n  \mleq{}  (i  +  1))\mkleeneclose{}\mcdot{}

---

Home Index