avewright/proofwiki-math huggingface dataset:
Theorem: Ray is Order-Convex

Let $\struct {S, \preceq}$ be an ordered set.
Let $I$ be a ray, either open or closed.
Then $I$ is order-convex in $S$.

Proof:
The cases for upward-pointing and downward-pointing rays are equivalent.
{{explain|"Dual of convex is convex" and duality, upon which the above statement depends.}}
{{WLOG}}, suppose that $U$ is an upward-pointing ray.
By the definition of a ray, there exists an $a \in S$ such that:
:$I = a^\succ$
or;
:$I = a^\succeq$
according to whether $U$ is open or closed.
Let $x, y, z \in S$ such that $x \prec y \prec z$ and $x, z \in I$.
Then:
:$a \preceq x \prec y$
so:
:$a \prec y$
Therefore:
:$y \in a^\succ \subseteq I$
Thus $I$ is order-convex.
{{qed}}
Theorem: Intersection of Order-Convex Sets is Order-Convex

Let $\struct {S, \preceq}$ be an ordered set.
Let $\CC$ be a set of order-convex sets in $S$.
Then $\bigcap \CC$ is order-convex.

Proof:
Let $a, b, c \in S$.
Let $a, c \in \bigcap \CC$.
Let $a \prec b \prec c$.
By the definition of intersection:
:$\forall T \in \CC: a, c \in T$
Since each $T \in \CC$ is order-convex:
:$\forall T \in \CC: b \in T$
Thus by the definition of intersection:
:$b \in \bigcap \CC$
Thus $\bigcap \CC$ is order-convex.
{{qed}}
Category:Order-Convex Sets
8w5d0bogxu5g5wby1b07efc0np6dv1p
Theorem: Upper and Lower Closures are Order-Convex

Let $\struct {S, \preceq}$ be an ordered set.
Let $a \in S$.
Then $a^\succeq$, $a^\succ$, $a^\preceq$, and $a^\prec$ are order-convex in $S$.

Proof:
The cases for upper and lower closures are dual, so we need only prove the case for upper closures.
Suppose, then, that $C = a^\succeq$ or $C = a^\succ$.
Suppose that $x, y, z \in S$, $x \prec y \prec z$, and $x, z \in C$.
Then $a \preceq x \prec y$, so $a \prec y$ by Extended Transitivity.
Therefore $y \in a^\succ \subseteq C$.
Thus $C$ is order-convex.
{{qed}}
Category:Lower Closures
Category:Upper Closures
Category:Order-Convex Sets
qzpgfcy0i9gf1e0fmyj7xcw25fbg9km
Theorem: Transitive Closure of Symmetric Relation is Symmetric

Let $S$ be a set.
Let $\RR$ be a symmetric relation on $S$.
Let $\TT$ be the transitive closure of $\RR$.
The $\TT$ is symmetric.

Proof:
Let $a, b \in S$ with $a \mathrel \TT b$.
By the definition of transitive closure, there is an $n \in \N$ such that $a \mathrel {\RR^n} b $.
Thus there are $x_0, x_1, \dots x_n \in S$ such that:
:$x_0 = a$
:$x_n = b$
:For $k = 0, \dots, n-1$: $x_k \mathrel \RR x_{k + 1}$
For $k = 0, \dots, n$, let $y_k = x_{n - k}$.
Then:
:$y_0 = x_n = b$
:$y_n = x_0 = a$
For $k = 0, \dots, n - 1$:
:$x_{n - k - 1} \mathrel \RR x_{n - k}$
Thus:
:$y_{k + 1} \mathrel \RR y_k$
Since $\RR$ is symmetric:
:For $k = 0, \dots, n - 1$: $y_k \mathrel \RR y_{k + 1}$
Thus $b \mathrel {\RR^n} a$, so $b \mathrel \TT a$.
{{qed}}
Category:Symmetric Relations
Category:Transitive Closures
f8dzwy12tasxttpb5j5h7nn0r62dcpb
Theorem: Transitive Closure of Reflexive Relation is Reflexive

Let $S$ be a set.
Let $\RR$ be a reflexive relation on $S$.
Let $\RR^+$ be the transitive closure of $\RR$.
Then $\RR^+$ is reflexive.

Proof:
Let $a \in S$.
Since $\RR$ is reflexive:
:$\tuple {a, a} \in \RR$
By the definition of transitive closure:
:$\RR \subseteq \RR^+$
Thus by the definition of subset:
:$\tuple {a, a} \in \RR^+$
Since this holds for all $a \in S$, it follows that $\RR^+$ is reflexive.
{{qed}}
Theorem: Transitive Closure of Reflexive Symmetric Relation is Equivalence

Let $S$ be a set.
Let $\RR$ be a symmetric and reflexive relation on $S$.
Then the transitive closure of $\RR$ is an equivalence relation.

Proof:
Let $\sim$ be the transitive closure of $\RR$.
Checking in turn each of the criteria for equivalence:
Theorem: Union of Overlapping Order-Convex Sets in Toset is Order-Convex

Let $\struct {S, \preceq}$ be a totally ordered set.
Let $U$ and $V$ be order-convex sets in $S$.
Let $U \cap V \ne \O$.
Then $U \cup V$ is also order-convex.

Proof:
Let $a,b,c \in S$
Let $a,c \in U \cup V$.
Let $a \prec b \prec c$.
If $a, c \in U$ then $b \in U$ because $U$ is order-convex.
Thus $b \in U \cup V$ by the definition of union.
Similarly, if $a,c \in V$ then $b \in U \cup V$.
Otherwise, {{WLOG}}, suppose that $a \in U$ and $c \in V$.
Since $U \cap V$ is nonempty by the premise, it has an element $p$.
Since $\preceq$ is a total ordering:
:$b \preceq p$ or $p \preceq b$.
If $b \preceq p$, then since $a \prec b$, $a, p \in U$, and $U$ is order-convex, we can conclude that
:$b \in U$
so $b \in U \cup V$.
A similar argument shows that it $p \preceq b$ then $b \in V$, so $b \in U \cup V$.
Thus in all cases we can conclude that $b \in U \cup V$, so $U \cup V$ is order-convex.
{{qed}}
Category:Order-Convex Sets
Category:Total Orderings
qim1ef1ojbjici6wnccb6tnf5gezye4
Theorem: Rule of Material Equivalence

The '''Rule of Material Equivalence''' is a valid deduction sequent in propositional logic:
:If we can conclude that $p$ implies $q$ and if we can also conclude that $q$ implies $p$, then we may infer that $p$ {{iff}} $q$.
==== Formulation 1 ====
{{:Rule of Material Equivalence/Formulation 1}}
==== Formulation 2 ====
{{:Rule of Material Equivalence/Formulation 2}}

Proof:
{{BeginTableau|p \iff q \vdash \paren {p \implies q} \land \paren {q \implies p} }}
{{Premise|1|p \iff q}}
{{BiconditionalElimination|2|1|p \implies q|1|1}}
{{BiconditionalElimination|3|1|q \implies p|1|2}}
{{Conjunction|4|1|\paren {p \implies q} \land \paren {q \implies p}|2|3}}
{{EndTableau}}
{{BeginTableau|\paren {p \implies q} \land \paren {q \implies p} \vdash p \iff q}}
{{Premise|1|\paren {p \implies q} \land \paren {q \implies p} }}
{{Simplification|2|1|p \implies q|1|1}}
{{Simplification|3|1|q \implies p|1|2}}
{{BiconditionalIntro|4|1|p \iff q|2|3}}
{{EndTableau}}
{{qed}}
Theorem: Rule of Material Equivalence

The '''Rule of Material Equivalence''' is a valid deduction sequent in propositional logic:
:If we can conclude that $p$ implies $q$ and if we can also conclude that $q$ implies $p$, then we may infer that $p$ {{iff}} $q$.
==== Formulation 1 ====
{{:Rule of Material Equivalence/Formulation 1}}
==== Formulation 2 ====
{{:Rule of Material Equivalence/Formulation 2}}

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|ccccccc|} \hline
p & \iff & q & (p & \implies & q) & \land & (q & \implies & p) \\
\hline
\F & \T & \F & \F & \T & \F & \T & \F & \T & \F \\
\F & \F & \T & \F & \T & \T & \F & \T & \F & \F \\
\T & \F & \F & \T & \F & \F & \F & \F & \T & \T \\
\T & \T & \T & \T & \T & \T & \T & \T & \T & \T \\
\hline
\end{array}$</nowiki>
{{qed}}
Theorem: Rule of Material Equivalence

The '''Rule of Material Equivalence''' is a valid deduction sequent in propositional logic:
:If we can conclude that $p$ implies $q$ and if we can also conclude that $q$ implies $p$, then we may infer that $p$ {{iff}} $q$.
==== Formulation 1 ====
{{:Rule of Material Equivalence/Formulation 1}}
==== Formulation 2 ====
{{:Rule of Material Equivalence/Formulation 2}}

Proof:
{{BeginTableau|\vdash \paren {p \iff q} \iff \paren {\paren {p \implies q} \land \paren {q \implies p} } }}
{{Assumption|1|p \iff q}}
{{SequentIntro|2|1|\paren {\paren {p \implies q} \land \paren {q \implies p} }|1|Rule of Material Equivalence: Formulation 1}}
{{Implication|3||\paren {p \iff q} \implies \paren {\paren {p \implies q} \land \paren {q \implies p} }|1|2}}
{{Assumption|4|\paren {p \implies q} \land \paren {q \implies p} }}
{{SequentIntro|5|4|p \iff q|4|Rule of Material Equivalence: Formulation 1}}
{{Implication|6||\paren {\paren {p \implies q} \land \paren {q \implies p} } \implies \paren {p \iff q}|4|5}}
{{BiconditionalIntro|7||\paren {p \iff q} \iff \paren {\paren {p \implies q} \land \paren {q \implies p} }|3|6}}
{{EndTableau|qed}}
Theorem: Rule of Material Equivalence

The '''Rule of Material Equivalence''' is a valid deduction sequent in propositional logic:
:If we can conclude that $p$ implies $q$ and if we can also conclude that $q$ implies $p$, then we may infer that $p$ {{iff}} $q$.
==== Formulation 1 ====
{{:Rule of Material Equivalence/Formulation 1}}
==== Formulation 2 ====
{{:Rule of Material Equivalence/Formulation 2}}

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|ccccccc|} \hline
(p & \iff & q) & \iff & (p & \implies & q) & \land & (q & \implies & p) \\
\hline
\F & \T & \F & \T & \F & \T & \F & \T & \F & \T & \F \\
\F & \F & \T & \T & \F & \T & \T & \F & \T & \F & \F \\
\T & \F & \F & \T & \T & \F & \F & \F & \F & \T & \T \\
\T & \T & \T & \T & \T & \T & \T & \T & \T & \T & \T \\
\hline
\end{array}$</nowiki>
{{qed}}
Theorem: Union of Overlapping Order-Convex Sets in Toset is Order-Convex/Infinite Union

Let $\struct {S, \preceq}$ be a totally ordered set.
Let $\AA$ be a set of order-convex subsets of $S$.
For any $P, Q \in \AA$, let there be elements $C_0, \dotsc, C_n \in \AA$ such that:
:$C_0 = P$
:$C_n = Q$
:For $k = 0, \dotsc, n - 1: C_k \cap C_{k + 1} \ne \O$
Then $\bigcup \AA$ is order-convex in $S$.

Proof:
Let $a, c \in \bigcup \AA$.
Let $b \in S$.
Let $a \prec b \prec c$.
Since $a, c \in \bigcup \AA$, there are $P, Q \in \AA$ such that $a \in P$ and $c \in Q$.
By the premise, there are elements $C_0, \dots, C_n \in \AA$ such that:
:$C_0 = P$
:$C_n = Q$
:For $k = 0, \dotsc, n - 1: C_k \cap C_{k + 1} \ne \O$
{{explain|details of induction. Consider putting the finite chain case into a separate lemma.}}
Applying Union of Overlapping Order-Convex Sets in Toset is Order-Convex inductively:
:$\ds \bigcup_{k \mathop = 0}^n C_k$ is order-convex.
Since $\ds a, c \in \bigcup_{k \mathop = 0}^n C_k$, by the definition of order-convexity:
:$\ds b \in \bigcup_{k \mathop = 0}^n C_k$
Thus:
:$\ds b \in \bigcup \AA$
Since this holds for all such triples $a, b, c$, it follows that $\AA$ is order-convex.
{{qed}}
Category:Total Orderings
1yxyuh0gi8wjanxoup1uy6hnovm0f6f
Theorem: Rule of Material Equivalence/Formulation 2

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

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

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

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|ccccccc|} \hline
(p & \iff & q) & \iff & (p & \implies & q) & \land & (q & \implies & p) \\
\hline
\F & \T & \F & \T & \F & \T & \F & \T & \F & \T & \F \\
\F & \F & \T & \T & \F & \T & \T & \F & \T & \F & \F \\
\T & \F & \F & \T & \T & \F & \F & \F & \F & \T & \T \\
\T & \T & \T & \T & \T & \T & \T & \T & \T & \T & \T \\
\hline
\end{array}$</nowiki>
{{qed}}
Theorem: Continuous Involution is Homeomorphism

Let $\struct {S, \tau}$ be a topological space.
Let $f: S \to S$ be a continuous involution.
Then $f$ is a homeomorphism.

Proof:
From Involution is Permutation, $f$ is a permutation and so a bijection.
Since $f$ is continuous, it suffices to verify that its inverse is also continuous.
Now recall $f$ is an involution, that is, $f^{-1} = f$.
Thus $f^{-1}$ is also continuous.
Hence $f$ is a homeomorphism.
{{qed}}
Category:Continuous Mappings
Category:Homeomorphisms (Topological Spaces)
Category:Involutions
hestthn2xk9q1ao7xht4g0lguz5y7fp
Theorem: Involution is Permutation

Let $S$ be a set.
Let $f: S \to S$ be an involution.
Then $f$ is a permutation.

Proof:
By definition, a permutation is a bijection from a set to itself.
Thus it is sufficient to show that $f$ is a bijection.
By definition of involution, for each $x \in S$:
:$\map f {\map f x} = x$
By Equality of Mappings:
:$f \circ f = I_S$
where $I_S$ is the identity mapping on $S$.
Thus $f$ is both a left inverse and a right inverse of itself.
The result follows from Bijection iff Left and Right Inverse.
{{qed}}
Category:Involutions
Category:Permutations
lmkkehwj86nc2klknsreb5iyj8uncj5
Theorem: Non-Equivalence as Disjunction of Conjunctions/Formulation 1/Forward Implication

: $\neg \left ({p \iff q}\right) \vdash \left({\neg p \land q}\right) \lor \left({p \land \neg q}\right)$

Proof:
{{BeginTableau|\neg \paren {p \iff q} \vdash \paren {\neg p \land q} \lor \paren {p \land \neg q} }}
{{Premise|1|\neg \paren {p \iff q} }}
{{SequentIntro|2|1|\neg \paren {\paren {p \implies q} \land \paren {q \implies p} }|1
  |Rule of Material Equivalence}}
{{SequentIntro|3|1|\neg \paren {\paren {\neg p \lor q} \land \paren {\neg q \lor p} }|2
  |Rule of Material Implication (twice)}}
{{DeMorgan|4|1|\neg \paren {\neg p \lor q} \lor \neg \paren {\neg q \lor p}|3|Disjunction of Negations}}
{{DeMorgan|5|1|\paren {\neg \neg  p \land \neg q} \lor \paren {\neg \neg q \land \neg p}|4|Conjunction of Negations}}
{{DoubleNegElimination|6|1|\paren {p \land \neg q} \lor \paren {q \land \neg p}|5}}
{{Commutation|7|1|\paren {p \land \neg q} \lor \paren {\neg p \land q}|6|Conjunction}}
{{Commutation|8|1|\paren {\neg p \land q} \lor \paren {p \land \neg q}|7|Disjunction}}
{{EndTableau|qed}}
{{LEM|Double Negation Elimination|3}}
Theorem: Non-Equivalence as Disjunction of Conjunctions/Formulation 1/Reverse Implication

: $\left({\neg p \land q}\right) \lor \left({p \land \neg q}\right) \vdash \neg \left ({p \iff q}\right)$

Proof:
{{BeginTableau|\paren {\neg p \land q} \lor \paren {p \land \neg q} \vdash \neg \paren {p \iff q} }}
{{Premise|1|\paren {\neg p \land q} \lor \paren {p \land \neg q} }}
{{Commutation|2|1|\paren {p \land \neg q} \lor \paren {\neg p \land q}|1|Disjunction}}
{{Commutation|3|1|\paren {p \land \neg q} \lor \paren {q \land \neg p}|2|Conjunction}}
{{DoubleNegIntro|4|1|\paren {\neg \neg  p \land \neg q} \lor \paren {\neg \neg q \land \neg p}|3}}
{{DeMorgan|5|1|\neg \paren {\neg p \lor q} \lor \neg \paren {\neg q \lor p}|4|Conjunction of Negations}}
{{DeMorgan|6|1|\neg \paren {\paren {\neg p \lor q} \land \paren {\neg q \lor p} }|5|Disjunction of Negations}}
{{SequentIntro|7|1 |\neg \paren {\paren {p \implies q} \land \paren {q \implies p} }|6
  |Rule of Material Implication (twice)}}
{{SequentIntro|8|1|\neg \paren {p \iff q}|7|Rule of Material Equivalence}}
{{EndTableau}}
{{qed}}
Theorem: Non-Equivalence as Disjunction of Conjunctions/Formulation 2

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

Proof:
{{BeginTableau|\vdash \paren {\neg \paren {p \iff q} } \iff \paren {\paren {\neg p \land q} \lor \paren {p \land \neg q} } }}
{{Assumption|1|\neg \paren {p \iff q} }}
{{SequentIntro|2|1|\paren {\neg p \land q} \lor \paren {p \land \neg q}|1|Non-Equivalence as Disjunction of Conjunctions: Formulation 1}}
{{Implication|3||\paren {\neg \paren {p \iff q} } \implies \paren {\paren {\neg p \land q} \lor \paren {p \land \neg q} }|1|2}}
{{Assumption|4|\paren {\neg p \land q} \lor \paren {p \land \neg q} }}
{{SequentIntro|5|4|\neg \paren {p \iff q}|4|Non-Equivalence as Disjunction of Conjunctions: Formulation 1}}
{{Implication|6||\paren {\paren {\neg p \land q} \lor \paren {p \land \neg q} } \implies \paren {\neg \paren {p \iff q} }|4|5}}
{{BiconditionalIntro|7||\paren {\neg \paren {p \iff q} } \iff \paren {\paren {\neg p \land q} \lor \paren {p \land \neg q} }|3|6}}
{{EndTableau|qed}}
Theorem: Non-Equivalence as Equivalence with Negation/Formulation 1/Forward Implication

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

Proof:
{{BeginTableau|\neg \paren {p \iff q} \vdash \paren {p \iff \neg q} }}
{{Premise             | 1|\neg \paren {p \iff q} }}
{{SequentIntro        | 2|1|\neg \paren {\paren {p \implies q} \land \paren {q \implies p} }|1|Rule of Material Equivalence}}
{{DeMorgan            | 3|1|\neg \paren {p \implies q} \lor \neg \paren {q \implies p} |2|Disjunction of Negations}}
{{Assumption          | 4|p}}
{{IdentityLaw         | 5|4|p|4}}
{{Assumption          | 6|q}}
{{Implication         | 7|6|p \implies q|4|6}}
{{DoubleNegIntro      | 8|6|\neg \neg \paren {p \implies q}|7}}
{{ModusTollendoPonens | 9|1, 6|\neg \paren {q \implies p}|3|8|1}}
{{SequentIntro        |10|1, 6|q \land \neg p|9|Conjunction with Negative is Equivalent to Negation of Conditional}}
{{Simplification      |11|1, 6|\neg p|10|2}}
{{NonContradiction    |12|1, 4, 6|4|11}}
{{Contradiction       |13|1, 4|\neg q|6|12}}
{{Implication         |14|1|p \implies \neg q|4|13}}
{{Assumption          |15|\neg q}}
{{IdentityLaw         |16|15|\neg q|15}}
{{Assumption          |17|\neg p}}
{{Implication         |18|17|\neg q \implies \neg p|16|17}}
{{SequentIntro        |19|17|p \implies q|18|Rule of Transposition}}
{{ModusTollendoPonens |20|1, 17|\neg \paren {q \implies p} |3|19|1}}
{{SequentIntro        |21|1, 17|q \land \neg p|20|Conjunction with Negative is Equivalent to Negation of Conditional}}
{{Simplification      |22|1, 17|q|21|1}}
{{NonContradiction    |23|1, 15, 17|15|22}}
{{Contradiction       |24|1, 15|p|17|23}}
{{Implication         |25|1|\neg q \implies p|15|24}}
{{BiconditionalIntro  |26|1|\paren {p \iff \neg q}|14|25}}
{{EndTableau|qed}}
{{LEM||3}}
Theorem: Non-Equivalence as Equivalence with Negation/Formulation 1

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

Proof:
{{BeginTableau|\neg \paren {p \iff q} \vdash \paren {p \iff \neg q} }}
{{Premise             | 1|\neg \paren {p \iff q} }}
{{SequentIntro        | 2|1|\neg \paren {\paren {p \implies q} \land \paren {q \implies p} }|1|Rule of Material Equivalence}}
{{DeMorgan            | 3|1|\neg \paren {p \implies q} \lor \neg \paren {q \implies p} |2|Disjunction of Negations}}
{{Assumption          | 4|p}}
{{IdentityLaw         | 5|4|p|4}}
{{Assumption          | 6|q}}
{{Implication         | 7|6|p \implies q|4|6}}
{{DoubleNegIntro      | 8|6|\neg \neg \paren {p \implies q}|7}}
{{ModusTollendoPonens | 9|1, 6|\neg \paren {q \implies p}|3|8|1}}
{{SequentIntro        |10|1, 6|q \land \neg p|9|Conjunction with Negative is Equivalent to Negation of Conditional}}
{{Simplification      |11|1, 6|\neg p|10|2}}
{{NonContradiction    |12|1, 4, 6|4|11}}
{{Contradiction       |13|1, 4|\neg q|6|12}}
{{Implication         |14|1|p \implies \neg q|4|13}}
{{Assumption          |15|\neg q}}
{{IdentityLaw         |16|15|\neg q|15}}
{{Assumption          |17|\neg p}}
{{Implication         |18|17|\neg q \implies \neg p|16|17}}
{{SequentIntro        |19|17|p \implies q|18|Rule of Transposition}}
{{ModusTollendoPonens |20|1, 17|\neg \paren {q \implies p} |3|19|1}}
{{SequentIntro        |21|1, 17|q \land \neg p|20|Conjunction with Negative is Equivalent to Negation of Conditional}}
{{Simplification      |22|1, 17|q|21|1}}
{{NonContradiction    |23|1, 15, 17|15|22}}
{{Contradiction       |24|1, 15|p|17|23}}
{{Implication         |25|1|\neg q \implies p|15|24}}
{{BiconditionalIntro  |26|1|\paren {p \iff \neg q}|14|25}}
{{EndTableau|qed}}
{{LEM||3}}
Theorem: Non-Equivalence as Equivalence with Negation/Formulation 1

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

Proof:
=== Forward Implication: Proof ===
{{:Non-Equivalence as Equivalence with Negation/Formulation 1/Forward Implication/Proof}}
=== Reverse Implication: Proof ===
{{:Non-Equivalence as Equivalence with Negation/Formulation 1/Reverse Implication/Proof}}
Theorem: Non-Equivalence as Equivalence with Negation/Formulation 1

:$\neg \paren {p \iff q} \dashv \vdash \paren {p \iff \neg 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.
$\begin{array}{|cccc||cccc|} \hline
\neg & (p & \iff & q) & (p & \iff & \neg & q) \\
\hline
\F & \F & \T & \F & \T & \F & \T & \F \\
\T & \F & \F & \T & \T & \T & \F & \T  \\
\T & \T & \F & \F & \F & \T & \T & \F  \\
\F & \T & \T & \T & \F & \F & \F & \T  \\
\hline
\end{array}$
{{qed}}
Theorem: Non-Equivalence as Equivalence with Negation/Formulation 1

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

Proof:
{{BeginTableau | \paren {p \iff \neg q} \vdash \neg \paren {p \iff q} }}
{{Premise      | 1 | p \iff \neg q}}
{{SequentIntro | 2 | 1 |\neg \paren {p \iff \neg \neg q} | 1 | Non-Equivalence as Equivalence with Negation: Forward Implication}}
{{TheoremIntro | 3 | \neg \neg q \iff q | Double Negation}}
{{SequentIntro | 4 | 1 |\neg \paren {p \iff q} |2, 3| Biconditional is Transitive}}
{{EndTableau}}
Theorem: Non-Equivalence as Equivalence with Negation/Formulation 1/Reverse Implication

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

Proof:
{{BeginTableau | \paren {p \iff \neg q} \vdash \neg \paren {p \iff q} }}
{{Premise      | 1 | p \iff \neg q}}
{{SequentIntro | 2 | 1 |\neg \paren {p \iff \neg \neg q} | 1 | Non-Equivalence as Equivalence with Negation: Forward Implication}}
{{TheoremIntro | 3 | \neg \neg q \iff q | Double Negation}}
{{SequentIntro | 4 | 1 |\neg \paren {p \iff q} |2, 3| Biconditional is Transitive}}
{{EndTableau}}
Theorem: Sign of Function Matches Sign of Definite Integral

Let $f$ be a real function continuous on some closed interval $\closedint a b$, where $a < b$.
Then:
:If $\forall x \in \closedint a b: \map f x \ge 0$ then $\ds \int_a^b \map f x \rd x \ge 0$
:If $\forall x \in \closedint a b: \map f x > 0$ then $\ds \int_a^b \map f x \rd x > 0$
:If $\forall x \in \closedint a b: \map f x \le 0$ then $\ds \int_a^b \map f x \rd x \le 0$
:If $\forall x \in \closedint a b: \map f x < 0$ then $\ds \int_a^b \map f x \rd x < 0$

Proof:
From Continuous Real Function is Darboux Integrable, the definite integrals under discussion are guaranteed to exist.
Consider the case where $\forall x \in \closedint a b: \map f x \ge 0$.
Define a constant mapping:
:$f_0: \closedint a b \to \R$:
:$\map {f_0} x = 0$
Then:
{{begin-eqn}}
{{eqn | l = \map {f_0} x
      | o = \le
      | r = \map f x
      | c = for any $x \in \closedint a b$: recall $\map f x \ge 0$
}}
{{eqn | ll= \leadsto
      | l = \int_a^b \map {f_0} x \rd x
      | o = \le
      | r = \int_a^b \map f x \rd x
      | c = Relative Sizes of Definite Integrals
}}
{{eqn | ll= \leadsto
      | l = 0 \paren {b - a}
      | o = \le
      | r = \int_a^b \map f x \rd x
      | c = Definite Integral of Constant
}}
{{eqn | ll= \leadsto
      | l = \int_a^b \map f x \rd x
      | o = \ge
      | r = 0
}}
{{end-eqn}}
The proofs of the other cases are similar.
{{qed}}
Category:Integral Calculus
mju52q8rsujft31aelwalep4rs0qzkb
Theorem: Non-Equivalence as Equivalence with Negation/Formulation 2

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

Proof:
{{BeginTableau|\vdash \neg \paren {p \iff q} \iff \paren {p \iff \neg q} }}
{{Assumption|1|\neg \paren {p \iff q} }}
{{SequentIntro|2|1|p \iff \neg q|1|Non-Equivalence as Equivalence with Negation: Formulation 1}}
{{Implication|3||\paren {\neg \paren {p \iff q} } \implies \paren {p \iff \neg q}|1|2}}
{{Assumption|4|p \iff \neg q}}
{{SequentIntro|5|4|\neg \paren {p \iff q}|4|Non-Equivalence as Equivalence with Negation: Formulation 1}}
{{Implication|6||\paren {p \iff \neg q} \implies \paren {\neg \paren {p \iff q} }|4|5}}
{{BiconditionalIntro|7||\paren {\neg \paren {p \iff q} } \iff \paren {p \iff \neg q}|3|6}}
{{EndTableau}}
{{qed}}