df-xneg - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > df-xneg		Structured version Visualization version GIF version

Definition df-xneg 13119

Description: Define the negative of an extended real number. (Contributed by FL, 26-Dec-2011.)

**Assertion**
Ref	Expression
df-xneg	⊢ -_𝑒𝐴 = if(𝐴 = +∞, -∞, if(𝐴 = -∞, +∞, -𝐴))

**Detailed syntax breakdown of Definition df-xneg**
Step	Hyp	Ref	Expression
1		cA	. . 3 class 𝐴
2	1	cxne 13116	. 2 class -_𝑒𝐴
3		cpnf 11270	. . . 4 class +∞
4	1, 3	wceq 1534	. . 3 wff 𝐴 = +∞
5		cmnf 11271	. . 3 class -∞
6	1, 5	wceq 1534	. . . 4 wff 𝐴 = -∞
7	1	cneg 11470	. . . 4 class -𝐴
8	6, 3, 7	cif 4525	. . 3 class if(𝐴 = -∞, +∞, -𝐴)
9	4, 5, 8	cif 4525	. 2 class if(𝐴 = +∞, -∞, if(𝐴 = -∞, +∞, -𝐴))
10	2, 9	wceq 1534	1 wff -_𝑒𝐴 = if(𝐴 = +∞, -∞, if(𝐴 = -∞, +∞, -𝐴))

Colors of variables: wff setvar class

This definition is referenced by: xnegeq 13213 xnegex 13214 xnegpnf 13215 xnegmnf 13216 rexneg 13217 nfxnegd 44814

	
		OSZAR »