Theorem xpncan

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

	Ref	Expression
Assertion	xpncan	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ ) → ( ( 𝐴 +𝑒 𝐵 ) +𝑒 -𝑒 𝐵 ) = 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		rexneg	⊢ ( 𝐵 ∈ ℝ → -𝑒 𝐵 = - 𝐵 )
2	1	adantl	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ ) → -𝑒 𝐵 = - 𝐵 )
3	2	oveq2d	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ ) → ( ( 𝐴 +𝑒 𝐵 ) +𝑒 -𝑒 𝐵 ) = ( ( 𝐴 +𝑒 𝐵 ) +𝑒 - 𝐵 ) )
4		renegcl	⊢ ( 𝐵 ∈ ℝ → - 𝐵 ∈ ℝ )
5	4	ad2antlr	⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 = -∞ ) → - 𝐵 ∈ ℝ )
6		rexr	⊢ ( - 𝐵 ∈ ℝ → - 𝐵 ∈ ℝ* )
7		renepnf	⊢ ( - 𝐵 ∈ ℝ → - 𝐵 ≠ +∞ )
8		xaddmnf2	⊢ ( ( - 𝐵 ∈ ℝ* ∧ - 𝐵 ≠ +∞ ) → ( -∞ +𝑒 - 𝐵 ) = -∞ )
9	6 7 8	syl2anc	⊢ ( - 𝐵 ∈ ℝ → ( -∞ +𝑒 - 𝐵 ) = -∞ )
10	5 9	syl	⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 = -∞ ) → ( -∞ +𝑒 - 𝐵 ) = -∞ )
11		oveq1	⊢ ( 𝐴 = -∞ → ( 𝐴 +𝑒 𝐵 ) = ( -∞ +𝑒 𝐵 ) )
12		rexr	⊢ ( 𝐵 ∈ ℝ → 𝐵 ∈ ℝ* )
13		renepnf	⊢ ( 𝐵 ∈ ℝ → 𝐵 ≠ +∞ )
14		xaddmnf2	⊢ ( ( 𝐵 ∈ ℝ* ∧ 𝐵 ≠ +∞ ) → ( -∞ +𝑒 𝐵 ) = -∞ )
15	12 13 14	syl2anc	⊢ ( 𝐵 ∈ ℝ → ( -∞ +𝑒 𝐵 ) = -∞ )
16	15	adantl	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ ) → ( -∞ +𝑒 𝐵 ) = -∞ )
17	11 16	sylan9eqr	⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 = -∞ ) → ( 𝐴 +𝑒 𝐵 ) = -∞ )
18	17	oveq1d	⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 = -∞ ) → ( ( 𝐴 +𝑒 𝐵 ) +𝑒 - 𝐵 ) = ( -∞ +𝑒 - 𝐵 ) )
19		simpr	⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 = -∞ ) → 𝐴 = -∞ )
20	10 18 19	3eqtr4d	⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 = -∞ ) → ( ( 𝐴 +𝑒 𝐵 ) +𝑒 - 𝐵 ) = 𝐴 )
21		simpll	⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 ≠ -∞ ) → 𝐴 ∈ ℝ* )
22		simpr	⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 ≠ -∞ ) → 𝐴 ≠ -∞ )
23	12	ad2antlr	⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 ≠ -∞ ) → 𝐵 ∈ ℝ* )
24		renemnf	⊢ ( 𝐵 ∈ ℝ → 𝐵 ≠ -∞ )
25	24	ad2antlr	⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 ≠ -∞ ) → 𝐵 ≠ -∞ )
26	4	ad2antlr	⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 ≠ -∞ ) → - 𝐵 ∈ ℝ )
27	26 6	syl	⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 ≠ -∞ ) → - 𝐵 ∈ ℝ* )
28		renemnf	⊢ ( - 𝐵 ∈ ℝ → - 𝐵 ≠ -∞ )
29	26 28	syl	⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 ≠ -∞ ) → - 𝐵 ≠ -∞ )
30		xaddass	⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐴 ≠ -∞ ) ∧ ( 𝐵 ∈ ℝ* ∧ 𝐵 ≠ -∞ ) ∧ ( - 𝐵 ∈ ℝ* ∧ - 𝐵 ≠ -∞ ) ) → ( ( 𝐴 +𝑒 𝐵 ) +𝑒 - 𝐵 ) = ( 𝐴 +𝑒 ( 𝐵 +𝑒 - 𝐵 ) ) )
31	21 22 23 25 27 29 30	syl222anc	⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 ≠ -∞ ) → ( ( 𝐴 +𝑒 𝐵 ) +𝑒 - 𝐵 ) = ( 𝐴 +𝑒 ( 𝐵 +𝑒 - 𝐵 ) ) )
32		simplr	⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 ≠ -∞ ) → 𝐵 ∈ ℝ )
33	32 26	rexaddd	⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 ≠ -∞ ) → ( 𝐵 +𝑒 - 𝐵 ) = ( 𝐵 + - 𝐵 ) )
34	32	recnd	⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 ≠ -∞ ) → 𝐵 ∈ ℂ )
35	34	negidd	⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 ≠ -∞ ) → ( 𝐵 + - 𝐵 ) = 0 )
36	33 35	eqtrd	⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 ≠ -∞ ) → ( 𝐵 +𝑒 - 𝐵 ) = 0 )
37	36	oveq2d	⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 ≠ -∞ ) → ( 𝐴 +𝑒 ( 𝐵 +𝑒 - 𝐵 ) ) = ( 𝐴 +𝑒 0 ) )
38		xaddrid	⊢ ( 𝐴 ∈ ℝ* → ( 𝐴 +𝑒 0 ) = 𝐴 )
39	38	ad2antrr	⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 ≠ -∞ ) → ( 𝐴 +𝑒 0 ) = 𝐴 )
40	37 39	eqtrd	⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 ≠ -∞ ) → ( 𝐴 +𝑒 ( 𝐵 +𝑒 - 𝐵 ) ) = 𝐴 )
41	31 40	eqtrd	⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 ≠ -∞ ) → ( ( 𝐴 +𝑒 𝐵 ) +𝑒 - 𝐵 ) = 𝐴 )
42	20 41	pm2.61dane	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ ) → ( ( 𝐴 +𝑒 𝐵 ) +𝑒 - 𝐵 ) = 𝐴 )
43	3 42	eqtrd	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ ) → ( ( 𝐴 +𝑒 𝐵 ) +𝑒 -𝑒 𝐵 ) = 𝐴 )