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 ) ⊆ ( 0 [,] +∞ ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | 0e0iccpnf | ⊢ 0 ∈ ( 0 [,] +∞ ) | |
| 2 | 1xr | ⊢ 1 ∈ ℝ* | |
| 3 | 0le1 | ⊢ 0 ≤ 1 | |
| 4 | pnfge | ⊢ ( 1 ∈ ℝ* → 1 ≤ +∞ ) | |
| 5 | 2 4 | ax-mp | ⊢ 1 ≤ +∞ |
| 6 | 0xr | ⊢ 0 ∈ ℝ* | |
| 7 | pnfxr | ⊢ +∞ ∈ ℝ* | |
| 8 | elicc1 | ⊢ ( ( 0 ∈ ℝ* ∧ +∞ ∈ ℝ* ) → ( 1 ∈ ( 0 [,] +∞ ) ↔ ( 1 ∈ ℝ* ∧ 0 ≤ 1 ∧ 1 ≤ +∞ ) ) ) | |
| 9 | 6 7 8 | mp2an | ⊢ ( 1 ∈ ( 0 [,] +∞ ) ↔ ( 1 ∈ ℝ* ∧ 0 ≤ 1 ∧ 1 ≤ +∞ ) ) |
| 10 | 2 3 5 9 | mpbir3an | ⊢ 1 ∈ ( 0 [,] +∞ ) |
| 11 | iccss2 | ⊢ ( ( 0 ∈ ( 0 [,] +∞ ) ∧ 1 ∈ ( 0 [,] +∞ ) ) → ( 0 [,] 1 ) ⊆ ( 0 [,] +∞ ) ) | |
| 12 | 1 10 11 | mp2an | ⊢ ( 0 [,] 1 ) ⊆ ( 0 [,] +∞ ) |