This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem renegcli

Description: Closure law for negative of reals. (Note: this inference proof style and the deduction theorem usage in renegcl is deprecated, but is retained for its demonstration value.) (Contributed by NM, 17-Jan-1997) (Proof shortened by Andrew Salmon, 22-Oct-2011)

Ref Expression
Hypothesis renegcl.1 
|- A e. RR
Assertion renegcli 
|- -u A e. RR

Proof

Step Hyp Ref Expression
1 renegcl.1 
 |-  A e. RR
2 ax-rnegex 
 |-  ( A e. RR -> E. x e. RR ( A + x ) = 0 )
3 recn 
 |-  ( x e. RR -> x e. CC )
4 df-neg 
 |-  -u A = ( 0 - A )
5 4 eqeq1i 
 |-  ( -u A = x <-> ( 0 - A ) = x )
6 0cn 
 |-  0 e. CC
7 1 recni 
 |-  A e. CC
8 subadd 
 |-  ( ( 0 e. CC /\ A e. CC /\ x e. CC ) -> ( ( 0 - A ) = x <-> ( A + x ) = 0 ) )
9 6 7 8 mp3an12 
 |-  ( x e. CC -> ( ( 0 - A ) = x <-> ( A + x ) = 0 ) )
10 5 9 bitrid 
 |-  ( x e. CC -> ( -u A = x <-> ( A + x ) = 0 ) )
11 3 10 syl 
 |-  ( x e. RR -> ( -u A = x <-> ( A + x ) = 0 ) )
12 eleq1a 
 |-  ( x e. RR -> ( -u A = x -> -u A e. RR ) )
13 11 12 sylbird 
 |-  ( x e. RR -> ( ( A + x ) = 0 -> -u A e. RR ) )
14 13 rexlimiv 
 |-  ( E. x e. RR ( A + x ) = 0 -> -u A e. RR )
15 1 2 14 mp2b 
 |-  -u A e. RR