Metamath Proof Explorer

Theorem xaddcom

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

Ref Expression
Assertion xaddcom ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 𝐴 +𝑒 𝐵 ) = ( 𝐵 +𝑒 𝐴 ) )

Proof

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