---

Step * of Lemma qsum_functionality_wrt_qle

∀[n,m:ℤ]. ∀[x,y:{n..m + 1-} ⟶ ℚ].
  Σn ≤ k < m. x[k] ≤ Σn ≤ k < m. y[k] supposing ∀k:ℤ. ((n ≤ k) ⇒ (k ≤ m) ⇒ (x[k] ≤ y[k]))
BY
{ (Auto
   THEN RepeatFor 3 (MoveToConcl (-1))
   THEN OldAutoBoolCase ⌜m <z n⌝⋅
   THEN Try ((Auto THEN RWO "qsum_unroll" 0 THEN CompleteAuto))) }

1
1. n : ℤ
2. m : ℤ
3. n ≤ m
⊢ ∀x,y:{n..m + 1-} ⟶ ℚ.  ((∀k:ℤ. ((n ≤ k) ⇒ (k ≤ m) ⇒ (x[k] ≤ y[k]))) ⇒ (Σn ≤ k < m. x[k] ≤ Σn ≤ k < m. y[k]))

---

Latex:

---

Latex:
\mforall{}[n,m:\mBbbZ{}].  \mforall{}[x,y:\{n..m  +  1\msupminus{}\}  {}\mrightarrow{}  \mBbbQ{}].
    \mSigma{}n  \mleq{}  k  <  m.  x[k]  \mleq{}  \mSigma{}n  \mleq{}  k  <  m.  y[k]  supposing  \mforall{}k:\mBbbZ{}.  ((n  \mleq{}  k)  {}\mRightarrow{}  (k  \mleq{}  m)  {}\mRightarrow{}  (x[k]  \mleq{}  y[k]))


By

---

Latex:
(Auto
  THEN  RepeatFor  3  (MoveToConcl  (-1))
  THEN  OldAutoBoolCase  \mkleeneopen{}m  <z  n\mkleeneclose{}\mcdot{}
  THEN  Try  ((Auto  THEN  RWO  "qsum\_unroll"  0  THEN  CompleteAuto)))

---

Home Index