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