src/HOL/Transcendental.thy
 changeset 55719 cdddd073bff8 parent 55417 01fbfb60c33e child 55734 3f5b2745d659
```     1.1 --- a/src/HOL/Transcendental.thy	Mon Feb 24 15:45:55 2014 +0000
1.2 +++ b/src/HOL/Transcendental.thy	Mon Feb 24 16:56:04 2014 +0000
1.3 @@ -60,6 +60,23 @@
1.4    apply (metis atLeastLessThan_iff diff_diff_cancel diff_less_Suc imageI le0 less_Suc_eq_le)
1.5    done
1.6
1.7 +lemma power_diff_1_eq:
1.8 +  fixes x :: "'a::{comm_ring,monoid_mult}"
1.9 +  shows "n \<noteq> 0 \<Longrightarrow> x^n - 1 = (x - 1) * (\<Sum>i=0..<n. (x^i))"
1.10 +using lemma_realpow_diff_sumr2 [of x _ 1]
1.11 +  by (cases n) auto
1.12 +
1.13 +lemma one_diff_power_eq':
1.14 +  fixes x :: "'a::{comm_ring,monoid_mult}"
1.15 +  shows "n \<noteq> 0 \<Longrightarrow> 1 - x^n = (1 - x) * (\<Sum>i=0..<n. x^(n - Suc i))"
1.16 +using lemma_realpow_diff_sumr2 [of 1 _ x]
1.17 +  by (cases n) auto
1.18 +
1.19 +lemma one_diff_power_eq:
1.20 +  fixes x :: "'a::{comm_ring,monoid_mult}"
1.21 +  shows "n \<noteq> 0 \<Longrightarrow> 1 - x^n = (1 - x) * (\<Sum>i=0..<n. x^i)"
1.22 +by (metis one_diff_power_eq' [of n x] nat_diff_setsum_reindex)
1.23 +
1.24  text{*Power series has a `circle` of convergence, i.e. if it sums for @{term
1.25    x}, then it sums absolutely for @{term z} with @{term "\<bar>z\<bar> < \<bar>x\<bar>"}.*}
1.26
```