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