Metamath Proof Explorer


Theorem xaddpnf1

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

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

Proof

Step Hyp Ref Expression
1 pnfxr
 |-  +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 pnfnemnf
 |-  +oo =/= -oo
5 ifnefalse
 |-  ( +oo =/= -oo -> if ( +oo = -oo , 0 , +oo ) = +oo )
6 4 5 mp1i
 |-  ( A =/= -oo -> if ( +oo = -oo , 0 , +oo ) = +oo )
7 ifnefalse
 |-  ( A =/= -oo -> if ( A = -oo , if ( +oo = +oo , 0 , -oo ) , if ( +oo = +oo , +oo , if ( +oo = -oo , -oo , ( A + +oo ) ) ) ) = if ( +oo = +oo , +oo , if ( +oo = -oo , -oo , ( A + +oo ) ) ) )
8 eqid
 |-  +oo = +oo
9 8 iftruei
 |-  if ( +oo = +oo , +oo , if ( +oo = -oo , -oo , ( A + +oo ) ) ) = +oo
10 7 9 eqtrdi
 |-  ( A =/= -oo -> if ( A = -oo , if ( +oo = +oo , 0 , -oo ) , if ( +oo = +oo , +oo , if ( +oo = -oo , -oo , ( A + +oo ) ) ) ) = +oo )
11 6 10 ifeq12d
 |-  ( 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 , +oo , +oo ) )
12 ifid
 |-  if ( A = +oo , +oo , +oo ) = +oo
13 11 12 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 )
14 3 13 sylan9eq
 |-  ( ( A e. RR* /\ A =/= -oo ) -> ( A +e +oo ) = +oo )