avewright/proofwiki-math huggingface dataset:
Theorem: Approximation to x+y Choose y

:$\ds \lim_{x, y \mathop \to \infty} \dbinom {x + y} y = \sqrt {\dfrac 1 {2 \pi} \paren {\frac 1 x + \frac 1 y} } \paren {1 + \dfrac y x}^x \paren {1 + \dfrac x y}^y$

Proof:
It can be assumed that both $x$ and $y$ are integers.
{{begin-eqn}}
{{eqn | l = \dbinom {x + y} y
      | r = \dfrac {\paren {x + y}!} {x! \, y!}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \ds \lim_{x, y \mathop \to \infty} \dbinom {x + y} y
      | r = \dfrac {\sqrt {2 \pi \paren {x + y} } \paren {\dfrac {x + y} e}^{\paren {x + y} } } {\sqrt {2 \pi x} \paren {\dfrac x e}^x \, \sqrt {2 \pi y} \paren {\dfrac y e}^y}
      | c = Stirling's Formula
}}
{{eqn | r = \dfrac 1 {\sqrt {2 \pi} } \dfrac {\paren {\frac 1 e}^{x + y} } {\paren {\frac 1 e}^x \paren {\frac 1 e}^y} \sqrt {\dfrac {x + y} {x y} } \dfrac {\paren {x + y}^x \paren {x + y}^y} {x^x \, y^y}
      | c = rearrangement
}}
{{eqn | r = \dfrac 1 {\sqrt {2 \pi} } \sqrt {\frac 1 x + \frac 1 y} \paren {1 + \dfrac y x}^x \paren {1 + \dfrac x y}^y
      | c = simplifying
}}
{{eqn | r = \sqrt {\dfrac 1 {2 \pi} \paren {\frac 1 x + \frac 1 y} } \paren {1 + \dfrac y x}^x \paren {1 + \dfrac x y}^y
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Approximation to 2n Choose n

:$\ds \lim_{n \mathop \to \infty} \dbinom {2 n} n = \dfrac {4^n} {\sqrt {n \pi} }$

Proof:
From Approximation to $\dbinom {x + y} y$:
:$\ds \lim_{x, y \mathop \to \infty} \dbinom {x + y} y = \sqrt {\dfrac 1 {2 \pi} \paren {\frac 1 x + \frac 1 y} } \paren {1 + \dfrac y x}^x \paren {1 + \dfrac x y}^y$
Thus:
{{begin-eqn}}
{{eqn | l = \lim_{n \mathop \to \infty} \dbinom {2 n} n
      | r = \sqrt {\dfrac 1 {2 \pi} \paren {\frac 1 n + \frac 1 n} } \paren {1 + \dfrac n n}^n \paren {1 + \dfrac n n}^n
      | c = 
}}
{{eqn | r = \sqrt {\dfrac 1 {2 \pi} \paren {\frac 2 n} } \paren {1 + 1}^n \paren {1 + 1}^n
      | c = 
}}
{{eqn | r = \sqrt {\dfrac 1 {n \pi} } 2^{2 n}
      | c = 
}}
{{eqn | r = \dfrac {4^n} {\sqrt {n \pi} }
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Product of r Choose k with r Minus Half Choose k/Formulation 1

Let $k \in \Z$, $r \in \R$.
:$\dbinom r k \dbinom {r - \frac 1 2} k = \dfrac {\dbinom {2 r} k \dbinom {2 r - k} k} {4^k}$
where $\dbinom r k$ denotes a binomial coefficient.

Proof:
First we establish the following:
{{begin-eqn}}
{{eqn | l = \paren {r - \frac 1 2}^{\underline k}
      | r = \paren {r - \frac 1 2} \paren {r - \frac 3 2} \paren {r - \frac 5 2} \dotsm \paren {r - \frac 1 2 - k + 1}
      | c = {{Defof|Falling Factorial}}
}}
{{eqn | r = \dfrac {2^k \paren {r - \frac 1 2} \paren {r - \frac 3 2} \paren {r - \frac 5 2} \cdots \paren {r - \frac 1 2 - k + 1} } {2^k}
      | c = 
}}
{{eqn | r = \dfrac {\paren {2 r - 1} \paren {2 r - 3} \paren {2 r - 5} \dotsm \paren {2 r - 2 k + 1} } {2^k}
      | c = 
}}
{{eqn | r = \dfrac {2 r \paren {2 r - 1} \paren {2 r - 2} \paren {2 r - 3} \dotsm \paren {2 r - 2 k + 2} \paren {2 r - 2 k + 1} } {2^k \paren {2 r \paren {2 r - 2} \paren {2 r - 4} \dotsm \paren {2 r - 2 k + 2} } }
      | c = 
}}
{{eqn | n = 1
      | r = \dfrac {\paren {2 r}^{\underline{2 k} } } {2^k \times 2^k r^{\underline k} }
      | c = {{Defof|Falling Factorial}}
}}
{{end-eqn}}
Then:
{{begin-eqn}}
{{eqn | l = \dbinom r k \dbinom {r - \frac 1 2} k
      | r = \dfrac {r^{\underline k} } {k!} \dfrac {\paren {r - \frac 1 2}^{\underline k} } {k!}
      | c = {{Defof|Binomial Coefficient|subdef = Real Numbers}}
}}
{{eqn | r = \dfrac {r^{\underline k} } {k!} \dfrac {\paren {2 r}^{\underline {2 k} } } {k! \, 2^{2 k} r^{\underline k} }
      | c = from $(1)$
}}
{{eqn | r = \dfrac {\paren {2 r}^{\underline {2 k} } } {\paren {k!}^2 \, 4^k}
      | c = simplifying
}}
{{eqn | r = \dfrac {\paren {2 r}^{\underline k} \paren {2 r - k}^{\underline k} } {\paren {k!}^2 \, 4^k}
      | c = Falling Factorial of Sum of Integers
}}
{{eqn | r = \dfrac 1 {4^k} \dfrac {\paren {2 r}^{\underline k} } {k!} \dfrac {\paren {2 r - k}^{\underline k} } {k!}
      | c = separating out
}}
{{eqn | r = \dfrac 1 {4^k} \dbinom {2 r} k \dbinom {2 r - k} k
      | c = {{Defof|Binomial Coefficient|subdef = Real Numbers}}
}}
{{end-eqn}}
Theorem: Provable Consequence of Theorems is Theorem

Let $\PP$ be a proof system for a formal language $\LL$.
Let $\FF$ be a collection of theorems of $\PP$.
Denote with $\map {\mathscr P} \FF$ the proof system obtained from $\mathscr P$ by adding all the WFFs from $\FF$ as axioms.
Let $\phi$ be a provable consequence of $\FF$:
:$\vdash_{\mathscr P} \FF$
:$\FF \vdash_{\mathscr P} \phi$
Then $\phi$ is also a theorem of $\mathscr P$:
:$\vdash_{\mathscr P} \phi$

Proof:
We have that $\phi$ is a provable consequence of $\FF$.
Hence it is a theorem of $\map {\mathscr P} \FF$, the proof system obtained from $\mathscr P$ by adding all of $\FF$ as axioms.
Now in the formal proof of $\phi$ in $\map {\mathscr P} \FF$, both axioms and rules of inference are used.
Each rule of inference of $\map {\mathscr P} \FF$ is also a rule of inference of $\mathscr P$.
Similarly, by construction, each axiom of $\map {\mathscr P} \FF$ is either an axiom of $\mathscr P$ or an element of $\FF$.
But the elements of $\FF$ are theorems of $\mathscr P$, each of which thus has a formal proof in $\mathscr P$.
By definition, the rules of inference of a proof system do not distinguish between theorems and axioms.
Therefore the formal proofs of the following can be combined:
:$\vdash_{\mathscr P} \FF$
:$\vdash_{\map {\mathscr P} \FF} \phi$
by letting the latter follow the former.
This yields a new formal proof, which is entirely formulated in $\mathscr P$.
This is the desired formal proof of $\phi$ from $\mathscr P$, and we conclude:
:$\vdash_{\mathscr P} \phi$
{{qed}}
Theorem: Binomial Coefficient of Minus Half

Let $k \in \Z$.
:$\dbinom {-\frac 1 2} k = \dfrac {\paren {-1}^k} {4^k} \dbinom {2 k} k$
where $\dbinom {-\frac 1 2} k$ denotes a binomial coefficient.

Proof:
From Product of r Choose k with r Minus Half Choose k:
:$\dbinom r k \dbinom {r - \frac 1 2} k = \dfrac {\dbinom {2 r} k \dbinom {2 r - k} k} {4^k}$
Setting $r = -\dfrac 1 2$:
{{begin-eqn}}
{{eqn | l = \dbinom {-\frac 1 2} k \dbinom {-1} k
      | r = \frac 1 {4^k} \dbinom {-1} k \dbinom {-1 - k} k
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \dbinom {-\frac 1 2} k
      | r = \frac 1 {4^k} \dbinom {-1 - k} k
      | c = 
}}
{{eqn | r = \frac {\paren {-1}^k} {4^k} \dbinom {k - \paren {-1 - k} - 1} k
      | c = Negated Upper Index of Binomial Coefficient
}}
{{eqn | r = \frac {\paren {-1}^k} {4^k} \dbinom {2 k} k
      | c = simplifying
}}
{{end-eqn}}
{{qed}}
Theorem: Falling Factorial of Sum of Integers

Let $r \in \R$ be a real number.
Let $a, b \in \Z$ be (positive) integers.
Then:
:$r^{\underline {a + b} } = r^{\underline a} \paren {r - a}^{\underline b}$
where $r^{\underline a}$ denotes the $a$th falling factorial of $r$.

Proof:
{{begin-eqn}}
{{eqn | l = r^{\underline {a + b} }
      | r = \prod_{j \mathop = 0}^{a + b - 1} \paren {r - j}
      | c = {{Defof|Falling Factorial}}
}}
{{eqn | r = \paren {\prod_{j \mathop = 0}^{a - 1} \paren {r - j} } \paren {\prod_{j \mathop = a}^{a + b - 1} \paren {r - j} }
      | c = 
}}
{{eqn | r = \paren {\prod_{j \mathop = 0}^{a - 1} \paren {r - j} } \paren {\prod_{j \mathop = 0}^{b - 1} \paren {r - a - j} }
      | c = Translation of Index Variable of Product
}}
{{eqn | r = r^{\underline a} \paren {r - a}^{\underline b}
      | c = {{Defof|Falling Factorial}}
}}
{{end-eqn}}
{{qed}}
Category:Falling Factorials
0g0j8sgf6yikukw3vmx1p5uejf37c09
Theorem: Riemann Zeta Function of 8

The Riemann zeta function of $8$ is given by:
{{begin-eqn}}
{{eqn | l = \map \zeta 8
      | r = \dfrac 1 {1^8} +  \dfrac 1 {2^8} +  \dfrac 1 {3^8} +  \dfrac 1 {4^8} + \cdots
      | c = 
}}
{{eqn | r = \dfrac {\pi^8} {9450}
      | c = 
}}
{{eqn | o = \approx
      | r = 1 \cdotp 00408 \, 3 \ldots
      | c = 
}}
{{end-eqn}}

Proof:
{{begin-eqn}}
{{eqn | l = \sum_{n \mathop = 1}^{\infty} \frac 1 {n^8} 
      | r = \map \zeta 8 
      | c = {{Defof|Riemann Zeta Function}}
}}
{{eqn | r = \paren {-1}^5 \frac {B_8 2^7 \pi^8} {8!} 
      | c = Riemann Zeta Function at Even Integers
}}
{{eqn | r = \frac 1 {30} \cdot \frac {2^7 \pi^8} {8!}
      | c = {{Defof|Sequence of Bernoulli Numbers}}
}}
{{eqn | r = \frac {128 \pi^8} {30 \cdot 40 \, 320} 
      | c = {{Defof|Factorial}}
}}
{{eqn | r = \frac {\pi^8} {9450}
}}
{{end-eqn}}
{{qed}}
Theorem: Sum of Sequence of Harmonic Numbers

:$\ds \sum_{k \mathop = 1}^n H_k = \paren {n + 1} H_n - n$
where $H_k$ denotes the $k$th harmonic number.

Proof:
{{begin-eqn}}
{{eqn | l = \sum_{k \mathop = 1}^n H_k
      | r = \sum_{k \mathop = 1}^n \paren {\sum_{j \mathop = 1}^k \frac 1 j}
      | c = {{Defof|Harmonic Numbers}}
}}
{{eqn | r = \sum_{j \mathop = 1}^n \paren {\sum_{k \mathop = j}^n \frac 1 j}
      | c = Summation of i from 1 to n of Summation of j from 1 to i
}}
{{eqn | r = \sum_{j \mathop = 1}^n \paren {\paren {1 + 1 + \cdots + 1} + \paren {\dfrac 1 2 + \dfrac 1 2 + \cdots + \dfrac 1 2} + \cdots + \paren {\dfrac 1 n} }
      | c = $n$ copies of $1$, $\paren {n - 1}$ copies of $\dfrac 1 2$, $\paren {n - 2}$ copies of $\dfrac 1 3$
}}
{{eqn | r = \sum_{j \mathop = 1}^n \paren {n + 1 - j} \times \frac 1 j
      | c = 
}}
{{eqn | r = \sum_{j \mathop = 1}^n \frac {n + 1 - j} j
      | c = 
}}
{{eqn | r = \sum_{j \mathop = 1}^n \frac {n + 1} j - \sum_{j \mathop = 1}^n \frac j j
      | c = Linear Combination of Convergent Series
}}
{{eqn | r = \paren {n + 1} H_n - n
      | c = Linear Combination of Convergent Series and {{Defof|Harmonic Numbers}}
}}
{{end-eqn}}
{{qed}}
Theorem: Sum of Sequence of Harmonic Numbers

:$\ds \sum_{k \mathop = 1}^n H_k = \paren {n + 1} H_n - n$
where $H_k$ denotes the $k$th harmonic number.

Proof:
From Sum over k to n of k Choose m by kth Harmonic Number:
:$\ds \sum_{k \mathop = 1}^n \binom k m H_k = \binom {n + 1} {m + 1} \paren {H_{n + 1} - \frac 1 {m + 1} }$
Setting $m = 0$:
{{begin-eqn}}
{{eqn | l = \sum_{k \mathop = 1}^n \binom k 0 H_k 
      | r = \binom {n + 1} {0 + 1} \paren {H_{n + 1} - \frac 1 {0 + 1} }
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \sum_{j \mathop = 1}^n H_k 
      | r = \paren {n + 1} \paren {H_{n + 1} - 1}
      | c = Binomial Coefficient with $0$, Binomial Coefficient with $1$
}}
{{eqn | r = \paren {n + 1} \paren {H_n + \frac 1 {n + 1} - 1}
      | c = {{Defof|Harmonic Number}}
}}
{{eqn | r = \paren {n + 1} H_n + \paren {n + 1} \frac 1 {n + 1} - \paren {n + 1} 1
      | c = 
}}
{{eqn | r = \paren {n + 1} H_n + 1 - \paren {n + 1}
      | c = 
}}
{{eqn | r = \paren {n + 1} H_n - n
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Sum of Sequence of Harmonic Numbers

:$\ds \sum_{k \mathop = 1}^n H_k = \paren {n + 1} H_n - n$
where $H_k$ denotes the $k$th harmonic number.

Proof:
Let $\sequence {a_n}$ be the sequence defined as:
:$\forall n \in \N_{> 0}: a_n = H_n$
where $H_n$ denotes the $n$th harmonic number.
Let $\map G z$ be the generating function for $\sequence {a_n}$.
From Generating Function for Sequence of Harmonic Numbers:
:$\map G z = \dfrac 1 {1 - z} \map \ln {\dfrac 1 {1 - z} }$
Then:
{{begin-eqn}}
{{eqn | l = \map {G'} z
      | r = \dfrac 1 {\paren {1 - z}^2} \map \ln {\dfrac 1 {1 - z} } + \dfrac 1 {\paren {1 - z}^2}
      | c = Derivative of Generating Function for Sequence of Harmonic Numbers
}}
{{eqn | r = \dfrac 1 {1 - z} \map G z + \dfrac 1 {\paren {1 - z}^2}
      | c = 
}}
{{end-eqn}}
From Generating Function for Sequence of Partial Sums of Series, $\dfrac 1 {1 - z} \map G z$ is the generating function for $\sequence {b_n}$ where:
:$b_n = \ds \sum_{k \mathop = 0}^n H_k$
and so:
:$\dfrac 1 {\paren {1 - z}^2} \map \ln {\dfrac 1 {1 - z} } = \ds \sum_{n \mathop \ge 0} \paren {\sum_{k \mathop = 0}^n H_k} z^n$
From Generating Function for Natural Numbers:
:$\dfrac 1 {\paren {1 - z}^2} = \ds \sum_{n \mathop \ge 0} \paren {n + 1} z^n$
That is:
:$\map {G'} z = \ds \sum_{n \mathop \ge 0} \paren {\sum_{k \mathop = 0}^n H_k + \paren {n + 1} } z^n$
Now we have:
{{begin-eqn}}
{{eqn | l = \map {G'} z
      | r = \map {\dfrac \d {\d z} } {\sum_{n \mathop \ge 0} H_n z^n}
      | c = Derivative of Generating Function for Sequence of Harmonic Numbers
}}
{{eqn | r = \sum_{n \mathop \ge 0} n H_n z^{n - 1}
      | c = Derivative of Power
}}
{{end-eqn}}
Equating coefficients of $z^n$ in these two expressions for $\map {G'} z$:
:$\ds \sum_{k \mathop = 0}^n H_k + \paren {n + 1} = \paren {n + 1} H_{n + 1}$
{{begin-eqn}}
{{eqn | l = \sum_{k \mathop = 0}^n H_k + \paren {n + 1}
      | r = \paren {n + 1} H_{n + 1}
      | c = 
}}
{{eqn | r = \paren {n + 1} H_n + \paren {n + 1} \paren {\dfrac 1 {n + 1} }
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \sum_{k \mathop = 1}^n H_k + n
      | r = \paren {n + 1} H_n
      | c = $H_k = 0$ when $k = 0$, and simplification
}}
{{end-eqn}}
The result follows.
{{qed}}
Theorem: Sum over k to n of k Choose m by kth Harmonic Number

:$\ds \sum_{k \mathop = 1}^n \binom k m H_k = \binom {n + 1} {m + 1} \paren {H_{n + 1} - \frac 1 {m + 1} }$
where:
:$\dbinom k m$ denotes a binomial coefficient
:$H_k$ denotes the $k$th harmonic number.

Proof:
First we note that by Pascal's Rule:
:$\dbinom k m = \dbinom {k + 1} {m + 1} - \dbinom k {m + 1}$
Thus:
{{begin-eqn}}
{{eqn | l = \dbinom k m H_k
      | r = \dbinom {k + 1} {m + 1} \paren {H_{k + 1} - \dfrac 1 {k + 1} } - \dbinom k {m + 1} H_k
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \sum_{k \mathop = 1}^n \binom k m H_k
      | r = \paren {\binom 2 {m + 1} H_2 - \binom 1 {m + 1} H_1}
      | c = 
}}
{{eqn | o = 
      | ro= +
      | r = \cdots
      | c = 
}}
{{eqn | o = 
      | ro= +
      | r = \paren {\binom {n + 1} {m + 1} H_{n + 1} - \binom n {m + 1} H_n}
      | c = 
}}
{{eqn | o = 
      | ro= -
      | r = \sum_{k \mathop = 1}^n \binom {k + 1} {m + 1} \frac 1 {k + 1}
      | c = 
}}
{{eqn | r = \binom {n + 1} {m + 1} H_{n + 1} - \binom 1 {m + 1} H_1 - \frac 1 {m + 1} \sum_{k \mathop = 0}^n \binom k m + \frac 1 {m + 1} \binom 0 m
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \sum_{k \mathop = 1}^n \binom k m H_k
      | r = \binom {n + 1} {m + 1} \paren {H_{n + 1} - \frac 1 {m + 1} }
      | c = Sum of Binomial Coefficients over Upper Index
}}
{{end-eqn}}
{{qed}}
Theorem: Upper Bound for Harmonic Number

:$H_{2^m} \le 1 + m$
where $H_{2^m}$ denotes the $2^m$th harmonic number.

Proof:
:$\ds \sum_{n \mathop = 1}^\infty \frac 1 n = \underbrace 1_{s_0} + \underbrace {\frac 1 2 + \frac 1 3}_{s_1} + \underbrace {\frac 1 4 + \frac 1 5 + \frac 1 6 + \frac 1 7}_{s_2} + \cdots$ 
where $\ds s_k = \sum_{i \mathop = 2^k}^{2^{k + 1} \mathop - 1} \frac 1 i$
From Ordering of Reciprocals:
:$\forall m, n \in \N_{>0}: m > n: \dfrac 1 m < \dfrac 1 n$
so each of the summands in a given $s_k$ is less than $\dfrac 1 {2^k}$.
The number of summands in a given $s_k$ is $2^{k + 1} - 2^k = 2 \times 2^k - 2^k = 2^k$, and so:
:$s_k < \dfrac {2^k} {2^k} = 1$
Hence the harmonic sum $H_{2^m}$ satisfies the following inequality:
{{begin-eqn}}
{{eqn | l = \sum_{n \mathop = 1}^{2^m} \frac 1 n
      | r = \sum_{k \mathop = 0}^m \paren {s_k}
      | c = 
}}
{{eqn | o = <
      | r = \sum_{a \mathop = 0}^m 1
      | c = 
}}
{{eqn | r = 1 + m
      | c = 
}}
{{end-eqn}}
Hence the result.
{{qed}}
Theorem: Power to Real Number by Decimal Expansion is Uniquely Defined

Let $r \in \R_{>1}$ be a real number greater than $1$, expressed by its decimal expansion:
:$r = n \cdotp d_1 d_2 d_3 \ldots$
The power $x^r$ of a (strictly) positive real number $x$ defined as:
:$(1): \quad \ds \lim_{k \mathop \to \infty} x^{\psi_1} \le \xi \le x^{\psi_2}$
where:
{{begin-eqn}}
{{eqn | l = \psi_1
      | r = n + \sum_{j \mathop = 1}^k \frac {d_1} {10^k} = n + \frac {d_1} {10} + \cdots + \frac {d_k} {10^k}
}}
{{eqn | l = \psi_2
      | r = \psi_1 + \dfrac 1 {10^k}
}}
{{end-eqn}}
is unique.

Proof:
If $r$ is rational this has already been established.
{{MissingLinks|Find where.}}
Let $d$ denote the difference between $x^{\psi^1}$ and $x^{\psi^2}$:
{{begin-eqn}}
{{eqn | l = d
      | r = x^{\psi^2} - x^{\psi^1}
      | c = 
}}
{{eqn | r = x^{\psi^1} \paren {x^{\frac 1 {10^k} } - 1}
      | c = 
}}
{{eqn | r = x^{\psi^1} \paren {x^{\frac 1 {10^k} } - 1}
      | c = 
}}
{{end-eqn}}
It follows from Nth Root of 1 plus x not greater than 1 plus x over n that:
:$d < \dfrac {x^{n + 1} \paren {x - 1} } {10^k}$
Thus as $k \to \infty$, $d \to 0$.
The result follows from the Squeeze Theorem.
{{qed}}
Theorem: Change of Base of Logarithm/Base 2 to Base 10

:$\log_{10} x = \left({\lg x}\right) \left({\log_{10} 2}\right) = 0 \cdotp 30102 \, 99956 \, 63981 \, 19521 \, 37389 \ldots \lg x$

Proof:
From Change of Base of Logarithm:
:$\log_a x = \log_a b \ \log_b x$
Substituting $a = 10$ and $b = 2$ gives:
:$\log_{10} x = \left({\lg x}\right) \left({\log_{10} 2}\right)$
The common logarithm of $2$:
:$\log_{10} 2 = 0 \cdotp 30102 \, 99956 \, 63981 \, 19521 \, 37389 \ldots$
can be calculated or looked up.
{{qed}}
Theorem: Smallest Strictly Positive Rational Number does not Exist

There exists no smallest element of the set of strictly positive rational numbers.

Proof:
{{AimForCont}} $x = \dfrac p q$ is the smallest strictly positive rational number.
By definition of strictly positive:
:$0 < \dfrac p q$
Let us calculate the mediant of $0$ and $\dfrac p q$:
:$\dfrac 0 1 < \dfrac {0 + p} {1 + q} < \dfrac p q$
The inequalities follow from Mediant is Between.
Thus $\dfrac p {1 + q}$ is a strictly positive rational number which is smaller than $\dfrac p q$.
Thus $\dfrac p q$ cannot be the smallest strictly positive rational number.
The result follows by Proof by Contradiction.
{{qed}}
Theorem: Necessary Precision for x equal to log base 10 of 2 to determine Decimal expansion of 10 to the x

Let $b = 10$.
Let $x \approx \log_{10} 2$.
Let it be necessary to calculate the decimal expansion of $x$ to determine the first $3$ decimal places of $b^x$.
An infinite number of decimal places of $x$ would in fact be necessary.

Proof:
This is a trick question:
:''How many decimal places of accuracy of $x$ are needed to determine the first $3$ decimal places of $b^x$?''
We have that $b^x = 10^{\log_{10} 2} = 2$.
Let $x_a < x < x_b$, where $x_a$ and $x_b$ are ever closer approximations to $x$.
Then:
:$x_a$ begins $1 \cdotp 999 \ldots$
:$x_b$ begins $2 \cdotp 000 \ldots$
and it will not be possible to achieve the full expansion of $b^x$.
{{qed}}
Theorem: Change of Base of Logarithm/Base 10 to Base e/Form 1

:$\ln x = \paren {\ln 10} \paren {\log_{10} x} = 2 \cdotp 30258 \, 50929 \, 94 \ldots \log_{10} x$

Proof:
From Change of Base of Logarithm:
:$\log_a x = \log_a b \ \log_b x$
Substituting $a = e$ and $b = 10$ gives:
:$\ln x = \paren {\ln 10} \paren {\log_{10} x}$
The Natural Logarithm of 10:
:$\ln 10 = 2 \cdotp 30258 \, 50929 \, 94 \ldots$
can be calculated or looked up.
{{qed}}
Theorem: Change of Base of Logarithm/Base 10 to Base e/Form 2

:$\ln x = \dfrac {\log_{10} x} {\log_{10} e} = \dfrac {\log_{10} x} {0 \cdotp 43429 \, 44819 \, 03 \ldots}$

Proof:
From Change of Base of Logarithm:
:$\log_a x = \dfrac {\log_b x} {\log_b a}$
Substituting $a = e$ and $b = 10$ gives:
:$\ln x = \dfrac {\log_{10} x} {\log_{10} e}$
The Common Logarithm of e:
:$\log_{10} e = 0 \cdotp 43429 \, 44819 \, 03 \ldots$
can then be calculated or looked up.
{{qed}}
Category:Examples of Change of Base of Logarithm
9pk1pf7ln90gee1arnrnnu7hei93er2
Theorem: Change of Base of Logarithm/Base e to Base 10/Form 1

:$\log_{10} x = \paren {\log_{10} e} \paren {\ln x} = 0 \cdotp 43429 \, 44819 \, 03 \ldots \ln x$

Proof:
From Change of Base of Logarithm:
:$\log_a x = \log_a b \, \log_b x$
Substituting $a = 10$ and $b = e$ gives:
:$\log_{10} x = \paren {\log_{10} e} \paren {\ln x}$
The Common Logarithm of e:
:$\log_{10} e = 0 \cdotp 43429 \, 44819 \, 03 \ldots$
can be calculated or looked up.
{{qed}}
Theorem: Change of Base of Logarithm/Base e to Base 10/Form 2

:$\log_{10} x = \dfrac {\ln x} {\ln 10} = \dfrac {\ln x} {2 \cdotp 30258 \, 50929 \, 94 \ldots}$

Proof:
From Change of Base of Logarithm:
:$\log_a x = \dfrac {\log_b x} {\log_b a}$
Substituting $a = 10$ and $b = e$ gives:
:$\log_{10} x = \dfrac {\ln x} {\ln 10}$
as by definition of $\ln x$:
:$\ln x := \log_e x$
The Natural Logarithm of 10:
:$\ln 10 = 2 \cdotp 30258 \, 50929 \, 94 \ldots$
can then be calculated or looked up.
{{qed}}
Theorem: Change of Base of Logarithm/Base 10 to Base 2

:$\lg x = \dfrac {\log_{10} x} {\log_{10} 2} = \dfrac {\log_{10} x} {0 \cdotp 30102 \, 99956 \, 63981 \, 19521 \, 37389 \ldots}$

Proof:
From Change of Base of Logarithm:
:$\log_a x = \dfrac {\log_b x} {\log_b a}$
Substituting $a = e$ and $b = 10$ gives:
:$\log_e x = \dfrac {\log_{10} x} {\log_{10} e}$
The Common Logarithm of 2:
:$\log_{10} 2 = 0 \cdotp 30102 \, 99956 \, 63981 \, 19521 \, 37389 \ldots$
can then be calculated or looked up.
{{qed}}
Category:Examples of Common Logarithms
Category:Examples of Binary Logarithms
Category:Examples of Change of Base of Logarithm
etifvsevdac1nxxs8fz4g3nk62chban
Theorem: Root of Quotient equals Quotient of Roots

:$\sqrt [n] {\dfrac a b} = \dfrac {\sqrt [n] a} {\sqrt [n] b}$

Proof:
{{begin-eqn}}
{{eqn | l = \sqrt [n] {\dfrac a b}
      | r = \paren {\dfrac a b}^{1 / n}
      | c = {{Defof|Root of Number|$n$th Root}}
}}
{{eqn | r = \paren {a \times \dfrac 1 b}^{1 / n}
      | c = 
}}
{{eqn | r = a^{1 / n} \times \paren {\dfrac 1 b}^{1 / n}
      | c = Power of Product
}}
{{eqn | r = a^{1 / n} \times b^{-1 / n}
      | c = Exponent Combination Laws/Negative Power
}}
{{eqn | r = a^{1 / n} \times \dfrac 1 {b^{1 / n} }
      | c = Exponent Combination Laws/Negative Power
}}
{{eqn | r = \sqrt [n] a \times \dfrac 1 {\sqrt [n] b}
      | c = {{Defof|Root of Number|$n$th Root}}
}}
{{eqn | r = \dfrac {\sqrt [n] a} {\sqrt [n] b}
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Logarithm to Own Base equals 1

Let $b \in \R_{>0}$ be a strictly positive real number such that $b \ne 1$.
Let $\log_b$ denote the logarithm to base $b$.
Then:
:$\log_b b = 1$

Proof:
By definition of logarithm:
{{begin-eqn}}
{{eqn | l = y
      | r = \log_b b
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | l = b^y
      | r = b
      | c = {{Defof|Real General Logarithm}}
}}
{{eqn | ll= \leadstoandfrom
      | l = y
      | r = 1
      | c = {{Defof|Power to Real Number}}
}}
{{end-eqn}}
{{qed}}
Category:Logarithms
nzbjueziu6rt7577su6ztppps8eck02
Theorem: General Logarithm/Examples/Base b of 1

:$\log_b 1 = 0$

Proof:
By definition of logarithm:
{{begin-eqn}}
{{eqn | l = \log_b 1
      | r = \frac {\log_e 1} {\log_e b}
      | c = Change of Base of Logarithm
}}
{{eqn | r = \frac 0 {\log_e b}
      | c = Natural Logarithm of 1 is 0
}}
{{eqn | r = 0
      | c = whatever $\log_e b$ happens to be
}}
{{end-eqn}}
{{qed}}
Theorem: General Logarithm/Examples/Base b of -1

:$\log_b \left({-1}\right)$ is undefined in the real number line.

Proof:
{{AimForCont}} $\log_b \left({-1}\right) = y \in \R$.
Then:
:$b^y = -1 < 0$
But from Power of Positive Real Number is Positive:
:$b^y > 0$
The result follows by Proof by Contradiction.
{{qed}}
Theorem: Change of Base of Logarithm/Base 2 to Base 8

:$\log_8 x = \dfrac {\lg x} 3$

Proof:
From Change of Base of Logarithm:
:$\log_a x = \dfrac {\log_b x} {\log_b a}$
Substituting $a = 8$ and $b = 2$ gives:
:$\log_8 x = \dfrac {\log_2 x} {\log_2 8}$
We have that:
{{begin-eqn}}
{{eqn | l = 2^3
      | r = 8
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \lg 8
      | r = \log_2 2^3
      | c = 
}}
{{eqn | r = 3 \log_2 2
      | c = 
}}
{{eqn | r = 3
      | c = Logarithm to Own Base equals 1
}}
{{end-eqn}}
The result follows.
{{qed}}