Metamath Proof Explorer

Theorem xaddmnf1

Description: Addition of negative infinity on the right. (Contributed by Mario Carneiro, 20-Aug-2015)

Ref Expression
Assertion xaddmnf1 
|- ( ( A e. RR* /\ A =/= +oo ) -> ( A +e -oo ) = -oo )

Proof

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