---

Step * 1 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
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)])
BY
{ (RWO "-1" 0 THEN Auto) }

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). y[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
9.  \mSigma{}n  \mleq{}  k  <  n  +  (k  -  1).  x[k]  \mleq{}  \mSigma{}n  \mleq{}  k  <  n  +  (k  -  1).  y[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:
(RWO  "-1"  0  THEN  Auto)

---

Home Index