xaddnemnf

Description: Closure of extended real addition in the subset RR* / { -oo } . (Contributed by Mario Carneiro, 20-Aug-2015)

		Ref	Expression
	Assertion	xaddnemnf	$⊢ ((A \in ℝ^{} \land A \neq −∞) \land (B \in ℝ^{} \land B \neq −∞)) \to A +_{𝑒} B \neq −∞$

Proof

Step	Hyp	Ref	Expression
1		xrnemnf	$⊢ (A \in ℝ^{*} \land A \neq −∞) \leftrightarrow (A \in ℝ \lor A = +∞)$
2		xrnemnf	$⊢ (B \in ℝ^{*} \land B \neq −∞) \leftrightarrow (B \in ℝ \lor B = +∞)$
3		rexadd	$⊢ (A \in ℝ \land B \in ℝ) \to A +_{𝑒} B = A + B$
4		readdcl	$⊢ (A \in ℝ \land B \in ℝ) \to A + B \in ℝ$
5	3 4	eqeltrd	$⊢ (A \in ℝ \land B \in ℝ) \to A +_{𝑒} B \in ℝ$
6	5	renemnfd	$⊢ (A \in ℝ \land B \in ℝ) \to A +_{𝑒} B \neq −∞$
7		oveq2	$⊢ B = +∞ \to A +_{𝑒} B = A +_{𝑒} +∞$
8		rexr	$⊢ A \in ℝ \to A \in ℝ^{*}$
9		renemnf	$⊢ A \in ℝ \to A \neq −∞$
10		xaddpnf1	$⊢ (A \in ℝ^{*} \land A \neq −∞) \to A +_{𝑒} +∞ = +∞$
11	8 9 10	syl2anc	$⊢ A \in ℝ \to A +_{𝑒} +∞ = +∞$
12	7 11	sylan9eqr	$⊢ (A \in ℝ \land B = +∞) \to A +_{𝑒} B = +∞$
13		pnfnemnf	$⊢ +∞ \neq −∞$
14	13	a1i	$⊢ (A \in ℝ \land B = +∞) \to +∞ \neq −∞$
15	12 14	eqnetrd	$⊢ (A \in ℝ \land B = +∞) \to A +_{𝑒} B \neq −∞$
16	6 15	jaodan	$⊢ (A \in ℝ \land (B \in ℝ \lor B = +∞)) \to A +_{𝑒} B \neq −∞$
17	2 16	sylan2b	$⊢ (A \in ℝ \land (B \in ℝ^{*} \land B \neq −∞)) \to A +_{𝑒} B \neq −∞$
18		oveq1	$⊢ A = +∞ \to A +_{𝑒} B = +∞ +_{𝑒} B$
19		xaddpnf2	$⊢ (B \in ℝ^{*} \land B \neq −∞) \to +∞ +_{𝑒} B = +∞$
20	18 19	sylan9eq	$⊢ (A = +∞ \land (B \in ℝ^{*} \land B \neq −∞)) \to A +_{𝑒} B = +∞$
21	13	a1i	$⊢ (A = +∞ \land (B \in ℝ^{*} \land B \neq −∞)) \to +∞ \neq −∞$
22	20 21	eqnetrd	$⊢ (A = +∞ \land (B \in ℝ^{*} \land B \neq −∞)) \to A +_{𝑒} B \neq −∞$
23	17 22	jaoian	$⊢ ((A \in ℝ \lor A = +∞) \land (B \in ℝ^{*} \land B \neq −∞)) \to A +_{𝑒} B \neq −∞$
24	1 23	sylanb	$⊢ ((A \in ℝ^{} \land A \neq −∞) \land (B \in ℝ^{} \land B \neq −∞)) \to A +_{𝑒} B \neq −∞$

Metamath Proof Explorer

Theorem xaddnemnf

Proof