author kleing Sun, 19 Feb 2006 22:40:18 +0100 changeset 19109 9804aa8d5756 parent 19108 6f8c1343341b child 19110 4bda27adcd2e
fixed document
 src/HOL/Complex/ex/ROOT.ML file | annotate | diff | comparison | revisions src/HOL/Library/ASeries.thy file | annotate | diff | comparison | revisions
--- a/src/HOL/Complex/ex/ROOT.ML	Sun Feb 19 22:12:30 2006 +0100
+++ b/src/HOL/Complex/ex/ROOT.ML	Sun Feb 19 22:40:18 2006 +0100
@@ -15,6 +15,9 @@
no_document use_thy "BigO";
use_thy "BigO_Complex";

+no_document use_thy "ASeries";
use_thy "ASeries_Complex";
use_thy "HarmonicSeries";
+
+no_document use_thy "NatPair";
use_thy "DenumRat";
--- a/src/HOL/Library/ASeries.thy	Sun Feb 19 22:12:30 2006 +0100
+++ b/src/HOL/Library/ASeries.thy	Sun Feb 19 22:40:18 2006 +0100
@@ -24,14 +24,14 @@
"http://mathworld.wolfram.com/ArithmeticSeries.html")
The proof is a simple forward proof. Let $S$ equal the sum above and
$a$ the first element, then we have
-\begin{align}
-\nonumber  S &= a + (a+d) + (a+2d) + ... a_n \\
-\nonumber    &= n*a + d (0 + 1 + 2 + ... n-1) \\
-\nonumber    &= n*a + d (\frac{1}{2} * (n-1) * n)    \mbox{..using a simple sum identity} \\
-\nonumber    &= \frac{n}{2} (2a + d(n-1)) \\
-\nonumber    & \mbox{..but $(a+a_n = a + (a + d(n-1)) = 2a + d(n-1))$ so} \\
-\nonumber  S &= \frac{n}{2} (a + a_n)
-\end{align}
+\begin{tabular}{ll}
+  $S$ &$= a + (a+d) + (a+2d) + ... a_n$ \\
+    &$= n*a + d (0 + 1 + 2 + ... n-1)$ \\
+    &$= n*a + d (\frac{1}{2} * (n-1) * n)$   ..using a simple sum identity \\
+    &$= \frac{n}{2} (2a + d(n-1))$ \\
+    & ..but $(a+a_n = a + (a + d(n-1)) = 2a + d(n-1))$ so \\
+  $S$ &$= \frac{n}{2} (a + a_n)$
+\end{tabular}
*}

section {* Formal Proof *}