Metamath Proof Explorer

Theorem xaddval

Description: Value of the extended real addition operation. (Contributed by Mario Carneiro, 20-Aug-2015)

Ref Expression
Assertion xaddval 
|- ( ( A e. RR* /\ B e. RR* ) -> ( A +e B ) = if ( A = +oo , if ( B = -oo , 0 , +oo ) , if ( A = -oo , if ( B = +oo , 0 , -oo ) , if ( B = +oo , +oo , if ( B = -oo , -oo , ( A + B ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 simpl 
 |-  ( ( x = A /\ y = B ) -> x = A )
2 1 eqeq1d 
 |-  ( ( x = A /\ y = B ) -> ( x = +oo <-> A = +oo ) )
3 simpr 
 |-  ( ( x = A /\ y = B ) -> y = B )
4 3 eqeq1d 
 |-  ( ( x = A /\ y = B ) -> ( y = -oo <-> B = -oo ) )
5 4 ifbid 
 |-  ( ( x = A /\ y = B ) -> if ( y = -oo , 0 , +oo ) = if ( B = -oo , 0 , +oo ) )
6 1 eqeq1d 
 |-  ( ( x = A /\ y = B ) -> ( x = -oo <-> A = -oo ) )
7 3 eqeq1d 
 |-  ( ( x = A /\ y = B ) -> ( y = +oo <-> B = +oo ) )
8 7 ifbid 
 |-  ( ( x = A /\ y = B ) -> if ( y = +oo , 0 , -oo ) = if ( B = +oo , 0 , -oo ) )
9 oveq12 
 |-  ( ( x = A /\ y = B ) -> ( x + y ) = ( A + B ) )
10 4 9 ifbieq2d 
 |-  ( ( x = A /\ y = B ) -> if ( y = -oo , -oo , ( x + y ) ) = if ( B = -oo , -oo , ( A + B ) ) )
11 7 10 ifbieq2d 
 |-  ( ( x = A /\ y = B ) -> if ( y = +oo , +oo , if ( y = -oo , -oo , ( x + y ) ) ) = if ( B = +oo , +oo , if ( B = -oo , -oo , ( A + B ) ) ) )
12 6 8 11 ifbieq12d 
 |-  ( ( x = A /\ y = B ) -> if ( x = -oo , if ( y = +oo , 0 , -oo ) , if ( y = +oo , +oo , if ( y = -oo , -oo , ( x + y ) ) ) ) = if ( A = -oo , if ( B = +oo , 0 , -oo ) , if ( B = +oo , +oo , if ( B = -oo , -oo , ( A + B ) ) ) ) )
13 2 5 12 ifbieq12d 
 |-  ( ( x = A /\ y = B ) -> if ( x = +oo , if ( y = -oo , 0 , +oo ) , if ( x = -oo , if ( y = +oo , 0 , -oo ) , if ( y = +oo , +oo , if ( y = -oo , -oo , ( x + y ) ) ) ) ) = if ( A = +oo , if ( B = -oo , 0 , +oo ) , if ( A = -oo , if ( B = +oo , 0 , -oo ) , if ( B = +oo , +oo , if ( B = -oo , -oo , ( A + B ) ) ) ) ) )
14 df-xadd 
 |-  +e = ( x e. RR* , y e. RR* |-> if ( x = +oo , if ( y = -oo , 0 , +oo ) , if ( x = -oo , if ( y = +oo , 0 , -oo ) , if ( y = +oo , +oo , if ( y = -oo , -oo , ( x + y ) ) ) ) ) )
15 c0ex 
 |-  0 e. _V
16 pnfex 
 |-  +oo e. _V
17 15 16 ifex 
 |-  if ( B = -oo , 0 , +oo ) e. _V
18 mnfxr 
 |-  -oo e. RR*
19 18 elexi 
 |-  -oo e. _V
20 15 19 ifex 
 |-  if ( B = +oo , 0 , -oo ) e. _V
21 ovex 
 |-  ( A + B ) e. _V
22 19 21 ifex 
 |-  if ( B = -oo , -oo , ( A + B ) ) e. _V
23 16 22 ifex 
 |-  if ( B = +oo , +oo , if ( B = -oo , -oo , ( A + B ) ) ) e. _V
24 20 23 ifex 
 |-  if ( A = -oo , if ( B = +oo , 0 , -oo ) , if ( B = +oo , +oo , if ( B = -oo , -oo , ( A + B ) ) ) ) e. _V
25 17 24 ifex 
 |-  if ( A = +oo , if ( B = -oo , 0 , +oo ) , if ( A = -oo , if ( B = +oo , 0 , -oo ) , if ( B = +oo , +oo , if ( B = -oo , -oo , ( A + B ) ) ) ) ) e. _V
26 13 14 25 ovmpoa 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( A +e B ) = if ( A = +oo , if ( B = -oo , 0 , +oo ) , if ( A = -oo , if ( B = +oo , 0 , -oo ) , if ( B = +oo , +oo , if ( B = -oo , -oo , ( A + B ) ) ) ) ) )