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

Definition df-nn 10562
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 10566), in contrast to the more elementary ordinal natural numbers , df-om 6701). See nnind 10579 for the principle of mathematical induction. See df-n0 10821 for the set of nonnegative integers . See dfn2 10833 for defined in terms of .

This is a technical definition that helps us avoid the Axiom of Infinity ax-inf2 8079 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 10575 (or its slight variant dfnn2 10574). (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 10561 . 2
2 vx . . . . 5
3 cvv 3109 . . . . 5
42cv 1394 . . . . . 6
5 c1 9514 . . . . . 6
6 caddc 9516 . . . . . 6
74, 5, 6co 6296 . . . . 5
82, 3, 7cmpt 4510 . . . 4
98, 5crdg 7094 . . 3
10 com 6700 . . 3
119, 10cima 5007 . 2
121, 11wceq 1395 1
Colors of variables: wff setvar class
This definition is referenced by:  nnexALT  10563  peano5nni  10564  1nn  10572  peano2nn  10573
  Copyright terms: Public domain W3C validator