Description: An extended nonnegative integer is an extended nonnegative real. (Contributed by AV, 10-Dec-2020)
Ref | Expression | ||
---|---|---|---|
Assertion | xnn0xrge0 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elxnn0 | |
|
2 | nn0re | |
|
3 | 2 | rexrd | |
4 | nn0ge0 | |
|
5 | elxrge0 | |
|
6 | 3 4 5 | sylanbrc | |
7 | 0xr | |
|
8 | pnfxr | |
|
9 | 0lepnf | |
|
10 | ubicc2 | |
|
11 | 7 8 9 10 | mp3an | |
12 | eleq1 | |
|
13 | 11 12 | mpbiri | |
14 | 6 13 | jaoi | |
15 | 1 14 | sylbi | |