avewright/proofwiki-math huggingface dataset:
Theorem: Primitive of Power

Let $n \in \R: n \ne -1$.
Then:
:$\ds \int x^n \rd x = \frac {x^{n + 1} } {n + 1} + C$
where $C$ is an arbitrary constant.

Proof:
Let $s \in \Z$. 
{{begin-eqn}}
{{eqn | l = v
      | r = x^s
      | c = 
}}
{{eqn | n = 1
      | ll= \leadsto
      | l = \frac {\d v} {\d x}
      | r = s x^{s - 1}
      | c = Power Rule for Derivatives
}}
{{end-eqn}}
Let $u \dfrac {\d v} {\d x} = x^m \paren {a x + b}^n$.
Then:
{{begin-eqn}}
{{eqn | l = u
      | r = \frac {x^m \paren {a x + b}^n} {s x^{s - 1} }
      | c = from $(1)$
}}
{{eqn | r = \frac {x^{m - s + 1} \paren {a x + b}^n} s
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \frac {\d u} {\d x}
      | r = \frac {x^{m - s + 1} a n \paren {a x + b}^{n - 1} } s + \frac {\paren {m - s + 1} x^{m - s} \paren {a x + b}^n} s
      | c = Primitive of Power of $a x + b$ and Product Rule for Derivatives
}}
{{eqn | r = \frac {x^{m - s} } s \paren {a x + b}^{n - 1} \paren {a n x + \paren {m - s + 1} \paren {a x + b} }
      | c = extracting $\dfrac {x^{m - s} \paren {a x + b}^n} s$ as a factor
}}
{{eqn | r = \frac {x^{m - s} } s \paren {a x + b}^{n - 1} \paren {a n x + a m x - a s x + a x + m b - s b + b}
      | c = multiplying out
}}
{{eqn | n = 2
      | r = \frac {x^{m - s} } s \paren {a x + b}^{n - 1} \paren {\paren {m + n + 1 - s} a x + \paren {m - s + 1} b}
      | c = gathering terms
}}
{{end-eqn}}
Let $s$ be selected such that $m + n + 1 - s = 0$.
Then $s = m + n + 1$.
Thus $(2)$ after rearrangement becomes:
:$\dfrac {\d u} {\d x} = \dfrac {x^{m - s} } {m + n + 1} \paren {a x + b}^{n - 1} \paren {\paren {m - s + 1} b}$
Then:
{{begin-eqn}}
{{eqn | l = u v
      | r = \frac {x^{m - s + 1} \paren {a x + b}^n} {m + n + 1} x^s
      | c = 
}}
{{eqn | r = \frac {x^{m + 1} \paren {a x + b}^n} {m + n + 1}
      | c = 
}}
{{end-eqn}}
and:
{{begin-eqn}}
{{eqn | l = v \frac {\d u} {\d x}
      | r = x^s \dfrac {x^{m - s} } {m + n + 1} \paren {a x + b}^{n - 1} \paren {\paren {m - s + 1} b}
      | c = 
}}
{{eqn | r = \dfrac {x^m} {m + n + 1} \paren {a x + b}^{n - 1} \paren {\paren {m - \paren {m + n + 1} + 1} b}
      | c = 
}}
{{eqn | r = \dfrac {x^m} {m + n + 1} \paren {a x + b}^{n - 1} \paren {-n b}
      | c = 
}}
{{end-eqn}}
Thus by Integration by Parts:
:$\ds \int x^m \paren {a x + b}^n \rd x = \frac {x^{m + 1} \paren {a x + b}^n} {m + n + 1} + \frac {n b} {m + n + 1} \int x^m \paren {a x + b}^{n - 1} \rd x$
{{qed}}
Theorem: Primitive of Power

Let $n \in \R: n \ne -1$.
Then:
:$\ds \int x^n \rd x = \frac {x^{n + 1} } {n + 1} + C$
where $C$ is an arbitrary constant.

Proof:
From Primitive of Power of $a x + b$ by Power of $p x + q$: Decrement of Power:
:$\ds \int \paren {a x + b}^m \paren {p x + q}^n \rd x = \frac {\paren {a x + b}^{m + 1} \paren {p x + q}^n} {\paren {m + n + 1} a} - \frac {n \paren {b p - a q} } {\paren {m + n + 1} a} \int \paren {a x + b}^m \paren {p x + q}^{n - 1} \rd x$
Setting $a := 1, b := 0, p x + q := a x + b$:
{{begin-eqn}}
{{eqn | l = \int x^m \paren {a x + b}^n \rd x
      | r = \frac {\paren {1 x + 0}^{m + 1} \paren {a x + b}^n} {\paren {m + n + 1} 1} - \frac {n \paren {0 a - 1 b} } {\paren {m + n + 1} 1} \int \paren {1 x + 0}^m \paren {a x + b}^{n - 1} \rd x
      | c = 
}}
{{eqn | r = \frac {x^{m + 1} \paren {a x + b}^n} {m + n + 1} - \frac {n b} {\paren {m + n + 1} } \int x^m \paren {a x + b}^{n - 1} \rd x
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Power

Let $n \in \R: n \ne -1$.
Then:
:$\ds \int x^n \rd x = \frac {x^{n + 1} } {n + 1} + C$
where $C$ is an arbitrary constant.

Proof:
Let $s \in \Z$. 
{{begin-eqn}}
{{eqn | l = v
      | r = \paren {a x + b}^s
      | c = 
}}
{{eqn | n = 1
      | ll= \leadsto
      | l = \frac {\d v} {\d x}
      | r = a s \paren {a x + b}^{s - 1}
      | c = Power Rule for Derivatives and Derivatives of Function of $a x + b$
}}
{{end-eqn}}
Let $u \dfrac {\d v} {\d x} = x^m \paren {a x + b}^n$.
Then:
{{begin-eqn}}
{{eqn | l = u
      | r = \frac {x^m \paren {a x + b}^n} {a s \paren {a x + b}^{s - 1} }
      | c = from $(1)$
}}
{{eqn | r = \frac {x^m} {a s} \paren {a x + b}^{n - s + 1}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \frac {\d u} {\d x}
      | r = \frac {m x^{m - 1} } {a s} \paren {a x + b}^{n - s + 1} + \frac {x^m} {a s} a \paren {n - s + 1} \paren {a x + b}^{n - s}
      | c = above rules and Product Rule for Derivatives
}}
{{eqn | r = \frac {x^{m - 1} } {a s} \paren {a x + b}^{n - s} \paren {m \paren {a x + b} + a \paren {n - s + 1} x}
      | c = extracting $\dfrac {x^{m - 1} } {a s} \paren {a x + b}^{n - s}$ as a factor
}}
{{eqn | n = 2
      | r = \frac {x^{m - 1} } {a s} \paren {a x + b}^{n - s} \paren {m b + a \paren {m + n - s + 1} x}
      | c = rearranging
}}
{{end-eqn}}
Let $s$ be selected such that $m + n + 1 - s = 0$.
Then $s = m + n + 1$.
Thus $(2)$ after rearrangement becomes:
:$\dfrac {\d u} {\d x} = \dfrac {m b x^{m - 1} \paren {a x + b}^{n - s} } {\paren {m + n + 1} a}$
Then:
{{begin-eqn}}
{{eqn | l = u v
      | r = \frac {x^m} {a s} \paren {a x + b}^{n - s + 1} \paren {a x + b}^s
      | c = 
}}
{{eqn | r = \frac {x^m \paren {a x + b}^{n + 1} } {\paren {m + n + 1} a}
      | c = 
}}
{{end-eqn}}
and:
{{begin-eqn}}
{{eqn | l = v \frac {\d u} {\d x}
      | r = \paren {a x + b}^s \frac {m b x^{m - 1} \paren {a x + b}^{n - s} } {\paren {m + n + 1} a}
      | c = 
}}
{{eqn | r = \frac {m b x^{m - 1} \paren {a x + b}^n} {\paren {m + n + 1} a}
      | c = 
}}
{{end-eqn}}
Thus by Integration by Parts:
:$\ds \int x^m \paren {a x + b}^n \rd x = \frac {x^m \paren {a x + b}^{n + 1} } {\paren {m + n + 1} a} - \frac {m b} {\paren {m + n + 1} a} \int x^{m - 1} \paren {a x + b}^n \rd x$
{{qed}}
Theorem: Primitive of Power

Let $n \in \R: n \ne -1$.
Then:
:$\ds \int x^n \rd x = \frac {x^{n + 1} } {n + 1} + C$
where $C$ is an arbitrary constant.

Proof:
From Primitive of Power of $a x + b$ by Power of $p x + q$: Decrement of Power:
:$\ds \int \paren {a x + b}^m \paren {p x + q}^n \rd x = \frac {\paren {a x + b}^{m + 1} \paren {p x + q}^n} {\paren {m + n + 1} a} - \frac {n \paren {b p - a q} } {\paren {m + n + 1} a} \int \paren {a x + b}^m \paren {p x + q}^{n - 1} \rd x$
Setting $p := 1, q := 0, n := m, m := n$:
{{begin-eqn}}
{{eqn | l = \int x^m \paren {a x + b}^n \rd x
      | r = \frac {\paren {a x + b}^{n + 1} \paren {1 x + 0}^m} {\paren {m + n + 1} a} - \frac {m \paren {b 1 - a 0} } {\paren {m + n + 1} a} \int \paren {a x + b}^n \paren {1 x + 0}^{m - 1} \rd x
      | c = 
}}
{{eqn | r = \frac {x^m \paren {a x + b}^{n + 1} } {\paren {m + n + 1} a} - \frac {m b} {\paren {m + n + 1} a} \int x^{m - 1} \paren {a x + b}^n \rd x
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Power

Let $n \in \R: n \ne -1$.
Then:
:$\ds \int x^n \rd x = \frac {x^{n + 1} } {n + 1} + C$
where $C$ is an arbitrary constant.

Proof:
From Primitive of Power of $x$ by Power of $a x + b$: Decrement of Power of $x$:
:$\ds \int x^m \paren {a x + b}^n \rd x = \frac {x^{m + 1} \paren {a x + b}^n} {m + n + 1} + \frac {n b} {m + n + 1} \int x^m \paren {a x + b}^{n - 1} \rd x$
Substituting $n + 1$ for $n$:
{{begin-eqn}}
{{eqn | l = \int x^m \paren {a x + b}^{n + 1} \rd x
      | r = \frac {x^{m + 1} \paren {a x + b}^{n + 1} } {m + n + 2} + \frac {\paren {n + 1} b} {m + n + 2} \int x^m \paren {a x + b}^n \rd x
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \frac {\paren {n + 1} b} {m + n + 2} \int x^m \paren {a x + b}^n \rd x
      | r = \frac {-x^{m + 1} \paren {a x + b}^{n + 1} } {m + n + 2} + \int x^m \paren {a x + b}^{n + 1} \rd x
      | c = rearrangement
}}
{{eqn | ll= \leadsto
      | l = \int x^m \paren {a x + b}^n \rd x
      | r = \frac {m + n + 2} {\paren {n + 1} b} \frac {-x^{m + 1} \paren {a x + b}^{n + 1} } {m + n + 2} + \frac {m + n + 2} {\paren {n + 1} b} \int x^m \paren {a x + b}^{n + 1} \rd x
      | c = rearrangement
}}
{{eqn | ll= \leadsto
      | l = \int x^m \paren {a x + b}^n \rd x
      | r = \frac {-x^{m + 1} \paren {a x + b}^{n + 1} } {\paren {n + 1} b} + \frac {m + n + 2} {\paren {n + 1} b} \int x^m \paren {a x + b}^{n + 1} \rd x
      | c = rearrangement
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Power

Let $n \in \R: n \ne -1$.
Then:
:$\ds \int x^n \rd x = \frac {x^{n + 1} } {n + 1} + C$
where $C$ is an arbitrary constant.

Proof:
From Primitive of Power of $a x + b$ by Power of $p x + q$: Increment of Power:
:$\ds \int \paren {a x + b}^m \paren {p x + q}^n \rd x = \frac 1 {\paren {n + 1} \paren {b p - a q} } \paren {\paren {a x + b}^{m + 1} \paren {p x + q}^{n + 1} - a \paren {m + n + 2} \int \paren {a x + b}^m \paren {p x + q}^{n + 1} \rd x}$
Setting $a := 1, b := 0, p x + q := a x + b$:
{{begin-eqn}}
{{eqn | l = \int x^m \paren {a x + b}^n \rd x
      | r = \frac 1 {\paren {n + 1} \paren {0 a - 1 b} } \paren {\paren {1 x + 0}^{m + 1} \paren {a x + b}^{n + 1} - 1 \paren {m + n + 2} \int \paren {1 x + 0}^m \paren {a x + b} ^{n + 1} \rd x}
      | c = 
}}
{{eqn | r = \frac 1 {\paren {n + 1} \paren {-b} } \paren {x^{m + 1} \paren {a x + b}^{n + 1} - \paren {m + n + 2} \int x^m \paren {a x + b}^{n + 1} \rd x}
      | c = 
}}
{{eqn | r = \frac {-x^{m + 1} \paren {a x + b}^{n + 1} } {\paren {n + 1} b} + \frac {m + n + 2} {\paren {n + 1} b} \int x^m \paren {a x + b}^{n + 1} \rd x
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Power

Let $n \in \R: n \ne -1$.
Then:
:$\ds \int x^n \rd x = \frac {x^{n + 1} } {n + 1} + C$
where $C$ is an arbitrary constant.

Proof:
From Primitive of Power of $x$ by Power of $a x + b$: Decrement of Power of $x$:
:$\ds \int x^m \paren {a x + b}^n \rd x = \frac {x^m \paren {a x + b}^{n + 1} } {\paren {m + n + 1} a} - \frac {m b} {\paren {m + n + 1} a} \int x^{m - 1} \paren {a x + b}^n \rd x$
Substituting $m + 1$ for $m$:
{{begin-eqn}}
{{eqn | l = \int x^{m + 1} \paren {a x + b}^n \rd x
      | r = \frac {x^{m + 1} \paren {a x + b}^{n + 1} } {\paren {m + n + 2} a} - \frac {\paren {m + 1} b} {\paren {m + n + 2} a} \int x^m \paren {a x + b}^n \rd x
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \frac {\paren {m + 1} b} {\paren {m + n + 2} a} \int x^m \paren {a x + b}^n \rd x
      | r = \frac {x^{m + 1} \paren {a x + b}^{n + 1} } {\paren {m + n + 2} a} - \int x^{m + 1} \paren {a x + b}^n \rd x
      | c = rearranging
}}
{{eqn | ll= \leadsto
      | l = \int x^m \paren {a x + b}^n \rd x
      | r = \frac {\paren {m + n + 2} a} {\paren {m + 1} b} \frac {x^{m + 1} \paren {a x + b}^{n + 1} } {\paren {m + n + 2} a} - \frac {\paren {m + n + 2} a} {\paren {m + 1} b} \int x^{m + 1} \paren {a x + b}^n \rd x
      | c = rearranging
}}
{{eqn | r = \frac {x^{m + 1} \paren {a x + b}^{n + 1} } {\paren {m + 1} b} - \frac {\paren {m + n + 2} a} {\paren {m + 1} b} \int x^{m + 1} \paren {a x + b}^n \rd x
      | c = rearranging
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Power

Let $n \in \R: n \ne -1$.
Then:
:$\ds \int x^n \rd x = \frac {x^{n + 1} } {n + 1} + C$
where $C$ is an arbitrary constant.

Proof:
From Primitive of Power of $a x + b$ by Power of $p x + q$: Increment of Power:
:$\ds \int \paren {a x + b}^m \paren {p x + q}^n \rd x = \frac 1 {\paren {n + 1} \paren {b p - a q} } \paren {\paren {a x + b}^{m + 1} \paren {p x + q}^{n + 1} - a \paren {m + n + 2} \int \paren {a x + b}^m \paren {p x + q}^{n + 1} \rd x}$
Setting $p := 1, q := 0, m := n, n := m$:
{{begin-eqn}}
{{eqn | l = \int x^m \paren {a x + b}^n \rd x
      | r = \frac 1 {\paren {m + 1} \paren {b 1 - a 0} } \paren {\paren {a x + b}^{n + 1} \paren {1 x + 0}^{m + 1} - a \paren {m + n + 2} \int \paren {a x + b}^n \paren {0 x + 1}^{m + 1} \rd x}
      | c = 
}}
{{eqn | r = \frac 1 {\paren {m + 1} b} \paren {\paren {a x + b}^{n + 1} x^{m + 1} - a \paren {m + n + 2} \int \paren {a x + b}^n x^{m + 1} \rd x}
      | c = 
}}
{{eqn | r = \frac {x^{m + 1} \paren {a x + b}^{n + 1} } {\paren {m + 1} b} - \frac {\paren {m + n + 2} a} {\paren {m + 1} b} \int x^{m + 1} \paren {a x + b}^n \rd x
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Power

Let $n \in \R: n \ne -1$.
Then:
:$\ds \int x^n \rd x = \frac {x^{n + 1} } {n + 1} + C$
where $C$ is an arbitrary constant.

Proof:
{{begin-eqn}}
{{eqn | l = \map {\frac \d {\d x} } {\dfrac {x^{n + 1} } {n + 1} }
      | r = \paren {n + 1} \paren {\dfrac {x^{\paren {n + 1} - 1} } {n + 1} }
      | c = Power Rule for Derivatives
}}
{{eqn | r = x^n
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \int x^n \rd x
      | r = \frac {x^{n + 1} } {n + 1} + C
      | c = {{Defof|Primitive (Calculus)}}
}}
{{end-eqn}}
When $n = -1$ we have $n + 1 = 0$, and $\dfrac {x^{n + 1} } {n + 1} = \dfrac {x^0} 0$ is undefined.
{{qed}}
Theorem: Sine Inequality

:$\size {\sin x} \le \size x$
for all $x \in \R$.

Proof:
Let $\map f x = x - \sin x$.
By Derivative of Sine Function:
:$\map {f'} x = 1 - \cos x$
From Real Cosine Function is Bounded we know $\cos x \le 1$ for all $x$.
Hence $\map f x \ge 0$ for all $x$.
From Derivative of Monotone Function, $\map f x$ is increasing. 
By Sine of Zero is Zero, $\map f 0 = 0$.
It follows that $\map f x \ge 0$ for all $x \ge 0$.
{{qed|lemma}}
Now let $\map g x = x^2 - \sin^2 x$.
{{begin-eqn}}
{{eqn | l = \map {g'} x
      | r = 2 x - 2 \sin x \cos x
      | c = Chain Rule for Derivatives and Derivative of Sine Function
}}
{{eqn | r = 2 x - \sin 2 x
      | c = Double Angle Formula for Sine
}}
{{eqn | o = \ge
      | r = 0
      | c = for $x \ge 0$, as shown above
}}
{{end-eqn}}
From Derivative of Monotone Function, $\map g x$ is increasing for $x \ge 0$. 
By Sine of Zero is Zero, $\map g 0 = 0$.
It follows that $\map g x \ge 0$ for all $x \ge 0$.
Observe that $\map g x$ is an even function.
This implies $\map g x \ge 0$ for all $x \in \R$.
Finally note that $\sin^2 x \le x^2 \iff \size {\sin x} \le \size x$.
{{qed}}
Theorem: Sine Inequality

:$\size {\sin x} \le \size x$
for all $x \in \R$.

Proof:
For $x = 0$, the inequality is trivial, as $\sin 0 = 0$.
If $\size x \ge 1$, the inequality also clear as:
{{begin-eqn}}
{{eqn | l = \size {\sin x}
      | o = \le
      | r = 1
      | c = Real Sine Function is Bounded
}}
{{eqn | o = \le
      | r = \size x
}}
{{end-eqn}}
Now, suppose $0 < \size x < 1$
Then on the one hand:
{{begin-eqn}}
{{eqn | l = \dfrac {\sin x} x
      | r = \sum_{n \mathop = 0}^\infty \paren {-1}^n \frac {x^{2 n} } {\paren {2 n + 1}!}
      | c = {{Defof|Real Sine Function}}
}}
{{eqn | r = 1 - \sum_{n \mathop = 1}^\infty \paren {-1}^{n-1} \frac {x^{2 n} } {\paren {2 n + 1}!}
}}
{{eqn | o = \ge
      | r = 1 - \sum_{k \mathop = 0}^\infty \frac {x^{4k+2} } {\paren {4k+3}!}
      | c = as $x^2 \ge 0$
}}
{{eqn | o = \ge
      | r = 1 - \sum_{k \mathop = 0}^\infty \frac 1 {\paren {4k+3}!}
      | c = as $x^2 \le 1$
}}
{{eqn | r = 1 - \frac 1 {3!} \paren {1 + \frac 1 {7 \cdot 6 \cdot 5 \cdot 4} + \frac 1 {11 \cdot 10 \cdot 9 \cdot 8 \cdot 7 \cdot 6 \cdot 5 \cdot 4} + \cdots }
}}
{{eqn | o = \ge
      | r = 1 - \frac 1 {3!} \paren {1 + \frac 1 {4^4} + \frac 1 {4^8} + \frac 1 {4^{12} } + \cdots }
}}
{{eqn | r = 1 - \frac {4^4} {3! \paren {4^4 - 1} }
      | c = Sum of Infinite Geometric Sequence
}}
{{eqn | o = \ge
      | r = 0
}}
{{end-eqn}}
On the one hand:
{{begin-eqn}}
{{eqn | l = \dfrac {\sin x} x
      | r = \sum_{n \mathop = 0}^\infty \paren {-1}^n \frac {x^{2 n} } {\paren {2 n + 1}!}
      | c = {{Defof|Real Sine Function}}
}}
{{eqn | r = 1 - \dfrac {x^2} 6 + \sum_{n \mathop = 2}^\infty \paren {-1}^n \frac {x^{2 n} } {\paren {2 n + 1}!}
}}
{{eqn | o = \le
      | r = 1 - \dfrac {x^2} 6 + \sum_{k \mathop = 1}^\infty \frac {x^{4k} } {\paren {4k+1}!}
      | c = as $x^2 \ge 0$
}}
{{eqn | r = 1 - x^2 \paren {\frac 1 6 - \sum_{k \mathop = 1}^\infty \frac {x^{2 \paren {k-1} } } {\paren {4k+1}!} }
}}
{{eqn | o = \le
      | r = 1 - x^2 \paren {\dfrac 1 6 - \sum_{k \mathop = 1}^\infty \frac 1 {\paren {4 k + 1}!} }
      | c = as $x^2 \le 1$
}}
{{end-eqn}}
The last expression is $\le 1$, since:
{{begin-eqn}}
{{eqn | l = \sum_{k \mathop = 1}^\infty \frac 1 {\paren {4 k + 1}!}
      | r = \frac 1 {5!} \sum_{k \mathop = 1}^\infty \frac {5 !} {\paren {4 k + 1}!}
}}
{{eqn | r = \frac 1 {5!} \paren {1 + \frac 1 {9 \cdot 8 \cdot 7 \cdot 6} + \frac 1 {13 \cdot 12 \cdot 11 \cdot 10 \cdot 9 \cdot 8 \cdot 7 \cdot 6} + \cdots}
}}
{{eqn | o = \le
      | r = \frac 1 {5!} \paren {1 + \frac 1 {6^4} + \frac 1 {6^8} + \frac 1 {6^{12} } + \cdots}
}}
{{eqn | r = \frac 1 {5!} \frac {6^4} {6^4 - 1}
      | c = Sum of Infinite Geometric Sequence
}}
{{eqn | r = \frac 1 6 \frac {6^4} {20 \paren {6^4 - 1} }
}}
{{eqn | o = <
      | r = \frac 1 6
}}
{{end-eqn}}
{{qed}}
Theorem: Jordan's Inequality

:300pxthumbright
:$\dfrac {2 x} \pi \le \sin x \le x$
for all $x$ in the interval $\closedint 0 {\dfrac \pi 2}$

Proof:
The {{RHS}} inequality is true by Sine Inequality.
The {{LHS}} inequality is true for $x = 0$ and $x = \dfrac \pi 2$, where we have equality.
Now consider $x \in \openint 0 {\dfrac \pi 2}$.
From Shape of Sine Function, $\sin x$ is concave on the interval $\closedint 0 \pi$.
Letting $x_1 = 0$, $x_2 = x$ and $x_3 = \dfrac \pi 2$ in the definition of Concave Real Function we obtain:
:$\dfrac {\sin x} x \ge \dfrac {1 - \sin x} {\dfrac \pi 2 - x}$
Rearranging gives the desired inequality.
{{qed}}
{{Namedfor|Marie Ennemond Camille Jordan|cat = Jordan, C}}
Theorem: Cosine Inequality

:$1 - \dfrac {x^2} 2 \le \cos x$
for all $x \in \R$.

Proof:
Let $\map f x = \cos x - \paren {1 - \dfrac {x^2} 2}$.
By Derivative of Cosine Function:
:$\map {f'} x = x - \sin x$
From Sine Inequality, we know $\sin x \le x$ for $x \ge 0$.
Hence $\map {f'} x \ge 0$ for $x \ge 0$.
From Derivative of Monotone Function, $\map f x$ is increasing for $x \ge 0$.
By Cosine of Zero is One, $\map f 0 = 0$.
It follows that $\map f x \ge 0$ for $x \ge 0$.
By Cosine Function is Even, $\map f x$ is an even function.
This implies $\map f x \ge 0$ for all $x \in \R$.
{{qed}}
Category:Cosine Function
sxm3zaovh90d8feog19hsx3m5qogudc
Theorem: Laplace Transform of Constant Mapping

Let $a \in \R$ be a real constant.
Let $f_a: \R \to \R$ or $\C$ be the constant mapping, defined as:
:$\forall t \in \R: \map {f_a} t = a$
Let $\laptrans {f_a}$ be the Laplace transform of $f_a$.
Then:
:$\laptrans {\map {f_a} t} = \dfrac a s$
for $\map \Re s > a$.

Proof:
{{begin-eqn}}
{{eqn | l = \laptrans {\map {f_a} t}
      | r = \laptrans a
      | c = {{Defof|Constant Mapping}}
}}
{{eqn | r = a \, \laptrans 1
      | c = Linear Combination of Laplace Transforms
}}
{{eqn | r = a \frac 1 s
      | c = Laplace Transform of 1
}}
{{eqn | r = \frac a s
}}
{{end-eqn}}
{{qed}}
Theorem: Laplace Transform of Constant Mapping

Let $a \in \R$ be a real constant.
Let $f_a: \R \to \R$ or $\C$ be the constant mapping, defined as:
:$\forall t \in \R: \map {f_a} t = a$
Let $\laptrans {f_a}$ be the Laplace transform of $f_a$.
Then:
:$\laptrans {\map {f_a} t} = \dfrac a s$
for $\map \Re s > a$.

Proof:
{{begin-eqn}}
{{eqn | l = \laptrans {\map {f_a} t}
      | r = \laptrans a
      | c = {{Defof|Constant Mapping}}
}}
{{eqn | r = a \, \laptrans 1
      | c = Linear Combination of Laplace Transforms
}}
{{eqn | r = a \int_0^{\to +\infty} e^{-s t} \rd t
      | c = {{Defof|Laplace Transform}}
}}
{{eqn | r = \intlimits {- \frac a s e^{-st} } {t \mathop = 0} {t \mathop \to +\infty}
}}
{{eqn | r = 0 - \paren {- \frac a s}
      | c = Complex Exponential Tends to Zero, Exponential of Zero
}}
{{eqn | r = \frac a s
}}
{{end-eqn}}
{{qed}}
Theorem: Laplace Transform of Identity Mapping

Let $\laptrans f$ denote the Laplace transform of a function $f$.
Let $\map {I_\R} t$ denote the identity mapping on $\R$ for $t > 0$.
Then:
:$\laptrans {\map {I_\R} t} = \dfrac 1 {s^2}$
for $\map \Re s > 0$.

Proof:
{{begin-eqn}}
{{eqn | l = \laptrans {\map {I_\R} t}
      | r = \laptrans t
      | c = {{Defof|Identity Mapping}}
}}
{{eqn | r = \int_0^{\to +\infty} t e^{-st} \rd t
      | c = {{Defof|Laplace Transform}}
}}
{{end-eqn}}
From Integration by Parts:
:$\ds \int f g' \rd t = f g - \int f'g \rd t$
Here:
{{begin-eqn}}
{{eqn | l = f
      | r = t
      | c = 
}}
{{eqn | ll= \leadsto
      | l = f'
      | r = 1
      | c = Derivative of Identity Function
}}
{{eqn | l = g'
      | r = e^{-st}
}}
{{eqn | ll= \leadsto
      | l = g
      | r = -\frac 1 s e^{-s t}
      | c = Primitive of Exponential Function
}}
{{end-eqn}}
So: 
{{begin-eqn}}
{{eqn | l = \int t e^{-s t} \rd t
      | r = -\frac t s e^{-s t} - \frac 1 s \int e^{-s t} \rd t
}}
{{eqn | r = -\frac t s e^{-s t} - \frac 1 {s^2} e^{-s t}
      | c = Primitive of Exponential Function
}}
{{end-eqn}}
Evaluating at $t = 0$ and $t \to +\infty$:
{{begin-eqn}}
{{eqn | l = \laptrans t
      | r = \intlimits {-\frac t s e^{-s t} - \frac 1 {s^2} e^{-s t} } {t \mathop = 0} {t \mathop \to +\infty}
}}
{{eqn | r = -\frac 1 s \lim_{t \mathop \to +\infty} \frac t { e^{s t} } - \paren {0 - \frac 1 {s^2} }
      | c = Exponential of Zero and One, Exponent Combination Laws: Negative Power
}}
{{eqn | r = 0 + \frac 1 {s^2}
      | c = Limit at Infinity of Polynomial over Complex Exponential
}}
{{eqn | r = \frac 1 {s^2}
}}
{{end-eqn}}
{{qed}}
Theorem: Laplace Transform of Positive Integer Power

Let $\laptrans f$ denote the Laplace transform of a function $f$.
Let $t^n: \R \to \R$ be $t$ to the $n$th power for some $n \in \N_{\ge 0}$.
Then:
:$\laptrans {t^n} = \dfrac {n!} {s^{n + 1} }$
for $\map \Re s > 0$.

Proof:
{{begin-eqn}}
{{eqn | l = \laptrans {t^n}
      | r = \int_0^{\to +\infty} t^n e^{-s t} \rd t
      | c = {{Defof|Laplace Transform}}
}}
{{eqn | r = \intlimits {\frac {e^{-s t} } {-s} \sum_{k \mathop = 0}^n \paren {\paren {-1}^k \frac {n^{\underline k} t^{n - k} } {\paren {-s}^k} } } {t \mathop = 0} {t \mathop \to +\infty}
      | c = Primitive of $x^n e^{a x}$
}}
{{eqn | r = \sum_{k \mathop = 0}^n \paren {0 - \frac 1 {-s} \paren {-1}^k \frac {n^{\underline k} 0^{n - k} } {\paren {-s}^k} }
      | c = Exponential Tends to Zero and Infinity, Exponent Combination Laws: Negative Power
}}
{{eqn | r = \sum_{k \mathop = 0}^n \paren {\dfrac 1 {s^{k + 1} } n^{\underline k} 0^{n - k} }
      | c = simplifying
}}
{{eqn | r = \dfrac 1 {s^{k + 1} } n^{\underline n}
      | c = $0^{n - k} = 0$ for all terms except $n = k$, when $0^{n - n} = 1$
}}
{{eqn | r = \dfrac {n!} {s^{k + 1} }
      | c = Integer to Power of Itself Falling is Factorial
}}
{{end-eqn}}
{{qed}}