This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐴 ≠ +∞ ) ∧ ( 𝐵 ∈ ℝ* ∧ 𝐵 ≠ +∞ ) ) → ( 𝐴 +𝑒 𝐵 ) ≠ +∞ )