src/HOL/Transcendental.thy
 changeset 35038 a1d93ce94235 parent 35028 108662d50512 child 35213 b9866ad4e3be
equal 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`