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 eqtrid
 |-  ( A e. RR -> -e A = -u A )