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 7217 | . 2 class R | |
2 | cnp 7211 | . . . 4 class P | |
3 | 2, 2 | cxp 4584 | . . 3 class (P × P) |
4 | cer 7216 | . . 3 class ~R | |
5 | 3, 4 | cqs 6479 | . 2 class ((P × P) / ~R ) |
6 | 1, 5 | wceq 1335 | 1 wff R = ((P × P) / ~R ) |
Colors of variables: wff set class |
This definition is referenced by: addsrpr 7665 mulsrpr 7666 ltsrprg 7667 gt0srpr 7668 0nsr 7669 0r 7670 1sr 7671 m1r 7672 addclsr 7673 mulclsr 7674 addcomsrg 7675 addasssrg 7676 mulcomsrg 7677 mulasssrg 7678 distrsrg 7679 lttrsr 7682 ltposr 7683 ltsosr 7684 0idsr 7687 1idsr 7688 00sr 7689 ltasrg 7690 recexgt0sr 7693 mulgt0sr 7698 aptisr 7699 mulextsr1 7701 archsr 7702 srpospr 7703 prsrcl 7704 ltpsrprg 7723 mappsrprg 7724 map2psrprg 7725 suplocsrlemb 7726 addvalex 7764 pitonnlem2 7767 pitore 7770 recnnre 7771 axcnex 7779 |
Copyright terms: Public domain | W3C validator |