![]() |
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 6281 |
. 2
![]() ![]() | |
2 | cnp 6275 |
. . . 4
![]() ![]() | |
3 | 2, 2 | cxp 4286 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() |
4 | cer 6280 |
. . 3
![]() ![]() | |
5 | 3, 4 | cqs 6041 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
6 | 1, 5 | wceq 1242 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
This definition is referenced by: addsrpr 6673 mulsrpr 6674 ltsrprg 6675 gt0srpr 6676 0nsr 6677 0r 6678 1sr 6679 m1r 6680 addclsr 6681 mulclsr 6682 addcomsrg 6683 addasssrg 6684 mulcomsrg 6685 mulasssrg 6686 distrsrg 6687 lttrsr 6690 ltposr 6691 ltsosr 6692 0idsr 6695 1idsr 6696 00sr 6697 ltasrg 6698 recexgt0sr 6701 mulgt0sr 6704 aptisr 6705 mulextsr1 6707 archsr 6708 pitonnlem2 6743 axcnex 6745 |
Copyright terms: Public domain | W3C validator |