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 7229 | . 2 | |
2 | cnp 7223 | . . . 4 | |
3 | 2, 2 | cxp 4596 | . . 3 |
4 | cer 7228 | . . 3 | |
5 | 3, 4 | cqs 6491 | . 2 |
6 | 1, 5 | wceq 1342 | 1 |
Colors of variables: wff set class |
This definition is referenced by: addsrpr 7677 mulsrpr 7678 ltsrprg 7679 gt0srpr 7680 0nsr 7681 0r 7682 1sr 7683 m1r 7684 addclsr 7685 mulclsr 7686 addcomsrg 7687 addasssrg 7688 mulcomsrg 7689 mulasssrg 7690 distrsrg 7691 lttrsr 7694 ltposr 7695 ltsosr 7696 0idsr 7699 1idsr 7700 00sr 7701 ltasrg 7702 recexgt0sr 7705 mulgt0sr 7710 aptisr 7711 mulextsr1 7713 archsr 7714 srpospr 7715 prsrcl 7716 ltpsrprg 7735 mappsrprg 7736 map2psrprg 7737 suplocsrlemb 7738 addvalex 7776 pitonnlem2 7779 pitore 7782 recnnre 7783 axcnex 7791 |
Copyright terms: Public domain | W3C validator |