Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/ex/HarmonicSeries.thy
changeset 72221 98ef41a82b73
parent 70113 c8deb8ba6d05 
--- a/src/HOL/ex/HarmonicSeries.thy	Thu Aug 27 15:23:48 2020 +0100
+++ b/src/HOL/ex/HarmonicSeries.thy	Thu Aug 27 16:48:21 2020 +0100
@@ -280,8 +280,8 @@
   then obtain n::nat where ndef: "n = nat \<lceil>2 * ?s\<rceil>" by simp
   then have ngt: "1 + real n/2 > ?s" by linarith
   define j where "j = (2::nat)^n"
-  have "\<forall>m\<ge>j. 0 < ?f m" by simp
-  with sf have "(\<Sum>i<j. ?f i) < ?s" by (rule sum_less_suminf)
+  have "(\<Sum>i<j. ?f i) < ?s" 
+    using sf by (simp add: sum_less_suminf)
   then have "(\<Sum>i\<in>{Suc 0..<Suc j}. 1/(real i)) < ?s"
     unfolding sum.shift_bounds_Suc_ivl by (simp add: atLeast0LessThan)
   with j_def have
isabelle