---

Step * of Lemma rprod-of-positive

∀n,m:ℤ. ∀x:{n..m + 1-} ⟶ ℝ.  r0 < rprod(n;m;k.x[k]) supposing ∀k:{n..m + 1-}. (r0 < x[k])
BY
{ (Auto
   THEN (Assert ∀d:ℕ. (((n + d) ≤ m) ⇒ (r0 < rprod(n;n + d;k.x[k]))) BY
               ((InductionOnNat THEN Auto)
                THEN Unhide
                THEN Auto
                THEN Unfold `rprod` 0
                THEN AutoSplit
                THEN (BLemma `rmul-is-positive` THENM OrLeft)
                THEN Auto
                THEN ((Subst' (n + d) - 1 ~ n + (d - 1) 0 THEN Auto) ORELSE (Unfold `rprod` 0 THEN AutoSplit))))
   ) }

1
1. n : ℤ
2. m : ℤ
3. x : {n..m + 1-} ⟶ ℝ
4. [%] : ∀k:{n..m + 1-}. (r0 < x[k])
5. ∀d:ℕ. (((n + d) ≤ m) ⇒ (r0 < rprod(n;n + d;k.x[k])))
⊢ r0 < rprod(n;m;k.x[k])

---

Latex:

---

Latex:
\mforall{}n,m:\mBbbZ{}.  \mforall{}x:\{n..m  +  1\msupminus{}\}  {}\mrightarrow{}  \mBbbR{}.    r0  <  rprod(n;m;k.x[k])  supposing  \mforall{}k:\{n..m  +  1\msupminus{}\}.  (r0  <  x[k])


By

---

Latex:
(Auto
  THEN  (Assert  \mforall{}d:\mBbbN{}.  (((n  +  d)  \mleq{}  m)  {}\mRightarrow{}  (r0  <  rprod(n;n  +  d;k.x[k])))  BY
                          ((InductionOnNat  THEN  Auto)
                            THEN  Unhide
                            THEN  Auto
                            THEN  Unfold  `rprod`  0
                            THEN  AutoSplit
                            THEN  (BLemma  `rmul-is-positive`  THENM  OrLeft)
                            THEN  Auto
                            THEN  ((Subst'  (n  +  d)  -  1  \msim{}  n  +  (d  -  1)  0  THEN  Auto)
                            ORELSE  (Unfold  `rprod`  0  THEN  AutoSplit)
                            )))
  )

---

Home Index