---

Step * 2 of Lemma rprod-split


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))
BY
{ (Auto
   THEN ((Decide ⌜n ≤ m⌝⋅ THENA Auto)
         THENL [((InstHyp [⌜m - n⌝;⌜n⌝] 1⋅ THENA Auto)
                 THEN (Subst' n + (m - n) ~ m -1 THENA Auto)
                 THEN BHyp -1
                 THEN Auto)
               ; (RWO "rprod-empty" 0 THEN Auto)]
        )
   ) }

---

Latex:

---

Latex:

1.  \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))
\mvdash{}  \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:
(Auto
  THEN  ((Decide  \mkleeneopen{}n  \mleq{}  m\mkleeneclose{}\mcdot{}  THENA  Auto)
              THENL  [((InstHyp  [\mkleeneopen{}m  -  n\mkleeneclose{};\mkleeneopen{}n\mkleeneclose{}]  1\mcdot{}  THENA  Auto)
                              THEN  (Subst'  n  +  (m  -  n)  \msim{}  m  -1  THENA  Auto)
                              THEN  BHyp  -1
                              THEN  Auto)
                          ;  (RWO  "rprod-empty"  0  THEN  Auto)]
            )
  )

---

Home Index