Description: The closed unit interval is a subset of the set of the real numbers. Useful lemma for manipulating probabilities within the closed unit interval. (Contributed by Thierry Arnoux, 21-Dec-2016)
Ref | Expression | ||
---|---|---|---|
Assertion | elunitrn | ⊢ ( 𝐴 ∈ ( 0 [,] 1 ) → 𝐴 ∈ ℝ ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elicc01 | ⊢ ( 𝐴 ∈ ( 0 [,] 1 ) ↔ ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ∧ 𝐴 ≤ 1 ) ) | |
2 | 1 | simp1bi | ⊢ ( 𝐴 ∈ ( 0 [,] 1 ) → 𝐴 ∈ ℝ ) |