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