Definition df-xadd 13166

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

Assertion

Ref	Expression
df-xadd	⊢ +𝑒 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥 = +∞, if(𝑦 = -∞, 0, +∞), if(𝑥 = -∞, if(𝑦 = +∞, 0, -∞), if(𝑦 = +∞, +∞, if(𝑦 = -∞, -∞, (𝑥 + 𝑦))))))

Distinct variable group:   𝑥,𝑦

Detailed syntax breakdown of Definition df-xadd

Step	Hyp	Ref	Expression
1		cxad 13163	. 2 class +𝑒
2		vx	. . 3 setvar 𝑥
3		vy	. . 3 setvar 𝑦
4		cxr 11269	. . 3 class ℝ*
5	2	cv 1569	. . . . 5 class 𝑥
6		cpnf 11267	. . . . 5 class +∞
7	5, 6	wceq 1570	. . . 4 wff 𝑥 = +∞
8	3	cv 1569	. . . . . 6 class 𝑦
9		cmnf 11268	. . . . . 6 class -∞
10	8, 9	wceq 1570	. . . . 5 wff 𝑦 = -∞
11		cc0 11127	. . . . 5 class 0
12	10, 11, 6	cif 4485	. . . 4 class if(𝑦 = -∞, 0, +∞)
13	5, 9	wceq 1570	. . . . 5 wff 𝑥 = -∞
14	8, 6	wceq 1570	. . . . . 6 wff 𝑦 = +∞
15	14, 11, 9	cif 4485	. . . . 5 class if(𝑦 = +∞, 0, -∞)
16		caddc 11130	. . . . . . . 8 class +
17	5, 8, 16	co 7416	. . . . . . 7 class (𝑥 + 𝑦)
18	10, 9, 17	cif 4485	. . . . . 6 class if(𝑦 = -∞, -∞, (𝑥 + 𝑦))
19	14, 6, 18	cif 4485	. . . . 5 class if(𝑦 = +∞, +∞, if(𝑦 = -∞, -∞, (𝑥 + 𝑦)))
20	13, 15, 19	cif 4485	. . . 4 class if(𝑥 = -∞, if(𝑦 = +∞, 0, -∞), if(𝑦 = +∞, +∞, if(𝑦 = -∞, -∞, (𝑥 + 𝑦))))
21	7, 12, 20	cif 4485	. . 3 class if(𝑥 = +∞, if(𝑦 = -∞, 0, +∞), if(𝑥 = -∞, if(𝑦 = +∞, 0, -∞), if(𝑦 = +∞, +∞, if(𝑦 = -∞, -∞, (𝑥 + 𝑦)))))
22	2, 3, 4, 4, 21	cmpo 7418	. 2 class (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥 = +∞, if(𝑦 = -∞, 0, +∞), if(𝑥 = -∞, if(𝑦 = +∞, 0, -∞), if(𝑦 = +∞, +∞, if(𝑦 = -∞, -∞, (𝑥 + 𝑦))))))
23	1, 22	wceq 1570	1 wff +𝑒 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥 = +∞, if(𝑦 = -∞, 0, +∞), if(𝑥 = -∞, if(𝑦 = +∞, 0, -∞), if(𝑦 = +∞, +∞, if(𝑦 = -∞, -∞, (𝑥 + 𝑦))))))

This definition is used by:  xaddval  13277  xaddf  13278