Definition df-n 5883

Description: The natural numbers of analysis start at one (unlike the ordinal natural numbers, i.e. the members of the set om, df-om 3128, 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 5895 for the principle of mathematical induction. See dfnn2 5894 for a slight variant. See df-n0 6057 for the set of nonnegative integers NN0 starting at zero. See dfn2 6069 for NN defined in terms of NN0.

Assertion

Ref	Expression
df-n	|- NN = |^|{x | (1 e. x /\ A.y e. x (y + 1) e. x)}

Distinct variable group:   x,y

Detailed syntax breakdown of Definition df-n

Step	Hyp	Ref	Expression
1		cn 5279	. 2 class NN
2		c1 5218	. . . . . 6 class 1
3		vx	. . . . . . 7 set x
4	3	cv 954	. . . . . 6 class x
5	2, 4	wcel 957	. . . . 5 wff 1 e. x
6		vy	. . . . . . . . 9 set y
7	6	cv 954	. . . . . . . 8 class y
8		caddc 5220	. . . . . . . 8 class +
9	7, 2, 8	co 3958	. . . . . . 7 class (y + 1)
10	9, 4	wcel 957	. . . . . 6 wff (y + 1) e. x
11	10, 6, 4	wral 1643	. . . . 5 wff A.y e. x (y + 1) e. x
12	5, 11	wa 223	. . . 4 wff (1 e. x /\ A.y e. x (y + 1) e. x)
13	12, 3	cab 1462	. . 3 class {x | (1 e. x /\ A.y e. x (y + 1) e. x)}
14	13	cint 2529	. 2 class |^|{x | (1 e. x /\ A.y e. x (y + 1) e. x)}
15	1, 14	wceq 955	1 wff NN = |^|{x | (1 e. x /\ A.y e. x (y + 1) e. x)}

This definition is referenced by:  peano5nn 5884  1nn 5892  peano2nn 5893  dfnn2 5894  dfuz 6160

Copyright terms: Public domain