![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > df-nr | Unicode version |
Description: Define class of signed reals. This is a "temporary" set used in the construction of complex numbers, and is intended to be used only by the construction. From Proposition 9-4.2 of [Gleason] p. 126. (Contributed by NM, 25-Jul-1995.) |
Ref | Expression |
---|---|
df-nr |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cnr 7047 |
. 2
![]() ![]() | |
2 | cnp 7041 |
. . . 4
![]() ![]() | |
3 | 2, 2 | cxp 4495 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() |
4 | cer 7046 |
. . 3
![]() ![]() | |
5 | 3, 4 | cqs 6380 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
6 | 1, 5 | wceq 1312 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
This definition is referenced by: addsrpr 7482 mulsrpr 7483 ltsrprg 7484 gt0srpr 7485 0nsr 7486 0r 7487 1sr 7488 m1r 7489 addclsr 7490 mulclsr 7491 addcomsrg 7492 addasssrg 7493 mulcomsrg 7494 mulasssrg 7495 distrsrg 7496 lttrsr 7499 ltposr 7500 ltsosr 7501 0idsr 7504 1idsr 7505 00sr 7506 ltasrg 7507 recexgt0sr 7510 mulgt0sr 7514 aptisr 7515 mulextsr1 7517 archsr 7518 srpospr 7519 prsrcl 7520 addvalex 7573 pitonnlem2 7576 pitore 7579 recnnre 7580 axcnex 7588 |
Copyright terms: Public domain | W3C validator |