This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem rexneg

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

Ref Expression
Assertion rexneg ⊢ A ∈ ℝ → − A = − A

Proof

Step Hyp Ref Expression
1 df-xneg ⊢ − A = if A = +∞ −∞ if A = −∞ +∞ − A
2 renepnf ⊢ A ∈ ℝ → A ≠ +∞
3 ifnefalse ⊢ A ≠ +∞ → if A = +∞ −∞ if A = −∞ +∞ − A = if A = −∞ +∞ − A
4 2 3 syl ⊢ A ∈ ℝ → if A = +∞ −∞ if A = −∞ +∞ − A = if A = −∞ +∞ − A
5 renemnf ⊢ A ∈ ℝ → A ≠ −∞
6 ifnefalse ⊢ A ≠ −∞ → if A = −∞ +∞ − A = − A
7 5 6 syl ⊢ A ∈ ℝ → if A = −∞ +∞ − A = − A
8 4 7 eqtrd ⊢ A ∈ ℝ → if A = +∞ −∞ if A = −∞ +∞ − A = − A
9 1 8 eqtrid ⊢ A ∈ ℝ → − A = − A