Definition df-xadd 9453

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

Assertion

Ref	Expression
df-xadd	|- +e = ( x e. RR* , y e. RR* |-> if ( x = +oo , if ( y = -oo , 0 , +oo ) , if ( x = -oo , if ( y = +oo , 0 , -oo ) , if ( y = +oo , +oo , if ( y = -oo , -oo , ( x + y ) ) ) ) ) )

Distinct variable group:   x, y

Detailed syntax breakdown of Definition df-xadd

Step	Hyp	Ref	Expression
1		cxad 9450	. 2 class +e
2		vx	. . 3 setvar x
3		vy	. . 3 setvar y
4		cxr 7723	. . 3 class RR*
5	2	cv 1313	. . . . 5 class x
6		cpnf 7721	. . . . 5 class +oo
7	5, 6	wceq 1314	. . . 4 wff x = +oo
8	3	cv 1313	. . . . . 6 class y
9		cmnf 7722	. . . . . 6 class -oo
10	8, 9	wceq 1314	. . . . 5 wff y = -oo
11		cc0 7547	. . . . 5 class 0
12	10, 11, 6	cif 3440	. . . 4 class if ( y = -oo , 0 , +oo )
13	5, 9	wceq 1314	. . . . 5 wff x = -oo
14	8, 6	wceq 1314	. . . . . 6 wff y = +oo
15	14, 11, 9	cif 3440	. . . . 5 class if ( y = +oo , 0 , -oo )
16		caddc 7550	. . . . . . . 8 class +
17	5, 8, 16	co 5728	. . . . . . 7 class ( x + y )
18	10, 9, 17	cif 3440	. . . . . 6 class if ( y = -oo , -oo , ( x + y ) )
19	14, 6, 18	cif 3440	. . . . 5 class if ( y = +oo , +oo , if ( y = -oo , -oo , ( x + y ) ) )
20	13, 15, 19	cif 3440	. . . 4 class if ( x = -oo , if ( y = +oo , 0 , -oo ) , if ( y = +oo , +oo , if ( y = -oo , -oo , ( x + y ) ) ) )
21	7, 12, 20	cif 3440	. . 3 class if ( x = +oo , if ( y = -oo , 0 , +oo ) , if ( x = -oo , if ( y = +oo , 0 , -oo ) , if ( y = +oo , +oo , if ( y = -oo , -oo , ( x + y ) ) ) ) )
22	2, 3, 4, 4, 21	cmpo 5730	. 2 class ( x e. RR* , y e. RR* |-> if ( x = +oo , if ( y = -oo , 0 , +oo ) , if ( x = -oo , if ( y = +oo , 0 , -oo ) , if ( y = +oo , +oo , if ( y = -oo , -oo , ( x + y ) ) ) ) ) )
23	1, 22	wceq 1314	1 wff +e = ( x e. RR* , y e. RR* |-> if ( x = +oo , if ( y = -oo , 0 , +oo ) , if ( x = -oo , if ( y = +oo , 0 , -oo ) , if ( y = +oo , +oo , if ( y = -oo , -oo , ( x + y ) ) ) ) ) )

This definition is referenced by:  xaddf  9520  xaddval  9521