avewright/proofwiki-math huggingface dataset:
Theorem: Integral of Power/Fermat's Proof

:$\ds \forall n \in \Q_{>0}: \int_0^b x^n \rd x = \frac {b^{n + 1} } {n + 1}$

Proof:
First let $n$ be a positive integer.
Take a real number $r \in \R$ such that $0 < r < 1$ but reasonably close to $1$.
Consider a subdivision $S$ of the closed interval $\closedint 0 b$ defined as:
:$S = \set {0, \ldots, r^2 b, r b, b}$
that is, by taking as the points of subdivision successive powers of $r$.
Now we take the upper Darboux sum $\map U S$ over $S$ (starting from the right):
{{begin-eqn}}
{{eqn | l = \map U S
      | r = b^n \paren {b - r b} + \paren {r b}^n \paren {r b - r^2 b} + \paren {r^2 b}^n \paren {r^2 b - r^3 b} + \cdots
      | c = 
}}
{{eqn | r = b^{n + 1} \paren {1 - r} + b^{n + 1} r^{n + 1} \paren {1 - r} + b^{n + 1} r^{2 n + 2} \paren {1 - r} + \cdots
      | c = 
}}
{{eqn | r = b^{n + 1} \paren {1 - r} \paren {1 + r^{n + 1} + r^{\paren {n + 1}^2} + \cdots}
      | c = 
}}
{{eqn | r = \frac {b^{n + 1} \paren {1 - r} } {1 - r^{n + 1} }
      | c = Sum of Geometric Sequence
}}
{{eqn | r = \frac {b^{n + 1} } {1 + r + r^2 + \cdots + r^n}
      | c = 
}}
{{end-eqn}}
Now we let $r \to 1$ and see that each of the terms on the bottom also approach $1$.
Thus:
:$\ds \lim_{r \mathop \to 1} S = \frac {b^{n + 1} } {n + 1}$
That is:
:$\ds \int_0^b x^n \rd x = \frac {b^{n + 1} } {n + 1}$
for every positive integer $n$.
Now assume $n = \dfrac p q$ be a strictly positive rational number.
We set $s = r^{1/q}$ and proceed:
{{begin-eqn}}
{{eqn | l = \frac {1 - r} {1 - r^{n + 1} }
      | r = \frac {1 - s^q} {1 - \paren {s^q}^{p / q + 1} }
      | c = 
}}
{{eqn | r = \frac {1 - s^q} {1 - s^{p + q} }
      | c = 
}}
{{eqn | r = \frac {\paren {1 - s^q} / \paren {1 - s} } {\paren {1 - s^{p + q} } / \paren {1 - s} }
      | c = 
}}
{{eqn | r = \frac {1 + s + s^2 + \cdots + s^{q - 1} }{1 + s + s^2 + \cdots + s^{p + q - 1} }
      | c = 
}}
{{end-eqn}}
As $r \to 1$ we have $s \to 1$ and so that last expression shows:
{{begin-eqn}}
{{eqn | l = \frac {1 - r} {1 - r^{n + 1} }
      | o = \to
      | r = \frac q {p + q}
      | c = 
}}
{{eqn | r = \frac 1 {p / q + 1}
      | c = 
}}
{{eqn | r = \frac 1 {n + 1}
      | c = 
}}
{{end-eqn}}
So the expression for the main result still holds for rational $n$.
{{qed}}
Theorem: Composition of Mapping with Inclusion is Restriction

Let $S$ and $T$ be sets.
Let $f: S \to T$ be a mapping.
Let $A \subseteq S$ be a subset of the domain of $S$.
Let $i_A: A \to S$ be the inclusion mapping from $A$ to $S$.
Then:
:$f \circ i_A = f \restriction_A$
where $f \restriction_A$ denotes the restriction of $f$ to $A$.

Proof:
=== Equality of Domains ===
{{begin-eqn}}
{{eqn | l = \Dom {f \circ i_A}
      | r = \Dom {i_A}
      | c = Domain of Composite Relation
}}
{{eqn | r = A
      | c = Definition of $i_A$
}}
{{eqn | r = \Dom {f \restriction_A}
      | c = {{Defof|Restriction of Mapping}}
}}
{{end-eqn}}
{{qed|lemma}}
Theorem: Equivalence of Subobjects is Equivalence

Let $\mathbf C$ be a metacategory.
Let $C$ be an object of $\mathbf C$.
Let $\map {\mathbf {Sub}_{\mathbf C} } C$ be the category of subobjects of $C$.
The relation $\sim$ on $\map {\mathbf {Sub}_{\mathbf C} } C$ defined by:
:$m \sim m'$ {{iff}} $m$ and $m'$ are equivalent
is an equivalence.
{{improve|That's not a relation since we can't know we're dealing with sets; cover this}}

Proof:
By Inclusion Relation on Subobjects is Preordering, $\subseteq$ is a preordering.
From Preorder Induces Equivalence, we see that $\sim$ is the equivalence induced by $\subseteq$.
In particular, $\sim$ is an equivalence.
{{qed}}
Category:Subobjects
Category:Examples of Equivalence Relations
9k9uru39wbxbdp6s08ugdiu78mwkplo
Theorem: Equivalent Subobjects have Isomorphic Domains

Let $\mathbf C$ be a metacategory.
Let $C$ be an object of $\mathbf C$.
Let $\mathbf{Sub}_{\mathbf C} \left({C}\right)$ be the category of subobjects of $C$.
Let $m, m'$ be equivalent subobjects of $C$.
Then there exists an isomorphism $f: m \to m'$.

Proof:
For brevity, let us write $\operatorname{dom} m = B$ and $\operatorname{dom} m' = B'$.
Since $m$ and $m'$ are equivalent subobjects of $C$, we have that:
:$m \subseteq m'$ and $m' \subseteq m$
where $\subseteq$ denotes the inclusion relation on subobjects.
That is, there exist morphisms $f: m \to m'$ and $f': m' \to m$ of $\mathbf{Sub}_{\mathbf C} \left({C}\right)$.
Hence, we have morphisms:
:$f \circ f': m' \to m'$
:$f' \circ f: m \to m$
By Category of Subobjects is Preorder Category, these are the unique such morphisms.
It follows that both are identity morphisms:
:$f \circ f' = \operatorname{id}_{m'}$
:$f' \circ f = \operatorname{id}_m$
That is, $f: m \to m'$ is an isomorphism.
{{qed}}
Theorem: Morphism Class Equivalence is Equivalence

Let $\mathbf C$ be a metacategory.
Let $C$ be an object of $\mathbf C$.
Let $\map {\mathbf {Sub}_{\mathbf C} } C$ be the category of subobjects of $C$.
Let $\sim$ denote morphism class equivalence on the morphisms of $\map {\mathbf {Sub}_{\mathbf C} } C$.
Then $\sim$ is an equivalence.

Proof:
Let us check the three conditions for an equivalence in turn.
Theorem: Category of Subobject Classes is Category

Let $\mathbf C$ be a metacategory.
Let $C$ be an object of $\mathbf C$.
Let $\map {\overline {\mathbf {Sub} }_{\mathbf C} } C$ be the category of subobject classes of $C$.
:$g \circ f : X \to Z$
called the composition of $f$ and $g$.
Then $\map {\overline {\mathbf {Sub} }_{\mathbf C} } C$ is a metacategory.

Proof:
Let us verify the axioms $(\text C 1)$ to $(\text C 3)$ for a metacategory.
{{finish|A feast of checking well-definedness}}
Theorem: Category of Subobject Classes is Order Category

Let $\mathbf C$ be a metacategory.
Let $C$ be an object of $\mathbf C$.
Let $\overline{\mathbf{Sub}}_{\mathbf C} \left({C}\right)$ be the category of subobject classes of $C$.
Then $\overline{\mathbf{Sub}}_{\mathbf C} \left({C}\right)$ is an order category.

Proof:
{{ProofWanted|Preliminary (rather, partial) results missing}}
Category:Categories of Subobjects
Category:Order Categories
2l7bbazegfq66yg4yxfb335atdvs5h8
Theorem: Reverse Triangle Inequality/Real and Complex Fields

Let $x$ and $y$ be elements of either the real numbers $\R$ or the complex numbers $\C$.
Then:
:$\cmod {x - y} \ge \size {\cmod x - \cmod y}$

Proof:
From the Reverse Triangle Inequality:
:$\cmod {x - y} \ge \cmod {\cmod x - \cmod y}$
By the definition of both absolute value and complex modulus:
:$\cmod {\cmod x - \cmod y} \ge 0$
As:
:$\cmod x - \cmod y = \pm \cmod {\cmod x - \cmod y}$
it follows that:
:$\cmod {\cmod x - \cmod y} \ge \cmod x - \cmod y$
Hence the result.
{{qed}}
Theorem: Reverse Triangle Inequality/Real and Complex Fields

Let $x$ and $y$ be elements of either the real numbers $\R$ or the complex numbers $\C$.
Then:
:$\cmod {x - y} \ge \size {\cmod x - \cmod y}$

Proof:
By the Triangle Inequality:
:$\cmod {x + y} - \cmod y \le \cmod x$
Let $z = x + y$.
Then $x = z - y$ and so:
:$\cmod z - \cmod y \le \cmod {z - y}$
Renaming variables as appropriate gives:
:$\cmod {x - y} \ge \cmod x - \cmod y$
{{qed}}
Theorem: Reverse Triangle Inequality/Real and Complex Fields

Let $x$ and $y$ be elements of either the real numbers $\R$ or the complex numbers $\C$.
Then:
:$\cmod {x - y} \ge \size {\cmod x - \cmod y}$

Proof:
Let $z_1$ and $z_2$ be represented by the points $A$ and $B$ respectively in the complex plane.
From Geometrical Interpretation of Complex Subtraction, we can construct the parallelogram $OACB$ where:
:$OA$ and $OB$ represent $z_1$ and $z_2$ respectively
:$BA$ represents $z_1 - z_2$.
:400px
But $OA$, $OB$ and $BA$ form the sides of a triangle.
The result then follows directly from Sum of Two Sides of Triangle Greater than Third Side.
{{qed}}
Theorem: Reverse Triangle Inequality/Real and Complex Fields

Let $x$ and $y$ be elements of either the real numbers $\R$ or the complex numbers $\C$.
Then:
:$\cmod {x - y} \ge \size {\cmod x - \cmod y}$

Proof:
Let $X$ denote either $\R$ or $\C$ as appropriate.
From Real Number Line is Metric Space and Complex Plane is Metric Space the distance function $d: X \times X \to \R$ can be defined as:
:$\map d {x, y} = \size {x - y}$
From the Reverse Triangle Inequality as applied to metric spaces:
:$(1): \quad \forall x, y, z \in X: \size {\map d {x, z} - \map d {y, z} } \le \map d {x, y}$
Let $z = 0$.
Then $(1)$ translates to:
:$\forall x, y, z \in X: \size {\size {x - 0} - \size {y - 0} } \le \size {x - y}$
Hence the result.
{{qed}}
Theorem: Reverse Triangle Inequality/Real and Complex Fields

Let $x$ and $y$ be elements of either the real numbers $\R$ or the complex numbers $\C$.
Then:
:$\cmod {x - y} \ge \size {\cmod x - \cmod y}$

Proof:
From proof $2$ of corollary $1$ to this result, which is derived independently:
:$\size {x - y} \ge \size x - \size y$
There are two cases:
$(1): \quad \size x \ge \size y$
We have :
:$\size {\size x - \size y} = \size x - \size y$
and the proof is finished.
{{qed|lemma}}
$(2): \quad \size y \ge \size x$
We have:
:$\size {y - x} \ge \size y - \size x = \size {\size y - \size x}$
But:
:$\size {y - x} = \size {x - y}$
and:
:$\size {\size y - \size x} = \size {\size x - \size y}$
From this we have:
:$-\size {\size x - \size y} \ge -\size {x - y}$
Since, by Negative of Absolute Value, we have that:
:$\size x - \size y \ge -\size {\size x - \size y}$
it follows that:
:$-\size {x - y} \le \size x - \size y \le \size {x - y}$
The result follows.
{{qed}}
Theorem: Triangle Inequality/Real Numbers

Let $x, y \in \R$ be real numbers.
Let $\size x$ denote the absolute value of $x$.
Then:
:$\size {x + y} \le \size x + \size y$

Proof:
{{begin-eqn}}
{{eqn | l = \size {x + y}^2
      | r = \paren {x + y}^2
      | c = Square of Real Number is Non-Negative
}}
{{eqn | r = x^2 + 2 x y + y^2
      | c = Square of Sum
}}
{{eqn | r = \size x^2 + 2 x y + \size y^2
      | c = Square of Real Number is Non-Negative
}}
{{eqn | o = \le
      | r = \size x^2 + 2 \size {x y} + \size y^2
      | c = Negative of Absolute Value
}}
{{eqn | r = \size x^2 + 2 \size x \cdot \size y + \size y^2
      | c = Absolute Value Function is Completely Multiplicative
}}
{{eqn | r = \paren {\size x + \size y}^2
      | c = Square of Sum
}}
{{end-eqn}}
Then by Order is Preserved on Positive Reals by Squaring:
:$\size {x + y} \le \size x + \size y$
{{qed}}
Theorem: Triangle Inequality/Real Numbers

Let $x, y \in \R$ be real numbers.
Let $\size x$ denote the absolute value of $x$.
Then:
:$\size {x + y} \le \size x + \size y$

Proof:
This can be seen to be a special case of Minkowski's Inequality for Sums, with $n = 1$.
{{qed}}
Theorem: Triangle Inequality/Real Numbers

Let $x, y \in \R$ be real numbers.
Let $\size x$ denote the absolute value of $x$.
Then:
:$\size {x + y} \le \size x + \size y$

Proof:
We have that Real Numbers form Ordered Integral Domain.
Therefore Sum of Absolute Values on Ordered Integral Domain applies directly.
{{qed}}
Theorem: Triangle Inequality/Real Numbers

Let $x, y \in \R$ be real numbers.
Let $\size x$ denote the absolute value of $x$.
Then:
:$\size {x + y} \le \size x + \size y$

Proof:
We do a case analysis.
=== $(1): \quad x \ge 0, y \ge 0$ ===
{{begin-eqn}}
{{eqn | l = x
      | o = \ge
      | r = 0
      | c = 
}}
{{eqn | l = y
      | o = \ge
      | r = 0
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \size {x + y}
      | r = x + y
      | c = 
}}
{{eqn | r = \size x + \size y
      | c = 
}}
{{end-eqn}}
{{qed|lemma}}
=== $(2): \quad x \le 0, y \le 0$ ===
{{begin-eqn}}
{{eqn | l = x
      | o = \le
      | r = 0
      | c = 
}}
{{eqn | l = y
      | o = \le
      | r = 0
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \size {x + y}
      | r = -x - y
      | c = 
}}
{{eqn | r = \size x + \size y
      | c = 
}}
{{end-eqn}}
{{qed|lemma}}
=== $(3): \quad x \ge 0, y \le 0$ ===
We have that $\size x = x$ and $\size y = -y$.
In this case we show:
:$\size {x + y} \le \max \set {\size x, \size y}$
Let $\size x \le \size y$.
Then:
{{begin-eqn}}
{{eqn | l = x
      | o = \le
      | r = -y
}}
{{eqn | ll= \leadsto
      | l = y 
      | o = \le
      | r = y + x
      | c = as $x \ge 0$
}}
{{eqn | o = \le
      | r = 0
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \size {x + y} 
      | r = -\paren {x + y}
}}
{{eqn | o = \le
      | r = -y
}}
{{eqn | r = \size y
}}
{{end-eqn}}
Let $\size x \ge \size y$.
Then:
{{begin-eqn}}
{{eqn | l = x
      | r = -y
      | o = \ge
}}
{{eqn | ll= \leadsto
      | l = x
      | o = \ge
      | r = x + y
      | c = as $y \le 0$
}}
{{eqn | o = \ge
      | r = 0
}}
{{eqn | ll= \leadsto
      | l = \size {x + y} = 
      | r = x + y
}}
{{eqn | o = \le
      | r = x
}}
{{eqn | r = \size x
}}
{{end-eqn}}
We have $\max \set {a, b} \le a + b$ for positive real numbers $a$ and $b$. 
The result follows by taking $a = \size x$ and $b = \size y$.
{{qed|lemma}}
=== $(4): \quad x \le 0, y \ge 0$ ===
Follows by symmetry from the case $(3)$.
{{qed}}
Theorem: Triangle Inequality/Real Numbers

Let $x, y \in \R$ be real numbers.
Let $\size x$ denote the absolute value of $x$.
Then:
:$\size {x + y} \le \size x + \size y$

Proof:
From Negative of Absolute Value, it is sufficient to prove that:
:$\size x + \size y \ge x + y$
and:
:$\size x + \size y \ge -\paren {x + y}$
By definition of absolute value:
:$x \le \size x$
and:
:$y \le \size y$
Then:
:$x + y \le \size x + \size y$ 
We also have that:
{{begin-eqn}}
{{eqn | l = -x
      | o = \le
      | r = \size {-x}
      | c = 
}}
{{eqn | r = \size x
      | c = Absolute Value of Negative
}}
{{eqn | l = -y
      | o = \le
      | r = \size {-y}
      | c = 
}}
{{eqn | r = \size y
      | c = Absolute Value of Negative
}}
{{eqn | ll= \leadsto
      | l = -\paren {x + y}
      | r = \paren {-x} + \paren {-y}
      | c = 
}}
{{eqn | o = \le
      | r = \size x + \size y
      | c = 
}}
{{end-eqn}}
Hence the result.
{{qed}}
Theorem: Triangle Inequality/Complex Numbers

Let $z_1, z_2 \in \C$ be complex numbers.
Let $\cmod z$ denote the modulus of $z$.
Then:
:$\cmod {z_1 + z_2} \le \cmod {z_1} + \cmod {z_2}$

Proof:
This is an instance of the General Triangle Inequality for Complex Numbers:
:$\cmod {z_1 + z_2 + \dotsb + z_n} \le \cmod {z_1} + \cmod {z_2} + \dotsb + \cmod {z_n}$
setting $n = 3$.
{{qed}}
Theorem: Triangle Inequality/Complex Numbers

Let $z_1, z_2 \in \C$ be complex numbers.
Let $\cmod z$ denote the modulus of $z$.
Then:
:$\cmod {z_1 + z_2} \le \cmod {z_1} + \cmod {z_2}$

Proof:
{{begin-eqn}}
{{eqn | l = \cmod {z_1 + z_2 + z_3}
      | r = \cmod {z_1 + \paren {z_2 + z_3} }
      | c = 
}}
{{eqn | o = \le
      | r = \cmod {z_1} + \cmod {z_2 + z_3}
      | c = Triangle Inequality for Complex Numbers
}}
{{eqn | o = \le
      | r = \cmod {z_1} + \cmod {z_2} + \cmod {z_3}
      | c = Triangle Inequality for Complex Numbers
}}
{{end-eqn}}
{{qed}}
Theorem: Triangle Inequality/Complex Numbers

Let $z_1, z_2 \in \C$ be complex numbers.
Let $\cmod z$ denote the modulus of $z$.
Then:
:$\cmod {z_1 + z_2} \le \cmod {z_1} + \cmod {z_2}$

Proof:
Let $z_1$, $z_2$ and $z_3$ be represented by the points $A$, $B$ and $C$ respectively in the complex plane.
From Geometrical Interpretation of Complex Addition, we can construct the parallelogram $OADB$ where:
:$OA$ and $OB$ represent $z_1$ and $z_2$ respectively
:$OD$ represents $z_1 + z_2$.
Also from Geometrical Interpretation of Complex Addition, we can construct the parallelogram $OCED$ where:
:$OC$ and $OD$ represent $z_3$ and $z_1 + z_2$ respectively
:$OD$ represents $z_1 + z_2 + z_3$.
:400px
As $OADB$ is a parallelogram, we have that $OB = AD$.
The lengths of $OA$, $AD$ and $OD$ are:
{{begin-eqn}}
{{eqn | l = OA
      | r = \cmod {z_1}
}}
{{eqn | l = AD
      | r = \cmod {z_2}
}}
{{eqn | l = OD
      | r = \cmod {z_1 + z_2}
}}
{{end-eqn}}
But $OA$, $OB$ and $OD$ form the sides of a triangle.
Thus from Sum of Two Sides of Triangle Greater than Third Side:
:$\cmod {z_1 + z_2} \le \cmod {z_1} + \cmod {z_2}$
Similarly, as $OCED$ is a parallelogram, we have that $OD = CE$.
The lengths of $OC$, $CE$ and $OE$ are:
{{begin-eqn}}
{{eqn | l = OC
      | r = \cmod {z_3}
}}
{{eqn | l = CE
      | r = \cmod {z_2 + z_2}
}}
{{eqn | l = OE
      | r = \cmod {z_1 + z_2 + z_3}
}}
{{end-eqn}}
But $OC$, $CE$ and $OE$ form the sides of a triangle.
Thus from Sum of Two Sides of Triangle Greater than Third Side:
:$\cmod {z_1 + z_2 + z_3} \le \cmod {z_1 + z_2} + \cmod {z_3}$
The result follows.
{{qed}}
Theorem: Triangle Inequality/Complex Numbers

Let $z_1, z_2 \in \C$ be complex numbers.
Let $\cmod z$ denote the modulus of $z$.
Then:
:$\cmod {z_1 + z_2} \le \cmod {z_1} + \cmod {z_2}$

Proof:
Let $z_1 = a_1 + i a_2, z_2 = b_1 + i b_2$.
Then from the definition of the modulus, the above equation translates into:
:$\paren {\paren {a_1 + b_1}^2 + \paren {a_2 + b_2}^2}^{\frac 1 2} \le \paren { {a_1}^2 + {a_2}^2}^{\frac 1 2} + \paren { {b_1}^2 + {b_2}^2}^{\frac 1 2}$
This is a special case of Minkowski's Inequality for Sums, with $n = 2$.
{{qed}}
Theorem: Triangle Inequality/Complex Numbers

Let $z_1, z_2 \in \C$ be complex numbers.
Let $\cmod z$ denote the modulus of $z$.
Then:
:$\cmod {z_1 + z_2} \le \cmod {z_1} + \cmod {z_2}$

Proof:
Let $z_1 = a_1 + i a_2, z_2 = b_1 + i b_2$.
{{begin-eqn}}
{{eqn | l = \cmod {z_1 + z_2}
      | o = \le
      | r = \cmod {z_1} + \cmod {z_2}
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | l = \paren {\paren {a_1 + b_1}^2 + \paren {a_2 + b_2}^2}^{\frac 1 2}
      | o = \le
      | r = \paren { {a_1}^2 + {a_2}^2}^{\frac 1 2} + \paren { {b_1}^2 + {b_2}^2}^{\frac 1 2}
      | c = {{Defof|Complex Modulus}}
}}
{{eqn | ll= \leadstoandfrom
      | l = \paren {a_1 + b_1}^2 + \paren {a_2 + b_2}^2
      | o = \le
      | r = {a_1}^2 + {a_2}^2 + {b_1}^2 + {b_2}^2 + 2 \paren { {a_1}^2 + {a_2}^2}^{\frac 1 2} \paren { {b_1}^2 + {b_2}^2}^{\frac 1 2}
      | c = squaring both sides
}}
{{eqn | ll= \leadstoandfrom
      | l = {a_1}^2 + 2 a_1 b_1 + {b_1}^2 + {a_2}^2 + 2 a_2 b_2 + {b_2}^2 
      | o = \le
      | r = {a_1}^2 + {a_2}^2 + {b_1}^2 + {b_2}^2 + 2 \paren { {a_1}^2 + {a_2}^2}^{\frac 1 2} \paren { {b_1}^2 + {b_2}^2}^{\frac 1 2}
      | c = multiplying out
}}
{{eqn | ll= \leadstoandfrom
      | l = a_1 b_1 + a_2 b_2 
      | o = \le
      | r = \paren { {a_1}^2 + {a_2}^2}^{\frac 1 2} \paren { {b_1}^2 + {b_2}^2}^{\frac 1 2}
      | c = simplifying
}}
{{eqn | ll= \leadstoandfrom
      | l = \paren {a_1 b_1 + a_2 b_2}^2
      | o = \le
      | r = \paren { {a_1}^2 + {a_2}^2} \paren { {b_1}^2 + {b_2}^2}
      | c = Cauchy's Inequality
}}
{{eqn | ll= \leadstoandfrom
      | l = {a_1}^2 {b_1}^2 + 2 a_1 b_1 a_2 b_2 + {a_2}^2 {b_2}^2
      | o = \le
      | r = {a_1}^2 {b_1}^2 + {a_2}^2 {b_2}^2 + {a_1}^2 {b_2}^2 + {a_2}^2 {b_1}^2
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | l = 2 a_1 b_1 a_2 b_2
      | o = \le
      | r = {a_1}^2 {b_2}^2 + {a_2}^2 {b_1}^2
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | l = 0
      | o = \le
      | r = \paren {a_1 b_2}^2 - 2 \paren {a_1 b_2} \paren {a_2 b_1} + \paren {a_2 b_1}^2
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | l = 0
      | o = \le
      | r = \paren {a_1 b_2 - a_2 b_1}^2
      | c = 
}}
{{end-eqn}}
The final statement is a tautology, and all implications are reversible.
Hence the result.
{{qed}}
Theorem: Triangle Inequality/Complex Numbers

Let $z_1, z_2 \in \C$ be complex numbers.
Let $\cmod z$ denote the modulus of $z$.
Then:
:$\cmod {z_1 + z_2} \le \cmod {z_1} + \cmod {z_2}$

Proof:
Let $z_1$ and $z_2$ be represented by the points $A$ and $B$ respectively in the complex plane.
From Geometrical Interpretation of Complex Addition, we can construct the parallelogram $OACB$ where:
:$OA$ and $OB$ represent $z_1$ and $z_2$ respectively
:$OC$ represents $z_1 + z_2$.
:400px
As $OACB$ is a parallelogram, we have that $OB = AC$.
The lengths of $OA$, $AC$ and $OC$ are:
{{begin-eqn}}
{{eqn | l = OA
      | r = \cmod {z_1}
}}
{{eqn | l = AC
      | r = \cmod {z_2}
}}
{{eqn | l = OC
      | r = \cmod {z_1 + z_2}
}}
{{end-eqn}}
But $OA$, $OB$ and $OC$ form the sides of a triangle.
The result then follows directly from Sum of Two Sides of Triangle Greater than Third Side.
{{qed}}
Theorem: Triangle Inequality/Complex Numbers

Let $z_1, z_2 \in \C$ be complex numbers.
Let $\cmod z$ denote the modulus of $z$.
Then:
:$\cmod {z_1 + z_2} \le \cmod {z_1} + \cmod {z_2}$

Proof:
{{begin-eqn}}
{{eqn | l = \cmod {z + w}^2
      | r = \paren {z + w} \paren {\overline z + \overline w}
      | c = Product of Complex Number with Conjugate
}}
{{eqn | r = z \overline z + w \overline w + w \overline z + z \overline w
      | c = 
}}
{{eqn | r = \cmod z^2 + \cmod w^2 + w \overline z + z \overline w
      | c = Product of Complex Number with Conjugate
}}
{{eqn | r = \cmod z^2 + \cmod w^2 + w \overline z + \overline {\paren {\overline z} } \overline w
      | c = Complex Conjugation is Involution
}}
{{eqn | r = \cmod z^2 + \cmod w^2 + \overline z w + \overline {\paren {\overline z w} }
      | c = Product of Complex Conjugates and Complex Multiplication is Commutative
}}
{{eqn | r = \cmod z^2 + \cmod w^2 + 2 \map \Re {z \overline w}
      | c = Sum of Complex Number with Conjugate
}}
{{eqn | o = \le
      | r = \cmod z^2 + \cmod w^2 + 2 \cmod {z \overline w}
      | c = Modulus Larger than Real Part
}}
{{eqn | r = \cmod z^2 + \cmod w^2 + 2 \cmod z \cmod {\overline w}
      | c = Complex Modulus of Product of Complex Numbers
}}
{{eqn | r = \cmod z^2 + \cmod w^2 + 2 \cmod z \cmod w
      | c = Complex Modulus equals Complex Modulus of Conjugate
}}
{{eqn | r = \paren {\cmod z + \cmod w}^2
      | c = Square of Sum
}}
{{eqn | ll= \leadsto
      | l = \cmod {z + w}
      | o = \le
      | r = \cmod z + \cmod w
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Triangle Inequality/Vectors in Euclidean Space

Let $\mathbf x, \mathbf y$ be vectors in the real Euclidean space $\R^n$.
Let $\norm {\, \cdot \,}$ denote vector length.
Then:
:$\norm {\mathbf x + \mathbf y} \le \norm {\mathbf x} + \norm {\mathbf y}$
If the two vectors are scalar multiples where said scalar is non-negative, an equality holds:
:$\exists \lambda \in \R, \lambda \ge 0: \mathbf x = \lambda \mathbf y \iff \norm {\mathbf x + \mathbf y} = \norm {\mathbf x} + \norm {\mathbf y}$

Proof:
Let $\mathbf x, \mathbf y \in \R^n$.
We have:
{{begin-eqn}}
{{eqn | l = \norm {\mathbf x + \mathbf y}^2
      | r = \paren {\mathbf x + \mathbf y} \cdot \paren {\mathbf x + \mathbf y}
      | c = Dot Product of Vector with Itself
}}
{{eqn | r = \mathbf x \cdot \mathbf x + \mathbf x \cdot \mathbf y + \mathbf y \cdot \mathbf x  + \mathbf y \cdot \mathbf y
      | c = Dot Product Distributes over Addition
}}
{{eqn | r = \mathbf x \cdot \mathbf x + 2 \paren {\mathbf x \cdot \mathbf y} + \mathbf y \cdot \mathbf y
      | c = Dot Product Operator is Commutative
}}
{{eqn | r = \norm {\mathbf x}^2 + 2 \paren {\mathbf x \cdot \mathbf y} + \norm {\mathbf y}^2
      | c = Dot Product of Vector with Itself
}}
{{end-eqn}}
From the Cauchy-Bunyakovsky-Schwarz Inequality:
{{begin-eqn}}
{{eqn | l = \size {\mathbf x \cdot \mathbf y}
      | o = \le 
      | r = \norm {\mathbf x} \norm {\mathbf y}
}}
{{eqn | ll= \leadsto
      | l = \mathbf x \cdot \mathbf y
      | o = \le
      | r = \norm {\mathbf x} \norm {\mathbf y}
      | c = Negative of Absolute Value
}}
{{eqn | ll = \leadsto
      | l = \norm {\mathbf x}^2 + 2 \paren {\mathbf x \cdot \mathbf y} + \norm {\mathbf y}^2
      | o = \le
      | r = \norm {\mathbf x}^2 + 2 \paren {\norm {\mathbf x} \norm {\mathbf y} } + \norm {\mathbf y}^2
      | c = multiply both sides with $2$, and add $\norm {\mathbf x}^2 + \norm {\mathbf y}^2$ to both sides
}}
{{eqn | r = \paren {\norm {\mathbf x} + \norm {\mathbf y} }^2
}}
{{eqn | ll= \leadsto
      | l = \norm {\mathbf x + \mathbf y}^2
      | o = \le
      | r = \paren {\norm {\mathbf x} + \norm {\mathbf y} }^2
}}
{{eqn | ll= \leadsto
      | l = \norm {\mathbf x + \mathbf y}
      | o = \le
      | r = \norm {\mathbf x} + \norm {\mathbf y}
      | c = taking the square root of both sides
}}
{{end-eqn}}
{{qed}}
To prove that the equality holds if the vectors are scalar multiples of each other, assume:
:$\exists \lambda \in \R, \lambda \ge 0: \mathbf v = \lambda \mathbf w$