equal
deleted
inserted
replaced
39 fixes x :: "'a::{comm_ring,monoid_mult}" |
39 fixes x :: "'a::{comm_ring,monoid_mult}" |
40 assumes "m \<le> n" |
40 assumes "m \<le> n" |
41 shows "(1 - x) * (\<Sum>i=m..n. x^i) = x^m - x^Suc n" |
41 shows "(1 - x) * (\<Sum>i=m..n. x^i) = x^m - x^Suc n" |
42 proof - |
42 proof - |
43 have "(1 - x) * (\<Sum>i=m..n. x^i) = x^m * (1 - x) * (\<Sum>i\<le>n-m. x^i)" |
43 have "(1 - x) * (\<Sum>i=m..n. x^i) = x^m * (1 - x) * (\<Sum>i\<le>n-m. x^i)" |
44 by (metis ab_semigroup_mult_class.mult_ac(1) assms mult.commute setsum_power_shift) |
44 by (metis mult.assoc mult.commute assms setsum_power_shift) |
45 also have "... =x^m * (1 - x^Suc(n-m))" |
45 also have "... =x^m * (1 - x^Suc(n-m))" |
46 by (metis ab_semigroup_mult_class.mult_ac(1) setsum_gp_basic) |
46 by (metis mult.assoc setsum_gp_basic) |
47 also have "... = x^m - x^Suc n" |
47 also have "... = x^m - x^Suc n" |
48 using assms |
48 using assms |
49 by (simp add: algebra_simps) (metis le_add_diff_inverse power_add) |
49 by (simp add: algebra_simps) (metis le_add_diff_inverse power_add) |
50 finally show ?thesis . |
50 finally show ?thesis . |
51 qed |
51 qed |
76 proof - |
76 proof - |
77 have "(\<Sum>i\<le>n. a i * x^i) - (\<Sum>i\<le>n. a i * y^i) = |
77 have "(\<Sum>i\<le>n. a i * x^i) - (\<Sum>i\<le>n. a i * y^i) = |
78 (\<Sum>i\<le>n. a i * (x^i - y^i))" |
78 (\<Sum>i\<le>n. a i * (x^i - y^i))" |
79 by (simp add: algebra_simps setsum_subtractf [symmetric]) |
79 by (simp add: algebra_simps setsum_subtractf [symmetric]) |
80 also have "... = (\<Sum>i\<le>n. a i * (x - y) * (\<Sum>j<i. y^(i - Suc j) * x^j))" |
80 also have "... = (\<Sum>i\<le>n. a i * (x - y) * (\<Sum>j<i. y^(i - Suc j) * x^j))" |
81 by (simp add: power_diff_sumr2 mult_ac) |
81 by (simp add: power_diff_sumr2 ac_simps) |
82 also have "... = (x - y) * (\<Sum>i\<le>n. (\<Sum>j<i. a i * y^(i - Suc j) * x^j))" |
82 also have "... = (x - y) * (\<Sum>i\<le>n. (\<Sum>j<i. a i * y^(i - Suc j) * x^j))" |
83 by (simp add: setsum_right_distrib mult_ac) |
83 by (simp add: setsum_right_distrib ac_simps) |
84 also have "... = (x - y) * (\<Sum>j<n. (\<Sum>i=Suc j..n. a i * y^(i - Suc j) * x^j))" |
84 also have "... = (x - y) * (\<Sum>j<n. (\<Sum>i=Suc j..n. a i * y^(i - Suc j) * x^j))" |
85 by (simp add: nested_setsum_swap') |
85 by (simp add: nested_setsum_swap') |
86 finally show ?thesis . |
86 finally show ?thesis . |
87 qed |
87 qed |
88 |
88 |