MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  conventions-labels Structured version   Visualization version   GIF version

Theorem conventions-labels 27812

The following gives conventions used in the Metamath Proof Explorer (MPE, regarding labels. For other conventions, see conventions 27811 and links therein.

Every statement has a unique identifying label, which serves the same purpose as an equation number in a book. We use various label naming conventions to provide easy-to-remember hints about their contents. Labels are not a 1-to-1 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 "ax-NAME", proofs of proven axioms are named "axNAME", and definitions are named "df-NAME". 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 (these ids are usually consecutive integers starting with 1, e.g. for rgen 3131"rgen.1 $e |- ( x e. A -> ph ) $." or letters corresponding to the (main) class variable used in the hypothesis, e.g. for mdet0 20787: "mdet0.d $e |- D = ( N maDet R ) $.").
  • Common names. If a theorem has a well-known name, that name (or a short version of it) is sometimes used directly. Examples include barbara 2746 and stirling 41098.
  • Principia Mathematica. Proofs of theorems from Principia Mathematica often use a special naming convention: "pm" followed by its identifier. For example, Theorem *2.27 of [WhiteheadRussell] p. 104 is named pm2.27 42.
  • 19.x series of theorems. Similar to the conventions for the theorems from Principia Mathematica, theorems from Section 19 of [Margaris] p. 90 often use a special naming convention: "19." resp. "r19." (for corresponding restricted quantifier versions) followed by its identifier. For example, Theorem 38 from Section 19 of [Margaris] p. 90 is labeled 19.38 1937, and the restricted quantifier version of Theorem 21 from Section 19 of [Margaris] p. 90 is labeled r19.21 3165.
  • Characters to be used for labels. Although the specification of Metamath allows for dots/periods "." in any label, it is usually used only in labels for hypotheses (see above). Exceptions are the labels of theorems from Principia Mathematica and the 19.x series of theorems from Section 19 of [Margaris] p. 90 (see above) and 0.999... 14993. Furthermore, the underscore "_" should not be used. Finally, only lower case characters should be used (except the special suffixes OLD, ALT and ALTV mentioned in bullet point "Suffixes"), at least in main (exceptions are tolerated in mathboxes).
  • Syntax label fragments. Most theorems are named using a concatenation of syntax label fragments (omitting variables) that represent the important part of the theorem's main conclusion. Almost every syntactic construct has a definition labeled "df-NAME", and normally NAME is the syntax label fragment. For example, the class difference construct (𝐴𝐵) is defined in df-dif 3801, and thus its syntax label fragment is "dif". Similarly, the subclass relation 𝐴𝐵 has syntax label fragment "ss" because it is defined in df-ss 3812. Most theorem names follow from these fragments, for example, the theorem proving (𝐴𝐵) ⊆ 𝐴 involves a class difference ("dif") of a subset ("ss"), and thus is labeled difss 3966. There are many other syntax label fragments, e.g., singleton construct {𝐴} has syntax label fragment "sn" (because it is defined in df-sn 4400), and the pair construct {𝐴, 𝐵} has fragment "pr" ( from df-pr 4402). 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 is-element-of (is member of) construct 𝐴𝐵 does not have a df-NAME definition; in this case its syntax label fragment is "el". Thus, because the theorem beginning with (𝐴 ∈ (𝐵 ∖ {𝐶}) uses is-element-of ("el") of a class difference ("dif") of a singleton ("sn"), it is labeled eldifsn 4538. An "n" is often used for negation (¬), e.g., nan 864.
  • Exceptions. Sometimes there is a definition df-NAME but the label fragment is not the NAME part. The definition should note this exception as part of its definition. In addition, the table below attempts to list all such cases and marks them in bold. For example, the label fragment "cn" represents complex numbers (even though its definition is in df-c 10265) and "re" represents real numbers ( definition df-r 10269). The empty set often uses fragment 0, even though it is defined in df-nul 4147. The syntax construct (𝐴 + 𝐵) usually uses the fragment "add" (which is consistent with df-add 10270), 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 labeled 2p2e4 11500.
  • Other markings. In labels we sometimes use "com" for "commutative", "ass" for "associative", "rot" for "rotation", and "di" for "distributive".
  • Focus on the important part of the conclusion. Typically the conclusion is the part the user is most interested in. So, a rough guideline is that a label typically provides a hint about only the conclusion; a label rarely says anything about the hypotheses or antecedents. If there are multiple theorems with the same conclusion but different hypotheses/antecedents, then the labels will need to differ; those label differences should emphasize what is different. There is no need to always fully describe the conclusion; just identify the important part. For example, cos0 15259 is the theorem that provides the value for the cosine of 0; we would need to look at the theorem itself to see what that value is. The label "cos0" is concise and we use it instead of "cos0eq1". There is no need to add the "eq1", because there will never be a case where we have to disambiguate between different values produced by the cosine of zero, and we generally prefer shorter labels if they are unambiguous.
  • Closures and values. As noted above, if a function df-NAME is defined, there is typically a proof of its value labeled "NAMEval" and of its closure labeld "NAMEcl". E.g., for cosine (df-cos 15180) we have value cosval 15232 and closure coscl 15236.
  • Special cases. Sometimes, syntax and related markings are insufficient to distinguish different theorems. For example, there are over a hundred different implication-only theorems. They are grouped in a more ad-hoc 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 is 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 ax-mp 5 and syl 17 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 27814 for a list), and that is about all you need for most things. As for the rest, you can just assume that if it involves at most three connectives, then it is probably already proved in, and searching for it will give you the label.
  • Suffixes. Suffixes are used to indicate the form of a theorem (see above). Additionally, we sometimes suffix with "v" the label of a theorem eliminating a hypothesis such as 𝑥𝜑 in 19.21 2249 via the use of disjoint variable conditions combined with nfv 2013. If two (or three) such hypotheses are eliminated, the suffix "vv" resp. "vvv" is used, e.g. exlimivv 2031. Conversely, we sometimes suffix with "f" the label of a theorem introducing such a hypothesis to eliminate the need for the disjoint variable condition; e.g. euf 2648 derived from eu6 2645. The "f" stands for "not free in" which is less restrictive than "does not occur in." The suffix "b" often means "biconditional" (, "iff" , "if and only if"), e.g. sspwb 5140. 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 17) -type inference in a proof. A theorem label is suffixed with "ALT" if it provides an alternate less-preferred proof of a theorem (e.g., the proof is clearer but uses more axioms than the preferred version). The "ALT" may be further suffixed with a number if there is more than one alternate theorem. Furthermore, a theorem label is suffixed with "OLD" if there is a new version of it and the OLD version is obsolete (and will be removed within one year). Finally, it should be mentioned that suffixes can be combined, for example in cbvaldva 2431 (cbval 2423 in deduction form "d" with a not free variable replaced by a disjoint variable condition "v" with a conjunction as antecedent "a"). As a general rule, the suffixes for the theorem forms ("i", "d" or "g") should be the first of multiple suffixes, as for example in vtocldf 3472 or rabeqif 3404. Here is a non-exhaustive list of common suffixes:
    • a : theorem having a conjunction as antecedent
    • b : theorem expressing a logical equivalence
    • c : contraction (e.g., sylc 65, syl2anc 579), commutes (e.g., biimpac 472)
    • d : theorem in deduction form
    • f : theorem with a hypothesis such as 𝑥𝜑
    • g : theorem in closed form having an "is a set" antecedent
    • i : theorem in inference form
    • l : theorem concerning something at the left
    • r : theorem concerning something at the right
    • r : theorem with something reversed (e.g., a biconditional)
    • s : inference that manipulates an antecedent ("s" refers to an application of syl 17 that is eliminated)
    • v : theorem with one (main) disjoint variable condition
    • vv : theorem with two (main) disjoint variable conditions
    • w : weak(er) form of a theorem
    • ALT : alternate proof of a theorem
    • ALTV : alternate version of a theorem or definition
    • OLD : old/obsolete version of a theorem/definition/proof
  • 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 commonly used abbreviations in labels, in alphabetical order. For each abbreviation we provide a mnenomic, the source theorem or the 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 df-NAME 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.

AbbreviationMnenomicSource ExpressionSyntax?Example(s)
aand (suffix) No biimpa 470, rexlimiva 3237
ablAbelian group df-abl 18556 Abel Yes ablgrp 18558, zringabl 20189
absabsorption No ressabs 16310
absabsolute value (of a complex number) df-abs 14360 (abs‘𝐴) Yes absval 14362, absneg 14401, abs1 14421
adadding No adantr 474, ad2antlr 718
addadd (see "p") df-add 10270 (𝐴 + 𝐵) Yes addcl 10341, addcom 10548, addass 10346
al"for all" 𝑥𝜑 No alim 1909, alex 1924
ALTalternative/less preferred (suffix) No idALT 23
anand df-an 387 (𝜑𝜓) Yes anor 1010, iman 392, imnan 390
antantecedent No adantr 474
assassociative No biass 376, orass 950, mulass 10347
asymasymmetric, antisymmetric No intasym 5757, asymref 5758, posasymb 17312
axaxiom No ax6dgen 2179, ax1cn 10293
bas, base base (set of an extensible structure) df-base 16235 (Base‘𝑆) Yes baseval 16288, ressbas 16300, cnfldbas 20117
b, bibiconditional ("iff", "if and only if") df-bi 199 (𝜑𝜓) Yes impbid 204, sspwb 5140
brbinary relation df-br 4876 𝐴𝑅𝐵 Yes brab1 4923, brun 4926
cbvchange bound variable No cbvalivw 2111, cbvrex 3380
clclosure No ifclda 4342, ovrcl 6950, zaddcl 11752
cncomplex numbers df-c 10265 Yes nnsscn 11362, nncn 11366
cnfldfield of complex numbers df-cnfld 20114 fld Yes cnfldbas 20117, cnfldinv 20144
cntzcentralizer df-cntz 18107 (Cntz‘𝑀) Yes cntzfval 18110, dprdfcntz 18775
cnvconverse df-cnv 5354 𝐴 Yes opelcnvg 5539, f1ocnv 6394
cocomposition df-co 5355 (𝐴𝐵) Yes cnvco 5544, fmptco 6651
comcommutative No orcom 901, bicomi 216, eqcomi 2834
concontradiction, contraposition No condan 852, con2d 132
csbclass substitution df-csb 3758 𝐴 / 𝑥𝐵 Yes csbid 3765, csbie2g 3788
cygcyclic group df-cyg 18640 CycGrp Yes iscyg 18641, zringcyg 20206
ddeduction form (suffix) No idd 24, impbid 204
df(alternate) definition (prefix) No dfrel2 5828, dffn2 6284
di, distrdistributive No andi 1035, imdi 381, ordi 1033, difindi 4113, ndmovdistr 7088
difclass difference df-dif 3801 (𝐴𝐵) Yes difss 3966, difindi 4113
divdivision df-div 11017 (𝐴 / 𝐵) Yes divcl 11023, divval 11019, divmul 11020
dmdomain df-dm 5356 dom 𝐴 Yes dmmpt 5875, iswrddm0 13605
e, eq, equequals df-cleq 2818 𝐴 = 𝐵 Yes 2p2e4 11500, uneqri 3984, equtr 2125
edgedge df-edg 26353 (Edg‘𝐺) Yes edgopval 26356, usgredgppr 26499
elelement of 𝐴𝐵 Yes eldif 3808, eldifsn 4538, elssuni 4691
enequinumerous df-en 𝐴𝐵 Yes domen 8241, enfi 8451
eu"there exists exactly one" eu6 2645 ∃!𝑥𝜑 Yes euex 2650, euabsn 4481
exexists (i.e. is a set) ∈ V No brrelex1 5394, 0ex 5016
ex"there exists (at least one)" df-ex 1879 𝑥𝜑 Yes exim 1932, alex 1924
expexport No expt 170, expcom 404
f"not free in" (suffix) No equs45f 2480, sbf 2511
ffunction df-f 6131 𝐹:𝐴𝐵 Yes fssxp 6301, opelf 6306
falfalse df-fal 1670 Yes bifal 1673, falantru 1692
fifinite intersection df-fi 8592 (fi‘𝐵) Yes fival 8593, inelfi 8599
fi, finfinite df-fin 8232 Fin Yes isfi 8252, snfi 8313, onfin 8426
fldfield (Note: there is an alternative definition Fld of a field, see df-fld 34332) df-field 19113 Field Yes isfld 19119, fldidom 19673
fnfunction with domain df-fn 6130 𝐴 Fn 𝐵 Yes ffn 6282, fndm 6227
frgpfree group df-frgp 18481 (freeGrp‘𝐼) Yes frgpval 18531, frgpadd 18536
fsuppfinitely supported function df-fsupp 8551 𝑅 finSupp 𝑍 Yes isfsupp 8554, fdmfisuppfi 8559, fsuppco 8582
funfunction df-fun 6129 Fun 𝐹 Yes funrel 6144, ffun 6285
fvfunction value df-fv 6135 (𝐹𝐴) Yes fvres 6456, swrdfv 13717
fzfinite set of sequential integers df-fz 12627 (𝑀...𝑁) Yes fzval 12628, eluzfz 12637
fz0finite set of sequential nonnegative integers (0...𝑁) Yes nn0fz0 12739, fz0tp 12742
fzohalf-open integer range df-fzo 12768 (𝑀..^𝑁) Yes elfzo 12774, elfzofz 12787
gmore general (suffix); eliminates "is a set" hypotheses No uniexg 7220
grgraph No uhgrf 26367, isumgr 26400, usgrres1 26619
grpgroup df-grp 17786 Grp Yes isgrp 17789, tgpgrp 22259
gsumgroup sum df-gsum 16463 (𝐺 Σg 𝐹) Yes gsumval 17631, gsumwrev 18153
hashsize (of a set) df-hash 13418 (♯‘𝐴) Yes hashgval 13420, hashfz1 13433, hashcl 13444
hbhypothesis builder (prefix) No hbxfrbi 1923, hbald 2218, hbequid 34983
hm(monoid, group, ring) homomorphism No ismhm 17697, isghm 18018, isrhm 19084
iinference (suffix) No eleq1i 2897, tcsni 8903
iimplication (suffix) No brwdomi 8749, infeq5i 8817
ididentity No biid 253
iedgindexed edge df-iedg 26304 (iEdg‘𝐺) Yes iedgval0 26345, edgiedgb 26359
idmidempotent No anidm 560, tpidm13 4511
im, impimplication (label often omitted) df-im 14225 (𝐴𝐵) Yes iman 392, imnan 390, impbidd 202
imaimage df-ima 5359 (𝐴𝐵) Yes resima 5671, imaundi 5790
impimport No biimpa 470, impcom 398
inintersection df-in 3805 (𝐴𝐵) Yes elin 4025, incom 4034
infinfimum df-inf 8624 inf(ℝ+, ℝ*, < ) Yes fiinfcl 8682, infiso 8689 (something a) ...? No isring 18912
jjoining, disjoining No jc 161, jaoi 888
lleft No olcd 905, simpl 476
mapmapping operation or set exponentiation df-map 8129 (𝐴𝑚 𝐵) Yes mapvalg 8137, elmapex 8148
matmatrix df-mat 20588 (𝑁 Mat 𝑅) Yes matval 20591, matring 20623
mdetdeterminant (of a square matrix) df-mdet 20766 (𝑁 maDet 𝑅) Yes mdetleib 20768, mdetrlin 20783
mgmmagma df-mgm 17602 Magma Yes mgmidmo 17619, mgmlrid 17626, ismgm 17603
mgpmultiplicative group df-mgp 18851 (mulGrp‘𝑅) Yes mgpress 18861, ringmgp 18914
mndmonoid df-mnd 17655 Mnd Yes mndass 17662, mndodcong 18319
mo"there exists at most one" df-mo 2605 ∃*𝑥𝜑 Yes eumo 2651, moim 2610
mpmodus ponens ax-mp 5 No mpd 15, mpi 20
mptmodus ponendo tollens No mptnan 1867, mptxor 1868
mptmaps-to notation for a function df-mpt 4955 (𝑥𝐴𝐵) Yes fconstmpt 5402, resmpt 5690
mpt2maps-to notation for an operation df-mpt2 6915 (𝑥𝐴, 𝑦𝐵𝐶) Yes mpt2mpt 7017, resmpt2 7023
mulmultiplication (see "t") df-mul 10271 (𝐴 · 𝐵) Yes mulcl 10343, divmul 11020, mulcom 10345, mulass 10347
n, notnot ¬ 𝜑 Yes nan 864, notnotr 128
nenot equaldf-ne 𝐴𝐵 Yes exmidne 3009, neeqtrd 3068
nelnot element ofdf-nel 𝐴𝐵 Yes neli 3104, nnel 3111
ne0not equal to zero (see n0) ≠ 0 No negne0d 10718, ine0 10796, gt0ne0 10824
nf "not free in" (prefix) No nfnd 1958
ngpnormed group df-ngp 22765 NrmGrp Yes isngp 22777, ngptps 22783
nmnorm (on a group or ring) df-nm 22764 (norm‘𝑊) Yes nmval 22771, subgnm 22814
nnpositive integers df-nn 11358 Yes nnsscn 11362, nncn 11366
nn0nonnegative integers df-n0 11626 0 Yes nnnn0 11633, nn0cn 11636
n0not the empty set (see ne0) ≠ ∅ No n0i 4151, vn0 4156, ssn0 4203
OLDold, obsolete (to be removed soon) No 19.43OLD 1986
onordinal number df-on 5971 𝐴 ∈ On Yes elon 5976, 1on 7838 onelon 5992
opordered pair df-op 4406 𝐴, 𝐵 Yes dfopif 4622, opth 5167
oror df-or 879 (𝜑𝜓) Yes orcom 901, anor 1010
otordered triple df-ot 4408 𝐴, 𝐵, 𝐶 Yes euotd 5201, fnotovb 6959
ovoperation value df-ov 6913 (𝐴𝐹𝐵) Yes fnotovb 6959, fnovrn 7074
pplus (see "add"), for all-constant theorems df-add 10270 (3 + 2) = 5 Yes 3p2e5 11516
pfxprefix df-pfx 13757 (𝑊 prefix 𝐿) Yes pfxlen 13769, ccatpfx 13787
pmPrincipia Mathematica No pm2.27 42
pmpartial mapping (operation) df-pm 8130 (𝐴pm 𝐵) Yes elpmi 8146, pmsspw 8162
prpair df-pr 4402 {𝐴, 𝐵} Yes elpr 4422, prcom 4487, prid1g 4515, prnz 4531
prm, primeprime (number) df-prm 15765 Yes 1nprm 15771, dvdsprime 15779
pssproper subset df-pss 3814 𝐴𝐵 Yes pssss 3930, sspsstri 3937
q rational numbers ("quotients") df-q 12079 Yes elq 12080
rright No orcd 904, simprl 787
rabrestricted class abstraction df-rab 3126 {𝑥𝐴𝜑} Yes rabswap 3332, df-oprab 6914
ralrestricted universal quantification df-ral 3122 𝑥𝐴𝜑 Yes ralnex 3201, ralrnmpt2 7040
rclreverse closure No ndmfvrcl 6468, nnarcl 7968
rereal numbers df-r 10269 Yes recn 10349, 0re 10365
relrelation df-rel 5353 Rel 𝐴 Yes brrelex1 5394, relmpt2opab 7528
resrestriction df-res 5358 (𝐴𝐵) Yes opelres 5639, f1ores 6396
reurestricted existential uniqueness df-reu 3124 ∃!𝑥𝐴𝜑 Yes nfreud 3322, reurex 3372
rexrestricted existential quantification df-rex 3123 𝑥𝐴𝜑 Yes rexnal 3203, rexrnmpt2 7041
rmorestricted "at most one" df-rmo 3125 ∃*𝑥𝐴𝜑 Yes nfrmod 3323, nrexrmo 3375
rnrange df-rn 5357 ran 𝐴 Yes elrng 5550, rncnvcnv 5585
rng(unital) ring df-ring 18910 Ring Yes ringidval 18864, isring 18912, ringgrp 18913
rotrotation No 3anrot 1126, 3orrot 1116
seliminates need for syllogism (suffix) No ancoms 452
sb(proper) substitution (of a set) df-sb 2068 [𝑦 / 𝑥]𝜑 Yes spsbe 2071, sbimi 2073
sbc(proper) substitution of a class df-sbc 3663 [𝐴 / 𝑥]𝜑 Yes sbc2or 3671, sbcth 3677
scascalar df-sca 16328 (Scalar‘𝐻) Yes resssca 16397, mgpsca 18857
simpsimple, simplification No simpl 476, simp3r3 1386
snsingleton df-sn 4400 {𝐴} Yes eldifsn 4538
spspecialization No spsbe 2071, spei 2414
sssubset df-ss 3812 𝐴𝐵 Yes difss 3966
structstructure df-struct 16231 Struct Yes brstruct 16238, structfn 16246
subsubtract df-sub 10594 (𝐴𝐵) Yes subval 10599, subaddi 10696
supsupremum df-sup 8623 sup(𝐴, 𝐵, < ) Yes fisupcl 8650, supmo 8633
suppsupport (of a function) df-supp 7565 (𝐹 supp 𝑍) Yes ressuppfi 8576, mptsuppd 7587
swapswap (two parts within a theorem) No rabswap 3332, 2reuswap 3637
sylsyllogism syl 17 No 3syl 18
symsymmetric No df-symdif 4072, cnvsym 5756
symgsymmetric group df-symg 18155 (SymGrp‘𝐴) Yes symghash 18162, pgrpsubgsymg 18185
t times (see "mul"), for all-constant theorems df-mul 10271 (3 · 2) = 6 Yes 3t2e6 11531
ththeorem No nfth 1900, sbcth 3677, weth 9639
tptriple df-tp 4404 {𝐴, 𝐵, 𝐶} Yes eltpi 4450, tpeq1 4497
trtransitive No bitrd 271, biantr 840
trutrue df-tru 1660 Yes bitru 1666, truanfal 1691
ununion df-un 3803 (𝐴𝐵) Yes uneqri 3984, uncom 3986
unitunit (in a ring) df-unit 19003 (Unit‘𝑅) Yes isunit 19018, nzrunit 19635
vdisjoint variable conditions used when a not-free hypothesis (suffix) No spimv 2410
vtxvertex df-vtx 26303 (Vtx‘𝐺) Yes vtxval0 26344, opvtxov 26310
vv2 disjoint variables (in a not-free hypothesis) (suffix) No 19.23vv 2042
wweak (version of a theorem) (suffix) No ax11w 2181, spnfw 2104
wrdword df-word 13582 Word 𝑆 Yes iswrdb 13587, wrdfn 13595, ffz0iswrd 13608
xpcross product (Cartesian product) df-xp 5352 (𝐴 × 𝐵) Yes elxp 5369, opelxpi 5383, xpundi 5408
xreXtended reals df-xr 10402 * Yes ressxr 10407, rexr 10409, 0xr 10410
z integers (from German "Zahlen") df-z 11712 Yes elz 11713, zcn 11716
zn ring of integers mod 𝑁 df-zn 20222 (ℤ/nℤ‘𝑁) Yes znval 20250, zncrng 20259, znhash 20273
zringring of integers df-zring 20186 ring Yes zringbas 20191, zringcrng 20187
0, z slashed zero (empty set) df-nul 4147 Yes n0i 4151, vn0 4156; snnz 4530, prnz 4531

(Contributed by the Metamath team, 27-Dec-2016.) Date of last revision. (Revised by the Metamath team, 22-Sep-2022.) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
conventions-labels.1 𝜑
Ref Expression
conventions-labels 𝜑

Proof of Theorem conventions-labels
StepHypRef Expression
1 conventions-labels.1 1 𝜑
Colors of variables: wff setvar class
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator