Users' Mathboxes Mathbox for Glauco Siliprandi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  xnegeqd Structured version   Visualization version   GIF version

Theorem xnegeqd 44954
Description: Equality of two extended numbers with -𝑒 in front of them. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
Hypothesis
Ref Expression
xnegeqd.1 (𝜑𝐴 = 𝐵)
Assertion
Ref Expression
xnegeqd (𝜑 → -𝑒𝐴 = -𝑒𝐵)

Proof of Theorem xnegeqd
StepHypRef Expression
1 xnegeqd.1 . 2 (𝜑𝐴 = 𝐵)
2 xnegeq 13221 . 2 (𝐴 = 𝐵 → -𝑒𝐴 = -𝑒𝐵)
31, 2syl 17 1 (𝜑 → -𝑒𝐴 = -𝑒𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1533  -𝑒cxne 13124
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2696
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-rab 3419  df-v 3463  df-dif 3947  df-un 3949  df-ss 3961  df-nul 4323  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4910  df-br 5150  df-iota 6501  df-fv 6557  df-ov 7422  df-neg 11479  df-xneg 13127
This theorem is referenced by:  supminfxr  44981  supminfxr2  44986  supminfxrrnmpt  44988  monoord2xrv  45001  liminfvalxr  45306  liminfvalxrmpt  45309  liminfval4  45312  liminfval3  45313  limsupval4  45317  liminfvaluz2  45318  limsupvaluz4  45323  climliminflimsupd  45324  xlimpnfxnegmnf  45337  liminfpnfuz  45339  xlimpnfxnegmnf2  45381  smfliminflem  46353
  Copyright terms: Public domain W3C validator