avewright/proofwiki-math huggingface dataset:
Theorem: Absolute Value of Components of Complex Number no greater than Root 2 of Modulus

Let $z = x + i y \in \C$ be a complex number.
Then:
:$\size x + \size y \le \sqrt 2 \cmod z$
where:
:$\size x$ and $\size y$ denote the absolute value of $x$ and $y$
:$\cmod z$ denotes the complex modulus of $z$.

Proof:
Let $z = x + i y \in \C$ be an arbitrary complex number.
{{AimForCont}} the contrary:
{{begin-eqn}}
{{eqn | l = \size x + \size y
      | o = >
      | r = \sqrt 2 \cmod z
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \paren {\size x + \size y}^2
      | o = >
      | r = 2 \cmod z^2
      | c = squaring both sides
}}
{{eqn | ll= \leadsto
      | l = \size x^2 + 2 \size x \, \size y + \size y^2
      | o = >
      | r = 2 \cmod z^2
      | c = multiplying out
}}
{{eqn | ll= \leadsto
      | l = x^2 + 2 \size x \, \size y + y^2
      | o = >
      | r = 2 \cmod z^2
      | c = {{Defof|Absolute Value}}
}}
{{eqn | ll= \leadsto
      | l = x^2 + 2 \size x \, \size y + y^2
      | o = >
      | r = 2 \paren {x^2 + y^2}
      | c = {{Defof|Complex Modulus}}
}}
{{eqn | ll= \leadsto
      | l = 2 \size x \, \size y
      | o = >
      | r = x^2 + y^2
      | c = 
}}
{{eqn | ll= \leadsto
      | l = 2 \size x \, \size y
      | o = >
      | r = \size x^2 + \size y^2
      | c = {{Defof|Absolute Value}}
}}
{{eqn | ll= \leadsto
      | l = \size x^2 - 2 \size x \, \size y + \size y^2
      | o = <
      | r = 0
      | c = rearranging
}}
{{eqn | ll= \leadsto
      | l = \paren {\size x - \size y}^2
      | o = <
      | r = 0
      | c = factoring
}}
{{end-eqn}}
But as $\size x$ and $\size y$ are both real this cannot happen.
Thus our initial assumption $\size x + \size y > \sqrt 2 \cmod z$ is false.
Hence the result.
{{qed}}
Theorem: Exclusive Or with Factor of Exclusive Or

:$\paren {p \oplus q} \oplus q \dashv \vdash p$

Proof:
{{begin-eqn}}
{{eqn | l = \paren {p \oplus q} \oplus q
      | o = \dashv \vdash
      | r = p \oplus \paren {q \oplus q}
      | c = Exclusive Or is Associative
}}
{{eqn | o = \dashv \vdash
      | r = p \oplus \bot
      | c = Exclusive Or with Itself
}}
{{eqn | o = \dashv \vdash
      | r = p
      | c = Exclusive Or with Contradiction
}}
{{end-eqn}}
{{qed}}
Theorem: Biconditional with Factor of Biconditional

:$\paren {p \iff q} \iff q \dashv \vdash p$

Proof:
{{begin-eqn}}
{{eqn | l = \paren {p \iff q} \iff q
      | o = \dashv \vdash
      | r = p \iff \paren {q \iff q}
      | c = Biconditional is Associative
}}
{{eqn | o = \dashv \vdash
      | r = p \iff \top
      | c = Biconditional with Itself
}}
{{eqn | o = \dashv \vdash
      | r = p
      | c = Biconditional with Tautology
}}
{{end-eqn}}
{{qed}}
Theorem: Conditional iff Biconditional of Antecedent with Conjunction

:$p \implies q \dashv \vdash p \iff \paren {p \land q}$

Proof:
We apply the Method of Truth Tables.
As can be seen by inspection, the appropriate truth values match for all boolean interpretations.
$\begin{array}{|ccc||ccccc|} \hline
p & \implies & q & p & \iff & (p & \land & q) \\
\hline
\F & \T & \F & \F & \T & \F & \F & \F \\
\F & \T & \T & \F & \T & \F & \F & \T \\
\T & \F & \F & \T & \F & \T & \F & \F \\
\T & \T & \T & \T & \T & \T & \T & \T \\
\hline
\end{array}$
{{qed}}
Theorem: Conditional iff Biconditional of Consequent with Disjunction

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

Proof:
We apply the Method of Truth Tables.
As can be seen by inspection, the appropriate truth values match for all boolean interpretations.
$\begin{array}{|ccc||ccccc|} \hline
p & \implies & q & q & \iff & (p & \lor & q) \\
\hline
\F & \T & \F & \F & \T & \F & \F & \F \\
\F & \T & \T & \T & \T & \F & \T & \T \\
\T & \F & \F & \F & \F & \T & \T & \F \\
\T & \T & \T & \T & \T & \T & \T & \T \\
\hline
\end{array}$
{{qed}}
Theorem: Conjunction iff Biconditional of Biconditional with Disjunction

:$p \land q \dashv \vdash \paren {p \iff q} \iff \paren {p \lor q}$

Proof:
We apply the Method of Truth Tables.
As can be seen by inspection, the appropriate truth values match for all boolean interpretations.
$\begin{array}{|ccc||ccccccc|} \hline
p & \land & q & (p & \iff & q) & \iff & (p & \lor & q) \\
\hline
\F & \F & \F & \F & \T & \F & \F & \F & \F & \F \\
\F & \F & \T & \F & \F & \T & \F & \F & \T & \T \\
\T & \F & \F & \T & \F & \F & \F & \T & \T & \F \\
\T & \T & \T & \T & \T & \T & \T & \T & \T & \T \\
\hline
\end{array}$
{{qed}}
Theorem: Functionally Incomplete Logical Connectives/Conjunction and Disjunction

:$\set {\land, \lor}$: And and Or

Proof:
Let $v_T$ be the boolean interpretation that assigns $T$ to each propositional symbol.
Then it follows by the nature of the truth functions for $\land$ and $\lor$ that:
:$\map {v_T} {\mathbf A} = T$
for each WFF $\mathbf A$ comprising only $\land$ and $\lor$.
On the other hand:
:$\map {v_T} {\neg p} = F$
Therefore, $\neg p$ cannot be expressed in terms of $\land$ and $\lor$.
Hence, $\set {\land, \lor}$ is not functionally complete.
{{qed}}
Theorem: Functionally Incomplete Logical Connectives/Negation and Biconditional

:$\set {\neg, \iff}$: Not and Iff

Proof:
Let $\mathbf A$ be a WFF comprising only the logical connectives $\neg$ and $\iff$.
The central claim to this proof is that:
:The number of models for $\mathbf A$ is even.
In this claim, we disregard the obvious exceptions of the form $\neg \cdots \neg p$.
Firstly, note that including any propositional symbols not occurring in $\mathbf A$ in the truth table for $\mathbf A$ simply doubles the number of boolean interpretations modelling $\mathbf A$.
Next, it is obvious that if the number of models of $\mathbf A$ is even, then this also holds for $\neg \mathbf A$.
For, by Count of Truth Functions, the total number of boolean interpretations is even.
Lastly, to consider $\mathbf A = \mathbf A_1 \iff \mathbf A_2$.
Suppose that the claim were verified for $\mathbf A_1$ and $\mathbf A_2$.
Then we have the following identities:
:$\set {v \mid \map v {\mathbf A_1} = T} = \set {v \mid \map v {\mathbf A_1} = T, \map v {\mathbf A_2} = F} \cup \set {v \mid \map v {\mathbf A_1} = T, \map v {\mathbf A_2} = T}$
:$\set {v \mid \map v {\mathbf A_1} = F} = \set {v \mid \map v {\mathbf A_1} = F, \map v {\mathbf A_2} = F} \cup \set {v \mid \map v {\mathbf A_1} = F, \map v {\mathbf A_2} = T}$
:$\set {v \mid \map v {\mathbf A_2} = T} = \set {v \mid \map v {\mathbf A_1} = T, \map v {\mathbf A_2} = T} \cup \set {v \mid \map v {\mathbf A_1} = F, \map v {\mathbf A_2} = T}$
:$\set {v \mid \map v {\mathbf A_2} = F} = \set {v \mid \map v {\mathbf A_1} = T, \map v {\mathbf A_2} = F} \cup \set {v \mid \map v {\mathbf A_1} = F, \map v {\mathbf A_2} = F}$
The sets on the {{RHS}} are disjoint, while the sets on the {{LHS}} have an even number of elements.
Therefore, the parity of the cardinalities of the sets on the {{RHS}} must be equal.
Then combining the first and fourth equations, the sets:
:$\set {v \mid \map v {\mathbf A_1} = T, \map v {\mathbf A_2} = T}$
:$\set {v \mid \map v {\mathbf A_1} = F, \map v {\mathbf A_2} = F}$ 
have equal parity.
Together, these two constitute the set of models for $\mathbf A$, as can be seen from the boolean interpretation of $\iff$.
Therefore, the number of models for $\mathbf A$ is even.
This completes the proof of the claim.
On the other hand, the truth table of $p \implies q$ has three entries $F$, and one $T$.
Therefore, $p \implies q$ cannot be expressed in terms of $\neg$ and $\iff$.
Hence, $\set {\neg, \iff}$ is not functionally complete.
{{qed}}
Theorem: Theory of Set of Formulas is Theory

Let $\LL$ be a logical language.
Let $\mathscr M$ be a formal semantics for $\LL$.
Let $\FF$ be a set of $\LL$-formulas.
Let $\map T \FF$ be the $\LL$-theory of $\FF$.
Then $\map T \FF$ is a theory.

Proof:
Let $\phi$ be a $\LL$-formula.
Suppose that $\map T \FF \models_{\mathscr M} \phi$.
By definition of $\map T \FF$:
:$\FF \models_{\mathscr M} \psi$
for every $\psi \in \map T \FF$.
Hence by definition of semantic consequence:
:$\FF \models_{\mathscr M} \map T \FF$
By Semantic Consequence is Transitive, it follows that:
:$\FF \models_{\mathscr M} \phi$
Finally, by definition of $\map T \FF$:
:$\phi \in \map T \FF$.
Since $\phi$ was arbitrary, the result follows.
{{qed}}
Theorem: Semantic Consequence is Transitive

Let $\LL$ be a logical language.
Let $\mathscr M$ be a formal semantics for $\LL$.
Let $\FF, \GG$ and $\HH$ be sets of $\LL$-formulas.
Suppose that:
{{begin-eqn}}
{{eqn | l = \FF
      | o = \models_{\mathscr M}
      | r = \GG
}}
{{eqn | l = \GG
      | o = \models_{\mathscr M}
      | r = \HH
}}
{{end-eqn}}
Then $\FF \models_{\mathscr M} \HH$.

Proof:
Let $\MM$ be an $\mathscr M$-structure.
By assumption, if $\MM$ is a model of $\FF$, it is one of $\GG$ as well.
But any model of $\GG$ is also a model of $\HH$.
In conclusion, any model of $\FF$ is also a model of $\HH$.
Hence the result, by definition of semantic consequence.
{{qed}}
Category:Formal Semantics
ekmhdnpnyes5y94jgh51nzbii93l2at
Theorem: Lemniscate of Bernoulli as Locus in Complex Plane

The locus of $z$ on the complex plane such that:
:$\cmod {z - a} \cmod {z + a} = a^2$
is a lemniscate of Bernoulli.

Proof:
{{begin-eqn}}
{{eqn | l = \cmod {z - a} \cmod {z + a}
      | r = a^2
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \paren {\paren {x - a}^2 + y^2} \paren {\paren {x + a}^2 + y^2}
      | r = a^4
      | c = {{Defof|Complex Modulus}}
}}
{{eqn | ll= \leadsto
      | l = \paren {x^2 - 2 a x + a^2 + y^2} \paren {x^2 + 2 a x + a^2 + y^2}
      | r = a^4
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \paren {\paren {x^2 + a^2 + y^2} - 2 a x} \paren {\paren {x^2 + a^2 + y^2} + 2 a x}
      | r = a^4
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \paren {x^2 + a^2 + y^2}^2 - 4 a^2 x^2
      | r = a^4
      | c = Difference of Two Squares
}}
{{eqn | ll= \leadsto
      | l = \paren {x^2 + y^2}^2 + a^4 + 2 \paren {x^2 + y^2} a^2 - 4 a^2 x^2
      | r = a^4
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \paren {x^2 + y^2}^2 + 2 a^2 \paren {x^2 - 2 x^2 + y^2}
      | r = 0
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \paren {x^2 + y^2}^2 + 2 a^2 \paren {y^2 - x^2}
      | r = 0
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \paren {x^2 + y^2}^2
      | r = 2 a^2 \paren {x^2 - y^2}
      | c = 
}}
{{end-eqn}}
which is the equation defining a lemniscate of Bernoulli with major semiaxis $a \sqrt 2$.
{{qed}}
Theorem: Product of Tangent and Cotangent

:$\tan \theta \cot \theta = 1$

Proof:
{{begin-eqn}}
{{eqn | l = \tan \theta \cot \theta
      | r = \frac {\sin \theta} {\cos \theta} \cot \theta
      | c = Tangent is Sine divided by Cosine
}}
{{eqn | r = \frac {\sin \theta} {\cos \theta} \frac {\cos \theta} {\sin \theta}
      | c = Cotangent is Cosine divided by Sine
}}
{{eqn | r = \frac {\sin \theta} {\sin \theta} \frac {\cos \theta} {\cos \theta}
      | c = 
}}
{{eqn | r = 1
      | c = 
}}
{{end-eqn}}
{{qed}}
Category:Tangent Function
Category:Cotangent Function
46j184iwn1vblxlg7w7srw5q3g4jcc2
Theorem: Product of Cotangents of Fractions of Pi

Let $m \in \Z$ such that $m > 1$.
Then:
:$\ds \prod_{k \mathop = 1}^{m - 1} \cot \frac {k \pi} {2 m} = 1$

Proof:
We have:
{{begin-eqn}}
{{eqn | l = \frac {k \pi} {2 m} + \frac {\paren {m - k} \pi} {2 m}
      | r = \frac {\paren {k + m - k} \pi} {2 m}
      | c = 
}}
{{eqn | r = \frac \pi 2
      | c = 
}}
{{end-eqn}}
That means:
:$(1): \quad \dfrac \pi 2 - \dfrac {k \pi} {2 m} = \dfrac {\paren {m - k} \pi} {2 m}$
Let $m$ be odd.
Then $m - 1$ is even, and so:
{{begin-eqn}}
{{eqn | l = \prod_{k \mathop = 1}^{m - 1} \cot \frac {k \pi} {2 m}
      | r = \prod_{k \mathop = 1}^{\frac {m - 1} 2} \cot \frac {k \pi} {2 m} \prod_{k \mathop = \frac {m - 1} 2 + 1}^{m - 1} \cot \frac {k \pi} {2 m}
      | c = 
}}
{{eqn | r = \prod_{k \mathop = 1}^{\frac {m - 1} 2} \cot \frac {k \pi} {2 m} \cot \frac {\paren {m - k} \pi} {2 m}
      | c = 
}}
{{eqn | r = \prod_{k \mathop = 1}^{\frac {m - 1} 2} \cot \frac {k \pi} {2 m} \map \cot {\frac \pi 2 - \frac {k \pi} {2 m} }
      | c = from $(1)$
}}
{{eqn | r = \prod_{k \mathop = 1}^{\frac {m - 1} 2} \cot \frac {k \pi} {2 m} \tan \frac {k \pi} {2 m}
      | c = Cotangent of Complement equals Tangent
}}
{{eqn | r = 1
      | c = Product of Tangent and Cotangent
}}
{{end-eqn}}
Now suppose $m$ is even.
Then $m - 1$ is odd, and so:
{{begin-eqn}}
{{eqn | l = \prod_{k \mathop = 1}^{m - 1} \cot \frac {k \pi} {2 m}
      | r = \paren {\prod_{k \mathop = 1}^{\frac m 2 - 1} \cot \frac {k \pi} {2 m} } \frac m 2 \frac \pi {2 m} \paren {\prod_{k \mathop = \frac m 2 + 1}^{m - 1} \cot \frac {k \pi} {2 m} }
      | c = 
}}
{{eqn | r = \paren {\prod_{k \mathop = 1}^{\frac m 2 - 1} \cot \frac {k \pi} {2 m} \cot \frac {\paren {m - k} \pi} {2 m} } \frac \pi 4
      | c = 
}}
{{eqn | r = \paren {\prod_{k \mathop = 1}^{\frac m 2 - 1} \cot \frac {k \pi} {2 m} \map \cot {\frac \pi 2 - \frac {k \pi} {2 m} } } \cot \frac \pi 4
      | c = from $(1)$
}}
{{eqn | r = \paren {\prod_{k \mathop = 1}^{\frac m 2 - 1} \cot \frac {k \pi} {2 m} \tan \frac {k \pi} {2 m} } \cot \frac \pi 4
      | c = Cotangent of Complement equals Tangent
}}
{{eqn | r = 1 \cot \frac \pi 4
      | c = Product of Tangent and Cotangent
}}
{{eqn | r = 1
      | c = Cotangent of $45 \degrees$
}}
{{end-eqn}}
{{qed}}
Theorem: Uncountable Set less Countable Set is Uncountable

Let $S$ be an uncountable set.
Let $T \subseteq S$ be a countable subset of $S$.
Then:
:$S \setminus T$ is uncountable
where $\setminus$ denotes set difference.

Proof:
{{AimForCont}} $S \setminus T$ were countable.
By definition of relative complement:
:$S \setminus T = \relcomp S T$
Thus from Union with Relative Complement:
:$\paren {S \setminus T} \cup T = S$
But from Finite Union of Countable Sets is Countable it follows that $S$ is countable.
From this contradiction it follows that $S \setminus T$ is uncountable.
{{qed}}
{{LEM|Union with Relative Complement}}
Category:Uncountable Sets
Category:Countable Sets
6ihlmj25zzqiff0xm1y2mrt578y9wfj
Theorem: Irrational Numbers are Uncountably Infinite

The set $\R \setminus \Q$ of irrational numbers is uncountable.

Proof:
From Real Numbers are Uncountable, $\R$ is an uncountable set.
From Rational Numbers are Countably Infinite $\Q$ is countable.
The result follows from Uncountable Set less Countable Set is Uncountable.
{{qed}}
{{AoC|Uncountable Set less Countable Set is Uncountable}}
Theorem: Product of Diagonals from Point of Regular Polygon

Let $A_0, A_1, \ldots, A_{n - 1}$ be the vertices of a regular $n$-gon $P = A_0 A_1 \cdots A_{n - 1}$ which is circumscribed by a unit circle.
Then:
:$\ds \prod_{k \mathop = 2}^{n - 2} A_0 A_k = \frac {n \csc^2 \frac \pi n} 4$
where $A_0 A_k$ is the length of the line joining $A_0$ to $A_k$.

Proof:
First it is worth examining the degenerate case $n = 3$, where there are no such lines.
In this case:
{{begin-eqn}}
{{eqn | l = \frac {n \csc^2 \frac \pi n} 4
      | r = \frac 4 3 \csc^2 \frac \pi 3
      | c = 
}}
{{eqn | r = \frac 3 4 \paren {\frac {2 \sqrt 3} 3}^2
      | c = Cosecant of $60 \degrees$
}}
{{eqn | r = 1
      | c = 
}}
{{end-eqn}}
The continued product $\ds \prod_{k \mathop = 2}^{n - 2} A_0 A_k$ is vacuous here.
By convention, such a vacuous product is defined as being equal to $1$.
So the result holds for $n = 3$.
:420px
Let $n > 3$.
The illustration above is a diagram of the case where $n = 7$.
From Complex Roots of Unity are Vertices of Regular Polygon Inscribed in Circle, the vertices of $P$ can be identified with the complex $n$th roots of unity.
Thus:
{{begin-eqn}}
{{eqn | l = \prod_{k \mathop = 2}^{n - 2} A_1 A_k
      | r = \prod_{k \mathop = 2}^{n - 2} \paren {1 - \alpha^k}
      | c = where $\alpha = e^{2 i \pi / n}$ is the first complex $n$th root of unity
}}
{{eqn | r = \dfrac 1 {\paren {1 - \alpha} \paren {1 - \alpha^{n - 1} } } \prod_{k \mathop = 1}^{n - 1} \paren {1 - \alpha^k}
      | c = 
}}
{{eqn | r = \dfrac n {\paren {1 - \alpha} \paren {1 - \alpha^{n - 1} } }
      | c = Product of Differences between 1 and Complex Roots of Unity
}}
{{eqn | r = \dfrac n {\paren {1 - \paren {\cos \frac {2 \pi} n + i \sin \frac {2 \pi} n} } \paren {1 - \paren {\cos \frac {2 \paren {n - 1} \pi} n + i \sin \frac {2 \paren {n - 1} \pi} n} } }
      | c = Definition of $\alpha$
}}
{{eqn | r = \dfrac n {\paren {1 - \paren {\cos \frac {2 \pi} n + i \sin \frac {2 \pi} n} } \paren {1 - \paren {\cos \frac {2 \pi} n - i \sin \frac {2 \pi} n} } }
      | c = 
}}
{{eqn | r = \dfrac n {\paren {1 - \cos \frac {2 \pi} n}^2 + \paren {\sin \frac {2 \pi} n}^2}
      | c = 
}}
{{eqn | r = \dfrac n {1 - 2 \cos \frac {2 \pi} n + \paren {\cos \frac {2 \pi} n}^2 + \paren {\sin \frac {2 \pi} n}^2}
      | c = 
}}
{{eqn | r = \dfrac n {2 - 2 \cos \frac {2 \pi} n}
      | c = Sum of Squares of Sine and Cosine
}}
{{eqn | r = \dfrac n {2 - 2 \paren {1 - 2 \sin^2 \frac \pi n} }
      | c = {{Corollary|Double Angle Formula for Cosine|2}}
}}
{{eqn | r = \dfrac n {2 - 2 + 4 \sin^2 \frac \pi n}
      | c = 
}}
{{eqn | r = \frac {n \csc^2 \frac \pi n} 4
      | c = {{Defof|Cosecant}}
}}
{{end-eqn}}
{{qed}}
Theorem: Condition on Conjugate from Real Product of Complex Numbers

Let $z_1, z_2 \in \C$ be complex numbers such that $z_1 z_2 \in \R_{\ne 0}$.
Then:
:$\exists p \in \R: z_1 = p \overline {z_2}$
where $\overline {z_2}$ denotes the complex conjugate of $z_2$.

Proof:
Let $z_1 = x_1 + i y_1, z_2 = x_2 + i y_2$.
As $z_1 z_2$ is real:
:$(1): \quad z_1 z_2 = x_1 x_2 - y_1 y_2$
and:
:$(2): \quad x_1 y_2 + y_1 x_2 = 0$
So:
{{begin-eqn}}
{{eqn | l = \frac {\paren {z_1} } {\paren {\overline {z_2} } }
      | r = \frac {x_1 + i y_1} {x_2 - i y_2}
      | c = {{Defof|Complex Conjugate}}
}}
{{eqn | r = \frac {\paren {x_1 + i y_1} \paren {x_2 + i y_2} } {\paren {x_2 - i y_2} \paren {x_2 + i y_2} }
      | c = multiplying top and bottom by $x_2 + i y_2$
}}
{{eqn | r = \frac {\paren {x_1 + i y_1} \paren {x_2 + i y_2} } { {x_2}^2 + {y_2}^2}
      | c = Difference of Two Squares and $i^2 = -1$
}}
{{eqn | r = \frac {x_1 x_2 - y_1 y_2} { {x_2}^2 + {y_2}^2}
      | c = from $(1)$
}}
{{end-eqn}}
So $z_1 / \overline {z_2} = p$ where $p = \dfrac {x_1 x_2 - y_1 y_2} { {x_2}^2 + {y_2}^2}$, which is real.
{{qed}}
Theorem: Real Natural Logarithm is Restriction of Complex Natural Logarithm

Let $\ln: \C_{\ne 0} \to \C$ be the complex natural logarithm.
Let $\ln': \R_{>0} \to \R$ be the real natural logarithm.
Then:
:$\ln' = \ln \restriction_{\R_{>0} \times \R}$
That is, the real natural logarithm is the restriction of the complex natural logarithm.

Proof:
From Domain of Real Natural Logarithm:
: $\operatorname{Dom} \left({\ln'}\right) = \R_{>0}$
From Image of Real Natural Logarithm:
: $\operatorname{Im} \left({\ln'}\right) = \R$
Let $z \in \C$ such that $z = x + i y$.
Let $z$ be expressed in exponential form as $z = r e^{i \theta}$.
Let $x > 0$ and $y = 0$.
Thus $z \in \R_{>0}$.
Then:
{{begin-eqn}}
{{eqn | l = \ln z
      | r = \left\{ {\ln' r + i \theta + 2 \pi k i}\right\}
      | c = 
}}
{{eqn | r = \left\{ {\ln' x + 2 \pi k i}\right\}
      | c = as $r = x$ and $\theta = 0$
}}
{{end-eqn}}
In order for $\ln z \in \R$ it is necessary that $k = 0$.
Thus $\ln z = \ln' x$.
Hence the result.
{{qed}}
Category:Natural Logarithms
j4h0xmkgtlc49xsftaqfnqphpm2d3yj
Theorem: Rule of Commutation/Disjunction/Formulation 2/Forward Implication

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

Proof:
Using a tableau proof for instance 1 of a Gentzen proof system:
{| border="1"
|+$\vdash \paren {p \lor q} \implies \paren {q \lor p}$
|-
! Line !!
! Pool
! Formula
! Rule
! Depends upon
! Notes
|-
| 1 || ||
| $\neg p, q, p$
| Axiom || ||
|-
| 2 || ||
| $\neg q, q, p$
| Axiom || ||
|-
| 3 || ||
| $\neg \paren {p \lor q}, q, p$
| $\alpha$-Rule: $\alpha\lor$
| 1, 2 ||
|-
| 4 || ||
| $\neg \paren {p \lor q}, q \lor p$
| $\beta$-Rule: $\beta\lor$
| 3 ||
|-
| 5 || ||
| $\paren {p \lor q} \implies \paren {q \lor p}$
| $\beta$-Rule: $\beta\implies$
| 4 ||
|}
{{qed}}
Theorem: Provable by Gentzen Proof System iff Negation has Closed Tableau/Formula

Let $\mathbf A$ be a WFF of propositional logic.
Then $\mathbf A$ is a $\mathscr G$-theorem {{iff}}:
:$\neg \mathbf A$ has a closed semantic tableau
where $\neg \mathbf A$ is the negation of $\mathbf A$.

Proof:
This is a specific instance of Provable by Gentzen Proof System iff Negation has Closed Tableau: Set of Formulas.
{{qed}}
Theorem: Provable by Gentzen Proof System iff Negation has Closed Tableau/Set of Formulas

Let $U$ be a set of WFFs of propositional logic.
Then:
:$U$ is a $\mathscr G$-theorem
{{iff}}:
:$\bar U$ has a closed semantic tableau
where $\bar U$ is the set comprising the logical complements of all WFFs in $U$.

Proof:
Denote with $\bar{\mathbf A}$ and $\bar U$ the logical complement of a WFF $\mathbf A$ and set $U$, respectively.
Theorem: Domain of Real Natural Logarithm

Let $\ln$ be the natural logarithm function on the real numbers.
Then the domain of $\ln$ is the set of strictly positive real numbers:
:$\Dom \ln = \R_{>0}$

Proof:
By definition of natural logarithm:
:$\ln^{-1} = \exp$
From Exponential Tends to Zero and Infinity:
:$\Dom \exp = \openint {-\infty} {+\infty}$
:$\Img \exp = \openint 0 {+\infty}$
From Exponential is Strictly Increasing:
:$\exp$ is strictly increasing.
From Strictly Monotone Real Function is Bijective, $\exp: \R \to \R_{>0}$ is a bijection.
Thus:
:$\Dom \ln = \Img \exp$
and so $\Dom \ln = \R_{>0}$.
{{qed}}
Category:Natural Logarithms
14154zzvbik35lknflmgrxyz0xxq2th
Theorem: Image of Real Natural Logarithm

Let $\ln$ be the natural logarithm function on the real numbers.
Then the image of $\ln$ is the set of real numbers:
:$\Img \ln = \R$

Proof:
By definition of natural logarithm:
:$\ln^{-1} = \exp$
From Exponential Tends to Zero and Infinity:
:$\Dom \exp = \openint {-\infty} {+\infty}$
:$\Img \exp = \openint 0 {+\infty}$
From Exponential is Strictly Increasing:
:$\exp$ is strictly increasing.
From Strictly Monotone Real Function is Bijective, $\exp: \R \to \R_{>0}$ is a bijection.
Thus:
:$\Img \ln = \Dom \exp$
and so $\Img \ln = \R$.
{{qed}}
Category:Natural Logarithms
4d0rbbqnorxwqsc2hkxxvh1ektnvkzw
Theorem: Soundness and Completeness of Gentzen Proof System

Let $\mathscr G$ be instance 1 of a Gentzen proof system.
Let $\mathrm{BI}$ be the formal semantics of boolean interpretations.
Then $\mathscr G$ is a sound and complete proof system for $\mathrm{BI}$.

Proof:
This is an immediate consequence of:
* Provable by Gentzen Proof System iff Negation has Closed Tableau
* Soundness and Completeness of Semantic Tableaux
{{qed}}