![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > xnegeq | Structured version Visualization version GIF version |
Description: Equality of two extended numbers with -𝑒 in front of them. (Contributed by FL, 26-Dec-2011.) (Proof shortened by Mario Carneiro, 20-Aug-2015.) |
Ref | Expression |
---|---|
xnegeq | ⊢ (𝐴 = 𝐵 → -𝑒𝐴 = -𝑒𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqeq1 2802 | . . 3 ⊢ (𝐴 = 𝐵 → (𝐴 = +∞ ↔ 𝐵 = +∞)) | |
2 | eqeq1 2802 | . . . 4 ⊢ (𝐴 = 𝐵 → (𝐴 = -∞ ↔ 𝐵 = -∞)) | |
3 | negeq 10563 | . . . 4 ⊢ (𝐴 = 𝐵 → -𝐴 = -𝐵) | |
4 | 2, 3 | ifbieq2d 4301 | . . 3 ⊢ (𝐴 = 𝐵 → if(𝐴 = -∞, +∞, -𝐴) = if(𝐵 = -∞, +∞, -𝐵)) |
5 | 1, 4 | ifbieq2d 4301 | . 2 ⊢ (𝐴 = 𝐵 → if(𝐴 = +∞, -∞, if(𝐴 = -∞, +∞, -𝐴)) = if(𝐵 = +∞, -∞, if(𝐵 = -∞, +∞, -𝐵))) |
6 | df-xneg 12190 | . 2 ⊢ -𝑒𝐴 = if(𝐴 = +∞, -∞, if(𝐴 = -∞, +∞, -𝐴)) | |
7 | df-xneg 12190 | . 2 ⊢ -𝑒𝐵 = if(𝐵 = +∞, -∞, if(𝐵 = -∞, +∞, -𝐵)) | |
8 | 5, 6, 7 | 3eqtr4g 2857 | 1 ⊢ (𝐴 = 𝐵 → -𝑒𝐴 = -𝑒𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1653 ifcif 4276 +∞cpnf 10359 -∞cmnf 10360 -cneg 10556 -𝑒cxne 12187 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1891 ax-4 1905 ax-5 2006 ax-6 2072 ax-7 2107 ax-9 2166 ax-10 2185 ax-11 2200 ax-12 2213 ax-13 2377 ax-ext 2776 |
This theorem depends on definitions: df-bi 199 df-an 386 df-or 875 df-3an 1110 df-tru 1657 df-ex 1876 df-nf 1880 df-sb 2065 df-clab 2785 df-cleq 2791 df-clel 2794 df-nfc 2929 df-rex 3094 df-rab 3097 df-v 3386 df-dif 3771 df-un 3773 df-in 3775 df-ss 3782 df-nul 4115 df-if 4277 df-sn 4368 df-pr 4370 df-op 4374 df-uni 4628 df-br 4843 df-iota 6063 df-fv 6108 df-ov 6880 df-neg 10558 df-xneg 12190 |
This theorem is referenced by: xnegcl 12290 xnegneg 12291 xneg11 12292 xltnegi 12293 xnegid 12315 xnegdi 12324 xsubge0 12337 xlesubadd 12339 xmulneg1 12345 xmulneg2 12346 xmulmnf1 12352 xmulm1 12357 xrsdsval 20109 xrsdsreclblem 20111 xblss2ps 22531 xblss2 22532 xrhmeo 23070 xaddeq0 30029 xrsmulgzz 30187 xrge0npcan 30203 carsgclctunlem2 30890 xnegeqd 40396 xnegeqi 40399 supminfxr2 40431 supminfxrrnmpt 40433 |
Copyright terms: Public domain | W3C validator |