equal
deleted
inserted
replaced
111 "6 * (\<Sum>i::nat=0..n. i^Suc (Suc 0)) = n * (n + 1) * (2 * n + 1)" |
111 "6 * (\<Sum>i::nat=0..n. i^Suc (Suc 0)) = n * (n + 1) * (2 * n + 1)" |
112 (is "?P n" is "?S n = _") |
112 (is "?P n" is "?S n = _") |
113 proof (induct n) |
113 proof (induct n) |
114 show "?P 0" by simp |
114 show "?P 0" by simp |
115 next |
115 next |
116 fix n have "?S (n + 1) = ?S n + 6 * (n + 1)^Suc (Suc 0)" by (simp add: distrib) |
116 fix n have "?S (n + 1) = ?S n + 6 * (n + 1)^Suc (Suc 0)" |
|
117 by (simp add: distrib) |
117 also assume "?S n = n * (n + 1) * (2 * n + 1)" |
118 also assume "?S n = n * (n + 1) * (2 * n + 1)" |
118 also have "... + 6 * (n + 1)^Suc (Suc 0) = |
119 also have "... + 6 * (n + 1)^Suc (Suc 0) = |
119 (n + 1) * (n + 2) * (2 * (n + 1) + 1)" by (simp add: distrib) |
120 (n + 1) * (n + 2) * (2 * (n + 1) + 1)" by (simp add: distrib) |
120 finally show "?P (Suc n)" by simp |
121 finally show "?P (Suc n)" by simp |
121 qed |
122 qed |