![]() |
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 7298 |
. 2
![]() ![]() | |
2 | cnp 7292 |
. . . 4
![]() ![]() | |
3 | 2, 2 | cxp 4626 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() |
4 | cer 7297 |
. . 3
![]() ![]() | |
5 | 3, 4 | cqs 6536 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
6 | 1, 5 | wceq 1353 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
This definition is referenced by: addsrpr 7746 mulsrpr 7747 ltsrprg 7748 gt0srpr 7749 0nsr 7750 0r 7751 1sr 7752 m1r 7753 addclsr 7754 mulclsr 7755 addcomsrg 7756 addasssrg 7757 mulcomsrg 7758 mulasssrg 7759 distrsrg 7760 lttrsr 7763 ltposr 7764 ltsosr 7765 0idsr 7768 1idsr 7769 00sr 7770 ltasrg 7771 recexgt0sr 7774 mulgt0sr 7779 aptisr 7780 mulextsr1 7782 archsr 7783 srpospr 7784 prsrcl 7785 ltpsrprg 7804 mappsrprg 7805 map2psrprg 7806 suplocsrlemb 7807 addvalex 7845 pitonnlem2 7848 pitore 7851 recnnre 7852 axcnex 7860 |
Copyright terms: Public domain | W3C validator |