avewright/proofwiki-math huggingface dataset:
Theorem: Cartesian Product of Group Actions

Let $\struct {G, \circ}$ be a group.
Let $S$ and $T$ be sets.
Let $*_S: G \times S \to S$ and $*_T: G \times T \to T$ be group actions.
Then the operation $*: G \times \paren {S \times T} \to S \times T$ defined as:
:$\forall \tuple {g, \tuple {s, t} } \in G \times \paren {S \times T}: g * \tuple {s, t} = \tuple {g *_S s, g *_T t}$
is a group action.

Proof:
The group action axioms are investigated in turn.
Let $g, h \in G$ and $s, t \in S$.
Thus:
{{begin-eqn}}
{{eqn | l = g * \tuple {h * \tuple {s, t} }
      | r = g * \tuple {h *_S s, h *_T t}
      | c = Definition of $*$
}}
{{eqn | r = \tuple {g *_S \tuple {h *_S s}, g *_T \tuple {h *_T t} }
      | c = Definition of $*$
}}
{{eqn | r = \tuple {\paren {g \circ h} *_S s, \paren {g \circ h} *_T t}
      | c = {{GroupActionAxiom|1}} for both $*_S$ and $*_T$
}}
{{eqn | r = \paren {g \circ h} * \tuple {s, t}
      | c = Definition of $*$
}}
{{end-eqn}}
demonstrating that {{GroupActionAxiom|1}} holds.
Then:
{{begin-eqn}}
{{eqn | l = e * \tuple {s, t}
      | r = \tuple {e *_S s, e *_T t}
      | c = Definition of $*$
}}
{{eqn | r = \tuple {s, t}
      | c = {{GroupActionAxiom|2}} for both $*_S$ and $*_T$
}}
{{end-eqn}}
demonstrating that {{GroupActionAxiom|2}} holds.
The group action axioms are thus seen to be fulfilled, and so $*$ is a group action.
{{qed}}
Theorem: Stabilizer of Cartesian Product of Group Actions

Let $\struct {G, \circ}$ be a group.
Let $S$ and $T$ be sets.
Let $*_S: G \times S \to S$ and $*_T: G \times T \to T$ be group actions.
Let the group action $*: G \times \paren {S \times T} \to S \times T$ be defined as:
:$\forall \tuple {g, \tuple {s, t} } \in G \times \paren {S \times T}: g * \tuple {s, t} = \tuple {g *_S s, g *_T t}$
Then the stabilizer of $\tuple {s, t} \in S \times T$ is given by:
:$\Stab {s, t} = \Stab s \cap \Stab t$
where $\Stab s$ and $\Stab t$ are the stabilizers of $s$ and $t$ under $*_S$ and $*_T$ respectively.

Proof:
By definition, the stabilizer of an element $x$ of $S$ is defined as:
:$\Stab x := \set {g \in G: g * x = x}$
where $*$ denotes the group action.
So:
{{begin-eqn}}
{{eqn | l = \Stab {s, t}
      | r = \set {g \in G: g * \tuple {s, t} = \tuple {s, t} }
      | c = {{Defof|Stabilizer}}
}}
{{eqn | r = \set {g \in G: \tuple {g *_S s, g *_T t} = \tuple {s, t} }
      | c = Definition of $*$
}}
{{eqn | r = \set {g \in G: g *_S s = s \land g *_T t = t}
      | c = {{Defof|Cartesian Product}}
}}
{{eqn | r = \set {g \in G: g \in \Stab s \land g \in \Stab t}
      | c = {{Defof|Stabilizer}}
}}
{{eqn | r = \Stab s \cap \Stab t
      | c = {{Defof|Set Intersection}}
}}
{{end-eqn}}
{{qed}}
Theorem: Index in Subgroup

Let $G$ be a group.
Let $H, K$ be subgroups of finite index of $G$.
Then:
:$\index H {H \cap K} \le \index G K$
where $\index G K$ denotes the index of $K$ in $G$.
Equality happens {{iff}} $G = H K$.

Proof:
We list out all the left cosets of $H \cap K$ in $H$:
:$H / \paren {H \cap K} = \set {h_n \paren {H \cap K}: h_n \in H, n \in I}$
where $I$ is some finite indexing set.
For each pair $h_i, h_j \in H \subseteq G$, where $i \ne j$:
:$h_i^{-1} h_j \notin H \cap K \quad$ Cosets are Equal iff Product with Inverse in Subgroup
Since $H$ is a subgroup, $h_i^{-1} h_j \in H$.
Thus:
:$h_i^{-1} h_j \notin K$
By Cosets are Equal iff Product with Inverse in Subgroup, $h_i K$ and $h_j K$ are different left cosets.
Hence there must be at least $\index H {H \cap K}$ left cosets of $K$ in $G$, namely $h_n K$ for each $n \in I$.
It follows that $\index H {H \cap K} \le \index G K$.
{{qed|lemma}}
Theorem: Finite Cyclic Group has Euler Phi Generators

Let $C_n$ be a (finite) cyclic group of order $n$.
Then $C_n$ has $\map \phi n$ generators, where $\map \phi n$ denotes the Euler $\phi$ function.

Proof:
From List of Elements in Finite Cyclic Group, the elements of $G$ are:
:$\set {g^k: g \in G, 0 \le k < n}$
From Power of Generator of Cyclic Group is Generator iff Power is Coprime with Order, $g^k$ generates $G$ {{iff}} $k \perp n$.
The result follows by definition of the Euler $\phi$ function.
{{qed}}
Theorem: Composition of Left Regular Representations

:$\lambda_x \circ \lambda_y = \lambda_{x * y}$

Proof:
Let $z \in S$.
{{begin-eqn}}
{{eqn | l = \map {\lambda_x \circ \lambda_y} z
      | r = \map {\lambda_x} {\map {\lambda_y} z}
      | c = {{Defof|Composition of Mappings}}
}}
{{eqn | r = \map {\lambda_x} {y * z}
      | c = {{Defof|Left Regular Representation}}
}}
{{eqn | r = x * \paren {y * z}
      | c = {{Defof|Left Regular Representation}}
}}
{{eqn | r = \paren {x * y} * z
      | c = {{Semigroup-axiom|1}}
}}
{{eqn | r = \map {\lambda_{x * y} } z
      | c = {{Defof|Left Regular Representation}}
}}
{{end-eqn}}
{{qed}}
Theorem: Composition of Right Regular Representations

:$\rho_x \circ \rho_y = \rho_{y * x}$

Proof:
Let $z \in S$.
{{begin-eqn}}
{{eqn | l = \map {\paren {\rho_x \circ \rho_y} } z
      | r = \map {\rho_x} {\map {\rho_y} z}
      | c = {{Defof|Composition of Mappings}}
}}
{{eqn | r = \map {\rho_x} {z * y}
      | c = {{Defof|Right Regular Representation}}
}}
{{eqn | r = \paren {z * y} * x
      | c = {{Defof|Right Regular Representation}}
}}
{{eqn | r = z * \paren {y * x}
      | c = {{Semigroup-axiom|1}}
}}
{{eqn | r = \map {\rho_{y * x} } z
      | c = {{Defof|Right Regular Representation}}
}}
{{end-eqn}}
{{qed}}
Theorem: Composition of Left Regular Representation with Right

:$\lambda_x \circ \rho_y = \rho_y \circ \lambda_x$

Proof:
Let $z \in S$.
{{begin-eqn}}
{{eqn | l = \map {\paren {\lambda_x \circ \rho_y} } z
      | r = \map {\lambda_x} {\map {\rho_y} z}
      | c = {{Defof|Composition of Mappings}}
}}
{{eqn | r = \map {\lambda_x} {z * y}
      | c = {{Defof|Right Regular Representation}}
}}
{{eqn | r = x * \paren {z * y}
      | c = {{Defof|Left Regular Representation}}
}}
{{eqn | r = \paren {x * z} * y
      | c = {{Semigroup-axiom|1}}
}}
{{eqn | r = \map {\rho_y} {x * z}
      | c = {{Defof|Right Regular Representation}}
}}
{{eqn | r = \map {\rho_y} {\map {\lambda_x} z}
      | c = {{Defof|Left Regular Representation}}
}}
{{eqn | r = \map {\paren {\rho_y \circ \lambda_x} } z
      | c = {{Defof|Composition of Mappings}}
}}
{{end-eqn}}
{{qed}}
Theorem: Extendability Theorem for Derivatives Continuous on Open Intervals

Let $f$ be a continuous real function defined on an interval $\closedint a b$ where $a < b$.
Then $f$ is continuously differentiable on $\closedint a b$ {{iff}}:
:$f$ is continuously differentiable on $\openint a b$
and:
:$\ds \lim_{x \mathop \to a^+} \map {f'} x$ and $\ds \lim_{x \mathop \to b^-} \map {f'} x$ exist.

Proof:
=== Necessary Condition ===
Suppose that $f$ is continuously differentiable on $\closedint a b$.
We need to show that:
:$f$ is continuously differentiable on $\openint a b$
and:
:$\ds \lim_{x \mathop \to a^+} \map {f'} x$ and $\ds \lim_{x \mathop \to b^-} \map {f'} x$ exist.
$f$ is continuously differentiable on $\openint a b$ because:
:$f$ is continuously differentiable on $\closedint a b$
:$\openint a b$ is a subset of $\closedint a b$. 
What remains to show is that $\ds \lim_{x \mathop \to a^+} \map {f'} x$ and $\ds \lim_{x \mathop \to b^-} \map {f'} x$ exist.
We shall only make a proof of the existence of $\ds \lim_{x \mathop \to a^+} \map {f'} x$ as the proof of the existence of $\ds \lim_{x \mathop \to b^-} \map {f'} x$ is similar.
Since $f$ is differentiable at $a$, $\map {f'} a$ exists.
Since $f'$ is continuous at $a$, the following equation is true:
:$\ds \map {f'} a = \lim_{x \mathop \to a^+} \map {f'} x$
Therefore the {{RHS}} of this equation exists.
{{qed|lemma}}
Theorem: Universal Affirmative and Universal Negative are Contrary iff First Predicate is not Vacuous

Consider the categorical statements:
{{begin-axiom}}
{{axiom | ll = \mathbf A:
        | lc= The universal affirmative:
        | q = \forall x
        | m = \map S x \implies \map P x
}}
{{axiom | ll= \mathbf E:
        | lc= The universal negative:
        | q = \forall x
        | m = \map S x \implies \neg \map P x
}}
{{end-axiom}}
Then:
:$\mathbf A$ and $\mathbf E$ are contrary
{{iff}}:
:$\exists x: \map S x$
Using the symbology of predicate logic:
:$\exists x: \map S x \iff \neg \paren {\paren {\forall x: \map S x \implies \map P x} \land \paren {\forall x: \map S x \implies \neg \map P x} }$

Proof:
=== Sufficient Condition ===
Let $\exists x: \map S x$.
Suppose $\mathbf A$ and $\mathbf E$ are both true.
As $\mathbf A$ is true, then by Modus Ponendo Ponens:
:$\map P x$
As $\mathbf E$ is true, then by Modus Ponendo Ponens:
:$\neg \map P x$
It follows by Proof by Contradiction that $\mathbf A$ and $\mathbf E$ are not both true.
Thus, by definition, $\mathbf A$ and $\mathbf E$ are contrary statements.
{{qed|lemma}}
Theorem: Particular Affirmative and Particular Negative are Subcontrary iff First Predicate is not Vacuous

Consider the categorical statements:
{{begin-axiom}}
{{axiom | ll = \mathbf I:
        | lc= The particular affirmative:
        | q = \exists x
        | m = \map S x \land \map P x
}}
{{axiom | ll= \mathbf O:
        | lc= The particular negative:
        | q = \exists x
        | m = \map S x \land \neg \map P x
}}
{{end-axiom}}
Then:
:$\mathbf I$ and $\mathbf O$ are subcontrary
{{iff}}:
:$\exists x: \map S x$
Using the symbology of predicate logic:
:$\exists x: \map S x \iff \paren {\paren {\exists x: \map S x \land \map P x} \lor \paren {\exists x: \map S x \land \neg \map P x} }$

Proof:
=== Sufficient Condition ===
Let $\exists x: \map S x$.
Suppose $\mathbf I$ and $\mathbf O$ are both false.
As $\mathbf I$ is false, then by the Rule of Conjunction:
:$\neg \map P x$
As $\mathbf O$ is false, then by the Rule of Conjunction:
:$\neg \neg \map P x$
and so by Double Negation:
:$\map P x$
It follows by Proof by Contradiction that $\mathbf I$ and $\mathbf O$ are not both false.
Thus, by definition, $\mathbf I$ and $\mathbf O$ are subcontrary statements.
{{qed|lemma}}
Theorem: Universal Affirmative and Particular Negative are Contradictory

Consider the categorical statements:
{{begin-axiom}}
{{axiom | ll = \mathbf A:
        | lc= The universal affirmative:
        | q = \forall x
        | m = \map S x \implies \map P x
}}
{{axiom | ll= \mathbf O:
        | lc= The particular negative:
        | q = \exists x
        | m = \map S x \land \neg \map P x
}}
{{end-axiom}}
Then $\mathbf A$ and $\mathbf O$ are contradictory.
Using the symbology of predicate logic:
:$\neg \paren {\paren {\forall x: \map S x \implies \map P x} \iff \paren {\exists x: \map S x \land \neg \map P x} }$

Proof:
{{begin-eqn}}
{{eqn | o = 
      | r = \mathbf A
      | c = 
}}
{{eqn | ll= \leadsto
      | q = \forall x
      | o = 
      | r = \map S x \implies \map P x
      | c = Definition of $\mathbf A$
}}
{{eqn | ll= \leadsto
      | q = \forall x
      | o = 
      | r = \neg \paren {\map S x \land \neg \map P x}
      | c = Conditional is Equivalent to Negation of Conjunction with Negative
}}
{{eqn | ll= \leadsto
      | q = \neg \exists x
      | o = 
      | r = \map S x \land \neg \map P x
      | c = De Morgan's Laws: Denial of Existence
}}
{{eqn | ll= \leadsto
      | o = 
      | r = \neg \mathbf O
      | c = Definition of $\mathbf O$
}}
{{end-eqn}}
The argument reverses:
{{begin-eqn}}
{{eqn | o = 
      | r = \mathbf O
      | c = 
}}
{{eqn | ll= \leadsto
      | q = \exists x
      | o = 
      | r = \map S x \land \neg \map P x
      | c = Definition of $\mathbf O$
}}
{{eqn | ll= \leadsto
      | q = \exists x
      | o = 
      | r = \neg \paren {\map S x \implies \map P x}
      | c = Conjunction with Negative is Equivalent to Negation of Conditional
}}
{{eqn | ll= \leadsto
      | q = \neg \forall x
      | o = 
      | r = \map S x \implies \map P x
      | c = De Morgan's Laws: Denial of Universality
}}
{{eqn | ll= \leadsto
      | o = 
      | r = \neg \mathbf A
      | c = Definition of $\mathbf A$
}}
{{end-eqn}}
The result follows by definition of contradictory.
{{qed}}
Theorem: Particular Affirmative and Universal Negative are Contradictory

Consider the categorical statements:
{{begin-axiom}}
{{axiom | ll = \mathbf I:
        | lc= The particular affirmative:
        | q = \exists x
        | m = \map S x \land \map P x
}}
{{axiom | ll= \mathbf E:
        | lc= The universal negative:
        | q = \forall x
        | m = \map S x \implies \neg \map P x
}}
{{end-axiom}}
Then $\mathbf I$ and $\mathbf E$ are contradictory.
Using the symbology of predicate logic:
:$\neg \paren {\paren {\exists x: \map S x \land \map P x} \iff \paren {\forall x: \map S x \implies \neg \map P x} }$

Proof:
{{begin-eqn}}
{{eqn | o = 
      | r = \mathbf E
      | c = 
}}
{{eqn | ll= \therefore
      | l = \forall x:
      | o = 
      | r = \map S x \implies \neg \map P x
      | c = Definition of $\mathbf E$
}}
{{eqn | ll= \therefore
      | l = \forall x:
      | o = 
      | r = \neg \paren {\map S x \land \map P x}
      | c = Modus Ponendo Tollens
}}
{{eqn | ll= \therefore
      | l = \neg \exists x:
      | o = 
      | r = \map S x \land \map P x
      | c = De Morgan's Laws: Denial of Existence
}}
{{eqn | ll= \therefore
      | o = 
      | r = \neg \mathbf I
      | c = Definition of $\mathbf I$
}}
{{end-eqn}}
The argument reverses:
{{begin-eqn}}
{{eqn | o = 
      | r = \mathbf I
      | c = 
}}
{{eqn | ll= \therefore
      | l = \exists x:
      | o = 
      | r = \map S x \land \map P x
      | c = Definition of $\mathbf I$
}}
{{eqn | ll= \therefore
      | l = \exists x:
      | o = 
      | r = \neg \paren {\map S x \implies \neg \map P x}
      | c = Conjunction is Equivalent to Negation of Conditional of Negative
}}
{{eqn | ll= \therefore
      | l = \neg \forall x:
      | o = 
      | r = \map S x \implies \neg \map P x
      | c = De Morgan's Laws: Denial of Universality
}}
{{eqn | ll= \therefore
      | o = 
      | r = \neg \mathbf E
      | c = Definition of $\mathbf E$
}}
{{end-eqn}}
The result follows by definition of contradictory.
{{qed}}
Theorem: Universal Affirmative implies Particular Affirmative iff First Predicate is not Vacuous

Consider the categorical statements:
{{begin-axiom}}
{{axiom | ll = \map {\mathbf A} {S, P}:
        | lc= The universal affirmative:
        | q = \forall x
        | m = \map S x \implies \map P x
}}
{{axiom | ll= \map {\mathbf I} {S, P}:
        | lc= The particular affirmative:
        | q = \exists x
        | m = \map S x \land \map P x
}}
{{end-axiom}}
Then:
:$\map {\mathbf A} {S, P} \implies \map {\mathbf I} {S, P}$
{{iff}}:
:$\exists x: \map S x$
Using the symbology of predicate logic:
:$\exists x: \map S x \iff \paren {\paren {\forall x: \map S x \implies \map P x} \implies \paren {\exists x: \map S x \land \map P x} }$

Proof:
=== Sufficient Condition ===
Let $\exists x: \map S x$.
Let $\map {\mathbf A} {S, P}$ be true.
As $\map {\mathbf A} {S, P}$ is true, then by Modus Ponendo Ponens:
:$\map P x$
From the Rule of Conjunction:
:$\map S x \land \map P x$
Thus $\map {\mathbf I} {S, P}$ holds.
So by the Rule of Implication:
:$\map {\mathbf A} {S, P} \implies \map {\mathbf I} {S, P}$
{{qed|lemma}}
Theorem: Universal Negative implies Particular Negative iff First Predicate is not Vacuous

Consider the categorical statements:
{{begin-axiom}}
{{axiom | ll = \map {\mathbf E} {S, P}:
        | lc= The universal negative:
        | q = \forall x
        | m = \map S x \implies \neg \map P x
}}
{{axiom | ll= \map {\mathbf O} {S, P}:
        | lc= The particular negative:
        | q = \exists x
        | m = \map S x \land \neg \map P x
}}
{{end-axiom}}
Then:
:$\map {\mathbf E} {S, P} \implies \map {\mathbf O} {S, P}$
{{iff}}:
:$\exists x: \map S x$
Using the symbology of predicate logic:
:$\exists x: \map S x \iff \paren {\paren {\forall x: \map S x \implies \neg \map P x} \implies \paren {\exists x: \map S x \land \neg \map P x} }$

Proof:
=== Sufficient Condition ===
Let $\exists x: \map S x$.
Let $\map {\mathbf E} {S, P}$ be true.
As $\map {\mathbf E} {S, P}$ is true, then by Modus Ponendo Ponens:
:$\neg \map P x$
From the Rule of Conjunction:
:$\map S x \land \neg \map P x$
Thus $\map {\mathbf O} {S, P}$ holds.
So by the Rule of Implication:
:$\map {\mathbf E} {S, P} \implies \map {\mathbf O} {S, P}$
{{qed|lemma}}
Theorem: Socrates is Mortal

:$(1): \quad$ ''All humans are mortal.''
:$(2): \quad$ ''{{AuthorRef|Socrates}} is human.''
:$(3): \quad$ ''Therefore {{AuthorRef|Socrates}} is mortal.''

Proof:
Let $x$ be an object variable from the universe of '''rational beings'''.
Let $\map H x$ denote the propositional function ''$x$ is '''human'''''.
Let $\map M x$ denote the propositional function ''$x$ is '''mortal'''''.
Let $S$ be a proper name that denotes {{AuthorRef|Socrates}}.
The argument can then be expressed as:
{{begin-eqn}}
{{eqn | n = 1
      | q = \forall x
      | l = \map H x
      | o = \implies
      | r = \map M x
      | c = 
}}
{{eqn | ll= \therefore
      | l = \map H S
      | o = \implies
      | r = \map M S
      | c = Universal Instantiation
}}
{{eqn | n = 2
      | l = \map H S
      | o = 
      | c = 
}}
{{eqn | n = 3
      | ll= \therefore
      | l = \map M S
      | o = 
      | c = Modus Ponendo Ponens
}}
{{end-eqn}}
That is: 
:''{{AuthorRef|Socrates}} is mortal.''
{{qed}}
Theorem: Right-Hand Differentiable Function is Right-Continuous

Let $f$ be a real function defined on an interval $I$.
Let $a$ be a point in $I$ where $f$ is right-hand differentiable.
Then $f$ is right-continuous at $a$.

Proof:
By hypothesis, $\map {f'_+} a$ exists.
First we note that $a$ cannot be the right hand end point of $I$ because values in $I$ greater than $a$ need to exist for $\map {f'_+} a$ to exist.
We form the following expression:
:$\ds \lim_{x \mathop \to a^+} \paren {\map f x - \map f a}$
We need to show that it is defined and to find its value.
We find:
{{begin-eqn}}
{{eqn | o = 
      | r = \lim_{x \mathop \to a^+} \paren {\map f x - \map f a}
      | c = 
}}
{{eqn | r = \lim_{x \mathop \to a^+} \paren {\frac {\map f x - \map f a} {x - a} \paren {x - a} }
      | c = where the denominator is unequal to $0$ since $x > a$
}}
{{eqn | r = \lim_{x \mathop \to a^+} \paren {\frac {\map f x - \map f a} {x - a} } \lim_{x \mathop \to a^+} \paren {x - a}
      | c = Product Rule for Limits of Real Functions since (see the next step) the two limits exist
}}
{{eqn | r = \map {f'_+} a \times 0
      | c = {{Defof|Right-Hand Derivative}}
}}
{{eqn | r = 0
}}
{{end-eqn}}
Note that this proves that $\ds \lim_{x \mathop \to a^+} \paren {\map f x - \map f a}$ exists.
We continue by manipulating the result above:
{{begin-eqn}}
{{eqn | l = \lim_{x \mathop \to a^+} \paren {\map f x - \map f a}
      | r = 0
}}
{{eqn | ll= \leadstoandfrom
      | l = \lim_{x \mathop \to a^+} \paren {\map f x - \map f a} + \map f a - \map f a
      | r = 0
}}
{{eqn | ll= \leadstoandfrom
      | l = \lim_{x \mathop \to a^+} \paren {\map f x - \map f a} + \lim_{x \mathop \to a^+} \map f a - \map f a
      | r = 0
}}
{{eqn | ll= \leadstoandfrom
      | l = \lim_{x \mathop \to a^+} \paren {\map f x - \map f a + \map f a} - \map f a
      | r = 0
      | c = Sum Rule for Limits of Real Functions since the two limits in the previous expression exist
}}
{{eqn | ll= \leadstoandfrom
      | l = \lim_{x \mathop \to a^+} \map f x - \map f a
      | r = 0
}}
{{eqn | ll= \leadstoandfrom
      | l = \lim_{x \mathop \to a^+} \map f x
      | r = \map f a
}}
{{end-eqn}}
which means that $f$ is right-continuous at $a$.
{{qed}}
Category:Continuous Real Functions
Category:Differentiable Real Functions
9830sha97llwlmm74g4jh220icwy929
Theorem: Left-Hand Differentiable Function is Left-Continuous

Let $f$ be a real function defined on an interval $I$.
Let $a$ be a point in $I$ where $f$ is left-hand differentiable.
Then $f$ is left-continuous at $a$.

Proof:
By hypothesis, $\map {f'_-} a$ exists.
First we note that $a$ cannot be the left-hand end point of $I$ because values in $I$ less than $a$ need to exist for $\map {f'_-} a$ to exist.
We form the following expression:
:$\ds \lim_{x \mathop \to a^-} \paren {\map f x - \map f a}$
We need to show that it is defined and to find its value.
We find:
{{begin-eqn}}
{{eqn | o = 
      | r = \lim_{x \mathop \to a^-} \paren {\map f x - \map f a}
      | c = 
}}
{{eqn | r = \lim_{x \mathop \to a^-} \paren {\frac {\map f x - \map f a} {x - a} \paren {x - a} }
      | c = where the denominator is unequal to $0$ since $x < a$
}}
{{eqn | r = \lim_{x \mathop \to a^-} \paren {\frac {\map f x - \map f a} {x - a} } \lim_{x \mathop \to a^-} \paren {x - a}
      | c = Product Rule for Limits of Real Functions since (see the next step) the two limits exist
}}
{{eqn | r = \map {f'_-} a \times 0
      | c = {{Defof|Left-Hand Derivative}}
}}
{{eqn | r = 0
}}
{{end-eqn}}
Note that this proves that $\ds \lim_{x \mathop \to a^-} \paren {\map f x - \map f a}$ exists.
We continue by manipulating the result above:
{{begin-eqn}}
{{eqn | l = \lim_{x \mathop \to a^-} \paren {\map f x - \map f a}
      | r = 0
}}
{{eqn | ll= \leadstoandfrom
      | l = \lim_{x \mathop \to a^-} \paren {\map f x - \map f a} + \map f a - \map f a
      | r = 0
}}
{{eqn | ll= \leadstoandfrom
      | l = \lim_{x \mathop \to a^-} \paren {\map f x - \map f a} + \lim_{x \mathop \to a^-} \map f a - \map f a
      | r = 0
}}
{{eqn | ll= \leadstoandfrom
      | l = \lim_{x \mathop \to a^-} \paren {\map f x - \map f a + \map f a} - \map f a
      | r = 0
      | c = Sum Rule for Limits of Real Functions since the two limits in the previous expression exist
}}
{{eqn | ll= \leadstoandfrom
      | l = \lim_{x \mathop \to a^-} \map f x - \map f a
      | r = 0
}}
{{eqn | ll= \leadstoandfrom
      | l = \lim_{x \mathop \to a^-} \map f x
      | r = \map f a
}}
{{end-eqn}}
which means that $f$ is left-continuous at $a$.
{{qed}}
Category:Continuous Real Functions
Category:Differentiable Real Functions
lfhy8xo3towmwzzjf4z7vgc72ek9jp4
Theorem: Left-Hand and Right-Hand Differentiable Function is Continuous

Let $f$ be a real function defined on an interval $I$.
Let $a$ be a point in $I$ where $f$ is left- and right-hand differentiable.
Then $f$ is continuous at $a$.

Proof:
By Left-Hand Differentiable Function is Left-Continuous, $f$ is left-continuous at $a$.
By Right-Hand Differentiable Function is Right-Continuous, $f$ is right-continuous at $a$.
By Continuous at Point iff Left-Continuous and Right-Continuous, $f$ is continuous at $a$.
{{qed}}
Category:Continuous Real Functions
Category:Differentiable Real Functions
78jtxwtfwuonzchv2xl9opvrnuag4rz