src/HOL/Analysis/Infinite_Products.thy
changeset 68517 6b5f15387353
parent 68452 c027dfbfad30
child 68527 2f4e2aab190a
     1.1 --- a/src/HOL/Analysis/Infinite_Products.thy	Tue Jun 26 19:29:14 2018 +0200
     1.2 +++ b/src/HOL/Analysis/Infinite_Products.thy	Tue Jun 26 20:48:49 2018 +0100
     1.3 @@ -1418,14 +1418,16 @@
     1.4    assumes ge0:"\<And>n. f n \<ge> 0" and ac: "abs_convergent_prod (\<lambda>n. exp (f n))"
     1.5    shows "prodinf (\<lambda>i. exp (f i)) = exp (suminf f)"
     1.6  proof -
     1.7 -  have "summable f" 
     1.8 +  have "summable f"
     1.9      using ac unfolding abs_convergent_prod_conv_summable
    1.10    proof (elim summable_comparison_test')
    1.11      fix n
    1.12 -    show "norm (f n) \<le> norm (exp (f n) - 1)" 
    1.13 -      using ge0[of n] 
    1.14 -      by (metis abs_of_nonneg add.commute diff_add_cancel diff_ge_0_iff_ge exp_ge_add_one_self 
    1.15 -          exp_le_cancel_iff one_le_exp_iff real_norm_def)
    1.16 +    have "\<bar>f n\<bar> = f n"
    1.17 +      by (simp add: ge0)
    1.18 +    also have "\<dots> \<le> exp (f n) - 1"
    1.19 +      by (metis diff_diff_add exp_ge_add_one_self ge_iff_diff_ge_0)
    1.20 +    finally show "norm (f n) \<le> norm (exp (f n) - 1)"
    1.21 +      by simp
    1.22    qed
    1.23    then show ?thesis
    1.24      by (simp add: prodinf_exp)