xpncan

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

		Ref	Expression
	Assertion	xpncan	$⊢ (A \in ℝ^{*} \land B \in ℝ) \to (A +_{𝑒} B) +_{𝑒} (- B) = A$

Proof

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

Metamath Proof Explorer

Theorem xpncan

Proof