MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  xnegeq Structured version   Unicode version

Theorem xnegeq 11291
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.)
Assertion
Ref Expression
xnegeq  |-  ( A  =  B  ->  -e
A  =  -e
B )

Proof of Theorem xnegeq
StepHypRef Expression
1 eqeq1 2458 . . 3  |-  ( A  =  B  ->  ( A  = +oo  <->  B  = +oo ) )
2 eqeq1 2458 . . . 4  |-  ( A  =  B  ->  ( A  = -oo  <->  B  = -oo ) )
3 negeq 9716 . . . 4  |-  ( A  =  B  ->  -u A  =  -u B )
42, 3ifbieq2d 3925 . . 3  |-  ( A  =  B  ->  if ( A  = -oo , +oo ,  -u A
)  =  if ( B  = -oo , +oo ,  -u B ) )
51, 4ifbieq2d 3925 . 2  |-  ( 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 11203 . 2  |-  -e
A  =  if ( A  = +oo , -oo ,  if ( A  = -oo , +oo ,  -u A ) )
7 df-xneg 11203 . 2  |-  -e
B  =  if ( B  = +oo , -oo ,  if ( B  = -oo , +oo ,  -u B ) )
85, 6, 73eqtr4g 2520 1  |-  ( A  =  B  ->  -e
A  =  -e
B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1370   ifcif 3902   +oocpnf 9529   -oocmnf 9530   -ucneg 9710    -ecxne 11200
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-rex 2805  df-rab 2808  df-v 3080  df-dif 3442  df-un 3444  df-in 3446  df-ss 3453  df-nul 3749  df-if 3903  df-sn 3989  df-pr 3991  df-op 3995  df-uni 4203  df-br 4404  df-iota 5492  df-fv 5537  df-ov 6206  df-neg 9712  df-xneg 11203
This theorem is referenced by:  xnegcl  11297  xnegneg  11298  xneg11  11299  xltnegi  11300  xnegid  11320  xnegdi  11325  xsubge0  11338  xlesubadd  11340  xmulneg1  11346  xmulneg2  11347  xmulmnf1  11353  xmulm1  11358  xrsdsval  17985  xrsdsreclblem  17987  xblss2ps  20111  xblss2  20112  xrhmeo  20653  xaddeq0  26217  xrsmulgzz  26304  xrge0npcan  26322
  Copyright terms: Public domain W3C validator