Description: The closed unit interval is a subset of the set of the extended nonnegative reals. Useful lemma for manipulating probabilities within the closed unit interval. (Contributed by Thierry Arnoux, 12-Dec-2016)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | unitssxrge0 | |- ( 0 [,] 1 ) C_ ( 0 [,] +oo ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | 0e0iccpnf | |- 0 e. ( 0 [,] +oo ) |
|
| 2 | 1xr | |- 1 e. RR* |
|
| 3 | 0le1 | |- 0 <_ 1 |
|
| 4 | pnfge | |- ( 1 e. RR* -> 1 <_ +oo ) |
|
| 5 | 2 4 | ax-mp | |- 1 <_ +oo |
| 6 | 0xr | |- 0 e. RR* |
|
| 7 | pnfxr | |- +oo e. RR* |
|
| 8 | elicc1 | |- ( ( 0 e. RR* /\ +oo e. RR* ) -> ( 1 e. ( 0 [,] +oo ) <-> ( 1 e. RR* /\ 0 <_ 1 /\ 1 <_ +oo ) ) ) |
|
| 9 | 6 7 8 | mp2an | |- ( 1 e. ( 0 [,] +oo ) <-> ( 1 e. RR* /\ 0 <_ 1 /\ 1 <_ +oo ) ) |
| 10 | 2 3 5 9 | mpbir3an | |- 1 e. ( 0 [,] +oo ) |
| 11 | iccss2 | |- ( ( 0 e. ( 0 [,] +oo ) /\ 1 e. ( 0 [,] +oo ) ) -> ( 0 [,] 1 ) C_ ( 0 [,] +oo ) ) |
|
| 12 | 1 10 11 | mp2an | |- ( 0 [,] 1 ) C_ ( 0 [,] +oo ) |