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 
|- +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 ) ) ) ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cxad 
 |-  +e
1 vx 
 |-  x
2 cxr 
 |-  RR*
3 vy 
 |-  y
4 1 cv 
 |-  x
5 cpnf 
 |-  +oo
6 4 5 wceq 
 |-  x = +oo
7 3 cv 
 |-  y
8 cmnf 
 |-  -oo
9 7 8 wceq 
 |-  y = -oo
10 cc0 
 |-  0
11 9 10 5 cif 
 |-  if ( y = -oo , 0 , +oo )
12 4 8 wceq 
 |-  x = -oo
13 7 5 wceq 
 |-  y = +oo
14 13 10 8 cif 
 |-  if ( y = +oo , 0 , -oo )
15 caddc 
 |-  +
16 4 7 15 co 
 |-  ( x + y )
17 9 8 16 cif 
 |-  if ( y = -oo , -oo , ( x + y ) )
18 13 5 17 cif 
 |-  if ( y = +oo , +oo , if ( y = -oo , -oo , ( x + y ) ) )
19 12 14 18 cif 
 |-  if ( x = -oo , if ( y = +oo , 0 , -oo ) , if ( y = +oo , +oo , if ( y = -oo , -oo , ( x + y ) ) ) )
20 6 11 19 cif 
 |-  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 ) ) ) ) )
21 1 3 2 2 20 cmpo 
 |-  ( 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 ) ) ) ) ) )
22 0 21 wceq 
 |-  +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 ) ) ) ) ) )