Metamath Proof Explorer

Theorem mnfaddpnf

Description: Addition of negative and positive infinity. This is often taken to be a "null" value or out of the domain, but we define it (somewhat arbitrarily) to be zero so that the resulting function is total, which simplifies proofs. (Contributed by Mario Carneiro, 20-Aug-2015)

Ref Expression
Assertion mnfaddpnf 
|- ( -oo +e +oo ) = 0

Proof

Step Hyp Ref Expression
1 mnfxr 
 |-  -oo e. RR*
2 pnfxr 
 |-  +oo e. RR*
3 xaddval 
 |-  ( ( -oo e. RR* /\ +oo e. RR* ) -> ( -oo +e +oo ) = if ( -oo = +oo , if ( +oo = -oo , 0 , +oo ) , if ( -oo = -oo , if ( +oo = +oo , 0 , -oo ) , if ( +oo = +oo , +oo , if ( +oo = -oo , -oo , ( -oo + +oo ) ) ) ) ) )
4 1 2 3 mp2an 
 |-  ( -oo +e +oo ) = if ( -oo = +oo , if ( +oo = -oo , 0 , +oo ) , if ( -oo = -oo , if ( +oo = +oo , 0 , -oo ) , if ( +oo = +oo , +oo , if ( +oo = -oo , -oo , ( -oo + +oo ) ) ) ) )
5 mnfnepnf 
 |-  -oo =/= +oo
6 ifnefalse 
 |-  ( -oo =/= +oo -> if ( -oo = +oo , if ( +oo = -oo , 0 , +oo ) , if ( -oo = -oo , if ( +oo = +oo , 0 , -oo ) , if ( +oo = +oo , +oo , if ( +oo = -oo , -oo , ( -oo + +oo ) ) ) ) ) = if ( -oo = -oo , if ( +oo = +oo , 0 , -oo ) , if ( +oo = +oo , +oo , if ( +oo = -oo , -oo , ( -oo + +oo ) ) ) ) )
7 5 6 ax-mp 
 |-  if ( -oo = +oo , if ( +oo = -oo , 0 , +oo ) , if ( -oo = -oo , if ( +oo = +oo , 0 , -oo ) , if ( +oo = +oo , +oo , if ( +oo = -oo , -oo , ( -oo + +oo ) ) ) ) ) = if ( -oo = -oo , if ( +oo = +oo , 0 , -oo ) , if ( +oo = +oo , +oo , if ( +oo = -oo , -oo , ( -oo + +oo ) ) ) )
8 eqid 
 |-  -oo = -oo
9 8 iftruei 
 |-  if ( -oo = -oo , if ( +oo = +oo , 0 , -oo ) , if ( +oo = +oo , +oo , if ( +oo = -oo , -oo , ( -oo + +oo ) ) ) ) = if ( +oo = +oo , 0 , -oo )
10 eqid 
 |-  +oo = +oo
11 10 iftruei 
 |-  if ( +oo = +oo , 0 , -oo ) = 0
12 9 11 eqtri 
 |-  if ( -oo = -oo , if ( +oo = +oo , 0 , -oo ) , if ( +oo = +oo , +oo , if ( +oo = -oo , -oo , ( -oo + +oo ) ) ) ) = 0
13 7 12 eqtri 
 |-  if ( -oo = +oo , if ( +oo = -oo , 0 , +oo ) , if ( -oo = -oo , if ( +oo = +oo , 0 , -oo ) , if ( +oo = +oo , +oo , if ( +oo = -oo , -oo , ( -oo + +oo ) ) ) ) ) = 0
14 4 13 eqtri 
 |-  ( -oo +e +oo ) = 0