Metamath Proof Explorer

Theorem rexadd

Description: The extended real addition operation when both arguments are real. (Contributed by Mario Carneiro, 20-Aug-2015)

Ref Expression
Assertion rexadd ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 +𝑒 𝐵 ) = ( 𝐴 + 𝐵 ) )

Proof

Step Hyp Ref Expression
1 rexr ⊢ ( 𝐴 ∈ ℝ → 𝐴 ∈ ℝ* )
2 rexr ⊢ ( 𝐵 ∈ ℝ → 𝐵 ∈ ℝ* )
3 xaddval ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 𝐴 +𝑒 𝐵 ) = if ( 𝐴 = +∞ , if ( 𝐵 = -∞ , 0 , +∞ ) , if ( 𝐴 = -∞ , if ( 𝐵 = +∞ , 0 , -∞ ) , if ( 𝐵 = +∞ , +∞ , if ( 𝐵 = -∞ , -∞ , ( 𝐴 + 𝐵 ) ) ) ) ) )
4 1 2 3 syl2an ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 +𝑒 𝐵 ) = if ( 𝐴 = +∞ , if ( 𝐵 = -∞ , 0 , +∞ ) , if ( 𝐴 = -∞ , if ( 𝐵 = +∞ , 0 , -∞ ) , if ( 𝐵 = +∞ , +∞ , if ( 𝐵 = -∞ , -∞ , ( 𝐴 + 𝐵 ) ) ) ) ) )
5 renepnf ⊢ ( 𝐴 ∈ ℝ → 𝐴 ≠ +∞ )
6 ifnefalse ⊢ ( 𝐴 ≠ +∞ → if ( 𝐴 = +∞ , if ( 𝐵 = -∞ , 0 , +∞ ) , if ( 𝐴 = -∞ , if ( 𝐵 = +∞ , 0 , -∞ ) , if ( 𝐵 = +∞ , +∞ , if ( 𝐵 = -∞ , -∞ , ( 𝐴 + 𝐵 ) ) ) ) ) = if ( 𝐴 = -∞ , if ( 𝐵 = +∞ , 0 , -∞ ) , if ( 𝐵 = +∞ , +∞ , if ( 𝐵 = -∞ , -∞ , ( 𝐴 + 𝐵 ) ) ) ) )
7 5 6 syl ⊢ ( 𝐴 ∈ ℝ → if ( 𝐴 = +∞ , if ( 𝐵 = -∞ , 0 , +∞ ) , if ( 𝐴 = -∞ , if ( 𝐵 = +∞ , 0 , -∞ ) , if ( 𝐵 = +∞ , +∞ , if ( 𝐵 = -∞ , -∞ , ( 𝐴 + 𝐵 ) ) ) ) ) = if ( 𝐴 = -∞ , if ( 𝐵 = +∞ , 0 , -∞ ) , if ( 𝐵 = +∞ , +∞ , if ( 𝐵 = -∞ , -∞ , ( 𝐴 + 𝐵 ) ) ) ) )
8 renemnf ⊢ ( 𝐴 ∈ ℝ → 𝐴 ≠ -∞ )
9 ifnefalse ⊢ ( 𝐴 ≠ -∞ → if ( 𝐴 = -∞ , if ( 𝐵 = +∞ , 0 , -∞ ) , if ( 𝐵 = +∞ , +∞ , if ( 𝐵 = -∞ , -∞ , ( 𝐴 + 𝐵 ) ) ) ) = if ( 𝐵 = +∞ , +∞ , if ( 𝐵 = -∞ , -∞ , ( 𝐴 + 𝐵 ) ) ) )
10 8 9 syl ⊢ ( 𝐴 ∈ ℝ → if ( 𝐴 = -∞ , if ( 𝐵 = +∞ , 0 , -∞ ) , if ( 𝐵 = +∞ , +∞ , if ( 𝐵 = -∞ , -∞ , ( 𝐴 + 𝐵 ) ) ) ) = if ( 𝐵 = +∞ , +∞ , if ( 𝐵 = -∞ , -∞ , ( 𝐴 + 𝐵 ) ) ) )
11 7 10 eqtrd ⊢ ( 𝐴 ∈ ℝ → if ( 𝐴 = +∞ , if ( 𝐵 = -∞ , 0 , +∞ ) , if ( 𝐴 = -∞ , if ( 𝐵 = +∞ , 0 , -∞ ) , if ( 𝐵 = +∞ , +∞ , if ( 𝐵 = -∞ , -∞ , ( 𝐴 + 𝐵 ) ) ) ) ) = if ( 𝐵 = +∞ , +∞ , if ( 𝐵 = -∞ , -∞ , ( 𝐴 + 𝐵 ) ) ) )
12 renepnf ⊢ ( 𝐵 ∈ ℝ → 𝐵 ≠ +∞ )
13 ifnefalse ⊢ ( 𝐵 ≠ +∞ → if ( 𝐵 = +∞ , +∞ , if ( 𝐵 = -∞ , -∞ , ( 𝐴 + 𝐵 ) ) ) = if ( 𝐵 = -∞ , -∞ , ( 𝐴 + 𝐵 ) ) )
14 12 13 syl ⊢ ( 𝐵 ∈ ℝ → if ( 𝐵 = +∞ , +∞ , if ( 𝐵 = -∞ , -∞ , ( 𝐴 + 𝐵 ) ) ) = if ( 𝐵 = -∞ , -∞ , ( 𝐴 + 𝐵 ) ) )
15 renemnf ⊢ ( 𝐵 ∈ ℝ → 𝐵 ≠ -∞ )
16 ifnefalse ⊢ ( 𝐵 ≠ -∞ → if ( 𝐵 = -∞ , -∞ , ( 𝐴 + 𝐵 ) ) = ( 𝐴 + 𝐵 ) )
17 15 16 syl ⊢ ( 𝐵 ∈ ℝ → if ( 𝐵 = -∞ , -∞ , ( 𝐴 + 𝐵 ) ) = ( 𝐴 + 𝐵 ) )
18 14 17 eqtrd ⊢ ( 𝐵 ∈ ℝ → if ( 𝐵 = +∞ , +∞ , if ( 𝐵 = -∞ , -∞ , ( 𝐴 + 𝐵 ) ) ) = ( 𝐴 + 𝐵 ) )
19 11 18 sylan9eq ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → if ( 𝐴 = +∞ , if ( 𝐵 = -∞ , 0 , +∞ ) , if ( 𝐴 = -∞ , if ( 𝐵 = +∞ , 0 , -∞ ) , if ( 𝐵 = +∞ , +∞ , if ( 𝐵 = -∞ , -∞ , ( 𝐴 + 𝐵 ) ) ) ) ) = ( 𝐴 + 𝐵 ) )
20 4 19 eqtrd ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 +𝑒 𝐵 ) = ( 𝐴 + 𝐵 ) )