Metamath Proof Explorer

Theorem xaddpnf2

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

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

Proof

Step Hyp Ref Expression
1 pnfxr 
 |-  +oo e. RR*
2 xaddval 
 |-  ( ( +oo e. RR* /\ A e. RR* ) -> ( +oo +e A ) = if ( +oo = +oo , if ( A = -oo , 0 , +oo ) , if ( +oo = -oo , if ( A = +oo , 0 , -oo ) , if ( A = +oo , +oo , if ( A = -oo , -oo , ( +oo + A ) ) ) ) ) )
3 1 2 mpan 
 |-  ( A e. RR* -> ( +oo +e A ) = if ( +oo = +oo , if ( A = -oo , 0 , +oo ) , if ( +oo = -oo , if ( A = +oo , 0 , -oo ) , if ( A = +oo , +oo , if ( A = -oo , -oo , ( +oo + A ) ) ) ) ) )
4 eqid 
 |-  +oo = +oo
5 4 iftruei 
 |-  if ( +oo = +oo , if ( A = -oo , 0 , +oo ) , if ( +oo = -oo , if ( A = +oo , 0 , -oo ) , if ( A = +oo , +oo , if ( A = -oo , -oo , ( +oo + A ) ) ) ) ) = if ( A = -oo , 0 , +oo )
6 ifnefalse 
 |-  ( A =/= -oo -> if ( A = -oo , 0 , +oo ) = +oo )
7 5 6 eqtrid 
 |-  ( A =/= -oo -> if ( +oo = +oo , if ( A = -oo , 0 , +oo ) , if ( +oo = -oo , if ( A = +oo , 0 , -oo ) , if ( A = +oo , +oo , if ( A = -oo , -oo , ( +oo + A ) ) ) ) ) = +oo )
8 3 7 sylan9eq 
 |-  ( ( A e. RR* /\ A =/= -oo ) -> ( +oo +e A ) = +oo )