Metamath Proof Explorer 
< Previous
Next >
Nearby theorems 

Mirrors > Home > MPE Home > Th. List > cnpi  Unicode version 
Description: The set of positive
integers, which is the set of natural numbers
with 0 removed.
Note: This is the start of the Dedekindcut construction of real and complex numbers. The last lemma of the construction is mulcnsrec 8952. The actual set of Dedekind cuts is defined by dfnp 8791. 
Ref  Expression 

cnpi 
Colors of variables: wff set class 
Copyright terms: Public domain  W3C validator 