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	$⊢ ((A \in ℝ^{} \land A \neq +∞) \land (B \in ℝ^{} \land B \neq +∞) \land (C \in ℝ^{*} \land C \neq +∞)) \to (A +_{𝑒} B) +_{𝑒} C = A +_{𝑒} (B +_{𝑒} C)$

Proof

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

Metamath Proof Explorer

Theorem xaddass2

Proof