Metamath Proof Explorer

Theorem pnfaddmnf

Description: Addition of positive and negative 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 pnfaddmnf 
|- ( +oo +e -oo ) = 0

Proof

Step Hyp Ref Expression
1 pnfxr 
 |-  +oo e. RR*
2 mnfxr 
 |-  -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 eqid 
 |-  +oo = +oo
6 5 iftruei 
 |-  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 , 0 , +oo )
7 eqid 
 |-  -oo = -oo
8 7 iftruei 
 |-  if ( -oo = -oo , 0 , +oo ) = 0
9 4 6 8 3eqtri 
 |-  ( +oo +e -oo ) = 0