# HG changeset patch
# User huffman
# Date 1159063203 -7200
# Node ID 4950e45442b8907ce071f65301f0bbcb17594bb9
# Parent  690d866a165d92ca6edb9f43bb205d6daf3a65d5
add proof of summable_LIMSEQ_zero

diff -r 690d866a165d -r 4950e45442b8 src/HOL/Hyperreal/Series.thy
--- a/src/HOL/Hyperreal/Series.thy	Sun Sep 24 03:38:36 2006 +0200
+++ b/src/HOL/Hyperreal/Series.thy	Sun Sep 24 04:00:03 2006 +0200
@@ -337,6 +337,16 @@
  "summable f = convergent (%n. setsum f {0..<n})"
 by (simp add: summable_def sums_def convergent_def)
 
+lemma summable_LIMSEQ_zero: "summable f \<Longrightarrow> f ----> 0"
+apply (drule summable_convergent_sumr_iff [THEN iffD1])
+apply (drule Cauchy_convergent_iff [THEN iffD2])
+apply (simp only: Cauchy_def LIMSEQ_def, safe)
+apply (drule_tac x="r" in spec, safe)
+apply (rule_tac x="M" in exI, safe)
+apply (drule_tac x="Suc n" in spec, simp)
+apply (drule_tac x="n" in spec, simp)
+done
+
 lemma summable_Cauchy:
      "summable f =  
       (\<forall>e > 0. \<exists>N. \<forall>m \<ge> N. \<forall>n. abs(setsum f {m..<n}) < e)"