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 7098 | . 2 | |
2 | cnp 7092 | . . . 4 | |
3 | 2, 2 | cxp 4532 | . . 3 |
4 | cer 7097 | . . 3 | |
5 | 3, 4 | cqs 6421 | . 2 |
6 | 1, 5 | wceq 1331 | 1 |
Colors of variables: wff set class |
This definition is referenced by: addsrpr 7546 mulsrpr 7547 ltsrprg 7548 gt0srpr 7549 0nsr 7550 0r 7551 1sr 7552 m1r 7553 addclsr 7554 mulclsr 7555 addcomsrg 7556 addasssrg 7557 mulcomsrg 7558 mulasssrg 7559 distrsrg 7560 lttrsr 7563 ltposr 7564 ltsosr 7565 0idsr 7568 1idsr 7569 00sr 7570 ltasrg 7571 recexgt0sr 7574 mulgt0sr 7579 aptisr 7580 mulextsr1 7582 archsr 7583 srpospr 7584 prsrcl 7585 ltpsrprg 7604 mappsrprg 7605 map2psrprg 7606 suplocsrlemb 7607 addvalex 7645 pitonnlem2 7648 pitore 7651 recnnre 7652 axcnex 7660 |
Copyright terms: Public domain | W3C validator |