avewright/proofwiki-math huggingface dataset:
Theorem: Rule of Material Implication/Formulation 1

:$p \implies q \dashv \vdash \neg p \lor q$

Proof:
{{BeginTableau   |\neg p \lor q \vdash p \implies q}}
{{Premise        |1|\neg p \lor q}}
{{DeMorgan       |2|1|\neg \paren {\neg \neg p \land \neg q}|1|Disjunction}}
{{SequentIntro   |3|1
  |\neg \neg p \implies q
  |2
  |Conditional is Equivalent to Negation of Conjunction with Negative: $\neg \paren {p \land \neg q} \vdash p \implies q$
}}
{{Assumption     |4|p}}
{{DoubleNegIntro |5|4|\neg \neg p|4}}
{{ModusPonens    |6|1, 4|q|3|5}}
{{Implication    |7|1|p \implies q|4|6}}
{{EndTableau|qed}}
Theorem: Rule of Material Implication/Formulation 1/Reverse Implication

:$\neg p \lor q \vdash p \implies q$

Proof:
{{BeginTableau|\neg p \lor q \vdash p \implies q}}
{{Premise|1|\neg p \lor q}}
{{Assumption|2|\neg p|Pick the first of the disjuncts ...}}
{{Assumption|3|p|Assume its negation ...}}
{{NonContradiction|4|2, 3|3|2| ... and demonstrate a contradiction}}
{{Explosion|5|2, 3|q|4| ... from a falsehood, ''any'' statement can be derived - pick $q$}}
{{Implication|6|2|p \implies q|3|5}}
{{Assumption|7|q|Pick the second of the disjuncts ...}}
{{Assumption|8|p|... again assume $p$ ...}}
{{IdentityLaw|9|7|q|7|The truth of $q$ still holds}}
{{Implication|10|7|p \implies q|8|9}}
{{ProofByCases|11|1|p \implies q|1|2|6|7|10}}
{{EndTableau}}
{{qed}}
Theorem: Rule of Material Implication/Formulation 1/Reverse Implication

:$\neg p \lor q \vdash p \implies q$

Proof:
{{BeginTableau   |\neg p \lor q \vdash p \implies q}}
{{Premise        |1|\neg p \lor q}}
{{DeMorgan       |2|1|\neg \paren {\neg \neg p \land \neg q}|1|Disjunction}}
{{SequentIntro   |3|1
  |\neg \neg p \implies q
  |2
  |Conditional is Equivalent to Negation of Conjunction with Negative: $\neg \paren {p \land \neg q} \vdash p \implies q$
}}
{{Assumption     |4|p}}
{{DoubleNegIntro |5|4|\neg \neg p|4}}
{{ModusPonens    |6|1, 4|q|3|5}}
{{Implication    |7|1|p \implies q|4|6}}
{{EndTableau|qed}}
Theorem: Rule of Material Implication/Formulation 2

:$\vdash \paren {p \implies q} \iff \paren {\neg p \lor q}$

Proof:
{{BeginTableau|\paren {p \implies q} \iff \paren {\neg p \lor q} }}
{{Assumption|1|p \implies q}}
{{SequentIntro|2|1|\neg p \lor q|1|Rule of Material Implication: Formulation 1}}
{{Implication|3||\paren {p \implies q} \implies \paren {\neg p \lor q}|1|2}}
{{Assumption|4|\neg p \lor q}}
{{SequentIntro|5|4|p \implies q|4|Rule of Material Implication: Formulation 1}}
{{Implication|6||\paren {\neg p \lor q} \implies \paren {p \implies q}|4|5}}
{{BiconditionalIntro|7||\paren {p \implies q} \iff \paren {\neg p \lor q}|3|6}}
{{EndTableau|qed}}
{{LEM|Rule of Material Implication/Formulation 1/Forward Implication|3}}
Theorem: Rule of Material Implication/Formulation 2

:$\vdash \paren {p \implies q} \iff \paren {\neg p \lor q}$

Proof:
We apply the Method of Truth Tables.
As can be seen by inspection, the truth values under the main connective are true for all boolean interpretations.
:<nowiki>$\begin{array}{|ccc|c|cccc|} \hline
(p & \implies & q) & \iff & (\neg & p & \lor & q) \\
\hline
\F & \T & \F & \T & \T & \F & \T & \F \\
\F & \T & \T & \T & \T & \F & \T & \T \\
\T & \F & \F & \F & \T & \T & \F & \F \\
\T & \T & \T & \F & \T & \T & \T & \T \\
\hline
\end{array}$</nowiki>
{{qed}}
Theorem: Modus Tollendo Ponens/Variant/Formulation 2

:$\vdash \paren {p \lor q} \iff \paren {\neg p \implies q}$

Proof:
{{BeginTableau|\vdash \paren {p \lor q} \iff \paren {\neg p \implies q} }}
{{Assumption|1|p \lor q}}
{{SequentIntro|2|1|\neg p \implies q|1|Modus Tollendo Ponens: Formulation 1}}
{{Implication|3||\paren {p \lor q} \implies \paren {\neg p \implies q}|1|2}}
{{Assumption|4|\neg p \implies q}}
{{SequentIntro|5|4|p \lor q|4|Modus Tollendo Ponens: Formulation 1}}
{{Implication|6||\paren {\neg p \implies q} \implies \paren {p \lor q}|4|5}}
{{BiconditionalIntro|7||\paren {p \lor q} \iff \paren {\neg p \implies q}|3|6}}
{{EndTableau}}
{{qed}}
{{LEM||4}}
Theorem: Modus Tollendo Ponens/Variant/Formulation 2

:$\vdash \paren {p \lor q} \iff \paren {\neg p \implies q}$

Proof:
We apply the Method of Truth Tables.
As can be seen by inspection, the truth values under the main connective are true for all boolean interpretations.
:<nowiki>$\begin{array}{|ccc|c|cccc|} \hline
p & \lor & q & \iff & \neg & p & \implies & q \\
\hline
\F & \F & \F & \T & \T & \F & \F & \F \\
\F & \T & \T & \T & \T & \F & \T & \T \\
\T & \T & \F & \T & \F & \T & \T & \F \\
\T & \T & \T & \T & \F & \T & \T & \T \\
\hline
\end{array}$</nowiki>
{{qed}}
Theorem: Modus Tollendo Ponens/Variant/Formulation 1

:$p \lor q \dashv \vdash \neg p \implies q$

Proof:
We apply the Method of Truth Tables.
As can be seen by inspection, the truth values under the main connectives match for all boolean interpretations.
:<nowiki>$\begin{array}{|ccc||cccc|} \hline
p & \lor & q & \neg & p & \implies & q \\
\hline
\F & \F & \F & \T & \F & \F & \F \\
\F & \T & \T & \T & \F & \T & \T \\
\T & \T & \F & \F & \T & \T & \F \\
\T & \T & \T & \F & \T & \T & \T \\
\hline
\end{array}$</nowiki>
{{qed}}
Theorem: Modus Tollendo Ponens/Variant/Formulation 1/Forward Implication

:$p \lor q \vdash \neg p \implies q$

Proof:
{{BeginTableau|p \lor q \vdash \neg p \implies q}}
{{Premise|1|p \lor q}}
{{Assumption|2|p|Pick the first of the disjuncts ...}}
{{Assumption|3|\neg p|Assume its negation ...}}
{{NonContradiction|4|2, 3|2|3|... which introduces a contradiction}}
{{Explosion|5|2, 3|q|4| ... from a falsehood, ''any'' statement can be derived - pick $q$}}
{{Implication|6|2|\neg p \implies q|3|5}}
{{Assumption|7|q|Pick the second of the disjuncts ...}}
{{Assumption|8|\neg p|... again assume the negation of $p$}}
{{IdentityLaw|9|7|q|7|$q$ still holds}}
{{Implication|10|7|\neg p \implies q|8|9}}
{{ProofByCases|11|1|\neg p \implies q|1|2|6|7|10}}
{{EndTableau}}
{{qed}}
Category:Modus Tollendo Ponens
4cs2ci8pnukzednwbx1w4bdyc16iswy
Theorem: Modus Tollendo Ponens/Variant/Formulation 1/Reverse Implication

:$\neg p \implies q \vdash p \lor q$

Proof:
{{BeginTableau|\neg p \implies q \vdash p \lor q}}
{{Premise|1|\neg p \implies q}}
{{ExcludedMiddle|2|p \lor \neg p}}
{{Assumption|3|p}}
{{Addition|4|3|p \lor q|3|1}}
{{Assumption|5|\neg p}}
{{ModusPonens|6|1, 5|q|1|5}}
{{Addition|7|1, 5|p \lor q|6|2}}
{{ProofByCases|8|1|p \lor q|2|3|4|5|7}}
{{EndTableau|qed}}
{{LEM}}
Theorem: Radius of Convergence of Power Series over Factorial/Complex Case

Let $\xi \in \C$ be a complex number.
Let $\ds \map f z = \sum_{n \mathop = 0}^\infty \dfrac {\paren {z - \xi}^n} {n!}$.
Then $\map f z$ converges absolutely for all $z \in \C$.
That is, the radius of convergence of the power series $\ds \sum_{n \mathop = 0}^\infty \frac {\paren {z - \xi}^n} {n!}$ is infinite.

Proof:
This is a power series in the form $\ds \sum_{n \mathop = 0}^\infty a_n \paren {z - \xi}^n$ where $\sequence {a_n} = \sequence {\dfrac 1 {n!} }$.
Applying Radius of Convergence from Limit of Sequence: Complex Case, we find that:
{{begin-eqn}}
{{eqn | l = \lim_{n \mathop \to \infty} \cmod {\dfrac {a_{n + 1} } {a_n} }
      | r = \lim_{n \mathop \to \infty} \cmod {\dfrac {\frac 1 {\paren {n + 1}!} } {\frac 1 {n!} } }
      | c = 
}}
{{eqn | r = \lim_{n \mathop \to \infty} \cmod {\dfrac {n!} {\paren {n + 1}!} }
      | c = 
}}
{{eqn | r = \lim_{n \mathop \to \infty} \cmod {\dfrac 1 {n + 1} }
      | c = 
}}
{{eqn | r = 0
      | c = Sequence of Powers of Reciprocals is Null Sequence
}}
{{end-eqn}}
Hence the result.
{{qed}}
Theorem: Radius of Convergence of Power Series over Factorial/Real Case

Let $\xi \in \R$ be a real number.
Let $\ds \map f x = \sum_{n \mathop = 0}^\infty \frac {\paren {x - \xi}^n} {n!}$.
Then $\map f x$ converges for all $x \in \R$.
That is, the interval of convergence of the power series $\ds \sum_{n \mathop = 0}^\infty \frac {\paren {x - \xi}^n} {n!}$ is $\R$.

Proof:
This is a power series in the form $\ds \sum_{n \mathop= 0}^\infty a_n \paren {x - \xi}^n$ where $\sequence {a_n} = \sequence {\dfrac 1 {n!} }$.
Applying Radius of Convergence from Limit of Sequence, we find that:
{{begin-eqn}}
{{eqn | l = \lim_{n \mathop \to \infty} \size {\dfrac {a_{n + 1} } {a_n} }
      | r = \lim_{n \mathop \to \infty} \size {\dfrac {\dfrac 1 {\paren {n + 1}!} } {\dfrac 1 {n!} } }
      | c = 
}}
{{eqn | r = \lim_{n \mathop \to \infty} \size {\dfrac {n!} {\paren {n + 1}!} }
      | c = 
}}
{{eqn | r = \lim_{n \mathop \to \infty} \size {\dfrac 1 {n + 1} }
      | c = 
}}
{{eqn | r = 0
      | c = Sequence of Powers of Reciprocals is Null Sequence
}}
{{end-eqn}}
Hence the result.
{{qed}}
Theorem: Sum of Logarithms/Natural Logarithm

Let $x, y \in \R$ be strictly positive real numbers.
Then:
:$\ln x + \ln y = \map \ln {x y}$
where $\ln$ denotes the natural logarithm.

Proof:
Let $y \in \R_{>0}$ be fixed.
Consider the function:
:$\map f x = \ln x y - \ln x$
From the definition of the natural logarithm, the Fundamental Theorem of Calculus and the Chain Rule for Derivatives:
:$\forall x > 0: \map {f'} x = \dfrac 1 {x y} y - \dfrac 1 x = \dfrac 1 x - \dfrac 1 x = 0$
Thus from Zero Derivative implies Constant Function, $f$ is constant:
:$\forall x > 0: \ln x y - \ln x = c$
To determine the value of $c$, put $x = 1$.
From Logarithm of 1 is 0:
:$\ln 1 = 0$
Thus:
:$c = \ln y - \ln 1 = \ln y$
and hence the result.
{{qed}}
Theorem: Sum of Logarithms/Natural Logarithm

Let $x, y \in \R$ be strictly positive real numbers.
Then:
:$\ln x + \ln y = \map \ln {x y}$
where $\ln$ denotes the natural logarithm.

Proof:
{{begin-eqn}}
{{eqn | l = \ln x + \ln y
      | r = \int_1^x \dfrac {\d t} t + \int_1^y \dfrac {\d s} s
      | c = {{Defof|Natural Logarithm}}
}}
{{eqn | r = \int_1^x \dfrac {\d t} t + \int_x^{x y} \dfrac {\d t / x} {t / x}
      | c = Integration by Substitution: $s \mapsto t / x$, $\d s \mapsto \d t / x$, $1 \mapsto x$, $y \mapsto x y$
}}
{{eqn | r = \int_1^x \dfrac {\d t} t + \int_x^{x y} \dfrac {\d t} t
      | c = simplifying
}}
{{eqn | r = \int_1^{x y} \dfrac {\d t} t
      | c = Sum of Integrals on Adjacent Intervals for Continuous Functions
}}
{{eqn | r = \ln x y
      | c = {{Defof|Natural Logarithm}}
}}
{{end-eqn}}
{{qed}}
Theorem: Sum of Logarithms/Natural Logarithm

Let $x, y \in \R$ be strictly positive real numbers.
Then:
:$\ln x + \ln y = \map \ln {x y}$
where $\ln$ denotes the natural logarithm.

Proof:
Let $\sequence {f_n}$ be the sequence of mappings $f_n : \R_{>0} \to \R$ defined as:
:$\map {f_n} x = n \paren {\sqrt [n] x - 1}$
Let $\map M t = \max \set {\size {t - 1}, \size {\dfrac {t - 1} t} }$
From Bounds of Natural Logarithm:
:$\forall t \in \R_{>0}: \size {\map {f_n} t} \le \map M t$
Fix $x, y \in \R_{>0}$.
Then:
{{begin-eqn}}
{{eqn | l = \size {\map {f_n} {x y} - \paren {\map {f_n} x + \map {f_n} x} }
      | r = \size {n \paren {\sqrt [n] {x y} - 1 - \sqrt [n] x + 1 - \sqrt [n] y + 1} }
      | c = Definition of $\map {f_n} x$
}}
{{eqn | r = n \size {\sqrt [n] {x y} - \sqrt [n] x - \sqrt [n] y + 1}
      | c = Absolute Value Function is Completely Multiplicative
}}
{{eqn | r = n \size {\sqrt [n] x - 1} \size {\sqrt [n] y - 1}
      | c = Absolute Value Function is Completely Multiplicative
}}
{{eqn | r = n \frac {\size {\map {f_n} x} } n \frac {\size {\map {f_n} y} } n
      | c = Definition of $\map {f_n} x$
}}
{{eqn | r = \frac 1 n \size {\map {f_n} x} \size {\map {f_n} y}
}}
{{eqn | o = \le
      | r = \frac {\map M x \map M y} n
      | c = Inequality of Product of Unequal Numbers
}}
{{eqn | ll= \leadsto
      | l = \size {\map \ln {x y} - \paren  {\map \ln x + \map \ln y} }
      | r = \size {\lim_{n \mathop \to \infty} \map {f_n} {x y} - \paren {\lim_{n \mathop \to \infty} \map {f_n} x + \lim_{n \mathop \to \infty} \map {f_n} y} }
}}
{{eqn | r = \lim_{n \mathop \to \infty} \size {\map {f_n} {x y} - \paren {\map {f_n} x + \map {f_n} y} }
      | c = Modulus of Limit
}}
{{eqn | o = \le
      | r = \lim_{n \mathop \to \infty} \frac {\map M x \map M y} n
      | c = Limit of Bounded Convergent Sequence is Bounded
}}
{{eqn | r = \map M x \map M y \lim_{n \mathop \to \infty} \frac 1 n
      | c = Multiple Rule for Real Sequences
}}
{{eqn | r = 0
}}
{{end-eqn}}
Thus:
:$\ds \lim_{n \mathop \to \infty} \map {f_n} {x y} = \lim_{n \mathop \to \infty} \paren {\map {f_n} x + \map {f_n} y}$
Hence the result, from the definition of $\ln$.
{{qed}}
Theorem: Sum of Logarithms/Natural Logarithm

Let $x, y \in \R$ be strictly positive real numbers.
Then:
:$\ln x + \ln y = \map \ln {x y}$
where $\ln$ denotes the natural logarithm.

Proof:
Recall the definition of the natural logarithm as the definite integral of the reciprocal function:
:$\ds \ln x := \int_1^x \frac {\d t} t$
:800px
Consider the diagram above.
The value of $\ln x$ is represented by the area between the points:
:$\tuple {1, 0}, \tuple {1, 1}, \tuple {x, \dfrac 1 x}, \tuple {x, 0}$
which is represented by the yellow region above.
Similarly, the value of $\ln y$ is represented by the area between the points:
:$\tuple {1, 0}, \tuple {1, 1}, \tuple {y, \dfrac 1 y}, \tuple {y, 0}$
Let the second of these areas be transformed by dividing its height by $x$ and multiplying its length by $x$.
This will preserve its area, while making it into the area between the points:
:$\tuple {x, 0}, \tuple {x, 1 / x}, \tuple {x y, \dfrac 1 {x y} }, \tuple {x y, 0}$
which is exactly the green area.
The total of the green and yellow areas represents the value of $\ln x y$.
{{qed}}
Theorem: Sum of Logarithms/Natural Logarithm

Let $x, y \in \R$ be strictly positive real numbers.
Then:
:$\ln x + \ln y = \map \ln {x y}$
where $\ln$ denotes the natural logarithm.

Proof:
{{begin-eqn}}
{{eqn | l = x y
      | r = x \times y
      | c = 
}}
{{eqn | ll = \leadsto
      | l = e^{\map \ln {xy} }
      | r = e^{\ln x} \times e^{\ln y}
      | c = Exponential of Natural Logarithm
}}
{{eqn | ll = \leadsto
      | l = e^{\map \ln {xy} }
      | r = e^{\ln x + \ln y}
      | c = Product of Powers
}}
{{eqn | ll = \leadsto
      | l = \map \ln {xy}
      | r = \ln x + \ln y
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Sum of Logarithms/General Logarithm

Let $x, y, b \in \R$ be strictly positive real numbers such that $b > 1$.
Then:
:$\log_b x + \log_b y = \map {\log_b} {x y}$
where $\log_b$ denotes the logarithm to base $b$.

Proof:
{{begin-eqn}}
{{eqn | l = \log_b x + \log_b y
      | r = \map {\log_b} {b^{\log_b x + \log_b y} }
      | c = {{Defof|General Logarithm}}
}}
{{eqn | r = \map {\log_b} {\paren {b^{\log_b x} } \paren {b^{\log_b y} } }
      | c = Product of Powers
}}
{{eqn | r = \map {\log_b} {x y}
      | c = {{Defof|General Logarithm}}
}}
{{end-eqn}}
{{qed}}
Theorem: Sum of Logarithms/General Logarithm

Let $x, y, b \in \R$ be strictly positive real numbers such that $b > 1$.
Then:
:$\log_b x + \log_b y = \map {\log_b} {x y}$
where $\log_b$ denotes the logarithm to base $b$.

Proof:
{{begin-eqn}}
{{eqn | l = \log_b x + \log_b y
      | r = \frac {\ln x} {\ln b} + \frac {\ln y} {\ln b}
      | c = Change of Base of Logarithm
}}
{{eqn | r = \frac {\ln x + \ln y} {\ln b}
      | c = 
}}
{{eqn | r = \frac {\map \ln {x y} } {\ln b}
      | c = Sum of Logarithms: Proof for Natural Logarithm
}}
{{eqn | r = \map {\log_b} {x y}
      | c = Change of Base of Logarithm
}}
{{end-eqn}}
{{qed}}
Theorem: Rule of Simplification/Sequent Form

The '''rule of simplification''' can be symbolised by the sequents:

Proof:
{{BeginTableau|p \land q \vdash p}}
{{Premise|1|p \land q}}
{{Simplification|2|1|p|1|1}}
{{EndTableau|qed}}
Theorem: Rule of Simplification/Sequent Form

The '''rule of simplification''' can be symbolised by the sequents:

Proof:
We apply the Method of Truth Tables.
:<nowiki>$\begin{array}{|ccc||c|} \hline
p & \land & q & p \\
\hline
\F & \F & \F & \F \\
\F & \F & \T & \F \\
\T & \F & \F & \T \\
\T & \T & \T & \T \\
\hline
\end{array}$</nowiki>
As can be seen, when $p \land q$ is true so is $p$.
{{qed}}
Theorem: Rule of Simplification/Sequent Form

The '''rule of simplification''' can be symbolised by the sequents:

Proof:
{{BeginTableau|p \land q \vdash q}}
{{Premise|1|p \land q}}
{{Simplification|2|1|q|1|2}}
{{EndTableau}}
{{Qed}}
Theorem: Rule of Simplification/Sequent Form

The '''rule of simplification''' can be symbolised by the sequents:

Proof:
We apply the Method of Truth Tables.
:<nowiki>$\begin{array}{|ccc||c|} \hline
p & \land & q & q \\
\hline
\F & \F & \F & \F \\
\F & \F & \T & \T \\
\T & \F & \F & \F \\
\T & \T & \T & \T \\
\hline
\end{array}$</nowiki>
As can be seen, when $p \land q$ is true so is $q$.
{{qed}}
Theorem: Rule of Simplification/Sequent Form

The '''rule of simplification''' can be symbolised by the sequents:

Proof:
We apply the Method of Truth Tables.
:<nowiki>$\begin {array} {|ccc||c|c|} \hline
p & \land & q & p & q \\
\hline
\F & \F & \F & \F & \F \\
\F & \F & \T & \F & \T \\
\T & \F & \F & \T & \F \\
\T & \T & \T & \T & \T \\
\hline
\end {array}$</nowiki>
As can be seen, when $p \land q$ is true so are both $p$ and $q$.
{{qed}}
Theorem: Rule of Simplification/Sequent Form

The '''rule of simplification''' can be symbolised by the sequents:

Proof:
=== Form 1 ===
{{:Rule of Simplification/Sequent Form/Formulation 2/Proof 1/Form 1}}
=== Form 2 ===
{{:Rule of Simplification/Sequent Form/Formulation 2/Proof 1/Form 2}}
Theorem: Rule of Simplification/Sequent Form

The '''rule of simplification''' can be symbolised by the sequents:

Proof:
We apply the Method of Truth Tables.
As can be seen by inspection, the truth values under the main connective are true for all boolean interpretations.
:<nowiki>$\begin{array}{|ccc|c|c||c|c|} \hline
p & \land & q & p & q & p \land q \implies p & p \land q \implies q \\
\hline
\F & \F & \F & \F & \F & \T & \T \\
\F & \F & \T & \F & \T & \T & \T \\
\T & \F & \F & \T & \F & \T & \T \\
\T & \T & \T & \T & \T & \T & \T \\
\hline
\end{array}$</nowiki>
{{qed}}
Theorem: Rule of Conjunction/Sequent Form

The Rule of Conjunction can be symbolised in sequent form as follows:

Proof:
{{BeginTableau|p, q \vdash p \land q}}
{{Premise|1|p}}
{{Premise|2|q}}
{{Conjunction|3|1, 2|p \land q|1|2}}
{{EndTableau|qed}}
Theorem: Rule of Conjunction/Sequent Form

The Rule of Conjunction can be symbolised in sequent form as follows:

Proof:
We apply the Method of Truth Tables.
$\begin{array}{|c|c||ccc|} \hline
p & q & p & \land & q\\
\hline
\F & \F & \F & \F & \F \\
\F & \T & \F & \F & \T \\
\T & \F & \T & \F & \F \\
\T & \T & \T & \T & \T \\
\hline
\end{array}$
As can be seen, only when both $p$ and $q$ are true, then so is $p \land q$.
{{qed}}
Theorem: Radius of Convergence of Derivative of Complex Power Series

Let $\xi \in \C$.
For all $z \in \C$, define the power series:
:$\ds \map S z = \sum_{n \mathop = 0}^\infty a_n \paren {z - \xi}^n$
and:
:$\ds \map {S'} z = \sum_{n \mathop = 1}^\infty n a_n \paren {z - \xi}^{n - 1}$
Let $R$ be the radius of convergence of $\map S z$, and let $R'$ be the radius of convergence of $\map {S'} z$.
Then $R = R'$.

Proof:
Suppose that $z \in \C$ with $\cmod {z - \xi} < R'$.
Then $\map {S'} z$ converges absolutely by Existence of Radius of Convergence of Complex Power Series, so:
{{begin-eqn}}
{{eqn | l = 1
      | o = \ge
      | r = \limsup_{n \mathop \to \infty} \cmod {n a_n \paren {z - \xi}^{n - 1} }^{1 / n}
      | c = $n$th Root Test
}}
{{eqn | o = >
      | r = \limsup_{n \mathop \to \infty} \cmod {a_n \paren {z - \xi}^n }^{1/n}
      | c = as $\cmod {n  \paren {z - \xi}^{n - 1} } > \cmod { \paren {z - \xi}^n }$ for all $n > \cmod {z - \xi}$
}}
{{end-eqn}}
From the $n$th Root Test, it follows that $S \paren z$ converges absolutely.
Hence, $R \ge R'$.
{{qed|lemma}}
Suppose that $z \in \C$ with $\cmod {z - \xi} < R$.
Find $z_o \in \C$ such that $\cmod {z - \xi} < \cmod {z_0 - \xi} < R$.
By Existence of Radius of Convergence of Complex Power Series, $\map S {z_0}$ converges absolutely.
From the $n$th Root Test, it follows that $\cmod {a_n \paren {z_0 - \xi}^n}^{1/n} < 1$ for all $n \ge N$ for some $N \in \N$.
Then:
{{begin-eqn}}
{{eqn | l = 1
      | r = \lim_{n \mathop \to \infty} \cmod n^{1/n}
      | c =  Limit of Integer to Reciprocal Power
}}
{{eqn | o = >
      | r = \lim_{n \mathop \to \infty} \cmod n^{1/n} \cmod {\frac {z - \xi} {z_0 - \xi} }
}}
{{eqn | r = \lim_{n \mathop \to \infty} \cmod n^{1/n} \lim_{n \mathop \to \infty} \cmod {\frac {z - \xi} {z_0 - \xi} }^{\paren {n - 1}/n}
}}
{{eqn | r = \lim_{n \mathop \to \infty} \cmod {n \paren {\frac {z - \xi} {z_0 - \xi} }^{n - 1} }^{1/n}
      | c = Product Rule for Sequences, Complex Modulus of Product of Complex Numbers
}}
{{eqn | o = \ge
      | r = \lim_{n \mathop \to \infty} \cmod {n \paren {\frac {z - \xi} {z_0 - \xi} }^{n - 1} } \limsup_{n \mathop \to \infty} \cmod {a_n \paren {z_0 - \xi}^{n - 1} }^{1/n}
      | c = $n$th Root Test, as remarked above
}}
{{eqn | o = \ge
      | r = \limsup_{n \mathop \to \infty} \cmod {n \paren {\frac {z - \xi} {z_0 - \xi} }^{n - 1} a_n \paren {z_0 - \xi}^{n - 1} }^{1/n}
}}
{{eqn | r = \limsup_{n \mathop \to \infty} \cmod {n a_n \paren {z - \xi}^{n - 1} }^{1/n}
}}
{{end-eqn}}
From the $n$th Root Test, it follows that $\map {S'} z$ converges absolutely.
Hence, $R' \ge R$, so $R' = R$.
{{qed}}
Theorem: Rule of Addition/Sequent Form

The '''rule of addition''' can be symbolised by the sequents:
{{begin-eqn}}
{{eqn | n = 1
      | l = p
      | o = 
}}
{{eqn | ll= \vdash 
      | l = p \lor q
      | o = 
}}
{{end-eqn}}
{{begin-eqn}}
{{eqn | n = 2
      | l = q
      | o = 
}}
{{eqn | ll= \vdash 
      | l = p \lor q
      | o = 
}}
{{end-eqn}}

Proof:
{{BeginTableau|q \vdash p \lor q}}
{{Premise|1|q}}
{{Addition|2|1|p \lor q|1|2}}
{{EndTableau|qed}}
Theorem: Rule of Addition/Sequent Form

The '''rule of addition''' can be symbolised by the sequents:
{{begin-eqn}}
{{eqn | n = 1
      | l = p
      | o = 
}}
{{eqn | ll= \vdash 
      | l = p \lor q
      | o = 
}}
{{end-eqn}}
{{begin-eqn}}
{{eqn | n = 2
      | l = q
      | o = 
}}
{{eqn | ll= \vdash 
      | l = p \lor q
      | o = 
}}
{{end-eqn}}

Proof:
{{BeginTableau|p \vdash p \lor q}}
{{Premise|1|p}}
{{Addition|2|1|p \lor q|1|1}}
{{EndTableau|qed}}
Theorem: Rule of Addition/Sequent Form

The '''rule of addition''' can be symbolised by the sequents:
{{begin-eqn}}
{{eqn | n = 1
      | l = p
      | o = 
}}
{{eqn | ll= \vdash 
      | l = p \lor q
      | o = 
}}
{{end-eqn}}
{{begin-eqn}}
{{eqn | n = 2
      | l = q
      | o = 
}}
{{eqn | ll= \vdash 
      | l = p \lor q
      | o = 
}}
{{end-eqn}}

Proof:
We apply the Method of Truth Tables.
$\begin{array}{|c||ccc|} \hline
p & p & \lor & q \\
\hline
\F & \F & \F & \F \\
\F & \F & \T & \T \\
\T & \T & \T & \F \\
\T & \T & \T & \T \\
\hline
\end{array}$
As can be seen, when $p$ is true so is $p \lor q$.
{{qed}}
Theorem: Rule of Addition/Sequent Form

The '''rule of addition''' can be symbolised by the sequents:
{{begin-eqn}}
{{eqn | n = 1
      | l = p
      | o = 
}}
{{eqn | ll= \vdash 
      | l = p \lor q
      | o = 
}}
{{end-eqn}}
{{begin-eqn}}
{{eqn | n = 2
      | l = q
      | o = 
}}
{{eqn | ll= \vdash 
      | l = p \lor q
      | o = 
}}
{{end-eqn}}

Proof:
We apply the Method of Truth Tables.
:<nowiki>$\begin{array}{|c||ccc|} \hline
q & p & \lor & q \\
\hline
\F & \F & \F & \F \\
\T & \F & \T & \T \\
\F & \T & \T & \F \\
\T & \T & \T & \T \\
\hline
\end{array}$</nowiki>
As can be seen, when $q$ is true so is $p \lor q$.
{{qed}}
Theorem: Rule of Addition/Sequent Form

The '''rule of addition''' can be symbolised by the sequents:
{{begin-eqn}}
{{eqn | n = 1
      | l = p
      | o = 
}}
{{eqn | ll= \vdash 
      | l = p \lor q
      | o = 
}}
{{end-eqn}}
{{begin-eqn}}
{{eqn | n = 2
      | l = q
      | o = 
}}
{{eqn | ll= \vdash 
      | l = p \lor q
      | o = 
}}
{{end-eqn}}

Proof:
{{BeginTableau|p \implies \paren {p \lor q} }}
{{Premise|1|p}}
{{Addition|2|1|p \lor q|1|1}}
{{Implication|3||p \implies \paren {p \lor q}|1|3}}
{{EndTableau}}
{{Qed}}