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

Definition df-nn 10032
Description: The natural numbers of analysis start at one (unlike the ordinal natural numbers, i.e. the members of the set  om, df-om 4875, which start at zero). This is the convention used by most analysis books, and it is often convenient in proofs because we don't have to worry about division by zero. See nnind 10049 for the principle of mathematical induction. See dfnn2 10044 for a slight variant. See df-n0 10253 for the set of nonnegative integers  NN0 starting at zero. See dfn2 10265 for  NN defined in terms of  NN0.

This is a technical definition that helps us avoid the Axiom of Infinity 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 10045. (Contributed by NM, 10-Jan-1997.)

Assertion
Ref Expression
df-nn  |-  NN  =  ( rec ( ( x  e.  _V  |->  ( x  +  1 ) ) ,  1 ) " om )

Detailed syntax breakdown of Definition df-nn
StepHypRef Expression
1 cn 10031 . 2  class  NN
2 vx . . . . 5  set  x
3 cvv 2962 . . . . 5  class  _V
42cv 1652 . . . . . 6  class  x
5 c1 9022 . . . . . 6  class  1
6 caddc 9024 . . . . . 6  class  +
74, 5, 6co 6110 . . . . 5  class  ( x  +  1 )
82, 3, 7cmpt 4291 . . . 4  class  ( x  e.  _V  |->  ( x  +  1 ) )
98, 5crdg 6696 . . 3  class  rec (
( x  e.  _V  |->  ( x  +  1
) ) ,  1 )
10 com 4874 . . 3  class  om
119, 10cima 4910 . 2  class  ( rec ( ( x  e. 
_V  |->  ( x  + 
1 ) ) ,  1 ) " om )
121, 11wceq 1653 1  wff  NN  =  ( rec ( ( x  e.  _V  |->  ( x  +  1 ) ) ,  1 ) " om )
Colors of variables: wff set class
This definition is referenced by:  nnexALT  10033  peano5nni  10034  1nn  10042  peano2nn  10043
  Copyright terms: Public domain W3C validator