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 ( 𝐴 ∈ ℝ → -𝑒 𝐴 = - 𝐴 )

Proof

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