avewright/proofwiki-math huggingface dataset:
Theorem: Scaled Real Function that Decreases Without Bound

Let $f: \R \to \R$ be a real function.
Let $\lambda \in \R_{\ne 0}$ be a nonzero constant.
Then:
For $\lambda > 0$:
:$\ds \lim_{x \mathop \to +\infty} \map f x = -\infty \implies \lim_{x \mathop \to +\infty} \lambda \map f x = -\infty$
:$\ds \lim_{x \mathop \to -\infty} \map f x = -\infty \implies \lim_{x \mathop \to -\infty} \lambda \map f x = -\infty$
For $\lambda < 0$:
:$\ds \lim_{x \mathop \to +\infty} \map f x = -\infty \implies \lim_{x \mathop \to +\infty} \lambda \map f x = +\infty$
:$\ds \lim_{x \mathop \to -\infty} \map f x = -\infty \implies \lim_{x \mathop \to -\infty} \lambda \map f x = +\infty$

Proof:
Let $\ds \lim_{x \mathop \to +\infty} \map f x = -\infty$.
From the definition of infinite limits at infinity, this means that:
:$\forall M < 0: \exists N > 0: x > N \implies \map f x < M$
Suppose $\lambda > 0$.
Then $M < 0 \iff \lambda^{-1}M < 0$.
Also, $\map f x < \lambda^{-1}M \iff \lambda \map f x < M$
So:
:$\forall M < 0: \exists N > 0: x > N \implies \lambda \map f x < M$
From the definition of infinite limits at infinity:
:$\ds \lim_{x \mathop \to +\infty} \lambda \map f x = -\infty$
The proof for $\ds \lim_{x \mathop \to -\infty} \map f x = -\infty$ is analogous.
Now, suppose $\lambda < 0$.
Then $-\lambda f < 0$, and so $-\lambda f \to -\infty$, from above.
Write $\lambda f = -\paren {-\lambda f}$ and the result follows from Negative of Real Function that Decreases Without Bound.
{{qed}}
Theorem: Existence of Fraction of Number Smaller than Given

Let $a, b \in \R_{>0}$ be two (strictly) positive real numbers, such that $a > b$.
Let the sequence $\sequence {a_n}$ be defined recursively as:
:$a_i = \begin{cases} a & : i = 1 \\
a_{i - 1} - c: \dfrac {a_{i - 1} } 2 < c < a_{i - 1} & : i > 1
\end{cases}$
Then:
: $\exists n \in \N_{>0}: a_n < b$
{{:Euclid:Proposition/X/1}}

Proof:
:400px
Let $AB$ and $C$ be two unequal magnitudes such that $AB > C$.
From {{EuclidDefLink|V|4|Existence of Ratio}} there exists a multiple of $C$ which is greater than $AB$.
Thus let $DE$ be a multiple of $C$ which is greater than $AB$.
Let $DE$ be divided into parts $DF$, $FG$ and $GE$ (for example) which are equal to $C$.
From $AB$ let $BH$ be subtracted which is greater than half $AB$.
From $AH$ let $HK$ be subtracted which is greater than half $AH$.
Let this process be continued until the divisions of $AB$ are equal in number to the divisions of $DE$.
Let $AK, KH, HB$ be divisions which are equal in number to $DF, FG, GE$.
We have that $DE > AB$.
From $DE$ there has been subtracted $EG$ which is less than half $DE$.
From $AB$ there has been subtracted $BH$ which is greater than half $AB$.
Therefore the remainder $GD$ of $DE$ is greater than the remainder $HA$ of $AB$.
From $GD$ there has been subtracted $GF$ which is half $GD$.
From $HA$ there has been subtracted $HK$ which is greater than half $HA$.
Therefore the remainder $DF$ of $GD$ is greater than the remainder $AK$ of $HA$.
But $DF = C$.
Therefore $C > AK$.
Therefore there is left of the magnitude $AB$ the magnitude $AK$ which is less than the lesser magnitude set out, which is $C$.
{{qed}}
{{Euclid Note|1|X}}
Theorem: Lines Through Endpoints of One Side of Triangle to Point Inside Triangle is Less than Sum of Other Sides/Corollary

The angle between the two line segments from the endpoints of one side to a point inside the triangle is greater than the angle between the other two sides of the triangle.

Proof:
:250px
From External Angle of Triangle is Greater than Internal Opposite:
:$\angle BDC > \angle CED$
Similarly:
: $\angle CEB > \angle BEC$
Since $\angle CED$ is the same angle as $\angle CEB$:
: $\angle BDC > \angle CEB > \angle BEC$
{{qed}}
{{Euclid Note|21|I}}
Theorem: Restriction of Continuous Mapping is Continuous/Topological Spaces

Let $T_1 = \struct {S_1, \tau_1}$ and $T_2 = \struct {S_2, \tau_2}$ be topological spaces.
Let $M_1 \subseteq S_1$ be a subset of $S_1$.
Let $f: S_1 \to S_2$ be a mapping which is continuous.
Let $M_2 \subseteq S_2$ be a subset of $S_2$ such that $f \sqbrk {M_1} \subseteq M_2$.
Let $f \restriction_{M_1 \times M_2}: M_1 \to M_2$ be the restriction of $f$ to $M_1 \times M_2$.
Then $f \restriction_{M_1 \times M_2}$ is continuous, where $M_1$ and $M_2$ are equipped with the respective subspace topologies.

Proof:
Consider first the restriction $f \restriction_{M_1}$.
From Composition of Mapping with Inclusion is Restriction:
:$f \restriction_{M_1} = f \circ i_{M_1}$
where $i_{M_1}$ is the inclusion of $M_1$ into $S_1$.
From Continuity of Composite with Inclusion: Mapping on Inclusion, it follows that $f \circ i_{M_1} = f \restriction_{M_1}$ is continuous.
{{qed|lemma}}
Consider now a mapping $\tilde f : S_1 \to M_2$ where $f \sqbrk {S_1} \subseteq M_2$
Then:
$f = i_{M_2} \circ \tilde f$
where $i_{M_2}$ is the inclusion of $M_2$ into $S_2$.
From Continuity of Composite with Inclusion: Inclusion on Mapping, it follows that $\tilde f$ is continuous {{iff}} $i_{M_2} \circ \tilde f = f$ is continuous.
Thus $\tilde f$ is continuous, since $f$ is continuous by assumption.
{{qed|lemma}}
The result follows from combining these partial results.
{{qed}}
Theorem: Restriction of Continuous Mapping is Continuous/Metric Spaces

Let $M_1 = \struct {A_1, d_1}$ and $M_2 = \struct {A_2, d_2}$ be metric spaces.
Let $S \subseteq M_1$ be a subset of $M_1$.
Let $f: M_1 \to M_2$ be a mapping which is continuous at a point $\alpha \in S$.
Let $f \restriction_S = g: S \to M_2$ be the restriction of $f$ to $S$.
Then $g$ is continuous at $\alpha$.

Proof:
Let $\sequence {z_n}$ be a sequence in $S$ such that:
:$\ds \lim_{n \mathop \to \infty} z_n = \alpha$
Since $\sequence {z_n}$ and $\alpha$ both lie in $S$:
:$\ds \lim_{n \mathop \to \infty} \map f {z_n} \to \alpha$
But:
:$\forall n \in \N: \map g {z_n} = \map f {z_n}$
and also:
:$\map g \alpha = \map f \alpha$
The result follows from Limit of Function by Convergent Sequences.
{{qed}}
Category:Metric Spaces
Category:Continuous Mappings on Metric Spaces
huwv9n8w1q3ywxoifmu65syrajilw8h
Theorem: Restriction of Homeomorphism is Homeomorphism

Let $T_1 = \struct {S_1, \tau_1}$, $T_2 = \struct {S_2, \tau_2}$ be topological spaces.
Let $f: S_1 \to S_2$ be a homeomorphism between $T_1$ and $T_2$.
Let $S$ be a subset of $S_1$.
Let $f {\restriction_{S \times f \sqbrk S} } : S \to f \sqbrk S$ be the restriction of $f$ to $S \times f \sqbrk S$.
Let $S$ and $f \sqbrk S$ bear their respective subspace topologies.
Then $f {\restriction_{S \times f \sqbrk S} }$ is a homeomorphism.

Proof:
By Restriction of Continuous Mapping is Continuous, $f {\restriction_{S \times f \sqbrk S} }$ is continuous.
By Restriction of Inverse is Inverse of Restriction, $\left({f {\restriction_{S \times f \sqbrk S} } }\right)^{-1}$ is well-defined and equal to $f^{-1} {\restriction_{f \sqbrk S \times S} }$.
By Restriction of Continuous Mapping is Continuous, $f^{-1} {\restriction_{f \sqbrk S \times S} }$ is continuous.
Since $\paren {f {\restriction_{S \times f \sqbrk S} } }^{-1} = f^{-1} {\restriction_{f \sqbrk S \times S} }$, $\paren {f {\restriction_{S \times f \sqbrk S} } }^{-1}$ is continuous.
Hence, $f {\restriction_{S \times f \sqbrk S} }$ is a homeomorphism.
{{qed}}
Theorem: Hölder's Inequality for Integrals/General

Let $\struct {X, \Sigma, \mu}$ be a measure space.
For $i = 1, \ldots, n$ let $p_i \in \R_{>0}$ such that:
:$\ds \sum_{i \mathop = 1}^n \frac 1 {p_i} = 1$
Let $f_i \in \map {\LL^{p_i} } \mu, f_i: X \to \R$, where $\LL$ denotes Lebesgue space.
Then their pointwise product $\ds \prod_{i \mathop = 1}^n f_i$ is integrable, that is:
:$\ds \prod_{i \mathop = 1}^n f_i \in \map {\LL^1} \mu$
and:
:$\ds \norm {\prod_{i \mathop = 1}^n f_i}_1 = \int \size {\prod_{i \mathop = 1}^n f_i} \rd \mu \le \prod_{i \mathop = 1}^n \norm {f_i}_{p_i}$
where the various instances of $\norm {\, \cdot \,}$ signify $p$-seminorms.

Proof:
{{explain|Has it been demonstrated for $i {{=}} 1$? Best if this were put into the house style of induction proofs.}}
We use the Principle of Mathematical Induction.
Let it be assumed that the result holds for $i = n - 1$.
We show that the result holds for $i = n$. 
Define:
:$q_n := \dfrac {p_n} {p_n - 1}$
and for $i = 1, \ldots, n - 1$, define:
:$r_i := p_i \cdot \paren {1 - \dfrac 1 {p_n} }$
Then:
:$\dfrac 1 {p_n} + \dfrac 1 {q_n} = 1$
:$\ds \sum_{i \mathop = 1}^{n - 1} \dfrac 1 {r_i} = 1$
and:
:$q_n \cdot r_i = p_i$
Applying Hölder's Inequality for Integrals to $\ds f := \prod_{i \mathop = 1}^{n - 1} f_i$ and $g := f_n$, we find:
{{begin-eqn}}
{{eqn | l = \int \size {\prod_{i \mathop = 1}^n f_i} \rd \mu
      | o = \le
      | r = \norm {f_n}_{p_n} \cdot \norm {\prod_{i \mathop = 1}^{n - 1} f_i}_{q_n}
      | c = 
}}
{{eqn | r = \norm {f_n}_{p_n} \cdot \paren {\int \prod_{i \mathop = 1}^{n - 1} \size { {f_i}^{q_n} } \rd \mu}^\frac 1 {q_n}
      | c = 
}}
{{eqn | o = \le
      | r = \norm {f_n}_{p_n} \cdot \paren {\prod_{i \mathop = 1}^{n-1} \norm { {f_i}^{q_n} }_{r_i} }^\frac 1 {q_n}
      | c = 
}}
{{eqn | r = \prod_{i \mathop = 1}^n \norm {f_i}_{p_i}
      | c = 
}}
{{end-eqn}}
{{qed}}
{{Namedfor|Otto Ludwig Hölder}}
Category:Hölder's Inequality for Integrals
blc1eixcorw4gn7sccvfomcmr313hfa
Theorem: Theorem of Even Perfect Numbers/Sufficient Condition

Let $n \in \N$ be such that $2^n - 1$ is prime.
Then $2^{n - 1} \paren {2^n - 1}$ is perfect.
{{:Euclid:Proposition/IX/36}}

Proof:
Suppose $2^n - 1$ is prime.
Let $a = 2^{n - 1} \paren {2^n - 1}$.
Then $n \ge 2$ which means $2^{n - 1}$ is even and hence so is $a = 2^{n - 1} \paren {2^n - 1}$.
Note that $2^n - 1$ is odd.
Since all divisors (except $1$) of $2^{n - 1}$ are even it follows that $2^{n - 1}$ and $2^n - 1$ are coprime.
Let $\map {\sigma_1} n$ be the divisor sum of $n$, that is, the sum of all divisors of $n$ (including $n$).
From Divisor Sum Function is Multiplicative, it follows that $\map {\sigma_1} a = \map {\sigma_1} {2^{n - 1} } \map {\sigma_1} {2^n - 1}$.
But as $2^n - 1$ is prime, $\map {\sigma_1} {2^n - 1} = 2^n$ from Divisor Sum of Prime Number.
Then we have that $\map {\sigma_1} {2^{n - 1} } = 2^n - 1$ from Divisor Sum of Power of Prime.
Hence it follows that $\map {\sigma_1} a = \paren {2^n - 1} 2^n = 2 a$.
Hence from the definition of perfect number it follows that $2^{n - 1} \paren {2^n - 1}$ is perfect.
Theorem: Theorem of Even Perfect Numbers/Necessary Condition

Let $a \in \N$ be an even perfect number.
Then $a$ is in the form:
:$2^{n - 1} \paren {2^n - 1}$
where $2^n - 1$ is prime.

Proof:
Let $a \in \N$ be an even perfect number.
We can extract the highest power of $2$ out of $a$ that we can, and write $a$ in the form:
:$a = m 2^{n - 1}$
where $n \ge 2$ and $m$ is odd.
Since $a$ is perfect and therefore $\map {\sigma_1} a = 2 a$:
{{begin-eqn}}     
{{eqn| l = m 2^n
     | r = 2 a
     | c =
}}
{{eqn| r = \map {\sigma_1} a
     | c =
}}
{{eqn| r = \map {\sigma_1} {m 2^{n - 1} }
     | c =
}}
{{eqn| r = \map {\sigma_1} m \map {\sigma_1} {2^{n - 1} }
     | c = Divisor Sum Function is Multiplicative
}}
{{eqn| r = \map {\sigma_1} m \paren {2^n - 1}
     | c = Divisor Sum of Power of Prime
}}
{{end-eqn}}
So:
:$\map {\sigma_1} m = \dfrac {m 2^n} {2^n - 1}$
But $\map {\sigma_1} m$ is an integer and so $2^n - 1$ divides $m 2^n$.
From Consecutive Integers are Coprime, $2^n$ and $2^n - 1$ are coprime.
So from Euclid's Lemma $2^n - 1$ divides $m$.
Thus $\dfrac m {2^n - 1}$ divides $m$.
Since $2^n - 1 \ge 3$ it follows that:
:$\dfrac m {2^n - 1} < m$
Now we can express $\map {\sigma_1} m$ as:
:$\map {\sigma_1} m = \dfrac {m 2^n} {2^n - 1} = m + \dfrac m {2^n - 1}$
This means that the sum of all the divisors of $m$ is equal to $m$ itself plus one other divisor of $m$.
Hence $m$ must have exactly two divisors, so it must be prime by definition.
This means that the other divisor of $m$, apart from $m$ itself, must be $1$.
That is:
:$\dfrac m {2^n - 1} = 1$
Hence the result.
{{qed}}
Theorem: Condition for Commensurability of Roots of Quadratic Equation

Consider the quadratic equation:
:$(1): \quad a x - x^2 = \dfrac {b^2} 4$
Then $x$ and $a - x$ are commensurable {{iff}} $\sqrt{a^2 - b^2}$ and $a$ are commensurable.
{{:Euclid:Proposition/X/17}}

Proof:
We have that:
{{begin-eqn}}
{{eqn | l = x \paren {a - x} + \paren {\frac a 2 - x}^2
      | r = a x - x^2 + \frac {a^2} 4 - 2 \frac a 2 x + x^2
      | c = 
}}
{{eqn | r = \frac {a^2} 4
      | c = simplifying
}}
{{eqn | ll= \leadsto
      | l = 4 x \paren {a - x} + 4 \paren {\frac a 2 - x}^2
      | r = a^2
      | c = 
}}
{{eqn | ll= \leadsto
      | l = b^2 + \paren {a - 2 x}^2
      | r = a^2
      | c = from $(1)$
}}
{{eqn | ll= \leadsto
      | l = a^2 - b^2
      | r = \paren {a - 2 x}^2
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \sqrt {a^2 - b^2}
      | r = a - 2 x
      | c = 
}}
{{end-eqn}}
Let $a \frown b$ denote that $a$ is commensurable with $b$.
Theorem: Condition for Incommensurability of Roots of Quadratic Equation

Consider the quadratic equation:
:$(1): \quad a x - x^2 = \dfrac {b^2} 4$
Then $x$ and $a - x$ are incommensurable {{iff}} $\sqrt {a^2 - b^2}$ and $a$ are incommensurable.
{{:Euclid:Proposition/X/18}}

Proof:
We have that:
{{begin-eqn}}
{{eqn | l = x \paren {a - x} + \paren {\frac a 2 - x}^2
      | r = a x - x^2 + \frac {a^2} 4 - 2 \frac a 2 x + x^2
      | c = 
}}
{{eqn | r = \frac {a^2} 4
      | c = simplifying
}}
{{eqn | ll= \leadsto
      | l = 4 x \paren {a - x} + 4 \paren {\frac a 2 - x}^2
      | r = a^2
      | c = 
}}
{{eqn | ll= \leadsto
      | l = b^2 + \paren {a - 2 x}^2
      | r = a^2
      | c = from $(1)$
}}
{{eqn | ll= \leadsto
      | l = a^2 - b^2
      | r = \paren {a - 2 x}^2
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \sqrt {a^2 - b^2}
      | r = a - 2 x
      | c = 
}}
{{end-eqn}}
Let:
:$a \smile b$ denote that $a$ is incommensurable with $b$
:$a \frown b$ denote that $a$ is commensurable with $b$.
Theorem: Apotome is Irrational

Every apotome is irrational, i.e.:
:$\ds \forall a, b \in \set {x \in \R_{>0} : x^2 \in \Q}: \paren {\frac a b \notin \Q \land \paren {\frac a b}^2 \in \Q} \implies \paren {\paren {a - b} \notin \Q \land \paren {a - b}^2 \notin \Q}$
{{:Euclid:Proposition/X/73}}

Proof:
:300px
Let $AB$ be a rational straight line.
Let a rational straight line $BC$ which is commensurable in square only with $AB$ be cut off from $AB$.
We have that $AB$ is incommensurable in length with $BC$.
We also have:
:$AB : BC = AB^2 : AB \cdot AC$
Therefore from {{EuclidPropLink|book = X|prop = 11|title = Commensurability of Elements of Proportional Magnitudes}}:
:$AB^2$ is incommensurable with $AB \cdot AC$.
But from {{EuclidPropLink|book = X|prop = 15|title = Commensurability of Sum of Commensurable Magnitudes}}:
:$AB^2 + BC^2$ is commensurable with $AB^2$.
and from {{EuclidPropLink|book = X|prop = 6|title = Magnitudes with Rational Ratio are Commensurable}}:
:$2 \cdot AB \cdot AC$ is commensurable with $AB \cdot AC$.
From {{EuclidPropLink|book = II|prop = 7|title = Square of Difference}}:
:$AB^2 + BC^2 = 2 \cdot AB \cdot AC + CA^2$
and so from:
:{{EuclidPropLink|book = X|prop = 13|title = Commensurable Magnitudes are Incommensurable with Same Magnitude}}
and:
:{{EuclidPropLink|book = X|prop = 16|title = Incommensurability of Sum of Incommensurable Magnitudes}}
it follows that:
:$AB^2 + BC^2$ is incommensurable with $AC^2$.
But $AB$ and $BC$ are rational.
Therefore $AC$ is irrational.
Such a straight line is known as an apotome.
{{qed}}
{{Euclid Note|73|X}}
Theorem: Construction of Apotome is Unique

Let $D$ be the domain $\left\{{x \in \R_{>0} : x^2 \in \Q}\right\}$, the rationally expressible numbers.
Let $a, b \in D$ be two rationally expressible numbers such that $a - b$ is an apotome.
Then, there exists only one $x \in D$ such that $a - b + x$ and $a$ are commensurable in square only.
{{:Euclid:Proposition/X/79}}

Proof:
:300px
Let $AB$ be an apotome.
Let $BC$ be added to $AB$ so that $AC$ and $CB$ are rational straight lines which are commensurable in square only.
It is to be proved that no other rational straight line can be added to $AB$ which is commensurable in square only with the whole.
Suppose $BD$ can be added to $AB$ so as to fulfil the conditions stated.
Then $AD$ and $DB$ are rational straight lines which are commensurable in square only.
From {{EuclidPropLink|book = II|prop = 7|title = Square of Difference}}:
:$AD^2 + DB^2 - 2 \cdot AD \cdot DB = AC^2 + CB^2 - 2 \cdot AC \cdot CB = AB^2$
Therefore:
:$AD^2 + DB^2 - AC^2 + CB^2 = 2 \cdot AD \cdot DB - 2 \cdot AC \cdot CB$
But $AD^2 + DB^2$ and $AC^2 + CB^2$ are both rational.
Therefore $AD^2 + DB^2 - AC^2 + CB^2$ is rational.
Therefore $2 \cdot AD \cdot DB - 2 \cdot AC \cdot CB$ is rational.
But from {{EuclidPropLink|book = X|prop = 21|title = Medial is Irrational}}:
:$2 \cdot AD \cdot DB$ and $2 \cdot AC \cdot CB$ are both medial.
From {{EuclidPropLink|book = X|prop = 26|title = Medial Area not greater than Medial Area by Rational Area}}:
:a medial area does not exceed a medial area by a rational area.
Therefore no other rational straight line can be added to $AB$ which is commensurable in square only with the whole.
Therefore only one rational straight line can be added to $AB$ which is commensurable in square only with the whole.
{{qed}}
{{Euclid Note|79|X}}
Theorem: Lower Bound of Natural Logarithm

:$\forall x \in \R_{>0}: 1 - \dfrac 1 x \le \ln x$
where $\ln x$ denotes the natural logarithm of $x$.

Proof:
Let $x > 0$.
{{begin-eqn}}
{{eqn | l = x - 1 
      | o = \ge
      | r = \ln x
      | c = Upper Bound of Natural Logarithm
}}
{{eqn | ll= \leadsto
      | l = \frac 1 x -1
      | o = \ge
      | r = \ln \frac 1 x
      | c = putting $\frac 1 x$ into the above inequality
}}
{{eqn | r = -\ln x
      | c = Logarithm of Reciprocal
}}
{{eqn | ll= \leadsto
      | l = 1 - \frac 1 x
      | o = \le
      | r = \ln x
      | c = multiplying throughout by $-1$
}}
{{end-eqn}}
{{qed}}
Theorem: Lower Bound of Natural Logarithm

:$\forall x \in \R_{>0}: 1 - \dfrac 1 x \le \ln x$
where $\ln x$ denotes the natural logarithm of $x$.

Proof:
Let $x > 0$.
Note that:
:$1 - \dfrac 1 x \le \ln x$
is logically equivalent to:
:$1 - \dfrac 1 x - \ln x \le 0$
Let $\map f x = 1 - \dfrac 1 x - \ln x$.
Then:
{{begin-eqn}}
{{eqn | l = \map f x
      | r = 1 - \dfrac 1 x - \ln x
}}
{{eqn | ll= \leadsto
      | l = \map {f'} x
      | r = \frac 1 {x^2} - \frac 1 x
      | c = Derivative of Constant, Power Rule for Derivatives, Derivative of Natural Logarithm Function
}}
{{eqn | r = \frac {1 - x} {x^2}
}}
{{eqn | ll= \leadsto
      | l = \map {f' '} x
      | r = - \frac 2 {x^3} + \frac 1 {x^2}
      | c = Power Rule for Derivatives
}}
{{end-eqn}} 
Note that $\map {f'} 1 = 0$.
Also, $\map {f' '} 1 < 0$.
So by the Second Derivative Test, $x = 1$ is a local maximum.
On $\openint 0 1$:
:$\map {f'} x > 0$
By Derivative of Monotone Function, $f$ is strictly increasing on that interval.
On $\openint 1 \to$:
:$\map {f'} x < 0$
By Derivative of Monotone Function, $f$ is strictly decreasing on that interval.
So $x = 1$ yields an absolute maximum, at which by Logarithm of 1 is 0:
:$\map f 1 = 1 - 1 - 0 = 0$
That is:
:$\forall x > 0: \map f x \le 0$
and so by definition of $\map f x$:
:$1 - \dfrac 1 x - \ln x \le 0$
{{qed}}
Theorem: Lower Bound of Natural Logarithm

:$\forall x \in \R_{>0}: 1 - \dfrac 1 x \le \ln x$
where $\ln x$ denotes the natural logarithm of $x$.

Proof:
Let $\sequence {f_n}$ be the sequence of mappings $f_n: \R_{>0} \to \R$ defined as:
:$\map {f_n} x = n \paren {\sqrt [n] x - 1 }$
Let $x \in \R_{>0}$ be fixed.
We first show that:
:$\forall n \in \N : 1 - \dfrac 1 x \le n \paren {\sqrt [n] x - 1}$
Let $n \in \N$.
From Sum of Geometric Sequence:
:$\sqrt [n] x - 1 = \dfrac {x - 1} {1 + \sqrt [n] x + \sqrt [n] x^2 + \cdots + \sqrt [n] x^{n - 1} }$
=== Case 1: $0 < x < 1$ ===
{{begin-eqn}}
{{eqn | l = 0 < x < 1
      | o = \leadsto
      | r = \forall k < n: \sqrt [n] x^{n - k} > x > 0
      | c = Power Function on Base between Zero and One is Strictly Decreasing/Rational Number
}}
{{eqn | o = \leadsto
      | r = 0 < n x < \sum_{k = 0}^{n - 1} \sqrt [n] x^{n - k}
      | c = Real Number Ordering is Compatible with Addition
}}
{{eqn | o = \leadsto
      | r = \dfrac 1 {1 + \sqrt [n] x + \sqrt [n] x^2 + \cdots + \sqrt [n] x^{n - 1} } > \dfrac 1 {n x}
      | c = Ordering of Reciprocals
}}
{{eqn | o = \leadsto
      | r = \dfrac {x - 1} {n x} < \dfrac {x - 1} {1 + \sqrt [n] x + \sqrt [n] x^2 + \cdots + \sqrt [n] x^{n - 1} }
      | c = Order of Real Numbers is Dual of Order of their Negatives
}}
{{eqn | o = \leadsto
      | r = \dfrac {x - 1} {n x} < \sqrt [n] x - 1
      | c = Sum of Geometric Sequence
}}
{{eqn | o = \leadsto
      | r = 1 - \dfrac 1 x < n \paren {\sqrt [n] x - 1}
      | c = Real Number Ordering is Compatible with Multiplication
}}
{{end-eqn}}
{{qed|lemma}}
=== Case 2: $x = 1$ ===
{{begin-eqn}}
{{eqn | l = \dfrac {x - 1} x
      | r = 0
}}
{{eqn | r = \sqrt [n] 1 - 1
}}
{{end-eqn}}
{{qed|lemma}}
=== Case 3: $x > 1$ ===
{{begin-eqn}}
{{eqn | l = x > 1
      | o = \leadsto
      | r = \forall k < n: 1 < \sqrt [n] x^{n - k} < x
      | c = Power Function on Base Greater than One is Strictly Increasing/Rational Number
}}
{{eqn | o = \leadsto
      | r = 0 < \sum_{k \mathop = 0}^{n - 1} \sqrt [n] x^{n - k} < n x
      | c = Real Number Ordering is Compatible with Addition
}}
{{eqn | o = \leadsto
      | r = 0 < \dfrac 1 {n x} < \dfrac 1 {1 + \sqrt [n] x + \sqrt [n] x^2 + \cdots + \sqrt [n] x^{n - 1} }
      | c = Ordering of Reciprocals
}}
{{eqn | o = \leadsto
      | r = \dfrac {x - 1} {n x} < \dfrac {x - 1} {1 + \sqrt [n] x + \sqrt [n] x^2 + \cdots + \sqrt [n] x^{n - 1} }
      | c = Real Number Ordering is Compatible with Multiplication
}}
{{eqn | o = \leadsto
      | r = \dfrac {x - 1} {n x} < \sqrt [n] x - 1
      | c = Sum of Geometric Sequence
}}
{{eqn | o = \leadsto
      | r = 1 - \dfrac 1 x < n \paren {\sqrt [n] x - 1 }
      | c = Real Number Ordering is Compatible with Multiplication
}}
{{end-eqn}}
{{qed|lemma}}
Thus:
:$\forall n \in \N : 1 - \dfrac 1 x \le n \paren {\sqrt [n] x - 1 }$
by Proof by Cases.
Thus:
:$\ds 1 - \dfrac 1 x \le \lim_{n \mathop \to \infty} n \paren {\sqrt [n] x - 1 }$
from Limit of Bounded Convergent Sequence is Bounded.
Hence the result, from the definition of $\ln$.
{{qed}}
Theorem: Bounds of Natural Logarithm

300pxthumbright
Let $\ln x$ be the natural logarithm of $x$ where $x \in \R_{>0}$.
Then $\ln$ satisfies the compound inequality:
:$1 - \dfrac 1 x \le \ln x \le x - 1$

Proof:
From Upper Bound of Natural Logarithm:
:$\ln x \le x - 1$
From Lower Bound of Natural Logarithm:
:$1 - \dfrac 1 x \le \ln x$
{{qed}}
Theorem: Mordell's Theorem

Let $C$ be an elliptic curve over $\Q$.
Then the group of rational points on $C$ is a finitely generated abelian group.

Proof:
{{ProofWanted}}
{{Namedfor|Louis Joel Mordell|cat = Mordell}}
Theorem: Common Ratio in Rational Geometric Sequence is Rational

Let $\sequence {a_k}$ be a geometric sequence whose terms are rational.
Then the common ratio of $\sequence {a_k}$ is rational.

Proof:
Let $r$ be the common ratio of $\sequence {a_k}$.
Let $p, q$ be consecutive terms of $r$.
We have {{hypothesis}} that:
:$p, q \in \Q$
Then, by definition of geometric sequence:
:$q = r p$
It follows that:
:$r = \dfrac q p$
From Rational Numbers form Field, $\Q$ is closed under division.
Thus $r \in \Q$ and hence the result.
{{qed}}
Category:Geometric Sequences
k3o31xwnbtpg026l08ditalhdmcmntr
Theorem: Common Ratio in Integer Geometric Sequence is Rational

Let $\sequence {a_k}$ be a geometric sequence whose terms are all integers.
Then the common ratio of $\sequence {a_k}$ is rational.

Proof:
From Integers form Subdomain of Rationals it follows that $a_k \in \Q$ for all $0 \le k \le n$.
The result follows from Common Ratio in Rational Geometric Sequence is Rational.
{{qed}}
Category:Geometric Sequences of Integers
0qft406itmha5ood9xvu2bzzz0xivkq