Description: Elementhood in the set of nonnegative extended reals. (Contributed by Mario Carneiro, 28-Jun-2014)
Ref | Expression | ||
---|---|---|---|
Assertion | elxrge0 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-3an | |
|
2 | 0xr | |
|
3 | pnfxr | |
|
4 | elicc1 | |
|
5 | 2 3 4 | mp2an | |
6 | pnfge | |
|
7 | 6 | adantr | |
8 | 7 | pm4.71i | |
9 | 1 5 8 | 3bitr4i | |