Theorem xaddnemnf

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

	Ref	Expression
Assertion	xaddnemnf	⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐴 ≠ -∞ ) ∧ ( 𝐵 ∈ ℝ* ∧ 𝐵 ≠ -∞ ) ) → ( 𝐴 +𝑒 𝐵 ) ≠ -∞ )

Proof

Step	Hyp	Ref	Expression
1		xrnemnf	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐴 ≠ -∞ ) ↔ ( 𝐴 ∈ ℝ ∨ 𝐴 = +∞ ) )
2		xrnemnf	⊢ ( ( 𝐵 ∈ ℝ* ∧ 𝐵 ≠ -∞ ) ↔ ( 𝐵 ∈ ℝ ∨ 𝐵 = +∞ ) )
3		rexadd	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 +𝑒 𝐵 ) = ( 𝐴 + 𝐵 ) )
4		readdcl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 + 𝐵 ) ∈ ℝ )
5	3 4	eqeltrd	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 +𝑒 𝐵 ) ∈ ℝ )
6	5	renemnfd	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 +𝑒 𝐵 ) ≠ -∞ )
7		oveq2	⊢ ( 𝐵 = +∞ → ( 𝐴 +𝑒 𝐵 ) = ( 𝐴 +𝑒 +∞ ) )
8		rexr	⊢ ( 𝐴 ∈ ℝ → 𝐴 ∈ ℝ* )
9		renemnf	⊢ ( 𝐴 ∈ ℝ → 𝐴 ≠ -∞ )
10		xaddpnf1	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐴 ≠ -∞ ) → ( 𝐴 +𝑒 +∞ ) = +∞ )
11	8 9 10	syl2anc	⊢ ( 𝐴 ∈ ℝ → ( 𝐴 +𝑒 +∞ ) = +∞ )
12	7 11	sylan9eqr	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 = +∞ ) → ( 𝐴 +𝑒 𝐵 ) = +∞ )
13		pnfnemnf	⊢ +∞ ≠ -∞
14	13	a1i	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 = +∞ ) → +∞ ≠ -∞ )
15	12 14	eqnetrd	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 = +∞ ) → ( 𝐴 +𝑒 𝐵 ) ≠ -∞ )
16	6 15	jaodan	⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∨ 𝐵 = +∞ ) ) → ( 𝐴 +𝑒 𝐵 ) ≠ -∞ )
17	2 16	sylan2b	⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ* ∧ 𝐵 ≠ -∞ ) ) → ( 𝐴 +𝑒 𝐵 ) ≠ -∞ )
18		oveq1	⊢ ( 𝐴 = +∞ → ( 𝐴 +𝑒 𝐵 ) = ( +∞ +𝑒 𝐵 ) )
19		xaddpnf2	⊢ ( ( 𝐵 ∈ ℝ* ∧ 𝐵 ≠ -∞ ) → ( +∞ +𝑒 𝐵 ) = +∞ )
20	18 19	sylan9eq	⊢ ( ( 𝐴 = +∞ ∧ ( 𝐵 ∈ ℝ* ∧ 𝐵 ≠ -∞ ) ) → ( 𝐴 +𝑒 𝐵 ) = +∞ )
21	13	a1i	⊢ ( ( 𝐴 = +∞ ∧ ( 𝐵 ∈ ℝ* ∧ 𝐵 ≠ -∞ ) ) → +∞ ≠ -∞ )
22	20 21	eqnetrd	⊢ ( ( 𝐴 = +∞ ∧ ( 𝐵 ∈ ℝ* ∧ 𝐵 ≠ -∞ ) ) → ( 𝐴 +𝑒 𝐵 ) ≠ -∞ )
23	17 22	jaoian	⊢ ( ( ( 𝐴 ∈ ℝ ∨ 𝐴 = +∞ ) ∧ ( 𝐵 ∈ ℝ* ∧ 𝐵 ≠ -∞ ) ) → ( 𝐴 +𝑒 𝐵 ) ≠ -∞ )
24	1 23	sylanb	⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐴 ≠ -∞ ) ∧ ( 𝐵 ∈ ℝ* ∧ 𝐵 ≠ -∞ ) ) → ( 𝐴 +𝑒 𝐵 ) ≠ -∞ )