avewright/proofwiki-math huggingface dataset:
Theorem: Laplace Transform of cos a t by cosh a t

:$\map {\laptrans {\cos a t \cosh a t} } s = \dfrac {s^3} {s^4 + 4 a^4}$

Proof:
First we note that:
{{begin-eqn}}
{{eqn | l = \cos a t \cosh a t
      | r = \cos a t \paren {\dfrac {e^{a t} + e^{-a t} } 2}
      | c = {{Defof|Hyperbolic Cosine}}
}}
{{eqn | n = 1
      | r = \dfrac 1 2 \paren {e^{a t} \cos a t + e^{-a t} \cos a t}
      | c = 
}}
{{end-eqn}}
Hence:
{{begin-eqn}}
{{eqn | l = \map {\laptrans {\cos a t \cosh a t} } s
      | r = \map {\laptrans {\dfrac 1 2 \paren {e^{a t} \cos a t + e^{-a t} \cos a t} } } s
      | c = from $(1)$
}}
{{eqn | r = \dfrac 1 2 \paren {\map {\laptrans {e^{a t} \cos a t} } s + \map {\laptrans {e^{-a t} \cos a t} } s}
      | c = Linear Combination of Laplace Transforms
}}
{{eqn | r = \dfrac 1 2 \paren {\dfrac {s - a} {\paren {s - a}^2 + a^2} + \dfrac {s + a} {\paren {s + a}^2 + a^2} }
      | c = Laplace Transform of Exponential times Cosine
}}
{{eqn | r = \dfrac 1 2 \paren {\dfrac {\paren {s - a} \paren {\paren {s + a}^2 + a^2} + \paren {s + a} \paren {\paren {s - a}^2 + a^2} } {\paren {\paren {s - a}^2 + a^2} \paren {\paren {s + a}^2 + a^2} } }
      | c = common denominator
}}
{{eqn | r = \dfrac 1 2 \paren {\dfrac {\paren {s - a} \paren {s^2 + 2 a s + 2 a^2} + \paren {s + a} \paren {s^2 - 2 a s + 2 a^2} } {\paren {s^2 - 2 a s + 2 a^2} \paren {s^2 + 2 a s + 2 a^2} } }
      | c = multiplying out
}}
{{eqn | r = \dfrac 1 2 \paren {\dfrac {s^3 + 2 a s^2 + 2 a^2 s - a s^2 - 2 a^2 s - 2 a^3 + s^3 - 2 a s^2 + 2 a^2 s + a s^2 - 2 a^2 s + 2 a^3} {s^4 + 4 a^4} }
      | c = multiplying out, and Sophie Germain's Identity
}}
{{eqn | r = \dfrac {s^3} {s^4 + 4 a^4}
      | c = simplifying
}}
{{end-eqn}}
{{qed}}
Theorem: Inverse Laplace Transform of 1 over s^4 - a^4

:$\map {\laptrans {\dfrac 1 {2 a^3} \paren {\sinh a t - \sin a t} } } s = \dfrac 1 {s^4 - a^4}$

Proof:
{{begin-eqn}}
{{eqn | l = \map {\laptrans {\dfrac 1 {2 a^3} \paren {\sinh a t - \sin a t} } } s
      | r = \dfrac 1 {2 a^3} \paren {\map {\laptrans {\sinh a t} } s - \map {\laptrans {\sin a t} } s}
      | c = Linear Combination of Laplace Transforms
}}
{{eqn | r = \dfrac 1 {2 a^3} \paren {\dfrac a {s^2 - a^2} - \dfrac a {s^2 + a^2} }
      | c = Laplace Transform of Hyperbolic Sine, Laplace Transform of Sine
}}
{{eqn | r = \dfrac 1 {2 a^3} \paren {\dfrac {a \paren {s^2 + a^2} - a \paren {s^2 - a^2} } {\paren {s^2 + a^2} \paren {s^2 - a^2} } }
      | c = common denominator
}}
{{eqn | r = \dfrac 1 {2 a^3} \paren {\dfrac {a s^2 + a^3 - a s^2 + a^3} {s^4 - a^4} }
      | c = multiplying out, and Difference of Two Squares
}}
{{eqn | r = \dfrac 1 {s^4 - a^4}
      | c = simplifying
}}
{{end-eqn}}
{{qed}}
Theorem: Inverse Laplace Transform of s over s^4 - a^4

:$\map {\laptrans {\dfrac 1 {2 a^2} \paren {\cosh a t - \cos a t} } } s = \dfrac s {s^4 - a^4}$

Proof:
{{begin-eqn}}
{{eqn | l = \map {\laptrans {\dfrac 1 {2 a^2} \paren {\cosh a t - \cos a t} } } s
      | r = \dfrac 1 {2 a^2} \paren {\map {\laptrans {\cosh a t} } s - \map {\laptrans {\cos a t} } s}
      | c = Linear Combination of Laplace Transforms
}}
{{eqn | r = \dfrac 1 {2 a^2} \paren {\dfrac s {s^2 - a^2} - \dfrac s {s^2 + a^2} }
      | c = Laplace Transform of Hyperbolic Cosine, Laplace Transform of Cosine
}}
{{eqn | r = \dfrac 1 {2 a^2} \paren {\dfrac {s \paren {s^2 + a^2} - s \paren {s^2 - a^2} } {\paren {s^2 + a^2} \paren {s^2 - a^2} } }
      | c = common denominator
}}
{{eqn | r = \dfrac 1 {2 a^2} \paren {\dfrac {s^3 + a^2 s - s^3 + a^2 s} {s^4 - a^4} }
      | c = multiplying out, and Difference of Two Squares
}}
{{eqn | r = \dfrac s {s^4 - a^4}
      | c = simplifying
}}
{{end-eqn}}
{{qed}}
Theorem: Inverse Laplace Transform of s^2 over s^4 - a^4

:$\map {\laptrans {\dfrac 1 {2 a} \paren {\sinh a t + \sin a t} } } s = \dfrac {s^2} {s^4 - a^4}$

Proof:
{{begin-eqn}}
{{eqn | l = \map {\laptrans {\dfrac 1 {2 a} \paren {\sinh a t + \sin a t} } } s
      | r = \dfrac 1 {2 a} \paren {\map {\laptrans {\sinh a t} } s + \map {\laptrans {\sin a t} } s}
      | c = Linear Combination of Laplace Transforms
}}
{{eqn | r = \dfrac 1 {2 a} \paren {\dfrac a {s^2 - a^2} + \dfrac a {s^2 + a^2} }
      | c = Laplace Transform of Hyperbolic Sine, Laplace Transform of Sine
}}
{{eqn | r = \dfrac 1 {2 a} \paren {\dfrac {a \paren {s^2 + a^2} + a \paren {s^2 - a^2} } {\paren {s^2 + a^2} \paren {s^2 - a^2} } }
      | c = common denominator
}}
{{eqn | r = \dfrac 1 {2 a} \paren {\dfrac {a s^2 + a^3 + a s^2 - a^3} {s^4 - a^4} }
      | c = multiplying out, and Difference of Two Squares
}}
{{eqn | r = \dfrac {s^2} {s^4 - a^4}
      | c = simplifying
}}
{{end-eqn}}
{{qed}}
Theorem: Inverse Laplace Transform of s^3 over s^4 - a^4

:$\map {\laptrans {\dfrac 1 2 \paren {\cosh a t - \cos a t} } } s = \dfrac {s^3} {s^4 - a^4}$

Proof:
{{begin-eqn}}
{{eqn | l = \map {\laptrans {\dfrac 1 2 \paren {\cosh a t + \cos a t} } } s
      | r = \dfrac 1 2 \paren {\map {\laptrans {\cosh a t} } s + \map {\laptrans {\cos a t} } s}
      | c = Linear Combination of Laplace Transforms
}}
{{eqn | r = \dfrac 1 2 \paren {\dfrac s {s^2 - a^2} + \dfrac s {s^2 + a^2} }
      | c = Laplace Transform of Hyperbolic Cosine, Laplace Transform of Cosine
}}
{{eqn | r = \dfrac 1 2 \paren {\dfrac {s \paren {s^2 + a^2} + s \paren {s^2 - a^2} } {\paren {s^2 + a^2} \paren {s^2 - a^2} } }
      | c = common denominator
}}
{{eqn | r = \dfrac 1 2 \paren {\dfrac {s^3 + a^2 s + s^3 - a^2 s} {s^4 - a^4} }
      | c = multiplying out, and Difference of Two Squares
}}
{{eqn | r = \dfrac {s^3} {s^4 - a^4}
      | c = simplifying
}}
{{end-eqn}}
{{qed}}
Theorem: Equivalence of Definitions of Complete Lattice Isomorphism

Let $L_1 = \struct {A_1, \preceq_1}$ and $L_2 = \struct {A_2, \preceq_2}$ be complete lattices.
Let $\phi: A_1 \to A_2$ be a mapping.
{{TFAE|def = Complete Lattice Isomorphism}}
=== Definition 1 ===
{{:Definition:Complete Lattice Isomorphism/Definition 1}}
=== Definition 2 ===
{{:Definition:Complete Lattice Isomorphism/Definition 2}}
=== Definition 3 ===
{{:Definition:Complete Lattice Isomorphism/Definition 3}}

Proof:
=== Definition 1 implies Definition 2 ===
Let $\phi : L_1 \to L_2$ be a bijective complete lattice homomorphism.
{{:Equivalence of Definitions of Complete Lattice Isomorphism/Definition 1 Implies Definition 2}}{{qed|lemma}}
Theorem: Equivalence of Definitions of Complete Lattice Isomorphism/Definition 1 Implies Definition 2

Let $L_1 = \struct {A_1, \preceq_1}$ and $L_2 = \struct {A_2, \preceq_2}$ be complete lattices.
Let $\phi : L_1 \to L_2$ be a bijective complete lattice homomorphism.
Then:
:$\phi : L_1 \to L_2$ is an order isomorphism

Proof:
From Complete Lattice Homomorphism is Lattice Homomorphism:
:$\phi : \struct {A_1, \vee_1, \wedge_1, \preceq_1} \to \struct {A_2, \vee_2, \wedge_2, \preceq_2}$ is a lattice homomorphism
where 
:$\wedge_1, \vee_1$ denote  the meet and join on $L_1$
:$\wedge_2, \vee_2$ denote  the meet and join on $L_2$
Hence $\phi : \struct {A_1, \vee_1, \wedge_1, \preceq_1} \to \struct {A_2, \vee_2, \wedge_2, \preceq_2}$ is a bijective lattice homomorphism.
That is, $\phi : \struct {A_1, \vee_1, \wedge_1, \preceq_1} \to \struct {A_2, \vee_2, \wedge_2, \preceq_2}$ is a lattice isomorphism by definition.
From Equivalence of Definitions of Lattice Isomorphism:
:$\phi : L_1 \to L_2$ is an order isomorphism
Theorem: Equivalence of Definitions of Complete Lattice Isomorphism/Definition 2 Implies Definition 3

Let $L_1 = \struct {A_1, \preceq_1}$ and $L_2 = \struct {A_2, \preceq_2}$ be complete lattices.
Let $\phi : L_1 \to L_2$ be an order isomorphism.
Then:
:$\phi : \struct {A_1, \vee_1, \wedge_1, \preceq_1} \to \struct {A_2, \vee_2, \wedge_2, \preceq_2}$ is a lattice isomorphism
where 
:$\wedge_1, \vee_1$ denote  the meet and join on $L_1$
:$\wedge_2, \vee_2$ denote  the meet and join on $L_2$

Proof:
From Complete Lattice is Lattice:
:$\struct {A_1, \vee_1, \wedge_1, \preceq_1}$ and $\struct {A_2, \vee_2, \wedge_2, \preceq_2}$ are lattices
where 
:$\wedge_1, \vee_1$ denote  the meet and join on $L_1$
:$\wedge_2, \vee_2$ denote  the meet and join on $L_2$
Hence $\phi : \struct {A_1, \vee_1, \wedge_1, \preceq_1} \to \struct {A_2, \vee_2, \wedge_2, \preceq_2}$ is an order isomorphism between lattices.
By definition of lattice isomorphism:
:$\phi : \struct {A_1, \vee_1, \wedge_1, \preceq_1} \to \struct {A_2, \vee_2, \wedge_2, \preceq_2}$ is a lattice isomorphism
Theorem: Equivalence of Definitions of Complete Lattice Isomorphism/Definition 3 Implies Definition 1

Let $L_1 = \struct {A_1, \preceq_1}$ and $L_2 = \struct {A_2, \preceq_2}$ be complete lattices.
Let $\phi : \struct {A_1, \vee_1, \wedge_1, \preceq_1} \to \struct {A_2, \vee_2, \wedge_2, \preceq_2}$ be a lattice isomorphism
where 
:$\wedge_1, \vee_1$ denote  the meet and join on $L_1$
:$\wedge_2, \vee_2$ denote  the meet and join on $L_2$
Then:
:$\phi : \struct {A_1, \vee_1, \wedge_1, \preceq_1} \to \struct {A_2, \vee_2, \wedge_2, \preceq_2}$ is a bijective complete lattice homomorphism

Proof:
From Complete Lattice is Lattice:
:$\struct {A_1, \vee_1, \wedge_1, \preceq_1}$ and $\struct {A_2, \vee_2, \wedge_2, \preceq_2}$ are lattices
where 
:$\wedge_1, \vee_1$ denote  the meet and join on $L_1$
:$\wedge_2, \vee_2$ denote  the meet and join on $L_2$
By definition of lattice isomorphism:
:$\phi : L_1 \to L_2$ is an order isomorphism
From Order Isomorphism Preserves Infima and Suprema:
:$\phi : L_1 \to L_2$ is arbitrary join preserving: $\forall A \subseteq S_1: \map \phi {\sup A} = \sup \set{\map \phi x : x \in A}$
and:
:$\phi : L_1 \to L_2$ is arbitrary meet preserving: $\forall A \subseteq S_1: \map \phi {\inf A} = \inf \set{\map \phi x : x \in A}$
By definition of complete lattice homomorphism:
:$\phi : L_1 \to L_2$ is a bijective complete lattice homomorphism.
Theorem: Complete Lattice Homomorphism is Lattice Homomorphism

Let $L_1 = \struct {S_1, \preceq_1}$ and $L_2 = \struct {S_2, \preceq_2}$ be complete lattices.
Let $\phi : L_1 \to L_2$ be a complete lattice homomorphism.
Then:
:$\phi : \struct {S_1, \vee_1, \wedge_1, \preceq_1} \to \struct {S_2, \vee_2, \wedge_2, \preceq_2}$ is a lattice homomorphism
where: 
:$\wedge_1, \vee_1$ denote  the meet and join on $L_1$
:$\wedge_2, \vee_2$ denote  the meet and join on $L_2$

Proof:
From Complete Lattice is Lattice:
:$\struct {S_1, \vee_1, \wedge_1, \preceq_1}$ and $\struct {S_2, \vee_2, \wedge_2, \preceq_2}$ are lattices
where 
:$\wedge_1, \vee_1$ denote  the meet and join on $L_1$
:$\wedge_2, \vee_2$ denote  the meet and join on $L_2$
By definition of complete lattice homomorphsim:
:$\phi$ satisfies the complete lattice homomorphism axioms:
{{:Axiom:Complete Lattice Homomorphism Axioms}}
Hence $\phi$ satisfies:
:$\forall$ $a, b \in S_1 : \map \phi {a \wedge_1 b} = \map \phi a \wedge_2 \map \phi b$
:$\forall$ $a, b \in S_1 : \map \phi {a \vee_1 b} = \map \phi a \vee_2 \map \phi b$
by definition of meet and join
By definition of the morphism property:
:$\vee_1, \wedge_1$ have the morphism property under $\phi$
Hence $\phi$ is a lattice homomorphism by definition.
{{qed}}
Category:Complete Lattice Homomorphisms
Category:Lattice Homomorphisms
py5h5cx81uqe60auxuich7l1eb73726
Theorem: Inverse of Complete Lattice Isomorphism is Complete Lattice Isomorphism

Let $L_1 = \struct {A_1, \preceq_1}$ and $L_2 = \struct {A_2, \preceq_2}$ be complete lattices.
Let $\phi: L_1 \to L_2$ be a complete lattice isomorphism.
Let $\phi^{-1} : A_2 \to A_1$ be the inverse of $\phi : A_1 \to A_2$.
Then:
:$\phi^{-1} : L_2 \to L_1$ is a complete lattice isomorphism

Proof:
By definition, a complete lattice isomorphism is a bijective complete lattice homomorphism.
The result follows from Inverse of Bijective Complete Lattice Homomorphism is Bijective Complete Lattice Homomorphism.
{{qed}}
Category:Complete Lattice Isomorphisms
g7m0iqfr6hqlityb0mxbmlnlreyi5sg
Theorem: Category of Complete Lattices is Category

Let $\mathbf {CLat}$ denote the category of complete lattices.
Then:
:$\mathbf {CLat}$ is a metacategory

Proof:
Let us verify the axioms $(\text C 1)$ up to $(\text C 3)$ for a metacategory.
For any two complete lattice homomorphisms their composition (in the usual set theoretic sense) is again a complete lattice homomorphism by Composite Complete Lattice Homomorphisms is Complete Lattice Homomorphism.
For any complete lattice $\struct{L, \preceq}$, we have the identity mapping $\operatorname{id}_L$.
From Identity Mapping is Complete Lattice Homomorphism we have $\operatorname{id}_L$ is a lattice homomorphism.
By Identity Mapping is Left Identity and Identity Mapping is Right Identity, this is the identity morphism for $\struct{L, \preceq}$.
Finally by Composition of Mappings is Associative, the associative property is satisfied.
Hence $\mathbf{CLat}$ is a metacategory.
{{qed}}
Category:Category of Complete Lattices
exln31ln18trr6z91msxaaesrz51o29
Theorem: Complete Lattice Isomorphism is Isomorphism in Category CLat

Let $\mathbf{CLat}$ denote the category of complete  lattices.
Let $\phi : L_1 \to L_2$ be a morphism of $\mathbf{CLat}$.
Then:
:$\phi$ is an isomorphism of $\mathbf{CLat}$ {{iff}} $\phi$ is a complete lattice isomorphsm

Proof:
Let $L_1$ and $L_2$ be the complete lattices $L_1 = \struct{A_1, \preceq_1}$ and $L_2 = \struct{A_2, \preceq_2}$ respectively.
By definition of category of complete lattices:
:$\phi$ is a complete lattice homomorphisms
By definition of an isomorphism:
:$\phi$ is an isomorphism of $\mathbf{CLat}$
{{iff}}:
:$(1):$ there exists a morphism of $\psi : L_2 \to L_1$ of $\mathbf{CLat}$ such that:
::$\psi \circ \phi = \operatorname{id}_{L_1}$ and $\phi \circ \psi = \operatorname{id}_{L_2}$
:where $\operatorname{id}_{L_1}$ and $\operatorname{id}_{L_2}$ are identity morphisms.
By definition of category of complete lattices:
:$\phi$ satisfies $(1)$
{{iff}}:
:$(2):$ there exists a complete lattice homomorphism $\psi : L_2 \to L_1$ such that:
::the standard compositions of mappings $\psi \circ \phi = \operatorname{id}_{A_1}$ and $\phi \circ \psi = \operatorname{id}_{A_2}$
:where $\operatorname{id}_{A_1}$ and $\operatorname{id}_{A_2}$ are identity mappings.
Theorem: Transition Mapping between Charts is Homeomorphism

Let $M$ be a topological space.
Let $d$ be a natural number.
Let $\struct {U, \phi}$ and $\struct {V, \psi}$ be $d$-dimensional charts of $M$
such that $U \cap V \ne \O$.
Then, the  transition map from $\phi$ to $\psi$:
:$\psi \circ \phi^{-1} : \map \phi {U \cap V} \to \map \psi {U \cap V}$
is an homeomorphism.

Proof:
By definition of charts, $U$ and $V$ are homeomorphisms.
By Inverse of Homeomorphism is Homeomorphism, $\phi^{-1}$ is an homeomorphism.
By Composite of Homeomorphisms is Homeomorphism, $\psi \circ \phi^{-1}$ is an homeomorphism.
{{qed}}
Category:Homeomorphisms (Topological Spaces)
p8fndu1hk29p5ei5ro2n490ornmjegf
Theorem: Algebraic Numbers form Countable Subfield of Complex Numbers

The set $\Bbb A$ of algebraic numbers forms a countable subfield of the field of complex numbers.

Proof:
By definition, $\Bbb A$ is the subset of the complex numbers which consists of roots of polynomials with coefficients in $\Q$.
From Algebraic Numbers form Field, $\Bbb A$ is a field.
The result follows by definition of subfield.
{{qed}}
Theorem: Complete Lattice is Lattice

Let $L= \struct{S, \preceq}$ be a complete lattice.
Then:
:$\struct {S, \vee, \wedge, \preceq}$ is a lattice
where $\vee$ and $\wedge$ denote the join and meet operations on $S$, respectively.

Proof:
By definition of complete lattice:
:$\forall T \subseteq S: T$ admits both a supremum and an infimum in $L$
Hence:
:$\forall x, y \in S$, the join and meet of $x$ and $y$ exist in $L$
Denote with $\vee$ and $\wedge$ the join and meet operations on $S$, respectively.
It follows that $\struct {S, \vee, \wedge, \preceq}$ is a lattice by definition.
{{qed}}
Category:Complete Lattices
Category:Lattices (Order Theory)
8otc47izwbr02zbat2102hbz9vflmjv
Theorem: Complete Lattice Homomorphism is Frame Homomorphism

Let $L_1 = \struct {S_1, \preceq_1}$ and $L_2 = \struct {S_2, \preceq_2}$ be complete lattices.
Let $\phi: L_1 \to L_2$ be a complete lattice homomorphsim between $L_1$ and $L_2$.
Then:
:$\phi$ is a frame homomorphism

Proof:
By definition of complete lattice homomorphsim:
:$\phi$ satisfies the complete lattice homomorphism axioms:
{{:Axiom:Complete Lattice Homomorphism Axioms}}
It follows that $\phi$ is finite meet preserving:
:$\forall$ finite $A \subseteq S_1 : \map \phi {\inf A} = \inf \set{\map \phi a : a \in A}$
Hence $\phi$ is finite meet preserving and arbitrary join preserving by definition.
Hence $\phi$ is a frame homomorphism by definition.
{{qed}}
Category:Complete Lattice Homomorphisms
Category:Frame Homomorphisms
1arohk1a3hcd7f02otikmngxh341u8f
Theorem: Algorithmic Complexity of Euclidean Algorithm

Let $a, b \in \Z_{>0}$ be (strictly) positive integers.
Let the Euclidean Algorithm be employed to find the GCD of $a$ and $b$.
Let $\CC$ be the algorithmic complexity of this operation.
Then:
:$\CC = \map \OO {\map \ln {\max \set {a, b} } }$
where $\OO$ denotes big-$\OO$ notation.

Proof:
Lamé's Theorem states that:
{{:Lamé's Theorem}}
It follows that:
{{begin-eqn}}
{{eqn | l = \CC
      | r = \map \OO {\map \log { \min \set {a, b} } }
}}
{{eqn | r = \map \OO {\map \log { \max \set {a, b} } }
      | c = $\min \set {a, b} \leq \max \set {a, b}$
}}
{{eqn | r = \map \OO {\log e \map \ln { \max \set {a, b} } }
      | c = Change of Base of Logarithm
}}
{{eqn | r = \map \OO {\map \ln { \max \set {a, b} } }
      | c = $\log e$ is a Constant
}}
{{end-eqn}}
{{qed}}
Theorem: Analytic Real Function has Derivatives of All Orders

Let $f$ be a real function which is analytic real function on the open interval $\openint a b$.
Then $f$ has continuous derivatives of all orders.

Proof:
{{Recall|Analytic Real Function}}
{{:Definition:Analytic Real Function}}
Hence, in order for $f$ to be analytic, $f$ is {{afortiori}} smooth.
Hence, by definition of smooth, $f$ has continuous derivatives of all orders.
{{qed}}
Theorem: Smooth Real Function is not necessarily Analytic

Let $f$ be a real function which is smooth on the open interval $\openint a b$.
real function which is analytic real function on the open interval $\openint a b$.
Then it is not necessarily the case that $f$ is also analytic on $\openint a b$.

Proof:
;Proof by Counterexample
Consider the real function $f: \R \to \R$ defined as:
:$\forall x \in \R: \map f x = \begin {cases} \map \exp {\dfrac {-1} {x^2} } & : x \ne 0 \\ 0 & : x = 0 \end {cases}$
$f$ is of differentiability class $C^\infty$ such that the derivatives of all orders equal $0$.
Thus the Taylor series of $f$ at $x = 0$ converges to $f$ at $0$ only.
Hence by definition $f$ is not an analytic real function.
{{qed}}
Theorem: Conditionally Convergent Series has Infinitely Many Positive and Negative Terms

Let $S = \sequence {s_n}$ be a real infinite series which is conditionally convergent.
Then it has infinitely many strictly positive and negative terms.

Proof:
{{WLOG}}, we show there are infinitely many negative terms.
{{AimForCont}} there are finitely many negative terms.
Let $N = \sequence {n_k}$ be the sequence defined as:
:$n_k = \sequence {\size {s_k} }$
where $\size {s_k}$ denotes the absolute value of $s_k$.
By Convergent Sequence with Finite Number of Terms Deleted is Convergent, we can remove the negative terms from $S$ while still having a convergent series.
By Convergent Sequence with Finite Number of Terms Inserted is Convergent, we can add the absolute values of those negative terms back into what remains of $S$, still preserving convergence.
<!-- Proof of redlink: This is true for finite sequences. For infinite sequences, split the infinite sequence into a finite sequence and an infinite sequence. Insert into the finite sequence. (The construction "let k be the last index to insert at" may be useful). This would also make Convergent Sequence with Finite Elements Prepended is Convergent Sequence and Convergent Sequence with Finite Number of Terms Deleted is Convergent (insert the negatives) trivial -->
So $N$ is convergent.
By definition of absolutely convergent series, $S$ is absolutely convergent.
By definition of conditionally convergent series, $S$ is not absolutely convergent.
Hence by Proof by Contradiction it follows that there are infinitely many negative terms.
{{Qed}}
Category:Convergent Series
10ps1puer9mjktdc8qepx4gs93w9h8f
Theorem: Sum of Logarithms/Complex Logarithm

Let $x, y \in \C$ where $x = r_1 e^{i \theta_1}$ and $y = r_2 e^{i \theta_2}$
Where:
:$r_1$ and $r_2$ are both (strictly) positive real numbers.
Then:
:$\ln x + \ln y = \map \ln {x y}$
where $\ln$ denotes the complex natural logarithm.

Proof:
We have:
{{begin-eqn}}
{{eqn | l = x
      | r = r_1 e^{i \theta_1}
      | c = 
}}
{{eqn | ll = \leadsto
      | l = \ln x
      | r = \map \ln {r_1} + i \paren {\theta_1 + 2 k \pi}
      | c = {{Defof|Complex Natural Logarithm}}
}}
{{end-eqn}}
and:
{{begin-eqn}}
{{eqn | l = y
      | r = r_2 e^{i \theta_2}
      | c = 
}}
{{eqn | ll = \leadsto
      | l = \ln y
      | r = \map \ln {r_2} + i \paren {\theta_2 + 2 k \pi}
      | c = {{Defof|Complex Natural Logarithm}}
}}
{{end-eqn}}
Finally, we have:
{{begin-eqn}}
{{eqn | l = x y
      | r = \paren {r_1 e^{i \theta_1} } \paren {r_2 e^{i \theta_2} }
      | c = 
}}
{{eqn | ll = \leadsto
      | l = x y
      | r = \paren {r_1 r_2 e^{i \paren {\theta_1 + \theta_2} } } 
      | c = Product of Powers
}}
{{eqn | ll = \leadsto
      | l = \map \ln {x y}
      | r = \map \ln {r_1 r_2} + i \paren {\theta_1 + \theta_2 + 2 k \pi}
      | c = {{Defof|Complex Natural Logarithm}}
}}
{{end-eqn}}
Therefore:
{{begin-eqn}}
{{eqn | l = \ln x + \ln y
      | r = \map \ln {r_1} + i \paren {\theta_1 + 2 k \pi} + \map \ln {r_2} + i \paren {\theta_2 + 2 k \pi}
      | c = 
}}
{{eqn | r = \map \ln {r_1 r_2} + i \paren {\theta_1 + \theta_2 + 2 k \pi}
      | c = Sum of Logarithms/Natural Logarithm
}}
{{eqn | r = \map \ln {x y}
      | c = 
}}
{{end-eqn}}
{{qed}}
Category:Sum of Logarithms
hirqum45euwih8sxv9p9ohe1lien5kj
Theorem: Hall's Theorem (Group Theory)

Let $G$ be a solvable group of order $ab$ such that $a$ and $b$ are coprime.
Then:
: $G$ contains a subgroup of order $a$,
and
: subgroups of order $a$ are mutually conjugate.

Proof:
{{ProofWanted}}
{{Namedfor|Philip Hall|cat = Hall}}
Theorem: Antilogarithm Function is Exponential Function

Let $y = \operatorname {alog}_b x$ be the antilogarithm of $x$ base $b$.
Then:
:$y = b^x$

Proof:
{{begin-eqn}}
{{eqn | l = y
      | r = \operatorname {alog}_b x
      | c = {{hypothesis}}
}}
{{eqn | ll= \leadsto
      | l = x
      | r = \log_b y
      | c = {{Defof|Antilogarithm}}
}}
{{eqn | ll= \leadsto
      | l = b^x
      | r = y
      | c = {{Defof|General Logarithm}}
}}
{{end-eqn}}
{{qed}}
Theorem: Composite Complete Lattice Homomorphisms is Complete Lattice Homomorphism

Let $L_1 = \struct{A_1, \preceq_1}$, $L_2 = \struct{A_2, \preceq_2}$ and $L_3 = \struct{A_3, \preceq_3}$ be complete lattices.
Let $\phi_1: L_1 \to L_2$ and $\phi_2: L_2 \to L_3$ be complete lattice homomorphisms.
Let $\phi_2 \circ \phi_1 : A_1 \to A_3$ be the composite mapping of $\phi_1$ and $\phi_2$  
Then:
:$\phi_2 \circ \phi_1$ is a complete lattice homomorphism of $L_1$ to $L_3$

Proof:
=== $\phi_2 \circ \phi_1$ is arbitrary join preserving ===
We have:
{{begin-eqn}}
{{eqn | q = \forall A \subseteq A_1
      | l = \map {\phi_2 \circ \phi_1} {\sup A}
      | r = \map {\phi_2} {\map {\phi_1} {\sup A} }
      | c = {{Defof|Composite Mapping}}
}}
{{eqn | r = \map {\phi_2} {\sup \paren{\phi_1 \sqbrk A} }
      | c = {{Defof|Complete Lattice Homomorphism}}
}}
{{eqn | r = \sup \paren{\phi_2 \sqbrk {\phi_1 \sqbrk A} } 
      | c = {{Defof|Complete Lattice Homomorphism}}
}}
{{eqn | r = \sup \paren{\phi_2 \circ \phi_1 \sqbrk A} 
      | c = Image of Subset under Composite Relation with Common Codomain and Domain
}}
{{end-eqn}}
It follows that $\phi_2 \circ \phi_1$ is arbitrary join preserving.
{{qed|lemma}}