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 syl6eq 
 |-  ( 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 syl6eq 
 |-  ( 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 )