This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem xaddcom

Description: The extended real addition operation is commutative. (Contributed by NM, 26-Dec-2011)

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

Proof

Step Hyp Ref Expression
1 elxr 
 |-  ( A e. RR* <-> ( A e. RR \/ A = +oo \/ A = -oo ) )
2 elxr 
 |-  ( B e. RR* <-> ( B e. RR \/ B = +oo \/ B = -oo ) )
3 recn 
 |-  ( A e. RR -> A e. CC )
4 recn 
 |-  ( B e. RR -> B e. CC )
5 addcom 
 |-  ( ( A e. CC /\ B e. CC ) -> ( A + B ) = ( B + A ) )
6 3 4 5 syl2an 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A + B ) = ( B + A ) )
7 rexadd 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A +e B ) = ( A + B ) )
8 rexadd 
 |-  ( ( B e. RR /\ A e. RR ) -> ( B +e A ) = ( B + A ) )
9 8 ancoms 
 |-  ( ( A e. RR /\ B e. RR ) -> ( B +e A ) = ( B + A ) )
10 6 7 9 3eqtr4d 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A +e B ) = ( B +e A ) )
11 oveq2 
 |-  ( B = +oo -> ( A +e B ) = ( A +e +oo ) )
12 rexr 
 |-  ( A e. RR -> A e. RR* )
13 renemnf 
 |-  ( A e. RR -> A =/= -oo )
14 xaddpnf1 
 |-  ( ( A e. RR* /\ A =/= -oo ) -> ( A +e +oo ) = +oo )
15 12 13 14 syl2anc 
 |-  ( A e. RR -> ( A +e +oo ) = +oo )
16 11 15 sylan9eqr 
 |-  ( ( A e. RR /\ B = +oo ) -> ( A +e B ) = +oo )
17 oveq1 
 |-  ( B = +oo -> ( B +e A ) = ( +oo +e A ) )
18 xaddpnf2 
 |-  ( ( A e. RR* /\ A =/= -oo ) -> ( +oo +e A ) = +oo )
19 12 13 18 syl2anc 
 |-  ( A e. RR -> ( +oo +e A ) = +oo )
20 17 19 sylan9eqr 
 |-  ( ( A e. RR /\ B = +oo ) -> ( B +e A ) = +oo )
21 16 20 eqtr4d 
 |-  ( ( A e. RR /\ B = +oo ) -> ( A +e B ) = ( B +e A ) )
22 oveq2 
 |-  ( B = -oo -> ( A +e B ) = ( A +e -oo ) )
23 renepnf 
 |-  ( A e. RR -> A =/= +oo )
24 xaddmnf1 
 |-  ( ( A e. RR* /\ A =/= +oo ) -> ( A +e -oo ) = -oo )
25 12 23 24 syl2anc 
 |-  ( A e. RR -> ( A +e -oo ) = -oo )
26 22 25 sylan9eqr 
 |-  ( ( A e. RR /\ B = -oo ) -> ( A +e B ) = -oo )
27 oveq1 
 |-  ( B = -oo -> ( B +e A ) = ( -oo +e A ) )
28 xaddmnf2 
 |-  ( ( A e. RR* /\ A =/= +oo ) -> ( -oo +e A ) = -oo )
29 12 23 28 syl2anc 
 |-  ( A e. RR -> ( -oo +e A ) = -oo )
30 27 29 sylan9eqr 
 |-  ( ( A e. RR /\ B = -oo ) -> ( B +e A ) = -oo )
31 26 30 eqtr4d 
 |-  ( ( A e. RR /\ B = -oo ) -> ( A +e B ) = ( B +e A ) )
32 10 21 31 3jaodan 
 |-  ( ( A e. RR /\ ( B e. RR \/ B = +oo \/ B = -oo ) ) -> ( A +e B ) = ( B +e A ) )
33 2 32 sylan2b 
 |-  ( ( A e. RR /\ B e. RR* ) -> ( A +e B ) = ( B +e A ) )
34 pnfaddmnf 
 |-  ( +oo +e -oo ) = 0
35 mnfaddpnf 
 |-  ( -oo +e +oo ) = 0
36 34 35 eqtr4i 
 |-  ( +oo +e -oo ) = ( -oo +e +oo )
37 simpr 
 |-  ( ( B e. RR* /\ B = -oo ) -> B = -oo )
38 37 oveq2d 
 |-  ( ( B e. RR* /\ B = -oo ) -> ( +oo +e B ) = ( +oo +e -oo ) )
39 37 oveq1d 
 |-  ( ( B e. RR* /\ B = -oo ) -> ( B +e +oo ) = ( -oo +e +oo ) )
40 36 38 39 3eqtr4a 
 |-  ( ( B e. RR* /\ B = -oo ) -> ( +oo +e B ) = ( B +e +oo ) )
41 xaddpnf2 
 |-  ( ( B e. RR* /\ B =/= -oo ) -> ( +oo +e B ) = +oo )
42 xaddpnf1 
 |-  ( ( B e. RR* /\ B =/= -oo ) -> ( B +e +oo ) = +oo )
43 41 42 eqtr4d 
 |-  ( ( B e. RR* /\ B =/= -oo ) -> ( +oo +e B ) = ( B +e +oo ) )
44 40 43 pm2.61dane 
 |-  ( B e. RR* -> ( +oo +e B ) = ( B +e +oo ) )
45 44 adantl 
 |-  ( ( A = +oo /\ B e. RR* ) -> ( +oo +e B ) = ( B +e +oo ) )
46 simpl 
 |-  ( ( A = +oo /\ B e. RR* ) -> A = +oo )
47 46 oveq1d 
 |-  ( ( A = +oo /\ B e. RR* ) -> ( A +e B ) = ( +oo +e B ) )
48 46 oveq2d 
 |-  ( ( A = +oo /\ B e. RR* ) -> ( B +e A ) = ( B +e +oo ) )
49 45 47 48 3eqtr4d 
 |-  ( ( A = +oo /\ B e. RR* ) -> ( A +e B ) = ( B +e A ) )
50 35 34 eqtr4i 
 |-  ( -oo +e +oo ) = ( +oo +e -oo )
51 simpr 
 |-  ( ( B e. RR* /\ B = +oo ) -> B = +oo )
52 51 oveq2d 
 |-  ( ( B e. RR* /\ B = +oo ) -> ( -oo +e B ) = ( -oo +e +oo ) )
53 51 oveq1d 
 |-  ( ( B e. RR* /\ B = +oo ) -> ( B +e -oo ) = ( +oo +e -oo ) )
54 50 52 53 3eqtr4a 
 |-  ( ( B e. RR* /\ B = +oo ) -> ( -oo +e B ) = ( B +e -oo ) )
55 xaddmnf2 
 |-  ( ( B e. RR* /\ B =/= +oo ) -> ( -oo +e B ) = -oo )
56 xaddmnf1 
 |-  ( ( B e. RR* /\ B =/= +oo ) -> ( B +e -oo ) = -oo )
57 55 56 eqtr4d 
 |-  ( ( B e. RR* /\ B =/= +oo ) -> ( -oo +e B ) = ( B +e -oo ) )
58 54 57 pm2.61dane 
 |-  ( B e. RR* -> ( -oo +e B ) = ( B +e -oo ) )
59 58 adantl 
 |-  ( ( A = -oo /\ B e. RR* ) -> ( -oo +e B ) = ( B +e -oo ) )
60 simpl 
 |-  ( ( A = -oo /\ B e. RR* ) -> A = -oo )
61 60 oveq1d 
 |-  ( ( A = -oo /\ B e. RR* ) -> ( A +e B ) = ( -oo +e B ) )
62 60 oveq2d 
 |-  ( ( A = -oo /\ B e. RR* ) -> ( B +e A ) = ( B +e -oo ) )
63 59 61 62 3eqtr4d 
 |-  ( ( A = -oo /\ B e. RR* ) -> ( A +e B ) = ( B +e A ) )
64 33 49 63 3jaoian 
 |-  ( ( ( A e. RR \/ A = +oo \/ A = -oo ) /\ B e. RR* ) -> ( A +e B ) = ( B +e A ) )
65 1 64 sylanb 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( A +e B ) = ( B +e A ) )