![]() |
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 10867 | . . . 4 ⊢ (𝐴 = 𝐵 → -𝐴 = -𝐵) | |
4 | 2, 3 | ifbieq2d 4450 | . . 3 ⊢ (𝐴 = 𝐵 → if(𝐴 = -∞, +∞, -𝐴) = if(𝐵 = -∞, +∞, -𝐵)) |
5 | 1, 4 | ifbieq2d 4450 | . 2 ⊢ (𝐴 = 𝐵 → if(𝐴 = +∞, -∞, if(𝐴 = -∞, +∞, -𝐴)) = if(𝐵 = +∞, -∞, if(𝐵 = -∞, +∞, -𝐵))) |
6 | df-xneg 12495 | . 2 ⊢ -𝑒𝐴 = if(𝐴 = +∞, -∞, if(𝐴 = -∞, +∞, -𝐴)) | |
7 | df-xneg 12495 | . 2 ⊢ -𝑒𝐵 = if(𝐵 = +∞, -∞, if(𝐵 = -∞, +∞, -𝐵)) | |
8 | 5, 6, 7 | 3eqtr4g 2858 | 1 ⊢ (𝐴 = 𝐵 → -𝑒𝐴 = -𝑒𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1538 ifcif 4425 +∞cpnf 10661 -∞cmnf 10662 -cneg 10860 -𝑒cxne 12492 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2113 ax-9 2121 ax-10 2142 ax-12 2175 ax-ext 2770 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 845 df-3an 1086 df-ex 1782 df-nf 1786 df-sb 2070 df-clab 2777 df-cleq 2791 df-clel 2870 df-rab 3115 df-v 3443 df-un 3886 df-in 3888 df-ss 3898 df-if 4426 df-sn 4526 df-pr 4528 df-op 4532 df-uni 4801 df-br 5031 df-iota 6283 df-fv 6332 df-ov 7138 df-neg 10862 df-xneg 12495 |
This theorem is referenced by: xnegcl 12594 xnegneg 12595 xneg11 12596 xltnegi 12597 xnegid 12619 xnegdi 12629 xsubge0 12642 xlesubadd 12644 xmulneg1 12650 xmulneg2 12651 xmulmnf1 12657 xmulm1 12662 xrsdsval 20135 xrsdsreclblem 20137 xblss2ps 23008 xblss2 23009 xrhmeo 23551 xaddeq0 30503 xrsmulgzz 30712 xrge0npcan 30728 carsgclctunlem2 31687 xnegeqd 42074 xnegeqi 42077 supminfxr2 42108 supminfxrrnmpt 42110 liminflbuz2 42457 |
Copyright terms: Public domain | W3C validator |