This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem rrpsscn

Description: The positive reals are a subset of the complex numbers. (Contributed by Glauco Siliprandi, 29-Jun-2017)

Ref Expression
Assertion rrpsscn 
|- RR+ C_ CC

Proof

Step Hyp Ref Expression
1 rpcn 
 |-  ( x e. RR+ -> x e. CC )
2 1 ssriv 
 |-  RR+ C_ CC