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

Metamath Proof Explorer

Theorem xnegeq

Description: Equality of two extended numbers with -e in front of them. (Contributed by FL, 26-Dec-2011) (Proof shortened by Mario Carneiro, 20-Aug-2015)

Ref Expression
Assertion xnegeq 
|- ( A = B -> -e A = -e B )

Proof

Step Hyp Ref Expression
1 eqeq1 
 |-  ( A = B -> ( A = +oo <-> B = +oo ) )
2 eqeq1 
 |-  ( A = B -> ( A = -oo <-> B = -oo ) )
3 negeq 
 |-  ( A = B -> -u A = -u B )
4 2 3 ifbieq2d 
 |-  ( A = B -> if ( A = -oo , +oo , -u A ) = if ( B = -oo , +oo , -u B ) )
5 1 4 ifbieq2d 
 |-  ( A = B -> if ( A = +oo , -oo , if ( A = -oo , +oo , -u A ) ) = if ( B = +oo , -oo , if ( B = -oo , +oo , -u B ) ) )
6 df-xneg 
 |-  -e A = if ( A = +oo , -oo , if ( A = -oo , +oo , -u A ) )
7 df-xneg 
 |-  -e B = if ( B = +oo , -oo , if ( B = -oo , +oo , -u B ) )
8 5 6 7 3eqtr4g 
 |-  ( A = B -> -e A = -e B )