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 7105 | . 2 class R | |
2 | cnp 7099 | . . . 4 class P | |
3 | 2, 2 | cxp 4537 | . . 3 class (P × P) |
4 | cer 7104 | . . 3 class ~R | |
5 | 3, 4 | cqs 6428 | . 2 class ((P × P) / ~R ) |
6 | 1, 5 | wceq 1331 | 1 wff R = ((P × P) / ~R ) |
Colors of variables: wff set class |
This definition is referenced by: addsrpr 7553 mulsrpr 7554 ltsrprg 7555 gt0srpr 7556 0nsr 7557 0r 7558 1sr 7559 m1r 7560 addclsr 7561 mulclsr 7562 addcomsrg 7563 addasssrg 7564 mulcomsrg 7565 mulasssrg 7566 distrsrg 7567 lttrsr 7570 ltposr 7571 ltsosr 7572 0idsr 7575 1idsr 7576 00sr 7577 ltasrg 7578 recexgt0sr 7581 mulgt0sr 7586 aptisr 7587 mulextsr1 7589 archsr 7590 srpospr 7591 prsrcl 7592 ltpsrprg 7611 mappsrprg 7612 map2psrprg 7613 suplocsrlemb 7614 addvalex 7652 pitonnlem2 7655 pitore 7658 recnnre 7659 axcnex 7667 |
Copyright terms: Public domain | W3C validator |