nyuuzyou/wikis huggingface dataset:
Leibniz's Formula for Pi/Leibniz's Proof

== Theorem ==
== Proof ==
:
The area $OAT$ is a quarter-circle whose area is $\dfrac \pi 4$ by Area of Circle.
Now consider the area $C$ of the segment $OPQT$, bounded by the arc $OT$ and the chord $OT$.
Consider the area $OPQ$, bounded by the line segments $OP$ and $OQ$ and the arc $PQ$.
As $P$ and $Q$ approach each other, the arc $PQ$ tends towards the straight line segment $\d s = PQ$.
We can therefore consider the area $OPQ$ as a triangle.
We extend the line segment $PQ$ and drop a perpendicular $OR$ to $O$.
Using Area of Triangle in Terms of Side and Altitude, we see that the area $\d C$ of $\triangle OPQ$ is given by:
:$\d C = \triangle OPQ = \dfrac {OR \cdot PQ} 2 = \dfrac {OR \cdot \d s} 2$
We also note from elementary Euclidean geometry that $\triangle ORS$ is similar to the small triangle on $PQ$.
Thus:
:$\dfrac {\d s} {\d x} = \dfrac {OS} {OR} \iff OR \cdot \d s = OS \cdot \d x$
Thus:
:$\d C = \dfrac {OS \cdot \d x} 2 = \dfrac {y \rd x} 2$
where $y = OS$.
We set the horizontal coordinate of $P$ as equal to $x$.
Thus the total area $C$ is equal to the total of all the areas of these small triangles as $x$ increases from $0$ to $1$.
So:
:$\ds C = \int \rd C = \frac 1 2 \int_0^1 y \rd x$
Now we use Integration by Parts to swap $x$ and $y$:
:$\ds C = \intlimits {\frac 1 2 x y} 0 1 - \frac 1 2 \int_0^1 x \rd y = \frac 1 2 - \frac 1 2 \int_0^1 x \rd y$
It can be seen that the limits on this new integral have to be $0$ and $1$ from the geometry of the situation.
Now we note that:
:$y = \tan \dfrac \phi 2$
From :
:$x = 1 - \cos \phi = 2 \sin^2 \dfrac \phi 2$
Thus:
and so:
:$\dfrac x 2 = \dfrac {y^2} {1 + y^2}$
Using Sum of Infinite Geometric Sequence:
:$\dfrac {y^2} {1 + y^2} = y^2 - y^4 + y^6 - y^8 + \cdots$
This gives us:
Remember, $C$ is the area of the segment $OPQT$.
Now we add to it the area of $\triangle OTA$, which trivially equals $\dfrac 1 2$, to get the area of the quarter circle which we know as equal to $\dfrac \pi 4$.
Putting it all together, this gives us:
:$\dfrac \pi 4 = 1 - \dfrac 1 3 + \dfrac 1 5 - \dfrac 1 7 + \dfrac 1 9 - \cdots$
== Sources ==
* : Chapter $\text {B}.13$: How Leibniz Discovered his Formula $\pi / 4 = 1 - \frac 1 3 + \frac 1 5 - \frac 1 7 + \cdots$
Category:Leibniz's Formula for Pi
Category:Formulas for Pi
Leibniz's Formula for Pi/Lemma

== Lemma ==
This holds for all real $t \in \R$.
== Proof ==
From Square of Real Number is Non-Negative, we have that:
:$t^2 \ge 0$
for all real $t$.
So $- t^2 \le 0$ and so $- t^2 \ne 1$.
So the conditions of Sum of Geometric Sequence are satisfied, and so the above argument holds for all real $t$.
Category:Analysis
Leibniz's Formula for Pi/Proof by Dirichlet Beta Function

== Theorem ==
== Proof ==
Recall the Dirichlet beta function:
:$\ds \map \beta s = \sum_{n \mathop = 0}^\infty \frac {\paren {-1}^n} {\paren {2 n + 1}^s}$
From Dirichlet Beta Function at Odd Positive Integers, we obtain:
:$\map \beta {2 n + 1} = \paren {-1}^n \dfrac {E_{2 n} \pi^{2 n + 1} } {4^{n + 1} \paren {2 n}!}$
Therefore, setting $n = 0$ above:
Category:Leibniz's Formula for Pi
Category:Formulas for Pi
Leibniz's Formula for Pi/Proof by Taylor Expansion

== Theorem ==
== Proof ==
From Power Series Expansion for Real Arctangent Function, we obtain:
:$\arctan x = x - \dfrac {x^3} 3 + \dfrac {x^5} 5 - \dfrac {x^7} 7 + \dfrac {x^9} 9 - \cdots$
Substituting $x = 1$ gives the required result.
Category:Leibniz's Formula for Pi
Category:Formulas for Pi
Leibniz's Integral Rule

== Theorem == 
Let $\map f {x, t}$, $\map a t$, $\map b t$ be continuously differentiable real functions on some region $R$ of the $\tuple {x, t}$ plane.
Then for all $\tuple {x, t} \in R$:
:$\ds \frac \d {\d t} \int_{\map a t}^{\map b t} \map f {x, t} \rd x = \map f {\map b t, t} \frac {\d b} {\d t} - \map f {\map a t, t} \frac {\d a} {\d t} + \int_{\map a t}^{\map b t} \frac \partial {\partial t} \map f {x, t} \rd x$
== Proof == 
By the Mean Value Theorem for Integrals, there exist $\xi_a \in \closedint {\map a t} {\map a {t + h} }$ and $\xi_b \in \closedint {\map b t} {\map b {t + h} }$ such that:
Now, consider the last term:
:$\ds \lim_{h \mathop \to 0} \int_{\map a t}^{\map b t} \frac {\map f {x, t + h} - \map f {x, t} } h \rd x$
By Limit of Function by Convergent Sequences, it suffices to find the following for an arbitrary sequence $\sequence {h_n}_{n \mathop \in \N}$ such that $\ds \lim_{n \mathop \to \infty} h_n = 0$:
:$\ds \lim_{n \mathop \to 0} \int_{\map a t}^{\map b t} \frac {\map f {x, t + h_n} - \map f {x, t} } {h_n} \rd x$
Fix such as sequence, as well as a value for $t$.
For each $n \in \N$, define a function $\map {f_n} x$ as:
:$\map {f_n} x = \frac {\map f {x, t + h_n} - \map f {x, t} } {h_n}$
when $\tuple {x, t}$ and $\tuple {x, t + h_n}$ are in $R$.
By the Extreme Value Theorem:
:$M = \sup_{\tuple x \in R_t} \size {\frac \partial {\partial t} \map f {x, t} }$
is well-defined, where $R_t$ is the subset of $R$ where $t$ matches our chosen value.
Then, from the Mean Value Theorem, it follows that:
:$\size {\map {f_n} x} \le M$
for all values of $n$ and $x$.
By Limit of Function by Convergent Sequences, as $n \to \infty$:
:$\ds \map {f_n} x \to \lim_{h \mathop \to 0} \frac {\map f {x, t + h} - \map f {x, t} } h = \frac \partial {\partial t} \map f {x, t}$
by definition of Partial Derivative.
Therefore, by Lebesgue's Dominated Convergence Theorem:
:$\ds \lim_{n \mathop \to 0} \int_{\map a t}^{\map b t} \frac {\map f {x, t + h_n} - \map f {x, t} } {h_n} \rd x = \int_{\map a t}^{\map b t} \frac \partial {\partial t} \map f {x, t} \rd x$
Combining with the result from before:
:$\ds \frac \d {\d t} \int_{\map a t}^{\map b t} \map f {x, t} \rd x = \frac {\d b} {\d t} \map f {\map b t, t} - \frac {\d a} {\d t} \map f {\map a t, t} + \int_{\map a t}^{\map b t} \frac \partial {\partial t} \map f {x, t} \rd x$
== Also known as ==
== Also see ==
* Definite Integral of Partial Derivative, where $\map a t$ and $\map b t$ are constant: 
:$\ds \frac {\rd} {\rd t} \int_a^b \map f {x, t} \rd x = \int_a^b \frac {\partial} {\partial t} \map f {x, t} \rd x$
 
== Sources ==
* : $3$: Elementary Analytic Methods: $3.3$ Rules for Differentiation and Integration: Leibniz's Theorem for Differentiation of an Integral: $3.3.7$
* : $\S 15$: Leibnitz's Rule for Differentiation of Integrals: $15.14$
* : $\S 18$: Definite Integrals: Leibnitz's Rules for Differentiation of Integrals: $18.14$
* 
Category:Leibniz's Integral Rule
Category:Definite Integrals
Leibniz's Integral Rule/Also known as

== Leibniz's Integral Rule: Also known as == 
Leibniz's Integral Rule is also referred to in some sources as Leibniz's Rule, but as this name is also used for a different result, it is necessary to distinguish between the two. 
Other popular names for this technique include:
:differentiation under the integral sign
:Feynman's technique after physicist .
Some sources refer to Leibnitz's Rule for Differentiation of Integrals or Leibnitz's Rule for Differentiation of an Integral or some such.
== Sources ==
* : $3$: Elementary Analytic Methods: $3.3$ Rules for Differentiation and Integration: Leibniz's Theorem for Differentiation of an Integral: $3.3.7$
* : $\S 15$: Leibnitz's Rule for Differentiation of Integrals
* : $\S 18$: Definite Integrals: Leibnitz's Rules for Differentiation of Integrals
Category:Leibniz's Integral Rule
Leibniz's Integral Rule/Mistake/First Edition

== Source Work ==
:
:$\S 15$: Definite Integrals
::Leibnitz's Rule for Differentiation of Integrals
== Mistake ==
:Leibnitz's Rule for Differentiation of Integrals
== Correction ==
The name is , not Leibnitz.
== Sources ==
* : $\S 15$: Leibnitz's Rule for Differentiation of Integrals
Category:Mistakes/Mathematical Handbook of Formulas and Tables
Leibniz's Integral Rule/Mistake/Third Edition

== Source Work ==
:
:$\S 18$: Definite Integrals
::Leibnitz's Rules for Differentiation of Integrals
== Mistake ==
:Leibnitz's Rules for Differentiation of Integrals
== Correction ==
The name is , not Leibnitz.
== Sources ==
* : $\S 18$: Definite Integrals: Leibnitz's Rules for Differentiation of Integrals
Category:Mistakes/Mathematical Handbook of Formulas and Tables
Leibniz's Law for Sets

== Theorem ==
Let $S$ be an arbitrary set.
Then:
:$x = y \dashv \vdash x \in S \iff y \in S$
for all $S$ in the universe of discourse.
This is therefore the justification behind the notion of the definition of set equality.
== Proof ==
A direct application of Leibniz's law.
== Also see ==
* Axiom:Axiom of Extensionality
== Sources ==
* : $\S 4.21$
* 
Category:Set Theory
Leibniz's Rule/One Variable

== Theorem ==
Let $f$ and $g$ be real functions defined on the open interval $I$.
Let $n \in \Z_{>0}$ be a (strictly) positive integer.
Let $x \in I$ be a point in $I$ at which both $f$ and $g$ are $n$ times differentiable.
Then:
:$\ds \paren {\map f x \map g x}^{\paren n} = \sum_{k \mathop = 0}^n \binom n k \map {f^{\paren k} } x \map {g^{\paren {n - k} } } x$
where $\paren n$ denotes the order of the derivative.
== Proof ==
Proof by induction:
=== Basis for the Induction ===
Let $n = 1$.
From Product Rule for Derivatives:
:$\paren {\map f x \map g x}' = \map f x \map {g'} x + \map {f'} x \map g x$
Likewise:
This is our basis for the induction.
=== Induction Hypothesis ===
Let $n \in \N$ be fixed.
We assume the inductive hypothesis:
:$\ds \paren {\map f x \map g x}^{\paren n} = \sum_{k \mathop = 0}^n \binom n k \map {f^{\paren k} } x \map {g^{\paren {n - k} } } x$
We need to show that:
:$\ds \paren {\map f x \map g x}^{\paren {n + 1} } = \sum_{k \mathop = 0}^{n + 1} \binom {n + 1} k \map {f^{\paren k} } x \map {g^{\paren {n + 1 - k} } } x$
=== Induction Step ===
By our inductive hypothesis:
Subsequently, we separate the $k = 0$ case from the second summation. 
For the first summation, we separate the case $k = n$ and then shift the indices up by $1$.
These manipulations give us the following:
By Pascal's Rule, we finally obtain:
The result follows by the Principle of Mathematical Induction.
== Also presented as ==
== Also known as ==
== Special Cases ==
=== Second Derivative ===
=== Third Derivative ===
== Examples ==
== Sources ==
* : $3$: Elementary Analytic Methods: $3.3$ Rules for Differentiation and Integration: Leibniz's Theorem for Differentiation of a Product: $3.3.8$
* : $\S 13$: Leibnitz's Rule for Higher Derivatives of Products: $13.46$
* : $4.$ Mathematics: $4.4$ Differential calculus: $\text {(ii)}$ Leibniz's rule
* : $\S 10.11 \ (6)$
* 
* 
* 
* 
Category:Leibniz's Rule
Leibniz's Rule/One Variable/Examples/8th Derivative of x^2 sin x

== Example of Use of Leibniz's Rule in One Variable ==
The $8$th derivative $x$ of $x^2 \sin x$ is given by:
:$\dfrac {\d^8} {\d x^8} x^2 \sin x = x^2 \sin x - 16 x \cos x - 56 \sin x$
== Proof ==
Leibniz's Rule in One Variable gives:
:$\ds \paren {\map f x \, \map g x}^{\paren n} = \sum_{k \mathop = 0}^n \binom n k \map {f^{\paren k} } x \, \map {g^{\paren {n - k} } } x$
where $\paren n$ denotes the order of the derivative.
Here we take:
:$\map f x = x^2$
:$\map g x = \sin x$
We note that:
and for all $n > 2$:
:$\dfrac {\d^n f} {d x^n} = 0$
Hence we need investigate only $\dfrac {\d^n g} {d x^n}$ where $n \in \set {6, 7, 8}$.
Thus:
Hence:
== Sources ==
* 
Category:Leibniz's Rule
Leibniz's Rule/One Variable/Second Derivative

== Theorem ==
Let $f$ and $g$ be real functions defined on the open interval $I$.
Let $x \in I$ be a point in $I$ at which both $f$ and $g$ are twice differentiable.
Then:
:$\paren {\map f x \map g x}' ' = \map f x \map {g' '} x + 2 \map {f'} x \map {g'} x + \map {f' '} x \map g x$
== Proof ==
From Leibniz's Rule in One Variable:
:$\ds \paren {\map f x \map g x}^{\paren n} = \sum_{k \mathop = 0}^n \binom n k \map {f^{\paren k} } x \map {g^{\paren {n - k} } } x$
where $\paren n$ denotes the order of the derivative.
Setting $n = 2$:
== Sources ==
* : $\S 13$: Leibnitz's Rule for Higher Derivatives of Products: $13.47$
* 
* 
Category:Leibniz's Rule
Leibniz's Rule/One Variable/Third Derivative

== Theorem ==
Let $f$ and $g$ be real functions defined on the open interval $I$.
Let $x \in I$ be a point in $I$ at which both $f$ and $g$ are thrice differentiable.
Then:
:$\paren {\map f x \map g x}' ' ' = \map f x \map {g' ' '} x + 3 \map {f'} x \map {g' '} x + 3 \map {f' '} x \map {g'} x + \map {f' ' '} x \map g x$
== Proof ==
From Leibniz's Rule in One Variable:
:$\ds \paren {\map f x \map g x}^{\paren n} = \sum_{k \mathop = 0}^n \binom n k \map {f^{\paren k} } x \map {g^{\paren {n - k} } } x$
where $\paren n$ denotes the order of the derivative.
Setting $n = 3$:
== Sources ==
* : $\S 13$: Leibnitz's Rule for Higher Derivatives of Products: $13.48$
Category:Leibniz's Rule
Leibniz's Rule in One Variable/Also presented as

== Leibniz's Rule in One Variable: Also presented as ==
Leibniz's Rule in One Variable can often be seen presented in this format:
== Sources ==
* : $3$: Elementary Analytic Methods: $3.3$ Rules for Differentiation and Integration: Leibniz's Theorem for Differentiation of a Product: $3.3.8$
Category:Leibniz's Rule
Lemmata for Euler's Third Substitution

== Theorem ==
Let Euler's third substitution be employed in order to evaluate a primitive of the form:
:$\ds \map R {x, \sqrt {a x^2 + b x + c} } \rd x$
where $R$ is a rational function of $x$ and $\sqrt {a x^2 + b x + c}$.
Thus:
:$\ds \sqrt {a x^2 + b x + c} = \sqrt {a \paren {x - \alpha} \paren {x - \beta} } = \paren {x - \alpha} t$
Then we have:
=== Lemma $1$ ===
=== Lemma $2$ ===
=== Lemma $3$ ===
=== Lemma $4$ ===
</onlyinclude>
== Also see ==
* Definition:Euler's Third Substitution
Category:Euler Substitutions
Lemmata for Euler's Third Substitution/Lemma 1

== Theorem ==
Let Euler's third substitution be employed in order to evaluate a primitive of the form:
:$\ds \map R {x, \sqrt {a x^2 + b x + c} } \rd x$
where $R$ is a rational function of $x$ and $\sqrt {a x^2 + b x + c}$.
Thus:
:$\ds \sqrt {a x^2 + b x + c} = \sqrt {a \paren {x - \alpha} \paren {x - \beta} } = \paren {x - \alpha} t$
Then we have:
:$x = \dfrac {a \beta - \alpha t^2} {a - t^2}$
== Proof ==
== Also see ==
* Definition:Euler's Third Substitution
Category:Euler Substitutions
Lemmata for Euler's Third Substitution/Lemma 2

== Theorem ==
Let Euler's third substitution be employed in order to evaluate a primitive of the form:
:$\ds \map R {x, \sqrt {a x^2 + b x + c} } \rd x$
where $R$ is a rational function of $x$ and $\sqrt {a x^2 + b x + c}$.
Thus:
:$\ds \sqrt {a x^2 + b x + c} = \sqrt {a \paren {x - \alpha} \paren {x - \beta} } = \paren {x - \alpha} t$
Then we have:
:$x - \alpha = \dfrac {a \paren {\alpha - \beta} } {t^2 - a}$
== Proof ==
== Also see ==
* Definition:Euler's Third Substitution
Category:Euler Substitutions
Lemmata for Euler's Third Substitution/Lemma 3

== Theorem ==
Let Euler's third substitution be employed in order to evaluate a primitive of the form:
:$\ds \map R {x, \sqrt {a x^2 + b x + c} } \rd x$
where $R$ is a rational function of $x$ and $\sqrt {a x^2 + b x + c}$.
Thus:
:$\ds \sqrt {a x^2 + b x + c} = \sqrt {a \paren {x - \alpha} \paren {x - \beta} } = \paren {x - \alpha} t$
Then we have:
:$\dfrac {\d x} {\d t} = \dfrac {2 t a \paren {\beta - \alpha} } {\paren {a - t^2}^2}$
== Proof ==
== Also see ==
* Definition:Euler's Third Substitution
Category:Euler Substitutions
Lemmata for Euler's Third Substitution/Lemma 4

== Theorem ==
Let Euler's third substitution be employed in order to evaluate a primitive of the form:
:$\ds \map R {x, \sqrt {a x^2 + b x + c} } \rd x$
where $R$ is a rational function of $x$ and $\sqrt {a x^2 + b x + c}$.
Thus:
:$\ds \sqrt {a x^2 + b x + c} = \sqrt {a \paren {x - \alpha} \paren {x - \beta} } = \paren {x - \alpha} t$
Then we have:
:$t = \pm \sqrt {\dfrac {a \paren {x - \beta} } {x - \alpha} }$
== Proof ==
== Also see ==
* Definition:Euler's Third Substitution
Category:Euler Substitutions
Lemniscate of Bernoulli as Locus in Complex Plane

== Theorem ==
The locus of $z$ on the complex plane such that:
:$\cmod {z - a} \cmod {z + a} = a^2$
is a lemniscate of Bernoulli.
== Proof ==
which is the equation defining a lemniscate of Bernoulli with major semiaxis $a \sqrt 2$.
== Sources ==
* : $1$: Complex Numbers: Supplementary Problems: Miscellaneous Problems: $141$
Category:Analytic Geometry
Category:Geometry of Complex Plane
Lemniscate of Bernoulli from Tangents to Rectangular Hyperbola

== Theorem ==
Let $\KK$ be a rectangular hyperbola.
Let $\LL$ be the locus of the foot of the perpendicular from the origin to the tangents to $\KK$.
Then $\LL$ is the lemniscate of Bernoulli.
== Proof ==
:
== Sources ==
* 
* 
Category:Lemniscate of Bernoulli
Category:Rectangular Hyperbolas
Lemniscate of Bernoulli is Special Case of Ovals of Cassini

== Theorem ==
The lemniscate of Bernoulli is a special case of the ovals of Cassini.
=== Proof from Geometric Definition ===
=== Proof from Cartesian Definition ===
=== Proof from Polar Definition ===
== Sources ==
* : $\S 11$: Special Plane Curves: Ovals of Cassini: $11.31$
* 
* 
* : $\S 9$: Special Plane Curves: Ovals of Cassini: $9.31.$
* 
* 
Category:Lemniscate of Bernoulli is Special Case of Ovals of Cassini
Category:Lemniscate of Bernoulli
Category:Ovals of Cassini
Lemniscate of Bernoulli is Special Case of Ovals of Cassini/Cartesian Proof

== Theorem ==
== Proof ==
The ovals of Cassini can be defined by a Cartesian equation as follows:
The lemniscate of Bernoulli can be defined by a Cartesian equation as follows:
Setting $b = a$:
It follows that the lemniscate of Bernoulli is an oval of Cassini where $b = a$.
Category:Lemniscate of Bernoulli is Special Case of Ovals of Cassini
Lemniscate of Bernoulli is Special Case of Ovals of Cassini/Geometric Proof

== Theorem ==
== Proof ==
The ovals of Cassini are defined as follows:
The lemniscate of Bernoulli is defined geometrically as:
It follows that the lemniscate of Bernoulli is an oval of Cassini where $b = a$.
Category:Lemniscate of Bernoulli is Special Case of Ovals of Cassini
Lemniscate of Bernoulli is Special Case of Ovals of Cassini/Polar Proof

== Theorem ==
== Proof ==
The ovals of Cassini can be defined by a polar equation as follows:
The lemniscate of Bernoulli can be defined by a polar equation as follows:
Setting $b = a$:
It follows that the lemniscate of Bernoulli is an oval of Cassini where $b = a$.
Category:Lemniscate of Bernoulli is Special Case of Ovals of Cassini
Lemoine's Conjecture

== Conjecture ==
Every odd integer $n$ such that $n > 5$ can be written as:
:$2 p_1 + p_2$
where $p_1 \le p_2$ and both $p_1$ and $p_2$ are prime.
== Also known as ==
* Levy's Conjecture, for 
== Also see ==
* Goldbach Conjecture
== Sources ==
* 
* 
::p. 46: In fact, Hardy and Littlewood [4] listed as their Conjecture I: Every large odd number $n$ is the sum of a prime and the double of a prime.
Category:Unproven Hypotheses
Length Function is Primitive Recursive

== Theorem ==
Let $n \in \N$.
Let $\map \len n$ denote the length of $n$.
Then the function $\len: \N \to \N$ is primitive recursive.
== Proof ==
Clearly $\map \len 0 = 0$.
For $n > 0$, we have:
:$\ds \map \len n = \sum_{y \mathop = 1}^n \map {\operatorname {div} } {n, \map p y}$
where:
:$\map {\operatorname {div} } {n, m}$ is defined as:
::$\map {\operatorname {div} } {n, y} = \begin{cases}
1 & : y \divides n \\
0 & : y \nmid n
\end{cases}$
:$\map p y$ is the $y$th prime number.
Let $g: \N^2 \to \N$ be the function defined by:
:$\ds \map g {n, z} = \begin{cases}
0 & : z = 0 \\
\ds \sum_{y \mathop = 1}^z \map {\operatorname {div} } {n, \map p y} & : z > 0
\end{cases}$
We have that:
:$\operatorname{div}$ is primitive recursive
:$p: \N \to \N$ is primitive recursive
:Bounded Summation is Primitive Recursive.
So it follows that $g$ is also primitive recursive.
Finally, as $\map \len n = \map g {n, n}$ it follows that $\len$ is primitive recursive.
Category:Primitive Recursive Functions
Length of Abelian Group

== Theorem ==
Let $G$ be an abelian group whose order is $n$.
Let $n$ have the prime decomposition:
:$\ds n = \prod_{i \mathop = 1}^r p_i^{k_i} = p_1^{k_1} p_2^{k_2} \cdots p_r^{k_r}$
where $p_1 < p_2 < \cdots < p_r$ are distinct primes and $k_1, k_2, \ldots, k_r$ are positive integers.
Then the length of $G$ is given by:
:$\ds \map l G = \sum_{i \mathop = 1}^r k_i = k_1 + k_2 + \cdots + k_r$
== Proof ==
== Sources ==
* : Chapter $2$: Normal and Composition Series: $\S 73 \gamma$
Category:Abelian Groups
Length of Angle Bisector

== Theorem ==
Let $\triangle ABC$ be a triangle.
Let $AD$ be the angle bisector of $\angle BAC$ in $\triangle ABC$.
:
Let $d$ be the length of $AD$.
Then $d$ is given by:
:$d^2 = \dfrac {b c} {\paren {b + c}^2} \paren {\paren {b + c}^2 - a^2}$
where $a$, $b$, and $c$ are the sides opposite $A$, $B$ and $C$ respectively.
== Proof 1 ==
== Proof 2 ==
Category:Length of Angle Bisector
Category:Triangles
Category:Angle Bisectors
Length of Angle Bisector/Proof 1

== Theorem ==
== Proof ==
Similarly, or by symmetry, we get:
:$BD = \dfrac {a c} {b + c}$
From Stewart's Theorem, we have:
:$b^2 \cdot BD + c^2 \cdot DC = d^2 \cdot a + BD \cdot DC \cdot a$
Substituting the above expressions for $BD$ and $DC$:
Category:Length of Angle Bisector
Length of Angle Bisector/Proof 2

== Theorem ==
== Proof ==
:
From Length of Angle Bisector: Proof 1, we have:
:$BD = \dfrac {a c} {b + c}$
:$DC = \dfrac {a b} {b + c}$
Then we have:
Then from Triangles with Two Equal Angles are Similar we have:
:$\triangle ABD \sim \triangle AFC$
So:
Now we use the Intersecting Chords Theorem, which gives us $BD \cdot DC = d \cdot DF$.
Category:Length of Angle Bisector
Length of Angle Bisector in terms of Angle

== Theorem ==
Let $\triangle ABC$ be a triangle with sides $a$, $b$ and $c$ opposite vertices $A$, $B$ and $C$ respectively.
Let $AD$ be the angle bisector of $\angle BAC$ that intersects $a$ at $D$.
:
Then:
:$AD = \dfrac {2 c b \cos \frac A 2} {b + c}$
== Proof ==
Then:
== Sources ==
* : $\text V$. Trigonometry: The angle bisector
Category:Length of Angle Bisector
Category:Triangles
Category:Angle Bisectors
Length of Arc of Astroid

== Theorem ==
The total length of the arcs of an astroid constructed within a deferent of radius $a$ is given by:
:$\LL = 6 a$
== Proof ==
Let $H$ be embedded in a cartesian plane with its center at the origin and its cusps positioned on the axes.
:
We have that $\LL$ is $4$ times the length of one arc of the astroid.
From Arc Length for Parametric Equations:
:$\ds \LL = 4 \int_{\theta \mathop = 0}^{\theta \mathop = \pi/2} \sqrt {\paren {\frac {\d x} {\d \theta} }^2 + \paren {\frac {\d y} {\d \theta} }^2} \rd \theta$
where, from Equation of Astroid:
:$\begin{cases}
x & = a \cos^3 \theta \\
y & = a \sin^3 \theta
\end{cases}$
We have:
Thus:
Thus:
== Sources ==
* : $\S 11$: Special Plane Curves: Hypocycloid with Four Cusps: $11.11$
* : Chapter $\text {B}.21$: The Cycloid: Problem $7$
* : $\S 9$: Special Plane Curves: Hypocycloid with Four Cusps: $9.11.$
Category:Astroids
Length of Arc of Cycloid

== Theorem ==
Let $C$ be a cycloid generated by the equations:
:$x = a \paren {\theta - \sin \theta}$
:$y = a \paren {1 - \cos \theta}$
Then the length of one arc of the cycloid is $8 a$.
== Proof 1 ==
== Proof 2 ==
== Also see ==
* Area under Arc of Cycloid
== Historical Note ==
== Sources ==
* : Solutions: $209$. -- A Wheel Fallacy
* : Answers: $293$. A Wheel Fallacy
* : $\S 11$: Special Plane Curves: Cycloid: $11.6$
* : $1$: The Nature of Differential Equations: $\S 6$: The Brachistochrone. Fermat and the Bernoullis
* : $\S 9$: Special Plane Curves: Cycloid: $9.7.$
Category:Cycloids
Category:Length of Arc of Cycloid
Length of Arc of Cycloid/Historical Note

== Historical Note on Length of Arc of Cycloid ==
The geometric proof of the length of the arc of a cycloid was demonstrated by in $1658$.
== Sources ==
* : Chapter $\text{V}$: "Greatness and Misery of Man"
* : Chapter $\text {A}.15$: Torricelli ()
* : Chapter $\text {B}.21$: The Cycloid
* 
* 
Category:Historical Notes