Metamath Proof Explorer

Definition df-xadd

Description: Define addition over extended real numbers. (Contributed by Mario Carneiro, 20-Aug-2015)

Ref Expression
Assertion df-xadd ⊢+𝑒=x∈ℝ*,y∈ℝ*⟼ifx=+∞ify=−∞0+∞ifx=−∞ify=+∞0−∞ify=+∞+∞ify=−∞−∞x+y

Detailed syntax breakdown

Step Hyp Ref Expression
0 cxad class+𝑒
1 vx setvarx
2 cxr classℝ*
3 vy setvary
4 1 cv setvarx
5 cpnf class+∞
6 4 5 wceq wffx=+∞
7 3 cv setvary
8 cmnf class−∞
9 7 8 wceq wffy=−∞
10 cc0 class0
11 9 10 5 cif classify=−∞0+∞
12 4 8 wceq wffx=−∞
13 7 5 wceq wffy=+∞
14 13 10 8 cif classify=+∞0−∞
15 caddc class+
16 4 7 15 co classx+y
17 9 8 16 cif classify=−∞−∞x+y
18 13 5 17 cif classify=+∞+∞ify=−∞−∞x+y
19 12 14 18 cif classifx=−∞ify=+∞0−∞ify=+∞+∞ify=−∞−∞x+y
20 6 11 19 cif classifx=+∞ify=−∞0+∞ifx=−∞ify=+∞0−∞ify=+∞+∞ify=−∞−∞x+y
21 1 3 2 2 20 cmpo classx∈ℝ*,y∈ℝ*⟼ifx=+∞ify=−∞0+∞ifx=−∞ify=+∞0−∞ify=+∞+∞ify=−∞−∞x+y
22 0 21 wceq wff+𝑒=x∈ℝ*,y∈ℝ*⟼ifx=+∞ify=−∞0+∞ifx=−∞ify=+∞0−∞ify=+∞+∞ify=−∞−∞x+y