avewright/proofwiki-math huggingface dataset:
Theorem: Inverse Tangent of Imaginary Number

:$\map {\tan^{-1} } {i x} = i \tanh^{-1} x$

Proof:
{{begin-eqn}}
{{eqn | l = y
      | r = \map {\tan^{-1} } {i x}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \tan y
      | r = i x
      | c = {{Defof|Inverse Tangent}}
}}
{{eqn | ll= \leadsto
      | l = i \tan y
      | r = - x
      | c = $i^2 = -1$
}}
{{eqn | ll= \leadsto
      | l = \map \tanh {i y}
      | r = -x
      | c = Tangent in terms of Hyperbolic Tangent
}}
{{eqn | ll= \leadsto
      | l = i y
      | r = \map {\tanh^{-1} } {-x}
      | c = {{Defof|Inverse Hyperbolic Tangent}}
}}
{{eqn | ll= \leadsto
      | l = i y
      | r = -\tanh^{-1} x
      | c = Inverse Hyperbolic Tangent is Odd Function
}}
{{eqn | ll= \leadsto
      | l = y
      | r = i \tanh^{-1} x
      | c = multiplying both sides by $-i$
}}
{{end-eqn}}
{{qed}}
Theorem: Inverse Tangent of Imaginary Number

:$\map {\tan^{-1} } {i x} = i \tanh^{-1} x$

Proof:
{{begin-eqn}}
{{eqn	| l = \map {\tan^{-1} } {i x}
	| r = \frac i 2 \map \ln {\frac {1 - i \paren {i x} } {1 + i \paren {i x} } }
	| c = Arctangent Logarithmic Formulation
}}
{{eqn	| r = \frac i 2 \map \ln {\frac {1 + x} {1 - x} }
}}
{{eqn	| r = i \tanh^{-1} x
	| c = {{Defof|Inverse Hyperbolic Tangent}} 
}}
{{end-eqn}}
{{qed}}
Theorem: Inverse Hyperbolic Tangent of Imaginary Number

:$\map {\tanh^{-1} } {i x} = i \tan^{-1} x$

Proof:
{{begin-eqn}}
{{eqn | l = y
      | r = \map {\tanh^{-1} } {i x}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \tanh y
      | r = i x
      | c = {{Defof|Inverse Hyperbolic Tangent}}
}}
{{eqn | ll= \leadsto
      | l = i \tanh y
      | r = -x
      | c = $i^2 = -1$
}}
{{eqn | ll= \leadsto
      | l = \map \tan {i y}
      | r = -x
      | c = Hyperbolic Tangent in terms of Tangent
}}
{{eqn | ll= \leadsto
      | l = i y
      | r = \map {\tan^{-1} } {-x}
      | c = {{Defof|Inverse Tangent}}
}}
{{eqn | ll= \leadsto
      | l = i y
      | r = -\tan^{-1} x
      | c = Inverse Tangent is Odd Function
}}
{{eqn | ll= \leadsto
      | l = y
      | r = i \tan^{-1} x
      | c = multiplying both sides by $-i$
}}
{{end-eqn}}
{{qed}}
Theorem: Inverse Cotangent of Imaginary Number

:$\map {\cot^{-1} } {i x} = - i \coth^{-1} x$

Proof:
{{begin-eqn}}
{{eqn | l = y
      | r = \map {\cot^{-1} } {i x}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \cot y
      | r = i x
      | c = {{Defof|Inverse Cotangent}}
}}
{{eqn | ll= \leadsto
      | l = i \cot y
      | r = - x
      | c = $i^2 = -1$
}}
{{eqn | ll= \leadsto
      | l = \map \coth {i y}
      | r = x
      | c = Cotangent in terms of Hyperbolic Cotangent
}}
{{eqn | ll= \leadsto
      | l = i y
      | r = \coth^{-1} x
      | c = {{Defof|Inverse Hyperbolic Cotangent}}
}}
{{eqn | ll= \leadsto
      | l = y
      | r = -i \coth^{-1} x
      | c = multiplying both sides by $-i$
}}
{{end-eqn}}
{{qed}}
Theorem: Inverse Hyperbolic Cotangent of Imaginary Number

:$\map {\coth^{-1} } {i x} = i \cot^{-1} x$

Proof:
{{begin-eqn}}
{{eqn | l = y
      | r = \map {\coth^{-1} } {i x}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \coth y
      | r = i x
      | c = {{Defof|Inverse Hyperbolic Cotangent}}
}}
{{eqn | ll= \leadsto
      | l = i \coth y
      | r = - x
      | c = $i^2 = -1$
}}
{{eqn | ll= \leadsto
      | l = \map \cot {i y}
      | r = x
      | c = Hyperbolic Cotangent in terms of Cotangent
}}
{{eqn | ll= \leadsto
      | l = i y
      | r = \cot^{-1} x
      | c = {{Defof|Inverse Cotangent}}
}}
{{eqn | ll= \leadsto
      | l = y
      | r = -i \cot^{-1} x
      | c = multiplying both sides by $-i$
}}
{{end-eqn}}
{{qed}}
Theorem: Inverse Secant of Imaginary Number

:$\sec^{-1} x = \pm i \sech^{-1} x$

Proof:
{{begin-eqn}}
{{eqn | l = y
      | r = \sec^{-1} x
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \sec y
      | r = x
      | c = {{Defof|Inverse Secant}}
}}
{{eqn | ll= \leadsto
      | l = \map \sec {\pm \, y}
      | r = x
      | c = Secant Function is Even
}}
{{eqn | ll= \leadsto
      | l = \map \sech {\pm \, i y}
      | r = x
      | c = Secant in terms of Hyperbolic Secant
}}
{{eqn | ll= \leadsto
      | l = \pm \, i y
      | r = \sech^{-1} x
      | c = {{Defof|Inverse Hyperbolic Secant}}
}}
{{eqn | ll= \leadsto
      | l = y
      | r = \pm \, i \sech^{-1} x
      | c = multiplying both sides by $\pm \, i$
}}
{{end-eqn}}
{{qed}}
Theorem: Inverse Hyperbolic Secant of Imaginary Number

:$\sech^{-1} x = \pm \, i \sec^{-1} x$

Proof:
{{begin-eqn}}
{{eqn | l = y
      | r = \sech^{-1} x
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \sech y
      | r = x
      | c = {{Defof|Inverse Hyperbolic Secant}}
}}
{{eqn | ll= \leadsto
      | l = \map \sech {\pm \, y}
      | r = x
      | c = Hyperbolic Secant Function is Even
}}
{{eqn | ll= \leadsto
      | l = \map \sec {\pm \, i y}
      | r = x
      | c = Hyperbolic Secant in terms of Secant
}}
{{eqn | ll= \leadsto
      | l = \pm \, i y
      | r = \sec^{-1} x
      | c = {{Defof|Inverse Secant}}
}}
{{eqn | ll= \leadsto
      | l = y
      | r = \pm \, i \sec^{-1} x
      | c = multiplying both sides by $\pm \, i$
}}
{{end-eqn}}
{{qed}}
Theorem: Inverse Cosecant of Imaginary Number

:$\map {\csc^{-1} } {i x} = i \csch^{-1} x$

Proof:
{{begin-eqn}}
{{eqn | l = y
      | r = \map {\csc^{-1} } {i x}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \csc y
      | r = i x
      | c = {{Defof|Inverse Cosecant}}
}}
{{eqn | ll= \leadsto
      | l = i \csc y
      | r = -x
      | c = $i^2 = -1$
}}
{{eqn | ll= \leadsto
      | l = \map \csch {i y}
      | r = -x
      | c = Cosecant in terms of Hyperbolic Cosecant
}}
{{eqn | ll= \leadsto
      | l = i y
      | r = \map {\csch^{-1} } {-x}
      | c = {{Defof|Inverse Hyperbolic Cosecant}}
}}
{{eqn | ll= \leadsto
      | l = i y
      | r = -\csch^{-1} x
      | c = Inverse Hyperbolic Cosecant is Odd Function
}}
{{eqn | ll= \leadsto
      | l = y
      | r = i \sinh^{-1} x
      | c = multiplying both sides by $-i$
}}
{{end-eqn}}
{{qed}}
Theorem: Inverse Hyperbolic Cosecant of Imaginary Number

:$\map {\csch^{-1} } {i x} = -i \csc^{-1} x$

Proof:
{{begin-eqn}}
{{eqn | l = y
      | r = \map {\csch^{-1} } {i x}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \csch y
      | r = i x
      | c = {{Defof|Inverse Hyperbolic Cosecant}}
}}
{{eqn | ll= \leadsto
      | l = i \csch y
      | r = - x
      | c = $i^2 = -1$
}}
{{eqn | ll= \leadsto
      | l = \map \csc {i y}
      | r = x
      | c = Hyperbolic Cosecant in terms of Cosecant
}}
{{eqn | ll= \leadsto
      | l = i y
      | r = \csc^{-1} x
      | c = {{Defof|Inverse Cosecant}}
}}
{{eqn | ll= \leadsto
      | l = y
      | r = -i \csc^{-1} x
      | c = multiplying both sides by $-i$
}}
{{end-eqn}}
{{qed}}
Theorem: Arccosecant of Reciprocal equals Arcsine

:$\map \arccsc {\dfrac 1 x} = \arcsin x$

Proof:
{{begin-eqn}}
{{eqn | l = \map \arccsc {\frac 1 x}
      | r = y
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | l = \frac 1 x
      | r = \csc y
      | c = {{Defof|Real Arccosecant}}
}}
{{eqn | ll= \leadstoandfrom
      | l = x
      | r = \sin y
      | c = Cosecant is Reciprocal of Sine
}}
{{eqn | ll= \leadstoandfrom
      | l = \arcsin x
      | r = y
      | c = {{Defof|Real Arcsine}}
}}
{{end-eqn}}
{{qed}}
Category:Arcsine Function
Category:Arccosecant Function
Category:Reciprocals
rnc2f533xwi3n71y3imohykb9ygh78j
Theorem: Arcsecant of Reciprocal equals Arccosine

:$\map \arcsec {\dfrac 1 x} = \arccos x$

Proof:
{{begin-eqn}}
{{eqn | l = \map \arcsec {\frac 1 x}
      | r = y
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | l = \frac 1 x
      | r = \sec y
      | c = {{Defof|Real Arcsecant}}
}}
{{eqn | ll= \leadstoandfrom
      | l = x
      | r = \cos y
      | c = Secant is Reciprocal of Cosine
}}
{{eqn | ll= \leadstoandfrom
      | l = \arccos x
      | r = y
      | c = {{Defof|Real Arcsecant}}
}}
{{end-eqn}}
{{qed}}
Category:Arccosine Function
Category:Arcsecant Function
Category:Reciprocals
azdgatzfzwhunql6i6gvtdyae65r27j
Theorem: Arccotangent of Reciprocal equals Arctangent

:$\map \arccot {\dfrac 1 x} = \arctan x$

Proof:
{{begin-eqn}}
{{eqn | l = \map \arccot {\frac 1 x}
      | r = y
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | l = \frac 1 x
      | r = \cot y
      | c = {{Defof|Real Arccotangent}}
}}
{{eqn | ll= \leadstoandfrom
      | l = x
      | r = \tan y
      | c = Cotangent is Reciprocal of Tangent
}}
{{eqn | ll= \leadstoandfrom
      | l = \arctan x
      | r = y
      | c = {{Defof|Real Arctangent}}
}}
{{end-eqn}}
{{qed}}
Category:Arctangent Function
Category:Arccotangent Function
Category:Reciprocals
66zcupv5ytazus0rt39dlmoj48kxzbp
Theorem: Solution to Quadratic Equation/Real Coefficients

Let $a, b, c \in \R$.
The quadratic equation $a x^2 + b x + c = 0$ has:
:Two real solutions if $b^2 - 4 a c > 0$
:One real solution if $b^2 - 4 a c = 0$
:Two complex solutions if $b^2 - 4 a c < 0$, and those two solutions are complex conjugates.

Proof:
From Solution to Quadratic Equation:
:$x = \dfrac {-b \pm \sqrt {b^2 - 4 a c} } {2 a}$
If the discriminant $b^2 - 4 a c > 0$ then $\sqrt {b^2 - 4 a c}$ has two values and the result follows.
If the discriminant $b^2 - 4 a c = 0$ then $\sqrt {b^2 - 4 a c} = 0$ and $x = \dfrac {-b} {2 a}$.
If the discriminant $b^2 - 4 a c < 0$, then it can be written as:
:$b^2 - 4 a c = \paren {-1} \size {b^2 - 4 a c}$
Thus:
:$\sqrt {b^2 - 4 a c} = \pm i \sqrt {\size {b^2 - 4 a c} }$
and the two solutions are:
:$x = \dfrac {-b} {2 a} + i \dfrac {\sqrt {\size {b^2 - 4 a c} } } {2 a}, x = \dfrac {-b} {2 a} - i \dfrac {\sqrt {\size {b^2 - 4 a c} } } {2 a}$
and once again the result follows.
{{qed}}
Theorem: Sum of Roots of Quadratic Equation

Let $P$ be the quadratic equation $a x^2 + b x + c = 0$.
Let $\alpha$ and $\beta$ be the roots of $P$.
Then:
:$\alpha + \beta = -\dfrac b a$

Proof:
{{begin-eqn}}
{{eqn | l = \alpha
      | r = \frac {-b + \sqrt {b^2 - 4 a c} } {2 a}
      | c = Solution to Quadratic Equation
}}
{{eqn | l = \beta
      | r = \frac {-b - \sqrt {b^2 - 4 a c} } {2 a}
      | c = {{WLOG}}, selecting $\alpha$ and $\beta$ as such
}}
{{eqn | ll= \leadsto
      | l = \alpha + \beta
      | r = \frac {-b - \sqrt {b^2 - 4 a c} - b + \sqrt {b^2 - 4 a c} } {2 a}
      | c = 
}}
{{eqn | r = \frac {-2 b} {2 a}
      | c = 
}}
{{eqn | r = -\frac b a
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Product of Roots of Quadratic Equation

Let $P$ be the quadratic equation $a x^2 + b x + c = 0$.
Let $\alpha$ and $\beta$ be the roots of $P$.
Then:
:$\alpha \beta = \dfrac c a$

Proof:
{{begin-eqn}}
{{eqn | l = \alpha
      | r = \frac {-b + \sqrt {b^2 - 4 a c} } {2 a}
      | c = Solution to Quadratic Equation
}}
{{eqn | l = \beta
      | r = \frac {-b - \sqrt {b^2 - 4 a c} } {2 a}
      | c = {{WLOG}}, selecting $\alpha$ and $\beta$ as such
}}
{{eqn | ll= \leadsto
      | l = \alpha \beta
      | r = \frac {\paren {-b - \sqrt {b^2 - 4 a c} } \paren {- b + \sqrt {b^2 - 4 a c} } } {4 a^2}
      | c = 
}}
{{eqn | r = \frac {b^2 - \paren {b^2 - 4 a c} } {4 a^2}
      | c = Difference of Two Squares
}}
{{eqn | r = \frac {4 a c} {4 a^2}
}}
{{eqn | r = \frac c a
}}
{{end-eqn}}
{{qed}}
Theorem: Cardano's Formula/Real Coefficients

:$(1): \quad$ If $D > 0$, then one root is real and two are complex conjugates.
:$(2): \quad$ If $D = 0$, then all roots are real, and at least two are equal.
:$(3): \quad$ If $D < 0$, then all roots are real and unequal.

Proof:
From Cardano's Formula, the roots of $P$ are:
{{begin-eqn}}
{{eqn | n = 1
      | l = x_1
      | r = S + T - \dfrac b {3 a}
}}
{{eqn | n = 2
      | l = x_2
      | r = -\dfrac {S + T} 2 - \dfrac b {3 a} + \dfrac {i \sqrt 3} 2 \paren {S - T}
}}
{{eqn | n = 3
      | l = x_3
      | r = -\dfrac {S + T} 2 - \dfrac b {3 a} - \dfrac {i \sqrt 3} 2 \paren {S - T}
}}
{{end-eqn}}
where:
{{begin-eqn}}
{{eqn | l = S
      | r = \sqrt [3] {R + \sqrt {Q^3 + R^2} }
}}
{{eqn | l = T
      | r = \sqrt [3] {R - \sqrt {Q^3 + R^2} }
}}
{{end-eqn}}
Theorem: Cardano's Formula/Trigonometric Form

Let $a, b, c, d \in \R$.
Let the discriminant $D < 0$, where $D := Q^3 + R^2$.
Then the solutions of $P$ can be expressed as:
{{begin-eqn}}
{{eqn | n = 1
      | l = x_1
      | r = 2 \sqrt {-Q} \map \cos {\dfrac \theta 3} - \dfrac b {3 a}
}}
{{eqn | n = 2
      | l = x_2
      | r = 2 \sqrt {-Q} \map \cos {\dfrac \theta 3 + \dfrac {2 \pi} 3} - \dfrac b {3 a}
}}
{{eqn | n = 3
      | l = x_3
      | r = 2 \sqrt {-Q} \map \cos {\dfrac \theta 3 + \dfrac {4 \pi} 3} - \dfrac b {3 a}
}}
{{end-eqn}}
where:
:$\cos \theta = \dfrac R {\sqrt {-Q^3} }$

Proof:
From Cardano's Formula, the roots of $P$ are:
{{begin-eqn}}
{{eqn | n = 1
      | l = x_1
      | r = S + T - \dfrac b {3 a}
}}
{{eqn | n = 2
      | l = x_2
      | r = -\dfrac {S + T} 2 - \dfrac b {3 a} + \dfrac {i \sqrt 3} 2 \paren {S - T}
}}
{{eqn | n = 3
      | l = x_3
      | r = -\dfrac {S + T} 2 - \dfrac b {3 a} - \dfrac {i \sqrt 3} 2 \paren {S - T}
}}
{{end-eqn}}
where:
{{begin-eqn}}
{{eqn | l = S
      | r = \sqrt [3] {R + \sqrt {Q^3 + R^2} }
}}
{{eqn | l = T
      | r = \sqrt [3] {R - \sqrt {Q^3 + R^2} }
}}
{{end-eqn}}
Let $D = Q^3 + R^2 < 0$.
Then:
:$S^3 = R + i \sqrt {\size {Q^3 + R^2} }$
We can express this in polar form:
:$S^3 = r \paren {\cos \theta + i \sin \theta}$
where:
:$r = \sqrt {R^2 + \paren {\sqrt {Q^3 + R^2} }^2} = \sqrt {R^2 - \paren {Q^3 + R^2} } = \sqrt {-Q^3}$
:$\tan \theta = \dfrac {\sqrt {\size {Q^3 + R^2} } } R$
Then:
:$\cos \theta = \dfrac R {\sqrt {-Q^3} }$
Similarly for $T^3$.
The result:
{{begin-eqn}}
{{eqn | n = 1
      | l = x_1
      | r = 2 \sqrt {-Q} \map \cos {\dfrac \theta 3} - \dfrac b {3 a}
}}
{{eqn | n = 2
      | l = x_2
      | r = 2 \sqrt {-Q} \map \cos {\dfrac \theta 3 + \dfrac {2 \pi} 3} - \dfrac b {3 a}
}}
{{eqn | n = 3
      | l = x_3
      | r = 2 \sqrt {-Q} \map \cos {\dfrac \theta 3 + \dfrac {4 \pi} 3} - \dfrac b {3 a}
}}
{{end-eqn}}
follows after some algebra.
{{qed}}
Theorem: Ring is Module over Itself

Let $\struct {R, +, \circ}$ be a ring.
Then $\struct {R, +, \circ}_R$ is an $R$-module.

Proof:
Note that:
$\struct {R, +, \circ}$ is a ring by assumption.
$\struct {R, +}$ is an abelian group by the definition of a ring.
Let us verify the module axioms:
{{begin-axiom}}
{{axiom | n = 1
        | q = \forall x, y, z \in R
        | m = x \circ \paren {y + z} = \paren {x \circ y} + \paren {x \circ z}
}}
{{axiom | n = 2
        | q = \forall x, y, z \in R
        | m = \paren {x + y} \circ z = \paren {x \circ z} + \paren {y \circ z}
}}
{{axiom | n = 3
        | q = \forall x, y, z \in R
        | m = \paren {x \circ y} \circ z = x \circ \paren {y \circ z}
}}
{{end-axiom}}
Axiom $(1)$ and $(2)$ follow from distributivity of $\circ$.
Axiom $(3)$ follows from associativity of $\circ$. 
{{qed}}
Theorem: Ring is Module over Itself

Let $\struct {R, +, \circ}$ be a ring.
Then $\struct {R, +, \circ}_R$ is an $R$-module.

Proof:
This is a special case of Module on Cartesian Product is Module:
:$\struct {R^n, +, \circ}_R$ is an $R$-module
where $n = 1$.
{{qed}}
Theorem: Rational Division is Closed

The set of rational numbers less zero is closed under division:
:$\forall a, b \in \Q_{\ne 0}: a / b \in \Q_{\ne 0}$

Proof:
From the definition of division:
:$a / b := a \times \paren {b^{-1} }$
where $b^{-1}$ is the inverse for rational multiplication.
From Non-Zero Rational Numbers under Multiplication form Infinite Abelian Group, the algebraic structure $\struct {\Q_{\ne 0}, \times}$ is a group.
From {{Group-axiom|3}} it follows that every $b \in \Q_{\ne 0}$ has an inverse element $b^{-1} \in \Q$ under multiplication.
From {{Group-axiom|0}} it follows that $\Q_{\ne 0}$ is closed under multiplication.
Hence the result:
:$\forall a, b \in \Q_{\ne 0}: a / b \in \Q_{\ne 0}$
{{qed}}
Theorem: Complex Modulus of Product of Complex Numbers/General Result

Let $z_1, z_2, \ldots, z_n \in \C$ be complex numbers.
Let $\cmod z$ be the modulus of $z$.
Then:
: $\cmod {z_1 z_2 \cdots z_n} = \cmod {z_1} \cdot \cmod {z_2} \cdots \cmod {z_n}$

Proof:
Proof by induction:
For all $n \in \N_{> 0}$, let $P \left({n}\right)$ be the proposition:
: $\cmod {z_1 z_2 \cdots z_n} = \cmod {z_1} \cdot \cmod {z_2} \cdots \cmod {z_n}$
$P \left({1}\right)$ is trivially true:
:$\cmod {z_1} = \cmod {z_1}$
Theorem: Complex Modulus of Quotient of Complex Numbers

Let $z_1, z_2 \in \C$ be complex numbers such that $z_2 \ne 0$.
Let $\cmod z$ denote the modulus of $z$.
Then:
:$\cmod {\dfrac {z_1} {z_2} } = \dfrac {\cmod {z_1} } {\cmod {z_2} }$

Proof:
{{begin-eqn}}
{{eqn | l = \cmod {\dfrac {z_1} {z_2} }
      | r = \cmod {z_1 \times z_2^{-1} }
      | c = {{Defof|Complex Division}}
}}
{{eqn | r = \cmod {z_1} \times \cmod {z_2^{-1} }
      | c = Complex Modulus of Product of Complex Numbers
}}
{{eqn | r = \cmod {z_1} \times \cmod {z_2}^{-1}
      | c = Complex Modulus of Reciprocal of Complex Number
}}
{{eqn | r = \dfrac {\cmod {z_1} } {\cmod {z_2} }
      | c = {{Defof|Real Division}}
}}
{{end-eqn}}
{{qed}}
Theorem: Complex Modulus of Reciprocal of Complex Number

Let $z \in \C$ be a complex number such that $z \ne 0$.
Let $\cmod z$ denote the complex modulus of $z$.
Then:
:$\cmod {\dfrac 1 z} = \dfrac 1 {\cmod z}$

Proof:
Let $z = a + i b$.
{{begin-eqn}}
{{eqn | l = \cmod {\frac 1 z}
      | r = \cmod {\frac {a - i b} {a^2 + b^2} }
      | c = Reciprocal of Complex Number
}}
{{eqn | r = \cmod {\frac a {a^2 + b^2} + i \frac {-b} {a^2 + b^2} }
      | c = 
}}
{{eqn | r = \sqrt {\paren {\frac a {a^2 + b^2} }^2 + \paren {\frac {-b} {a^2 + b^2} }^2}
      | c = {{Defof|Complex Modulus}}
}}
{{eqn | r = \frac {\sqrt {a^2 + b^2} } {a^2 + b^2}
      | c = 
}}
{{eqn | r = \frac 1 {\sqrt {a^2 + b^2} }
      | c = 
}}
{{eqn | r = \frac 1 {\cmod z}
      | c = {{Defof|Complex Modulus}}
}}
{{end-eqn}}
{{qed}}
Theorem: Triangle Inequality/Complex Numbers/General Result

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

Proof:
Proof by induction:
For all $n \in \N_{> 0}$, let $\map P n$ be the proposition:
:$\cmod {z_1 + z_2 + \dotsb + z_n} \le \cmod {z_1} + \cmod {z_2} + \dotsb + \cmod {z_n}$
$\map P 1$ is true by definition of the usual ordering on real numbers:
:$\cmod {z_1} \le \cmod {z_1}$
Theorem: Triangle Inequality for Complex Numbers/Corollary 1

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

Proof:
Let $z_3 := z_1 + z_2$.
Then:
{{begin-eqn}}
{{eqn | l = \cmod {z_3} + \cmod {\paren {-z_2} }
      | o = \ge
      | r = \cmod {z_3 + \paren {-z_2} }
      | c = Triangle Inequality for Complex Numbers
}}
{{eqn | ll= \leadsto
      | l = \cmod {z_3} + \cmod {z_2}
      | o = \ge
      | r = \cmod {z_3 - z_2}
      | c = Complex Modulus of Additive Inverse
}}
{{eqn | ll= \leadsto
      | l = \cmod {z_1 + z_2} + \cmod {z_2}
      | o = \ge
      | r = \cmod {z_1}
      | c = substituting $z_3 = z_1 + z_2$
}}
{{eqn | ll= \leadsto
      | l = \cmod {z_1 + z_2}
      | o = \ge
      | r = \cmod {z_1} - \cmod {z_2}
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Complex Modulus of Additive Inverse

Let $z \in \C$ be a complex number.
Let $-z$ be the negative of $z$:
:$z + \paren {-z} = 0$
Then:
:$\cmod z = \cmod {\paren {-z} }$
where $\cmod z$ denotes the modulus of $z$.

Proof:
Let $z = a + i b$.
{{begin-eqn}}
{{eqn | l = \cmod {\paren {-z} }
      | r = \cmod {\paren {-a - i b} }
      | c = {{Defof|Negative of Complex Number}}
}}
{{eqn | r = \sqrt {\paren {-a}^2 + \paren {-b}^2}
      | c = {{Defof|Complex Modulus}}
}}
{{eqn | r = \sqrt {a^2 + b^2}
      | c = Even Power of Negative Real Number
}}
{{eqn | r = \cmod {a + i b}
      | c = {{Defof|Complex Modulus}}
}}
{{eqn | r = \cmod z
      | c = Definition of $z$
}}
{{end-eqn}}
{{qed}}
Category:Complex Modulus
6wt6y75bct78sw0c4q7wfse098r4xw7
Theorem: Even Power of Negative Real Number

Let $x \in \R$ be a real number.
Let $n \in \Z$ be an even integer.
Then:
:$\paren {-x}^n = x^n$

Proof:
From Real Numbers form Totally Ordered Field, $\R$ is a field {{afortiori}}.
By definition, $\R$ is therefore a ring.
The result follows from Power of Ring Negative.
{{qed}}
Category:Real Numbers
fypi6553dimnhzhw1mbscas78azp2zy
Theorem: Complex Addition is Closed/Proof 1

The set of complex numbers $\C$ is closed under addition:
:$\forall z, w \in \C: z + w \in \C$

Proof:
From the informal definition of complex numbers, we define the following:
:$z = x_1 + i y_1$
:$w = x_2 + i y_2$
where $i = \sqrt {-1}$ and $x_1, x_2, y_1, y_2 \in \R$.
Then from the definition of complex addition:
:$z + w = \paren {x_1 + x_2} + i \paren {y_1 + y_2}$
From Real Numbers under Addition form Group, real addition is closed.
So:
:$\paren {x_1 + x_2} \in \R$ and $\paren {y_1 + y_2} \in \R$
Hence the result.
{{qed}}
Theorem: Complex Addition is Closed/Proof 2

The set of complex numbers $\C$ is closed under addition:
:$\forall z, w \in \C: z + w \in \C$

Proof:
From the formal definition of complex numbers, we have:
:$z = \tuple {x_1, y_1}$
:$w = \tuple {x_2, y_2}$
where $x_1, x_2, y_1, y_2 \in \R$.
Then from the definition of complex addition:
:$z + w = \tuple {x_1 + x_2, y_1 + y_2}$
From Real Numbers under Addition form Group, real addition is closed.
So:
:$\paren {x_1 + x_2} \in \R$ and $\paren {y_1 + y_2} \in \R$
and hence the result.
{{qed}}
Theorem: Cardinality of Cartesian Product of Finite Sets/General Result

Let $\ds \prod_{k \mathop = 1}^n S_k$ be the cartesian product of a (finite) sequence of sets $\sequence {S_n}$.
Then:
:$\ds \card {\prod_{k \mathop = 1}^n S_k} = \prod_{k \mathop = 1}^n \card {S_k}$

Proof:
{{tidy|I'll get to it}}
Proof by mathematical induction.
Let:
:$\ds \map P n = \paren {\card {\prod_{k \mathop = 1}^n S_k} = \prod_{k \mathop = 1}^n \card {S_k} }$
For $n = 1$:
:$\ds \card {\prod_{k \mathop = 1}^1 S_k} = \card{S_1} = \prod_{k \mathop = 1}^1 \card {S_k}$
These equalities follow directly from the definition of a finite cartesian product.
Thus $\map P n$ is true for $n = 1$. 
For $n = m + 1$ we have:
:$\ds \card {\prod_{k \mathop = 1}^{m + 1} S_k} = \card {\paren {\prod_{k \mathop = 1}^m S_k} \times S_{m + 1} }$
Applying Cardinality of Cartesian Product of Finite Sets:
:$\ds \card {\paren {\prod_{k \mathop = 1}^m S_k} \times S_{m + 1} } = \card {\prod_{k \mathop = 1}^m S_k} \times \card {S_{m + 1} }$
Applying the induction step for $n = m$:
:$\ds \card {\prod_{k \mathop = 1}^m S_k} \times \card {S_{m + 1} } = \prod_{k \mathop = 1}^m \card {S_k} \times \card {S_{m + 1} } = \prod_{k \mathop = 1}^{m + 1} \card {S_k}$
Hence for $n = m + 1$, assuming $\map P m$:
:$\ds \card {\prod_{k \mathop = 1}^{m + 1} S_k} = \prod_{k \mathop = 1}^{m + 1} \card {S_k}$
which completes the proof.
{{qed}}
Category:Cardinality of Cartesian Product
ledo04nzu1jjptq7qj378snh6fz9zgw
Theorem: Cardinality of Cartesian Product of Finite Sets/General Result/Corollary

Let $S$ be a finite set.
Let $S^n$ be a cartesian space on $S$.
Then:
:$\card {S^n} = \card S^n$

Proof:
This is an instance of Cardinality of Cartesian Product of Finite Sets: General Result, where each set is equal. 
{{qed}}
Category:Cardinality of Cartesian Product
tb04pnvlwn6zextob4zydc2tkh7xy6k
Theorem: Product of Complex Numbers in Polar Form/General Result

Let $z_1, z_2, \ldots, z_n \in \C$ be complex numbers.
Let $z_j = \polar {r_j, \theta_j}$ be $z_j$ expressed in polar form for each $j \in \set {1, 2, \ldots, n}$.
Then:
:$z_1 z_2 \cdots z_n = r_1 r_2 \cdots r_n \paren {\map \cos {\theta_1 + \theta_2 + \cdots + \theta_n} + i \map \sin {\theta_1 + \theta_2 + \cdots + \theta_n} }$

Proof:
Proof by induction:
For all $n \in \N_{>0}$, let $\map P n$ be the proposition:
:$z_1 z_2 \cdots z_n = r_1 r_2 \cdots r_n \paren {\map \cos {\theta_1 + \theta_2 + \cdots + \theta_n} + i \map \sin {\theta_1 + \theta_2 + \cdots + \theta_n} }$
Let this be expressed as:
:$\ds \prod_{j \mathop = 1}^n z_j = \prod_{j \mathop = 1}^n r_j \sum_{j \mathop = 1}^n \paren {\cos \theta_j + i \sin \theta_j}$
$\map P 1$ is the case:
:$r_1 \paren {\cos x + i \sin x} = r_1 \paren {\cos x + i \sin x }$
which is trivially true.