Description: Closure law for subtraction of reals. (Contributed by NM, 17-Jan-1997) (Revised by Mario Carneiro, 27-May-2016)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | renegcl.1 | |- A e. RR |
|
| resubcl.2 | |- B e. RR |
||
| Assertion | resubcli | |- ( A - B ) e. RR |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | renegcl.1 | |- A e. RR |
|
| 2 | resubcl.2 | |- B e. RR |
|
| 3 | 1 | recni | |- A e. CC |
| 4 | 2 | recni | |- B e. CC |
| 5 | negsub | |- ( ( A e. CC /\ B e. CC ) -> ( A + -u B ) = ( A - B ) ) |
|
| 6 | 3 4 5 | mp2an | |- ( A + -u B ) = ( A - B ) |
| 7 | 2 | renegcli | |- -u B e. RR |
| 8 | 1 7 | readdcli | |- ( A + -u B ) e. RR |
| 9 | 6 8 | eqeltrri | |- ( A - B ) e. RR |