Theorem xnegneg

Description: Extended real version of negneg . (Contributed by Mario Carneiro, 20-Aug-2015)

	Ref	Expression
Assertion	xnegneg	⊢ ( 𝐴 ∈ ℝ* → -e -e 𝐴 = 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		elxr	⊢ ( 𝐴 ∈ ℝ* ↔ ( 𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞ ) )
2		rexneg	⊢ ( 𝐴 ∈ ℝ → -e 𝐴 = - 𝐴 )
3		xnegeq	⊢ ( -e 𝐴 = - 𝐴 → -e -e 𝐴 = -e - 𝐴 )
4	2 3	syl	⊢ ( 𝐴 ∈ ℝ → -e -e 𝐴 = -e - 𝐴 )
5		renegcl	⊢ ( 𝐴 ∈ ℝ → - 𝐴 ∈ ℝ )
6		rexneg	⊢ ( - 𝐴 ∈ ℝ → -e - 𝐴 = - - 𝐴 )
7	5 6	syl	⊢ ( 𝐴 ∈ ℝ → -e - 𝐴 = - - 𝐴 )
8		recn	⊢ ( 𝐴 ∈ ℝ → 𝐴 ∈ ℂ )
9	8	negnegd	⊢ ( 𝐴 ∈ ℝ → - - 𝐴 = 𝐴 )
10	4 7 9	3eqtrd	⊢ ( 𝐴 ∈ ℝ → -e -e 𝐴 = 𝐴 )
11		xnegmnf	⊢ -e -∞ = +∞
12		xnegeq	⊢ ( 𝐴 = +∞ → -e 𝐴 = -e +∞ )
13		xnegpnf	⊢ -e +∞ = -∞
14	12 13	eqtrdi	⊢ ( 𝐴 = +∞ → -e 𝐴 = -∞ )
15		xnegeq	⊢ ( -e 𝐴 = -∞ → -e -e 𝐴 = -e -∞ )
16	14 15	syl	⊢ ( 𝐴 = +∞ → -e -e 𝐴 = -e -∞ )
17		id	⊢ ( 𝐴 = +∞ → 𝐴 = +∞ )
18	11 16 17	3eqtr4a	⊢ ( 𝐴 = +∞ → -e -e 𝐴 = 𝐴 )
19		xnegeq	⊢ ( 𝐴 = -∞ → -e 𝐴 = -e -∞ )
20	19 11	eqtrdi	⊢ ( 𝐴 = -∞ → -e 𝐴 = +∞ )
21		xnegeq	⊢ ( -e 𝐴 = +∞ → -e -e 𝐴 = -e +∞ )
22	20 21	syl	⊢ ( 𝐴 = -∞ → -e -e 𝐴 = -e +∞ )
23		id	⊢ ( 𝐴 = -∞ → 𝐴 = -∞ )
24	13 22 23	3eqtr4a	⊢ ( 𝐴 = -∞ → -e -e 𝐴 = 𝐴 )
25	10 18 24	3jaoi	⊢ ( ( 𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞ ) → -e -e 𝐴 = 𝐴 )
26	1 25	sylbi	⊢ ( 𝐴 ∈ ℝ* → -e -e 𝐴 = 𝐴 )