equal
deleted
inserted
replaced
49 also have "... = (x - y) * (\<Sum>p = 0..<Suc (Suc n). x ^ p * y ^ (Suc n - p))" |
49 also have "... = (x - y) * (\<Sum>p = 0..<Suc (Suc n). x ^ p * y ^ (Suc n - p))" |
50 by (simp add: setsum_op_ivl_Suc [where n = "Suc n"] distrib_left lemma_realpow_diff_sumr |
50 by (simp add: setsum_op_ivl_Suc [where n = "Suc n"] distrib_left lemma_realpow_diff_sumr |
51 del: setsum_op_ivl_Suc) |
51 del: setsum_op_ivl_Suc) |
52 finally show ?case . |
52 finally show ?case . |
53 qed |
53 qed |
|
54 |
|
55 corollary power_diff_sumr2: --{*COMPLEX_POLYFUN in HOL Light*} |
|
56 fixes x :: "'a::{comm_ring,monoid_mult}" |
|
57 shows "x^n - y^n = (x - y) * (\<Sum>i=0..<n. y^(n - Suc i) * x^i)" |
|
58 using lemma_realpow_diff_sumr2[of x "n - 1" y] |
|
59 by (cases "n = 0") (simp_all add: field_simps) |
54 |
60 |
55 lemma lemma_realpow_rev_sumr: |
61 lemma lemma_realpow_rev_sumr: |
56 "(\<Sum>p=0..<Suc n. (x ^ p) * (y ^ (n - p))) = |
62 "(\<Sum>p=0..<Suc n. (x ^ p) * (y ^ (n - p))) = |
57 (\<Sum>p=0..<Suc n. (x ^ (n - p)) * (y ^ p))" |
63 (\<Sum>p=0..<Suc n. (x ^ (n - p)) * (y ^ p))" |
58 apply (rule setsum_reindex_cong [where f="\<lambda>i. n - i"]) |
64 apply (rule setsum_reindex_cong [where f="\<lambda>i. n - i"]) |