avewright/proofwiki-math huggingface dataset:
Theorem: Area of Circle

The area $A$ of a circle is given by:
:$A = \pi r^2$
where $r$ is the radius of the circle.

Proof:
:400px
Construct a circle with radius $r$ and circumference $c$, whose area is denoted by $C$.
Construct a triangle with height $r$ and base $c$, whose area is denoted by $T$.
=== Lemma $1$ ===
{{:Area of Circle/Proof 3/Lemma 1}}{{qed|lemma}}
=== Lemma $2$ ===
{{:Area of Circle/Proof 3/Lemma 2}}{{qed|lemma}}
=== Lemma $3$ ===
{{:Area of Circle/Proof 3/Lemma 3}}{{qed|lemma}}
=== Final Proof ===
From Lemma $2$:
:$T \ge C$
From Lemma $3$:
:$T \le C$
Therefore:
:$T \mathop = C$
and so from Lemma $1$:
:$C \mathop = T \mathop = \pi r^2$
{{qed}}
Theorem: Area of Circle

The area $A$ of a circle is given by:
:$A = \pi r^2$
where $r$ is the radius of the circle.

Proof:
Expressing the area in polar coordinates:
{{begin-eqn}}
{{eqn | l = \iint \rd A
      | r = \int_0^r \int_0^{2 \pi} t \rd t \rd \theta
      | c = 
}}
{{eqn | r = \intlimits {\int_0^r t \theta} 0 {2 \pi} \rd t
      | c = 
}}
{{eqn | r = \int_0^r 2 \pi t \rd t
      | c = 
}}
{{eqn | r = 2 \pi \paren {\intlimits {\frac 1 2 t^2} 0 r}
      | c = 
}}
{{eqn | r = 2 \pi \paren {\frac 1 2 r^2}
      | c = 
}}
{{eqn | r = \pi r^2
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Area of Circle

The area $A$ of a circle is given by:
:$A = \pi r^2$
where $r$ is the radius of the circle.

Proof:
From Equation of Circle:
:$x^2 + y^2 = r^2$
Let $A$ be the area of the circle whose equation is given by $x^2 + y^2 = r^2$.
We have that:
:$y = \pm \sqrt {r^2 - x^2}$
For the upper half of the circle:
:$y = +\sqrt {r^2 - x^2}$
Thus for the right hand half of the upper half of the circle:
{{begin-eqn}}
{{eqn | l = \frac A 4
      | r = \int_0^r \sqrt {r^2 - x^2} \rd x
}}
{{eqn | r = \frac {\pi r^2} 4
      | c = Definite Integral from $0$ to $r$ of $\sqrt {r^2 - x^2}$
}}
{{end-eqn}}
Hence the result.
{{qed}}
Theorem: Distance Formula

The distance $d$ between two points $A = \tuple {x_1, y_1}$ and $B = \tuple {x_2, y_2}$ on a Cartesian plane is:
:$d = \sqrt {\paren {x_1 - x_2}^2 + \paren {y_1 - y_2}^2}$

Proof:
The distance in the horizontal direction between $A$ and $B$ is given by $\size {x_1 - x_2}$.
The distance in the vertical direction between $A$ and $B$ is given by $\size {y_1 - y_2}$.
By definition, the angle between a horizontal and a vertical line is a right angle.
So when we place a point $C = \tuple {x_1, y_2}$, $\triangle ABC$ is a right triangle.
Thus, by Pythagoras's Theorem:
:$d^2 = \size {x_1 - x_2}^2 + \size {y_1 - y_2}^2$
and the result follows.
{{qed}}
Theorem: Null URM Program Computes Identity Function

The null URM program computes the '''identity function''' $I_\N: \N \to \N$, defined as:
:$\forall n \in \N: \map {I_\N} n = n$

Proof:
The null URM program by definition has no instructions.
Therefore, the contents of $R_1$ remain unchanged when "running" it.
{{qed}}
Category:Null URM Program
Category:URM Programs
Category:Identity Mappings
65n8m35btsd14erhzyw0kkxv192buj6
Theorem: Composition of One-Variable URM Computable Functions

Let $f: \N \to \N$ and $g: \N \to \N$ be URM computable functions of one variable.
Let $f \circ g$ be the composition of $f$ and $g$.
Then $f \circ g: \N \to \N$ is a URM computable function.

Proof:
Let $f: \N \to \N$ and $g: \N \to \N$ be URM computable functions of one variable.
Let $P$ be a URM program which computes $f$.
Let $Q$ be a URM program which computes $g$.
Let $s = \map \lambda Q$ be the number of basic instructions in $Q$.
Let $u = \map \rho Q$ be the number of registers used by $Q$.
In order to compute $f \circ g$ the program must compute $g$ first (by running $Q$), then use the output of $Q$ as the input of $P$, which must then compute $f$.
After $Q$ has computed the value of $\map g n$, its output is to be found in $R_1$.
Its instruction pointer is greater than $s$, and may at this point be indeterminate.
Also, the contents of $R_2, R_3, \ldots, R_u$ are also indeterminate.
So we need to do the following things:
# The instruction pointer needs to be set to the line immediately after the end of $Q$, that is, to line $s+1$.
# The registers used by $Q$, except $R_1$, the one holding the output of $Q$, must be set to $0$. So a Clear Registers Program $\map Z {2, u}$ must be appended to the end of $Q$.
# The program $P$ must be appended to the end of $Q$ with $\map Z {2, u}$ appended. However, $P$ no longer starts at line $1$ but at line $\tuple {q + u - 1}$, so any <tt>Jump</tt> instructions of the form $\map J {m, n, q}$ in $P$ must have $q$ changed to $\tuple {q + u - 1}$.
When that has been achieved, the following happens:
# The program runs $Q$, amended if necessary so that the instruction pointer ends up at $s+1$.
# The contents of $R_2$ to $R_u$ are then set to zero.
# $P$ is now run, with the output of $Q$ in its input $R_1$, and all the other registers set to zero.
The output of $P$ can now be found in $R_1$.
The resulting program $Q$ followed by $\map Z {2, u}$ followed by $P$ is called:
* the '''concatenation of $Q$ and $P$''', or, in general:
* a '''concatenated''' program,
and is denoted $Q * P$.
Note that this is read:
* Run $Q$ first;
* Then run $P$.
So it is read from '''left to right'''.
In that sense the notation is different from that of $f \circ g$ for the composition of $f$ and $g$, which is read from '''right to left'''.
So $f \circ g$ is computed by $Q * P$.
{{qed}}
Its length $\map \lambda {Q * P}$ is given as:
:$\map \lambda {Q * P} = \map \lambda Q + \paren {u - 1} \map \lambda P$
The $u - 1$ comes from the length of the Clear Registers Program.
Thus we have an algorithm for concatenating two URM programs, as follows:
Theorem: Concatenation of URM Programs is Associative

Let $P, Q, R$ be one-variable URM programs.
Then the concatenated URM programs $P * \paren {Q * R}$ and $\paren {P * Q} * R$ are the same.

Proof:
For ease of analysis, let us assume that:
:Each of $P$ and $Q$ have already had the appropriate Clear Registers Program $\map Z {2, \map \rho P}$ and $\map Z {2, \map \rho Q}$ appended to them
:Each of $P$ and $Q$ have already had the appropriate amendments made to their exit jumps so as to lead to the first line of the appropriate Clear Registers Program. (Note that if the latter is a null URM program, this will be the line immediately following the end of the program).
Thus we can discuss $P$ and $Q$ without reference to these technical details.
When concatenating programs, the only amendments made to the programs themselves are to the contents of the <tt>Jump</tt>.
So it is clear that the number, type and order of the basic instructions of both programs are the same.
All we have to consider are the amendments to the <tt>Jump</tt>s.
Suppose the lengths of $P$ and $Q$ are as follows:
:$\map \lambda P = t$
:$\map \lambda Q = s$
First we look at the <tt>Jump</tt>s of $R$.
When we form $\paren {Q * R}$, every <tt>Jump</tt> of $R$ of the form $\map J {m, n, q}$ is replaced by $\map J {m, n, q + s}$.
Then when forming $P * \paren {Q * R}$ the <tt>Jump</tt> $\map J {m, n, q + s}$ is replaced by $\map J {m, n, q + s + t}$.
On the other hand, when we form $\paren {P * Q} * R$, every <tt>Jump</tt> of $R$ of the form $\map J {m, n, q}$ is replaced directly by $\map J {m, n, q + \paren {s + t} }$.
Thus the <tt>Jump</tt>s of $R$ have been replaced by the same instructions in each of $\paren {P * Q} * R$ and $P * \paren {Q * R}$.
Now we look at the <tt>Jump</tt>s of $Q$.
When forming $\paren {Q * R}$, we have already ensured that every <tt>Jump</tt> of $Q$ of the form $\map J {m, n, q}$ where $q > s$ has been replaced by $\map J {m, n, s + 1}$.
So when forming $P * \paren {Q * R}$ the <tt>Jump</tt> $\map J {m, n, s + 1}$ is replaced by $\map J {m, n, s + t + 1}$.
On the other hand, when forming $\paren {P * Q}$, every <tt>Jump</tt> of $Q$ of the form $\map J {m, n, q}$ is replaced by $\map J {m, n, q + t}$.
We have that $\paren {P * Q}$ has $s + t$ instructions. When $q > s$, we take account of the fact that $q + t > s + t$.
So in $\paren {P * Q} * R$, <tt>Jump</tt>s of the form $\map J {m, n, s + 1}$ are replaced by $\map J {m, n, s + t + 1}$.
This agrees with the corresponding <tt>Jump</tt>s in $P * \paren {Q * R}$.
Similarly, we can show that all other <tt>Jump</tt>s of $Q$, and all <tt>Jump</tt>s of $P$, are amended in exactly the same way in each of $\paren {P * Q} * R$ and $P * \paren {Q * R}\right)$.
Hence the result.
{{qed}}
Category:URM Programs
ijpjhuroxk728ote6neotfp4oehspe7
Theorem: Primitive of Cosine Function

:$\ds \int \cos x \rd x = \sin x + C$

Proof:
From Derivative of Sine Function:
:$\dfrac \d {\d x} \sin x = \cos x$
The result follows from the definition of primitive.
{{Qed}}
Theorem: Primitive of Cosine Function

:$\ds \int \cos x \rd x = \sin x + C$

Proof:
{{begin-eqn}}
{{eqn | l = \int \cos x \rd x
      | r = \frac 1 2 \int \paren {e^{i x} + e^{-i x} } \rd x
      | c = Euler's Cosine Identity
}}
{{eqn | r = \frac 1 {2 i} \paren {e^{i x} - e^{-i x} } + C
      | c = Primitive of Exponential of a x
}}
{{eqn | r = \sin x + C
      | c = Euler's Sine Identity
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Sine Function

:$\ds \int \sin x \rd x = -\cos x + C$

Proof:
From Derivative of Cosine Function:
:$\map {\dfrac \d {\d x} } {-\cos x} = \sin x$
The result follows from the definition of primitive.
{{qed}}
Theorem: Normalized URM Program

Let $P$ be a URM program.
Let $l = \map \lambda P$ be the number of basic instructions in $P$.
Let $u = \map \rho P$ be the number of registers used by $P$.
Then $P$ can be modified as follows:
:Every <tt>Jump</tt> of the form $\map J {m, n, q}$ where $q > l$ may be replaced by $\map J {m, n, l + 1}$
:If $u > 0$, a Clear Registers Program $\map Z {2, u}$ can be appended to the end of $P$ at lines $l + 1$ to $l + u - 1$.
The new program $P'$ that results from the above modifications produces exactly the same output as $P$ for each input.
Note now though that $\map \lambda {P'} = l + u - 1$.
Such a program as $P'$ is called a '''normalized URM program'''.
The point of doing this is so as to make programs easier to concatenate. Once the above have been done, each program has a well-defined exit line which can be used as the start line of the program that immediately follows it.

Proof:
Each <tt>Jump</tt> of the form $\map J {m, n, q}$ where $q > l$ leads to a line which does not contain an instruction.
The line $\map J {m, n, l + 1}$ likewise contains no instructions, by definition.
Therefore, when jumping to $\map J {m, n, l + 1}$ the program behaves in exactly the same way: that is, it stops when the instruction $\map J {m, n, l + 1}$ causes the program to jump to line $l + 1$.
After the URM program has terminated, its output sits in $R_1$ by convention.
Once the URM program reaches line $l + 1$ it has by definition terminated, and because of the modifications to the <tt>Jump</tt>s as defined above, there is no other way that it ''can'' terminate.
Any further instructions that are added to a URM program that are placed at line $l + 1$ and those following will therefore be executed in order (as long as none of them are <tt>Jump</tt>s) and the program will then ''really'' terminate.
By adding the Clear Registers Program $\map Z {2, u}$ to the end of $P$, the only effect this will have on the operation of the program is to clear all the registers to $0$ except the one the output is in.
{{qed}}
Category:URM Programs
3idjvvy7g1q60kp5zl2886w4xbxk2n4
Theorem: Block Copy Program

Let $k, m, n \in \N$ be natural numbers such that:
* $k \ge 1$;
* $\size {m - n} \ge k$.
The URM program defined as:
{|
|-
! align="right" | Line !!
! align="left" | Command
|-
| align="right" | $1$ ||
| align="left" | $\map C {m, n}$
|-
| align="right" | $2$ ||
| align="left" | $\map C {m + 1, n + 1}$
|-
| align="right" | $\vdots$ ||
| align="left" | $\vdots$
|-
| align="right" | $k$ ||
| align="left" | $\map C {m + k - 1, n + k - 1}$
|}
is called a '''block copy program'''.
It is abbreviated $\map C {m, n, k}$.
It has the effect of copying the contents of registers $R_m, R_{m + 1}, \ldots, R_{m + k - 1}$ into the registers $R_n, R_{n + 1}, \ldots, R_{n + k - 1}$ respectively.
It has length defined as $\map \lambda {\map C {m, n, k} } = k$.

Proof:
Immediate.
{{Qed}}
Category:URM Programs
6xd5p0svdom0u5gch47nnjtclz687el
Theorem: Primitive Recursive Function is URM Computable

Every primitive recursive function is URM computable.

Proof:
This follows immediately from:
* The fact that the basic primitive recursive functions are URM computable;
* Functions obtained by substitution from URM computable functions are URM computable;
* Functions obtained by primitive recursion from URM computable functions are URM computable;
* The definition of primitive recursive function.
{{qed}}
Theorem: Constant Function is Primitive Recursive

The constant function $f_c: \N \to \N$, defined as:
:$\map {f_c} n = c$ where $c \in \N$
is primitive recursive.

Proof:
The proof proceeds by the Principle of Mathematical Induction.
Theorem: Heron's Formula

Let $\triangle ABC$ be a triangle with sides $a$, $b$ and $c$ opposite vertices $A$, $B$ and $C$ respectively.
Then the area $\AA$ of $\triangle ABC$ is given by:
:$\AA = \sqrt {s \paren {s - a} \paren {s - b} \paren {s - c} }$
where $s = \dfrac {a + b + c} 2$ is the semiperimeter of $\triangle ABC$.

Proof:
Construct the altitude from $A$.
Let the length of the altitude be $h$ and the foot of the altitude be $D$.
Let the distance from $D$ to $B$ be $z$.
:300px
From Pythagoras's Theorem:
:$\paren 1: \quad h^2 + \paren {a - z}^2 = b^2$
and:
:$\paren 2: \quad h^2 + z^2 = c^2$
By subtracting $\paren 1$ from $\paren 2$:
:$2 a z - a^2 = c^2 - b^2$
which can be expressed in terms of $z$ as:
:$z = \dfrac {a^2 + c^2 - b^2} {2 a}$
Substituting for $z$ in $\paren 2$ and simplifying yields:
:$h = \sqrt {c^2 - \paren {\dfrac {a^2 + c^2 - b^2} {2a} }^2}$
and so:
{{begin-eqn}}
{{eqn | l = \AA
      | r = \frac 1 2 a \sqrt {c^2 - \paren {\frac{a^2 + c^2 - b^2}{2a} }^2}
      | c = Area of Triangle in Terms of Side and Altitude
}}
{{eqn | r = \sqrt {\frac {4 c^2 a^2 - \left({a^2 + c^2 - b^2}\right)^2} {16} }
}}
{{eqn | r = \sqrt {\frac {\paren {2ac - a^2 - c^2 + b^2} \paren {2ac + a^2 + c^2 - b^2} } {16} }
      | c = Difference of Two Squares
}}
{{eqn | r = \sqrt {\frac {\paren {b^2 - \paren {a - c}^2} \paren {\paren {a + c}^2 - b^2} } {16} }
}}
{{eqn | r = \sqrt {\frac {\paren {b - a + c} \paren {b + a - c} \paren {a + c - b} \paren {a + b + c} } {16} }
      | c = Difference of Two Squares
}}
{{eqn | r = \sqrt {\frac {\paren {a + b + c} \paren {a + b - c} \paren {a - b + c} \paren {-a + b + c} } {16} }
}}
{{eqn | r = \sqrt {\paren {\frac {a + b + c} 2} \paren {\frac {a + b + c} 2 - c} \paren {\frac {a + b + c} 2 - b} \paren {\frac {a + b + c} 2 - a} }
}}
{{eqn | r = \sqrt {s \paren {s - c} \paren {s - b} \paren{s - a} }
      | c = {{Defof|Semiperimeter}}
}}
{{end-eqn}}
{{qed}}
Theorem: Heron's Formula

Let $\triangle ABC$ be a triangle with sides $a$, $b$ and $c$ opposite vertices $A$, $B$ and $C$ respectively.
Then the area $\AA$ of $\triangle ABC$ is given by:
:$\AA = \sqrt {s \paren {s - a} \paren {s - b} \paren {s - c} }$
where $s = \dfrac {a + b + c} 2$ is the semiperimeter of $\triangle ABC$.

Proof:
A triangle can be considered as a cyclic quadrilateral one of whose sides has degenerated to zero.
From Brahmagupta's Formula, the area of a cyclic quadrilateral is given by:
:$\sqrt {\paren {s - a} \paren {s - b} \paren {s - c} \paren {s - d}}$
where $s$ is the semiperimeter:
:$s = \dfrac {a + b + c + d} 2$
The result follows by letting $d$ tend to zero.
{{qed}}
Theorem: Heron's Formula

Let $\triangle ABC$ be a triangle with sides $a$, $b$ and $c$ opposite vertices $A$, $B$ and $C$ respectively.
Then the area $\AA$ of $\triangle ABC$ is given by:
:$\AA = \sqrt {s \paren {s - a} \paren {s - b} \paren {s - c} }$
where $s = \dfrac {a + b + c} 2$ is the semiperimeter of $\triangle ABC$.

Proof:
:700px
Let $\AA$ be the area of $\triangle ABC$.
Construct the incircle of $\triangle ABC$.
Let the incenter of $\triangle ABC$ be $M$.
Let the inradius of $\triangle ABC$ be $r$.
$\triangle ABC$ is made up of three triangles: $\triangle AMB$, $\triangle BMC$ and $\triangle CMA$.
From Area of Triangle in Terms of Side and Altitude, the areas of $\triangle AMB$, $\triangle BMC$ and $\triangle CMA$ are given by:
:$\Area \paren {\triangle AMB} = \dfrac {r c} 2$
:$\Area \paren {\triangle BMC} = \dfrac {r a} 2$
:$\Area \paren {\triangle CMA} = \dfrac {r b} 2$
Thus:
:$(1): \quad \AA = \dfrac {r \paren {c + a + b} } 2 = r s$
where $s$ is the semiperimeter of $\triangle ABC$.
Construct the excircle of $\triangle ABC$ with excenter $N$ tangent to $AB$, and to $AC$ and $BC$ produced at $D$ and $E$ respectively.
By Length of Tangent to Excircle:
:$s = CD = CE$
Therefore:
:$DA = s - b$
:$EB = s - a$
Note that:
:$AF + DA = BG + EB$
and:
:$AF + BG = C$
We need to show that $\triangle MAF \sim \triangle DNA$.
Note that:
:$AM$ bisects $\angle BAC$
:$AN$ bisects $\angle BAD$
But $\angle BAC$ and $\angle BAD$ are supplementary angles.
Hence the half-angles $\angle MAF$ and $\angle DAN$ are complementary angles.
It follows that:
:$\angle MAF = \angle DNA$
Since $\triangle MAF$ and $\triangle DNA$ are both right triangles:
:$\triangle DNA \sim \triangle MAF$
As right triangles sharing an acute angle:
:$\triangle NDC \sim \triangle MFC$
from which:
{{begin-eqn}}
{{eqn | l = \dfrac R r
      | r = \dfrac s {s - c}
}}
{{eqn | l = \dfrac R {s - b}
      | r = \dfrac {s - a} r
}}
{{eqn | ll= \leadsto
      | l = R
      | r = \dfrac {r s} {s - c}
      | c = substituting for $R$
}}
{{eqn | r = \dfrac {\paren {s - a} \paren {s - b} } r
      | c = 
}}
{{eqn | ll= \leadsto
      | l = r^2
      | r = \dfrac {\paren {s - a} \paren {s - b} \paren {s - c} } s
      | c = rearranging
}}
{{eqn | ll= \leadsto
      | l = \AA
      | r = s \sqrt {\dfrac {\paren {s - a} \paren {s - b} \paren {s - c} } s}
      | c = from $(1)$
}}
{{eqn | r = \sqrt {s \paren {s - a} \paren {s - b} \paren {s - c} }
      | c = simplifying
}}
{{end-eqn}}
{{qed}}
Theorem: Heron's Formula

Let $\triangle ABC$ be a triangle with sides $a$, $b$ and $c$ opposite vertices $A$, $B$ and $C$ respectively.
Then the area $\AA$ of $\triangle ABC$ is given by:
:$\AA = \sqrt {s \paren {s - a} \paren {s - b} \paren {s - c} }$
where $s = \dfrac {a + b + c} 2$ is the semiperimeter of $\triangle ABC$.

Proof:
{{begin-eqn}}
{{eqn | l = \AA
      | r = \dfrac {a b \sin C} 2
      | c = Area of Triangle in Terms of Two Sides and Angle
}}
{{eqn | r = \dfrac {a b} 2 \cdot 2 \sin \dfrac C 2 \cos \dfrac C 2
      | c = Double Angle Formula for Sine
}}
{{eqn | r = a b \sqrt {\dfrac {\paren {s - a} \paren {s - b} } {a b} } \sqrt {\dfrac {s \paren {s - c} } {a b} }
      | c = Sine of Half Angle in Triangle, Cosine of Half Angle in Triangle
}}
{{eqn | r = \sqrt {s \paren {s - a} \paren {s - b} \paren {s - c} }
      | c = simplifying
}}
{{end-eqn}}
Theorem: Addition is Primitive Recursive

The function $\Add: \N^2 \to \N$, defined as:
:$\map \Add {n, m} = n + m$
is primitive recursive.

Proof:
We observe that:
:$\map \Add {n, 0} = n + 0 = n$
and that
:$\map \Add {n, m + 1} = n + \paren {m + 1} = \paren {n + m} + 1 = \map \Succ {\map \Add {n, m} }$
where $\Succ$ is the successor function, which is a basic primitive recursive function.
We are to show that $\Add$ is defined by primitive recursion.
So we need to find primitive recursive functions $f: \N \to \N$ and $g: \N^3 \to \N$ such that:
:$\map \Add {n, m} = \begin{cases}
\map f n & : m = 0 \\
\map g {n, m - 1, \map \Add {n, m - 1} } & : m > 0
\end{cases}$
Because $\map \Add {n, 0} = n$, we can see that:
:$\map f n = n$.
That is, $f$ is the basic primitive recursive function $\pr_1^1: \N \to \N$.
Because $\map \Add {n, m + 1} = \map \Succ {\map \Add {n, m} }$, we can see that $g$ needs to be a function which maps the ordered triple $\tuple {n, m, \map \Add {n, m} }$ to $\map \Succ {\map \Add {n, m} }$.
A suitable function is:
:$g: \N^3 \to \N$ where $\map g {n_1, n_2, n_3} = \map \Succ {n_3}$
because then:
:$\map g {n, m, \map \Add {n, m} } = \map \Succ {\map \Add {n, m} }$
It remains to be shown that $g$ is primitive recursive.
This is achieved by using the projection function:
:$\map g {n_1, n_2, n_3} = \map \Succ {\map {\pr_3^3} {n_1, n_2, n_3} }$
Thus $g$ is obtained by substitution from the basic primitive recursive functions $\Succ$ and $\pr_3^3$ and so is primitive recursive.
So $\Add$ is obtained by primitive recursion from the primitive recursive functions $\pr_1^1$ and $g$, and so is primitive recursive.
{{qed}}
Category:Primitive Recursive Functions
95nbchdnbufaaogke2kaxcs6usiyunb
Theorem: Exact Form of Prime-Counting Function

Let: 
:$\ds \map \Pi x = \map \Li x - \sum_\rho \map \Li {x^\rho} - \map \ln 2 + \int_x^\infty \frac {\d t} {t \paren {t^2 - 1} \map \ln t}$ 
where:
:$\map \Li x$ is the offset logarithmic integral
:the sum $\ds \sum_\rho$ is taken over all $0 < \rho \in \R$ such that the zeta function $\map \zeta {\alpha + i \rho} = 0$ for some $\alpha \in \R$.
Then the prime-counting function is precisely:
:$\ds \map \pi x = \sum_{n \mathop = 1}^\infty \paren {\frac {\map \mu n} n \map \Pi {x^{1 / n} } }$
where $\map \mu n$ denotes the Möbius function.

Proof:
{{proof wanted}}
Category:Number Theory
9yaebhxvtysdkgbw2vyfjvgca7a6f15
Theorem: Multiplication is Primitive Recursive

The function $\operatorname{mult}: \N^2 \to \N$, defined as:
:$\map \Mult {n, m} = n \times m$
is primitive recursive.

Proof:
We observe that:
:$\map \Mult {n, 0} = n \times 0 = 0$
and that
:$\map \Mult {n, m + 1} = n \times \paren {m + 1} = \paren {n \times m} + n = \map \Add {\map \Mult {n, m}, n}$.
We are to show that $\Mult$ is obtained by primitive recursion from known primitive recursive functions.
First we note that:
:$\map \Mult {n, 0} = 0 = \map \Zero n$
where $\map \Zero n$ is the  zero function, which is basic primitive recursive.
Next we need to find a primitive recursive function $g: \N^3 \to \N$ such that:
:$\map \Mult {n, m + 1} = \map g {n, m, \map \Mult {n, m} }$
Because $\map \Mult {n, m + 1} = \map \Add {\map \Mult {n, m}, n}$, we see that a suitable function for $g$ is:
:$\map g {n_1, n_2, n_3} = \map \Add {n_3, n_1}$
Using projection functions, we can write this as:
:$\map g {n_1, n_2, n_3} = \map \Add {\map {\pr_3^3} {n_1, n_2, n_3}, \map {\pr_1^3} {n_1, n_2, n_3} }$.
This shows that $g$ is obtained by substitution from $\Add$, which is primitive recursive, and the basic primitive recursive functions $\pr_3^3$ and $\pr_1^3$.
So $g$ is primitive recursive.
So $\Mult$ is obtained by primitive recursion from the primitive recursive functions $g$ and $\Zero$, and so is primitive recursive.
{{qed}}
Category:Primitive Recursive Functions
nuewcnrlqmjys1fme8euz4utktjtlv1
Theorem: Linear Function is Primitive Recursive

The function $f: \N \to \N$, defined as:
:$\map f n = a n + b$
where $a$ and $b$ are constants, is primitive recursive.

Proof:
We have that:
{{begin-eqn}}
{{eqn | l = a n + b
      | r = \map \Add {\map \Mult {a, n}, b}
      | c = 
}}
{{eqn | r = \map \Add {\map \Mult {a, n}, \map {f_b} n}
      | c = 
}}
{{eqn | r = \map \Add {\map \Mult {\map {f_a} n, \map {\pr_1^1} n}, \map {f_b} n}
      | c = 
}}
{{end-eqn}}
where:
* $\Mult$ is primitive recursive
* $\Add$ is primitive recursive
* the constant functions $f_a$ and $f_b$ are primitive recursive
* The projection function $\pr_1^1$ is a basic primitive recursive function.
Note that we need to use the projection function (in this case, the identity function) in order to satisfy the definition of substitution, even when there is only one variable.
So $\Mult$ is obtained by using two levels of substitution from the above primitive recursive functions.
{{qed}}
Category:Primitive Recursive Functions
4yt2hry6ggmnj7w5vojcg1hwjv9binf