---

Step * 1 1 of Lemma qsum_functionality_wrt_qle


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])
BY
{ xxx((Subst' (n + k) - 1 ~ n + (k - 1) 0 THEN Auto) THEN (InstHyp [⌜x⌝;⌜y⌝] 4⋅ THENA Auto))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
9. Σn ≤ k < n + (k - 1). x[k] ≤ Σn ≤ k < n + (k - 1). y[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.  k  :  \mBbbZ{}
3.  0  <  k
4.  \mforall{}x,y:\{n..(n  +  (k  -  1))  +  1\msupminus{}\}  {}\mrightarrow{}  \mBbbQ{}.
          ((\mforall{}k@0:\mBbbZ{}.  ((n  \mleq{}  k@0)  {}\mRightarrow{}  (k@0  \mleq{}  (n  +  (k  -  1)))  {}\mRightarrow{}  (x[k@0]  \mleq{}  y[k@0])))
          {}\mRightarrow{}  (\mSigma{}n  \mleq{}  k  <  n  +  (k  -  1).  x[k]  \mleq{}  \mSigma{}n  \mleq{}  k  <  n  +  (k  -  1).  y[k]))
5.  x  :  \{n..(n  +  k)  +  1\msupminus{}\}  {}\mrightarrow{}  \mBbbQ{}
6.  y  :  \{n..(n  +  k)  +  1\msupminus{}\}  {}\mrightarrow{}  \mBbbQ{}
7.  \mforall{}k@0:\mBbbZ{}.  ((n  \mleq{}  k@0)  {}\mRightarrow{}  (k@0  \mleq{}  (n  +  k))  {}\mRightarrow{}  (x[k@0]  \mleq{}  y[k@0]))
8.  n  <  n  +  k
\mvdash{}  (\mSigma{}n  \mleq{}  k  <  (n  +  k)  -  1.  x[k]  +  x[(n  +  k)  -  1])  \mleq{}  (\mSigma{}n  \mleq{}  k  <  (n  +  k)  -  1.  y[k]  +  y[(n  +  k)  -  1])


By

---

Latex:
xxx((Subst'  (n  +  k)  -  1  \msim{}  n  +  (k  -  1)  0  THEN  Auto)  THEN  (InstHyp  [\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{}]  4\mcdot{}  THENA  Auto))xxx

---

Home Index