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 13138

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 13038	. 2 ⊢ -_𝑒𝐴 = if(𝐴 = +∞, -∞, if(𝐴 = -∞, +∞, -𝐴))
2		renepnf 11192	. . . 4 ⊢ (𝐴 ∈ ℝ → 𝐴 ≠ +∞)
3		ifnefalse 4493	. . . 4 ⊢ (𝐴 ≠ +∞ → if(𝐴 = +∞, -∞, if(𝐴 = -∞, +∞, -𝐴)) = if(𝐴 = -∞, +∞, -𝐴))
4	2, 3	syl 17	. . 3 ⊢ (𝐴 ∈ ℝ → if(𝐴 = +∞, -∞, if(𝐴 = -∞, +∞, -𝐴)) = if(𝐴 = -∞, +∞, -𝐴))
5		renemnf 11193	. . . 4 ⊢ (𝐴 ∈ ℝ → 𝐴 ≠ -∞)
6		ifnefalse 4493	. . . 4 ⊢ (𝐴 ≠ -∞ → if(𝐴 = -∞, +∞, -𝐴) = -𝐴)
7	5, 6	syl 17	. . 3 ⊢ (𝐴 ∈ ℝ → if(𝐴 = -∞, +∞, -𝐴) = -𝐴)
8	4, 7	eqtrd 2772	. 2 ⊢ (𝐴 ∈ ℝ → if(𝐴 = +∞, -∞, if(𝐴 = -∞, +∞, -𝐴)) = -𝐴)
9	1, 8	eqtrid 2784	1 ⊢ (𝐴 ∈ ℝ → -_𝑒𝐴 = -𝐴)

Colors of variables: wff setvar class

Syntax hints: → wi 4 = wceq 1542 ∈ wcel 2114 ≠ wne 2933 ifcif 4481 ℝcr 11037 +∞cpnf 11175 -∞cmnf 11176 -cneg 11377 -_𝑒cxne 13035

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 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2185 ax-ext 2709 ax-sep 5243 ax-nul 5253 ax-pow 5312 ax-pr 5379 ax-un 7690 ax-resscn 11095

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2540 df-eu 2570 df-clab 2716 df-cleq 2729 df-clel 2812 df-nfc 2886 df-ne 2934 df-nel 3038 df-ral 3053 df-rex 3063 df-rab 3402 df-v 3444 df-sbc 3743 df-csb 3852 df-dif 3906 df-un 3908 df-in 3910 df-ss 3920 df-nul 4288 df-if 4482 df-pw 4558 df-sn 4583 df-pr 4585 df-op 4589 df-uni 4866 df-br 5101 df-opab 5163 df-mpt 5182 df-id 5527 df-xp 5638 df-rel 5639 df-cnv 5640 df-co 5641 df-dm 5642 df-rn 5643 df-res 5644 df-ima 5645 df-iota 6456 df-fun 6502 df-fn 6503 df-f 6504 df-f1 6505 df-fo 6506 df-f1o 6507 df-fv 6508 df-er 8645 df-en 8896 df-dom 8897 df-sdom 8898 df-pnf 11180 df-mnf 11181 df-xneg 13038

This theorem is referenced by: xneg0 13139 xnegcl 13140 xnegneg 13141 xltnegi 13143 rexsub 13160 xnegid 13165 xnegdi 13175 xpncan 13178 xnpcan 13179 xmulneg1 13196 xmulm1 13208 xadddi 13222 xlt2addrd 32850 xrsmulgzz 33102 rexnegd 45502 xnegrecl 45796

W3C validator