avewright/proofwiki-math huggingface dataset:
Theorem: Lower Closure is Dual to Upper Closure

Let $\left({S, \preccurlyeq}\right)$ be an ordered set.
Let $a, b \in S$.
Let $T \subseteq S$
The following are pairs of dual statements:
:$b \in a^\preccurlyeq$, the lower closure of $a$
:$b \in a^\succcurlyeq$, the upper closure of $a$
:$b \in T^\preccurlyeq$, the lower closure of $T$
:$b \in T^\succcurlyeq$, the upper closure of $T$

Proof:
=== Elements ===
By definition of lower closure, $b \in a^\preccurlyeq$ {{iff}}:
:$b \preccurlyeq a$
The dual of this statement is:
:$a \preccurlyeq b$
by Dual Pairs (Order Theory).
By definition of upper closure, this means $b \in a^\succcurlyeq$.
The converse follows from Dual of Dual Statement (Order Theory).
{{qed|lemma}}
Theorem: Strict Lower Closure is Dual to Strict Upper Closure

Let $\left({S, \preceq}\right)$ be an ordered set.
Let $a, b \in S$.
The following are dual statements:
:$b \in a^\prec$, the strict lower closure of $a$
:$b \in a^\succ$, the strict upper closure of $a$

Proof:
By definition of strict lower closure:
:$b \in a^\prec$
{{iff}}
:$b$ strictly precedes $a$
The dual of this statement is:
:$b$ strictly succeeds $a$
by Dual Pairs (Order Theory).
By definition of strict upper closure, this means:
: $b \in a^\succ$
The converse follows from Dual of Dual Statement (Order Theory).
{{qed}}
Theorem: Join is Dual to Meet

Let $\struct {S, \preceq}$ be an ordered set.
Let $a, b, c \in S$.
The following are dual statements:
:$c = a \vee b$, the join of $a$ and $b$
:$c = a \wedge b$ the meet of $a$ and $b$

Proof:
By definition of join, $c = a \vee b$ {{iff}}:
:$c = \sup \set {a, b}$
where $\sup$ denotes supremum.
The dual of this statement is:
:$c = \inf \set {a, b}$
where $\inf$ denotes infimum, by Dual Pairs (Order Theory).
By definition of meet, this means $c = a \wedge b$.
{{qed}}
Theorem: Self-Distributive Law for Conditional/Formulation 1/Forward Implication

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

Proof:
{{BeginTableau|p \implies \paren {q \implies r} \vdash \paren {p \implies q} \implies \paren {p \implies r} }}
{{Premise|1|p \implies \paren {q \implies r} }}
{{Assumption|2|p \implies q}}
{{Assumption|3|p}}
{{ModusPonens|4|1, 3|q \implies r|1|3}}
{{ModusPonens|5|2, 3|q|2|3}}
{{ModusPonens|6|1, 2, 3|r|4|5}}
{{Implication|7|1, 2|p \implies r|3|6}}
{{Implication|8|1|\paren {p \implies q} \implies \paren {p \implies r}|2|7}}
{{EndTableau|qed}}
Theorem: Self-Distributive Law for Conditional/Formulation 1/Reverse Implication

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

Proof:
{{BeginTableau|\paren {p \implies q} \implies \paren {p \implies r} \vdash p \implies \paren {q \implies r} }}
{{Premise|1|\paren {p \implies q} \implies \paren {p \implies r} }}
{{Assumption|2|p}}
{{Assumption|3|q}}
{{SequentIntro|4|3|p \implies q|3|True Statement is implied by Every Statement}}
{{ModusPonens|5|1, 3|p \implies r|1|4}}
{{ModusPonens|6|1, 2, 3|r|5|2}}
{{Implication|7|1, 2|q \implies r|3|6}}
{{Implication|8|1|p \implies \paren {q \implies r}|2|7}}
{{EndTableau}}
{{qed}}
Theorem: Rule of Exportation/Formulation 1

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

Proof:
{{BeginTableau|\paren {p \land q} \implies r \vdash p \implies \paren {q \implies r} }}
{{Premise|1|\paren {p \land q} \implies r}}
{{Assumption|2|p}}
{{Assumption|3|q}}
{{Conjunction|4|2, 3|p \land q|2|3}}
{{ModusPonens|5|1, 2, 3|r|1|4}}
{{Implication|6|1, 2|q \implies r|3|5}}
{{Implication|7|1|p \implies \paren {q \implies r} |2|6}}
{{EndTableau}}
{{qed}}
Theorem: Rule of Exportation/Formulation 1

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

Proof:
=== Proof of Forward Implication ===
{{:Rule of Exportation/Formulation 1/Forward Implication/Proof}}
=== Proof of Reverse Implication ===
{{:Rule of Exportation/Formulation 1/Reverse Implication/Proof}}
Theorem: Rule of Exportation/Formulation 1

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

Proof:
We apply the Method of Truth Tables to the proposition.
As can be seen by inspection, the truth values under the main connectives match for all boolean interpretations.
:<nowiki>$\begin{array}{|ccccc||ccccc|} \hline
(p & \land & q) & \implies & r & p & \implies & (q & \implies & r) \\
\hline
\F & \F & \F & \T & \F & \F & \T & \F & \T & \F \\
\F & \F & \F & \T & \T & \F & \T & \F & \T & \T \\
\F & \F & \T & \T & \F & \F & \T & \T & \F & \F \\
\F & \F & \T & \T & \T & \F & \T & \T & \T & \T \\
\T & \F & \F & \T & \F & \T & \T & \F & \T & \F \\
\T & \F & \F & \T & \T & \T & \T & \F & \T & \T \\
\T & \T & \T & \F & \F & \T & \F & \T & \F & \F \\
\T & \T & \T & \T & \T & \T & \T & \T & \T & \T \\
\hline
\end{array}$</nowiki>
{{qed}}
Theorem: Rule of Exportation/Formulation 1

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

Proof:
{{BeginTableau|p \implies \paren {q \implies r} \vdash \paren {p \land q} \implies r}}
{{Premise|1|p \implies \paren {q \implies r} }}
{{Assumption|2|p \land q}}
{{Simplification|3|2|p|2|1}}
{{Simplification|4|2|q|2|2}}
{{ModusPonens|5|1, 2|q \implies r|1|3}}
{{ModusPonens|6|1, 2|r|5|4}}
{{Implication|7|1|\paren {p \land q} \implies r|2|6}}
{{EndTableau|qed}}
Theorem: Square Matrix with Duplicate Columns has Zero Determinant

If two columns of a square matrix over a commutative ring $\struct {R, +, \circ}$ are identical, then its determinant is zero.

Proof:
Let $\mathbf A$ be a square matrix over $R$ with two identical columns.
Let $\mathbf A^\intercal$ denote the transpose of $\mathbf A$.
Then $\mathbf A^\intercal$ has two identical rows.
Then:
{{begin-eqn}}
{{eqn | l = \map \det {\mathbf A}
      | r = \map \det {\mathbf A^\intercal}
      | c = Determinant of Transpose
}}
{{eqn | r = 0
      | c = Square Matrix with Duplicate Rows has Zero Determinant
}}
{{end-eqn}}
{{qed}}
Theorem: Inverses of Elements Related by Compatible Relation

:$\forall x, y \in G: x \mathrel \RR y \iff y^{-1} \mathrel \RR x^{-1}$

Proof:
Let $e$ be the group identity of $G$.
By Relation Compatible with Group Operation is Strongly Compatible: Corollary:
:$(1): \quad x \mathrel \RR y \iff e \mathrel \RR y \circ x^{-1}$
By Relation Compatible with Group Operation is Strongly Compatible: Corollary, also:
:$(2): \quad y^{-1} \mathrel \RR x^{-1} \iff e \mathrel \RR \paren {y^{-1} }^{-1} \circ x^{-1}$
By Inverse of Group Inverse:
:$\paren {y^{-1} }^{-1} = y$
Thus, we can rewrite $(2)$ as:
:$(3): \quad y^{-1} \mathrel \RR x^{-1} \iff e \mathrel \RR y \circ x^{-1}$
Now note that the {{RHS}} of $(3)$ is the same as the {{RHS}} in $(1)$.
We conclude that:
:$x \mathrel \RR y \iff y^{-1} \mathrel \RR x$
{{qed}}
Category:Relations Compatible with Group Operation
3otsb6ciojx5b162drxbtus6jiznlb6
Theorem: Ordering Induced by Join Semilattice

Let $\struct {S, \vee, \preceq}$ be a join semilattice.
By Join Semilattice is Semilattice, $\struct {S, \vee}$ is a semilattice.
By Semilattice Induces Ordering, $\struct {S, \vee}$ induces an ordering $\preceq'$ on $S$, by:
:$a \preceq' b$ {{iff}} $a \vee b = b$
for all $a, b \in S$.
The ordering $\preceq'$ coincides with the original ordering $\preceq$.

Proof:
It is to be shown that, for all $a, b \in S$:
:$a \preceq b$ {{iff}} $b = \sup \set {a, b}$
by definition of join.
Here $\sup$ denotes supremum.
Since any upper bound $c$ of $\set {a, b}$ must satisfy:
:$b \preceq c$
it suffices to verify that:
:$a \preceq b$ {{iff}} $b$ is an upper bound for $\set {a, b}$
Since $\preceq$ is reflexive, we know that:
:$b \preceq b$
and therefore said equivalence is established.
We conclude that $\preceq'$ and $\preceq$ coincide.
{{qed}}
{{expand|We need to start using a construct for duality. (Global) Dual is Ordering Induced by Meet Semilattice}}
Category:Order Theory
Category:Join Semilattices
jpbccrl0458y7uq2xoubhwfm96lwej8
Theorem: Combination Theorem for Complex Derivatives

Let $D$ be an open subset of the set of complex numbers $\C$.
Let $f, g: D \to \C$ be complex-differentiable functions on $D$
Let $z \in D$.
Let $w, c \in \C$ be arbitrary complex numbers.
Then the following results hold:
=== Sum Rule ===
{{:Combination Theorem for Complex Derivatives/Sum Rule}}
=== Multiple Rule ===
{{:Combination Theorem for Complex Derivatives/Multiple Rule}}
=== Combined Sum Rule ===
{{:Combination Theorem for Complex Derivatives/Combined Sum Rule}}
=== Product Rule ===
{{:Combination Theorem for Complex Derivatives/Product Rule}}
=== Quotient Rule ===
{{:Combination Theorem for Complex Derivatives/Quotient Rule}}

Proof:
Define $k: D \to \C$ as the pointwise product of $f$ and $g$, so $k = fg$.
Let $z_0 \in D$ be a point in $D$.
{{begin-eqn}}
{{eqn | l = \map {k'} {z_0}
      | r = \lim_{h \mathop \to 0} \frac {\map k {z_0 + h} - \map k {z_0} } h
      | c =
}}
{{eqn | r = \lim_{h \mathop \to 0} \frac {\map f {z_0 + h} \, \map g {z_0 + h} - \map f {z_0} \, \map g {z_0} } h
      | c =
}}
{{eqn | r = \lim_{h \mathop \to 0} \frac {\map f {z_0 + h} \, \map g {z_0 + h} - \map f {z_0 + h} \, \map g {z_0} + \map f {z_0 + h} \, \map g {z_0} - \map f {z_0} \, \map g {z_0} } h
      | c =
}}
{{eqn | r = \lim_{h \mathop \to 0} \paren {\map f {z_0 + h} \frac {\map g {z_0 + h} - \map g {z_0} } h + \frac {\map f {z_0 + h} - \map f {z_0} } h \, \map g {z_0} }
      | c =
}}
{{eqn | r = \map f {z_0} \, \map {g'} {z_0} + \map {f'} {z_0} \, \map g {z_0}
      | c =
}}
{{eqn | ll= \leadsto
      | q = \forall z \in D
      | l = \map {k'} z
      | r = \map f z \, \map {g'} z + \map {f'} z \, \map g z
      | c = {{Defof|Derivative of Complex Function}}
}}
{{end-eqn}}
{{qed}}
Theorem: Combination Theorem for Complex Derivatives

Let $D$ be an open subset of the set of complex numbers $\C$.
Let $f, g: D \to \C$ be complex-differentiable functions on $D$
Let $z \in D$.
Let $w, c \in \C$ be arbitrary complex numbers.
Then the following results hold:
=== Sum Rule ===
{{:Combination Theorem for Complex Derivatives/Sum Rule}}
=== Multiple Rule ===
{{:Combination Theorem for Complex Derivatives/Multiple Rule}}
=== Combined Sum Rule ===
{{:Combination Theorem for Complex Derivatives/Combined Sum Rule}}
=== Product Rule ===
{{:Combination Theorem for Complex Derivatives/Product Rule}}
=== Quotient Rule ===
{{:Combination Theorem for Complex Derivatives/Quotient Rule}}

Proof:
Denote the open ball of $0$ by radius $r \in \R_{>0}$ as $\map {B_r} 0$.
Let $z \in D$.
By the Epsilon-Function Complex Differentiability Condition, it follows that there exists $r \in \R_{>0}$ such that for all $h \in \map {B_r} 0 \setminus \set 0$:
:$\map f {z + h} = \map f z + \map h {\map {f'} z + \map {\epsilon_f} h}$
:$\map g {z + h} = \map g z + \map h {\map {g'} z + \map {\epsilon_g} h}$
where $\epsilon_f, \epsilon_g: \map {B_r} 0 \setminus \set 0 \to \C$ are complex functions that converge to $0$ as $h$ tends to $0$.
Then:
{{begin-eqn}}
{{eqn | l = \map {\paren {f g} } {z + h}
      | r = \map f z \map g z + \map h {\map f z \map {g'} z + \map f z \map {\epsilon_g} h} + h \paren {\map g z \map {f'} z + \map g z \map {\epsilon_f} h} + {h^2} \paren {\map {f'} z + \map {\epsilon_f} h} \paren {\map {g'} z + \map {\epsilon_g} h}
}}
{{eqn | r = \map {\paren {f g} } z + h \paren {\map {f'} z \map g z + \map f z \map {g'} z + h \paren {\map {f'} z + \map {\epsilon_f} h} \paren {\map {g'} z + \map {\epsilon_g} h} }
}}
{{end-eqn}}
Define $\epsilon: \map {B_r} 0 \setminus \set 0 \to \C$ by:
:$\map \epsilon h = h \paren {\map {f'} z + \map {\epsilon_f} h} \paren {\map {g'} z + \map {\epsilon_g} h}$
From Product Rule for Limits of Complex Functions and Combined Sum Rule for Limits of Complex Functions:
:$\ds \lim_{h \mathop \to 0} \map \epsilon h = \paren {\lim_{h \mathop \to 0} h} \paren {\lim_{h \mathop \to 0} \paren {\map {f'} z + \map {\epsilon_f} h} } \paren {\lim_{h \mathop \to 0} \paren {\map {g'} z + \map {\epsilon_g} h} } = 0$
Then the Epsilon-Function Complex Differentiability Condition shows that:
:$\map {\paren {f g}'} z = \map {f'} z \map g z + \map f z \map {g'} z$
{{qed}}
Theorem: Combination Theorem for Complex Derivatives

Let $D$ be an open subset of the set of complex numbers $\C$.
Let $f, g: D \to \C$ be complex-differentiable functions on $D$
Let $z \in D$.
Let $w, c \in \C$ be arbitrary complex numbers.
Then the following results hold:
=== Sum Rule ===
{{:Combination Theorem for Complex Derivatives/Sum Rule}}
=== Multiple Rule ===
{{:Combination Theorem for Complex Derivatives/Multiple Rule}}
=== Combined Sum Rule ===
{{:Combination Theorem for Complex Derivatives/Combined Sum Rule}}
=== Product Rule ===
{{:Combination Theorem for Complex Derivatives/Product Rule}}
=== Quotient Rule ===
{{:Combination Theorem for Complex Derivatives/Quotient Rule}}

Proof:
Let $z_0 \in D$ be a point in $D$.
Define $k : D \to \Z$ by $\map k {z_0} = \map f {z_0} + \map g {z_0}$.
Then:
{{begin-eqn}}
{{eqn | l = \map { k' } {z_0}
      | r = \lim_{h \mathop \to 0} \frac {\map k {z_0 + h} - \map k {z_0} } h
      | c = {{Defof|Derivative of Complex Function}}
}}
{{eqn | r = \lim_{h \mathop \to 0} \frac {\paren {\map f {z_0 + h} + \map g {z_0 + h} } - \paren {\map f {z_0} +\map g {z_0} } } h
      | c = 
}}
{{eqn | r = \lim_{h \mathop \to 0} \frac {\map f {z_0 + h} + \map g {z_0 + h} - \map f {z_0} - \map g {z_0} } h
      | c = 
}}
{{eqn | r = \lim_{h \mathop \to 0} \frac {\paren {\map f {z_0 + h} - \map f {z_0} } + \paren {\map g {z_0 + h} - \map g {z_0} } } h
      | c = 
}}
{{eqn | r = \lim_{h \mathop \to 0} \paren {\frac {\map f {z_0 + h} - \map f {z_0} } h + \frac {\map g {z_0 + h} - \map g {z_0} } h}
      | c = Complex Multiplication Distributes over Addition
}}
{{eqn | r = \lim_{h \mathop \to 0} \frac {\map f {z_0 + h} - \map f {z_0} } h + \lim_{h \mathop \to 0} \frac {\map g {z_0 + h} - \map g {z_0} } h
      | c = Sum Rule for Limits of Complex Functions
}}
{{eqn | r = \map {f'} {z_0} + \map {g'} {z_0}
      | c = {{Defof|Derivative of Complex Function}}
}}
{{eqn | ll= \leadsto
      | q = \forall z \in D
      | l = \map { \paren{f+g}' } z
      | r = \map {f'} z + \map {g'} z
      | c = {{Defof|Derivative of Complex Function}}
}}
{{end-eqn}}
{{qed}}
Theorem: Combination Theorem for Complex Derivatives

Let $D$ be an open subset of the set of complex numbers $\C$.
Let $f, g: D \to \C$ be complex-differentiable functions on $D$
Let $z \in D$.
Let $w, c \in \C$ be arbitrary complex numbers.
Then the following results hold:
=== Sum Rule ===
{{:Combination Theorem for Complex Derivatives/Sum Rule}}
=== Multiple Rule ===
{{:Combination Theorem for Complex Derivatives/Multiple Rule}}
=== Combined Sum Rule ===
{{:Combination Theorem for Complex Derivatives/Combined Sum Rule}}
=== Product Rule ===
{{:Combination Theorem for Complex Derivatives/Product Rule}}
=== Quotient Rule ===
{{:Combination Theorem for Complex Derivatives/Quotient Rule}}

Proof:
Denote the open ball of $0$ with radius $r \in \R_{>0}$ as $\map {B_r} 0$.
Let $z \in D$.
By the Epsilon-Function Complex Differentiability Condition, it follows that there exists $r \in \R_{>0}$ such that for all $h \in \map {B_r} 0 \setminus \set 0$:
:$\map f {z + h} = \map f z + h \paren {\map {f'} z + \map {\epsilon_f} h}$
:$\map g {z + h} = \map g z + h \paren {\map {g'} z + \map {\epsilon_g} h}$
where $\epsilon_f, \epsilon_g: \map {B_r} 0 \setminus \set 0 \to \C$ are complex functions that converge to $0$ as $h$ tends to $0$.
Then:
{{begin-eqn}}
{{eqn | l = \map {\paren {f + g} } {z + h}
      | r = \map f z + h \paren {\map {f'} z + \map {\epsilon_f} h} + \map g z + h \paren {\map {g'} z + \map {\epsilon_g} h}
}}
{{eqn | r = \map {\paren {f + g} } z + h \paren {\map {f'} z + \map {g'} z + \map {\paren {\epsilon_f + \epsilon_g} } h}
}}
{{end-eqn}}
From Sum Rule for Limits of Complex Functions, it follows that $\ds \lim_{h \mathop \to 0} \map {\paren {\epsilon_f + \epsilon_g} } h = 0$.
By the Epsilon-Function Complex Differentiability Condition, it follows that:
:$\map {\paren {f + g}'} z = \map {f'} z + \map {g'} z$
{{qed}}
Theorem: Combination Theorem for Complex Derivatives/Sum Rule

:$\map {\paren {f + g}'} z = \map {f'} z + \map {g'} z$

Proof:
Let $z_0 \in D$ be a point in $D$.
Define $k : D \to \Z$ by $\map k {z_0} = \map f {z_0} + \map g {z_0}$.
Then:
{{begin-eqn}}
{{eqn | l = \map { k' } {z_0}
      | r = \lim_{h \mathop \to 0} \frac {\map k {z_0 + h} - \map k {z_0} } h
      | c = {{Defof|Derivative of Complex Function}}
}}
{{eqn | r = \lim_{h \mathop \to 0} \frac {\paren {\map f {z_0 + h} + \map g {z_0 + h} } - \paren {\map f {z_0} +\map g {z_0} } } h
      | c = 
}}
{{eqn | r = \lim_{h \mathop \to 0} \frac {\map f {z_0 + h} + \map g {z_0 + h} - \map f {z_0} - \map g {z_0} } h
      | c = 
}}
{{eqn | r = \lim_{h \mathop \to 0} \frac {\paren {\map f {z_0 + h} - \map f {z_0} } + \paren {\map g {z_0 + h} - \map g {z_0} } } h
      | c = 
}}
{{eqn | r = \lim_{h \mathop \to 0} \paren {\frac {\map f {z_0 + h} - \map f {z_0} } h + \frac {\map g {z_0 + h} - \map g {z_0} } h}
      | c = Complex Multiplication Distributes over Addition
}}
{{eqn | r = \lim_{h \mathop \to 0} \frac {\map f {z_0 + h} - \map f {z_0} } h + \lim_{h \mathop \to 0} \frac {\map g {z_0 + h} - \map g {z_0} } h
      | c = Sum Rule for Limits of Complex Functions
}}
{{eqn | r = \map {f'} {z_0} + \map {g'} {z_0}
      | c = {{Defof|Derivative of Complex Function}}
}}
{{eqn | ll= \leadsto
      | q = \forall z \in D
      | l = \map { \paren{f+g}' } z
      | r = \map {f'} z + \map {g'} z
      | c = {{Defof|Derivative of Complex Function}}
}}
{{end-eqn}}
{{qed}}
Theorem: Combination Theorem for Complex Derivatives/Sum Rule

:$\map {\paren {f + g}'} z = \map {f'} z + \map {g'} z$

Proof:
Denote the open ball of $0$ with radius $r \in \R_{>0}$ as $\map {B_r} 0$.
Let $z \in D$.
By the Epsilon-Function Complex Differentiability Condition, it follows that there exists $r \in \R_{>0}$ such that for all $h \in \map {B_r} 0 \setminus \set 0$:
:$\map f {z + h} = \map f z + h \paren {\map {f'} z + \map {\epsilon_f} h}$
:$\map g {z + h} = \map g z + h \paren {\map {g'} z + \map {\epsilon_g} h}$
where $\epsilon_f, \epsilon_g: \map {B_r} 0 \setminus \set 0 \to \C$ are complex functions that converge to $0$ as $h$ tends to $0$.
Then:
{{begin-eqn}}
{{eqn | l = \map {\paren {f + g} } {z + h}
      | r = \map f z + h \paren {\map {f'} z + \map {\epsilon_f} h} + \map g z + h \paren {\map {g'} z + \map {\epsilon_g} h}
}}
{{eqn | r = \map {\paren {f + g} } z + h \paren {\map {f'} z + \map {g'} z + \map {\paren {\epsilon_f + \epsilon_g} } h}
}}
{{end-eqn}}
From Sum Rule for Limits of Complex Functions, it follows that $\ds \lim_{h \mathop \to 0} \map {\paren {\epsilon_f + \epsilon_g} } h = 0$.
By the Epsilon-Function Complex Differentiability Condition, it follows that:
:$\map {\paren {f + g}'} z = \map {f'} z + \map {g'} z$
{{qed}}
Theorem: Combination Theorem for Complex Derivatives/Multiple Rule

:$\map {\paren {w f}'} z = w \map {f'} z$

Proof:
Denote the open ball of $0$ with radius $r \in \R_{>0}$ as $\map {B_r} 0$.
Let $z \in D$.
By the Epsilon-Function Complex Differentiability Condition, it follows that there exists $r \in \R_{>0}$ such that for all $h \in \map {B_r} 0 \setminus \set 0$:
:$\map f {z + h} = \map f z + h \paren {\map {f'} z + \map \epsilon h}$
where $\epsilon: \map {B_r} 0 \setminus \set 0 \to \C$ is a complex function such that $\ds \lim_{h \mathop \to 0} \map \epsilon h = 0$.
Then:
:$w \map f {z + h} = w \map f z + h \paren {w \map {f'} z + w \map \epsilon h}$
From Multiple Rule for Limits of Complex Functions, it follows that:
:$\ds \lim_{h \mathop \to 0} w \map \epsilon h = \paren {\lim_{h \mathop \to 0} w} \paren {\lim_{h \mathop \to 0} \map \epsilon h} = 0$
Then the Epsilon-Function Complex Differentiability Condition shows that:
:$\map {\paren {w f}'} z = w \map {f'} z$
{{qed}}
Theorem: Join Absorbs Meet

Let $\struct {S, \wedge, \preceq}$ be a meet semilattice.
Let $\vee$ denote join.
Then $\vee$ absorbs $\wedge$.
That is, for all $a, b \in S$:
:$a \vee \paren {a \wedge b} = a$

Proof:
By Ordering in terms of Join, we have that:
:$a \vee \paren {a \wedge b} = a$ {{iff}} $a \wedge b \preceq a$
The result thus follows from Meet Precedes Operands.
{{qed}}
Theorem: Meet Absorbs Join

Let $\struct {S, \vee, \preceq}$ be a join semilattice.
Let $\wedge$ denote meet.
Then $\wedge$ absorbs $\vee$.
That is, for all $a, b \in S$:
:$a \wedge \paren {a \vee b} = a$

Proof:
By Dual Pairs (Order Theory), we observe that the theorem statement is dual to that of Join Absorbs Meet.
The result follows by the Global Duality Principle.
{{qed}}
Theorem: Rule of Exportation/Formulation 2

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

Proof:
=== Proof of Forward Implication ===
{{:Rule of Exportation/Formulation 2/Forward Implication/Proof 1}}
Theorem: Rule of Exportation/Formulation 2

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

Proof:
{{BeginTableau|\vdash \paren {\paren {p \land q} \implies r} \implies \paren {p \implies \paren {q \implies r} } }}
{{Assumption|1|\paren {p \land q} \implies r}}
{{Assumption|2|p}}
{{Assumption|3|q}}
{{Conjunction|4|2, 3|p \land q|2|3}}
{{ModusPonens|5|1, 2, 3|r|1|4}}
{{Implication|6|1, 2|q \implies r|3|5}}
{{Implication|7|1|p \implies \paren {q \implies r} |2|6}}
{{Implication|8||\paren {\paren {p \land q} \implies r} \implies \paren {p \implies \paren {q \implies r} }|1|7}}
{{EndTableau|lemma}}
Theorem: Rule of Exportation/Formulation 2

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

Proof:
{{BeginTableau|\vdash \paren {\paren {p \land q} \implies r} \implies \paren {p \implies \paren {q \implies r} } }}
{{Assumption|1|\paren {p \land q} \implies r}}
{{SequentIntro|2|1|p \implies \paren {q \implies r}|1|Rule of Exportation: Formulation 1: Forward Implication}}
{{Implication|3||\paren {\paren {p \land q} \implies r} \implies \paren {p \implies \paren {q \implies r} }|1|2}}
{{EndTableau}}
{{qed}}
Theorem: Rule of Exportation/Formulation 2

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

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

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

Proof:
{{BeginTableau|\vdash \paren {p \implies \paren {q \implies r} } \implies \paren {\paren {p \land q} \implies r} }}
{{Assumption|1|p \implies \paren {q \implies r} }}
{{Assumption|2|p \land q}}
{{Simplification|3|2|p|2|1}}
{{Simplification|4|2|q|2|2}}
{{ModusPonens|5|1, 2|q \implies r|1|3}}
{{ModusPonens|6|1, 2|r|5|4}}
{{Implication|7|1|\paren {p \land q} \implies r|2|6}}
{{Implication|8||\paren {p \implies \paren {q \implies r} } \implies \paren {\paren {p \land q} \implies r}|1|7}}
{{EndTableau|lemma}}
Theorem: Rule of Exportation/Formulation 2

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

Proof:
{{BeginTableau|\vdash \paren {p \implies \paren {q \implies r} } \implies \paren {\paren {p \land q} \implies r} }}
{{Assumption|1|p \implies \paren {q \implies r} }}
{{SequentIntro|2|1|\paren {p \land q} \implies r|1|Rule of Exportation: Formulation 1: Reverse Implication}}
{{Implication|3||\paren {p \implies \paren {q \implies r} } \implies \paren {\paren {p \land q} \implies r}|1|2}}
{{EndTableau|qed}}