Metamath Proof Explorer

Theorem rexadd

Description: The extended real addition operation when both arguments are real. (Contributed by Mario Carneiro, 20-Aug-2015)

Ref Expression
Assertion rexadd 
|- ( ( A e. RR /\ B e. RR ) -> ( A +e B ) = ( A + B ) )

Proof

Step Hyp Ref Expression
1 rexr 
 |-  ( A e. RR -> A e. RR* )
2 rexr 
 |-  ( B e. RR -> B e. RR* )
3 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 ) ) ) ) ) )
4 1 2 3 syl2an 
 |-  ( ( 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 ) ) ) ) ) )
5 renepnf 
 |-  ( A e. RR -> A =/= +oo )
6 ifnefalse 
 |-  ( A =/= +oo -> 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 ) ) ) ) ) = if ( A = -oo , if ( B = +oo , 0 , -oo ) , if ( B = +oo , +oo , if ( B = -oo , -oo , ( A + B ) ) ) ) )
7 5 6 syl 
 |-  ( A e. RR -> 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 ) ) ) ) ) = if ( A = -oo , if ( B = +oo , 0 , -oo ) , if ( B = +oo , +oo , if ( B = -oo , -oo , ( A + B ) ) ) ) )
8 renemnf 
 |-  ( A e. RR -> A =/= -oo )
9 ifnefalse 
 |-  ( A =/= -oo -> if ( A = -oo , if ( B = +oo , 0 , -oo ) , if ( B = +oo , +oo , if ( B = -oo , -oo , ( A + B ) ) ) ) = if ( B = +oo , +oo , if ( B = -oo , -oo , ( A + B ) ) ) )
10 8 9 syl 
 |-  ( A e. RR -> if ( A = -oo , if ( B = +oo , 0 , -oo ) , if ( B = +oo , +oo , if ( B = -oo , -oo , ( A + B ) ) ) ) = if ( B = +oo , +oo , if ( B = -oo , -oo , ( A + B ) ) ) )
11 7 10 eqtrd 
 |-  ( A e. RR -> 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 ) ) ) ) ) = if ( B = +oo , +oo , if ( B = -oo , -oo , ( A + B ) ) ) )
12 renepnf 
 |-  ( B e. RR -> B =/= +oo )
13 ifnefalse 
 |-  ( B =/= +oo -> if ( B = +oo , +oo , if ( B = -oo , -oo , ( A + B ) ) ) = if ( B = -oo , -oo , ( A + B ) ) )
14 12 13 syl 
 |-  ( B e. RR -> if ( B = +oo , +oo , if ( B = -oo , -oo , ( A + B ) ) ) = if ( B = -oo , -oo , ( A + B ) ) )
15 renemnf 
 |-  ( B e. RR -> B =/= -oo )
16 ifnefalse 
 |-  ( B =/= -oo -> if ( B = -oo , -oo , ( A + B ) ) = ( A + B ) )
17 15 16 syl 
 |-  ( B e. RR -> if ( B = -oo , -oo , ( A + B ) ) = ( A + B ) )
18 14 17 eqtrd 
 |-  ( B e. RR -> if ( B = +oo , +oo , if ( B = -oo , -oo , ( A + B ) ) ) = ( A + B ) )
19 11 18 sylan9eq 
 |-  ( ( A e. RR /\ B e. RR ) -> 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 ) ) ) ) ) = ( A + B ) )
20 4 19 eqtrd 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A +e B ) = ( A + B ) )