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=ifA=+∞ifB=−∞0+∞ifA=−∞ifB=+∞0−∞ifB=+∞+∞ifB=−∞−∞A+B
4 1 2 3 syl2an ⊢A∈ℝ∧B∈ℝ→A+𝑒B=ifA=+∞ifB=−∞0+∞ifA=−∞ifB=+∞0−∞ifB=+∞+∞ifB=−∞−∞A+B
5 renepnf ⊢A∈ℝ→A≠+∞
6 ifnefalse ⊢A≠+∞→ifA=+∞ifB=−∞0+∞ifA=−∞ifB=+∞0−∞ifB=+∞+∞ifB=−∞−∞A+B=ifA=−∞ifB=+∞0−∞ifB=+∞+∞ifB=−∞−∞A+B
7 5 6 syl ⊢A∈ℝ→ifA=+∞ifB=−∞0+∞ifA=−∞ifB=+∞0−∞ifB=+∞+∞ifB=−∞−∞A+B=ifA=−∞ifB=+∞0−∞ifB=+∞+∞ifB=−∞−∞A+B
8 renemnf ⊢A∈ℝ→A≠−∞
9 ifnefalse ⊢A≠−∞→ifA=−∞ifB=+∞0−∞ifB=+∞+∞ifB=−∞−∞A+B=ifB=+∞+∞ifB=−∞−∞A+B
10 8 9 syl ⊢A∈ℝ→ifA=−∞ifB=+∞0−∞ifB=+∞+∞ifB=−∞−∞A+B=ifB=+∞+∞ifB=−∞−∞A+B
11 7 10 eqtrd ⊢A∈ℝ→ifA=+∞ifB=−∞0+∞ifA=−∞ifB=+∞0−∞ifB=+∞+∞ifB=−∞−∞A+B=ifB=+∞+∞ifB=−∞−∞A+B
12 renepnf ⊢B∈ℝ→B≠+∞
13 ifnefalse ⊢B≠+∞→ifB=+∞+∞ifB=−∞−∞A+B=ifB=−∞−∞A+B
14 12 13 syl ⊢B∈ℝ→ifB=+∞+∞ifB=−∞−∞A+B=ifB=−∞−∞A+B
15 renemnf ⊢B∈ℝ→B≠−∞
16 ifnefalse ⊢B≠−∞→ifB=−∞−∞A+B=A+B
17 15 16 syl ⊢B∈ℝ→ifB=−∞−∞A+B=A+B
18 14 17 eqtrd ⊢B∈ℝ→ifB=+∞+∞ifB=−∞−∞A+B=A+B
19 11 18 sylan9eq ⊢A∈ℝ∧B∈ℝ→ifA=+∞ifB=−∞0+∞ifA=−∞ifB=+∞0−∞ifB=+∞+∞ifB=−∞−∞A+B=A+B
20 4 19 eqtrd ⊢A∈ℝ∧B∈ℝ→A+𝑒B=A+B