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 ⊢ A ∈ ℝ ∧ B ∈ ℝ → A + 𝑒 B = A + B

Proof

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