equal
deleted
inserted
replaced
104 |
104 |
105 lemma of_nat_sum_of_fourth_powers: |
105 lemma of_nat_sum_of_fourth_powers: |
106 "30 * of_nat (\<Sum>i=0..<m. i * i * i * i) = |
106 "30 * of_nat (\<Sum>i=0..<m. i * i * i * i) = |
107 of_nat m * (of_nat m - 1) * (of_nat (2 * m) - 1) * |
107 of_nat m * (of_nat m - 1) * (of_nat (2 * m) - 1) * |
108 (of_nat (3 * m * m) - of_nat (3 * m) - (1::int))" |
108 (of_nat (3 * m * m) - of_nat (3 * m) - (1::int))" |
109 by (induct m) simp_all |
109 by (induct m) (simp_all add: of_nat_mult) |
110 |
110 |
111 |
111 |
112 text {* |
112 text {* |
113 \medskip Sums of geometric series: @{text 2}, @{text 3} and the |
113 \medskip Sums of geometric series: @{text 2}, @{text 3} and the |
114 general case. |
114 general case. |