Description: 0 is a member of ( 0 , +oo ) . (Contributed by David A. Wheeler, 8-Dec-2018)
Ref | Expression | ||
---|---|---|---|
Assertion | 0e0iccpnf | |- 0 e. ( 0 [,] +oo ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 0xr | |- 0 e. RR* |
|
2 | 0le0 | |- 0 <_ 0 |
|
3 | elxrge0 | |- ( 0 e. ( 0 [,] +oo ) <-> ( 0 e. RR* /\ 0 <_ 0 ) ) |
|
4 | 1 2 3 | mpbir2an | |- 0 e. ( 0 [,] +oo ) |