| Metamath Proof Explorer |
< Previous
Next >
Related theorems Unicode version |
| Description: Define class of signed reals. This is a "temporary" set used in the construction of complex numbers df-c 6835, and is intended to be used only by the construction. From Proposition 9-4.2 of [Gleason] p. 126. |
| Ref | Expression |
|---|---|
| df-nr |
|
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | cnr 6588 |
. 2
| |
| 2 | cnp 6580 |
. . . 4
| |
| 3 | 2, 2 | cxp 4149 |
. . 3
|
| 4 | cer 6587 |
. . 3
| |
| 5 | 3, 4 | cqs 5518 |
. 2
|
| 6 | 1, 5 | wceq 1615 |
1
|
| Colors of variables: wff set class |
| This definition is referenced by: srex 6774 addsrpr 6779 mulsrpr 6780 ltsrpr 6781 0nsr 6783 0r 6784 1sr 6785 m1r 6786 addclsr 6787 mulclsr 6788 addcomsr 6791 addasssr 6792 mulcomsr 6793 mulasssr 6794 distrsr 6795 ltsosr 6798 0idsr 6801 1idsr 6802 00sr 6803 ltasr 6804 recexsrlem 6807 mulgt0sr 6809 map2psrpr 6815 |