Description: Define the set of extended nonnegative integers that includes positive infinity. Analogue of the extension of the real numbers RR* , see df-xr . (Contributed by AV, 10-Dec-2020)
Ref | Expression | ||
---|---|---|---|
Assertion | df-xnn0 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
0 | cxnn0 | |
|
1 | cn0 | |
|
2 | cpnf | |
|
3 | 2 | csn | |
4 | 1 3 | cun | |
5 | 0 4 | wceq | |