avewright/proofwiki-math huggingface dataset:
Theorem: Cauchy Mean Value Theorem

Let $f$ and $g$ be real functions which are continuous on the closed interval $\closedint a b$ and differentiable on the open interval $\openint a b$.
Suppose:
:$\forall x \in \openint a b: \map {g'} x \ne 0$
Then:
:$\exists \xi \in \openint a b: \dfrac {\map {f'} \xi} {\map {g'} \xi} = \dfrac {\map f b - \map f a} {\map g b - \map g a}$

Proof:
First we check $\map g a \ne \map g b$.
{{AimForCont}} $\map g a = \map g b$.
From Rolle's Theorem:
:$\exists \xi \in \openint a b: \map {g'} \xi = 0$.
This contradicts $\forall x \in \openint a b: \map {g'} x \ne 0$.
Thus by Proof by Contradiction $\map g a \ne \map g b$.
Let $h = \dfrac {\map f b - \map f a} {\map g b - \map g a}$.
Let $F$ be the real function defined on $\closedint a b$ by:
:$\map F x = \map f x - h \map g x$.
Then:
{{begin-eqn}}
{{eqn | l = \map F b - \map F a
      | r = \paren {\map f b - h \map g b} - \paren {\map f a - h \map g a}
      | c = as $\map F x = \map f x - h \map g x$
}}
{{eqn | r = \paren {\map f b - \map f a} - h \paren {\map g b - \map g a}
}}
{{eqn | r = 0
}}
{{eqn | ll= \leadsto
      | l = \map F a
      | r = \map F b
}}
{{eqn | ll= \leadsto
      | q = \exists \xi \in \openint a b
      | l = \map {F'} \xi
      | r = \map {f'} \xi - h \map {g'} \xi
      | c = Sum Rule for Derivatives, Derivative of Constant Multiple
}}
{{eqn | r = 0
      | c = Rolle's Theorem
}}
{{eqn | ll= \leadsto
      | q = \exists \xi \in \openint a b
      | l = \frac {\map {f'} \xi} {\map {g'} \xi}
      | r = h
      | c = $\forall x \in \openint a b: \map {g'} x \ne 0$
}}
{{eqn | r = \frac {\map f b - \map f a} {\map g b - \map g a}
}}
{{end-eqn}}
{{qed}}
Theorem: Cauchy Mean Value Theorem

Let $f$ and $g$ be real functions which are continuous on the closed interval $\closedint a b$ and differentiable on the open interval $\openint a b$.
Suppose:
:$\forall x \in \openint a b: \map {g'} x \ne 0$
Then:
:$\exists \xi \in \openint a b: \dfrac {\map {f'} \xi} {\map {g'} \xi} = \dfrac {\map f b - \map f a} {\map g b - \map g a}$

Proof:
Let $G$ be a real-valued function continuous on $\closedint a x$ and differentiable with non-vanishing derivative on $\openint a x$.
Let:
:$\map F t = \map f t + \dfrac {\map {f'} t} {1!} \paren {x - t} + \dotsb + \dfrac {\map {f^{\paren n} } t} {n!} \paren {x - t}^n$
By the Cauchy Mean Value Theorem:
:$(1): \quad \dfrac {\map {F'} x} {\map {G'} \xi} = \dfrac {\map F x - \map F a} {\map G x - \map G a}$
for some $\xi \in \openint a x$.
Note that the numerator:
:$\map F x - \map F a = R_n$
is the remainder of the Taylor polynomial for $\map f x$.
On the other hand, computing $\map {F'} \xi$:
:$\map {F'} \xi = \map {f'} \xi - \map {f'} \xi + \dfrac {\map {f' '} \xi} {1!} \paren {x - \xi} - \dfrac {\map {f' '} \xi} {1!} \paren {x - \xi} + \dotsb + \dfrac {\map {f^{\paren {n + 1} } } t} {n!} \paren {x - \xi}^n = \dfrac {\map {f^{\paren {n + 1} } } \xi} {n!} \paren {x - \xi}^n$
Putting these two facts together and rearranging the terms of $(1)$ yields:
:$R_n = \dfrac {\map {f^{\paren {n + 1} } } \xi} {n!} \paren {x - \xi}^n \dfrac {\map G x - \map G a} {\map {G'} \xi}$
which was to be shown.
{{improve|Find a way of neatly handling the two different remainder forms}}
Note that the Lagrange Form of the Remainder comes from taking $\map G t = \paren {x - t}^{n + 1}$ and the given Cauchy Form of the Remainder comes from taking $\map G t = t - a$.
{{qed}}
Theorem: Homology Group is Group

The $p$th singular homology group of a space $X$ is a group.

Proof:
{{ProofWanted}}
Category:Homology Groups
mxxmlkcw505h513v0osmyasyxkzb38y
Theorem: Limit of Absolute Value

Let $x, \xi \in \R$ be real numbers.
Then:
:$\size {x - \xi} \to 0$ as $x \to \xi$
where $\size {x - \xi}$ denotes the Absolute Value.

Proof:
Let $\epsilon > 0$.
Let $\delta = \epsilon$.
From the definition of a limit of a function, we need to show that $\size {\map f x - 0} < \epsilon$ provided that $0 < \size {x - \xi} < \delta$, where $\map f x = \size {x - \xi}$.
Thus, provided $0 < \size {x - \xi} < \delta$, we have:
{{begin-eqn}}
{{eqn | l = \size {x - \xi} - 0
      | r = \size {x - \xi}
      | c = 
}}
{{eqn | o = <
      | r = \delta
      | c = 
}}
{{eqn | r = \epsilon
      | c = 
}}
{{end-eqn}}
Hence the result.
{{qed}}
Theorem: Limit of Function in Interval

Let $f$ be a real function which is defined on the open interval $\openint a b$.
Let $\xi \in \openint a b$
Suppose that, $\forall x \in \openint a b$, either:
:$\xi \le \map f x \le x$
or:
:$x \le \map f x \le \xi$
Then $\map f x \to \xi$ as $x \to \xi$.

Proof:
Note that $\size {\map f x - \xi} \le \size {\xi - x}$.
From Limit of Absolute Value we have that $\size {x - \xi} \to 0$ as $x \to \xi$.
The result follows from the Squeeze Theorem.
{{qed}}
Theorem: Strictly Monotone Real Function is Bijective

Let $f$ be a real function which is defined on $I \subseteq \R$.
Let $f$ be strictly monotone on $I$.
Let the image of $f$ be $J$. 
Then $f: I \to J$ is a bijection.

Proof:
From Strictly Monotone Mapping with Totally Ordered Domain is Injective, $f$ is an injection.
From Surjection by Restriction of Codomain, $f: I \to J$ is a surjection.
{{qed}}
Theorem: Inverse of Strictly Monotone Function

Let $f$ be a real function which is defined on $I \subseteq \R$.
Let $f$ be strictly monotone on $I$.
Let the image of $f$ be $J$. 
Then $f$ always has an inverse function $f^{-1}$ and:
:if $f$ is strictly increasing then so is $f^{-1}$
:if $f$ is strictly decreasing then so is $f^{-1}$.

Proof:
The function $f$ is a bijection from Strictly Monotone Real Function is Bijective.
Hence from Bijection iff Inverse is Bijection, $f^{-1}$ always exists and is also a bijection.
From the definition of strictly increasing:
:$X < Y \iff \map f X < \map f Y$
Hence, substituting $X = \map {f^{-1}} x$ and $Y = \map {f^{-1}} y$:
:$\map {f^{-1}} x < \map {f^{-1}} y \iff \map f {\map {f^{-1}} x} < \map f {\map {f^{-1}} y}$
and so:
:$\map {f^{-1}} x < \map {f^{-1}} y \iff x < y$
Similarly, from the definition of strictly decreasing:
:$X < Y \iff \map f X > \map f Y$
Hence, substituting $X = \map {f^{-1}} x$ and $Y = \map {f^{-1}} y$:
:$\map {f^{-1}} x < \map {f^{-1}} y \iff \map f {\map {f^{-1}} x} > \map f {\map {f^{-1}} y}$
and so:
:$\map {f^{-1}} x < \map {f^{-1}} y \iff x > y$
{{qed}}
Theorem: Rokhlin's Theorem (Intersection Forms)

Let $M$ be a smooth 4-manifold.
Then:
:$\map {\omega_2} {\map T M} = 0 \implies \operatorname {sign} Q_M = 0 \pmod {16}$
where:
:$Q_M$ is the intersection form
:$\map T M$ is the tangent bundle
:$\omega_2$ is the second Stiefel-Whitney class.

Proof:
{{Explain|What does "sign" mean in this context?}}
{{ProofWanted}}
{{Namedfor|Vladimir Abramovich Rokhlin|cat = Rokhlin}}
Category:Smooth Manifolds
e3ky606b3n719em4ptt4lryvu2cn6uk
Theorem: Convex Real Function is Continuous

Let $f$ be a real function which is convex on the open interval $\openint a b$.
Then $f$ is continuous on $\openint a b$.

Proof:
From Convex Real Function is Left-Hand and Right-Hand Differentiable, $f$ is left-hand and right-hand differentiable on $\openint a b$.
From Left-Hand and Right-Hand Differentiable Function is Continuous, $f$ is continuous on $\openint a b$.
{{qed}}
Theorem: Convex Real Function is Left-Hand and Right-Hand Differentiable

Let $f$ be a real function which is convex on the open interval $\openint a b$.
Then the left-hand derivative $\map {f'_-} x$ and right-hand derivative $\map {f'_+} x$ both exist for all $x \in \openint a b$.

Proof:
Let $f$ be convex on $\openint a b$.
Then by definition of convexity:
:$\forall x_1, x_2, x_3 \in \openint a b: x_1 < x_2 < x_3: \dfrac {\map f {x_2} - \map f {x_1} } {x_2 - x_1} \le \dfrac {\map f {x_3} - \map f {x_1} } {x_3 - x_1}$
Let $0 < h_1 < h_2$.
Substitute $x_1 = x$, $x_2 = x + h_1$, $x_3 = x + h_2$. Then:
:$\dfrac {\map f {x + h_1} - \map f x} {h_1} \le \dfrac {\map f {x + h_2} - \map f x} {h_2}$
Hence the function $\map F h = \dfrac {\map f {x + h} - \map f x} h$ increases in some $\openint 0 \delta$.
Thus from Limit of Increasing Function it follows that both $\ds \lim_{h \mathop \to 0^+} \map F h = \map {f'_+} x$ and $\ds \lim_{h \mathop \to 0^-} \map F h = \map {f'_-} x$ exist.
{{qed}}
Theorem: Real Function is Convex iff Derivative is Increasing

Let $f$ be a real function which is differentiable on the open interval $\openint a b$.
Then:
:$f$ is convex on $\openint a b$
{{iff}}:
:its derivative $f'$ is increasing on $\openint a b$.
Thus the intuitive result that a convex function "gets steeper".

Proof:
=== Necessary Condition ===
Let $f$ be convex on $\openint a b$.
Let $x_1, x_2, x_3, x_4 \in \openint a b$ such that:
:$x_1 < x_2 < x_3 < x_4$
By the definition of convex function:
:$\dfrac {\map f {x_2} - \map f {x_1} } {x_2 - x_1} \le \dfrac {\map f {x_3} - \map f {x_2} } {x_3 - x_2} \le \dfrac {\map f {x_4} - \map f {x_3} } {x_4 - x_3}$
Ignore the middle term and let $x_2 \to x_1^+$ and $x_3 \to x_4^-$.
Thus:
:$\map {f'} {x_1} \le \map {f'} {x_4}$
Hence $f'$ is increasing on $\openint a b$.
{{qed|lemma}}
Theorem: Inverse of Strictly Increasing Convex Real Function is Concave

Let $f$ be a real function which is convex on the open interval $I$.
Let $J = f \sqbrk I$.
If $f$ be strictly increasing on $I$, then $f^{-1}$ is concave on $J$.

Proof:
Let:
:$X = \map f x \in J$
:$Y = \map f y \in J$.
From the definition of convex:
:$\forall \alpha, \beta \in \R_{>0}, \alpha + \beta = 1: \map f {\alpha x + \beta y} \le \alpha \map f x + \beta \map f y$
Let $f$ be strictly increasing on $I$.
From Inverse of Strictly Monotone Function it follows that, $f^{-1}$ is strictly increasing on $J$.
Thus:
:$\alpha \map {f^{-1} } X + \beta \map {f^{-1} } Y = \alpha x + \beta y \le \map {f^{-1} } {\alpha X + \beta Y}$
Hence $f^{-1}$ is concave on $J$.
{{qed}}
Theorem: Darboux's Theorem

Let $f$ be a real function which is bounded on the closed interval $\closedint a b$.
Then:
:$\ds m \paren {b - a} \le \underline {\int_a^b} \map f x \rd x \le \overline {\int_a^b} \map f x \rd x \le M \paren {b - a}$
where:
:$M$ is an upper bound of $f$ on $\closedint a b$
:$m$ is a lower bound of $f$ on $\closedint a b$
:$\ds \overline {\int_a^b} \map f x \rd x$ denotes the upper Darboux integral of $f$ on $\closedint a b$
:$\ds \underline {\int_a^b} \map f x \rd x$ denotes the lower Darboux integral of $f$ on $\closedint a b$
If $f$ is Darboux integrable on $\closedint a b$, then in fact:
:$\ds m \paren {b - a} \le \int_a^b \map f x \rd x \le M \paren {b - a}$

Proof:
Consider the finite subdivision of $\closedint a b$ given by:
:$P = \set {a, b}$
From their definitions, the upper and lower Darboux sums can be computed as:
:$\ds \map {U^{\paren f}} P = \paren {b - a} \sup_{x \in \closedint a b} \map f x$
:$\ds \map {L^{\paren f}} P = \paren {b - a} \inf_{x \in \closedint a b} \map f x$
Since by definitions of the supremum and infimum:
:$\ds \sup_{x \in \closedint a b} \map f x \le M$
:$\ds \inf_{x \in \closedint a b} \map f x \ge m$
we can conclude that:
:$\ds \map {U^{\paren f}} P \le \paren {b - a} M$
:$\ds \map {L^{\paren f}} P \ge \paren {b - a} m$
Moreover, by definitions of the upper and lower Darboux integrals:
:$\ds \overline {\int_a^b} \map f x \rd x \le \map {U^{\paren f}} P$
:$\ds \underline {\int_a^b} \map f x \rd x \ge \map {L^{\paren f}} P$
The inequalities stated in the theorem follow by transitivity, along with Upper Darboux Integral Never Smaller than Lower Darboux Integral.
The final inequality regarding the proper Darboux integral of $f$ follows immediately from:
:$\ds \int_a^b \map f x \rd x = \overline {\int_a^b} \map f x \rd x = \underline {\int_a^b} \map f x \rd x$
whenever $f$ is Darboux integrable.
{{qed}}
{{Namedfor|Jean-Gaston Darboux|cat = Darboux}}
Theorem: Wilson's Theorem

A (strictly) positive integer $p$ is a prime {{iff}}:
:$\paren {p - 1}! \equiv -1 \pmod p$

Proof:
If $p = 2$ the result is immediate.
Therefore we assume that $p$ is an odd prime.
Theorem: Wilson's Theorem

A (strictly) positive integer $p$ is a prime {{iff}}:
:$\paren {p - 1}! \equiv -1 \pmod p$

Proof:
Proof by induction:
Let $\map P n$ be the proposition:
:$\dfrac {n!} {p^\mu} \equiv \paren {-1}^\mu a_0! a_1! \dotsm a_k! \pmod p$
where $p, a_0, \dots, a_k, \mu$ are as defined above.
=== Basis for the Induction ===
For $n = 1$:
:$a_0 = 1, \mu = 0$
$\map P 1$ reduces to:
:$\dfrac {1!} {p^0} \equiv \paren {-1}^0 1! \pmod p$
which holds trivially.
This is the basis for the induction.
=== Induction Hypothesis ===
This is our induction hypothesis:
:$\dfrac {r!} {p^\mu} \equiv \paren {-1}^\mu a_0! a_1! \dots a_k! \pmod p$
Now we need to show true for $n = r + 1$:
:$\dfrac {\paren {r + 1}!} {p^{\mu'}} \equiv \paren {-1}^{\mu'} b_0! b_1! \dots b_k! \pmod p$
where $\ds r + 1 = \sum_{j \mathop = 0}^k b_j p^j$ is the base $p$ presentation of $r + 1$, and:
:$p^{\mu'} \divides \paren {r + 1}!$
:$p^{\mu' + 1} \nmid \paren {r + 1}!$
=== Induction Step ===
This is our induction step:
Let $p^m$ be the largest power of $p$ which divides $r + 1$, that is:
:$p^m \divides r + 1$
:$p^{m + 1} \nmid r + 1$
Then we must have:
:$b_m \ne 0$
:$b_j = 0$ for $0 \le j < m$
:$\mu' = \mu + m$
and consequently:
:$a_j = b_j$ for $j > m$
:$a_m + 1 = b_m$
:$a_j = p - 1$ for $0 \le j < m$
Thus:
{{begin-eqn}}
{{eqn | l = \frac {\paren {r + 1}!} {p^{\mu'} }
      | r = \frac {r!} {p^\mu} \times \frac {r + 1} {p^m}
}}
{{eqn | o = \equiv
      | r = \paren {-1}^\mu a_0! \dots a_{m - 1}! a_m! \dots a_k! \times \frac {r + 1} {p^m}
      | rr= \pmod p
      | c = Induction Hypothesis
}}
{{eqn | o = \equiv
      | r = \paren {-1}^\mu \paren {\paren {p - 1}!}^m \paren {b_m - 1}! b_{m + 1}! \dots b_k! \times \frac 1 {p^m} \sum_{j \mathop = m}^k b_j p^j
      | rr= \pmod p
      | c = from above
}}
{{eqn | o = \equiv
      | r = \paren {-1}^\mu \paren {-1}^m \paren {b_m - 1}! b_{m + 1}! \dots b_k! \times \sum_{j \mathop = m}^k b_j p^{j - m}
      | rr= \pmod p
      | c = Wilson's Theorem
}}
{{eqn | o = \equiv
      | r = \paren {-1}^{\mu'} \paren {b_m - 1}! b_{m + 1}! \dots b_k! b_m
      | rr= \pmod p
      | c = because $b_j p^{j - m} \equiv 0 \pmod p$ for $j - m > 0$
}}
{{eqn | o = \equiv
      | r = \paren {-1}^{\mu'} b_m! b_{m + 1}! \dots b_k!
      | rr= \pmod p
      | c = {{Defof|Factorial}}
}}
{{eqn | o = \equiv
      | r = \paren {-1}^{\mu'} b_0! \dots b_k!
      | rr= \pmod p
      | c = Factorial of Zero: $b_j = 0$ for $0 \le j < m$
}}
{{end-eqn}}
By the Principle of Mathematical Induction, $\map P n$ is true for all $n \in \Z_{>0}$.
{{qed}}
Theorem: Wilson's Theorem

A (strictly) positive integer $p$ is a prime {{iff}}:
:$\paren {p - 1}! \equiv -1 \pmod p$

Proof:
Consider the numbers of $\set {1, 2, \ldots, n}$ which are not multiples of $p$.
There are $\floor {\dfrac n p}$ complete sets of $p - 1$ such consecutive elements of $\set {1, 2, \ldots, n}$.
Each one of these has a product which is congruent to $-1 \pmod p$ by Wilson's Theorem.
There are also $a_0$ left over which are congruent to $a_0! \pmod p$.
Thus:
:the contributions of the divisors which are not multiples of $p$ is $\paren {-1}^{\floor {n / p} } a_0!$
:the contributions of the divisors which are multiples of $p$ is the same as the contribution in $\floor {\dfrac n p}!$
Thus the argument can be repeated on $\floor {\dfrac n p}!$ until the formula is complete.
{{qed}}
Theorem: Wilson's Theorem

A (strictly) positive integer $p$ is a prime {{iff}}:
:$\paren {p - 1}! \equiv -1 \pmod p$

Proof:
If $p = 2$ the result is obvious.
Therefore we assume that $p$ is an odd prime.
Let $p$ be prime.
Consider $n \in \Z, 1 \le n < p$.
As $p$ is prime, $n \perp p$.
From Law of Inverses (Modulo Arithmetic), we have:
:$\exists n' \in \Z, 1 \le n' < p: n n' \equiv 1 \pmod p$
By Solution of Linear Congruence, for each $n$ there is '''exactly one''' such $n'$, and $\paren {n'}' = n$.
So, provided $n \ne n'$, we can pair any given $n$ from $1$ to $p$ with another $n'$ from $1$ to $p$.
We are then left with the numbers such that $n = n'$.
Then we have $n^2 \equiv 1 \pmod p$.
Consider $n^2 - 1 = \paren {n + 1} \paren {n - 1}$ from Difference of Two Squares.
So either $n + 1 \divides p$ or $n - 1 \divides p$.
Observe that these cases do not occur simultaneously, as their difference is $2$, and $p$ is an odd prime.
From Negative Number is Congruent to Modulus minus Number:
:$p - 1 \equiv -1 \pmod p$
Hence $n = 1$ or $n = p - 1$.
So, we have that $\paren {p - 1}!$ consists of numbers multiplied together as follows:
:in pairs whose product is congruent to $1 \pmod p$
:the numbers $1$ and $p - 1$.
The product of all these numbers is therefore congruent to $1 \times 1 \times \cdots \times 1 \times p - 1 \pmod p$ by modulo multiplication.
From Negative Number is Congruent to Modulus minus Number:
:$\paren {p - 1}! \equiv -1 \pmod p$
{{qed}}
Theorem: Wilson's Theorem

A (strictly) positive integer $p$ is a prime {{iff}}:
:$\paren {p - 1}! \equiv -1 \pmod p$

Proof:
If $p = 2$ the result is obvious.
Therefore we assume that $p$ is an odd prime.
Consider $p$ points on the circumference of a circle $C$ dividing it into $p$ equal arcs.
By joining these points in a cycle, we can create polygons, some of them stellated.
From Number of Different n-gons that can be Inscribed in Circle, the number of different such polygons is $\dfrac {\paren {p - 1}!} 2$.
When you rotate these polygons through an angle of $\dfrac {2 \pi} p$, exactly $\dfrac {p - 1} 2$ are unaltered.
These are the regular $p$-gons and regular stellated $p$-gons.
That there are $\dfrac {p - 1} 2$ of them follows from Number of Regular Stellated Odd n-gons.
The remaining $\dfrac {\paren {p - 1}!} 2 - \dfrac {p - 1} 2$ polygons can be partitioned into sets of $p$ elements: those which can be obtained from each other by rotation through multiples of $\dfrac {2 \pi} p$.
{{Explain|Why are there always $p$ of them? See Fermat's Little Theorem/Corollary 1.}}
The total number of such sets is then:
:$\dfrac {\paren {p - 1}! - \paren {p - 1} } {2 p}$
Thus we have that:
:$2 p \divides \paren {\paren {p - 1}! - \paren {p - 1} }$
That is:
:$p \divides \paren {\paren {p - 1}! + 1}$
{{qed}}
Theorem: Wilson's Theorem

A (strictly) positive integer $p$ is a prime {{iff}}:
:$\paren {p - 1}! \equiv -1 \pmod p$

Proof:
Let $p$ be prime.
Consider $\struct {\Z_p, +, \times}$, the ring of integers modulo $m$.
From Ring of Integers Modulo Prime is Field, $\struct {\Z_p, +, \times}$ is a field.
Hence, apart from $\eqclass 0 p$, all elements of $\struct {\Z_p, +, \times}$ are units
As $\struct {\Z_p, +, \times}$ is a field, it is also by definition an integral domain, we can apply:
From Product of Units of Integral Domain with Finite Number of Units, the product of all elements of $\struct {\Z_p, +, \times}$ is $-1$.
But the product of all elements of $\struct {\Z_p, +, \times}$ is $\paren {p - 1}!$
The result follows.
{{qed}}
Theorem: Integral of Constant

Let $c$ be a constant.

Proof:
Let $F$ be a primitive of $f$ on $\closedint a b$.
By Primitive of Constant Multiple of Function, $H = c F$ is a primitive of $c f$ on $\closedint a b$.
Hence by the Fundamental Theorem of Calculus:
{{begin-eqn}}
{{eqn | l = \int_a^b c \map f x \rd x
      | r = \bigintlimits {c \map F x} a b
      | c = 
}}
{{eqn | r = c \bigintlimits {\map F x} a b
      | c = 
}}
{{eqn | r = c \int_a^b \map f x \rd x
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Integral of Constant

Let $c$ be a constant.

Proof:
Let $F$ be a primitive of $f$ on $\closedint a b$.
By Linear Combination of Definite Integrals:
:$\ds \int_a^b \paren {\lambda \map f t + \mu \map g t} \rd t = \lambda \int_a^b \map f t \rd t + \mu \int_a^b \map g t \rd t$
for real functions $f$ and $g$ which are integrable on the closed interval $\closedint a b$, where $\lambda$ and $\mu$ be real numbers.
The result follows by setting $\lambda = c$ and $\mu = 0$.
{{qed}}
Theorem: Sum of Integrals on Adjacent Intervals for Continuous Functions

Let $f$ be a real function which is continuous on any closed interval $I$.
Let $a, b, c \in I$.
Then:
:$\ds \int_a^c \map f t \rd t + \int_c^b \map f t \rd t = \int_a^b \map f t \rd t$

Proof:
By Continuous Real Function is Darboux Integrable, $f$ is integrable on $I$.
The result follows by application of Sum of Integrals on Adjacent Intervals for Integrable Functions.
{{qed}}
Theorem: Primitives which Differ by Constant

Let $F$ be a primitive for a real function $f$ on the closed interval $\closedint a b$.
Let $G$ be a real function defined on $\closedint a b$.
Then $G$ is a primitive for $f$ on $\closedint a b$ {{iff}}:
:$\exists c \in \R: \forall x \in \closedint a b: \map G x = \map F x + c$
That is, {{iff}} $F$ and $G$ differ by a constant on the whole interval.

Proof:
=== Necessary Condition ===
Suppose $G$ is a primitive for $f$.
Then $F - G$ is continuous on $\closedint a b$, differentiable on $\openint a b$, and for any $x \in \openint a b$, we have:
{{begin-eqn}}
{{eqn | l = \map {D_x} {\map F x - \map G x}
      | r = \map {D_x} {\map F x} - \map {D_x} {\map G x}
      | c = Sum Rule for Derivatives
}}
{{eqn | r = \map f x - \map f x
      | c = $F, G$ are a primitives for $f$
}}
{{eqn | r = 0
}}
{{end-eqn}}
From Zero Derivative implies Constant Function it follows that $F - G$ is constant on $\closedint a b$.
Hence the result.
{{qed|lemma}}
Theorem: Definite Integral of Function plus Constant

Let $f$ be a real function which is continuous on the closed interval $\closedint a b$.
Let $c$ be a constant.
Then:
:$\ds \int_a^b \paren {\map f t + c} \rd t = \int_a^b \map f t \rd t + c \paren {b - a}$

Proof:
Let $P = \set {x_0, x_1, x_2, \ldots, x_n}$ be a finite subdivision of $\closedint a b$.
Let $\map {L^{\paren {f + c} } } P$ be the lower Darboux sum of $\map f x + c$ on $\closedint a b$ belonging to $P$.
Let:
:$\ds m_k^{\paren {f + c} } = \map {\inf_{x \mathop \in \closedint {x_{k - 1} } {x_k} } } {\map f x + c}$
where $k \in \set {0, 1, \ldots, n}$.
So:
{{begin-eqn}}
{{eqn | l = m_k^{\paren {f + c} }
      | r = \map {\inf_{x \mathop \in \closedint {x_{k - 1} } {x_k} } } {\map f x + c}
      | c = 
}}
{{eqn | r = c + \map {\inf_{x \mathop \in \closedint {x_{k - 1} } {x_k} } } {\map f x}
      | c =
}}
{{eqn | r = c + m_k^{\paren f}
      | c =
}}
{{end-eqn}}
It follows that:
{{begin-eqn}}
{{eqn | l = \map {L^{\paren {f + c} } } P
      | r = \sum_{k \mathop = 1}^n {m_k^{\paren {f + c} } } \paren {x_k - x_{k - 1} }
      | c = 
}}
{{eqn | r = \sum_{k \mathop = 1}^n m_k^{\paren f} \paren {x_k - x_{k - 1} } + c \sum_{k \mathop = 1}^n \paren {x_k - x_{k - 1} }
      | c = 
}}
{{eqn | r = \map {L^{\paren f} } P + c \paren {b - a}
      | c = as $\ds \sum_{k \mathop = 1}^n \paren {x_k - x_{k - 1} }$ telescopes
}}
{{end-eqn}}
So from the definition of definite integral, it follows that:
{{begin-eqn}}
{{eqn | l = \int_a^b \paren {\map f t + c} \rd t
      | r = \map {\sup_P} {\map {L^{\paren {f + c} } } P}
      | c = 
}}
{{eqn | r = \map {\sup_P} {\map {L^{\paren f} } P + c \paren {b - a} }
      | c = 
}}
{{eqn | r = \map {\sup_P} {\map {L^{\paren f} } P} + c \paren {b - a}
      | c = 
}}
{{eqn | r = \int_a^b \map f t \rd t + c \paren {b - a}
      | c = 
}}
{{end-eqn}}
{{Qed}}