src/HOL/Transcendental.thy
changeset 59865 8a20dd967385
parent 59862 44b3f4fa33ca
child 59867 58043346ca64
     1.1 --- a/src/HOL/Transcendental.thy	Tue Mar 31 15:01:06 2015 +0100
     1.2 +++ b/src/HOL/Transcendental.thy	Tue Mar 31 16:48:48 2015 +0100
     1.3 @@ -4542,16 +4542,6 @@
     1.4    (is "summable (?c x)")
     1.5    by (rule summable_Leibniz(1), rule zeroseq_arctan_series[OF assms], rule monoseq_arctan_series[OF assms])
     1.6  
     1.7 -lemma less_one_imp_sqr_less_one:
     1.8 -  fixes x :: real
     1.9 -  assumes "\<bar>x\<bar> < 1"
    1.10 -  shows "x\<^sup>2 < 1"
    1.11 -proof -
    1.12 -  have "\<bar>x\<^sup>2\<bar> < 1"
    1.13 -    by (metis abs_power2 assms pos2 power2_abs power_0 power_strict_decreasing zero_eq_power2 zero_less_abs_iff)
    1.14 -  thus ?thesis using zero_le_power2 by auto
    1.15 -qed
    1.16 -
    1.17  lemma DERIV_arctan_series:
    1.18    assumes "\<bar> x \<bar> < 1"
    1.19    shows "DERIV (\<lambda> x'. \<Sum> k. (-1)^k * (1 / real (k*2+1) * x' ^ (k*2+1))) x :> (\<Sum> k. (-1)^k * x^(k*2))"
    1.20 @@ -4568,7 +4558,7 @@
    1.21    {
    1.22      fix x :: real
    1.23      assume "\<bar>x\<bar> < 1"
    1.24 -    hence "x\<^sup>2 < 1" by (rule less_one_imp_sqr_less_one)
    1.25 +    hence "x\<^sup>2 < 1" by (simp add: abs_square_less_1)
    1.26      have "summable (\<lambda> n. (- 1) ^ n * (x\<^sup>2) ^n)"
    1.27        by (rule summable_Leibniz(1), auto intro!: LIMSEQ_realpow_zero monoseq_realpow `x\<^sup>2 < 1` order_less_imp_le[OF `x\<^sup>2 < 1`])
    1.28      hence "summable (\<lambda> n. (- 1) ^ n * x^(2*n))" unfolding power_mult .
    1.29 @@ -4676,7 +4666,7 @@
    1.30              hence "\<bar>x\<bar> < r" by auto
    1.31              hence "\<bar>x\<bar> < 1" using `r < 1` by auto
    1.32              have "\<bar> - (x\<^sup>2) \<bar> < 1"
    1.33 -              using less_one_imp_sqr_less_one[OF `\<bar>x\<bar> < 1`] by auto
    1.34 +              using abs_square_less_1 `\<bar>x\<bar> < 1` by auto
    1.35              hence "(\<lambda> n. (- (x\<^sup>2)) ^ n) sums (1 / (1 - (- (x\<^sup>2))))"
    1.36                unfolding real_norm_def[symmetric] by (rule geometric_sums)
    1.37              hence "(?c' x) sums (1 / (1 - (- (x\<^sup>2))))"