Step * 1 1 1 1 1 2 1 1 of Lemma Kummer-criterion


1. : ℕ ⟶ ℝ
2. : ℕ ⟶ ℝ
3. {c:ℝr0 < c} 
4. : ℕ
5. ∀n:{N...}. ((r0 < a[n]) ∧ (r0 < x[n]))
6. ∀n:{N...}. ((r0 < a[n]) ∧ (c ≤ ((a[n] x[n]/x[n 1]) a[n 1])))
7. : ℕ+
8. : ℕ+
9. (r1/r(M)) < (c/r(k))
10. N1 : ℕ
11. ∀n:ℕ((N1 ≤ n)  (|(a[n] x[n]) r0| ≤ (r1/r(2 M))))
12. : ℤ
13. imax(N;N1) J ∈ ℤ
14. N ≤ J
15. N1 ≤ J
16. ∀n,m:ℕ.  ((J ≤ n)  (J ≤ m)  (|(a[n] x[n]) a[m] x[m]| < (c/r(k))))
17. {J...}
18. {m...}
⊢ {x[i] 1≤i≤n}| ≤ (r1/r(k))
BY
(InstLemma `rsum_functionality_wrt_rleq` [⌜1⌝;⌜n⌝;⌜x⌝;⌜λ2i.(r1/c) ((a[i 1] x[i 1]) a[i] x[i])⌝]⋅
   THENA Auto
   }

1
.....antecedent..... 
1. : ℕ ⟶ ℝ
2. : ℕ ⟶ ℝ
3. {c:ℝr0 < c} 
4. : ℕ
5. ∀n:{N...}. ((r0 < a[n]) ∧ (r0 < x[n]))
6. ∀n:{N...}. ((r0 < a[n]) ∧ (c ≤ ((a[n] x[n]/x[n 1]) a[n 1])))
7. : ℕ+
8. : ℕ+
9. (r1/r(M)) < (c/r(k))
10. N1 : ℕ
11. ∀n:ℕ((N1 ≤ n)  (|(a[n] x[n]) r0| ≤ (r1/r(2 M))))
12. : ℤ
13. imax(N;N1) J ∈ ℤ
14. N ≤ J
15. N1 ≤ J
16. ∀n,m:ℕ.  ((J ≤ n)  (J ≤ m)  (|(a[n] x[n]) a[m] x[m]| < (c/r(k))))
17. {J...}
18. {m...}
⊢ x[k] ≤ (r1/c) ((a[k 1] x[k 1]) a[k] x[k]) for k ∈ [m 1,n]

2
1. : ℕ ⟶ ℝ
2. : ℕ ⟶ ℝ
3. {c:ℝr0 < c} 
4. : ℕ
5. ∀n:{N...}. ((r0 < a[n]) ∧ (r0 < x[n]))
6. ∀n:{N...}. ((r0 < a[n]) ∧ (c ≤ ((a[n] x[n]/x[n 1]) a[n 1])))
7. : ℕ+
8. : ℕ+
9. (r1/r(M)) < (c/r(k))
10. N1 : ℕ
11. ∀n:ℕ((N1 ≤ n)  (|(a[n] x[n]) r0| ≤ (r1/r(2 M))))
12. : ℤ
13. imax(N;N1) J ∈ ℤ
14. N ≤ J
15. N1 ≤ J
16. ∀n,m:ℕ.  ((J ≤ n)  (J ≤ m)  (|(a[n] x[n]) a[m] x[m]| < (c/r(k))))
17. {J...}
18. {m...}
19. Σ{x[k] 1≤k≤n} ≤ Σ{(r1/c) ((a[k 1] x[k 1]) a[k] x[k]) 1≤k≤n}
⊢ {x[i] 1≤i≤n}| ≤ (r1/r(k))


Latex:


Latex:

1.  a  :  \mBbbN{}  {}\mrightarrow{}  \mBbbR{}
2.  x  :  \mBbbN{}  {}\mrightarrow{}  \mBbbR{}
3.  c  :  \{c:\mBbbR{}|  r0  <  c\} 
4.  N  :  \mBbbN{}
5.  \mforall{}n:\{N...\}.  ((r0  <  a[n])  \mwedge{}  (r0  <  x[n]))
6.  \mforall{}n:\{N...\}.  ((r0  <  a[n])  \mwedge{}  (c  \mleq{}  ((a[n]  *  x[n]/x[n  +  1])  -  a[n  +  1])))
7.  k  :  \mBbbN{}\msupplus{}
8.  M  :  \mBbbN{}\msupplus{}
9.  (r1/r(M))  <  (c/r(k))
10.  N1  :  \mBbbN{}
11.  \mforall{}n:\mBbbN{}.  ((N1  \mleq{}  n)  {}\mRightarrow{}  (|(a[n]  *  x[n])  -  r0|  \mleq{}  (r1/r(2  *  M))))
12.  J  :  \mBbbZ{}
13.  imax(N;N1)  =  J
14.  N  \mleq{}  J
15.  N1  \mleq{}  J
16.  \mforall{}n,m:\mBbbN{}.    ((J  \mleq{}  n)  {}\mRightarrow{}  (J  \mleq{}  m)  {}\mRightarrow{}  (|(a[n]  *  x[n])  -  a[m]  *  x[m]|  <  (c/r(k))))
17.  m  :  \{J...\}
18.  n  :  \{m...\}
\mvdash{}  |\mSigma{}\{x[i]  |  m  +  1\mleq{}i\mleq{}n\}|  \mleq{}  (r1/r(k))


By


Latex:
(InstLemma  `rsum\_functionality\_wrt\_rleq`  [\mkleeneopen{}m  +  1\mkleeneclose{};\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}i.(r1/c)
                                                                                                                      *  ((a[i  -  1]  *  x[i  -  1])  -  a[i]  *  x[i])\mkleeneclose{}]
  \mcdot{}
  THENA  Auto
  )




Home Index