src/HOL/Transcendental.thy
changeset 35038 a1d93ce94235
parent 35028 108662d50512
child 35213 b9866ad4e3be
equal deleted inserted replaced
35037:748f0bc3f7ca 35038:a1d93ce94235
  2902     proof (cases "x = 0")
  2902     proof (cases "x = 0")
  2903       case True thus ?thesis using suminf_arctan_zero by auto
  2903       case True thus ?thesis using suminf_arctan_zero by auto
  2904     next
  2904     next
  2905       case False hence "0 < \<bar>x\<bar>" and "- \<bar>x\<bar> < \<bar>x\<bar>" by auto
  2905       case False hence "0 < \<bar>x\<bar>" and "- \<bar>x\<bar> < \<bar>x\<bar>" by auto
  2906       have "suminf (?c (-\<bar>x\<bar>)) - arctan (-\<bar>x\<bar>) = suminf (?c 0) - arctan 0"
  2906       have "suminf (?c (-\<bar>x\<bar>)) - arctan (-\<bar>x\<bar>) = suminf (?c 0) - arctan 0"
  2907         by (rule suminf_eq_arctan_bounded[where x="0" and a="-\<bar>x\<bar>" and b="\<bar>x\<bar>", symmetric], auto simp add: `\<bar>x\<bar> < r` `-\<bar>x\<bar> < \<bar>x\<bar>`)
  2907         by (rule suminf_eq_arctan_bounded[where x="0" and a="-\<bar>x\<bar>" and b="\<bar>x\<bar>", symmetric])
       
  2908           (simp_all only: `\<bar>x\<bar> < r` `-\<bar>x\<bar> < \<bar>x\<bar>` neg_less_iff_less)
  2908       moreover
  2909       moreover
  2909       have "suminf (?c x) - arctan x = suminf (?c (-\<bar>x\<bar>)) - arctan (-\<bar>x\<bar>)"
  2910       have "suminf (?c x) - arctan x = suminf (?c (-\<bar>x\<bar>)) - arctan (-\<bar>x\<bar>)"
  2910         by (rule suminf_eq_arctan_bounded[where x="x" and a="-\<bar>x\<bar>" and b="\<bar>x\<bar>"], auto simp add: `\<bar>x\<bar> < r` `-\<bar>x\<bar> < \<bar>x\<bar>`)
  2911         by (rule suminf_eq_arctan_bounded[where x="x" and a="-\<bar>x\<bar>" and b="\<bar>x\<bar>"])
       
  2912           (simp_all only: `\<bar>x\<bar> < r` `-\<bar>x\<bar> < \<bar>x\<bar>` neg_less_iff_less)
  2911       ultimately 
  2913       ultimately 
  2912       show ?thesis using suminf_arctan_zero by auto
  2914       show ?thesis using suminf_arctan_zero by auto
  2913     qed
  2915     qed
  2914     thus ?thesis by auto
  2916     thus ?thesis by auto
  2915   qed } note when_less_one = this
  2917   qed } note when_less_one = this