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

Metamath Proof Explorer

Theorem xaddpnf1

Description: Addition of positive infinity on the right. (Contributed by Mario Carneiro, 20-Aug-2015)

Ref Expression
Assertion xaddpnf1 ( ( 𝐴 ∈ ℝ* ∧ 𝐴 ≠ -∞ ) → ( 𝐴 +𝑒 +∞ ) = +∞ )

Proof

Step Hyp Ref Expression
1 pnfxr ⊢ +∞ ∈ ℝ*
2 xaddval ⊢ ( ( 𝐴 ∈ ℝ* ∧ +∞ ∈ ℝ* ) → ( 𝐴 +𝑒 +∞ ) = if ( 𝐴 = +∞ , if ( +∞ = -∞ , 0 , +∞ ) , if ( 𝐴 = -∞ , if ( +∞ = +∞ , 0 , -∞ ) , if ( +∞ = +∞ , +∞ , if ( +∞ = -∞ , -∞ , ( 𝐴 + +∞ ) ) ) ) ) )
3 1 2 mpan2 ⊢ ( 𝐴 ∈ ℝ* → ( 𝐴 +𝑒 +∞ ) = if ( 𝐴 = +∞ , if ( +∞ = -∞ , 0 , +∞ ) , if ( 𝐴 = -∞ , if ( +∞ = +∞ , 0 , -∞ ) , if ( +∞ = +∞ , +∞ , if ( +∞ = -∞ , -∞ , ( 𝐴 + +∞ ) ) ) ) ) )
4 pnfnemnf ⊢ +∞ ≠ -∞
5 ifnefalse ⊢ ( +∞ ≠ -∞ → if ( +∞ = -∞ , 0 , +∞ ) = +∞ )
6 4 5 mp1i ⊢ ( 𝐴 ≠ -∞ → if ( +∞ = -∞ , 0 , +∞ ) = +∞ )
7 ifnefalse ⊢ ( 𝐴 ≠ -∞ → if ( 𝐴 = -∞ , if ( +∞ = +∞ , 0 , -∞ ) , if ( +∞ = +∞ , +∞ , if ( +∞ = -∞ , -∞ , ( 𝐴 + +∞ ) ) ) ) = if ( +∞ = +∞ , +∞ , if ( +∞ = -∞ , -∞ , ( 𝐴 + +∞ ) ) ) )
8 eqid ⊢ +∞ = +∞
9 8 iftruei ⊢ if ( +∞ = +∞ , +∞ , if ( +∞ = -∞ , -∞ , ( 𝐴 + +∞ ) ) ) = +∞
10 7 9 eqtrdi ⊢ ( 𝐴 ≠ -∞ → if ( 𝐴 = -∞ , if ( +∞ = +∞ , 0 , -∞ ) , if ( +∞ = +∞ , +∞ , if ( +∞ = -∞ , -∞ , ( 𝐴 + +∞ ) ) ) ) = +∞ )
11 6 10 ifeq12d ⊢ ( 𝐴 ≠ -∞ → if ( 𝐴 = +∞ , if ( +∞ = -∞ , 0 , +∞ ) , if ( 𝐴 = -∞ , if ( +∞ = +∞ , 0 , -∞ ) , if ( +∞ = +∞ , +∞ , if ( +∞ = -∞ , -∞ , ( 𝐴 + +∞ ) ) ) ) ) = if ( 𝐴 = +∞ , +∞ , +∞ ) )
12 ifid ⊢ if ( 𝐴 = +∞ , +∞ , +∞ ) = +∞
13 11 12 eqtrdi ⊢ ( 𝐴 ≠ -∞ → if ( 𝐴 = +∞ , if ( +∞ = -∞ , 0 , +∞ ) , if ( 𝐴 = -∞ , if ( +∞ = +∞ , 0 , -∞ ) , if ( +∞ = +∞ , +∞ , if ( +∞ = -∞ , -∞ , ( 𝐴 + +∞ ) ) ) ) ) = +∞ )
14 3 13 sylan9eq ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐴 ≠ -∞ ) → ( 𝐴 +𝑒 +∞ ) = +∞ )