Description: The positive reals are a subset of the complex numbers. (Contributed by SN, 1-Oct-2025)
Ref | Expression | ||
---|---|---|---|
Assertion | rpsscn | |- RR+ C_ CC |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rpssre | |- RR+ C_ RR |
|
2 | ax-resscn | |- RR C_ CC |
|
3 | 1 2 | sstri | |- RR+ C_ CC |