Metamath Proof Explorer


Theorem unitsscn

Description: The closed unit interval is a subset of the set of the complex numbers. Useful lemma for manipulating probabilities within the closed unit interval. (Contributed by Thierry Arnoux, 12-Dec-2016)

Ref Expression
Assertion unitsscn ( 0 [,] 1 ) ⊆ ℂ

Proof

Step Hyp Ref Expression
1 unitssre ( 0 [,] 1 ) ⊆ ℝ
2 ax-resscn ℝ ⊆ ℂ
3 1 2 sstri ( 0 [,] 1 ) ⊆ ℂ