![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > df-nr | GIF 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 | ⊢ R = ((P × P) / ~R ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cnr 7295 | . 2 class R | |
2 | cnp 7289 | . . . 4 class P | |
3 | 2, 2 | cxp 4624 | . . 3 class (P × P) |
4 | cer 7294 | . . 3 class ~R | |
5 | 3, 4 | cqs 6533 | . 2 class ((P × P) / ~R ) |
6 | 1, 5 | wceq 1353 | 1 wff R = ((P × P) / ~R ) |
Colors of variables: wff set class |
This definition is referenced by: addsrpr 7743 mulsrpr 7744 ltsrprg 7745 gt0srpr 7746 0nsr 7747 0r 7748 1sr 7749 m1r 7750 addclsr 7751 mulclsr 7752 addcomsrg 7753 addasssrg 7754 mulcomsrg 7755 mulasssrg 7756 distrsrg 7757 lttrsr 7760 ltposr 7761 ltsosr 7762 0idsr 7765 1idsr 7766 00sr 7767 ltasrg 7768 recexgt0sr 7771 mulgt0sr 7776 aptisr 7777 mulextsr1 7779 archsr 7780 srpospr 7781 prsrcl 7782 ltpsrprg 7801 mappsrprg 7802 map2psrprg 7803 suplocsrlemb 7804 addvalex 7842 pitonnlem2 7845 pitore 7848 recnnre 7849 axcnex 7857 |
Copyright terms: Public domain | W3C validator |