rexneg - Metamath Proof Explorer

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

Theorem rexneg 13105

Description: Minus a real number. Remark [BourbakiTop1] p. IV.15. (Contributed by FL, 26-Dec-2011.) (Proof shortened by Mario Carneiro, 20-Aug-2015.)

**Assertion**
Ref	Expression
rexneg	⊢ (𝐴 ∈ ℝ → -_𝑒𝐴 = -𝐴)

**Proof of Theorem rexneg**
Step	Hyp	Ref	Expression
1		df-xneg 13006	. 2 ⊢ -_𝑒𝐴 = if(𝐴 = +∞, -∞, if(𝐴 = -∞, +∞, -𝐴))
2		renepnf 11155	. . . 4 ⊢ (𝐴 ∈ ℝ → 𝐴 ≠ +∞)
3		ifnefalse 4482	. . . 4 ⊢ (𝐴 ≠ +∞ → if(𝐴 = +∞, -∞, if(𝐴 = -∞, +∞, -𝐴)) = if(𝐴 = -∞, +∞, -𝐴))
4	2, 3	syl 17	. . 3 ⊢ (𝐴 ∈ ℝ → if(𝐴 = +∞, -∞, if(𝐴 = -∞, +∞, -𝐴)) = if(𝐴 = -∞, +∞, -𝐴))
5		renemnf 11156	. . . 4 ⊢ (𝐴 ∈ ℝ → 𝐴 ≠ -∞)
6		ifnefalse 4482	. . . 4 ⊢ (𝐴 ≠ -∞ → if(𝐴 = -∞, +∞, -𝐴) = -𝐴)
7	5, 6	syl 17	. . 3 ⊢ (𝐴 ∈ ℝ → if(𝐴 = -∞, +∞, -𝐴) = -𝐴)
8	4, 7	eqtrd 2766	. 2 ⊢ (𝐴 ∈ ℝ → if(𝐴 = +∞, -∞, if(𝐴 = -∞, +∞, -𝐴)) = -𝐴)
9	1, 8	eqtrid 2778	1 ⊢ (𝐴 ∈ ℝ → -_𝑒𝐴 = -𝐴)

Colors of variables: wff setvar class

Syntax hints: → wi 4 = wceq 1541 ∈ wcel 2111 ≠ wne 2928 ifcif 4470 ℝcr 11000 +∞cpnf 11138 -∞cmnf 11139 -cneg 11340 -_𝑒cxne 13003

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2113 ax-9 2121 ax-10 2144 ax-11 2160 ax-12 2180 ax-ext 2703 ax-sep 5229 ax-nul 5239 ax-pow 5298 ax-pr 5365 ax-un 7663 ax-resscn 11058

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-nf 1785 df-sb 2068 df-mo 2535 df-eu 2564 df-clab 2710 df-cleq 2723 df-clel 2806 df-nfc 2881 df-ne 2929 df-nel 3033 df-ral 3048 df-rex 3057 df-rab 3396 df-v 3438 df-sbc 3737 df-csb 3846 df-dif 3900 df-un 3902 df-in 3904 df-ss 3914 df-nul 4279 df-if 4471 df-pw 4547 df-sn 4572 df-pr 4574 df-op 4578 df-uni 4855 df-br 5087 df-opab 5149 df-mpt 5168 df-id 5506 df-xp 5617 df-rel 5618 df-cnv 5619 df-co 5620 df-dm 5621 df-rn 5622 df-res 5623 df-ima 5624 df-iota 6432 df-fun 6478 df-fn 6479 df-f 6480 df-f1 6481 df-fo 6482 df-f1o 6483 df-fv 6484 df-er 8617 df-en 8865 df-dom 8866 df-sdom 8867 df-pnf 11143 df-mnf 11144 df-xneg 13006

This theorem is referenced by: xneg0 13106 xnegcl 13107 xnegneg 13108 xltnegi 13110 rexsub 13127 xnegid 13132 xnegdi 13142 xpncan 13145 xnpcan 13146 xmulneg1 13163 xmulm1 13175 xadddi 13189 xlt2addrd 32734 xrsmulgzz 32982 rexnegd 45180 xnegrecl 45476

W3C validator