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 7073 | . 2 class R | |
2 | cnp 7067 | . . . 4 class P | |
3 | 2, 2 | cxp 4507 | . . 3 class (P × P) |
4 | cer 7072 | . . 3 class ~R | |
5 | 3, 4 | cqs 6396 | . 2 class ((P × P) / ~R ) |
6 | 1, 5 | wceq 1316 | 1 wff R = ((P × P) / ~R ) |
Colors of variables: wff set class |
This definition is referenced by: addsrpr 7521 mulsrpr 7522 ltsrprg 7523 gt0srpr 7524 0nsr 7525 0r 7526 1sr 7527 m1r 7528 addclsr 7529 mulclsr 7530 addcomsrg 7531 addasssrg 7532 mulcomsrg 7533 mulasssrg 7534 distrsrg 7535 lttrsr 7538 ltposr 7539 ltsosr 7540 0idsr 7543 1idsr 7544 00sr 7545 ltasrg 7546 recexgt0sr 7549 mulgt0sr 7554 aptisr 7555 mulextsr1 7557 archsr 7558 srpospr 7559 prsrcl 7560 ltpsrprg 7579 mappsrprg 7580 map2psrprg 7581 suplocsrlemb 7582 addvalex 7620 pitonnlem2 7623 pitore 7626 recnnre 7627 axcnex 7635 |
Copyright terms: Public domain | W3C validator |