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