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 NN is a subset of complex numbers ( nnsscn ), in contrast to the more elementary ordinal natural numbers _om , df-om ). See nnind for the principle of mathematical induction. See df-n0 for the set of nonnegative integers NN0 . See dfn2 for NN defined in terms of NN0 .
This is a technical definition that helps us avoid the Axiom of Infinity ax-inf2 in certain proofs. For a more conventional and intuitive definition ("the smallest set of reals containing 1 as well as the successor of every member") see dfnn3 (or its slight variant dfnn2 ). (Contributed by NM, 10-Jan-1997) (Revised by Mario Carneiro, 3-May-2014)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | df-nn | |- NN = ( rec ( ( x e. _V |-> ( x + 1 ) ) , 1 ) " _om ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 0 | cn | |- NN |
|
| 1 | vx | |- x |
|
| 2 | cvv | |- _V |
|
| 3 | 1 | cv | |- x |
| 4 | caddc | |- + |
|
| 5 | c1 | |- 1 |
|
| 6 | 3 5 4 | co | |- ( x + 1 ) |
| 7 | 1 2 6 | cmpt | |- ( x e. _V |-> ( x + 1 ) ) |
| 8 | 7 5 | crdg | |- rec ( ( x e. _V |-> ( x + 1 ) ) , 1 ) |
| 9 | com | |- _om |
|
| 10 | 8 9 | cima | |- ( rec ( ( x e. _V |-> ( x + 1 ) ) , 1 ) " _om ) |
| 11 | 0 10 | wceq | |- NN = ( rec ( ( x e. _V |-> ( x + 1 ) ) , 1 ) " _om ) |