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 ∈ ℝ * ⟼ if x = +∞ if y = −∞ 0 +∞ if x = −∞ if y = +∞ 0 −∞ if y = +∞ +∞ if y = −∞ −∞ x + y

Detailed syntax breakdown

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