Theorem xaddnepnf

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

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

Proof

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