---

Step * 1 of Lemma qsum_functionality_wrt_qle


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]))
BY
{ xxx((GenConcl ⌜(m - n) = k ∈ ℕ⌝⋅ THENA Auto')
      THEN (Subst ⌜m ~ n + k⌝ 0⋅ THENA Auto')
      THEN ThinVar `m'
      THEN NatInd (-1)
      THEN (Auto THEN (RWO "qsum_unroll" 0 THENA Auto) THEN AutoSplit)⋅)xxx }

1
1. n : ℤ
2. k : ℤ
3. 0 < k
4. ∀x,y:{n..(n + (k - 1)) + 1-} ⟶ ℚ.
     ((∀k@0:ℤ. ((n ≤ k@0) ⇒ (k@0 ≤ (n + (k - 1))) ⇒ (x[k@0] ≤ y[k@0])))
     ⇒ (Σn ≤ k < n + (k - 1). x[k] ≤ Σn ≤ k < n + (k - 1). y[k]))
5. x : {n..(n + k) + 1-} ⟶ ℚ
6. y : {n..(n + k) + 1-} ⟶ ℚ
7. ∀k@0:ℤ. ((n ≤ k@0) ⇒ (k@0 ≤ (n + k)) ⇒ (x[k@0] ≤ y[k@0]))
8. n < n + k
⊢ (Σn ≤ k < (n + k) - 1. x[k] + x[(n + k) - 1]) ≤ (Σn ≤ k < (n + k) - 1. y[k] + y[(n + k) - 1])

---

Latex:

---

Latex:

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


By

---

Latex:
xxx((GenConcl  \mkleeneopen{}(m  -  n)  =  k\mkleeneclose{}\mcdot{}  THENA  Auto')
        THEN  (Subst  \mkleeneopen{}m  \msim{}  n  +  k\mkleeneclose{}  0\mcdot{}  THENA  Auto')
        THEN  ThinVar  `m'
        THEN  NatInd  (-1)
        THEN  (Auto  THEN  (RWO  "qsum\_unroll"  0  THENA  Auto)  THEN  AutoSplit)\mcdot{})xxx

---

Home Index