equal
deleted
inserted
replaced
71 "(\<Sum>i\<in>{..<n}. a+?I i*d) = |
71 "(\<Sum>i\<in>{..<n}. a+?I i*d) = |
72 ((\<Sum>i\<in>{..<n}. a) + (\<Sum>i\<in>{..<n}. ?I i*d))" |
72 ((\<Sum>i\<in>{..<n}. a) + (\<Sum>i\<in>{..<n}. ?I i*d))" |
73 by (rule setsum_addf) |
73 by (rule setsum_addf) |
74 also from ngt1 have "\<dots> = ?n*a + (\<Sum>i\<in>{..<n}. ?I i*d)" by simp |
74 also from ngt1 have "\<dots> = ?n*a + (\<Sum>i\<in>{..<n}. ?I i*d)" by simp |
75 also from ngt1 have "\<dots> = (?n*a + d*(\<Sum>i\<in>{1..<n}. ?I i))" |
75 also from ngt1 have "\<dots> = (?n*a + d*(\<Sum>i\<in>{1..<n}. ?I i))" |
76 by (simp add: setsum_mult setsum_head_upt) |
76 by (simp add: setsum_right_distrib setsum_head_upt) |
77 also have "(1+1)*\<dots> = (1+1)*?n*a + d*(1+1)*(\<Sum>i\<in>{1..<n}. ?I i)" |
77 also have "(1+1)*\<dots> = (1+1)*?n*a + d*(1+1)*(\<Sum>i\<in>{1..<n}. ?I i)" |
78 by simp |
78 by simp |
79 also from ngt1 have "{1..<n} = {1..n - 1}" |
79 also from ngt1 have "{1..<n} = {1..n - 1}" |
80 by (cases n) (auto simp: atLeastLessThanSuc_atLeastAtMost) |
80 by (cases n) (auto simp: atLeastLessThanSuc_atLeastAtMost) |
81 also from ngt1 |
81 also from ngt1 |