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

Definition df-nn 10003
 Description: The natural numbers of analysis start at one (unlike the ordinal natural numbers, i.e. the members of the set , df-om 4848, 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 10020 for the principle of mathematical induction. See dfnn2 10015 for a slight variant. See df-n0 10224 for the set of nonnegative integers starting at zero. See dfn2 10236 for defined in terms of . 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 as well as the successor of every member") see dfnn3 10016. (Contributed by NM, 10-Jan-1997.)
Assertion
Ref Expression
df-nn

Detailed syntax breakdown of Definition df-nn
StepHypRef Expression
1 cn 10002 . 2
2 vx . . . . 5
3 cvv 2958 . . . . 5
42cv 1652 . . . . . 6
5 c1 8993 . . . . . 6
6 caddc 8995 . . . . . 6
74, 5, 6co 6083 . . . . 5
82, 3, 7cmpt 4268 . . . 4
98, 5crdg 6669 . . 3
10 com 4847 . . 3
119, 10cima 4883 . 2
121, 11wceq 1653 1
 Colors of variables: wff set class This definition is referenced by:  nnexALT  10004  peano5nni  10005  1nn  10013  peano2nn  10014
 Copyright terms: Public domain W3C validator