Description: Closure law for negative of reals. The weak deduction theorem dedth is used to convert hypothesis of the inference (deduction) form of this theorem, renegcli , to an antecedent. (Contributed by NM, 20-Jan-1997) (Proof modification is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | renegcl | |- ( A e. RR -> -u A e. RR ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | negeq | |- ( A = if ( A e. RR , A , 1 ) -> -u A = -u if ( A e. RR , A , 1 ) ) |
|
| 2 | 1 | eleq1d | |- ( A = if ( A e. RR , A , 1 ) -> ( -u A e. RR <-> -u if ( A e. RR , A , 1 ) e. RR ) ) |
| 3 | 1re | |- 1 e. RR |
|
| 4 | 3 | elimel | |- if ( A e. RR , A , 1 ) e. RR |
| 5 | 4 | renegcli | |- -u if ( A e. RR , A , 1 ) e. RR |
| 6 | 2 5 | dedth | |- ( A e. RR -> -u A e. RR ) |