avewright/proofwiki-math huggingface dataset:
Theorem: Subset of Sigma-Locally Finite Set of Subsets is Sigma-Locally Finite

Let $T = \struct{S, \tau}$ be a topological space.
Let $\FF \subseteq \powerset S$ be a set of subsets of $S$.
Let $\GG \subseteq \FF$.
If $\FF$ is $\sigma$-locally finite then $\GG$ is $\sigma$-locally finite.

Proof:
By definition of $\sigma$-locally finite:
:$\FF = \ds \bigcup_{n \in \N} \FF_n$
where $\FF_n$ is locally finite for each $n \in \N$.
For each $n \in \N$, let:
:$\GG_n = \GG \cap \FF_n$
We have:
{{begin-eqn}}
{{eqn | l = \GG
      | r = \GG \cap \FF
      | c = Intersection with Subset is Subset
}}
{{eqn | r = \GG \cap \paren{\bigcup_{n \in \N} \FF_n}
      | c = Definition of $\FF$
}}
{{eqn | r = \bigcup_{n \in \N} \GG \cap \FF_n
      | c = Intersection Distributes over Union
}}
{{eqn | r = \bigcup_{n \in \N} \GG_n
      | c = Definition of $\GG_n$
}}
{{end-eqn}}
From Intersection is Subset:
:$\GG_n \subseteq \FF_n$
From Subset of Locally Finite Set of Subsets is Locally Finite:
:$\GG_n$ is locally finite for each $n \in \N$
By definition, $\GG$ is $\sigma$-locally finite.
{{qed}}
Category:Sigma-Locally Finite Sets of Subsets
ffp1vwf7u7naxgh4q62m5il9g5vh4m5
Theorem: Real Function is Expressible as Sum of Even Function and Odd Function

Let $f: \R \to \R$ be a real function which is neither an even function nor an odd function.
Then $f$ may be expressed as the pointwise sum of an even function and an odd function.

Proof:
Let:
{{begin-eqn}}
{{eqn | l = \map g x
      | r = \dfrac {\map f x + \map f {-x} } 2
}}
{{eqn | l = \map h x
      | r = \dfrac {\map f x - \map f {-x} } 2
}}
{{end-eqn}}
We note that:
{{begin-eqn}}
{{eqn | l = \map g {-x}
      | r = \dfrac {\map f {-x} + \map f {-\paren {-x} } } 2
      | c = 
}}
{{eqn | r = \dfrac {\map f {-x} + \map f x} 2
      | c = 
}}
{{eqn | r = \map g x
      | c = 
}}
{{end-eqn}}
Thus $g$ is an even function.
Then:
{{begin-eqn}}
{{eqn | l = \map h {-x}
      | r = \dfrac {\map f {-x} - \map f {-\paren {-x} } } 2
      | c = 
}}
{{eqn | r = \dfrac {\map f {-x} - \map f x} 2
      | c = 
}}
{{eqn | r = -\dfrac {\map f x - \map f {-x} } 2
      | c = 
}}
{{eqn | r = -\map h x
      | c = 
}}
{{end-eqn}}
Thus $h$ is an odd function.
Then:
{{begin-eqn}}
{{eqn | l = \map g x + \map h x
      | r = \dfrac {\map f x + \map f {-x} } 2 + \dfrac {\map f x - \map f {-x} } 2
      | c = 
}}
{{eqn | r = \dfrac {\map f x } 2 + \dfrac {\map f {-x} } 2 + \dfrac {\map f x } 2 - \dfrac {\map f {-x} } 2
      | c = 
}}
{{eqn | r = \map f x
      | c = 
}}
{{end-eqn}}
Hence the result.
{{qed}}
Theorem: Characteristics of Vector in Plane

Let a Cartesian plane $\CC$ be established with origin $O$.
Let $\tuple {A_x, A_y}$ be an ordered pair of real numbers that can be used to represent a point in $\CC$.
Then:
:$\tuple {A_x, A_y}$ are the Cartesian coordinates of the terminal point of a position vector $\mathbf A$
{{iff}}:
:$\tuple {A_x, A_y}$ can be transformed into $\tuple { {A'}_x, {A'}_y}$ by rotating $\CC$ about $O$ through an angle $\varphi$ using:
{{begin-eqn}}
{{eqn | l = {A'}_x
      | r = A_x \cos \varphi + A_y \sin \varphi
      | c = 
}}
{{eqn | l = {A'}_y
      | r = -A_x \sin \varphi + A_y \cos \varphi
      | c = 
}}
{{end-eqn}}

Proof:
=== Sufficient Condition ===
Let $\tuple {A_x, A_y}$ represent the terminal point of a position vector $\mathbf A$.
Then from Rotation of Cartesian Axes around Vector:
{{begin-eqn}}
{{eqn | l = {A'}_x
      | r = A_x \cos \varphi + A_y \sin \varphi
      | c = 
}}
{{eqn | l = {A'}_y
      | r = -A_x \sin \varphi + A_y \cos \varphi
      | c = 
}}
{{end-eqn}}
{{qed|lemma}}
Theorem: Regular Space with Sigma-Locally Finite Basis is Normal

Let $T = \struct {S, \tau}$ be a regular space.
Let there exist a $\sigma$-locally finite basis for $T$.
Then:
:$T$ is a normal space

Proof:
{{Recall|Normal Space|normal space|index = 1}}
{{:Definition:Normal Space/Definition 1}}
{{Recall|Regular Space|regular space}}
{{:Definition:Regular Space/Definition 2}}
From $T_3$ Space with Sigma-Locally Finite Basis is $T_4$ Space:
:$T$ is a $T_4$ space
Hence $T$ is a normal space by definition.
{{qed}}
Category:Regular Spaces
Category:Sigma-Locally Finite Bases
Category:Normal Spaces
npkvm20t6qes45ck3259ho297n349kd
Theorem: Zero Vector is Orthogonal to All Vectors

Let $\mathbf V$ be a vector space of $n$ dimensions.
Let $\bszero \in \mathbf V$ be the zero vector.
Let $\mathbf a \in \mathbf V$ be an arbitrary vector in $\mathbf V$
Then $\bszero$ is orthogonal to $\mathbf a$.

Proof:
By definition, $\mathbf a$ and $\mathbf b$ are orthogonal {{iff}} their dot product is zero:
:$\mathbf a \cdot \mathbf b = 0$
We have:
{{begin-eqn}}
{{eqn | l = \mathbf a
      | r = \sum_{k \mathop = 1}^n a_k \mathbf e_k
}}
{{eqn | l = \mathbf b
      | r = \sum_{k \mathop = 1}^n b_k \mathbf e_k
}}
{{end-eqn}}
where $\tuple {\mathbf e_1, \mathbf e_2, \ldots, \mathbf e_n}$ is the standard ordered basis of $\mathbf V$.
By definition of dot product:
:$\ds \mathbf a \cdot \mathbf b = \sum_{k \mathop = 1}^n a_k b_k$
By definition of zero vector:
{{begin-eqn}}
{{eqn | l = \bszero
      | r = \sum_{k \mathop = 1}^n 0 \mathbf e_k
}}
{{end-eqn}}
Hence:
{{begin-eqn}}
{{eqn | l = \bszero \cdot \mathbf a
      | r = \sum_{k \mathop = 1}^n 0 \times a_k
      | c = 
}}
{{eqn | r = 0
      | c = 
}}
{{end-eqn}}
Hence the result.
{{qed}}
Theorem: Standard Ordered Basis Vectors are Orthogonal

Let $\struct {\mathbf V, +, \circ}_{\mathbb F}$ be a vector space over a field $\mathbb F$, as defined by the vector space axioms.
Let $\tuple {\mathbf e_1, \mathbf e_2, \ldots, \mathbf e_n}$ be the standard ordered basis of $\mathbf V$.
Let $\mathbf e_i$ and $\mathbf e_j$ be elements of $\tuple {\mathbf e_1, \mathbf e_2, \ldots, \mathbf e_n}$ such that $i \ne j$.
:$\mathbf e_i$ and $\mathbf e_j$ are orthogonal.

Proof:
By definition of standard ordered basis:
:$\mathbf e_i$ is a vector whose $i$th component is $1_{\mathbb F}$ with all other components $0_{\mathbb F}$.
Hence:
:$\mathbf e_i \cdot \mathbf e_j = \delta_{i j}$
where $\delta_{i j}$ denotes the Kronecker delta.
That is:
:$i \ne j \implies \mathbf e_i \cdot \mathbf e_j = 0$
Hence the result by definition of orthogonal.
{{qed}}
Theorem: Open Cover with Closed Locally Finite Refinement is Even Cover

Let $T = \struct {X, \tau}$ be a topological Space.
Let $\UU$ be an open cover of $T$ with a closed locally finite refinement.
Then:
:$\UU$ is an even cover.

Proof:
Let $\AA$ be a closed locally finite refinement of $\UU$.
By definition of refinement:
:$\forall A \in \AA : \exists U \in \UU : A \subseteq U$
For each $A \in \AA$, let $U_A \in \UU$ such that $A \subseteq U_A$.
Let $T \times T = \struct {X \times X, \tau_{X \times X} }$  denote the product space of $T$ with itself.
For each $A \in \AA$, let:
:$V_A = \paren {U_A \times U_A} \cup \paren {\paren {X \setminus A} \times \paren {X \setminus A} }$
Let:
:$V = \ds \bigcap_{A \mathop \in \AA} V_A$
For each $x \in X$, let:
:$\map V x = \set {y \in X : \tuple {x, y} \in V}$
where:
:$V$ is seen as a relation on $X \times X$
:$\map V x$ denotes the image of $x$ under $V$.
Theorem: Equivalence of Definitions of Orthogonal Matrix

{{TFAE|def = Orthogonal Matrix}}
Let $\mathbf Q$ be a nonsingular square matrix over a field $\GF$.

Proof:
=== Definition $(1)$ is equivalent to Definition $(2)$ ===
{{begin-eqn}}
{{eqn | l = \mathbf Q^{-1}
      | r = \mathbf Q^\intercal
      | c = {{Defof|Orthogonal Matrix|index = 1}}
}}
{{eqn | ll= \leadstoandfrom
      | l = \mathbf Q^{-1} \mathbf Q
      | r = \mathbf Q^\intercal \mathbf Q
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | l = \mathbf I
      | r = \mathbf Q^\intercal \mathbf Q
      | c = {{Defof|Orthogonal Matrix|index = 2}}
}}
{{end-eqn}}
{{qed|lemma}}
Theorem: Set is Neighborhood of Subset iff Neighborhood of all Points of Subset

Let $T = \struct {S, \tau}$ be a topological space.
Let $N \subseteq S$ be a subset of $T$.
Let $A \subseteq N$ be a subset of $T$.
Then:
:$N$ is a neighborhood of $A$ in $T$
{{iff}}:
:$N$ is a neighborhood of all points in $A$

Proof:
=== Necessary Condition ===
Let $N$ be a neighborhood of $A$ in $T$.
By definition of neighborhood of set:
:$\exists U \in \tau : A \subseteq U \subseteq N$
Let $z \in A$.
By definition of subset:
:$z \in U$
From Set is Open iff Neighborhood of all its Points:
:$U$ is a neighborhood of $z$
From Superset of Neighborhood in Topological Space is Neighborhood:
:$N$ is a neighborhood of $z$
Since $z$ was arbitrary:
:$N$ is a neighborhood of all points in $A$
{{qed|lemma}}
Theorem: Open Cover with Closed Locally Finite Refinement is Even Cover/Lemma 4

:$\forall A \in \AA : V_A$ is an open neighborhood of the diagonal $\Delta_X$ in $T \times T$

Proof:
Let $A \in \AA$.
By definition of closed set:
:$X \setminus A$ is open in $T$
By definition of product topology:
:$U_A \times U_A, \paren {X \setminus A} \times \paren {X \setminus A}$ are open in $T \times T$
By {{Open-set-axiom|1}}:
:$V_A = \paren {U_A \times U_A} \cup \paren {\paren {X \setminus A} \times \paren {X \setminus A}}$ is open in $T \times T$
Let $x \in X$.
By definition of set difference:
:either $x \in A$ or $x \in X \setminus A$.
By definition of subset:
:either $x \in U_A$ or $x \in X \setminus A$.
By definition of cartesian product:
:either $\tuple {x, x} \in U_A \times U_A$ or $\tuple {x, x} \in \paren {X \setminus A} \times \paren {X \setminus A}$
By definition of set union:
:$\tuple {x, x} \in V_A$
Since $x$ was arbitrary:
:$\forall x \in X : \tuple {x, x} \in V_A$
By definition of diagonal:
:$\Delta_X \subseteq V_A$
Since $A$ was arbitrary:
:$\forall A \in \AA : V_A$ is an open neighborhood of the diagonal $\Delta_X$ in $T \times T$
{{qed}}
Category:Open Cover with Closed Locally Finite Refinement is Even Cover
48ao8m8d7flshtcedky3hacy4ljcmzg
Theorem: Open Cover with Closed Locally Finite Refinement is Even Cover/Lemma 3

:$\forall A \in \AA, x \in A : \map {V_A} x = U_A$

Proof:
We have:
{{begin-eqn}}
{{eqn | q = \forall A \in \AA, x \in A
      | l = \map {V_A} x
      | r = \set {y \in X : \tuple{x, y} \in V_A}
      | c = Definition of $\map {V_A} x$
}}
{{eqn | r = \set {y \in X : \tuple {x, y} \in \paren {U_A \times U_A} \cup \paren {\paren {X \setminus A} \times \paren {X \setminus A} } }
      | c = Definition of $V_A$
}}
{{eqn | r = \set {y \in X : \tuple {x, y} \in U_A \times U_A \text{ or } \tuple {x, y} \in \paren {X \setminus A} \times \paren {X \setminus A} }
      | c = {{Defof|Set Union}}
}}
{{eqn | r = \set {y \in X : \tuple {x, y} \in U_A \times U_A}
      | c = as $x \in A$
}}
{{eqn | r = \set {y \in X : y \in U_A}
      | c = {{Defof|Cartesian Product}}
}}
{{eqn | r = U_A
      | c = {{Defof|Set}}
}}
{{end-eqn}}
{{qed}}
Category:Open Cover with Closed Locally Finite Refinement is Even Cover
9lopsnw4wp7okw7sp88ayj24t6ux1k0
Theorem: Open Cover with Closed Locally Finite Refinement is Even Cover/Lemma 1

:$\set {\map V x : x \in X}$ is a refinement of $\UU$.

Proof:
Let $x \in X$.
By definition of refinement:
:$\AA$ is a cover of $X$
By definition of cover:
:$\exists A \in \AA : x \in A$
Theorem: Open Cover with Closed Locally Finite Refinement is Even Cover/Lemma 2

:$V$ is a neighborhood of the diagonal $\Delta_X$ in $T \times T$.

Proof:
Let $x \in X$.
By definition of locally finite:
:$\exists W \in \tau : x \in W : \set {A \in \AA : W \cap A \ne \O}$ is finite.
Let:
:$A \in \AA : W \cap A = \O$
From Subset of Set Difference iff Disjoint Set:
:$W \subseteq X \setminus A$
From Cartesian Product of Subsets:
:$W \times W \subseteq \paren {X \setminus A} \times \paren {X \setminus A} \subseteq V_A$
Since $A$ was arbitrary, we have established:
:$\forall A \in \AA : W \cap A = \O \leadsto W \times W \subseteq V_A$
From Set is Subset of Intersection of Supersets:
:$W \times W \subseteq \bigcap \set {V_A : A \in \AA : W \cap A = \O}$
From Intersection with Subset is Subset:
:$(1): \quad W \times W = \paren {W \times W} \cap \bigcap \set {V_A : A \in \AA : W \cap A = \O}$
We have:
{{begin-eqn}}
{{eqn | l = \paren {W \times W} \cap V
      | r = \paren {W \times W} \cap \bigcap \set {V_A : A \in \AA}
      | c = Definition of $V$
}}
{{eqn | r = \paren {W \times W} 
}}
{{eqn | o =
      | r = \cap \bigcap \set {V_A : A \in \AA : W \cap A = \O}
}}
{{eqn | o =
      | r = \cap \bigcap \set {V_A : A \in \AA : W \cap A \ne \O}
}}
{{eqn | r = \paren {W \times W} \cap \bigcap \set {V_A : A \in \AA : W \cap A \ne \O}
      | c = from $(1)$
}}
{{end-eqn}}
By definition of product topology:
:$W \times W$ is open in $T \times T$
Theorem: Angle between Vector Quantities in terms of Direction Cosines

Let $\mathbf a$ and $\mathbf b$ be vector quantities embedded in Cartesian $3$-space
Let $\theta$ be the angle between $\mathbf a$ and $\mathbf b$.
Then:
:$\cos \theta = \lambda_a \lambda_b + \mu_a \mu_b + \nu_a \nu_b$
where $\lambda_a$, $\mu_a$ and $\nu_a$ are the direction cosines of $\mathbf a$ with respect to the $x$-axis, $y$-axis and $z$-axis respectively, and similarly for $\mathbf b$.

Proof:
Let $\mathbf r$ be an arbitrary vector quantity embedded in a Cartesian $3$-space.
From Components of Vector in terms of Direction Cosines:
{{begin-eqn}}
{{eqn | l = x
      | r = r \lambda_r
}}
{{eqn | l = y
      | r = r \mu_r
}}
{{eqn | l = z
      | r = r \nu_r
}}
{{end-eqn}}
where:
:$x$, $y$ and $z$ denote the components of $\mathbf r$ in the $\mathbf i$, $\mathbf j$ and $\mathbf k$ directions respectively.
:$r$ denotes the magnitude of $\mathbf r$.
Hence:
{{begin-eqn}}
{{eqn | l = \mathbf a \cdot \mathbf b
      | r = a b \cos \theta
      | c = {{Defof|Dot Product|subdef = Real Euclidean Space}}
}}
{{eqn | r = \paren {a \lambda_a} \paren {b \lambda_b} + \paren {a \mu_a} \paren {b \mu_b} + \paren {a \nu_a} \paren {b \nu_b}
      | c = {{Defof|Dot Product|subdef = General Context}}
}}
{{eqn | ll= \leadsto
      | l = \cos \theta
      | r = \lambda_a \lambda_b + \mu_a \mu_b + \nu_a \nu_b
      | c = dividing by $a b$
}}
{{end-eqn}}
{{qed}}
Theorem: Hex Theorem/Corollary

Every game of Hex has exactly one winner.

Proof:
{{AimForCont}} there is a sequence of moves:
:$P_1, Q_1, P_2, Q_2, \dotsc$
such that neither player wins.
By the Pigeonhole Principle, every tile is marked after $n^2$ moves.
But, by the Hex Theorem, that board has exactly one winner.
This contradicts the assertion that neither player wins.
Thus, by Proof by Contradiction, every game of Hex has at least one winner.
{{qed|lemma}}
{{AimForCont}} there is a game of Hex in which both players win.
Let $B$ be the board at the end of the game.
Let every unmarked tile of $B$ be marked with an arbitrary player symbol, by the Principle of Finite Choice.
Then, the resulting board $B'$ has every tile marked.
But, by definition of winning, each player has a finite sequence of adjacent tiles marked with their own symbol, which spans their opposite sides.
In particular, every tile in the sequence is marked in $B$, and so is marked the same in $B'$.
Thus, both players win in $B'$.
This contradicts the Hex Theorem.
Thus, by Proof by Contradiction, every game of Hex has no more than one winner.
The result follows.
{{qed}}
Category:Hex Theorem
jnp8ufozeadot3jvf3uo7m3m15w8jcn
Theorem: Characterization of Paracompactness in T3 Space/Lemma 1

:$\VV$ is an open cover of $T$

Proof:
Let $x \in S$.
By definition of open cover:
:$\exists U \in \UU : x \in U$
From Characterization of T3 Space:
:$\exists V \in \tau : x \in V : V^- \subseteq U$
Hence:
:$V \in \VV$
Since $x$ was arbitrary, $\VV$ is an open cover by definition.
{{qed}}
Category:Characterization of Paracompactness in T3 Space
1t9o2hrsoy6m3dt6fvjpw554g6df4sv
Theorem: Characterization of Paracompactness in T3 Space/Lemma 2

:$\BB$ is a cover of $T$ consisting of closed sets

Proof:
Let $x \in X$.
By definition of refinement:
:$\AA$ is a cover of $X$
By definition of cover of set:
:$\exists A \in \AA : x \in A$
From Set is Subset of its Topological Closure:
:$A \subseteq A^-$
By definition of subset:
:$x \in A^-$
By definition of $\BB$:
:$A^- \in \BB$
Since $x$ was arbitrary, $\BB$ is a cover of $T$ by definition.
From Topological Closure is Closed, every element of $\BB$ is closed in $T$
{{qed}}
Category:Characterization of Paracompactness in T3 Space
fwmp418nqyo9r9prchajt2n69ref41g
Theorem: Characterization of Paracompactness in T3 Space/Lemma 3

:$\BB$ is a refinement of $\UU$

Proof:
==== Lemma 2 ====
{{:Characterization of Paracompactness in T3 Space/Lemma 2}}{{qed|lemma}}
Let $B \in \BB$.
By definition of $\BB$:
:$\exists A \in \AA : A^- = B$
By definition of refinement:
:$\exists V \in \VV : A \subseteq V$
From Set Closure Preserves Set Inclusion:
:$B = A^- \subseteq V^-$
By definition of $\VV$:
:$\exists U \in \UU : V^- \subseteq U$
From Subset Relation is Transitive:
:$B \subseteq U$
It follows that $\BB$ is a refinement of $\UU$ by definition.
{{qed}}
Category:Characterization of Paracompactness in T3 Space
5x53041ilo03utzl4a8c1rft076kv3p
Theorem: Cross Product of Parallel Vectors

Let $\mathbf a$ and $\mathbf b$ be vector quantities which are parallel.
Let $\mathbf a \times \mathbf b$ denote the cross product of $\mathbf a$ with $\mathbf b$.
Then:
:$\mathbf a \times \mathbf b = \mathbf 0$
where $\mathbf 0$ denotes the zero vector.

Proof:
By definition of cross product:
:$\norm {\mathbf a} \norm {\mathbf b} \sin \theta \, \mathbf {\hat n}$
where:
:$\norm {\mathbf a}$ denotes the length of $\mathbf a$
:$\theta$ denotes the angle from $\mathbf a$ to $\mathbf b$, measured in the positive direction
:$\hat {\mathbf n}$ is the unit vector perpendicular to both $\mathbf a$ and $\mathbf b$ in the direction according to the right-hand rule.
By definition of parallel, the direction of $\mathbf a$ is the same as the direction of $\mathbf b$
Hence when $\mathbf a$ and $\mathbf b$ are parallel, $\theta = 0$ by definition.
Hence from Sine of Zero is Zero, $\sin \theta = 0$.
Hence the result.
{{qed}}
Theorem: Rotating Indices Property of Vector Triple Product

Let $\mathbf a$, $\mathbf b$ and $\mathbf c$ be vectors in a Euclidean $3$-space.
Then:
:$\mathbf a \times \paren {\mathbf b \times \mathbf c} + \mathbf b \times \paren {\mathbf c \times \mathbf a} + \mathbf c \times \paren {\mathbf a \times \mathbf b} = 0$
where $\mathbf a \times \paren {\mathbf b \times \mathbf c}$ denotes the vector triple product operator.

Proof:
{{begin-eqn}}
{{eqn | o = 
      | r = \mathbf a \times \paren {\mathbf b \times \mathbf c} + \mathbf b \times \paren {\mathbf c \times \mathbf a} + \mathbf c \times \paren {\mathbf a \times \mathbf b}
      | c = 
}}
{{eqn | r = \paren {\mathbf a \cdot \mathbf c} \mathbf b - \paren {\mathbf a \cdot \mathbf b} \mathbf c + \paren {\mathbf b \cdot \mathbf a} \mathbf c - \paren {\mathbf b \cdot \mathbf c} \mathbf a + \paren {\mathbf c \cdot \mathbf b} \mathbf a - \paren {\mathbf c \cdot \mathbf a} \mathbf b
      | c = Lagrange's Formula: $\mathbf a \cdot \mathbf b$ denotes dot product
}}
{{eqn | r = \paren {\mathbf a \cdot \mathbf c} \mathbf b - \paren {\mathbf a \cdot \mathbf b} \mathbf c + \paren {\mathbf a \cdot \mathbf b} \mathbf c - \paren {\mathbf b \cdot \mathbf c} \mathbf a + \paren {\mathbf b \cdot \mathbf c} \mathbf a - \paren {\mathbf a \cdot \mathbf c} \mathbf b
      | c = Dot Product Operator is Commutative
}}
{{eqn | r = 0
      | c = gathering terms and simplifying
}}
{{end-eqn}}
{{qed}}
Theorem: Square of Vector Cross Product

Let $\mathbf a$ and $\mathbf b$ be vectors in a vector space $\mathbf V$ of $3$ dimensions.
Let $\mathbf a \times \mathbf b$ denote the vector cross product of $\mathbf a$ with $\mathbf b$.
Then:
:$\paren {\mathbf a \times \mathbf b}^2 = \mathbf a^2 \mathbf b^2 - \paren {\mathbf a \cdot \mathbf b}^2$
where:
:$\paren {\mathbf a \times \mathbf b}^2$ denotes the square of $\mathbf a \times \mathbf b$
:$\mathbf a \cdot \mathbf b$ denotes the dot product of $\mathbf a \times \mathbf b$.

Proof:
Let $\theta$ denote the angle between $\mathbf a$ and $\mathbf b$
{{begin-eqn}}
{{eqn | l = \paren {\mathbf a \times \mathbf b}^2
      | r = \paren {\mathbf a \times \mathbf b} \cdot \paren {\mathbf a \times \mathbf b}
      | c = {{Defof|Square of Vector Quantity}}
}}
{{eqn | r = \paren {\norm {\mathbf a} \norm {\mathbf b} \sin \theta \, \hat {\mathbf n} } \cdot \paren {\norm {\mathbf a} \norm {\mathbf b} \sin \theta \, \hat {\mathbf n} }
      | c = {{Defof|Vector Cross Product|index = 2}}: $\hat {\mathbf n}$ is a unit vector
}}
{{eqn | r = \paren {\norm {\mathbf a} \norm {\mathbf b} \sin \theta}^2
      | c = Dot Product of Vector with Itself
}}
{{eqn | r = \paren {\norm {\mathbf a} \norm {\mathbf b} }^2 \paren {1 - \cos^2 \theta}
      | c = Sum of Squares of Sine and Cosine
}}
{{eqn | r = \norm {\mathbf a}^2 \norm {\mathbf b}^2 - \paren {\norm {\mathbf a} \norm {\mathbf b} \cos \theta}^2
      | c = rearranging
}}
{{eqn | r = \mathbf a^2 \mathbf b^2 - \paren {\mathbf a \cdot \mathbf b}^2
      | c = {{Defof|Square of Vector Quantity}}, {{Defof|Dot Product|subdef = Real Euclidean Space}}
}}
{{end-eqn}}
Theorem: Order of Simple Group divides Factorial of Index of Subgroup

Let $G$ be a simple group, and let $H$ be a subgroup of $G$ with index $n$. Then $|G|$ divides $n!$.

Proof:
Let $G$ act on the cosets of $H$, $G/H$ by the left regular action.
By Group Action defines Permutation Representation, this defines a homomorphism $\tilde \phi: G \to \map \Gamma X$.
By Kernel is Normal Subgroup of Domain, $\ker \tilde \phi$ is a normal subgroup of $G$.
Since $G$ is simple, $\ker \tilde \phi = \{e\}$ or $G$.
If $\ker \tilde \phi = G$, then the action is trivial, but the action consists of an orbit of size $n$, so it is not trivial.
Hence $\ker \tilde \phi = \{e\}$, so $\tilde \phi$ is injective. So $G$ is isomorphic to $\tilde \phi (G)$ which is a subgroup of $\Gamma (X)$.
By Lagrange's Theorem (Group Theory), $|G|$ divides $n!$.
{{qed}}
2sducxy00uegnaxea3gc4d9hezqutbj
Theorem: Number of Sylow p-Subgroups is Index of Normalizer of Sylow p-Subgroup

Let $P$ be a Sylow p-subgroup of a group $G$, $N_G (S)$ its normalizer, and $n_p$ be the number of Sylow p-subgroups in $G$.
Then $[ G : N_G (S) ] = n_p$.

Proof:
By Number of Distinct Conjugate Subsets is Index of Normalizer, $[ G : N_G (S) ] = n_p$.
{{qed}}
dngs99iml7th8u6v95kmmnlthoaatmo
Theorem: Group of Order 36 is not Simple

Let $G$ be of order $36$.
Then $G$ is not simple.

Proof:
{{AimForCont}} $G$ is simple.
We have that:
:$36 = 2^2 \times 3^2$
Let $n_3$ denote the number of Sylow $3$-subgroups of $G$.
From the Fourth Sylow Theorem:
:$n_3 \equiv 1 \pmod 3$
and from the Fifth Sylow Theorem:
:$n_3 \divides 4$
where $\divides$ denotes divisibility.
Hence $n_3$ must be either $1$ or $4$.
Let $P$ be a Sylow $3$-subgroup of $G$. 
Let $n_3 = 4$.
By Number of Sylow p-Subgroups is Index of Normalizer of Sylow p-Subgroup, the normalizer of $P$ has index $4$.
By Order of Simple Group divides Factorial of Index of Subgroup:
:$\order G \divides 4!$
But $36$ does not divide $24$.
Hence it cannot be the case that $n_3 = 4$.
Hence $n_3 = 1$.
From Sylow $p$-Subgroup is Unique iff Normal, $P$ is normal.
This contradicts the assumption that $G$ is simple.
Hence $G$ is not simple.
{{qed}}
Category:Groups of Order 36
5hlcj01vd598mx4r5u5oc6v6v40a424
Theorem: Group of Order 48 is not Simple

Let $G$ be of order $48$.
Then $G$ is not simple.

Proof:
{{AimForCont}} $G$ is simple.
We have that:
:$48 = 2^4 \times 3$
Let $n_2$ denote the number of Sylow $2$-subgroups of $G$.
From Sylow $2$-Subgroups in Group of Order $48$, $n_2$ is either $1$ or $3$.
Let $P$ be a Sylow $2$-subgroup of $G$.
Let $n_2 = 3$.
By Number of Sylow p-Subgroups is Index of Normalizer of Sylow p-Subgroup, the normalizer of $P$ has index $3$.
By Order of Simple Group divides Factorial of Index of Subgroup:
:$\order G \divides 3!$
But $48$ does not divide $6$.
Hence it cannot be the case that $n_2 = 3$.
Hence $n_2 = 1$.
From Sylow $p$-Subgroup is Unique iff Normal, $P$ is normal.
This contradicts the assumption that $G$ is simple.
Hence $G$ is not simple.
{{qed}}
Category:Groups of Order 48
14vv2swyyrbui02fczpr201tjdvzusc
Theorem: Ordering of Natural Numbers is Provable

Let $x, y \in \N$.
Suppose $x < y$.
Let $\sqbrk a$ denote the unary representation of $a \in \N$.
Then $\sqbrk x < \sqbrk y$ is a theorem of minimal arithmetic.

Proof:
Fix $x$, and let $z > 0$ be arbitrary.
Proceed by induction on $z$.