| 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 5212, 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 4965 |
. 2
| |
| 2 | cnp 4957 |
. . . 4
| |
| 3 | 2, 2 | cxp 3158 |
. . 3
|
| 4 | cer 4964 |
. . 3
| |
| 5 | 3, 4 | cqs 4244 |
. 2
|
| 6 | 1, 5 | wceq 953 |
1
|
| Colors of variables: wff set class |
| This definition is referenced by: srex 5151 addsrpr 5156 mulsrpr 5157 ltsrpr 5158 0nsr 5160 0r 5161 1r 5162 m1r 5163 addclsr 5164 mulclsr 5165 addcomsr 5168 addasssr 5169 mulcomsr 5170 mulasssr 5171 distrsr 5172 ltsosr 5175 0idsr 5178 1idsr 5179 00sr 5180 ltasr 5181 recexsrlem 5184 mulgt0sr 5186 map2psrpr 5192 |