nyuuzyou/wikis huggingface dataset:
Dedekind's Theorem/Proof 2

== Theorem ==
== Proof ==
=== Proof of Uniqueness ===
 both $\alpha$ and $\beta$ produce $\tuple {L, R}$.
By the Trichotomy Law for Real Numbers either $\beta < \alpha$ or $\alpha < \beta$.
Suppose that $\beta < \alpha$.
From Real Numbers are Densely Ordered, there exists at least one real number $c$ such that $\beta < c$ and $c < \alpha$.
Because $c < \alpha$, it must be the case that $c \in L$.
Because $\beta < c$, it must be the case that $c \in R$.
That is:
:$c \in L \cap R$
But by the definition of Dedekind Cut, $\tuple {L, R}$ is a partition of $\R$.
That is, $L$ and $R$ are disjoint.
That is:
:$L \cap R = \O$
This is a contradiction.
Similarly, $\alpha < \beta$ also leads to a contradiction.
It follows that $\alpha$ is unique.
=== Proof of Existence ===
Let $\alpha = \sup L$.
Let $u_1 \in \R$ such that $u_1 < \alpha$.
 $u_1 \in R$.
Suppose there is no real number $s \in L$ such that $u_1 < s \le \alpha$.
Then $u_1$ would be an upper bound of $L$ which is less than $\sup {L}$.
This is a contradiction.
So there exists at least one real number $s \in L$ such that $u_1 < s \le \alpha$.
But this is also a contradiction because all the elements of $R$ are greater than all the elements of $L$.
It follows that $u_1 \in L$.
Let $u_2 \in \R$ such that $\alpha < u_2$.
 $u_2 \in L$.
There exists $s' \in \R$ such that $\alpha < s' < u_2$.
But $s' \notin L$ and thus $s' \in R$.
This is a contradiction because all the elements of $R$ are greater than all the elements of $L$.
It follows that $u_2 \in R$.
Hence, $\alpha$ produces the cut $\tuple {L, R}$.
Category:Dedekind's Theorem
Dedekind's Theorem/Proof 3

== Theorem ==
== Proof ==
=== Proof of Uniqueness ===
 both $\alpha$ and $\beta$ produce $\tuple {L, R}$.
By the Trichotomy Law for Real Numbers either $\beta < \alpha$ or $\alpha < \beta$.
Suppose that $\beta < \alpha$.
From Real Numbers are Densely Ordered, there exists at least one real number $c$ such that $\beta < c$ and $c < \alpha$.
Because $c < \alpha$, it must be the case that $c \in L$.
Because $\beta < c$, it must be the case that $c \in R$.
That is:
:$c \in L \cap R$
But by the definition of Dedekind Cut, $\tuple {L, R}$ is a partition of $\R$.
That is, $L$ and $R$ are disjoint.
That is:
:$L \cap R = \O$
This is a contradiction.
Similarly, $\alpha < \beta$ also leads to a contradiction.
It follows that $\alpha$ is unique.
=== Proof of Existence ===
Let $\gamma$ be the set of all rational numbers $p$ such that $p \in \alpha$ for some $\alpha \in L$.
It is to be verified that $\gamma$ is a cut.
Because $L$ is not empty, neither is $\gamma$.
Suppose $\beta \in \R$ and $q \notin \beta$.
Then because $\alpha < \beta$, we have that $q \notin \alpha$ for any $\alpha \in L$.
Thus $q \notin \gamma$.
Thus $\gamma$ satisfies criterion $(1)$ for being a cut.
Suppose $p \in \gamma$ and $q < p$.
Then $p \in \alpha$ for some $\alpha \in L$.
Hence $q \in \alpha$.
Hence $q \in \gamma$.
Thus $\gamma$ satisfies criterion $(2)$ for being a cut.
Suppose $p \in \gamma$.
Then $p \in \alpha$ for some $\alpha \in L$.
Hence there exists $q > p$ such that $q \in \alpha$.
Hence $q \in \gamma$.
Thus $\gamma$ satisfies criterion $(3)$ for being a cut.
Thus, by definition of the real numbers by identifying them with cuts, $\gamma$ is a real number.
We have that:
:$\alpha \le \gamma$
for all $\alpha \in L$.
 there exists $\beta \in R$ such that $\beta < \gamma$.
Then there exists some rational number $p \in\ Q$ such that $p \in \gamma$ and $p \notin beta$.
But if $p \in \gamma$ then $p \in \alpha$ for some $\alpha\ in L$.
This implies that $\beta < \alpha$.
But this contradicts the definition of Dedekind cut:
:$(3): \quad \forall x \in L: \forall y \in R: x < y$
Thus $\gamma \le \beta$ for all $\beta \in R$.
That is, $\gamma$ is a producer of $\tuple {L, R}$.
== Sources ==
* : Chapter $1$: The Real and Complex Number Systems: Real Numbers: Proof of Theorem $1.32$
Category:Dedekind's Theorem
Dedekind-Complete Bounded Ordered Set is Complete Lattice

== Theorem ==
Let $\struct {L, \preceq}$ be an ordered set.
Let $L$ have a lower bound $\bot$ and an upper bound $\top$.
Let $\struct {L, \preceq}$ be Dedekind-complete.
Then $\struct {L, \preceq}$ is a complete lattice.
== Proof ==
Let $S \subseteq L$.
If $S = \O$, then $S$ has a supremum of $\bot$ and an infimum of $\top$.
Let $S \ne \O$.
$S$ is bounded above by $\top$.
As $\struct {L, \preceq}$ is Dedekind complete, $S$ has a supremum.
$S$ is bounded below by $\bot$.
By Dedekind Completeness is Self-Dual, $S$ has an infimum.
Thus every subset of $L$ has a supremum and an infimum.
So, by definition, $\struct {L, \preceq}$ is a complete lattice.
Category:Complete Lattices
Dedekind Completeness is Self-Dual

== Theorem ==
Let $\struct {S, \preceq}$ be an ordered set.
Then $\struct {S, \preceq}$ is Dedekind complete every non-empty subset of $S$ that is bounded below admits an infimum in $S$.
That is, an ordered set is Dedekind complete its dual is Dedekind complete.
== Proof ==
=== Necessary Condition ===
Let $\struct {S, \preceq}$ be Dedekind complete.
Let $A \subseteq S$ be non-empty and bounded below.
Let $B \subseteq S$ be set of all lower bounds for $A$.
Then every element of $A$ is an upper bound for $B$.
Therefore, $B$ is non-empty and bounded above.
By the definition of Dedekind completeness, $B$ admits a supremum $x \in S$.
By the definition of supremum, it follows that every element of $A$ succeeds $x$.
That is, $x$ is a lower bound for $A$.
If $y \in S$ is a lower bound for $A$, then $y \in B$, and so $y \preceq x$.
Hence, $x$ is the infimum of $A$.
=== Sufficient Condition ===
Follows directly from the Necessary Condition and Dual of Dual Ordering.
== Sources ==
* : $1$: Set Theory and Logic: $\S 3$: Relations: Exercise $3.13$
Category:Order Theory
Dedekind Completion is Unique up to Isomorphism

== Theorem ==
Let $S$ be an ordered set.
Let $\struct {X, f}$ and $\struct {Y, g}$ be Dedekind completions of $S$.
Then there exists a unique order isomorphism $\phi: X \to Y$ such that $\phi \circ f = g$.
== Proof ==
By assumption, $\struct {X, f}$ is a Dedekind completion of $S$.
Also, $g: S \to Y$ is an order embedding and $Y$ is Dedekind complete.
Hence by definition of Dedekind completion, there exists a unique $\phi: X \to Y$ such that:
:$\phi \circ f = g$
It only remains to show that $\psi$ is an order isomorphism.
By reversing the roles of $X$ and $Y$ in the above, we obtain a unique $\psi: Y \to X$ subject to:
:$\psi \circ g = f$
Therefore:
:$\psi \circ \phi \circ f = f$
:$\phi \circ \psi \circ g = g$
By the uniqueness clause of the definition of Dedekind completion, it follows that:
:$\psi \circ \phi = I_X$
:$\phi \circ \psi = I_Y$
where $I_X$ and $I_Y$ are the identity mappings on $X$ and $Y$ respectively.
Hence $\psi$ is an order isomorphism.
== Also see ==
* Existence of Dedekind Completion
Category:Order Theory
Deduction Theorem

== Theorem ==
Let $\mathscr H$ be instance 1 of a Hilbert proof system.
Then the deduction rule:
::$\dfrac{U,\mathbf A \vdash \mathbf B}{U \vdash \mathbf A \implies \mathbf B}$
is a derived rule for $\mathscr H$.
== Proof ==
For any proof of $U, \mathbf A \vdash \mathbf B$, we indicate how to transform it into a proof of $U \vdash \mathbf A \implies \mathbf B$ without using the deduction rule.
This is done by applying the Second Principle of Mathematical Induction to the length $n$ of the proof of $U,\mathbf A \vdash \mathbf B$.
If $n = 1$, then one of the following must occur:
* $\mathbf B \in U$
* $\mathbf B = \mathbf A$
* $\mathbf B$ is an axiom or a theorem of $\mathscr H$
In the first case, obviously $U \vdash \mathbf B$.
By Axiom 1, $U \vdash \mathbf B \implies \paren {\mathbf A \implies \mathbf B}$.
By Modus Ponens, $U \vdash \mathbf A \implies \mathbf B$.
In the second case, $U \vdash \mathbf A \implies \mathbf A$ by the Law of Identity.
Finally, in the third case, we have $U \vdash \mathbf B$.
As in the first case, we conclude $U \vdash \mathbf A \implies \mathbf B$.
If $n > 1$, the only other option for arriving at $U, \mathbf A \vdash \mathbf B$ is through Modus Ponens.
That is to say, two earlier lines of the proof contain:
:$U, \mathbf A \vdash \mathbf C$
:$U, \mathbf A \vdash \mathbf C \implies \mathbf B$
for some WFF $\mathbf C$.
But then these sequents have shorter proofs.
Hence, they satisfy the induction hypothesis.
Thus, we may infer:
:$U \vdash \mathbf A \implies \mathbf C$
:$U \vdash \mathbf A \implies \paren {\mathbf C \implies \mathbf B}$
This allows us to give the following proof of $U \vdash \mathbf A \implies \mathbf B$:
The result follows by the Second Principle of Mathematical Induction.
== Sources ==
* 
* 
Category:Deduction Theorem
Category:Propositional Logic
Category:Named Theorems
Deduction Theorem for Hilbert Proof System for Predicate Logic

== Theorem ==
Let $\mathscr H$ be instance 1 of a Hilbert proof system for predicate logic.
Then the deduction rule:
::$\dfrac{U,\mathbf A \vdash \mathbf B}{U \vdash \mathbf A \implies \mathbf B}$
is a derived rule for provable consequences in $\mathscr H$.
== Proof ==
For any proof of $U, \mathbf A \vdash \mathbf B$, we indicate how to transform it into a proof of $U \vdash \mathbf A \implies \mathbf B$ without using the deduction rule.
This is done by applying the Second Principle of Mathematical Induction to the length $n$ of the proof of $U,\mathbf A \vdash \mathbf B$.
By definition of $\mathscr H$, then one of the following must occur:
* $\mathbf B \in U$
* $\mathbf B$ is an axiom of $\mathscr H$
* $\mathbf B = \mathbf A$
* $\mathbf B$ is derived from Modus Ponens
In the first two cases, we can craft the following proof of $U \vdash \mathbf A \implies \mathbf B$:
Next, if $\mathbf B = \mathbf A$, then $\mathbf A \implies \mathbf B$ is a tautology, and hence satisfies axiom 1 of $\mathscr H$.
Lastly, suppose that $\mathbf B$ is derived from Modus Ponens, so that we have $\mathbf B'$ and $\mathbf B' \implies \mathbf B$ as provable consequences of $U, \mathbf A$.
By the induction hypothesis, we have proofs of $U \vdash \mathbf A \implies \mathbf B'$ and $U \vdash \mathbf A \implies \paren{ \mathbf B' \implies \mathbf B }$.
Then, expanding upon these proofs:
Hence the result by the Second Principle of Mathematical Induction.
== Sources ==
* : $\text{II}.11$ Some Strategies for Constructing Proofs: Lemma $\text{II}.11.1$ (The Deduction Theorem)
Category:Deduction Theorem
Category:Hilbert Proof System Instance 1 for Predicate Logic
Deficient Number/Sequence

== Sequence of Deficient Numbers ==
The sequence of deficient numbers begins:
:$2, 3, 4, 5, 7, 8, 9, 10, 11, 13, 14, 15, 16, 17, 19, 21, \ldots$
== Sources ==
* : $2$
* : $2$
Category:Deficient Numbers
Defining Sequence of Natural Logarithm is Convergent

== Theorem ==
Let $x \in \R$ be a real number such that $x > 0$.
Let $\left\langle{ f_n }\right\rangle$ be the sequence of mappings $f_n : \R_{>0} \to \R$ defined as:
:$f_n \left({ x }\right) = n \left({ \sqrt[n]{ x } - 1 }\right)$
Then $\left\langle{ f_n }\right\rangle$ is pointwise convergent.
== Proof ==
Fix $x \in \R_{>0}$.
From Defining Sequence of Natural Logarithm is Strictly Decreasing, $\left\langle{ f_n \left({ x }\right) }\right\rangle$ is strictly decreasing.
From Lower Bound of Natural Logarithm/Proof 3, $\left\langle{ f_n \left({ x }\right) }\right\rangle$ is bounded below.
From Monotone Convergence Theorem, $\left\langle{ f_n \left({ x }\right) }\right\rangle$ is convergent
Hence the result, by definition of pointwise convergence.
Category:Natural Logarithms
Defining Sequence of Natural Logarithm is Strictly Decreasing

== Theorem ==
Let $x \in \R$ be a real number such that $x > 0$.
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}$
Then $\forall x \in \R_{>0}: \sequence {\map {f_n} x}$ is strictly decreasing.
== Proof ==
Fix $t \in R_{>0}$.
Then:
Thus:
:$n \paren {t^{n + 1} - 1} > \paren {n + 1} \paren {t^n - 1}$
Fix $x \in \R_{>0}$.
From Power of Positive Real Number is Positive: Rational Number:
:$\forall n \in \N : x^{1 / \paren {n \paren {n + 1} } } \in \R_{>0}$
Thus:
Hence the result, by definition of strictly decreasing sequence.
Category:Natural Logarithms
Defining Sequence of Natural Logarithm is Uniformly Convergent on Compact Sets

== Theorem ==
Let $x \in \R$ be a real number such that $x > 0$.
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 $K \subseteq \R_{>0}$ be compact.
Then $\sequence {f_n}$ is uniformly convergent on $K$.
== Proof ==
From Continuity of Root Function and Combination Theorem for Continuous Real Functions:
:$\forall n \in \N : \map {f_n} x$ is continuous on $K$
From Defining Sequence of Natural Logarithm is Convergent, $\sequence {f_n}$ is pointwise convergent to $\ln$.
From Real Natural Logarithm Function is Continuous, $\ln$ is continuous on $K$.
From Defining Sequence of Natural Logarithm is Strictly Decreasing:
:$\forall x \in K: \sequence {\map {f_n} x}$ is monotone.
From Dini's Theorem, $\sequence {f_n}$ is uniformly convergent to $\ln$.
Hence the result.
Category:Natural Logarithms
Definite Integral/Examples

== Examples of Definite Integrals ==
=== Definite Integral of $2 x$ from $2$ to $3$ ===
=== Definite Integral of $x^2$ from $0$ to $2$ ===
=== Definite Integral of $\sqrt x$ from $0$ to $4$ ===
=== Definite Integral of $\cos x$ from $0$ to $\dfrac \pi 2$ ===
=== Definite Integral of $\dfrac 1 x$ from $1$ to $e$ ===
=== Definite Integral of $\dfrac 1 {1 - x}$ from $2$ to $3$ ===
Category:Examples of Definite Integrals
Definite Integral/Examples/Cosine of x from 0 to pi by 2

== Example of Definite Integral ==
:$\ds \int_0^{\pi / 2} \cos x \rd x = 1$
== Proof ==
== Sources ==
* : $\text {II}$. Calculus: Exercises $\text {XV}$: $1. \ \text{(c)}$
Category:Examples of Definite Integrals
Definite Integral/Examples/Reciprocal of 1 - x from 2 to 3

== Example of Definite Integral ==
:$\ds \int_2^3 \dfrac {\d x} {1 - x} = \ln \dfrac 1 2$
== Proof ==
Then we re-evaluate the limits:
Hence:
== Sources ==
* : $\text {II}$. Calculus: Exercises $\text {XV}$: $1. \ \text{(e)}$
Category:Examples of Definite Integrals
Definite Integral/Examples/Reciprocal of x from 1 to e

== Example of Definite Integral ==
:$\ds \int_1^e \dfrac {\d x} x = 1$
== Proof ==
== Sources ==
* : $\text {II}$. Calculus: Exercises $\text {XV}$: $1. \ \text{(d)}$
Category:Examples of Definite Integrals
Definite Integral/Examples/Root x from 0 to 4

== Example of Definite Integral ==
:$\ds \int_0^4 \sqrt x \rd x = \dfrac {16} 3$
== Proof ==
== Sources ==
* : $\text {II}$. Calculus: Exercises $\text {XV}$: $1. \ \text{(b)}$
Category:Examples of Definite Integrals
Definite Integral/Examples/x squared from 0 to 2

== Example of Definite Integral ==
:$\ds \int_0^2 x^2 \rd x = \dfrac 8 3$
== Proof ==
== Sources ==
* : $\text {II}$. Calculus: Exercises $\text {XV}$: $1. \ \text{(a)}$
Category:Examples of Definite Integrals
Definite Integral from -a to a of Power of a plus x by Power of a minus x

== Theorem ==
:$\ds \int_{-a}^a \paren {a + x}^{m - 1} \paren {a - x}^{n - 1} \rd x = \paren {2 a}^{m + n - 1} \frac {\map \Gamma m \map \Gamma n} {\map \Gamma {m + n} }$
where:
:$\Gamma$ denotes the Gamma function
:$a$, $m$ and $n$ are positive real numbers.
== Proof ==
Note the resemblance of this result to the integral defining the beta function.
In view of this, we apply the substitution: 
:$u = \dfrac {a + x} {2 a}$
We then have, by Derivative of Power: 
:$\dfrac {\d u} {\d x} = \dfrac 1 {2 a}$
and:
so that: 
:$a + x = 2 a u$
and:
:$a - x = \paren {2 a} \paren {1 - u}$
and:
:$\dfrac {\d x} {\d u} = 2 a$
We therefore have: 
== Sources ==
* : $\S 15$: Miscellaneous Definite Integrals: $15.120$
* : $\S 18$: Definite Integrals: Miscellaneous Definite Integrals: $18.120$
Category:Examples of Definite Integrals
Definite Integral from 0 to 1 of Arcsine of x by Arccosine of x over x

== Theorem ==
:$\ds \int_0^1 \frac {\arcsin x \arccos x } x \rd x = \dfrac 7 8 \map \zeta 3$
where $\map \zeta 3$ is Apéry's constant: the Riemann $\zeta$ function of $3$.
== Proof ==
With a view to expressing the primitive in the form:
let:
and let:
Then:
== Sources ==
* https://www.instagram.com/p/C1WXakXxdhZ/
Category:Apéry's Constant
Category:Arcsine Function
Category:Arccosine Function
Category:Dirichlet Eta Function
Category:Riemann Zeta Function
Definite Integral from 0 to 1 of Arcsine of x over x

== Theorem ==
:$\ds \int_0^1 \frac {\arcsin x} x = \frac \pi 2 \ln 2$
== Proof ==
Let: 
:$x = \sin \theta$
By Derivative of Sine Function, we have: 
:$\dfrac {\d x} {\d \theta} = \cos \theta$
We have, by Arcsine of Zero is Zero: 
:as $x \to 0$, $\theta \to \arcsin 0 = 0$.
By Arcsine of One is Half Pi, we have: 
:as $x \to 1$, $\theta \to \arcsin 1 = \dfrac \pi 2$.
We have:
By Primitive of Cotangent Function:
:$\ds \int \cot \theta \rd \theta = \map \ln {\sin \theta} + C$
So:
 
We have: 
giving: 
:$\ds \int_0^{\pi/2} \theta \cot \theta \rd \theta = \frac \pi 2 \ln 2$
hence the result.
== Sources ==
* : $\S 15$: Definite Integrals involving Trigonometric Functions: $15.64$
Category:Definite Integrals involving Arcsine Function
Definite Integral from 0 to 1 of Arctangent of x over x

== Theorem ==
:$\ds \int_0^1 \frac {\arctan x} x \rd x = G$
where $G$ denotes Catalan's constant.
== Proof ==
== Sources ==
* : $\S 15$: Definite Integrals involving Trigonometric Functions: $15.63$
Category:Definite Integrals involving Arctangent Function
Definite Integral from 0 to 1 of Difference of Powers of x over Logarithm of x

== Theorem ==
:$\ds \int_0^1 \frac {x^m - x^n} {\ln x} \rd x = \map \ln {\frac {m + 1} {n + 1} }$
where $m$ and $n$ are real numbers with $m, n > -1$.
== Proof ==
Let: 
:$x = e^{-u}$
We have, by Derivative of Exponential Function:
:$\dfrac {\d x} {\d u} = -e^{-u}$ 
By Exponential Tends to Zero and Infinity: 
:as $x \to 0$, $u \to \infty$
By Exponential of Zero: 
:as $x \to 1$, $u \to 0$.
So:
== Sources ==
* : $\S 15$: Definite Integrals involving Logarithmic Functions: $15.98$
Category:Definite Integrals involving Logarithm Function
Definite Integral from 0 to 1 of Even Powers of Logarithm of 1 - x over x

== Theorem ==
Let $n \in \Z_{> 0}$ be a (strictly) positive integer.
:$\ds \int_0^1 \map {\ln^{2n} } {\dfrac {1 - x} x} \rd x = \paren {-1}^{n + 1} B_{2 n} \paren {2^{2 n} - 2} \pi^{2 n}$
:where $B_{2 n}$ is the $2 n$th Bernoulli number.
=== Corollary ===
== Proof ==
let:
and also:
Then:
From Sum of Infinite Geometric Sequence, we have:
:$\ds \sum_{k \mathop = 0}^\infty \paren {-1}^k \paren {e^{-u} }^k = \dfrac 1 {1 + e^{-u} }$
Taking the derivative of both sides, we have:
Therefore:
Category:Definite Integrals involving Logarithm Function
Category:Bernoulli Numbers
Category:Riemann Zeta Function at Even Integers
Definite Integral from 0 to 1 of Even Powers of Logarithm of 1 - x over x/Corollary

== Corollary to Definite Integral from 0 to 1 of Even Powers of Logarithm of 1 - x over x ==
Let $n \in \Z_{> 0}$ be a (strictly) positive integer.
:$\ds \int_0^1 \map {\ln^{2n} } {\dfrac {1 - x} x} \rd x = 2 \map \zeta {2 n} \paren {2 n}! \paren {1 - \dfrac 1 {2^{2n-1} } }$
== Proof ==
Definite Integral from 0 to 1 of Logarithm of One minus x over x

== Theorem ==
:$\ds \int_0^1 \frac {\map \ln {1 - x} } x \rd x = -\frac {\pi^2} 6$
== Proof ==
== Also see ==
* Definite Integral $\ds \int_0^1 \frac {\ln x} {1 - x} \rd x$
== Sources ==
* : $\S 15$: Definite Integrals involving Logarithmic Functions: $15.94$
Category:Definite Integrals involving Logarithm Function
Definite Integral from 0 to 1 of Logarithm of One plus x over x

== Theorem ==
:$\ds \int_0^1 \frac {\map \ln {1 + x} } x \rd x = \frac {\pi^2} {12}$
== Proof ==
== Sources ==
* : $\S 15$: Definite Integrals involving Logarithmic Functions: $15.93$
Category:Definite Integrals involving Logarithm Function
Definite Integral from 0 to 1 of Logarithm of x by Logarithm of One minus x

== Theorem ==
:$\ds \int_0^1 \ln x \map \ln {1 - x} \rd x = 2 - \frac {\pi^2} 6$
== Proof ==
== Sources ==
* : $\S 15$: Definite Integrals involving Logarithmic Functions: $15.96$
Category:Definite Integrals involving Logarithm Function
Definite Integral from 0 to 1 of Logarithm of x by Logarithm of One minus x over One minus x

== Theorem ==
:$\ds \int_0^1 \dfrac {\ln x \map \ln {1 - x} } {\paren {1 - x} } \rd x = \map \zeta 3$
where $\map \zeta 3$ is Apéry's constant: the Riemann $\zeta$ function of $3$.
== Proof 1 ==
== Proof 2 ==
Category:Definite Integral from 0 to 1 of Logarithm of x by Logarithm of One minus x over One minus x
Category:Apéry's Constant
Category:Definite Integrals involving Logarithm Function
Definite Integral from 0 to 1 of Logarithm of x by Logarithm of One minus x over One minus x/Proof 2

== Theorem ==
== Proof ==
With a view to expressing the primitive in the form:
let:
and let:
Then:
Category:Definite Integral from 0 to 1 of Logarithm of x by Logarithm of One minus x over One minus x
Definite Integral from 0 to 1 of Logarithm of x by Logarithm of One plus x

== Theorem ==
:$\ds \int_0^1 \ln x \map \ln {1 + x} \rd x = 2 - 2 \ln 2 - \frac {\pi^2} {12}$
== Proof ==
== Sources ==
* : $\S 15$: Definite Integrals involving Logarithmic Functions: $15.95$
Category:Definite Integrals involving Logarithm Function
Definite Integral from 0 to 1 of Logarithm of x over One minus x

== Theorem ==
:$\ds \int_0^1 \frac {\ln x} {1 - x} \rd x = -\frac {\pi^2} 6$
== Proof ==
== Also see ==
* Definite Integral $\ds \int_0^1 \frac {\map \ln {1 - x} } x \rd x$
== Sources ==
* : $\S 15$: Definite Integrals involving Logarithmic Functions: $15.92$
Category:Definite Integrals involving Logarithm Function
Definite Integral from 0 to 1 of Logarithm of x over One plus x

== Theorem ==
:$\ds \int_0^1 \frac {\ln x} {1 + x} \rd x = -\frac {\pi^2} {12}$
== Proof ==
== Sources ==
* : $\S 15$: Definite Integrals involving Logarithmic Functions: $15.91$
Category:Definite Integrals involving Logarithm Function
Definite Integral from 0 to 1 of Power of u over 1 + Power of u

== Theorem ==
where $a, d > 0$. 
== Proof ==
== Sources ==
* : $\S 19$: Series involving Reciprocals of Powers of Positive Integers: $19.34$
* : $\S 21$: Series of Constants: Series Involving Reciprocals of Powers of Positive Integers: $21.34.$
Category:Examples of Definite Integrals
Definite Integral from 0 to 1 of Power of x by Power of Logarithm of x

== Theorem ==
:$\ds \int_0^1 x^m \paren {\ln x}^n \rd x = \frac {\paren {-1}^n \map \Gamma {n + 1} } {\paren {m + 1}^{n + 1} }$
where:
:$n$ is a non-negative integer
:$m$ is a real number with $m > -1$.
== Proof 1 ==
 
== Proof 2 ==
== Sources ==
* : $\S 15$: Definite Integrals involving Logarithmic Functions: $15.90$
Category:Definite Integrals involving Logarithm Function
Category:Definite Integral from 0 to 1 of Power of x by Power of Logarithm of x
Definite Integral from 0 to 1 of Power of x by Power of Logarithm of x/Proof 1

== Theorem ==
== Proof ==
Let: 
:$x = \map \exp {-\dfrac u {m + 1} }$
Then, by Derivative of Exponential Function: 
:$\dfrac {\d x} {\d u} = -\dfrac 1 {m + 1} \map \exp {-\dfrac u {m + 1} }$
We have by Exponential of Zero: 
:as $x \to 1$, $u \to 0$
We also have, by Exponential Tends to Zero and Infinity: 
:as $x \to 0$, $u \to \infty$
So: 
Category:Definite Integral from 0 to 1 of Power of x by Power of Logarithm of x
Definite Integral from 0 to 1 of Power of x by Power of Logarithm of x/Proof 2

== Theorem ==
== Proof ==
From Primitive of Power, we have: 
:$\ds \int_0^1 x^m \rd x = \frac 1 {m + 1}$
We have: 
So: 
Category:Definite Integral from 0 to 1 of Power of x by Power of Logarithm of x
Definite Integral from 0 to 1 of Zeta of 2 minus Dilogarithm of x over One minus x

== Theorem ==
:$\ds \int_{\to 0}^{\to 1} \dfrac {\paren {\map \zeta 2 - \map {\Li_2} x } } {1 - x} \rd x = 2 \map \zeta 3$
where:
:$\map {\Li_2} x$ is the Dilogarithm function of $x$
:$\map \zeta 2$ is the Riemann $\zeta$ function of $2$
:$\map \zeta 3$ is Apéry's constant: the Riemann $\zeta$ function of $3$.
== Proof ==
With a view to expressing the primitive in the form:
let:
and let:
Then:
Category:Spence's Function
Category:Apéry's Constant
Category:Definite Integrals involving Logarithm Function