avewright/proofwiki-math huggingface dataset:
Theorem: Valid Syllogism in Figure III needs Particular Conclusion and if Negative then Negative Major Premise

Let $Q$ be a valid categorical syllogism in Figure $\text {III}$.
Then it is a necessary condition that:
:The conclusion of $Q$ be a particular categorical statement
and:
:If the conclusion of $Q$ be a negative categorical statement, then so is the major premise of $Q$.

Proof:
Consider Figure $\text {III}$:
{{:Definition:Figure of Categorical Syllogism/III}}
Let the major premise of $Q$ be denoted $\text{Maj}$.
Let the minor premise of $Q$ be denoted $\text{Min}$.
Let the conclusion of $Q$ be denoted $\text{C}$.
$M$ is:
:the subject of $\text{Maj}$
:the subject of $\text{Min}$.
So, in order for $M$ to be distributed, either:
:$(1): \quad$ From Universal Categorical Statement Distributes its Subject: $\text{Maj}$ must be universal
or:
:$(2): \quad$ From Universal Categorical Statement Distributes its Subject: $\text{Min}$ must be universal.
Suppose $\text{Min}$ to be a negative categorical statement.
Then by No Valid Categorical Syllogism contains two Negative Premises:
:$\text{Maj}$ is an affirmative categorical statement.
From Conclusion of Valid Categorical Syllogism is Negative iff one Premise is Negative:
:$\text{C}$ is a negative categorical statement.
From Negative Categorical Statement Distributes its Predicate:
:$P$ is distributed in $\text{C}$.
From Negative Categorical Statement Distributes its Predicate:
:$P$ is undistributed in $\text{Maj}$.
From Distributed Term of Conclusion of Valid Categorical Syllogism is Distributed in Premise:
:$P$ is distributed in $\text{Maj}$.
That is, $P$ is both distributed and undistributed in $\text{Maj}$.
From this Proof by Contradiction it follows that $\text{Min}$ is an affirmative categorical statement.
Thus from Conclusion of Valid Categorical Syllogism is Negative iff one Premise is Negative:
:if $\text{C}$ is a negative categorical statement, then so is $\text{Maj}$
{{qed|lemma}}
We have that $\text{Min}$ is an affirmative categorical statement.
Hence from Negative Categorical Statement Distributes its Predicate:
:$S$ is undistributed in $\text{Min}$.
From Distributed Term of Conclusion of Valid Categorical Syllogism is Distributed in Premise:
:$S$ is undistributed in $\text{C}$.
So from Universal Categorical Statement Distributes its Subject:
:$\text{C}$ is a particular categorical statement.
{{qed|lemma}}
Hence, in order for $Q$ to be valid:
:$\text{C}$ must be a particular categorical statement
:if $\text{C}$ is a negative categorical statement, then so is $\text{Maj}$.
{{qed}}
Theorem: Valid Syllogisms in Figure IV

Let $Q$ be a valid categorical syllogism in Figure $\text {IV}$.
Then it is a necessary condition that:
:$(1): \quad$ Either:
:: the major premise of $Q$ be a negative categorical statement
:or:
:: the minor premise of $Q$ be a universal categorical statement
:or both.
:$(2): \quad$ If the conclusion of $Q$ be a negative categorical statement, then the major premise of $Q$ be a universal categorical statement.
:$(3): \quad$ If the conclusion of $Q$ be a universal categorical statement, then the minor premise of $Q$ be a negative categorical statement.

Proof:
Consider Figure $\text {IV}$:
{{:Definition:Figure of Categorical Syllogism/IV}}
Let the major premise of $Q$ be denoted $\text{Maj}$.
Let the minor premise of $Q$ be denoted $\text{Min}$.
Let the conclusion of $Q$ be denoted $\text{C}$.
$M$ is:
:the predicate of $\text{Maj}$
:the subject of $\text{Min}$.
We have:
:Middle Term of Valid Categorical Syllogism is Distributed at least Once.
So, in order for $M$ to be distributed, either:
:From Negative Categorical Statement Distributes its Predicate: $\text{Maj}$ must be negative
or:
:From Universal Categorical Statement Distributes its Subject: $\text{Min}$ must be universal.
Both may be the case.
Thus $(1)$ is seen to hold.
{{qed|lemma}}
Let $\text{C}$ be a negative categorical statement.
From Negative Categorical Statement Distributes its Predicate:
:$P$ is distributed in $\text{C}$.
From Distributed Term of Conclusion of Valid Categorical Syllogism is Distributed in Premise:
:$P$ is distributed in $\text{Maj}$.
So from Universal Categorical Statement Distributes its Subject:
:$\text{Maj}$ is a universal categorical statement.
Thus $(2)$ is seen to hold.
{{qed|lemma}}
Let $\text{C}$ be a universal categorical statement.
From Universal Categorical Statement Distributes its Subject:
:$S$ is distributed in $\text{C}$.
From Distributed Term of Conclusion of Valid Categorical Syllogism is Distributed in Premise:
:$S$ is distributed in $\text{Min}$.
From Negative Categorical Statement Distributes its Predicate:
:$S$ is a negative categorical statement.
Thus $(3)$ is seen to hold.
{{qed}}
Theorem: Elimination of all but 24 Categorical Syllogisms as Invalid

Of the $256$ different types of categorical syllogism, all but $24$ can be identified as invalid.
These are the $24$ patterns which may still be valid:
:$\begin{array}{rl}
\text{I} & AAA \\
\text{I} & AII \\
\text{I} & EAE \\
\text{I} & EIO \\
\text{I} & AAI \\
\text{I} & EAO \\
\end{array}
\qquad
\begin{array}{rl}
\text{II} & EAE \\
\text{II} & AEE \\
\text{II} & AOO \\
\text{II} & EIO \\
\text{II} & EAO \\
\text{II} & AEO \\
\end{array}
\qquad
\begin{array}{rl}
\text{III} & AAI \\
\text{III} & AII \\
\text{III} & IAI \\
\text{III} & EAO \\
\text{III} & EIO \\
\text{III} & OAO \\
\end{array}
\qquad
\begin{array}{rl}
\text{IV} & AAI \\
\text{IV} & AEE \\
\text{IV} & EAO \\
\text{IV} & EIO \\
\text{IV} & IAI \\
\text{IV} & AEO \\
\end{array}$

Proof:
From Elimination of all but 48 Categorical Syllogisms as Invalid there are $12$ possible patterns of categorical syllogism per figure:
:$\begin{array}{cccccc}
AAA & AAI & AEE & AEO & AII & AOO \\
EAE & EAO & EIO & IAI & IEO & OAO \\
\end{array}$
Theorem: Extension of Contradictory Branch is Contradictory

Let $T$ be a propositional tableau.
Let $\Gamma$ be a contradictory branch of $T$.
Let $\Gamma'$ be an extension of $\Gamma$.
Then $\Gamma'$ is also contradictory.

Proof:
Since $\Gamma$ is contradictory, there is some WFF $\mathbf A$ such that both $\mathbf A$ and $\neg \mathbf A$ occur along $\Gamma$.
Since $\Gamma'$ is an extension of $\Gamma$, $\mathbf A$ and $\neg \mathbf A$ also occur along $\Gamma'$.
Hence $\Gamma'$ is contradictory.
{{qed}}
Category:Propositional Tableaux
50yd0247a2wmsfrou02s7crnv5wy9j8
Theorem: Finished Propositional Tableau has Finished Branch or is Confutation

Let $\struct {T, \mathbf H, \Phi}$ be a finished propositional tableau.
Then one of the following holds:
:$T$ has a finished branch
:$T$ is a tableau confutation.

Proof:
Suppose $T$ has no finished branch.
Then since $T$ is finished, every branch of $T$ is contradictory.
Hence $T$ is a tableau confutation.
{{qed}}
Theorem: Alternating Harmonic Series is Conditionally Convergent

The alternating harmonic series:
:$\ds \sum_{n \mathop = 1}^\infty \frac {\paren {-1}^\paren {n - 1} } n = 1 - \frac 1 2 + \frac 1 3 - \frac 1 4 + \cdots$
is conditionally convergent.

Proof:
Note first that:
:$\ds \sum_{n \mathop = 1}^\infty \size {\frac {\paren {-1}^\paren {n - 1} } n} = \sum_{n \mathop = 1}^\infty \frac 1 n$
which is divergent by Harmonic Series is Divergent.
Hence by definition $\ds \sum_{n \mathop = 1}^\infty \size {\frac {\paren {-1}^\paren {n - 1} } n}$ is not '''absolutely convergent'''.
{{qed}}
Next note that $\size {\dfrac 1 n}$ is a basic null sequence:
:$\ds \lim_{n \mathop \to \infty} \dfrac 1 n = 0$
and that:
:$\forall n \in \N_{>0}: \dfrac 1 n > 0$
From Reciprocal Sequence is Strictly Decreasing:
:$\dfrac 1 n > \dfrac 1 {n + 1}$
The result follows from the Alternating Series Test.
{{qed}}
Theorem: Manipulation of Absolutely Convergent Series/Permutation

If $\pi: \N \to \N$ is a permutation of $N$, then:
:$\ds \sum_{n \mathop = 1}^\infty a_n = \sum_{n \mathop = 1}^\infty a_{\map \pi n}$

Proof:
Let $\epsilon > 0$.
From Tail of Convergent Series tends to Zero, it follows that there exists $N \in \N$ such that:
:$\ds \sum_{n \mathop = N}^\infty \size {a_n} < \epsilon$
By definition, a permutation is bijective.
Hence we can find $M \in \N$ such that:
:$\set {1, \ldots, N - 1} \subseteq \set {\map \pi 1, \ldots, \map \pi M}$
Let $m \in \N$, and put $B = \set {n \in N: \map {\pi^{-1} } n > m}$.
For all $m \ge M$, it follows that:
{{begin-eqn}}
{{eqn | l = \size {\sum_{n \mathop = 1}^\infty a_n - \sum_{k \mathop = 1}^m a_{\map \pi k} }
      | r = \size {\sum_{n \mathop = 1}^\infty a_n \map {\chi_B} n}
      | c = where $\chi_B$ is the characteristic function of $B$
}}
{{eqn | o = \le
      | r = \sum_{n \mathop = 1}^\infty \size {a_n} \map {\chi_B} n
      | c = Triangle Inequality
}}
{{eqn | o = \le
      | r = \sum_{n \mathop = N}^\infty \size {a_n}
      | c = as $\chi_B = 0$ for all $n < N$
}}
{{eqn | o = <
      | r = \epsilon
}}
{{end-eqn}}
By definition of convergent series, it follows that:
:$\ds \sum_{n \mathop = 1}^\infty a_n = \lim_{m \mathop \to \infty} \sum_{k \mathop = 1}^m a_{\map \pi k} = \sum_{k \mathop = 1}^\infty a_{\map \pi k}$
{{qed}}
Theorem: Manipulation of Absolutely Convergent Series/Characteristic Function

Let $A \subseteq \N$.
Then:
:$\ds \sum_{n \mathop = 1}^\infty a_n \map {\chi_A} n = \sum_{n \mathop \in A} a_n$
where $\chi_A$ is the characteristic function of $A$.

Proof:
For all $N \in \N$, we have:
:$\ds \sum_{n \mathop = 1}^N \size {a_n \map {\chi_A} n} \le \sum_{n \mathop = 1}^N \size {a_n} \le \sum_{n \mathop = 1}^\infty \size {a_n}$
It follows that:
:$\ds \sum_{n \mathop = 1}^\infty \size {a_n \map {\chi_A} n} \le \sum_{n \mathop = 1}^\infty \size {a_n}$
Then $\ds \sum_{n \mathop = 1}^\infty a_n \map {\chi_A} n$ is absolutely convergent.
It follows from Manipulation of Absolutely Convergent Series: Permutation that the order of the terms in the series does not matter.
As $\map {\chi_A} n = 0$ for all $n \notin A$, we have:
:$\ds \sum_{n \mathop = 1}^\infty a_n \map {\chi_A} n = \sum_{n \mathop \in A} a_n$
{{qed}}
Category:Series
Category:Convergence
qwu9clcdeqfjxdurknw54t3fntyojwn
Theorem: Manipulation of Absolutely Convergent Series/Scale Factor

Let $c \in \R$, or $c \in \C$.
Then:
:$\ds c \sum_{n \mathop = 1}^\infty a_n = \sum_{n \mathop = 1}^\infty c a_n$

Proof:
{{begin-eqn}}
{{eqn | l = c \sum_{n \mathop = 1}^\infty a_n
      | r = c \lim_{N \mathop \to \infty} \sum_{n \mathop = 1}^N a_n
}}
{{eqn | r = \lim_{N \mathop \to \infty} \sum_{n \mathop = 1}^N c a_n
      | c = Multiple Rule for Sequences
}}
{{eqn | r = \sum_{n \mathop = 1}^\infty c a_n
}}
{{end-eqn}}
{{qed}}
Category:Series
Category:Convergence
m043wqeh1ne98z5qvtsy4ve027u2xbe
Theorem: Binomial Coefficient with Self minus One

:$\forall n \in \N_{>0}: \dbinom n {n - 1} = n$

Proof:
The case where $n = 1$ can be taken separately.
From Binomial Coefficient with Zero:
:$\dbinom 1 0 = 1$
demonstrating that the result holds for $n = 1$.
Let $n \in \N: n > 1$.
From the definition of binomial coefficients:
:$\dbinom n {n - 1} = \dfrac {n!} {\paren {n - 1}! \paren {n - \paren {n - 1} }!} = \dfrac {n!} {\paren {n - 1}! \ 1!}$
the result following directly from the definition of the factorial.
{{qed}}
Theorem: Binomial Coefficient with Self minus One

:$\forall n \in \N_{>0}: \dbinom n {n - 1} = n$

Proof:
From Cardinality of Set of Subsets, $\dbinom n {n - 1}$ is the number of combination of things taken $n - 1$ at a time.
Choosing $n - 1$ things from $n$ is the same thing as choosing which $1$ of the elements to be left out.
There are $n$ different choices for that $1$ element.
Therefore there are $n$ ways to choose $n - 1$ things from $n$.
{{qed}}
Theorem: Definite Integral of Uniformly Convergent Series of Continuous Functions

Let $\sequence {f_n}$ be a sequence of real functions.
Let each of $\sequence {f_n}$ be continuous on the interval $\hointr a b$.
{{explain|Investigation needed as to whether there is a mistake in {{BookReference|Special Functions of Mathematics for Engineers|1992|Larry C. Andrews|ed = 2nd|edpage = Second Edition}} -- should it actually be a closed interval?}}
Let the series:
:$\ds \map f x := \sum_{n \mathop = 1}^\infty \map {f_n} x$
be uniformly convergent for all $x \in \closedint a b$.
Then:
:$\ds \int_a^b \map f x \rd x = \sum_{n \mathop = 1}^\infty \int_a^b \map {f_n} x \rd x$

Proof:
Define $\map {S_N} x = \ds \sum_{n \mathop = 1}^N \map {f_n} x$.
We have:
{{begin-eqn}}
{{eqn | l = \size {\int_a^b \map f x \rd x - \sum_{n \mathop = 1}^N \int_a^b \map {f_n} x \rd x}
      | r = \size {\int_a^b \paren {\map f x - \map {S_N} x} \rd x}
      | c = 
}}
{{eqn | o = \le
      | r = \paren {b - a} \sup_{x \mathop \in \closedint a b} \size {\map f x - \map {S_N} x}
      | c = 
}}
{{eqn | o = \to
      | r = 0
      | c = as $N \to +\infty$
}}
{{end-eqn}}
{{qed}}
Theorem: Power Series Converges Uniformly within Radius of Convergence

Let $\ds S := \sum_{n \mathop = 0}^\infty a_n \paren {x - \xi}^n$ be a power series about a point $\xi$.
Let $R$ be the radius of convergence of $S$.
Let $\rho \in \R$ such that $0 \le \rho < R$.
Then $S$ is uniformly convergent on $D = \set {x: \size {x - \xi} \le \rho}$.

Proof:
We shall make use of the Weierstrass M-Test to prove this result.
To begin with, for each $n \in N$, define for $x \in D$:
:$\map {f_n} x = a_n \paren {x - \xi}^n$
We have:
{{begin-eqn}}
{{eqn | l = \size {\map {f_n} x}
      | r = \size {a_n \paren {x - \xi}^n}
}}
{{eqn | o = \le
      | r = \size {a_n \rho^n}
      | c = $x \in D$
}}
{{end-eqn}}
Define $M_n = \size {a_n \rho^n}$.
Then $M_n$ is an upper bound for $\size {\map {f_n} x}$.
So, by the definition of a supremum:
:$\ds \sup_{x \mathop \in D} \size {\map {f_n} x} \le M_n$
Next, to apply the Weierstrass M-Test, it remains to be shown that $\ds \sum_{n \mathop = 0}^\infty M_n = \sum_{n \mathop = 0}^\infty \size {a_n \rho^n}$ converges.
Choose $x = \xi + \rho$ and note that:
:$\size {x - \xi} = \size \rho = \rho < R$
Hence, by definition of radius of convergence, $x$ falls within the interval of convergence of $S$.
Thus $\ds S = \sum_{n \mathop = 0}^\infty a_n (x - \xi)^n = \sum_{n \mathop = 0}^\infty a_n \rho^n$ converges.
By Existence of Interval of Convergence of Power Series, a power series always converges absolutely at all points in its interval of convergence.
Hence $\ds \sum_{n \mathop = 0}^\infty M_n = \sum_{n \mathop = 0}^\infty \size {a_n \rho^n}$ also converges.
Finally then, having satisfied all the requirements to use Weierstrass M-Test, we can conclude that $\ds \sum_{n \mathop = 0}^\infty \map {f_n} x = \sum_{n \mathop = 0}^\infty a_n \paren {x - \xi}^n$ converges uniformly in $D$.
{{qed}}
Theorem: Power Series Converges to Continuous Function

Let $\ds \map f x := \sum_{n \mathop = 0}^\infty a_n \paren {x - \xi}^n$ be a power series about a point $\xi$.
Let $R$ be the radius of convergence of $S$.
Then $\map f x$ is a continuous function on $\set {x: \size {x - \xi} < R}$.

Proof:
Let $\rho \in \R$ such that $0 \le \rho < R$.
From Power Series Converges Uniformly within Radius of Convergence, $\map f x$ is uniformly convergent on $\set {x: \size {x - \xi} \le \rho}$.
From Real Polynomial Function is Continuous, each of $\map {f_n} x = a_n x^n$ is a continuous function of $x$.
The result follows from Uniformly Convergent Series of Continuous Functions is Continuous.
{{qed}}
Theorem: Power Series is Termwise Integrable within Radius of Convergence

Let $\ds \map f x := \sum_{n \mathop = 0}^\infty a_n \paren {x - \xi}^n$ be a power series about a point $\xi$.
Let $R$ be the radius of convergence of $S$.
Then:
:$\ds \int_a^b \map f x \rd x = \sum_{n \mathop = 0}^\infty \int_a^b a_n x^n \rd x = \sum_{n \mathop = 0}^\infty a_n \frac {x^{n + 1} } {n + 1}$

Proof:
Let $\rho \in \R$ such that $0 \le \rho < R$.
From Power Series Converges Uniformly within Radius of Convergence, $\map f x$ is uniformly convergent on $\set {x: \size {x - \xi} \le \rho}$.
From Real Polynomial Function is Continuous, each of $\map {f_n} x = a_n x^n$ is a continuous function of $x$.
Then from Definite Integral of Uniformly Convergent Series of Continuous Functions:
:$\ds \int_a^b \map f x \rd x = \sum_{n \mathop = 0}^\infty \int_a^b a_n x^n \rd x$
The final result follows from Integral of Power.
{{qed}}
Theorem: Power Series is Termwise Differentiable within Radius of Convergence

Let $\ds \map f x := \sum_{n \mathop = 0}^\infty a_n \paren {x - \xi}^n$ be a power series about a point $\xi$.
Let $R$ be the radius of convergence of the series.
Then:
:$\ds \frac \d {\d x} \map f x = \sum_{n \mathop = 0}^\infty \frac \d {\d x} a_n \paren {x - \xi}^n = \sum_{n \mathop = 1}^\infty  n a_n \paren {x - \xi}^{n - 1}$
for $\size {x - \xi} < R$.

Proof:
Let $\rho \in \R$ such that $0 \le \rho < R$.
From Power Series Converges Uniformly within Radius of Convergence, $\map f x$ is uniformly convergent on $\set {x: \size {x - \xi} \le \rho}$.
From Real Polynomial Function is Continuous, each of $\map {f_n} x = a_n \paren {x - \xi}^n$ is a continuous function of $x$.
From Power Rule for Derivatives:
:$\dfrac \d {\d x} \paren {x - \xi}^n = n \paren {x - \xi}^{n - 1}$
and again from Real Polynomial Function is Continuous, each of $\dfrac \d {\d x} \map {f_n} x = n a_n \paren {x - \xi}^{n - 1}$ is a continuous function of $x$.
Then from Derivative of Uniformly Convergent Series of Continuously Differentiable Functions:
{{begin-eqn}}
{{eqn | l = \frac \d {\d x} \map f x
      | r = \sum_{n \mathop = 0}^\infty \frac \d {\d x} a_n \paren {x - \xi}^n
}}
{{eqn | r = \sum_{n \mathop = 0}^\infty n a_n \paren {x - \xi}^{n - 1}
      | c = 
}}
{{eqn | r = \sum_{n \mathop = 1}^\infty n a_n \paren {x - \xi}^{n - 1}
      | c = as $n a_n \paren {x - \xi}^{n - 1} = 0$ when $n = 0$
}}
{{end-eqn}}
{{qed}}
Theorem: Power Series Expansion for Logarithm of 1 + x

The Newton-Mercator series defines the  natural logarithm function as a power series expansion:
{{begin-eqn}}
{{eqn | l = \map \ln {1 + x}
      | r = \sum_{n \mathop = 1}^\infty \paren {-1}^{n - 1} \frac {x^n} n
}}
{{eqn | r = x - \frac {x^2} 2 + \frac {x^3} 3 - \frac {x^4} 4 + \cdots
}}
{{end-eqn}}
valid for all $x \in \R$ such that $-1 < x \le 1$.

Proof:
From Sum of Infinite Geometric Sequence, putting $-x$ for $x$:
:$(1): \quad \ds \sum_{n \mathop = 0}^\infty \paren {-x}^n = \frac 1 {1 + x}$
for $-1 < x < 1$.
From Power Series Converges Uniformly within Radius of Convergence, $(1)$ is uniformly convergent on every closed interval within the interval $\openint {-1} 1$.
From Power Series is Termwise Integrable within Radius of Convergence, $(1)$ can be integrated term by term:
{{begin-eqn}}
{{eqn | l = \int_0^x \frac 1 {1 + t} \rd t
      | r = \sum_{n \mathop = 0}^\infty \int_0^x \paren {-t}^n \rd t
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \map \ln {1 + x}
      | r = \sum_{n \mathop = 0}^\infty \paren {-1}^n \frac {x^{n + 1} } {n + 1}
      | c = Primitive of Reciprocal and Integral of Power
}}
{{eqn | ll= \leadsto
      | l = \map \ln {1 + x}
      | r = \sum_{n \mathop = 1}^\infty \paren {-1}^{n - 1} \frac {x^n} n
      | c = letting $n \to n - 1$
}}
{{end-eqn}}
{{finish|Cover the case where $x {{=}} 1$}}
Theorem: Newton-Mercator Series/Examples/2

The Newton-Mercator Series for $x = 1$ converges to the natural logarithm of $2$:
{{begin-eqn}}
{{eqn | l = \sum_{n \mathop = 1}^\infty \frac {\paren {-1}^\paren {n - 1} } n
      | r = 1 - \frac 1 2 + \frac 1 3 - \frac 1 4 + \dotsb
      | c = 
}}
{{eqn | r = \ln 2
      | c = 
}}
{{end-eqn}}
This real number is known as Mercator's constant.

Proof:
From the definition of the Newton-Mercator Series:
{{begin-eqn}}
{{eqn | l = \map \ln {1 + x}
      | r = x - \dfrac {x^2} 2 + \dfrac {x^3} 3 - \dfrac {x^4} 4 + \cdots
      | c = 
}}
{{eqn | r = \sum_{n \mathop = 1}^\infty \frac {\paren {-1}^{n + 1} } n x^n
      | c = 
}}
{{end-eqn}}
This is valid for $-1 < x \le 1$.
Setting $x = 1$:
{{begin-eqn}}
{{eqn | l = \map \ln {1 + 1}
      | r = 1 - \dfrac {1^2} 2 + \dfrac {1^3} 3 - \dfrac {1^4} 4 + \cdots
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \ln 2
      | r = 1 - \dfrac 1 2 + \dfrac 1 3 - \dfrac 1 4 + \dfrac 1 5 - \cdots
      | c = 
}}
{{end-eqn}}
The fact that it does indeed converge is shown in Alternating Harmonic Series is Conditionally Convergent.
{{qed}}
Theorem: Power Series Expansion for Sine Function

The sine function has the power series expansion:
{{begin-eqn}}
{{eqn | l = \sin x
      | r = \sum_{n \mathop = 0}^\infty \paren {-1}^n \frac {x^{2 n + 1} } {\paren {2 n + 1}!}
      | c = 
}}
{{eqn | r = x - \frac {x^3} {3!} + \frac {x^5} {5!} - \frac {x^7} {7!} + \cdots
      | c = 
}}
{{end-eqn}}
valid for all $x \in \R$.

Proof:
From Derivative of Sine Function:
:$\dfrac \d {\d x} \sin x = \cos x$
From Derivative of Cosine Function:
:$\dfrac \d {\d x} \cos x = -\sin x$
Hence:
{{begin-eqn}}
{{eqn | l = \dfrac {\d^2} {\d x^2} \sin x
      | r = -\sin x
      | c = 
}}
{{eqn | l = \dfrac {\d^3} {\d x^3} \sin x
      | r = -\cos x
      | c = 
}}
{{eqn | l = \dfrac {\d^4} {\d x^4} \sin x
      | r = \sin x
      | c = 
}}
{{end-eqn}}
and so for all $m \in \N$:
{{begin-eqn}}
{{eqn | ll= m = 4 k:
      | l = \dfrac {\d^m} {\d x^m} \sin x
      | r = \sin x
      | c = 
}}
{{eqn | ll= m = 4 k + 1:
      | l = \dfrac {\d^m} {\d x^m} \sin x
      | r = \cos x
      | c = 
}}
{{eqn | ll= m = 4 k + 2:
      | l = \dfrac {\d^m} {\d x^m} \sin x
      | r = -\sin x
      | c = 
}}
{{eqn | ll= m = 4 k + 3:
      | l = \dfrac {\d^m} {\d x^m} \sin x
      | r = -\cos x
      | c = 
}}
{{end-eqn}}
where $k \in \Z$.
This leads to the Maclaurin series expansion:
{{begin-eqn}}
{{eqn | l = \sin x
      | r = \sum_{k \mathop = 0}^\infty \paren {\frac {x^{4 k} } {\paren {4 k}!} \map \sin 0 + \frac {x^{4 k + 1} } {\paren {4 k + 1}!} \map \cos 0 - \frac {x^{4 k + 2} } {\paren {4 k + 2}!} \map \sin 0 - \frac {x^{4 k + 3} } {\paren {4 k + 3}!} \map \cos 0}
      | c = 
}}
{{eqn | r = \sum_{k \mathop = 0}^\infty \paren {\frac {x^{4 k + 1} } {\paren {4 k + 1}!} - \frac {x^{4 k + 3} } {\paren {4 k + 3}!} }
      | c = Sine of Zero is Zero, Cosine of Zero is One
}}
{{eqn | r = \sum_{n \mathop = 0}^\infty \paren {-1}^n \frac {x^{2 n + 1} } {\paren {2 n + 1}!}
      | c = setting $n = 2 k$
}}
{{end-eqn}}
From Series of Power over Factorial Converges, it follows that this series is convergent for all $x$.
{{qed}}
Theorem: Power Series Expansion for Cosine Function

The cosine function has the power series expansion:
{{begin-eqn}}
{{eqn | l = \cos x
      | r = \sum_{n \mathop = 0}^\infty \paren {-1}^n \frac {x^{2 n} } {\paren {2 n}!}
      | c = 
}}
{{eqn | r = 1 - \frac {x^2} {2!} + \frac {x^4} {4!} - \frac {x^6} {6!} + \cdots
      | c = 
}}
{{end-eqn}}
valid for all $x \in \R$.

Proof:
From Derivative of Cosine Function:
:$\dfrac \d {\d x} \cos x = -\sin x$
From Derivative of Sine Function:
:$\dfrac \d {\d x} \sin x = \cos x$
Hence:
{{begin-eqn}}
{{eqn | l = \dfrac {\d^2} {\d x^2} \cos x
      | r = -\cos x
      | c = 
}}
{{eqn | l = \dfrac {\d^3} {\d x^3} \cos x
      | r = \sin x
      | c = 
}}
{{eqn | l = \dfrac {\d^4} {\d x^4} \cos x
      | r = \cos x
      | c = 
}}
{{end-eqn}}
and so for all $m \in \N$:
{{begin-eqn}}
{{eqn | ll = m = 4 k:
      | l = \dfrac {\d^m} {\d x^m} \cos x
      | r = \cos x
      | c = 
}}
{{eqn | ll = m = 4 k + 1:
      | l = \dfrac {\d^m} {\d x^m} \cos x
      | r = -\sin x
      | c = 
}}
{{eqn | ll = m = 4 k + 2:
      | l = \dfrac {\d^m} {\d x^m} \cos x
      | r = -\cos x
      | c = 
}}
{{eqn | ll = m = 4 k + 3:
      | l = \dfrac {\d^m} {\d x^m} \cos x
      | r = \sin x
      | c = 
}}
{{end-eqn}}
where $k \in \Z$.
This leads to the Maclaurin series expansion:
{{begin-eqn}}
{{eqn | l = \cos x
      | r = \sum_{k \mathop = 0}^\infty \paren {\frac {x^{4 k} } {\paren {4 k}!} \map \cos 0 - \frac {x^{4 k + 1} } {\paren {4 k + 1}!} \map \sin 0 - \frac {x^{4 k + 2} } {\paren {4 k + 2}!} \map \cos 0 + \frac {x^{4 k + 3} } {\paren {4 k + 3}!} \map \sin 0}
      | c = 
}}
{{eqn | r = \sum_{k \mathop = 0}^\infty \paren {\frac {x^{4 k} } {\paren {4 k}!} - \frac {x^{4 k + 2} } {\paren {4 k + 2}!} }
      | c = Sine of Zero is Zero, Cosine of Zero is One
}}
{{eqn | r = \sum_{n \mathop = 0}^\infty \paren {-1}^n \frac {x^{2 n} } {\paren {2 n}!}
      | c = setting $n = 2 k$
}}
{{end-eqn}}
From Series of Power over Factorial Converges, it follows that this series is convergent for all $x$.
{{qed}}