![]() |
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 7129 | . 2 class R | |
2 | cnp 7123 | . . . 4 class P | |
3 | 2, 2 | cxp 4545 | . . 3 class (P × P) |
4 | cer 7128 | . . 3 class ~R | |
5 | 3, 4 | cqs 6436 | . 2 class ((P × P) / ~R ) |
6 | 1, 5 | wceq 1332 | 1 wff R = ((P × P) / ~R ) |
Colors of variables: wff set class |
This definition is referenced by: addsrpr 7577 mulsrpr 7578 ltsrprg 7579 gt0srpr 7580 0nsr 7581 0r 7582 1sr 7583 m1r 7584 addclsr 7585 mulclsr 7586 addcomsrg 7587 addasssrg 7588 mulcomsrg 7589 mulasssrg 7590 distrsrg 7591 lttrsr 7594 ltposr 7595 ltsosr 7596 0idsr 7599 1idsr 7600 00sr 7601 ltasrg 7602 recexgt0sr 7605 mulgt0sr 7610 aptisr 7611 mulextsr1 7613 archsr 7614 srpospr 7615 prsrcl 7616 ltpsrprg 7635 mappsrprg 7636 map2psrprg 7637 suplocsrlemb 7638 addvalex 7676 pitonnlem2 7679 pitore 7682 recnnre 7683 axcnex 7691 |
Copyright terms: Public domain | W3C validator |