equal
deleted
inserted
replaced
2778 {assume x1: "x\<noteq>1" |
2778 {assume x1: "x\<noteq>1" |
2779 hence x1': "x - 1 \<noteq> 0" "1 - x \<noteq> 0" "x - 1 = - (1 - x)" "- (1 - x) \<noteq> 0" by auto |
2779 hence x1': "x - 1 \<noteq> 0" "1 - x \<noteq> 0" "x - 1 = - (1 - x)" "- (1 - x) \<noteq> 0" by auto |
2780 from geometric_sum[OF x1, of "Suc n", unfolded x1'] |
2780 from geometric_sum[OF x1, of "Suc n", unfolded x1'] |
2781 have "(- (1 - x)) * setsum (\<lambda>i. x^i) {0 .. n} = - (1 - x^(Suc n))" |
2781 have "(- (1 - x)) * setsum (\<lambda>i. x^i) {0 .. n} = - (1 - x^(Suc n))" |
2782 unfolding atLeastLessThanSuc_atLeastAtMost |
2782 unfolding atLeastLessThanSuc_atLeastAtMost |
2783 using x1' apply (auto simp only: field_simps) |
2783 using x1' apply (auto simp only: field_eq_simps) |
2784 apply (simp add: ring_simps) |
2784 apply (simp add: ring_simps) |
2785 done |
2785 done |
2786 then have ?thesis by (simp add: ring_simps) } |
2786 then have ?thesis by (simp add: ring_simps) } |
2787 ultimately show ?thesis by metis |
2787 ultimately show ?thesis by metis |
2788 qed |
2788 qed |
2813 moreover |
2813 moreover |
2814 {assume "\<not> n < m" hence nm: "m \<le> n" by arith |
2814 {assume "\<not> n < m" hence nm: "m \<le> n" by arith |
2815 {assume x: "x = 1" hence ?thesis by simp} |
2815 {assume x: "x = 1" hence ?thesis by simp} |
2816 moreover |
2816 moreover |
2817 {assume x: "x \<noteq> 1" hence nz: "1 - x \<noteq> 0" by simp |
2817 {assume x: "x \<noteq> 1" hence nz: "1 - x \<noteq> 0" by simp |
2818 from sum_gp_multiplied[OF nm, of x] nz have ?thesis by (simp add: field_simps)} |
2818 from sum_gp_multiplied[OF nm, of x] nz have ?thesis by (simp add: field_eq_simps)} |
2819 ultimately have ?thesis by metis |
2819 ultimately have ?thesis by metis |
2820 } |
2820 } |
2821 ultimately show ?thesis by metis |
2821 ultimately show ?thesis by metis |
2822 qed |
2822 qed |
2823 |
2823 |