MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-xadd Unicode version

Definition df-xadd 10449
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
StepHypRef Expression
1 cxad 10446 . 2  class  + e
2 vx . . 3  set  x
3 vy . . 3  set  y
4 cxr 8862 . . 3  class  RR*
52cv 1623 . . . . 5  class  x
6 cpnf 8860 . . . . 5  class  +oo
75, 6wceq 1624 . . . 4  wff  x  = 
+oo
83cv 1623 . . . . . 6  class  y
9 cmnf 8861 . . . . . 6  class  -oo
108, 9wceq 1624 . . . . 5  wff  y  = 
-oo
11 cc0 8733 . . . . 5  class  0
1210, 11, 6cif 3567 . . . 4  class  if ( y  =  -oo , 
0 ,  +oo )
135, 9wceq 1624 . . . . 5  wff  x  = 
-oo
148, 6wceq 1624 . . . . . 6  wff  y  = 
+oo
1514, 11, 9cif 3567 . . . . 5  class  if ( y  =  +oo , 
0 ,  -oo )
16 caddc 8736 . . . . . . . 8  class  +
175, 8, 16co 5820 . . . . . . 7  class  ( x  +  y )
1810, 9, 17cif 3567 . . . . . 6  class  if ( y  =  -oo ,  -oo ,  ( x  +  y ) )
1914, 6, 18cif 3567 . . . . 5  class  if ( y  =  +oo ,  +oo ,  if ( y  =  -oo ,  -oo ,  ( x  +  y ) ) )
2013, 15, 19cif 3567 . . . 4  class  if ( x  =  -oo ,  if ( y  =  +oo ,  0 ,  -oo ) ,  if ( y  = 
+oo ,  +oo ,  if ( y  =  -oo , 
-oo ,  ( x  +  y ) ) ) )
217, 12, 20cif 3567 . . 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 ) ) ) ) )
222, 3, 4, 4, 21cmpt2 5822 . 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 ) ) ) ) ) )
231, 22wceq 1624 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 ) ) ) ) ) )
Colors of variables: wff set class
This definition is referenced by:  xaddval  10545  xaddf  10546
  Copyright terms: Public domain W3C validator