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	⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐴 ≠ +∞ ) ∧ ( 𝐵 ∈ ℝ* ∧ 𝐵 ≠ +∞ ) ∧ ( 𝐶 ∈ ℝ* ∧ 𝐶 ≠ +∞ ) ) → ( ( 𝐴 +𝑒 𝐵 ) +𝑒 𝐶 ) = ( 𝐴 +𝑒 ( 𝐵 +𝑒 𝐶 ) ) )