equal
deleted
inserted
replaced
2950 qed |
2950 qed |
2951 hence "0 \<le> ?a x n - ?diff x n" by auto |
2951 hence "0 \<le> ?a x n - ?diff x n" by auto |
2952 } |
2952 } |
2953 hence "\<forall> x \<in> { 0 <..< 1 }. 0 \<le> ?a x n - ?diff x n" by auto |
2953 hence "\<forall> x \<in> { 0 <..< 1 }. 0 \<le> ?a x n - ?diff x n" by auto |
2954 moreover have "\<And>x. isCont (\<lambda> x. ?a x n - ?diff x n) x" |
2954 moreover have "\<And>x. isCont (\<lambda> x. ?a x n - ?diff x n) x" |
2955 unfolding diff_def divide_inverse |
2955 unfolding diff_minus divide_inverse |
2956 by (auto intro!: isCont_add isCont_rabs isCont_ident isCont_minus isCont_arctan isCont_inverse isCont_mult isCont_power isCont_const isCont_setsum) |
2956 by (auto intro!: isCont_add isCont_rabs isCont_ident isCont_minus isCont_arctan isCont_inverse isCont_mult isCont_power isCont_const isCont_setsum) |
2957 ultimately have "0 \<le> ?a 1 n - ?diff 1 n" by (rule LIM_less_bound) |
2957 ultimately have "0 \<le> ?a 1 n - ?diff 1 n" by (rule LIM_less_bound) |
2958 hence "?diff 1 n \<le> ?a 1 n" by auto |
2958 hence "?diff 1 n \<le> ?a 1 n" by auto |
2959 } |
2959 } |
2960 have "?a 1 ----> 0" |
2960 have "?a 1 ----> 0" |
2966 obtain N :: nat where N_I: "\<And> n. N \<le> n \<Longrightarrow> ?a 1 n < r" using LIMSEQ_D[OF `?a 1 ----> 0` `0 < r`] by auto |
2966 obtain N :: nat where N_I: "\<And> n. N \<le> n \<Longrightarrow> ?a 1 n < r" using LIMSEQ_D[OF `?a 1 ----> 0` `0 < r`] by auto |
2967 { fix n assume "N \<le> n" from `?diff 1 n \<le> ?a 1 n` N_I[OF this] |
2967 { fix n assume "N \<le> n" from `?diff 1 n \<le> ?a 1 n` N_I[OF this] |
2968 have "norm (?diff 1 n - 0) < r" by auto } |
2968 have "norm (?diff 1 n - 0) < r" by auto } |
2969 thus "\<exists> N. \<forall> n \<ge> N. norm (?diff 1 n - 0) < r" by blast |
2969 thus "\<exists> N. \<forall> n \<ge> N. norm (?diff 1 n - 0) < r" by blast |
2970 qed |
2970 qed |
2971 from this[unfolded LIMSEQ_rabs_zero diff_def add_commute[of "arctan 1"], THEN LIMSEQ_add_const, of "- arctan 1", THEN LIMSEQ_minus] |
2971 from this[unfolded LIMSEQ_rabs_zero diff_minus add_commute[of "arctan 1"], THEN LIMSEQ_add_const, of "- arctan 1", THEN LIMSEQ_minus] |
2972 have "(?c 1) sums (arctan 1)" unfolding sums_def by auto |
2972 have "(?c 1) sums (arctan 1)" unfolding sums_def by auto |
2973 hence "arctan 1 = (\<Sum> i. ?c 1 i)" by (rule sums_unique) |
2973 hence "arctan 1 = (\<Sum> i. ?c 1 i)" by (rule sums_unique) |
2974 |
2974 |
2975 show ?thesis |
2975 show ?thesis |
2976 proof (cases "x = 1", simp add: `arctan 1 = (\<Sum> i. ?c 1 i)`) |
2976 proof (cases "x = 1", simp add: `arctan 1 = (\<Sum> i. ?c 1 i)`) |