src/HOL/Analysis/Complex_Transcendental.thy
changeset 66827 c94531b5007d
parent 66793 deabce3ccf1f
child 67135 1a94352812f4
     1.1 --- a/src/HOL/Analysis/Complex_Transcendental.thy	Tue Oct 10 14:03:51 2017 +0100
     1.2 +++ b/src/HOL/Analysis/Complex_Transcendental.thy	Tue Oct 10 17:15:37 2017 +0100
     1.3 @@ -2102,7 +2102,7 @@
     1.4    have "(\<lambda>n. ln(1 + 1/n) / ln n) \<longlonglongrightarrow> 0"
     1.5    proof (rule Lim_transform_bound)
     1.6      show "(inverse o real) \<longlonglongrightarrow> 0"
     1.7 -      by (metis comp_def seq_harmonic tendsto_explicit)
     1.8 +      by (metis comp_def lim_inverse_n tendsto_explicit)
     1.9      show "\<forall>\<^sub>F n in sequentially. norm (ln (1 + 1 / n) / ln n) \<le> norm ((inverse \<circ> real) n)"
    1.10      proof
    1.11        fix n::nat