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

Metamath Proof Explorer

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