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 |