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 44195
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 13186 . 2 (𝐴 = 𝐵 → -𝑒𝐴 = -𝑒𝐵)
31, 2syl 17 1 (𝜑 → -𝑒𝐴 = -𝑒𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1542  -𝑒cxne 13089
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-v 3477  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-br 5150  df-iota 6496  df-fv 6552  df-ov 7412  df-neg 11447  df-xneg 13092
This theorem is referenced by:  supminfxr  44222  supminfxr2  44227  supminfxrrnmpt  44229  monoord2xrv  44242  liminfvalxr  44547  liminfvalxrmpt  44550  liminfval4  44553  liminfval3  44554  limsupval4  44558  liminfvaluz2  44559  limsupvaluz4  44564  climliminflimsupd  44565  xlimpnfxnegmnf  44578  liminfpnfuz  44580  xlimpnfxnegmnf2  44622  smfliminflem  45594
  Copyright terms: Public domain W3C validator