avewright/proofwiki-math huggingface dataset:
Theorem: Powers of Semigroup Element Commute

Let $\struct {S, \odot}$ be a semigroup.
Let $a \in S$.
Let $m, n \in \Z_{>0}$.
Then:
:$\forall m, n \in \Z_{>0}: a^n \odot a^m = a^m \odot a^n$

Proof:
{{begin-eqn}}
{{eqn | l = a^n \odot a^m
      | r = a^{n + m}
      | c = Index Laws for Semigroup: Sum of Indices
}}
{{eqn | r = a^{m + n}
      | c = Integer Addition is Commutative
}}
{{eqn | r = a^m \odot a^n
      | c = Index Laws for Semigroup: Sum of Indices
}}
{{end-eqn}}
{{Qed}}
Theorem: Equivalence of Definitions of Derivative

{{TFAE|def = Derivative of Real Function at Point}}
Let $I$ be an open real interval.
Let $f: I \to \R$ be a real function defined on $I$.
Let $\xi \in I$ be a point in $I$.

Proof:
{{begin-eqn}}
{{eqn | l = f' \left({\xi}\right)
      | r = \lim_{h \mathop \to 0} \frac {f \left({\xi + h}\right) - f \left({\xi}\right)} h
      | c = 
}}
{{eqn | r = \lim_{x - \xi \mathop \to 0} \frac {f \left({x}\right) - f \left({\xi}\right)} {\xi + h - \xi}
      | c = substituting $x = \xi + h$
}}
{{eqn | r = \lim_{x \mathop \to \xi} \frac {f \left({x}\right) - f \left({\xi}\right)} {x - \xi}
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Derivative of x to the x

:$\dfrac \d {\d x} x^x = x^x \paren {\ln x + 1}$

Proof:
Note that the Power Rule cannot be used because the index is not a constant.
Let $y := x^x$.
As $x$ was stipulated to be positive, we can take the natural logarithm of both sides:
{{begin-eqn}}
{{eqn | l = \ln y
      | r = \ln x^x
}}
{{eqn | r = x \ln x
      | c = Laws of Logarithms
}}
{{eqn | l = \map {\frac \d {\d x} } {\ln y}
      | r = \map {\frac \d {\d x} } {x \ln x}
      | c = differentiating both sides {{WRT|Differentiation}} $x$
}}
{{eqn | l = \frac 1 y \frac {\d y} {\d x}
      | r = \map {\frac \d {\d x} } {x \ln x}
      | c = Chain Rule for Derivatives and Derivative of Natural Logarithm Function
}}
{{eqn | r = \map {\frac \d {\d x} } x \cdot \ln x + x \frac {\d} {\d x} \ln x
      | c = Product Rule for Derivatives
}}
{{eqn | r = 1 \cdot \ln x + x \cdot \frac 1 x
      | c = Derivative of Identity Function and Derivative of Natural Logarithm Function
}}
{{eqn | r = \ln x + 1
      | c = simplification
}}
{{eqn | l = \frac {\d y} {\d x}
      | r = x^x \paren {\ln x + 1}
      | c = multiplying both sides by $y = x^x$
}}
{{end-eqn}}
{{qed}}
Theorem: Derivative of x to the x

:$\dfrac \d {\d x} x^x = x^x \paren {\ln x + 1}$

Proof:
Note that the Power Rule cannot be used because the index is not a constant.
{{begin-eqn}}
{{eqn | l = \frac \d {\d x} x^x
      | r = \frac \d {\d x} \map \exp {x \ln x}
      | c = {{Defof|Power (Algebra)|subdef = Real Number|index = 1}}
}}
{{eqn | r = \paren {\frac \d {\map \d {x \ln x} } \map \exp {x \ln x} } \paren {\map {\frac \d {\d x} } {x \ln x} }
      | c = Chain Rule for Derivatives
}}
{{eqn | r = \map \exp {x \ln x} \paren {\map {\frac \d {\d x} } {x \ln x} }
      | c = Derivative of Exponential Function
}}
{{eqn | r = \map \exp {x \ln x} \paren {\map {\frac \d {\d x} } x \cdot \ln x + x \frac \d {\d x} \ln x}
      | c = Product Rule for Derivatives
}}
{{eqn | r = \map \exp {x \ln x} \paren {1 \cdot \ln x + x \cdot \frac 1 x}
      | c = Derivative of Identity Function and Derivative of Natural Logarithm Function
}}
{{eqn | r = \map \exp {x \ln x} \paren {\ln x + 1}
      | c = Real Multiplication Identity is One and Inverse for Real Multiplication
}}
{{eqn | r = x^x \paren {\ln x + 1}
      | c = {{Defof|Power (Algebra)|subdef = Real Number|index = 1}}
}}
{{end-eqn}}
{{qed}}
Theorem: Derivative of x to the x

:$\dfrac \d {\d x} x^x = x^x \paren {\ln x + 1}$

Proof:
From Derivative of $x^{a x}$ we have:
:$\dfrac \d {\d x} x^{a x} = a x^{a x} \paren {\ln x + 1}$
The result follows on setting $a = 1$.
{{qed}}
Theorem: Commutativity of Powers in Semigroup

:$\forall m, n \in \N_{>0}: a \circ b = b \circ a \implies a^m \circ b^n = b^n \circ a^m$
but it is not necessarily the case that:
:$\forall m, n \in \N_{>0}: a^m \circ b^n = b^n \circ a^m \implies a \circ b = b \circ a$

Proof:
Let $a, b \in S: a \circ b = b \circ a$.
Then from Powers of Commuting Elements of Semigroup Commute:
:$\forall m, n \in \N_{>0}: a^m \circ b^n = b^n \circ a^m$
{{qed|lemma}}
However, consider the dihedral group $D_3$ $= \gen {a, b: a^3 = b^2 = e, b a b = a^{−1} }$.
A group is a semigroup.
Moreover, the Cancellation Laws hold in a group.
Hence both $a$ and $b$ are cancellable.
We have $a^3 \circ b^2 = b^2 \circ a^3 = e \circ e = e$.
However $a \circ b \ne b \circ a$.
Hence the result by Proof by Counterexample.
{{qed}}
Category:Semigroups
Category:Commutativity
5mm0or7how3n76ul1oqe1k6fzc5bf1l
Theorem: Power of Product of Commutative Elements in Semigroup

:$\forall n \in \N_{>1}: \paren {x \circ y}^n = x^n \circ y^n \iff x \circ y = y \circ x$

Proof:
=== Necessary Condition ===
Let $x \circ y = y \circ x$.
Then by Power of Product of Commuting Elements in Semigroup equals Product of Powers:
:$\forall n \in \N_{>1}: \paren {x \circ y}^n = x^n \circ y^n$
{{qed|lemma}}
Theorem: Sum of Arcsecant and Arccosecant

Let $x \in \R$ be a real number such that $\size x \ge 1$.
Then:
: $\arcsec x + \arccsc x = \dfrac \pi 2$
where $\arcsec$ and $\arccsc$ denote arcsecant and arccosecant respectively.

Proof:
Let $y \in \R$ such that:
:$\exists x \in \R: \size x \ge 1$ and $x = \map \csc {y + \dfrac \pi 2}$
Then:
{{begin-eqn}}
{{eqn | l = x
      | r = \map \sec {y + \frac \pi 2}
      | c = 
}}
{{eqn | r = -\csc y
      | c = Secant of Angle plus Right Angle
}}
{{eqn | r = \map \csc {-y}
      | c = Cosecant Function is Odd
}}
{{end-eqn}}
Suppose $-\dfrac \pi 2 \le y \le \dfrac \pi 2$.
Then we can write:
:$-y = \arccsc x$
But then:
:$\map \csc {y + \dfrac \pi 2} = x$
Now because $-\dfrac \pi 2 \le y \le \dfrac \pi 2$ it follows that:
:$0 \le y + \dfrac \pi 2 \le \pi$
Hence:
:$y + \dfrac \pi 2 = \arcsec x$
That is:
:$\dfrac \pi 2 = \arcsec x + \arccsc x$
{{qed}}
Theorem: Equation of Straight Line Tangent to Circle

Let $\tuple {a, b}$ be the center of a circle $\CC$ whose radius is $r$.
Let $P_n = \tuple {x_n, y_n}$ be any point on $\CC$.
The equation of a non-vertical tangent line $\TT$ to $\CC$ is given by:
:$y - y_n = \dfrac {a - x_n} {y_n - b} \paren {x - x_n}$
The equations of the vertical tangent lines to $\CC$ are:
:$x = r - a$ for $P = \tuple {r - a, b}$
:$x = a - r$ for $P = \tuple {a - r, b}$

Proof:
=== Non-Vertical Tangent Lines ===
From Equation of Circle, $\CC$ can be described on the $x y$-plane in the form:
:$\paren {x - a}^2 + \paren {y - b}^2 = r^2$
where $P = \tuple {a, b}$ is the center of the circle and $r$ is the radius. 
We use the definition of the derivative as the gradient of the tangent line $\TT$.
Taking the derivative {{WRT|Differentiation}} $x$ of both sides of the equation we get:
{{begin-eqn}}
{{eqn | l = 2 \paren {x - a} + 2 \paren {y - b} \frac {\d y} {\d x}
      | r = 0
      | c = Derivative of Constant, Chain Rule for Derivatives, Power Rule for Derivatives
}}
{{eqn | ll= \leadsto
      | l = \frac {\d y} {\d x}
      | r = \frac {a - x} {y - b}
      | c =
}}
{{end-eqn}}
This is the slope at any point on $\CC$.
From the slope-intercept form of a line, the equation of such a line is:
:$y - y_n = m \paren {x - x_n}$
given any point $\paren {x_n, y_n}$ and the gradient $m$.
For $\TT$:
:$m = \valueat {\dfrac {\d y} {\d x} } {x \mathop = x_n, y \mathop = y_n}$
Thus the equation of $\TT$ is:
:$y - y_n = \dfrac {a - x_n} {y_n - b} \paren {x - x_n}$
{{qed|lemma}}
Theorem: Index Laws for Monoids/Negative Index

:$\forall n \in \Z: \paren {a^n}^{-1} = a^{-n} = \paren {a^{-1} }^n$

Proof:
We have $a^0 = e$ so it follows trivially that $a^{-0} = \paren {a^{-1} }^0$.
From the general inverse of product, we have:
:$\paren {a_1 \circ a_2 \circ \cdots \circ a_n}^{-1} = a_n^{-1} \circ \cdots \circ a_2^{-1} \circ a_1^{-1}$
where $a_1, a_2, \ldots, a_n \in S$ are all invertible for $\circ$.
Hence we have:
:$a_1, a_2, \ldots, a_n = a$
and we have that:
:$a^n$ is invertible for all $n \in \N$
:$\forall n \in \N: \paren {a^n}^{-1} = \paren {a^{-1} }^n$
From the above:
:$a^{-n} = \paren {a^{-1} }^n$
Thus:
{{begin-eqn}}
{{eqn | l = \paren {a^{-n} }^{-1}
      | r = \paren {\paren {a^{-1} }^n}^{-1}
      | c = 
}}
{{eqn | r = \paren {\paren {a^{-1} }^{-1} }^n
      | c = 
}}
{{eqn | r = a^{-\paren {-n} }
      | c = 
}}
{{end-eqn}}
Similarly, if $a$ is invertible then $a^{-1}$ is also invertible.
So we also have:
:$\circ^{-n} \paren {a^{-1} } = \circ^n \paren {\paren {a^{-1} }^{-1} }$
Thus:
{{begin-eqn}}
{{eqn | l = a^{-\paren {-n} }
      | r = \paren {\paren {a^{-1} }^{-1} }^n
      | c = 
}}
{{eqn | r = \paren {a^{-1} }^{-n}
      | c = 
}}
{{end-eqn}}
Thus the result holds for all $n \in \Z$.
{{qed}}
Theorem: Infinite Limit Theorem

Let $f$ be a real function of $x$ of the form 
:$\map f x = \dfrac {\map g x} {\map h x}$
Further, let $g$ and $h$ be continuous on some open interval $\mathbb I$, where $c$ is a constant in $\mathbb I$.
If:
:$(1): \quad \map g c \ne 0$
:$(2): \quad \map h c = 0$
:$(3): \quad \forall x \in \mathbb I: x \ne c \implies \map h x \ne 0$
then the limit of $f$ as $x \to c$ will not exist, and:
:$\ds \lim_{x \mathop \to c^+} \map f x = +\infty$ or $-\infty$
:$\ds \lim_{x \mathop \to c^-} \map f x = +\infty$ or $-\infty$

Proof:
To prove the claim, it will suffice to show that for each $N \in \R_{>0}$, one can find an $\epsilon > 0$ such that:
:$\size {x - c} < \epsilon \implies \size {\map f x} \ge N$
So fix $N \in \R_{>0}$.
First, by continuity of $g$, find an $\epsilon_1 > 0$ such that:
:$\size {x - c} < \epsilon_1 \implies \size {\map g x - \map g c} < \size {\dfrac {\map g c} 2}$
which by {{Corollary|Reverse Triangle Inequality/Real and Complex Fields|1|disp = Reverse Triangle Inequality}} implies that:
:$\size {x - c} < \epsilon_1 \implies \size {\map g c} - \size {\map g x} < \size {\dfrac {\map g c} 2}$
and by rearranging, this becomes:
:$\size {x - c} < \epsilon_1 \implies \size {\map g x} > \size {\dfrac {\map g c} 2}$
Next, by continuity of $h$, find an $\epsilon_2 > 0$ such that $\epsilon_1 > \epsilon_2$ and:
:$\size {x - c} < \epsilon_2 \implies \size {\map h x} < \dfrac {\size {\map g c} } {2 N}$
From Ordering of Reciprocals, this means:
:$\size {x - c} < \epsilon_2 \implies \dfrac 1 {\size {\map h x} } > \dfrac {2 N} {\size {\map g c} }$
These together imply that, whenever $0 < \size {x - c} < \epsilon_2$, we have:
{{begin-eqn}}
{{eqn | l = \size {\map f x}
      | r = \size {\frac {\map g x} {\map h x)} }
}}
{{eqn | r = \size {\map g x} \cdot \size {\frac 1 {\map h x} }
}}
{{eqn | o = >
      | r = \size {\frac {\map g c} 2} \cdot \frac 1 {\size {\map h x} }
      | c = since $\epsilon_2 < \epsilon_1$
}}
{{eqn | o = >
      | r = \size {\frac {\map g c} 2} \cdot \frac {2 N} {\size {\map g c} }
}}
{{eqn | r = N
}}
{{end-eqn}}
Thus $\epsilon_2$ is a valid choice for the sought $\epsilon$.
Hence the result.
{{qed}}
Theorem: Index Laws for Monoids/Product of Indices

:$\forall m, n \in \Z: a^{n m} = \paren {a^m}^n = \paren {a^n}^m$

Proof:
Let $m \in \N, c = a^m, d = \paren {a^{-1}}^m$.
We define the mapping $g_c: \Z \to S$ as:
:$\forall n \in \Z: \map {g_c} n = \map {\circ^n} c$
as defined in the proof of the Index Law for Sum of Indices.
Let $h: \Z \to \Z$ be the mapping defined as:
:$\forall z \in \Z: \map h z = z m$
Then:
{{begin-eqn}}
{{eqn | l = a^{n m}
      | r = \map {\paren {g_a \circ h} } n
}}
{{eqn | l = \paren {a^m}^n
      | r = \map {g_c} n
}}
{{end-eqn}}
By Index Law for Sum of Indices and Index Laws for Semigroup: Product of Indices, $g_a \circ h$ and $g_c$ are homomorphisms from $\Z$ to $S$ which coincide on $\N$.
So by the Extension Theorem for Homomorphisms:
:$g_a \circ h = g_c$
Therefore:
:$\forall n \in \Z, m \in \N: a^{n m} = \paren {a^m}^n$
Also:
{{begin-eqn}}
{{eqn | l = a^{n \paren {-m} }
      | r = a^{-\paren {n m} }
}}
{{eqn | r = \paren {a^{-1} }^{n m}
}}
{{eqn | r = \map {\paren {g_{a^{-1} } \circ h} } n
}}
{{end-eqn}}
and:
{{begin-eqn}}
{{eqn | l = \paren {a^{-m} }^n
      | r = \paren {\paren {a^{-1} }^m}^n
}}
{{eqn | r = \map {g_d} n
}}
{{end-eqn}}
So, by the same reasoning as before:
:$g_{a^{-1} } \circ h = g_d$
Therefore:
:$\forall n \in \Z, m \in \N: a^{n \paren {-m}} = \paren {a^{-m}}^n$
Thus:
:$\forall n, m \in \Z: a^{n m} = \paren {a^m}^n$
As $n m = m n$, the result follows.
{{qed}}
Theorem: Powers of Group Elements/Negative Index

:$\forall n \in \Z: \paren {g^n}^{-1} = g^{-n} = \paren {g^{-1} }^n$

Proof:
All elements of a group are invertible, so we can directly use the result from Index Laws for Monoids: Sum of Indices:
:$\forall n \in \Z: \paren {g^n}^{-1} = g^{-n} = \paren {g^{-1} }^n$
{{qed}}
Theorem: Powers of Group Elements/Sum of Indices

:$\forall m, n \in \Z: g^m \circ g^n = g^{m + n}$

Proof:
All elements of a group are invertible, so we can directly use the result from Index Laws for Monoids: Sum of Indices:
:$\forall m, n \in \Z: g^m \circ g^n = g^{m + n}$
{{qed}}
Theorem: Powers of Group Elements/Product of Indices

:$\forall m, n \in \Z: \paren {g^m}^n = g^{m n} = \paren {g^n}^m$

Proof:
All elements of a group are invertible, so we can directly use the result from Index Laws for Monoids: Product of Indices:
:$\forall m, n \in \Z: g^{m n} = \paren {g^m}^n = \paren {g^n}^m$
{{qed}}
Theorem: Group Element Commutes with Inverse

Let $\struct {G, \circ}$ be a group whose identity is $e$.
Let $x \in G$.
Then:
:$x \circ x^{-1} = x^{-1} \circ x$
That is, $x$ commutes with its inverse $x^{-1}$.

Proof:
By definition of inverse element:
:$x \circ x^{-1} = e = x^{-1} \circ x$
Hence the result by definition.
Theorem: Commutativity of Powers in Monoid

:$\forall m, n \in \Z: a^m \circ b^n = b^n \circ a^m$

Proof:
By Powers of Commuting Elements of Semigroup Commute, if $m > 0$ and $n > 0$ then $a^m$ commutes with $b^n$.
By Commutation with Inverse in Monoid, again if $m > 0$ and $n > 0$ then $a^m$ commutes with $\paren {b^n}^{-1} = b^{-n}$.
Similarly $b^n$ commutes with $a^{-m}$.
But as $a^{-m}$ commutes with $b^n$, it also commutes with $\paren {b^n}^{-1} = b^{-n}$, again by Commutation with Inverse in Monoid.
Hence the result.
{{qed}}
Theorem: Power of Product of Commutative Elements in Monoid

:$\forall n \in \Z: \paren {a \circ b}^n = a^n \circ b^n$

Proof:
From Power of Product of Commutative Elements in Semigroup, this result holds if $n \ge 0$.
Since $a$ and $b$ commute, then so do $a^{-1}$ and $b^{-1}$ by Commutation of Inverses in Monoid.
Hence, if $n > 0$:
{{begin-eqn}}
{{eqn | l = \paren {a \circ b}^{-n}
      | r = \paren {\paren {a \circ b}^{-1} }^n
}}
{{eqn | r = \paren {b^{-1} \circ a^{-1} }^n
      | c = Inverse of Product
}}
{{eqn | r = \paren {a^{-1} \circ b^{-1} }^n
      | c = Commutation of Inverses in Monoid
}}
{{eqn | r = \paren {a^{-1} }^n \circ \paren {b^{-1} }^n
      | c = 
}}
{{eqn | r = a^{-n} \circ b^{-n}
      | c = 
}}
{{end-eqn}}
The result follows.
{{qed}}
Theorem: Commutativity of Powers in Group

: $\forall m, n \in \Z: a^m \circ b^n = b^n \circ a^m$

Proof:
By definition, all elements of a group are invertible.
Therefore Commutativity of Powers in Monoid can be applied directly.
{{Qed}}
Category:Group Theory
Category:Commutativity
s8ogf503onvplgoz7ir9lu0b4wljf2f
Theorem: Power of Product of Commutative Elements in Group

:$a \circ b = b \circ a \iff \forall n \in \Z: \paren {a \circ b}^n = a^n \circ b^n$

Proof:
=== Necessary Condition ===
Let $a \circ b = b \circ a$.
By definition, all elements of a group are invertible.
Therefore the results in Power of Product of Commutative Elements in Monoid can be applied directly.
{{qed|lemma}}
Theorem: Primitive of Tangent Function/Cosine Form

:$\ds \int \tan x \rd x = -\ln \size {\cos x} + C$
where $\cos x \ne 0$.

Proof:
{{begin-eqn}}
{{eqn | l = \int \tan x \rd x
      | r = \int \frac {\sin x} {\cos x} \rd x
      | c = {{Defof|Real Tangent Function}}
}}
{{eqn | r = -\int \frac {-\sin x} {\cos x} \rd x
      | c = Primitive of Constant Multiple of Function
}}
{{eqn | r = -\int \frac {\paren {\cos x}'} {\cos x} \rd x
      | c = Derivative of Cosine Function
}}
{{eqn | r = -\ln \size {\cos x} + C
      | c = Primitive of Function under its Derivative
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Reciprocal

:$\ds \int \frac {\d x} x = \ln \size x + C$
for $x \ne 0$.

Proof:
{{begin-eqn}}
{{eqn | l = \map {\dfrac \d {\d x} } {\arctan x}
      | r = \dfrac 1 {1 + x^2}
      | c = Derivative of Arctangent Function
}}
{{eqn | ll= \leadsto
      | l = \int \dfrac {\d x} {1 + x^2} 
      | r = \arctan x + C
      | c = {{Defof|Primitive (Calculus)}}
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Reciprocal

:$\ds \int \frac {\d x} x = \ln \size x + C$
for $x \ne 0$.

Proof:
From Primitive of $\dfrac {x^m} {\ln x}$:
:$\ds \int \frac {x^m \rd x} {\ln x} = \map \ln {\ln x} + \paren {m + 1} \ln x + \sum_{k \mathop \ge 2}^n \frac {\paren {m + 1}^k \paren {\ln x}^k} {k \times k!} + C$
The result follows by setting $m = 0$.
{{qed}}
Theorem: Primitive of Reciprocal

:$\ds \int \frac {\d x} x = \ln \size x + C$
for $x \ne 0$.

Proof:
From Primitive of $\dfrac {1 + x^2} {1 + x^4}$, we have:
:$\ds \int \frac {x^2 + 1} {x^4 + 1} \rd x = \frac 1 {\sqrt 2} \map \arctan {\frac 1 {\sqrt 2} \paren {x - \frac 1 x} } + C$
From Primitive of $\dfrac {-1 + x^2} {1 + x^4}$, we have:
:$\ds \int \frac {x^2 - 1} {x^4 + 1} \rd x = \frac 1 {2 \sqrt 2} \ln \size {\frac {x^2 - \sqrt 2 x + 1} {x^2 + \sqrt 2 x + 1} } + C$
We therefore have: 
{{begin-eqn}}
{{eqn	| l = \int \frac 1 {1 + x^4} \rd x
	| r = \frac 1 2 \int \frac {x^2 + 1 - \paren {x^2 - 1} } {1 + x^4} \rd x
}}
{{eqn	| r = \frac 1 2 \paren {\int \frac {x^2 + 1} {x^4 + 1} \rd x - \int \frac {x^2 - 1} {x^4 + 1} \rd x}
}}
{{eqn	| r = \frac 1 {2 \sqrt 2} \paren {\map \arctan {\frac 1 {\sqrt 2} \paren {x - \frac 1 x} } - \frac 1 2 \ln \size {\frac {x^2 - \sqrt 2 x + 1} {x^2 + \sqrt 2 x + 1} } } + C
}}
{{eqn	| r = \frac 1 {2 \sqrt 2} \paren {\map \arctan {\frac 1 {\sqrt 2} \paren {x - \frac 1 x} } + \frac 1 2 \ln \size {\frac {x^2 + \sqrt 2 x + 1} {x^2 - \sqrt 2 x + 1} } } + C
	| c = Logarithm of Reciprocal
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Reciprocal

:$\ds \int \frac {\d x} x = \ln \size x + C$
for $x \ne 0$.

Proof:
A special case of Primitive of $\dfrac 1 {x^4 + a^4}$, setting $a = 1$.
{{begin-eqn}}
{{eqn | l = \int \frac {\d x} {x^4 + a^4}
      | r = \frac 1 {4 a^3 \sqrt 2} \map \ln {\frac {x^2 + a x \sqrt 2 + a^2} {x^2 - a x \sqrt 2 + a^2} } - \frac 1 {2 a^3 \sqrt 2} \paren {\map \arctan {1 - \frac {x \sqrt 2} a} - \map \arctan {1 + \frac {x \sqrt 2} a} } + C
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \int \frac {\d x} {1 + x^4}
      | r = \frac 1 {4 \sqrt 2} \map \ln {\frac {x^2 + x \sqrt 2 + 1} {x^2 - x \sqrt 2 + 1} } - \frac 1 {2 \sqrt 2} \paren {\map \arctan {1 - x \sqrt 2} - \map \arctan {1 + x \sqrt 2} } + C
      | c = 
}}
{{eqn | r = \frac 1 {2 \sqrt 2} \paren {\dfrac 1 2 \map \ln {\frac {x^2 + x \sqrt 2 + 1} {x^2 - x \sqrt 2 + 1} } - \paren {\map \arctan {1 - x \sqrt 2} - \map \arctan {1 + x \sqrt 2} } } + C
      | c = extracting factor
}}
{{eqn | r = \frac 1 {2 \sqrt 2} \paren {\dfrac 1 2 \map \ln {\frac {x^2 + x \sqrt 2 + 1} {x^2 - x \sqrt 2 + 1} } - \map \arctan {\dfrac {\paren {1 - x \sqrt 2} - \paren {1 + x \sqrt 2} } {1 + \paren {1 - x \sqrt 2} \paren {1 + x \sqrt 2} } } } + C
      | c = Difference of Arctangents
}}
{{eqn | r = \frac 1 {2 \sqrt 2} \paren {\dfrac 1 2 \map \ln {\frac {x^2 + x \sqrt 2 + 1} {x^2 - x \sqrt 2 + 1} } - \map \arctan {\dfrac {-2 x \sqrt 2} {1 + \paren {1 - 2 x^2} } } } + C
      | c = Difference of Two Squares
}}
{{eqn | r = \frac 1 {2 \sqrt 2} \paren {\dfrac 1 2 \map \ln {\frac {x^2 + x \sqrt 2 + 1} {x^2 - x \sqrt 2 + 1} } + \map \arctan {\sqrt 2 \dfrac x {1 - x^2} } } + C
      | c = Inverse Tangent is Odd Function
}}
{{eqn | r = \frac 1 {2 \sqrt 2} \paren {\dfrac 1 2 \map \ln {\frac {x^2 + x \sqrt 2 + 1} {x^2 - x \sqrt 2 + 1} } + \paren {\frac \pi 2 - \map \arctan {\frac 1 {\sqrt 2} \paren {\frac {1 - x^2} x} } } } + C
      | c = Sum of Arctangent and Arccotangent
}}
{{eqn | r = \frac 1 {2 \sqrt 2} \paren {\frac 1 2 \ln \size {\frac {x^2 + \sqrt 2 x + 1} {x^2 - \sqrt 2 x + 1} } + \map \arctan {\frac 1 {\sqrt 2} \paren {x - \frac 1 x} } } + C'
      | c = Arctangent is Odd Function, setting $C' = \dfrac \pi 2 + C$
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Reciprocal

:$\ds \int \frac {\d x} x = \ln \size x + C$
for $x \ne 0$.

Proof:
From Primitive of $\dfrac 1 {\sqrt {a^2 - x^2} }$: Arcsine Form:
:$\ds \int \frac {\d x} {\sqrt {a^2 - x^2} } = \arcsin \frac x a + C$
The result follows by setting $a = 1$.
{{Qed}}
Theorem: Primitive of Reciprocal

:$\ds \int \frac {\d x} x = \ln \size x + C$
for $x \ne 0$.

Proof:
{{begin-eqn}}
{{eqn | l = \map {\dfrac \d {\d x} } {\arcsin x}
      | r = \dfrac 1 {\sqrt {1 - x^2} }
      | c = Derivative of Arcsine Function
}}
{{eqn | ll= \leadsto
      | l = \int \dfrac {\d x} {\sqrt {1 - x^2} } 
      | r = \arcsin x + C
      | c = {{Defof|Primitive (Calculus)}}
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Reciprocal

:$\ds \int \frac {\d x} x = \ln \size x + C$
for $x \ne 0$.

Proof:
Let:
{{begin-eqn}}
{{eqn | l = x
      | r = a \cos^2 \theta + b \sin^2 \theta
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \dfrac {\d x} {\d \theta}
      | r = 2 a \cos \theta \paren {-\sin \theta} + 2 b \sin \theta \cos \theta
      | c = Chain Rule for Derivatives, Derivative of Cosine Function, Derivative of Sine Function
}}
{{eqn | n = 1
      | r = 2 \paren {b - a} \cos \theta \sin \theta
      | c = 
}}
{{end-eqn}}
Then we have:
{{begin-eqn}}
{{eqn | l = x
      | r = a \cos^2 \theta + b \sin^2 \theta
      | c = 
}}
{{eqn | r = a \paren {1 - \sin^2 \theta} + b \sin^2 \theta
      | c = Sum of Squares of Sine and Cosine
}}
{{eqn | n = 2
      | ll= \leadsto
      | l = a - x
      | r = \paren {a - b} \sin^2 \theta
      | c = after algebra
}}
{{end-eqn}}
and:
{{begin-eqn}}
{{eqn | l = x
      | r = a \cos^2 \theta + b \sin^2 \theta
      | c = 
}}
{{eqn | r = a \cos^2 \theta + b \paren {1 - \cos^2 \theta}
      | c = Sum of Squares of Sine and Cosine
}}
{{eqn | n = 3
      | ll= \leadsto
      | l = x - b
      | r = \paren {a - b} \cos^2 \theta
      | c = after algebra
}}
{{eqn | n = 4
      | ll= \leadsto
      | l = \dfrac {a - x} {x - b}
      | r = \dfrac {\paren {a - b} \sin^2 \theta} {\paren {a - b} \cos^2 \theta}
      | c = $(2)$ divided by $(3)$
}}
{{eqn | l = \dfrac {a - x} {x - b}
      | r = \tan^2 \theta
      | c = {{Defof|Real Tangent Function}}
}}
{{end-eqn}}
Hence:
{{begin-eqn}}
{{eqn | l = \int \dfrac {\d x} {\paren {a - x}^{1/2} \paren {x - b}^{3/2} }
      | r = \int \dfrac {2 \paren {b - a} \cos \theta \sin \theta \rd \theta} {\paren {a - b}^{1/2} \sin \theta \paren {a - b}^{3/2} \cos \theta}
      | c = substituting from $(1)$, $(2)$ and $(3)$
}}
{{eqn | r = \dfrac 2 {b - a} \int \sec^2 \theta \rd \theta
      | c = simplification, and {{Defof|Real Secant Function}}
}}
{{eqn | r = \dfrac 2 {b - a} \tan \theta + C
      | c = Primitive of Square of Secant Function
}}
{{eqn | r = \dfrac 2 {b - a} \sqrt {\dfrac {a - x} {x - b} } + C
      | c = substituting from $(4)$
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Reciprocal

:$\ds \int \frac {\d x} x = \ln \size x + C$
for $x \ne 0$.

Proof:
{{begin-eqn}}
{{eqn | l = \int \dfrac {\d x} {\sqrt {2 + 4 x - 3 x^2} }
      | r = \dfrac 1 {\sqrt 3} \int \dfrac {\d x} {\sqrt {\frac 2 3 + \frac 4 3 x - x^2} }
      | c = 
}}
{{eqn | r = \dfrac 1 {\sqrt 3} \int \dfrac {\d x} {\sqrt {\frac {10} 9 - \paren {x - \frac 2 3}^2} }
      | c = Completing the Square
}}
{{eqn | r = \dfrac 1 {\sqrt 3} \map \arcsin {\dfrac {x - \frac 2 3} {\sqrt {\frac {10} 9} } } + C
      | c = Primitive of $\dfrac 1 {\sqrt {a^2 - x^2} }$
}}
{{eqn | r = \dfrac 1 {\sqrt 3} \map \arcsin {\dfrac {3 x - 2} {\sqrt {10} } } + C
      | c = simplifying
}}
{{end-eqn}}
{{qed}}