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 ) C_ CC

Proof

Step Hyp Ref Expression
1 unitssre
 |-  ( 0 [,] 1 ) C_ RR
2 ax-resscn
 |-  RR C_ CC
3 1 2 sstri
 |-  ( 0 [,] 1 ) C_ CC