Home Metamath Proof Explorer < Previous   Next > Related theorems Unicode version

Definition df-n 7441
 Description: The natural numbers of analysis start at one (unlike the ordinal natural numbers, i.e. the members of the set , df-om 4086, 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 7453 for the principle of mathematical induction. See dfnn2 7452 for a slight variant. See df-n0 7649 for the set of nonnegative integers starting at zero. See dfn2 7661 for defined in terms of .
Assertion
Ref Expression
df-n
Distinct variable group:   ,

Detailed syntax breakdown of Definition df-n
StepHypRef Expression
1 cn 6992 . 2
2 c1 6753 . . . . . 6
3 vx . . . . . . 7
43cv 1585 . . . . . 6
52, 4wcel 1588 . . . . 5
6 vy . . . . . . . . 9
76cv 1585 . . . . . . . 8
8 caddc 6755 . . . . . . . 8
97, 2, 8co 4981 . . . . . . 7
109, 4wcel 1588 . . . . . 6
1110, 6, 4wral 2355 . . . . 5
125, 11wa 337 . . . 4
1312, 3cab 2128 . . 3
1413cint 3400 . 2
151, 14wceq 1586 1
 Colors of variables: wff set class This definition is referenced by:  peano5nni 7442  1nn 7450  peano2nn 7451  dfnn2 7452  dfuzi 7757