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

Metamath Proof Explorer

Theorem xaddass2

Description: Associativity of extended real addition. See xaddass for notes on the hypotheses. (Contributed by Mario Carneiro, 20-Aug-2015)

Ref Expression
Assertion xaddass2 ( ( ( 𝐴 ∈ ℝ* ∧ 𝐴 ≠ +∞ ) ∧ ( 𝐵 ∈ ℝ* ∧ 𝐵 ≠ +∞ ) ∧ ( 𝐶 ∈ ℝ* ∧ 𝐶 ≠ +∞ ) ) → ( ( 𝐴 +𝑒 𝐵 ) +𝑒 𝐶 ) = ( 𝐴 +𝑒 ( 𝐵 +𝑒 𝐶 ) ) )

Proof

Step Hyp Ref Expression
1 simp1l ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐴 ≠ +∞ ) ∧ ( 𝐵 ∈ ℝ* ∧ 𝐵 ≠ +∞ ) ∧ ( 𝐶 ∈ ℝ* ∧ 𝐶 ≠ +∞ ) ) → 𝐴 ∈ ℝ* )
2 xnegcl ⊢ ( 𝐴 ∈ ℝ* → -𝑒 𝐴 ∈ ℝ* )
3 1 2 syl ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐴 ≠ +∞ ) ∧ ( 𝐵 ∈ ℝ* ∧ 𝐵 ≠ +∞ ) ∧ ( 𝐶 ∈ ℝ* ∧ 𝐶 ≠ +∞ ) ) → -𝑒 𝐴 ∈ ℝ* )
4 simp1r ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐴 ≠ +∞ ) ∧ ( 𝐵 ∈ ℝ* ∧ 𝐵 ≠ +∞ ) ∧ ( 𝐶 ∈ ℝ* ∧ 𝐶 ≠ +∞ ) ) → 𝐴 ≠ +∞ )
5 pnfxr ⊢ +∞ ∈ ℝ*
6 xneg11 ⊢ ( ( 𝐴 ∈ ℝ* ∧ +∞ ∈ ℝ* ) → ( -𝑒 𝐴 = -𝑒 +∞ ↔ 𝐴 = +∞ ) )
7 1 5 6 sylancl ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐴 ≠ +∞ ) ∧ ( 𝐵 ∈ ℝ* ∧ 𝐵 ≠ +∞ ) ∧ ( 𝐶 ∈ ℝ* ∧ 𝐶 ≠ +∞ ) ) → ( -𝑒 𝐴 = -𝑒 +∞ ↔ 𝐴 = +∞ ) )
8 7 necon3bid ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐴 ≠ +∞ ) ∧ ( 𝐵 ∈ ℝ* ∧ 𝐵 ≠ +∞ ) ∧ ( 𝐶 ∈ ℝ* ∧ 𝐶 ≠ +∞ ) ) → ( -𝑒 𝐴 ≠ -𝑒 +∞ ↔ 𝐴 ≠ +∞ ) )
9 4 8 mpbird ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐴 ≠ +∞ ) ∧ ( 𝐵 ∈ ℝ* ∧ 𝐵 ≠ +∞ ) ∧ ( 𝐶 ∈ ℝ* ∧ 𝐶 ≠ +∞ ) ) → -𝑒 𝐴 ≠ -𝑒 +∞ )
10 xnegpnf ⊢ -𝑒 +∞ = -∞
11 10 a1i ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐴 ≠ +∞ ) ∧ ( 𝐵 ∈ ℝ* ∧ 𝐵 ≠ +∞ ) ∧ ( 𝐶 ∈ ℝ* ∧ 𝐶 ≠ +∞ ) ) → -𝑒 +∞ = -∞ )
12 9 11 neeqtrd ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐴 ≠ +∞ ) ∧ ( 𝐵 ∈ ℝ* ∧ 𝐵 ≠ +∞ ) ∧ ( 𝐶 ∈ ℝ* ∧ 𝐶 ≠ +∞ ) ) → -𝑒 𝐴 ≠ -∞ )
13 simp2l ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐴 ≠ +∞ ) ∧ ( 𝐵 ∈ ℝ* ∧ 𝐵 ≠ +∞ ) ∧ ( 𝐶 ∈ ℝ* ∧ 𝐶 ≠ +∞ ) ) → 𝐵 ∈ ℝ* )
14 xnegcl ⊢ ( 𝐵 ∈ ℝ* → -𝑒 𝐵 ∈ ℝ* )
15 13 14 syl ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐴 ≠ +∞ ) ∧ ( 𝐵 ∈ ℝ* ∧ 𝐵 ≠ +∞ ) ∧ ( 𝐶 ∈ ℝ* ∧ 𝐶 ≠ +∞ ) ) → -𝑒 𝐵 ∈ ℝ* )
16 simp2r ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐴 ≠ +∞ ) ∧ ( 𝐵 ∈ ℝ* ∧ 𝐵 ≠ +∞ ) ∧ ( 𝐶 ∈ ℝ* ∧ 𝐶 ≠ +∞ ) ) → 𝐵 ≠ +∞ )
17 xneg11 ⊢ ( ( 𝐵 ∈ ℝ* ∧ +∞ ∈ ℝ* ) → ( -𝑒 𝐵 = -𝑒 +∞ ↔ 𝐵 = +∞ ) )
18 13 5 17 sylancl ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐴 ≠ +∞ ) ∧ ( 𝐵 ∈ ℝ* ∧ 𝐵 ≠ +∞ ) ∧ ( 𝐶 ∈ ℝ* ∧ 𝐶 ≠ +∞ ) ) → ( -𝑒 𝐵 = -𝑒 +∞ ↔ 𝐵 = +∞ ) )
19 18 necon3bid ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐴 ≠ +∞ ) ∧ ( 𝐵 ∈ ℝ* ∧ 𝐵 ≠ +∞ ) ∧ ( 𝐶 ∈ ℝ* ∧ 𝐶 ≠ +∞ ) ) → ( -𝑒 𝐵 ≠ -𝑒 +∞ ↔ 𝐵 ≠ +∞ ) )
20 16 19 mpbird ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐴 ≠ +∞ ) ∧ ( 𝐵 ∈ ℝ* ∧ 𝐵 ≠ +∞ ) ∧ ( 𝐶 ∈ ℝ* ∧ 𝐶 ≠ +∞ ) ) → -𝑒 𝐵 ≠ -𝑒 +∞ )
21 20 11 neeqtrd ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐴 ≠ +∞ ) ∧ ( 𝐵 ∈ ℝ* ∧ 𝐵 ≠ +∞ ) ∧ ( 𝐶 ∈ ℝ* ∧ 𝐶 ≠ +∞ ) ) → -𝑒 𝐵 ≠ -∞ )
22 simp3l ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐴 ≠ +∞ ) ∧ ( 𝐵 ∈ ℝ* ∧ 𝐵 ≠ +∞ ) ∧ ( 𝐶 ∈ ℝ* ∧ 𝐶 ≠ +∞ ) ) → 𝐶 ∈ ℝ* )
23 xnegcl ⊢ ( 𝐶 ∈ ℝ* → -𝑒 𝐶 ∈ ℝ* )
24 22 23 syl ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐴 ≠ +∞ ) ∧ ( 𝐵 ∈ ℝ* ∧ 𝐵 ≠ +∞ ) ∧ ( 𝐶 ∈ ℝ* ∧ 𝐶 ≠ +∞ ) ) → -𝑒 𝐶 ∈ ℝ* )
25 simp3r ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐴 ≠ +∞ ) ∧ ( 𝐵 ∈ ℝ* ∧ 𝐵 ≠ +∞ ) ∧ ( 𝐶 ∈ ℝ* ∧ 𝐶 ≠ +∞ ) ) → 𝐶 ≠ +∞ )
26 xneg11 ⊢ ( ( 𝐶 ∈ ℝ* ∧ +∞ ∈ ℝ* ) → ( -𝑒 𝐶 = -𝑒 +∞ ↔ 𝐶 = +∞ ) )
27 22 5 26 sylancl ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐴 ≠ +∞ ) ∧ ( 𝐵 ∈ ℝ* ∧ 𝐵 ≠ +∞ ) ∧ ( 𝐶 ∈ ℝ* ∧ 𝐶 ≠ +∞ ) ) → ( -𝑒 𝐶 = -𝑒 +∞ ↔ 𝐶 = +∞ ) )
28 27 necon3bid ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐴 ≠ +∞ ) ∧ ( 𝐵 ∈ ℝ* ∧ 𝐵 ≠ +∞ ) ∧ ( 𝐶 ∈ ℝ* ∧ 𝐶 ≠ +∞ ) ) → ( -𝑒 𝐶 ≠ -𝑒 +∞ ↔ 𝐶 ≠ +∞ ) )
29 25 28 mpbird ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐴 ≠ +∞ ) ∧ ( 𝐵 ∈ ℝ* ∧ 𝐵 ≠ +∞ ) ∧ ( 𝐶 ∈ ℝ* ∧ 𝐶 ≠ +∞ ) ) → -𝑒 𝐶 ≠ -𝑒 +∞ )
30 29 11 neeqtrd ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐴 ≠ +∞ ) ∧ ( 𝐵 ∈ ℝ* ∧ 𝐵 ≠ +∞ ) ∧ ( 𝐶 ∈ ℝ* ∧ 𝐶 ≠ +∞ ) ) → -𝑒 𝐶 ≠ -∞ )
31 xaddass ⊢ ( ( ( -𝑒 𝐴 ∈ ℝ* ∧ -𝑒 𝐴 ≠ -∞ ) ∧ ( -𝑒 𝐵 ∈ ℝ* ∧ -𝑒 𝐵 ≠ -∞ ) ∧ ( -𝑒 𝐶 ∈ ℝ* ∧ -𝑒 𝐶 ≠ -∞ ) ) → ( ( -𝑒 𝐴 +𝑒 -𝑒 𝐵 ) +𝑒 -𝑒 𝐶 ) = ( -𝑒 𝐴 +𝑒 ( -𝑒 𝐵 +𝑒 -𝑒 𝐶 ) ) )
32 3 12 15 21 24 30 31 syl222anc ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐴 ≠ +∞ ) ∧ ( 𝐵 ∈ ℝ* ∧ 𝐵 ≠ +∞ ) ∧ ( 𝐶 ∈ ℝ* ∧ 𝐶 ≠ +∞ ) ) → ( ( -𝑒 𝐴 +𝑒 -𝑒 𝐵 ) +𝑒 -𝑒 𝐶 ) = ( -𝑒 𝐴 +𝑒 ( -𝑒 𝐵 +𝑒 -𝑒 𝐶 ) ) )
33 xnegdi ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → -𝑒 ( 𝐴 +𝑒 𝐵 ) = ( -𝑒 𝐴 +𝑒 -𝑒 𝐵 ) )
34 1 13 33 syl2anc ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐴 ≠ +∞ ) ∧ ( 𝐵 ∈ ℝ* ∧ 𝐵 ≠ +∞ ) ∧ ( 𝐶 ∈ ℝ* ∧ 𝐶 ≠ +∞ ) ) → -𝑒 ( 𝐴 +𝑒 𝐵 ) = ( -𝑒 𝐴 +𝑒 -𝑒 𝐵 ) )
35 34 oveq1d ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐴 ≠ +∞ ) ∧ ( 𝐵 ∈ ℝ* ∧ 𝐵 ≠ +∞ ) ∧ ( 𝐶 ∈ ℝ* ∧ 𝐶 ≠ +∞ ) ) → ( -𝑒 ( 𝐴 +𝑒 𝐵 ) +𝑒 -𝑒 𝐶 ) = ( ( -𝑒 𝐴 +𝑒 -𝑒 𝐵 ) +𝑒 -𝑒 𝐶 ) )
36 xnegdi ⊢ ( ( 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) → -𝑒 ( 𝐵 +𝑒 𝐶 ) = ( -𝑒 𝐵 +𝑒 -𝑒 𝐶 ) )
37 13 22 36 syl2anc ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐴 ≠ +∞ ) ∧ ( 𝐵 ∈ ℝ* ∧ 𝐵 ≠ +∞ ) ∧ ( 𝐶 ∈ ℝ* ∧ 𝐶 ≠ +∞ ) ) → -𝑒 ( 𝐵 +𝑒 𝐶 ) = ( -𝑒 𝐵 +𝑒 -𝑒 𝐶 ) )
38 37 oveq2d ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐴 ≠ +∞ ) ∧ ( 𝐵 ∈ ℝ* ∧ 𝐵 ≠ +∞ ) ∧ ( 𝐶 ∈ ℝ* ∧ 𝐶 ≠ +∞ ) ) → ( -𝑒 𝐴 +𝑒 -𝑒 ( 𝐵 +𝑒 𝐶 ) ) = ( -𝑒 𝐴 +𝑒 ( -𝑒 𝐵 +𝑒 -𝑒 𝐶 ) ) )
39 32 35 38 3eqtr4d ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐴 ≠ +∞ ) ∧ ( 𝐵 ∈ ℝ* ∧ 𝐵 ≠ +∞ ) ∧ ( 𝐶 ∈ ℝ* ∧ 𝐶 ≠ +∞ ) ) → ( -𝑒 ( 𝐴 +𝑒 𝐵 ) +𝑒 -𝑒 𝐶 ) = ( -𝑒 𝐴 +𝑒 -𝑒 ( 𝐵 +𝑒 𝐶 ) ) )
40 xaddcl ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 𝐴 +𝑒 𝐵 ) ∈ ℝ* )
41 1 13 40 syl2anc ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐴 ≠ +∞ ) ∧ ( 𝐵 ∈ ℝ* ∧ 𝐵 ≠ +∞ ) ∧ ( 𝐶 ∈ ℝ* ∧ 𝐶 ≠ +∞ ) ) → ( 𝐴 +𝑒 𝐵 ) ∈ ℝ* )
42 xnegdi ⊢ ( ( ( 𝐴 +𝑒 𝐵 ) ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) → -𝑒 ( ( 𝐴 +𝑒 𝐵 ) +𝑒 𝐶 ) = ( -𝑒 ( 𝐴 +𝑒 𝐵 ) +𝑒 -𝑒 𝐶 ) )
43 41 22 42 syl2anc ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐴 ≠ +∞ ) ∧ ( 𝐵 ∈ ℝ* ∧ 𝐵 ≠ +∞ ) ∧ ( 𝐶 ∈ ℝ* ∧ 𝐶 ≠ +∞ ) ) → -𝑒 ( ( 𝐴 +𝑒 𝐵 ) +𝑒 𝐶 ) = ( -𝑒 ( 𝐴 +𝑒 𝐵 ) +𝑒 -𝑒 𝐶 ) )
44 xaddcl ⊢ ( ( 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) → ( 𝐵 +𝑒 𝐶 ) ∈ ℝ* )
45 13 22 44 syl2anc ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐴 ≠ +∞ ) ∧ ( 𝐵 ∈ ℝ* ∧ 𝐵 ≠ +∞ ) ∧ ( 𝐶 ∈ ℝ* ∧ 𝐶 ≠ +∞ ) ) → ( 𝐵 +𝑒 𝐶 ) ∈ ℝ* )
46 xnegdi ⊢ ( ( 𝐴 ∈ ℝ* ∧ ( 𝐵 +𝑒 𝐶 ) ∈ ℝ* ) → -𝑒 ( 𝐴 +𝑒 ( 𝐵 +𝑒 𝐶 ) ) = ( -𝑒 𝐴 +𝑒 -𝑒 ( 𝐵 +𝑒 𝐶 ) ) )
47 1 45 46 syl2anc ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐴 ≠ +∞ ) ∧ ( 𝐵 ∈ ℝ* ∧ 𝐵 ≠ +∞ ) ∧ ( 𝐶 ∈ ℝ* ∧ 𝐶 ≠ +∞ ) ) → -𝑒 ( 𝐴 +𝑒 ( 𝐵 +𝑒 𝐶 ) ) = ( -𝑒 𝐴 +𝑒 -𝑒 ( 𝐵 +𝑒 𝐶 ) ) )
48 39 43 47 3eqtr4d ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐴 ≠ +∞ ) ∧ ( 𝐵 ∈ ℝ* ∧ 𝐵 ≠ +∞ ) ∧ ( 𝐶 ∈ ℝ* ∧ 𝐶 ≠ +∞ ) ) → -𝑒 ( ( 𝐴 +𝑒 𝐵 ) +𝑒 𝐶 ) = -𝑒 ( 𝐴 +𝑒 ( 𝐵 +𝑒 𝐶 ) ) )
49 xaddcl ⊢ ( ( ( 𝐴 +𝑒 𝐵 ) ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) → ( ( 𝐴 +𝑒 𝐵 ) +𝑒 𝐶 ) ∈ ℝ* )
50 41 22 49 syl2anc ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐴 ≠ +∞ ) ∧ ( 𝐵 ∈ ℝ* ∧ 𝐵 ≠ +∞ ) ∧ ( 𝐶 ∈ ℝ* ∧ 𝐶 ≠ +∞ ) ) → ( ( 𝐴 +𝑒 𝐵 ) +𝑒 𝐶 ) ∈ ℝ* )
51 xaddcl ⊢ ( ( 𝐴 ∈ ℝ* ∧ ( 𝐵 +𝑒 𝐶 ) ∈ ℝ* ) → ( 𝐴 +𝑒 ( 𝐵 +𝑒 𝐶 ) ) ∈ ℝ* )
52 1 45 51 syl2anc ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐴 ≠ +∞ ) ∧ ( 𝐵 ∈ ℝ* ∧ 𝐵 ≠ +∞ ) ∧ ( 𝐶 ∈ ℝ* ∧ 𝐶 ≠ +∞ ) ) → ( 𝐴 +𝑒 ( 𝐵 +𝑒 𝐶 ) ) ∈ ℝ* )
53 xneg11 ⊢ ( ( ( ( 𝐴 +𝑒 𝐵 ) +𝑒 𝐶 ) ∈ ℝ* ∧ ( 𝐴 +𝑒 ( 𝐵 +𝑒 𝐶 ) ) ∈ ℝ* ) → ( -𝑒 ( ( 𝐴 +𝑒 𝐵 ) +𝑒 𝐶 ) = -𝑒 ( 𝐴 +𝑒 ( 𝐵 +𝑒 𝐶 ) ) ↔ ( ( 𝐴 +𝑒 𝐵 ) +𝑒 𝐶 ) = ( 𝐴 +𝑒 ( 𝐵 +𝑒 𝐶 ) ) ) )
54 50 52 53 syl2anc ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐴 ≠ +∞ ) ∧ ( 𝐵 ∈ ℝ* ∧ 𝐵 ≠ +∞ ) ∧ ( 𝐶 ∈ ℝ* ∧ 𝐶 ≠ +∞ ) ) → ( -𝑒 ( ( 𝐴 +𝑒 𝐵 ) +𝑒 𝐶 ) = -𝑒 ( 𝐴 +𝑒 ( 𝐵 +𝑒 𝐶 ) ) ↔ ( ( 𝐴 +𝑒 𝐵 ) +𝑒 𝐶 ) = ( 𝐴 +𝑒 ( 𝐵 +𝑒 𝐶 ) ) ) )
55 48 54 mpbid ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐴 ≠ +∞ ) ∧ ( 𝐵 ∈ ℝ* ∧ 𝐵 ≠ +∞ ) ∧ ( 𝐶 ∈ ℝ* ∧ 𝐶 ≠ +∞ ) ) → ( ( 𝐴 +𝑒 𝐵 ) +𝑒 𝐶 ) = ( 𝐴 +𝑒 ( 𝐵 +𝑒 𝐶 ) ) )