Metamath Proof Explorer

Theorem rexneg

Description: Minus a real number. Remark BourbakiTop1 p. IV.15. (Contributed by FL, 26-Dec-2011) (Proof shortened by Mario Carneiro, 20-Aug-2015)

Ref Expression
Assertion rexneg 
|- ( A e. RR -> -e A = -u A )

Proof

Step Hyp Ref Expression
1 df-xneg 
 |-  -e A = if ( A = +oo , -oo , if ( A = -oo , +oo , -u A ) )
2 renepnf 
 |-  ( A e. RR -> A =/= +oo )
3 ifnefalse 
 |-  ( A =/= +oo -> if ( A = +oo , -oo , if ( A = -oo , +oo , -u A ) ) = if ( A = -oo , +oo , -u A ) )
4 2 3 syl 
 |-  ( A e. RR -> if ( A = +oo , -oo , if ( A = -oo , +oo , -u A ) ) = if ( A = -oo , +oo , -u A ) )
5 renemnf 
 |-  ( A e. RR -> A =/= -oo )
6 ifnefalse 
 |-  ( A =/= -oo -> if ( A = -oo , +oo , -u A ) = -u A )
7 5 6 syl 
 |-  ( A e. RR -> if ( A = -oo , +oo , -u A ) = -u A )
8 4 7 eqtrd 
 |-  ( A e. RR -> if ( A = +oo , -oo , if ( A = -oo , +oo , -u A ) ) = -u A )
9 1 8 syl5eq 
 |-  ( A e. RR -> -e A = -u A )