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	syl6eq	⊢ ( 𝐴 ≠ -∞ → if ( 𝐴 = -∞ , if ( +∞ = +∞ , 0 , -∞ ) , if ( +∞ = +∞ , +∞ , if ( +∞ = -∞ , -∞ , ( 𝐴 + +∞ ) ) ) ) = +∞ )
11	6 10	ifeq12d	⊢ ( 𝐴 ≠ -∞ → if ( 𝐴 = +∞ , if ( +∞ = -∞ , 0 , +∞ ) , if ( 𝐴 = -∞ , if ( +∞ = +∞ , 0 , -∞ ) , if ( +∞ = +∞ , +∞ , if ( +∞ = -∞ , -∞ , ( 𝐴 + +∞ ) ) ) ) ) = if ( 𝐴 = +∞ , +∞ , +∞ ) )
12		ifid	⊢ if ( 𝐴 = +∞ , +∞ , +∞ ) = +∞
13	11 12	syl6eq	⊢ ( 𝐴 ≠ -∞ → if ( 𝐴 = +∞ , if ( +∞ = -∞ , 0 , +∞ ) , if ( 𝐴 = -∞ , if ( +∞ = +∞ , 0 , -∞ ) , if ( +∞ = +∞ , +∞ , if ( +∞ = -∞ , -∞ , ( 𝐴 + +∞ ) ) ) ) ) = +∞ )
14	3 13	sylan9eq	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐴 ≠ -∞ ) → ( 𝐴 +𝑒 +∞ ) = +∞ )