avewright/proofwiki-math huggingface dataset:
Theorem: Subset Product Action is Group Action

Let $\struct {G, \circ}$ be a group whose identity is $e$.
Let $\powerset G$ be the power set of $\struct {G, \circ}$.
For any $S \in \powerset G$ and for any $g \in G$, the subset product action:
:$\forall g \in G: \forall S \in \powerset G: g * S = g \circ S$
is a group action.

Proof:
Let $g \in G$.
First we note that since $G$ is closed, and $g \circ S$ consists of products of elements of $G$, it follows that:
:$g * S \subseteq G$
Next we note:
:$e * S = e \circ S = \set {e \circ s: s \in S} = \set {s: s \in S} = S$
and so {{GroupActionAxiom|2}} is satisfied.
Now let $g, h \in G$.
We have:
{{begin-eqn}}
{{eqn | l = \paren {g \circ h} * S
      | r = \paren {g \circ h} \circ S
      | c = {{Defof|Subset Product Action}}
}}
{{eqn | r = \set {\paren {g \circ h} \circ s: s \in S}
      | c = 
}}
{{eqn | r = \set {g \circ \paren {h \circ s}: s \in S}
      | c = {{Group-axiom|1}}
}}
{{eqn | r = g * \set {h \circ s: s \in S}
      | c = 
}}
{{eqn | r = g * \paren {h \circ S}
      | c = 
}}
{{eqn | r = g * \paren {h * S}
      | c = {{Defof|Subset Product Action}}
}}
{{end-eqn}}
and so {{GroupActionAxiom|1}} is satisfied.
Hence the result.
{{qed}}
Theorem: Subgroup of Elements whose Order Divides Integer

Let $A$ be an abelian group.
Let $k \in \Z$ and $B$ be a set of the form:
:$\left\{{x \in A : x^k = e}\right\}$
Then $B$ is a subgroup of $A$.

Proof:
First note that the identity $e$ satisfies $e^k = e$ and so $B$ is non-empty.
Now assume that $a, b \in B$.
Then:
{{begin-eqn}}
{{eqn | l=\left({ab^{-1} }\right)^k
      | r=a^k \left({b^{-1} }\right)^k
      | c=Power of Product in Abelian Group
}}
{{eqn | r=a^k \left({b^k}\right)^{-1}
      | c=Powers of Group Elements
}}
{{eqn | r=ee^{-1}
      | c=as $a^k = b^k = e \in B$
}}
{{eqn | r=e
      | c=Identity is Self-Inverse
}}
{{end-eqn}}
Hence, by the One-Step Subgroup Test, $B$ is a subgroup of $A$.
{{qed}}
Category:Abelian Groups
l27o0qcigojo3cxmvwlx9mpc6om1o7t
Theorem: Abelian Group Factored by Prime

Let $G$ be a finite abelian group.
Let $p$ be a prime.
Factor the order of $G$ as:
:$\order G = m p^n$
such that $p$ does not divide $m$.
Then:
:$G = H \times K$
where:
:$H = \set {x \in G : x^{p^n} = e}$
and:
:$K = \set {x \in G : x^m = e}$
Furthermore:
:$\order H = p^n$

Proof:
From Subgroup of Elements whose Order Divides Integer, both $H$ and $K$ are subgroups of $G$.
Also, because $G$ is abelian, $H$ and $K$ are normal by Subgroup of Abelian Group is Normal.
In order to prove $G = H \times K$, by the Internal Direct Product Theorem it suffices to show that $G = H K$ and $H \cap K = \set e$.
Since we have $\gcd \set {m, p^n} = 1$, there are integers $s$ and $t$ such that $1 = s m + t p^n$ by Bézout's Identity. 
Let $s$ and $t$ be two such integers.
So:
:$\forall x \in G: x = x^{s m + t p^n} = x^{s m} x^{t p^n}$
From Element to Power of Group Order is Identity:
:$x^{\order G} = e$
Therefore:
:$\paren {x^{s m} }^{p^n} = \paren {x^{p^n m} }^s = e^s = e$
and:
:$\paren {x^{t p^n} }^m = \paren {x^{p^n m} }^t = e^t = e$
By definition, $x^{s m} \in H$ and $x^{t p^n} \in K$.
We conclude that $G = H K$.
Now suppose that some $x \in H \cap K$.
Then $x^{p^n} = e = x^m$, so from Element to Power of Multiple of Order is Identity $\order x$ divides both $p^n$ and $m$.
Since $p$ does not divide $m$, it follows that $\order x = 1$.
Therefore, by Identity is Only Group Element of Order 1:
:$x = e$
Thus:
:$H \cap K = \set e$
It follows that $G = H \times K$.
Suppose that $p \divides \order K$.
From Cauchy's Lemma (Group Theory), this implies that there is some element (call it $k$) of $K$ with order $p$.
But we also have $k^m = e$ from the definition of $K$, so by Element to Power of Multiple of Order is Identity we must have $p \divides m$, a contradiction.
We conclude that:
:$p$ does not divide $\order K$
It follows that:
:$p^n \divides \order H$
{{AimForCont}} a prime $q$ (with $q \ne p$) divides $\order H$.
Again from Cauchy's Lemma (Group Theory), this implies that there is some element $h$ of $H$ with order $q$.
But since $h^{p^n} = e$ from the definition of $H$, Element to Power of Multiple of Order is Identity gives us $q \divides p^n$, a contradiction.
It follows by Proof by Contradiction that $q$ does not divide $\order H$.
We conclude $\order H = p^n$, as desired.
{{qed}}
Category:Abelian Groups
mrehh3s89lnh7tfz60q4zf9yoanvn73
Theorem: Abelian Group of Prime-power Order is Product of Cyclic Groups

Let $G$ be an abelian group of prime-power order.
Let $a$ be an element of maximal order in $G$.
Then $G$ can be written in the form $\gen a \times K$ for some $K \le G$.

Proof:
Suppose $\order G = p^n$ with $p$ a prime.
We proceed by induction on $n$.
Theorem: Power of Product in Abelian Group

Let $\struct {G, \circ}$ be an abelian group.
Then:
:$\forall x, y \in G: \forall k \in \Z: \paren {x \circ y}^k = x^k \circ y^k$

Proof:
By definition of abelian group, $x$ and $y$ commute.
That is:
:$x \circ y = y \circ x$
The result follows from Power of Product of Commutative Elements in Group.
{{qed}}
Theorem: Union of Mappings with Disjoint Domains is Mapping

Let $S_1, S_2, T_1, T_2$ be sets.
Let $f: S_1 \to T_1$ and $g: S_2 \to T_2$ be mappings.
Let $h = f \cup g$ be their union.
If $S_1 \cap S_2 = \O$, then $h: S_1 \cup S_2 \to T_1 \cup T_2$ is a mapping whose domain is $S_1 \cup S_2$.

Proof:
From the definition of mapping, it is clear that $h$ is a relation.
Suppose $\tuple {x, y_1}, \tuple {x, y_2} \in h$.
Clearly $x \in S_1$ or $x \in S_2$ but as $S_1 \cap S_2 = \O$ it is not in both.
If $x \in S_1$ then $y_1 = y_2$ as $\tuple {x, y_1}, \tuple {x, y_2} \in f$, and $f$ is a mapping.
Similarly, if $x \in S_2$ then $y_1 = y_2$ as $\tuple {x, y_1}, \tuple {x, y_2} \in g$, and $g$ is a mapping.
So $\tuple {x, y_1}, \tuple {x, y_2} \in h \implies y_1 = y_2$.
Now suppose $x \in \Dom h$.
Either $x \in S_1$ or $x \in S_2$.
As both $f$ and $g$ are mappings it follows that either $\exists y \in T_1: \tuple {x, y} \in f$ or $\exists y \in T_2: \tuple {x, y} \in g$.
In either case, $\exists y \in T_1 \cup T_2: \tuple {x, y} \in h$.
So $h$ is a mapping whose domain is $S_1 \cup S_2$, as we were to show.
{{qed}}
Theorem: Identity Element of Natural Number Addition is Zero

The identity element for the natural numbers under addition is zero ($0$):
:$\forall n \in \N: 0 + n = n$

Proof:
Take the definition of natural numbers $\N$ as a naturally ordered semigroup $\struct {\N, +, \le}$.
The result follows from Zero is Identity in Naturally Ordered Semigroup.
{{qed}}
Theorem: Sum of Tangent and Cotangent

:$\tan x + \cot x = \sec x \csc x$

Proof:
{{begin-eqn}}
{{eqn | l = \tan x + \cot x
      | r = \frac {\sin x} {\cos x} + \cot x
      | c = Tangent is Sine divided by Cosine
}}
{{eqn | r = \frac {\sin x} {\cos x} + \frac {\cos x} {\sin x}
      | c = Cotangent is Cosine divided by Sine
}}
{{eqn | r = \frac {\sin^2 x + \cos^2x} {\cos x \sin x}
      | c = 
}}
{{eqn | r = \frac 1 {\cos x \sin x}
      | c = Sum of Squares of Sine and Cosine
}}
{{eqn | r = \sec x \frac 1 {\sin x}
      | c = Secant is Reciprocal of Cosine
}}
{{eqn | r = \sec x \csc x
      | c = Cosecant is Reciprocal of Sine
}}
{{end-eqn}}
{{qed}}
Category:Trigonometric Identities
jz8w9priubh8wtrir60t5myg7ke5ubr
Theorem: Tangent times Tangent plus Cotangent

:$\tan x \paren {\tan x + \cot x} = \sec^2 x$

Proof:
{{begin-eqn}}
{{eqn|l = \tan x \left({\tan x + \cot x}\right)
     |r = \tan x \sec x \csc x
     |c = Sum of Tangent and Cotangent
}}
{{eqn|r = \frac {\sin x} {\cos x} \sec x \csc x
     |c = Tangent is Sine divided by Cosine
}}
{{eqn|r = \frac {\sin x} {\cos^2 x} \csc x
     |c = Secant is Reciprocal of Cosine
}}
{{eqn|r = \frac {\sin x} {\cos^2 x \sin x}
     |c = Cosecant is Reciprocal of Sine
}}
{{eqn|r = \frac 1 {\cos^2 x}
}}
{{eqn|r = \sec^2 x
     |c = Secant is Reciprocal of Cosine
}}
{{end-eqn}}
{{qed}}
Theorem: Tangent times Tangent plus Cotangent

:$\tan x \paren {\tan x + \cot x} = \sec^2 x$

Proof:
{{begin-eqn}}
{{eqn | l = \tan x \paren {\tan x + \cot x}
      | r = \frac {\sin x} {\cos x} \paren {\frac {\sin x} {\cos x} + \frac {\cos x} {\sin x} }
      | c = {{Defof|Tangent Function}} and {{Defof|Cotangent}}
}}
{{eqn | r = \frac {\sin x} {\cos x} \paren {\frac {\sin^2 x + \cos^2 x} {\cos x \sin x} }
}}
{{eqn | r = \frac {\sin x} {\cos x} \paren {\frac 1 {\cos x \sin x} }
      | c = Sum of Squares of Sine and Cosine
}}
{{eqn | r = \frac 1 {\cos^2 x}
}}
{{eqn | r = \sec^2 x
      | c = {{Defof|Secant Function}}
}}
{{end-eqn}}
{{qed}}
Theorem: Secant Minus Cosine

:$\sec x - \cos x = \sin x \tan x$

Proof:
{{begin-eqn}}
{{eqn | l = \sec x - \cos x
      | r = \frac 1 {\cos x} - \cos x
      | c = Secant is Reciprocal of Cosine
}}
{{eqn | r = \frac {1 - \cos^2 x} {\cos x}
}}
{{eqn | r = \frac {\sin^2 x} {\cos x}
      | c = Sum of Squares of Sine and Cosine
}}
{{eqn | r = \sin x \tan x
      | c = Tangent is Sine divided by Cosine
}}
{{end-eqn}}
{{qed}}
Category:Trigonometric Identities
oyc8fxhwro7if7zvojvnw9t2ysh21ml
Theorem: Square of Tangent Minus Square of Sine

:$\tan^2 x - \sin^2 x = \tan^2 x \ \sin^2 x$

Proof:
{{begin-eqn}}
{{eqn | l=\tan^2 x - \sin^2 x
      | r=\frac {\sin^2 x} {\cos^2x} - \sin^2 x
      | c=Tangent is Sine divided by Cosine
}}
{{eqn | r=\frac {\sin^2 x - \sin^2 x \ \cos^2 x} {\cos^2x}
}}
{{eqn | r=\frac{\sin^2 x \left({1 - \cos^2 x}\right)} {\cos^2 x}
}}
{{eqn | r=\tan^2 x \left({1 - \cos^2 x}\right)
      | c=Tangent is Sine divided by Cosine
}}
{{eqn | r=\tan^2 x \ \sin^2 x
      | c=Sum of Squares of Sine and Cosine
}}
{{end-eqn}}
{{qed}}
Category:Trigonometric Identities
0udy0som302lkqdfshoshg6bzttkw29
Theorem: Difference of Fourth Powers of Cosine and Sine

:$\sin^4 x - \cos^4 x = \sin^2 x - \cos^2 x$

Proof:
{{begin-eqn}}
{{eqn | l = \sin^4 x - \cos^4 x
      | r = \sin^2 x \left({1 - \cos^2 x}\right) - \cos^2 x \left({1 - \sin^2 x}\right)
      | c = Sum of Squares of Sine and Cosine
}}
{{eqn | r = \sin^2 x - \sin^2 x \ \cos^2 x - \cos^2 x + \sin^2 x \ \cos^2 x
}}
{{eqn | r = \sin^2 x - \cos^2 x
}}
{{end-eqn}}
{{qed}}
Theorem: Difference of Fourth Powers of Cosine and Sine

:$\sin^4 x - \cos^4 x = \sin^2 x - \cos^2 x$

Proof:
{{begin-eqn}}
{{eqn | l = \sin^2 x - \cos^2 x
      | r = \left({\sin^2 x - \cos^2 x}\right) \left({\sin^2 x + \cos^2 x}\right)
      | c = Sum of Squares of Sine and Cosine
}}
{{eqn | r = \sin^4 x - \cos^4 x
      | c = Difference of Two Squares
}}
{{end-eqn}}
{{qed}}
Theorem: Cosecant Minus Sine

:$\csc x - \sin x = \cos x \ \cot x$

Proof:
{{begin-eqn}}
{{eqn | l=\csc x - \sin x
      | r=\frac 1 {\sin x} - \sin x
      | c={{Defof|Cosecant}}
}}
{{eqn | r=\frac {1 - \sin^2 x} {\sin x}
}}
{{eqn | r=\frac {\cos^2 x} {\sin x}
      | c=Sum of Squares of Sine and Cosine
}}
{{eqn | r=\cos x \ \cot x
      | c={{Defof|Cotangent}}
}}
{{end-eqn}}
{{qed}}
Category:Trigonometric Identities
rabqz83w0fpc3rgi57tpkp7nmejr8yp
Theorem: Sum of Squares of Secant and Cosecant

:$\sec^2 x + \csc^2 x = \sec^2 x \csc^2 x$

Proof:
{{begin-eqn}}
{{eqn | l = \sec^2 x + \csc^2 x
      | r = \frac 1 {\cos^2 x} + \frac 1 {\sin^2 x}
      | c = {{Defof|Secant Function}} and {{Defof|Cosecant}}
}}
{{eqn | r = \frac {\sin^2 x + \cos^2 x} {\cos^2 x \sin^2 x}
      | c = 
}}
{{eqn | r = \frac 1 {\cos^2 x \sin^2 x}
      | c = Sum of Squares of Sine and Cosine
}}
{{eqn | r = \sec^2 x \csc^2 x
      | c = {{Defof|Secant Function}} and {{Defof|Cosecant}}
}}
{{end-eqn}}
{{qed}}
Category:Trigonometric Identities
f2qk26s0otejvk2vlje2jx2os2b089o
Theorem: Difference of Fourth Powers of Secant and Tangent

:$\sec^4 x - \tan^4 x = \sec^2 x + \tan^2 x$

Proof:
{{begin-eqn}}
{{eqn | l = \sec^4 x - \tan^4 x
      | r = \sec^4 x - \frac {\sin^4 x} {\cos^4 x}
      | c = Tangent is Sine divided by Cosine
}}
{{eqn | r = \frac 1 {\cos^4 x} - \frac {\sin^4 x} {\cos^4 x}
      | c = Secant is Reciprocal of Cosine
}}
{{eqn | r = \frac {1 - \sin^4 x} {\cos^4x}
}}
{{eqn | r = \frac {1 - \sin^2 x \paren {1 - \cos^2 x} } {\cos^2 x \paren {1 - \sin^2 x} }
      | c = Sum of Squares of Sine and Cosine
}}
{{eqn | r = \frac {1 - \sin^2 x + \sin^2 x \ \cos^2 x} {\cos^2 x - \sin^2 x \ \cos^2 x}
}}
{{eqn | r = \frac {\cos^2 x + \sin^2 x \ \cos^2 x} {\cos^2 x - \sin^2 x \ \cos^2 x}
      | c = Sum of Squares of Sine and Cosine
}}
{{eqn | r = \frac {\cos^2 x \paren {1 + \sin^2 x} } {\cos^2 x \paren {1 - \sin^2 x} }
}}
{{eqn | r = \frac {1 + \sin^2 x} {1 - \sin^2 x}
}}
{{eqn | r = \frac {1 + \sin^2 x} {\cos^2 x}
      | c = Sum of Squares of Sine and Cosine
}}
{{eqn | r = \frac 1 {\cos^2 x} + \frac {\sin^2 x} {\cos^2 x}
}}
{{eqn | r = \frac 1 {\cos^2 x} x + \tan^2 x
      | c = Tangent is Sine divided by Cosine
}}
{{eqn | r = \sec^2 x + \tan^2 x
      | c = Secant is Reciprocal of Cosine
}}
{{end-eqn}}
{{qed}}
Category:Trigonometric Identities
2iut7jzyvgs10jxbyaok8kai56cpyns
Theorem: Sum of Reciprocals of One Plus and Minus Sine

:$\dfrac 1 {1 - \sin x} + \dfrac 1 {1 + \sin x} = 2 \sec^2 x$

Proof:
{{begin-eqn}}
{{eqn | l = \frac 1 {1 - \sin x} + \frac 1 {1 + \sin x}
      | r = \frac {1 + \sin x + 1 - \sin x} {1 - \sin^2 x}
      | c = Difference of Two Squares
}}
{{eqn | r = \frac 2 {\cos^2 x}
      | c = Sum of Squares of Sine and Cosine
}}
{{eqn | r = 2 \sec^2 x
      | c = {{Defof|Secant Function}}
}}
{{end-eqn}}
{{qed}}
Category:Trigonometric Identities
Category:Sine Function
eoc9yum0imskau1zik8jiechj2yjo89
Theorem: Difference of Reciprocals of One Plus and Minus Sine

:$\ds \frac 1 {1 - \sin x} - \frac 1 {1 + \sin x} = 2 \tan x \sec x$

Proof:
{{begin-eqn}}
{{eqn | l = \frac 1 {1 - \sin x} - \frac 1 {1 + \sin x}
      | r = \frac {1 + \sin x} {1 - \sin^2 x} - \frac {1 - \sin x} {1 - \sin^2 x}
      | c = Difference of Two Squares
}}
{{eqn | r = \frac {2 \sin x} {\cos^2 x}
      | c = Sum of Squares of Sine and Cosine
}}
{{eqn | r = \frac {2 \tan x} {\cos x}
      | c = Tangent is Sine divided by Cosine
}}
{{eqn | r = 2 \tan x \sec x
      | c = Secant is Reciprocal of Cosine
}}
{{end-eqn}}
{{qed}}
Category:Trigonometric Identities
Category:Sine Function
cd2btxsuohuetmepu1y7fos9wse0cb9
Theorem: Sum of Secant and Tangent

:$\sec x + \tan x = \dfrac {1 + \sin x} {\cos x}$

Proof:
{{begin-eqn}}
{{eqn | l = \sec x + \tan x
      | r = \sec x + \frac {\sin x} {\cos x}
      | c = Tangent is Sine divided by Cosine
}}
{{eqn | r = \frac 1 {\cos x} + \frac {\sin x} {\cos x}
      | c = Secant is Reciprocal of Cosine
}}
{{eqn | r = \frac {1 + \sin x} {\cos x}
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Cosine over Sum of Secant and Tangent

:$\dfrac {\cos x} {\sec x + \tan x} = 1 - \sin x$

Proof:
{{begin-eqn}}
{{eqn | l = \frac {\cos x} {\sec x + \tan x}
      | r = \frac {\cos^2 x} {1 + \sin x}
      | c = Sum of Secant and Tangent
}}
{{eqn | r = \frac {1 - \sin^2 x} {1 + \sin x}
      | c = Sum of Squares of Sine and Cosine
}}
{{eqn | r = \frac {\paren {1 + \sin x} \paren {1 - \sin x} } {1 + \sin x}
      | c = Difference of Two Squares
}}
{{eqn | r = 1 - \sin x
}}
{{end-eqn}}
{{qed}}
Category:Trigonometric Identities
j1dy19ag3ylw8gkc1yh8rx9voltltmz
Theorem: Secant Plus One over Secant Squared

:$\dfrac {\sec x + 1} {\sec^2 x} = \dfrac {\sin^2 x} {\sec x - 1}$

Proof:
{{begin-eqn}}
{{eqn | l = \frac {\sec x + 1} {\sec^2 x}
      | r = \cos^2 x \paren {\frac 1 {\cos x} + 1}
      | c = {{Defof|Secant Function}}
}}
{{eqn | r = \cos x + \cos^2x
}}
{{eqn | r = \cos x \paren {1 + \cos x}
}}
{{eqn | r = \cos x \frac {\paren {1 + \cos x} \paren {1 - \cos x} } {1 - \cos x}
}}
{{eqn | r = \frac {1 - \cos^2 x} {\frac {1 - \cos x} {\cos x} }
      | c = Difference of Two Squares
}}
{{eqn | r = \frac {\sin^2 x} {\frac 1 {\cos x} - 1}
      | c = Sum of Squares of Sine and Cosine
}}
{{eqn | r = \frac {\sin^2 x} {\sec x - 1}
      | c = {{Defof|Secant Function}}
}}
{{end-eqn}}
{{qed}}
Category:Trigonometric Identities
iaf30ctyjtayzh4xmt23fszdhwdby7w
Theorem: Sine Plus Cosine times Tangent Plus Cotangent

:$\paren {\sin x + \cos x} \paren {\tan x + \cot x} = \sec x + \csc x$

Proof:
{{begin-eqn}}
{{eqn | l = \paren {\sin x + \cos x} \paren {\tan x + \cot x}
      | r = \paren {\sin x + \cos x} \paren {\sec x \csc x}
      | c = Sum of Tangent and Cotangent
}}
{{eqn | r = \frac {\sin x + \cos x} {\sin x \cos x}
      | c = {{Defof|Secant Function}} and {{Defof|Cosecant}}
}}
{{eqn | r = \frac 1 {\cos x} + \frac 1 {\sin x}
}}
{{eqn | r = \sec x + \csc x
      | c = {{Defof|Secant Function}} and {{Defof|Cosecant}}
}}
{{end-eqn}}
{{qed}}
Category:Trigonometric Identities
mfhi8x6zpj7jjyn9usxkwmft0vebngd
Theorem: Tangent over Secant Plus One

:$\dfrac {\tan x} {\sec x + 1} = \dfrac {\sec x - 1} {\tan x}$

Proof:
{{begin-eqn}}
{{eqn | l = \frac {\tan x} {\sec x + 1}
      | r = \frac {\sin x} {\cos x \paren {\sec x + 1} }
      | c = Tangent is Sine divided by Cosine
}}
{{eqn | r = \frac {\sin x} {\cos x \paren {\frac 1 {\cos x} + 1} }
      | c = Secant is Reciprocal of Cosine
}}
{{eqn | r = \frac {\sin x} {1 + \cos x}
      | c = simplifying
}}
{{eqn | r = \frac {\sin^2 x} {\sin x \paren {1 + \cos x} }
      | c = Multiply by $1 = \dfrac {\sin x} {\sin x}$
}}
{{eqn | r = \frac {1 - \cos^2 x} {\sin x \paren {1 + \cos x} }
      | c = Sum of Squares of Sine and Cosine
}}
{{eqn | r = \frac {\paren {1 + \cos x} \paren {1 - \cos x} } {\sin x \paren {1 + \cos x} }
      | c = Difference of Two Squares
}}
{{eqn | r = \frac {1 - \cos x} {\sin x}
}}
{{eqn | r = \frac {\cos x \paren {\frac 1 {\cos x} - 1} } {\sin x}
}}
{{eqn | r = \frac {\cos x \paren {\sec x - 1} } {\sin x}
      | c = Secant is Reciprocal of Cosine
}}
{{eqn | r = \frac {\sec x - 1} {\tan x}
      | c = Tangent is Sine divided by Cosine
}}
{{end-eqn}}
{{qed}}
Category:Trigonometric Identities
idig4zjx0302z67krfm7key0yiovfz0
Theorem: Squares of Linear Combination of Sine and Cosine

:$\paren {a \cos x + b \sin x}^2 + \paren {b \cos x - a \sin x}^2 = a^2 + b^2$

Proof:
{{begin-eqn}}
{{eqn | l = \paren {a \cos x + b \sin x}^2 + \paren {b \cos x - a \sin x}^2
      | r = a^2 \cos^2 x + 2 a b \cos x \ \sin x + b^2 \sin^2 x
}}
{{eqn | o =
      | ro= +
      | r = b^2 \cos^2 x - 2 a b \sin x \ \cos x + a^2 \sin^2 x
}}
{{eqn | r = \paren {a^2 + b^2} \paren {\sin^2 x + \cos^2 x}
}}
{{eqn | r = a^2 + b^2
      | c = Sum of Squares of Sine and Cosine
}}
{{end-eqn}}
{{qed}}
Category:Trigonometric Identities
bcmlhj8tnly0k2075zockuxa90pn0nn
Theorem: Reciprocal of One Minus Secant

:$\dfrac {\sin^2 x + 2 \cos x - 1} {\sin^2 x + 3 \cos x - 3} = \dfrac 1 {1 - \sec x}$

Proof:
{{begin-eqn}}
{{eqn | l = \frac {\sin^2 x + 2 \cos x - 1} {\sin^2 x + 3 \cos x - 3}
      | r = \frac {1 - \cos^2 x - 2 \cos x - 1} {1 - \cos^2 x + 3 \cos x - 3}
      | c = Sum of Squares of Sine and Cosine
}}
{{eqn | r = \frac {\cos^2 x - 2 \cos x} {\cos^2 x - 3 \cos x + 2}
}}
{{eqn | r = \frac {\cos x \paren {\cos x - 2} } {\paren {\cos x - 1} \paren {\cos x - 2} }
}}
{{eqn | r = \frac {\cos x} {\cos x - 1}
}}
{{eqn | r = \frac 1 {1 - \frac 1 {\cos x} }
}}
{{eqn | r = \frac 1 {1 - \sec x}
      | c = {{Defof|Secant Function}}
}}
{{end-eqn}}
{{qed}}
Category:Trigonometric Identities
Category:Reciprocals
jw6l8r12fpiz009jcnowmdwb2xhvxx0
Theorem: Reciprocal of One Plus Cosecant

:$\dfrac {\cos^2 x + 3 \sin x - 1} {\cos^2 x + 2 \sin x + 2} = \dfrac 1 {1 + \csc x}$

Proof:
{{begin-eqn}}
{{eqn | l = \frac {\cos^2 x + 3 \sin x - 1} {\cos^2 x + 2 \sin x + 2}
      | r = \frac {1 - \sin^2 x + 3 \sin x - 1} {1 - \sin^2 x + 2 \sin x + 2}
      | c = Sum of Squares of Sine and Cosine
}}
{{eqn | r = \frac {\sin^2 x - 3 \sin x} {\sin^2 x - 2 \sin x - 3}
}}
{{eqn | r = \frac {\sin x \paren {\sin x - 3} } {\paren {\sin x - 3} \paren {\sin x + 1} }
}}
{{eqn | r = \frac {\sin x} {\sin x + 1}
}}
{{eqn | r = \frac 1 {1 + \dfrac 1 {\sin x} }
}}
{{eqn | r = \frac 1 {1 + \csc x}
      | c = {{Defof|Real Cosecant Function}}
}}
{{end-eqn}}
{{qed}}
Category:Trigonometric Identities
Category:Reciprocals
5pi4374lgdmak9nbd7rwo0oczh4a6oa
Theorem: Conversion of Cauchy-Euler Equation to Constant Coefficient Linear ODE/General Result

Let $n \in \Z_{>0}$ be a strictly positive integer.
The ordinary differential equation:
:$a_n x^n \, \map {f^{\paren n} } x + \dotsb + a_1 x \, \map {f'} c + a_0 \, \map f x = 0$
can be transformed to a linear differential equation with constant coefficients by substitution $x = e^t$.

Proof:
Let $y = \map f x$.
First the following are established:
{{begin-eqn}}
{{eqn | l = x
      | r = e^t
      | c = Derivative of Exponential Function
}}
{{eqn | ll= \leadsto
      | l = \frac {\d x} {\d t}
      | r = e^t
      | c = 
}}
{{eqn | n = 1
      | r = x
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \frac {\d t} {\d x}
      | r = \frac 1 x
      | c = Derivative of Inverse Function
}}
{{eqn | n = 2
      | r = e^{-t}
      | c = 
}}
{{end-eqn}}
The proof now proceeds by induction.
For all $n \in \Z_{> 0}$, let $\map P n$ be the proposition:
:$a_n x^n \, \map {f^{\paren n} } x + \dotsb + a_1 x \, \map {f'} x + a_0 \, \map f x = 0$
can be transformed to a linear differential equation with constant coefficients by substitution $x = e^t$.
Theorem: Condition for Composite Relation with Inverse to be Identity

Let $\RR \subseteq S \times T$ be a relation on $S \times T$.
Let $\RR \circ \RR^{-1}$ be the composite of $\RR$ with its inverse.
Let $I_T$ be the identity mapping on $T$.
Then:
:$\RR \circ \RR^{-1} = I_T$
{{iff}}:
:$\RR$ is many-to-one
and:
:$\RR$ is right-total.

Proof:
=== Sufficient Condition ===
Let $\RR \circ \RR^{-1} = I_T$.
{{AimForCont}}:
:$\exists t \in T: t \notin \Img \RR$
Then:
:$t \notin \Img {\RR \circ \RR^{-1} }$
But:
:$t \in \Img {I_T}$
by definition of the identity mapping on $T$.
Hence:
:$\RR \circ \RR^{-1} \ne I_T$
From this contradiction we deduce that:
:$\RR \circ \RR^{-1} = I_T \implies T \setminus \Img \RR = \O$
where $T \setminus \Img \RR$ denotes set difference.
So from Set Difference with Superset is Empty Set:
:$T \subseteq \Img \RR$
But from Image is Subset of Codomain we have:
:$T \supseteq \Img \RR$
and so:
:$\Img \RR = T$
which means $\RR$ is right-total.
{{qed|lemma}}
Suppose $\RR$ is not many-to-one.
Then:
:$\exists s \in S: \exists t_1, t_2 \in T, t_1 \ne t_2: \tuple {s, t_1} \in \RR \land \tuple {s, t_2} \in \RR$
By definition of inverse relation:
:$\exists s \in S: \exists t_1, t_2 \in T: \tuple {t_1, s} \in \RR^{-1} \land \tuple {t_2, s} \in \RR^{-1}$
The composite of $\RR^{-1}$ and $\RR$ is defined as:
:$\RR \circ \RR^{-1} = \set {\tuple {x, z} \in T \times T: \exists y \in S: \tuple {x, y} \in \RR^{-1} \land \tuple {y, z} \in \RR}$
Thus:
{{begin-eqn}}
{{eqn | l = \tuple {t_1, s}
      | o = \in
      | r = \RR^{-1}
      | c = 
}}
{{eqn | l = \tuple {s, t_2}
      | o = \in
      | r = \RR
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \tuple {t_1, t_2}
      | o = \in
      | r = \RR \circ \RR^{-1}
      | c = where $t_1 \ne t_2$ (from above)
}}
{{end-eqn}}
So, by definition of identity mapping:
:$\RR \circ \RR^{-1} \ne I_T$
From this contradiction we deduce that $\RR$ must be many-to-one.
{{qed|lemma}}
So it has been demonstrated that if:
:$\RR \circ \RR^{-1} = I_T$
then:
:$\RR$ is many-to-one
and
:$\RR$ is right-total.
{{qed|lemma}}
Theorem: Set of All Relations is a Monoid

The set of all relations $\Bbb E = \set {\RR: \RR \subseteq S \times S}$ on a set $S$ forms a monoid in which the operation is composition of relations.
The only invertible elements of $\Bbb E$ are permutations.
If $\RR$ is invertible, its inverse is $\RR^{-1}$.

Proof:
=== Closure ===
A relation followed by another relation is another relation, from the definition of composition of relations.
As the domain and codomain of two relations are the same, then:
:$\forall \RR_1, \RR_2 \subseteq S \times S: \RR_1 \circ \RR_2 \subseteq S \times S$
Therefore composition of relations on a set is closed.
{{qed|lemma}}