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 (MoveToConcl (-1))
   THEN OldAutoBoolCase ⌜m <n⌝⋅
   THEN Try ((Auto THEN RWO "qsum_unroll" THEN CompleteAuto))) }

1
1. : ℤ
2. : ℤ
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