xaddnepnf

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

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

Proof

Step	Hyp	Ref	Expression
1		xrnepnf	$⊢ (A \in ℝ^{*} \land A \neq +∞) \leftrightarrow (A \in ℝ \lor A = −∞)$
2		xrnepnf	$⊢ (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	renepnfd	$⊢ (A \in ℝ \land B \in ℝ) \to A +_{𝑒} B \neq +∞$
7		oveq2	$⊢ B = −∞ \to A +_{𝑒} B = A +_{𝑒} −∞$
8		rexr	$⊢ A \in ℝ \to A \in ℝ^{*}$
9		renepnf	$⊢ A \in ℝ \to A \neq +∞$
10		xaddmnf1	$⊢ (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		mnfnepnf	$⊢ −∞ \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		xaddmnf2	$⊢ (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 xaddnepnf

Proof