Metamath Proof Explorer

Theorem xaddpnf2

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

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

Proof

Step Hyp Ref Expression
1 pnfxr ⊢ +∞ ∈ ℝ*
2 xaddval ⊢ ( ( +∞ ∈ ℝ* ∧ 𝐴 ∈ ℝ* ) → ( +∞ +𝑒 𝐴 ) = if ( +∞ = +∞ , if ( 𝐴 = -∞ , 0 , +∞ ) , if ( +∞ = -∞ , if ( 𝐴 = +∞ , 0 , -∞ ) , if ( 𝐴 = +∞ , +∞ , if ( 𝐴 = -∞ , -∞ , ( +∞ + 𝐴 ) ) ) ) ) )
3 1 2 mpan ⊢ ( 𝐴 ∈ ℝ* → ( +∞ +𝑒 𝐴 ) = if ( +∞ = +∞ , if ( 𝐴 = -∞ , 0 , +∞ ) , if ( +∞ = -∞ , if ( 𝐴 = +∞ , 0 , -∞ ) , if ( 𝐴 = +∞ , +∞ , if ( 𝐴 = -∞ , -∞ , ( +∞ + 𝐴 ) ) ) ) ) )
4 eqid ⊢ +∞ = +∞
5 4 iftruei ⊢ if ( +∞ = +∞ , if ( 𝐴 = -∞ , 0 , +∞ ) , if ( +∞ = -∞ , if ( 𝐴 = +∞ , 0 , -∞ ) , if ( 𝐴 = +∞ , +∞ , if ( 𝐴 = -∞ , -∞ , ( +∞ + 𝐴 ) ) ) ) ) = if ( 𝐴 = -∞ , 0 , +∞ )
6 ifnefalse ⊢ ( 𝐴 ≠ -∞ → if ( 𝐴 = -∞ , 0 , +∞ ) = +∞ )
7 5 6 syl5eq ⊢ ( 𝐴 ≠ -∞ → if ( +∞ = +∞ , if ( 𝐴 = -∞ , 0 , +∞ ) , if ( +∞ = -∞ , if ( 𝐴 = +∞ , 0 , -∞ ) , if ( 𝐴 = +∞ , +∞ , if ( 𝐴 = -∞ , -∞ , ( +∞ + 𝐴 ) ) ) ) ) = +∞ )
8 3 7 sylan9eq ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐴 ≠ -∞ ) → ( +∞ +𝑒 𝐴 ) = +∞ )