MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-nn Unicode version

Definition df-nn 10269
Description: Define the set of positive integers. Some authors, especially in analysis books, call these the natural numbers, whereas other authors choose to include 0 in their definition of natural numbers. Note that is a subset of complex numbers (nnsscn 10273), in contrast to the more elementary ordinal natural numbers , df-om 6447). See nnind 10286 for the principle of mathematical induction. See dfnn2 10281 for a slight variant. See df-n0 10526 for the set of nonnegative integers . See dfn2 10538 for defined in terms of .

This is a technical definition that helps us avoid the Axiom of Infinity ax-inf2 7794 in certain proofs. For a more conventional and intuitive definition ("the smallest set of reals containing as well as the successor of every member") see dfnn3 10282. (Contributed by NM, 10-Jan-1997.) (Revised by Mario Carneiro, 3-May-2014.)

Assertion
Ref Expression
df-nn

Detailed syntax breakdown of Definition df-nn
StepHypRef Expression
1 cn 10268 . 2
2 vx . . . . 5
3 cvv 2951 . . . . 5
42cv 1686 . . . . . 6
5 c1 9229 . . . . . 6
6 caddc 9231 . . . . . 6
74, 5, 6co 6061 . . . . 5
82, 3, 7cmpt 4325 . . . 4
98, 5crdg 6824 . . 3
10 com 6446 . . 3
119, 10cima 4814 . 2
121, 11wceq 1687 1
Colors of variables: wff setvar class
This definition is referenced by:  nnexALT  10270  peano5nni  10271  1nn  10279  peano2nn  10280
  Copyright terms: Public domain W3C validator