Type  Label  Description 
Statement 

Theorem  selberg2b 20701* 
Convert eventual boundedness in selberg2 20700 to boundedness on any
interval .
(We have to bound away from zero because the
log terms diverge at zero.) (Contributed by Mario Carneiro,
25May2016.)

ψ
Λ ψ 

Theorem  chpdifbndlem1 20702* 
Lemma for chpdifbnd 20704. (Contributed by Mario Carneiro,
25May2016.)

ψ Λ ψ
ψ ψ


Theorem  chpdifbndlem2 20703* 
Lemma for chpdifbnd 20704. (Contributed by Mario Carneiro,
25May2016.)

ψ Λ ψ ψ ψ


Theorem  chpdifbnd 20704* 
A bound on the difference of nearby ψ values. Theorem 10.5.2 of
[Shapiro], p. 427. (Contributed by
Mario Carneiro, 25May2016.)

ψ ψ


Theorem  logdivbnd 20705* 
A bound on a sum of logs, used in pntlemk 20755. This is not as precise as
logdivsum 20682 in its asymptotic behavior, but it is valid
for all
and does not require a limit value. (Contributed by Mario Carneiro,
13Apr2016.)



Theorem  selberg3lem1 20706* 
Introduce a log weighting on the summands of
ΛΛ, the core of selberg2 20700
(written here as Λψ ). Equation
10.4.21 of [Shapiro], p. 422.
(Contributed by Mario Carneiro,
30May2016.)

Λ ψ
Λ ψ Λ ψ 

Theorem  selberg3lem2 20707* 
Lemma for selberg3 20708. Equation 10.4.21 of [Shapiro], p. 422.
(Contributed by Mario Carneiro, 30May2016.)

Λ ψ Λ ψ 

Theorem  selberg3 20708* 
Introduce a log weighting on the summands of
ΛΛ, the core of selberg2 20700
(written here as Λψ ). Equation
10.6.7 of [Shapiro], p. 422.
(Contributed by Mario Carneiro,
30May2016.)

ψ
Λ ψ 

Theorem  selberg4lem1 20709* 
Lemma for selberg4 20710. Equation 10.4.20 of [Shapiro], p. 422.
(Contributed by Mario Carneiro, 30May2016.)

Λ ψ
Λ Λ ψ


Theorem  selberg4 20710* 
The Selberg symmetry formula for products of three primes, instead of
two. The sum here can also be written in the symmetric form
ΛΛΛ; we eliminate one
of the nested sums by using the definition of
ψ Λ. This statement can thus
equivalently be written ψ
ΛΛΛ .
Equation 10.4.23 of [Shapiro], p. 422.
(Contributed by Mario Carneiro,
30May2016.)

ψ
Λ Λ ψ 

Theorem  pntrval 20711* 
Define the residual of the second Chebyshev function. The goal is to
have , or .
(Contributed
by Mario Carneiro, 8Apr2016.)

ψ ψ


Theorem  pntrf 20712 
Functionality of the residual. Lemma for pnt 20763. (Contributed by Mario
Carneiro, 8Apr2016.)

ψ 

Theorem  pntrmax 20713* 
There is a bound on the residual valid for all . (Contributed by
Mario Carneiro, 9Apr2016.)

ψ


Theorem  pntrsumo1 20714* 
A bound on a sum over . Equation 10.1.16 of [Shapiro], p.
403.
(Contributed by Mario Carneiro, 25May2016.)

ψ


Theorem  pntrsumbnd 20715* 
A bound on a sum over . Equation 10.1.16 of [Shapiro], p.
403.
(Contributed by Mario Carneiro, 25May2016.)

ψ


Theorem  pntrsumbnd2 20716* 
A bound on a sum over . Equation 10.1.16 of [Shapiro], p.
403.
(Contributed by Mario Carneiro, 14Apr2016.)

ψ


Theorem  selbergr 20717* 
Selberg's symmetry formula, using the residual of the second Chebyshev
function. Equation 10.6.2 of [Shapiro], p. 428. (Contributed by Mario
Carneiro, 16Apr2016.)

ψ
Λ 

Theorem  selberg3r 20718* 
Selberg's symmetry formula, using the residual of the second Chebyshev
function. Equation 10.6.8 of [Shapiro], p. 429. (Contributed by Mario
Carneiro, 30May2016.)

ψ
Λ 

Theorem  selberg4r 20719* 
Selberg's symmetry formula, using the residual of the second Chebyshev
function. Equation 10.6.11 of [Shapiro], p. 430. (Contributed by Mario
Carneiro, 30May2016.)

ψ
Λ Λ


Theorem  selberg34r 20720* 
The sum of selberg3r 20718 and selberg4r 20719. (Contributed by Mario
Carneiro, 31May2016.)

ψ
Λ Λ Λ 

Theorem  pntsval 20721* 
Define the "Selberg function", whose asymptotic behavior is the
content
of selberg 20697. (Contributed by Mario Carneiro,
31May2016.)

Λ ψ
Λ ψ 

Theorem  pntsf 20722* 
Functionality of the Selberg function. (Contributed by Mario Carneiro,
31May2016.)

Λ ψ 

Theorem  selbergs 20723* 
Selberg's symmetry formula, using the definition of the Selberg
function. (Contributed by Mario Carneiro, 31May2016.)

Λ ψ


Theorem  selbergsb 20724* 
Selberg's symmetry formula, using the definition of the Selberg
function. (Contributed by Mario Carneiro, 31May2016.)

Λ ψ


Theorem  pntsval2 20725* 
The Selberg function can be expressed using the convolution product of
the von Mangoldt function with itself. (Contributed by Mario Carneiro,
31May2016.)

Λ ψ
Λ
Λ Λ 

Theorem  pntrlog2bndlem1 20726* 
The sum of selberg3r 20718 and selberg4r 20719. (Contributed by Mario
Carneiro, 31May2016.)

Λ ψ ψ


Theorem  pntrlog2bndlem2 20727* 
Lemma for pntrlog2bnd 20733. Bound on the difference between the
Selberg
function and its approximation, inside a sum. (Contributed by Mario
Carneiro, 31May2016.)

Λ ψ ψ ψ


Theorem  pntrlog2bndlem3 20728* 
Lemma for pntrlog2bnd 20733. Bound on the difference between the
Selberg
function and its approximation, inside a sum. (Contributed by Mario
Carneiro, 31May2016.)

Λ ψ ψ


Theorem  pntrlog2bndlem4 20729* 
Lemma for pntrlog2bnd 20733. Bound on the difference between the
Selberg
function and its approximation, inside a sum. (Contributed by Mario
Carneiro, 31May2016.)

Λ ψ ψ


Theorem  pntrlog2bndlem5 20730* 
Lemma for pntrlog2bnd 20733. Bound on the difference between the
Selberg
function and its approximation, inside a sum. (Contributed by Mario
Carneiro, 31May2016.)

Λ ψ ψ


Theorem  pntrlog2bndlem6a 20731* 
Lemma for pntrlog2bndlem6 20732. (Contributed by Mario Carneiro,
7Jun2016.)

Λ ψ ψ


Theorem  pntrlog2bndlem6 20732* 
Lemma for pntrlog2bnd 20733. Bound on the difference between the
Selberg
function and its approximation, inside a sum. (Contributed by Mario
Carneiro, 31May2016.)

Λ ψ ψ


Theorem  pntrlog2bnd 20733* 
A bound on . Equation 10.6.15 of [Shapiro],
p. 431. (Contributed by Mario Carneiro, 1Jun2016.)

ψ


Theorem  pntpbnd1a 20734* 
Lemma for pntpbnd 20737. (Contributed by Mario Carneiro,
11Apr2016.)

ψ


Theorem  pntpbnd1 20735* 
Lemma for pntpbnd 20737. (Contributed by Mario Carneiro,
11Apr2016.)

ψ


Theorem  pntpbnd2 20736* 
Lemma for pntpbnd 20737. (Contributed by Mario Carneiro,
11Apr2016.)

ψ


Theorem  pntpbnd 20737* 
Lemma for pnt 20763. Establish smallness of at a point. Lemma
10.6.1 in [Shapiro], p. 436.
(Contributed by Mario Carneiro,
10Apr2016.)

ψ


Theorem  pntibndlem1 20738 
Lemma for pntibnd 20742. (Contributed by Mario Carneiro,
10Apr2016.)

ψ


Theorem  pntibndlem2a 20739* 
Lemma for pntibndlem2 20740. (Contributed by Mario Carneiro,
7Jun2016.)

ψ


Theorem  pntibndlem2 20740* 
Lemma for pntibnd 20742. The main work, after eliminating all the
quantifiers. (Contributed by Mario Carneiro, 10Apr2016.)

ψ
ψ ψ


Theorem  pntibndlem3 20741* 
Lemma for pntibnd 20742. Package up pntibndlem2 20740 in quantifiers.
(Contributed by Mario Carneiro, 10Apr2016.)

ψ


Theorem  pntibnd 20742* 
Lemma for pnt 20763. Establish smallness of on an interval. Lemma
10.6.2 in [Shapiro], p. 436.
(Contributed by Mario Carneiro,
10Apr2016.)

ψ


Theorem  pntlemd 20743 
Lemma for pnt 20763. Closure for the constants used in the
proof. For
comparison with Equation 10.6.27 of [Shapiro], p. 434, is C^*,
is c_{1}, is λ, is c_{2}, and is c_{3}.
(Contributed by Mario Carneiro, 13Apr2016.)

ψ
;


Theorem  pntlemc 20744* 
Lemma for pnt 20763. Closure for the constants used in the
proof. For
comparison with Equation 10.6.27 of [Shapiro], p. 434, is α,
is ε,
and is K.
(Contributed by Mario Carneiro,
13Apr2016.)

ψ
;


Theorem  pntlema 20745* 
Lemma for pnt 20763. Closure for the constants used in the
proof. The
mammoth expression is a number large enough to satisfy all the
lower bounds needed for . For comparison with Equation 10.6.27 of
[Shapiro], p. 434, is x_{2},
is x_{1}, is the bigO
constant in Equation 10.6.29 of [Shapiro], p. 435, and is the
unnamed lower bound of "for sufficiently large x" in Equation
10.6.34 of
[Shapiro], p. 436. (Contributed by
Mario Carneiro, 13Apr2016.)

ψ
;
;


Theorem  pntlemb 20746* 
Lemma for pnt 20763. Unpack all the lower bounds contained in
, in
the form they will be used. For comparison with Equation 10.6.27 of
[Shapiro], p. 434, is x. (Contributed by Mario Carneiro,
13Apr2016.)

ψ
;
;
; 

Theorem  pntlemg 20747* 
Lemma for pnt 20763. Closure for the constants used in the
proof. For
comparison with Equation 10.6.27 of [Shapiro], p. 434, is j^*
and is
ĵ. (Contributed by Mario Carneiro, 13Apr2016.)

ψ
;
;


Theorem  pntlemh 20748* 
Lemma for pnt 20763. Bounds on the subintervals in the
induction.
(Contributed by Mario Carneiro, 13Apr2016.)

ψ
;
;


Theorem  pntlemn 20749* 
Lemma for pnt 20763. The "naive" base bound, which we
will slightly
improve. (Contributed by Mario Carneiro, 13Apr2016.)

ψ
;
;


Theorem  pntlemq 20750* 
Lemma for pntlemj 20752. (Contributed by Mario Carneiro,
7Jun2016.)

ψ
;
;
..^ 

Theorem  pntlemr 20751* 
Lemma for pntlemj 20752. (Contributed by Mario Carneiro,
7Jun2016.)

ψ
;
;
..^


Theorem  pntlemj 20752* 
Lemma for pnt 20763. The induction step. Using pntibnd 20742, we find
an interval in which is
sufficiently
large and has a much smaller value,
(instead
of our original bound ). (Contributed by
Mario Carneiro, 13Apr2016.)

ψ
;
;
..^


Theorem  pntlemi 20753* 
Lemma for pnt 20763. Eliminate some assumptions from pntlemj 20752.
(Contributed by Mario Carneiro, 13Apr2016.)

ψ
;
;
..^


Theorem  pntlemf 20754* 
Lemma for pnt 20763. Add up the pieces in pntlemi 20753 to get an estimate
slightly better than the naive lower bound . (Contributed by
Mario Carneiro, 13Apr2016.)

ψ
;
;
;


Theorem  pntlemk 20755* 
Lemma for pnt 20763. Evaluate the naive part of the estimate.
(Contributed by Mario Carneiro, 14Apr2016.)

ψ
;
;


Theorem  pntlemo 20756* 
Lemma for pnt 20763. Combine all the estimates to establish a
smaller
eventual bound on .
(Contributed by Mario Carneiro,
14Apr2016.)

ψ
;
;


Theorem  pntleme 20757* 
Lemma for pnt 20763. Package up pntlemo 20756 in quantifiers. (Contributed by
Mario Carneiro, 14Apr2016.)

ψ
;
;


Theorem  pntlem3 20758* 
Lemma for pnt 20763. Equation 10.6.35 in [Shapiro], p. 436.
(Contributed by Mario Carneiro, 8Apr2016.)

ψ
ψ


Theorem  pntlemp 20759* 
Lemma for pnt 20763. Wrapping up more quantifiers.
(Contributed by
Mario Carneiro, 14Apr2016.)

ψ
;


Theorem  pntleml 20760* 
Lemma for pnt 20763. Equation 10.6.35 in [Shapiro], p. 436. (Contributed
by Mario Carneiro, 14Apr2016.)

ψ
;
ψ


Theorem  pnt3 20761 
The Prime Number Theorem, version 3: the second Chebyshev function tends
asymptotically to . (Contributed by Mario Carneiro,
1Jun2016.)

ψ 

Theorem  pnt2 20762 
The Prime Number Theorem, version 2: the first Chebyshev function tends
asymptotically to . (Contributed by Mario Carneiro,
1Jun2016.)



Theorem  pnt 20763 
The Prime Number Theorem: the number of prime numbers less than
tends asymptotically to as goes to infinity.
(Contributed by Mario Carneiro, 1Jun2016.)

π


13.4.13 Ostrowski's theorem


Theorem  abvcxp 20764* 
Raising an absolute value to a power less than one yields another
absolute value. (Contributed by Mario Carneiro, 8Sep2014.)

AbsVal 

Theorem  padicfval 20765* 
Value of the padic absolute value. (Contributed by Mario Carneiro,
8Sep2014.)



Theorem  padicval 20766* 
Value of the padic absolute value. (Contributed by Mario Carneiro,
8Sep2014.)



Theorem  ostth2lem1 20767* 
Lemma for ostth2 20786, although it is just a simple statement
about
exponentials which does not involve any specifics of ostth2 20786. If a
power is upper bounded by a linear term, the exponent must be less than
one. Or in bigO notation, for any
.
(Contributed by Mario Carneiro, 10Sep2014.)



Theorem  qrngbas 20768 
The base set of the field of rationals. (Contributed by Mario Carneiro,
8Sep2014.)

ℂ_{fld}
↾_{s} 

Theorem  qdrng 20769 
The rationals form a division ring. (Contributed by Mario Carneiro,
8Sep2014.)

ℂ_{fld}
↾_{s} 

Theorem  qrng0 20770 
The zero element of the field of rationals. (Contributed by Mario
Carneiro, 8Sep2014.)

ℂ_{fld}
↾_{s} 

Theorem  qrng1 20771 
The unit element of the field of rationals. (Contributed by Mario
Carneiro, 8Sep2014.)

ℂ_{fld}
↾_{s} 

Theorem  qrngneg 20772 
The additive inverse in the field of rationals. (Contributed by Mario
Carneiro, 8Sep2014.)

ℂ_{fld}
↾_{s}


Theorem  qrngdiv 20773 
The division operation in the field of rationals. (Contributed by Mario
Carneiro, 8Sep2014.)

ℂ_{fld}
↾_{s} /_{r} 

Theorem  qabvle 20774 
By using induction on , we show a longrange inequality coming
from the triangle inequality. (Contributed by Mario Carneiro,
10Sep2014.)

ℂ_{fld}
↾_{s} AbsVal


Theorem  qabvexp 20775 
Induct the product rule abvmul 15594 to find the absolute value of a power.
(Contributed by Mario Carneiro, 10Sep2014.)

ℂ_{fld}
↾_{s} AbsVal 

Theorem  ostthlem1 20776* 
Lemma for ostth 20788. If two absolute values agree on the
positive
integers greater than one, then they agree for all rational numbers
and thus are equal as functions. (Contributed by Mario Carneiro,
9Sep2014.)

ℂ_{fld}
↾_{s} AbsVal


Theorem  ostthlem2 20777* 
Lemma for ostth 20788. Refine ostthlem1 20776 so that it is sufficient to
only show equality on the primes. (Contributed by Mario Carneiro,
9Sep2014.) (Revised by Mario Carneiro, 20Jun2015.)

ℂ_{fld}
↾_{s} AbsVal 

Theorem  qabsabv 20778 
The regular absolute value function on the rationals is in fact an
absolute value under our definition. (Contributed by Mario Carneiro,
9Sep2014.)

ℂ_{fld}
↾_{s} AbsVal 

Theorem  padicabv 20779* 
The padic absolute value (with arbitrary base) is an absolute value.
(Contributed by Mario Carneiro, 9Sep2014.)

ℂ_{fld}
↾_{s} AbsVal 

Theorem  padicabvf 20780* 
The padic absolute value is an absolute value. (Contributed by Mario
Carneiro, 9Sep2014.)

ℂ_{fld}
↾_{s} AbsVal


Theorem  padicabvcxp 20781* 
All positive powers of the padic absolute value are absolute values.
(Contributed by Mario Carneiro, 9Sep2014.)

ℂ_{fld}
↾_{s} AbsVal


Theorem  ostth1 20782* 
 Lemma for ostth 20788: trivial case. (Not that the proof is
trivial,
but that we are proving that the function is trivial.) If is
equal to on
the primes, then by complete induction and the
multiplicative property abvmul 15594 of the absolute value, is
equal to on
all the integers, and ostthlem1 20776 extends this to
the other rational numbers. (Contributed by Mario Carneiro,
10Sep2014.)

ℂ_{fld}
↾_{s} AbsVal


Theorem  ostth2lem2 20783* 
Lemma for ostth2 20786. (Contributed by Mario Carneiro,
10Sep2014.)

ℂ_{fld}
↾_{s} AbsVal


Theorem  ostth2lem3 20784* 
Lemma for ostth2 20786. (Contributed by Mario Carneiro,
10Sep2014.)

ℂ_{fld}
↾_{s} AbsVal


Theorem  ostth2lem4 20785* 
Lemma for ostth2 20786. (Contributed by Mario Carneiro,
10Sep2014.)

ℂ_{fld}
↾_{s} AbsVal


Theorem  ostth2 20786* 
 Lemma for ostth 20788: regular case. (Contributed by Mario
Carneiro,
10Sep2014.)

ℂ_{fld}
↾_{s} AbsVal


Theorem  ostth3 20787* 
 Lemma for ostth 20788: padic case. (Contributed by Mario
Carneiro,
10Sep2014.)

ℂ_{fld}
↾_{s} AbsVal


Theorem  ostth 20788* 
Ostrowski's theorem, which classifies all absolute values on .
Any such absolute value must either be the trivial absolute value
, a constant
exponent times the regular absolute
value, or a positive exponent times the padic absolute value.
(Contributed by Mario Carneiro, 10Sep2014.)

ℂ_{fld}
↾_{s} AbsVal


PART 14 GUIDES AND
MISCELLANEA


14.1 Guides (conventions, explanations, and
examples)


14.1.1 Conventions
This section describes the conventions we use.
However, these conventions often refer to existing mathematical
practices, which are discussed in more detail in other references.
Logic and set theory provide a foundation for all of mathematics. To learn
about them, you should study one or more of the references listed below.
We indicate references using square brackets. The
textbooks provide a motivation for what we are doing, whereas Metamath lets you
see in detail all hidden and implicit steps. Most standard theorems are
accompanied by citations. Some closely followed texts include the following:
 Axioms of propositional calculus  [Margaris].
 Axioms of predicate calculus  [Megill] (System S3' in the article
referenced).
 Theorems of propositional calculus  [WhiteheadRussell].
 Theorems of pure predicate calculus  [Margaris].
 Theorems of equality and substitution  [Monk2], [Tarski], [Megill].
 Axioms of set theory  [BellMachover].
 Development of set theory  [TakeutiZaring]. (The first part of [Quine]
has a good explanation of the powerful device of "virtual" or
class abstractions, which is essential to our development.)
 Construction of real and complex numbers  [Gleason]
 Theorems about real numbers  [Apostol]


Theorem  conventions 20789 
Here are some of the conventions we use in the
Metamath Proof Explorer (aka "set.mm"), and how they correspond to
typical textbook language (skipping the many cases
where they're identical):
 Notation.
Where possible, the notation attempts to conform to modern
conventions, with variations due to our choice of the axiom system
or to make proofs shorter. However, our notation is strictly
sequential (lefttoright). For example, summation is written in the
form (dfsum 12159) which denotes that index
variable ranges over when evaluating . Thus,
means 1/2 + 1/4 + 1/8 + ...
= 1 (geoihalfsum 12338). Also, the method of definition,
the axioms for predicate calculus, and the
development of substitution are somewhat different from those found
in standard texts. For example, the expressions for the
axioms were designed for direct derivation of
standard results without excessive use of metatheorems.
(See Theorem 9.7 of [Megill] p. 448 for a rigorous justification.)
The notation is usually explained in more detail when first introduced.
 Axiomatic assertions ($a).
All axiomatic assertions ($a statements)
starting with " " have labels starting
with "ax" (axioms) or "df" (definitions). A statement with a
label starting with "ax" corresponds to what is traditionally
called an axiom. A statement with a label starting with "df"
introduces new symbols or a new relationship among symbols
that can be eliminated; they always extend the definition of
a wff or class. Metamath blindly treats $a statements as new
given facts but does not try to justify them. The mmj2 program
will justify the definitions as sound, except for 4 (dfbi,
dfcleq, dfclel, dfclab) that require a more complex
metalogical justification by hand.
 Proven axioms.
In some cases we wish to treat an expression as an axiom in
later theorems, even though it can be proved. For example,
we derive the postulates or axioms of complex arithmetic as
theorems of ZFC set theory. For convenience, after deriving
the postulates we reintroduce them as new axioms on
top of set theory. This lets us easily identify which axioms
are needed for a particular complex number proof, without the
obfuscation of the set theory used to derive them. For more, see
http://us.metamath.org/mpeuni/mmcomplex.html. When we wish
to use a previouslyproven assertion as an axiom, our convention
is that we use the
regular "axNAME" label naming convention to define the axiom,
but we precede it with a proof of the same statement with the label
"axNAME" . An example is complex arithmetic axiom ax1cn 8795,
proven by the preceding theorem ax1cn 8771.
The metamath.exe program will warn if an axiom does not match the
preceding theorem that justifies it if the names match in this way.
 Definitions (df...).
We encourage definitions to include hypertext links to proven examples.
 Statements with hypotheses. Many theorems and some axioms,
such as axmp 8, have hypotheses that must be satisfied in order for
the conclusion to hold, in this case min and maj. When presented in
summarized form such as in the Theorem List (click on "Nearby theorems"
on the axmp 8 page), the hypotheses are connected with an ampersand and
separated from the conclusion with a big arrow, such as in "
& => ". These symbols are not
part of the Metamath language but are just informal notation meaning
"and" and "implies".
 Discouraged use and modification.
If something should only be used in limited ways, it is marked with
"(New usage is discouraged.)". This is used, for example, when something
can be constructed in more than one way, and we do not want later
theorems to depend on that specific construction.
This marking is also used if we want later proofs to use proven axioms.
For example, we want later proofs to
use ax1cn 8795 (not ax1cn 8771) and ax1ne0 8806 (not ax1ne0 8782), as these
are proven axioms for complex arithmetic. Thus, both
ax1cn 8771 and ax1ne0 8782 are marked as "(New usage is discouraged.)".
In some cases a proof should not normally be changed, e.g., when it
demonstrates some specific technique.
These are marked with "(Proof modification is discouraged.)".
 New definitions infrequent.
Typically we are minimalist when introducing new definitions; they are
introduced only when a clear advantage becomes apparent for reducing
the number of symbols, shortening proofs, etc. We generally avoid
the introduction of gratuitous definitions because each one requires
associated theorems and additional elimination steps in proofs.
For example, we use and for inequality expressions, and
use instead of sinh
for the hyperbolic sine.
 Axiom of choice.
The axiom of choice (dfac 7743) is widely accepted, and ZFC is the most
commonlyaccepted fundamental set of axioms for mathematics.
However, there have been and still are some lingering controversies
about the Axiom of Choice. Therefore, where a proof
does not require the axiom of choice, we prefer that proof instead.
E.g., our proof of the SchroederBernstein Theorem (sbth 6981)
does not use the axiom of choice.
In some cases, the weaker axiom of countable choice (axcc 8061)
or axiom of dependent choice (axdc 8072) can be used instead.
 Variables.
Typically, Greek letters
( = phi, = psi, = chi, etc.),... are used for
propositional (wff) variables;
, , ,... for individual (set) variables;
and , , ,... for class variables.
 Turnstile.
"", meaning "It is provable that," is the first token
of all assertions
and hypotheses that aren't syntax constructions. This is a standard
convention in logic. For us, it also prevents any ambiguity with
statements that are syntax constructions, such as "wff ".
 Biconditional ().
There are basically two ways to maximize the effectiveness of
biconditionals ():
you can either have onedirectional simplifications of all theorems
that produce biconditionals, or you can have onedirectional
simplifications of theorems that consume biconditionals.
Some tools (like Lean) follow the first approach, but set.mm follows
the second approach. Practically, this means that in set.mm, for
every theorem that uses an implication in the hypothesis, like
axmp 8, there is a corresponding version with a biconditional or a
reversed biconditional, like mpbi 199 or mpbir 200. We prefer this
second approach because the number of duplications in the second
approach is bounded by the size of the propositional calculus section,
which is much smaller than the number of possible theorems in all later
sections that produce biconditionals. So although theorems like
biimpi 186 are available, in most cases there is already a theorem that
combines it with your theorem of choice, like mpbir2an 886, sylbir 204,
or 3imtr4i 257.
 Substitution.
" " should be read "the wff that results from the
proper substitution of for in wff ." See dfsb 1630
and the related dfsbc 2992 and dfcsb 3082.
 Isa set.
" " should be read
"Class is a set (i.e. exists)."
This is a convenient convention based on
Definition 2.9 of [Quine] p. 19. See dfv 2790 and isset 2792.
 Converse.
"" should be read "converse of (relation) "
and is the same as the more standard notation R^{1}
(the standard notation is ambiguous). See dfcnv 4697.
This can be used to define a subset, e.g., dftan 12353 notates
"the set of values whose cosine is a nonzero complex number" as
.
 Function application.
"()" should be read "the value
of function at " and has the same meaning as the more
familiar but ambiguous notation F(x). For example,
(see cos0 12430). The left apostrophe notation
originated with Peano and was adopted in Definition *30.01 of
[WhiteheadRussell] p. 235, Definition 10.11 of [Quine] p. 68, and
Definition 6.11 of [TakeutiZaring] p. 26. See dffv 5263.
In the ASCII (input) representation there are spaces around the grave
accent; there is a single accent when it is used directly,
and it is doubled within comments.
 Infix and parentheses.
When a function that takes two classes and produces a class
is applied as part of an infix expression, the expression is always
surrounded by parentheses (see dfov 5861).
For example, the in ; see 2p2e4 9842.
Function application is itself an example of this.
Similarly, predicate expressions
in infix form that take two or three wffs and produce a wff
are also always surrounded by parentheses, such as
, , , and
(see wi 4, dfor 359, dfan 360, and dfbi 177 respectively).
In contrast, a binary relation (which compares two classes and
produces a wff) applied in an infix expression is not
surrounded by parentheses.
This includes set membership (see wel 1685),
equality (see dfcleq 2276),
subset (see dfss 3166), and
lessthan (see dflt 8750). For the general definition
of a binary relation in the form , see dfbr 4024.
For example, ( see 0lt1 9296) does not use parentheses.
 Unary minus.
The symbol is used to indicate a unary minus, e.g., .
It is specially defined because it is so commonly used.
See cneg 9038.
 Function definition.
Functions are typically defined by first defining the constant symbol
(using $c) and declaring that its symbol is a class with the
label cNAME (e.g., ccos 12346).
The function is then defined labelled dfNAME; definitions
are typically given using the mapsto notation (e.g., dfcos 12352).
Typically there are other proofs such as its
closure labelled NAMEcl (e.g., coscl 12407), its
function application form labelled NAMEval (e.g., cosval 12403),
and at least one simple value (e.g., cos0 12430).
 Factorial.
The factorial function is traditionally a postfix operation,
but we treat it as a normal function applied in prefix form, e.g.,
; (dffac 11289 and fac4 11296).
 Unambiguous symbols.
A given symbol has a single unambiguous meaning in general.
Thus, where the literature might use the same symbol with different
meanings, here we use different (variant) symbols for different
meanings. These variant symbols often have suffixes, subscripts,
or underlines to distinguish them. For example, here
"" always means the value zero (df0 8744), while
"" is the group identity element (df0g 13404),
"" is the poset zero (dfp0 14145),
"" is the zero polynomial (df0p 19025),
"" is the zero vector in a normed complex vector space
(df0v 21154), and
"" is a class variable for use as a connective symbol
(this is used, for example, in p0val 14147).
There are other class variables used as connective symbols
where traditional notation would use ambiguous symbols, including
"", "", "", and "".
These symbols are very similar to traditional notation, but because
they are different symbols they eliminate ambiguity.
 Natural numbers.
There are different definitions of "natural" numbers in the literature.
We use (dfnn 9747) for the integer numbers starting
from 1, and (dfn0 9966) for the set of nonnegative integers
starting at zero.
 Decimal numbers.
Numbers larger than ten are often expressed in base 10
using the decimal constructor dfdec 10125, e.g.,
;;; (see 4001prm 13143 for a proof that 4001 is prime).
 Theorem forms.
We often call a theorem a "deduction" whenever the conclusion and
all hypotheses are each prefixed
with the same antecedent . Deductions are often the
preferred form for theorems because they
allow us to easily use the theorem in places where
(in traditional textbook formalizations) the standard
Deduction Theorem would be used. See, for example, a1d 22.
A deduction hypothesis can have an indirect antecedent via definitions,
e.g., see lhop 19363. Deductions have a label suffix of "d"
if there are other forms of the same theorem. By contrast,
we tend to call the simpler version with no common antecedent an
"inference" and suffix its label with "i"; compare theorem a1i 10.
Finally, a "tautology" would be the form with no hypotheses,
and its label would have no suffix. For example, see pm2.43 47,
pm2.43i 43, and pm2.43d 44.
 Deduction theorem.
The Deduction Theorem is a metalogical theorem that
provides an algorithm for constructing a proof of a theorem from
the proof of its corresponding deduction.
In ordinary mathematics, no one actually carries out the algorithm,
because (in its most basic form) it involves an exponential
explosion of the number of proof steps as more hypotheses are
eliminated. Instead, in ordinary mathematics the Deduction Theorem
is invoked simply to claim that something can be done in principle,
without actually doing it. For more details, see
http://us.metamath.org/mpeuni/mmdeduction.html.
The Deduction Theorem is a metalogical theorem that cannot be
applied directly in metamath, and the explosion of steps would
be a problem anyway, so alternatives are used. One alternative
we use sometimes is the "weak deduction theorem" dedth 3606,
which works in certain cases in set theory. We also
sometimes use dedhb 2935.
However, the primary mechanism we use today for
emulating the deduction theorem is to write proofs in the deduction
theorem form (aka "deduction style") described earlier; the
prefixed mimics the context in a deduction proof system.
In practice this mechanism works very well.
This approach is described in the
deduction form
and natural deduction page; a list of translations
for common natural deduction rules is given in natded 20790.
 Recursion. We define recursive functions
using various "recursion constructors". These allow us to define, with
compact direct definitions, functions that are usually defined in
textbooks with indirect selfreferencing recursive definitions.
This produces compact definition and much simpler proofs, and
greatly reduces the risk of creating unsound definitions.
Examples of recursion constructors include recs in dfrecs 6388,
in dfrdg 6423, seq_{𝜔} in dfseqom 6460, and
in dfseq 11047.
These have characteristic function and initial value .
(_{g} in dfgsum 13405 isn't really designed for arbitrary recursion,
but you could do it with the right magma.)
The logically primary one is dfrecs 6388, but for the "average user"
the most useful one is probably dfseq 11047 provided that
a countable sequence is sufficient for the recursion.
 Extensible structures.
Mathematics includes many structures such as
ring, group, poset, etc. We define an "extensible structure"
which is then used to define group, ring, poset, etc.
This allows theorems from more general structures (groups)
to be reused for more specialized structures (rings) without
having to reprove them. See dfstruct 13150.
 Organizing proofs.
Humans have trouble understanding long proofs.
It is often preferable to break longer proofs into
smaller parts (just as with traditional proofs). In Metamath
this is done by creating separate proofs of the separate parts.
A proof with the sole purpose of supporting a final proof is a
lemma; the naming convention for a lemma is the final proof's name
followed by "lem", and a number if there is more than one. E.g.,
sbthlem1 6971 is the first lemma for sbth 6981. Also, consider proving
reusable results separately, so that others will be able to easily
reuse that part of your work.
 Hypertext links.
We strongly encourage comments to have many links to related material,
with accompanying text that explains the relationship.
These can help readers understand the context.
Links to other statements, or to HTTP/HTTPS URLs,
can be inserted in ASCII source text by prepending a
spaceseparated tilde.
When metamath.exe is used to generate HTML it automatically inserts
hypertext links for syntax used (e.g., every symbol used),
every axiom and definition depended on, the justification
for each step in a proof, and to both the
next and previous assertion.
 Bibliography references.
Please include a bibliographic reference to any external material used.
A name in square brackets in a comment indicates a
bibliographic reference. The full reference must be of the form
KEYWORD IDENTIFIER? NOISEWORD(S)* [AUTHOR(S)] p. NUMBER 
note that this is a very specific form that requires a page number.
There should be no comma between the author reference and the
"p." (a constant indicator).
Whitespace, comma, period, or semicolon should follow NUMBER.
An example is Theorem 3.1 of [Monk1] p. 22,
The KEYWORD, which is not casesensitive,
must be one of the following: Axiom, Chapter, Compare, Condition,
Corollary, Definition, Equation, Example, Exercise, Figure, Item,
Lemma, Lemmas, Line, Lines, Notation, Part, Postulate, Problem,
Property, Proposition, Remark, Rule, Scheme, Section, or Theorem.
The IDENTIFIER is optional, as in for example
"Remark in [Monk1] p. 22".
The NOISEWORDS(S) are zero or more from the list: from, in, of, on.
The AUTHOR(S) must be present in the file identified with the
htmlbibliography assignment (e.g. mmset.html) as a named anchor
(NAME=). If there is more than one document by the same author(s),
add a numeric suffix (as shown here).
The NUMBER is a page number, and may be any alphanumeric string such as
an integer or Roman numeral.
Note that we require page numbers in comments for individual
$a or $p statements. We allow names in square brackets without
page numbers (a reference to an entire document) in
heading comments.
If this is a new reference, please also add it to the
"Bibliography" section of mmset.html.
(The file mmbiblio.html is automatically rebuilt, e.g.,
using the metamath.exe "write bibliography" command.)
 Input format.
The input is in ASCII with twospace indents.
Tab characters are not allowed.
Use embedded math comments or HTML entities for nonASCII characters
(e.g., "é" for "é").
 Information on syntax, axioms, and definitions.
For a hyperlinked list of syntax, axioms, and definitions, see
http://us.metamath.org/mpeuni/mmdefinitions.html.
If you have questions about a specific symbol or axiom, it is best
to go directly to its definition to learn more about it.
The generated HTML for each theorem and axiom includes hypertext
links to each symbol's definition.
Naming conventions
Every statement has a unique identifying label.
We use various label naming conventions to provide
easytoremember hints about their contents.
Labels are not a 1to1 mapping, because that would create
long names that would be difficult to remember and tedious to type.
Instead, label names are relatively short while
suggesting their purpose.
Names are occasionally changed to make them more consistent or
as we find better ways to name them.
Here are a few of the label naming conventions:
 Axioms, definitions, and wff syntax.
As noted earlier, axioms are named "axNAME",
proofs of proven axioms are named "axNAME", and
definitions are named "dfNAME".
Wff syntax declarations have labels beginning with "w"
followed by short fragment suggesting its purpose.
 Hypotheses.
Hypotheses have the name of the final axiom or theorem, followed by
".", followed by a unique id.
 Common names.
If a theorem has a wellknown name, that name (or a short version of it)
is sometimes used directly. Examples include
barbara 2240 and stirling 27838.
 Syntax label fragments.
Most theorems are named using syntax label fragments.
Almost every syntactic construct has a definition labelled "dfNAME",
and NAME normally is the syntax label fragment.
For example, the difference construct
is defined in dfdif 3155, and thus its syntax label fragment is "dif".
Similarly, the singleton construct
has syntax label fragment "sn"
(because it is defined in dfsn 3646),
the subclass (subset) relation has "ss"
(because it is defined in dfss 3166), and
the pair construct has "pr" (dfpr 3647).
Theorem names are often a concatenation of the syntax label fragments
(omitting variables).
For example, a theorem about
involves a difference ("dif")
of a subset ("ss"), and thus is named difss 3303.
Digits are used to represent themselves.
Suffixes (e.g., with numbers) are sometimes used to distinguish
multiple theorems that would otherwise produce the same label.
 Phantom definitions.
In some cases there are common label fragments for something that
could be in a definition, but for technical reasons is not.
The iselementof (is member of) construct
does not have a dfNAME definition; in this case its syntax
label fragment is "el".
Thus, because the theorem beginning with
uses iselementof ("el")
of a difference ("dif") of a singleton ("sn"), it is named eldifsn 3749.
An "n" is often used for negation (), e.g., nan 563.
 Exceptions.
Sometimes there is a definition dfNAME but the
label fragment is not the NAME part.
The table below attempts to list all such cases and marks them in bold.
For example, label fragment
"cn" represents complex numbers (even though its definition
is in dfc 8743) and "re" represents real numbers .
The empty set often uses fragment 0, even though it is defined
in dfnul 3456.
Syntax construct usually uses the fragment "add"
(which is consistent with dfadd 8748),
but "p" is used as the fragment for constant theorems.
Equality often uses "e" as the fragment.
As a result, "two plus two equals four" is named 2p2e4 9842.
 Other markings.
In labels we sometimes use "com" for "commutative",
"ass" for "associative", "rot" for "rotation",
and "di" for "distributive".
 Principia Mathematica.
Proofs of theorems from Principia Mathematica often use a different
naming convention.
They are instead often named "pm" followed by its identifier.
For example, Theorem *2.27 of [WhiteheadRussell] p. 104 is named
pm2.27 35.
 Closures and values.
As noted above,
if a function dfNAME is defined, there is typically a proof
of its value named "NAMEval" and its closure named "NAMEcl".
E.g., for cosine (dfcos 12352) we have
value cosval 12403 and closure coscl 12407.
 Special cases.
Sometimes syntax and related markings are
insufficient to distinguish different theorems.
For example, there are over 100 different
implicationexclusive theorems.
These are then grouped in a more adhoc way that attempts to
make their distinctions clearer.
These often use abbreviations such as "mp" for "modus ponens",
"syl" for syllogism, and "id" for "identity".
It's especially hard to give good names in the propositional
calculus section because there are so few primitives. However,
in most cases this is not a serious problem. There are a few
very common theorems like axmp 8 and syl 15 that you will have no
trouble remembering, a few theorem series like syl*anc and simp*
that you can use parametrically, and a few other useful glue things
for destructuring 'and's and 'or's (see natded 20790 for a list),
and that's about all you need for most things. As for the rest,
you can just assume that if it involves three or less connectives
we probably already have a proof, and searching for it will give
you the name.
 Suffixes.
We sometimes suffix with "v" the label of a theorem
eliminating a hypothesis such as in 19.21 1791 via the use of
distinct variable conditions combined with nfv 1605. Conversely, we
sometimes suffix with "f" the label of a theorem introducing such a
hypothesis to eliminate the need for the distinct variable condition;
e.g. euf 2149 derived from dfeu 2147. The "f" stands for "not free in"
which is less restrictive than "does not occur in."
We sometimes suffix with "s" the label of an inference
that manipulates an
antecedent, leaving the consequent unchanged. The "s" means that the
inference eliminates the need for a syllogism (syl 15) type inference
in a proof. When an inference is converted to a
theorem by eliminating an "is a set" hypothesis, we sometimes
suffix the theorem form with "g" (for "more general") as in
uniex 4516 vs. uniexg 4517.
A theorem name is suffixed with "ALT" if it's an alternative
lesspreferred proof of a theorem.
 Reuse.
When creating a new theorem or axiom, try to reuse abbreviations
used elsewhere. A comment should explain the first use of an
abbreviation.
The following table shows some commonlyused abbreviations in labels,
in alphabetical order.
For each abbreviation we provide a mnenomic to help you remember it,
the source theorem/assumption defining it, an expression showing
what it looks like, whether or not it is a "syntax fragment"
(an abbreviation that indicates a particular kind of syntax), and
hyperlinks to label examples that use the abbreviation.
The abbreviation is bolded if there is a dfNAME definition but
the label fragment is not NAME.
This is not a complete list of abbreviations, though
we do want this to eventually be a complete list of exceptions.
Abbreviation  Mnenomic  Source 
Expression  Syntax?  Example(s) 
add  add (see "p")  dfadd 8748 
 Yes 
addcl 8819, addcom 8998, addass 8824 
ALT  alternative/less preferred (suffix)  
 No  
an  and  dfan 360 
 Yes 
anor 475, iman 413, imnan 411 
ass  associative  
 No  biass 348, orass 510, mulass 8825 
bi  biconditional  dfbi 177 
 Yes  impbid 183 
cn  complex numbers  dfc 8743 
 Yes  nnsscn 9751, nncn 9754 
com  commutative  
 No  orcom 376, bicomi 193, eqcomi 2287 
d  deduction form  
 No  idd 21, impbid 183 
di, distr  distributive  
 No 
andi 837, imdi 352, ordi 834, difindi 3423, ndmovdistr 6009 
dif  difference  dfdif 3155 
 Yes 
difss 3303, difindi 3423 
div  division  dfdiv 9424 
 Yes 
divcl 9430, divval 9426, divmul 9427 
e, eq  equals  dfcleq 2276 
 Yes  2p2e4 9842, uneqri 3317 
el  element of  
 