xaddass

Description: Associativity of extended real addition. The correct condition here is "it is not the case that both +oo and -oo appear as one of A , B , C , i.e. -. { +oo , -oo } C_ { A , B , C } ", but this condition is difficult to work with, so we break the theorem into two parts: this one, where -oo is not present in A , B , C , and xaddass2 , where +oo is not present. (Contributed by Mario Carneiro, 20-Aug-2015)

		Ref	Expression
	Assertion	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)$

Proof

Step	Hyp	Ref	Expression
1		recn	$⊢ A \in ℝ \to A \in ℂ$
2		recn	$⊢ B \in ℝ \to B \in ℂ$
3		recn	$⊢ C \in ℝ \to C \in ℂ$
4		addass	$⊢ (A \in ℂ \land B \in ℂ \land C \in ℂ) \to A + B + C = A + B + C$
5	1 2 3 4	syl3an	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ) \to A + B + C = A + B + C$
6	5	3expa	$⊢ ((A \in ℝ \land B \in ℝ) \land C \in ℝ) \to A + B + C = A + B + C$
7		readdcl	$⊢ (A \in ℝ \land B \in ℝ) \to A + B \in ℝ$
8		rexadd	$⊢ (A + B \in ℝ \land C \in ℝ) \to (A + B) +_{𝑒} C = A + B + C$
9	7 8	sylan	$⊢ ((A \in ℝ \land B \in ℝ) \land C \in ℝ) \to (A + B) +_{𝑒} C = A + B + C$
10		readdcl	$⊢ (B \in ℝ \land C \in ℝ) \to B + C \in ℝ$
11		rexadd	$⊢ (A \in ℝ \land B + C \in ℝ) \to A +_{𝑒} (B + C) = A + B + C$
12	10 11	sylan2	$⊢ (A \in ℝ \land (B \in ℝ \land C \in ℝ)) \to A +_{𝑒} (B + C) = A + B + C$
13	12	anassrs	$⊢ ((A \in ℝ \land B \in ℝ) \land C \in ℝ) \to A +_{𝑒} (B + C) = A + B + C$
14	6 9 13	3eqtr4d	$⊢ ((A \in ℝ \land B \in ℝ) \land C \in ℝ) \to (A + B) +_{𝑒} C = A +_{𝑒} (B + C)$
15		rexadd	$⊢ (A \in ℝ \land B \in ℝ) \to A +_{𝑒} B = A + B$
16	15	adantr	$⊢ ((A \in ℝ \land B \in ℝ) \land C \in ℝ) \to A +_{𝑒} B = A + B$
17	16	oveq1d	$⊢ ((A \in ℝ \land B \in ℝ) \land C \in ℝ) \to (A +_{𝑒} B) +_{𝑒} C = (A + B) +_{𝑒} C$
18		rexadd	$⊢ (B \in ℝ \land C \in ℝ) \to B +_{𝑒} C = B + C$
19	18	adantll	$⊢ ((A \in ℝ \land B \in ℝ) \land C \in ℝ) \to B +_{𝑒} C = B + C$
20	19	oveq2d	$⊢ ((A \in ℝ \land B \in ℝ) \land C \in ℝ) \to A +_{𝑒} (B +_{𝑒} C) = A +_{𝑒} (B + C)$
21	14 17 20	3eqtr4d	$⊢ ((A \in ℝ \land B \in ℝ) \land C \in ℝ) \to (A +_{𝑒} B) +_{𝑒} C = A +_{𝑒} (B +_{𝑒} C)$
22	21	adantll	$⊢ ((((A \in ℝ^{} \land A \neq −∞) \land (B \in ℝ^{} \land B \neq −∞) \land (C \in ℝ^{*} \land C \neq −∞)) \land (A \in ℝ \land B \in ℝ)) \land C \in ℝ) \to (A +_{𝑒} B) +_{𝑒} C = A +_{𝑒} (B +_{𝑒} C)$
23		oveq2	$⊢ C = +∞ \to (A +_{𝑒} B) +_{𝑒} C = (A +_{𝑒} B) +_{𝑒} +∞$
24		simp1l	$⊢ ((A \in ℝ^{} \land A \neq −∞) \land (B \in ℝ^{} \land B \neq −∞) \land (C \in ℝ^{} \land C \neq −∞)) \to A \in ℝ^{}$
25		simp2l	$⊢ ((A \in ℝ^{} \land A \neq −∞) \land (B \in ℝ^{} \land B \neq −∞) \land (C \in ℝ^{} \land C \neq −∞)) \to B \in ℝ^{}$
26		xaddcl	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to A +_{𝑒} B \in ℝ^{*}$
27	24 25 26	syl2anc	$⊢ ((A \in ℝ^{} \land A \neq −∞) \land (B \in ℝ^{} \land B \neq −∞) \land (C \in ℝ^{} \land C \neq −∞)) \to A +_{𝑒} B \in ℝ^{}$
28		xaddnemnf	$⊢ ((A \in ℝ^{} \land A \neq −∞) \land (B \in ℝ^{} \land B \neq −∞)) \to A +_{𝑒} B \neq −∞$
29	28	3adant3	$⊢ ((A \in ℝ^{} \land A \neq −∞) \land (B \in ℝ^{} \land B \neq −∞) \land (C \in ℝ^{*} \land C \neq −∞)) \to A +_{𝑒} B \neq −∞$
30		xaddpnf1	$⊢ (A +_{𝑒} B \in ℝ^{*} \land A +_{𝑒} B \neq −∞) \to (A +_{𝑒} B) +_{𝑒} +∞ = +∞$
31	27 29 30	syl2anc	$⊢ ((A \in ℝ^{} \land A \neq −∞) \land (B \in ℝ^{} \land B \neq −∞) \land (C \in ℝ^{*} \land C \neq −∞)) \to (A +_{𝑒} B) +_{𝑒} +∞ = +∞$
32	23 31	sylan9eqr	$⊢ (((A \in ℝ^{} \land A \neq −∞) \land (B \in ℝ^{} \land B \neq −∞) \land (C \in ℝ^{*} \land C \neq −∞)) \land C = +∞) \to (A +_{𝑒} B) +_{𝑒} C = +∞$
33		xaddpnf1	$⊢ (A \in ℝ^{*} \land A \neq −∞) \to A +_{𝑒} +∞ = +∞$
34	33	3ad2ant1	$⊢ ((A \in ℝ^{} \land A \neq −∞) \land (B \in ℝ^{} \land B \neq −∞) \land (C \in ℝ^{*} \land C \neq −∞)) \to A +_{𝑒} +∞ = +∞$
35	34	adantr	$⊢ (((A \in ℝ^{} \land A \neq −∞) \land (B \in ℝ^{} \land B \neq −∞) \land (C \in ℝ^{*} \land C \neq −∞)) \land C = +∞) \to A +_{𝑒} +∞ = +∞$
36	32 35	eqtr4d	$⊢ (((A \in ℝ^{} \land A \neq −∞) \land (B \in ℝ^{} \land B \neq −∞) \land (C \in ℝ^{*} \land C \neq −∞)) \land C = +∞) \to (A +_{𝑒} B) +_{𝑒} C = A +_{𝑒} +∞$
37		oveq2	$⊢ C = +∞ \to B +_{𝑒} C = B +_{𝑒} +∞$
38		xaddpnf1	$⊢ (B \in ℝ^{*} \land B \neq −∞) \to B +_{𝑒} +∞ = +∞$
39	38	3ad2ant2	$⊢ ((A \in ℝ^{} \land A \neq −∞) \land (B \in ℝ^{} \land B \neq −∞) \land (C \in ℝ^{*} \land C \neq −∞)) \to B +_{𝑒} +∞ = +∞$
40	37 39	sylan9eqr	$⊢ (((A \in ℝ^{} \land A \neq −∞) \land (B \in ℝ^{} \land B \neq −∞) \land (C \in ℝ^{*} \land C \neq −∞)) \land C = +∞) \to B +_{𝑒} C = +∞$
41	40	oveq2d	$⊢ (((A \in ℝ^{} \land A \neq −∞) \land (B \in ℝ^{} \land B \neq −∞) \land (C \in ℝ^{*} \land C \neq −∞)) \land C = +∞) \to A +_{𝑒} (B +_{𝑒} C) = A +_{𝑒} +∞$
42	36 41	eqtr4d	$⊢ (((A \in ℝ^{} \land A \neq −∞) \land (B \in ℝ^{} \land B \neq −∞) \land (C \in ℝ^{*} \land C \neq −∞)) \land C = +∞) \to (A +_{𝑒} B) +_{𝑒} C = A +_{𝑒} (B +_{𝑒} C)$
43	42	adantlr	$⊢ ((((A \in ℝ^{} \land A \neq −∞) \land (B \in ℝ^{} \land B \neq −∞) \land (C \in ℝ^{*} \land C \neq −∞)) \land (A \in ℝ \land B \in ℝ)) \land C = +∞) \to (A +_{𝑒} B) +_{𝑒} C = A +_{𝑒} (B +_{𝑒} C)$
44		simp3	$⊢ ((A \in ℝ^{} \land A \neq −∞) \land (B \in ℝ^{} \land B \neq −∞) \land (C \in ℝ^{} \land C \neq −∞)) \to (C \in ℝ^{} \land C \neq −∞)$
45		xrnemnf	$⊢ (C \in ℝ^{*} \land C \neq −∞) \leftrightarrow (C \in ℝ \lor C = +∞)$
46	44 45	sylib	$⊢ ((A \in ℝ^{} \land A \neq −∞) \land (B \in ℝ^{} \land B \neq −∞) \land (C \in ℝ^{*} \land C \neq −∞)) \to (C \in ℝ \lor C = +∞)$
47	46	adantr	$⊢ (((A \in ℝ^{} \land A \neq −∞) \land (B \in ℝ^{} \land B \neq −∞) \land (C \in ℝ^{*} \land C \neq −∞)) \land (A \in ℝ \land B \in ℝ)) \to (C \in ℝ \lor C = +∞)$
48	22 43 47	mpjaodan	$⊢ (((A \in ℝ^{} \land A \neq −∞) \land (B \in ℝ^{} \land B \neq −∞) \land (C \in ℝ^{*} \land C \neq −∞)) \land (A \in ℝ \land B \in ℝ)) \to (A +_{𝑒} B) +_{𝑒} C = A +_{𝑒} (B +_{𝑒} C)$
49	48	anassrs	$⊢ ((((A \in ℝ^{} \land A \neq −∞) \land (B \in ℝ^{} \land B \neq −∞) \land (C \in ℝ^{*} \land C \neq −∞)) \land A \in ℝ) \land B \in ℝ) \to (A +_{𝑒} B) +_{𝑒} C = A +_{𝑒} (B +_{𝑒} C)$
50		xaddpnf2	$⊢ (C \in ℝ^{*} \land C \neq −∞) \to +∞ +_{𝑒} C = +∞$
51	50	3ad2ant3	$⊢ ((A \in ℝ^{} \land A \neq −∞) \land (B \in ℝ^{} \land B \neq −∞) \land (C \in ℝ^{*} \land C \neq −∞)) \to +∞ +_{𝑒} C = +∞$
52	51 34	eqtr4d	$⊢ ((A \in ℝ^{} \land A \neq −∞) \land (B \in ℝ^{} \land B \neq −∞) \land (C \in ℝ^{*} \land C \neq −∞)) \to +∞ +_{𝑒} C = A +_{𝑒} +∞$
53	52	adantr	$⊢ (((A \in ℝ^{} \land A \neq −∞) \land (B \in ℝ^{} \land B \neq −∞) \land (C \in ℝ^{*} \land C \neq −∞)) \land B = +∞) \to +∞ +_{𝑒} C = A +_{𝑒} +∞$
54		oveq2	$⊢ B = +∞ \to A +_{𝑒} B = A +_{𝑒} +∞$
55	54 34	sylan9eqr	$⊢ (((A \in ℝ^{} \land A \neq −∞) \land (B \in ℝ^{} \land B \neq −∞) \land (C \in ℝ^{*} \land C \neq −∞)) \land B = +∞) \to A +_{𝑒} B = +∞$
56	55	oveq1d	$⊢ (((A \in ℝ^{} \land A \neq −∞) \land (B \in ℝ^{} \land B \neq −∞) \land (C \in ℝ^{*} \land C \neq −∞)) \land B = +∞) \to (A +_{𝑒} B) +_{𝑒} C = +∞ +_{𝑒} C$
57		oveq1	$⊢ B = +∞ \to B +_{𝑒} C = +∞ +_{𝑒} C$
58	57 51	sylan9eqr	$⊢ (((A \in ℝ^{} \land A \neq −∞) \land (B \in ℝ^{} \land B \neq −∞) \land (C \in ℝ^{*} \land C \neq −∞)) \land B = +∞) \to B +_{𝑒} C = +∞$
59	58	oveq2d	$⊢ (((A \in ℝ^{} \land A \neq −∞) \land (B \in ℝ^{} \land B \neq −∞) \land (C \in ℝ^{*} \land C \neq −∞)) \land B = +∞) \to A +_{𝑒} (B +_{𝑒} C) = A +_{𝑒} +∞$
60	53 56 59	3eqtr4d	$⊢ (((A \in ℝ^{} \land A \neq −∞) \land (B \in ℝ^{} \land B \neq −∞) \land (C \in ℝ^{*} \land C \neq −∞)) \land B = +∞) \to (A +_{𝑒} B) +_{𝑒} C = A +_{𝑒} (B +_{𝑒} C)$
61	60	adantlr	$⊢ ((((A \in ℝ^{} \land A \neq −∞) \land (B \in ℝ^{} \land B \neq −∞) \land (C \in ℝ^{*} \land C \neq −∞)) \land A \in ℝ) \land B = +∞) \to (A +_{𝑒} B) +_{𝑒} C = A +_{𝑒} (B +_{𝑒} C)$
62		simpl2	$⊢ (((A \in ℝ^{} \land A \neq −∞) \land (B \in ℝ^{} \land B \neq −∞) \land (C \in ℝ^{} \land C \neq −∞)) \land A \in ℝ) \to (B \in ℝ^{} \land B \neq −∞)$
63		xrnemnf	$⊢ (B \in ℝ^{*} \land B \neq −∞) \leftrightarrow (B \in ℝ \lor B = +∞)$
64	62 63	sylib	$⊢ (((A \in ℝ^{} \land A \neq −∞) \land (B \in ℝ^{} \land B \neq −∞) \land (C \in ℝ^{*} \land C \neq −∞)) \land A \in ℝ) \to (B \in ℝ \lor B = +∞)$
65	49 61 64	mpjaodan	$⊢ (((A \in ℝ^{} \land A \neq −∞) \land (B \in ℝ^{} \land B \neq −∞) \land (C \in ℝ^{*} \land C \neq −∞)) \land A \in ℝ) \to (A +_{𝑒} B) +_{𝑒} C = A +_{𝑒} (B +_{𝑒} C)$
66		simpl3	$⊢ (((A \in ℝ^{} \land A \neq −∞) \land (B \in ℝ^{} \land B \neq −∞) \land (C \in ℝ^{} \land C \neq −∞)) \land A = +∞) \to (C \in ℝ^{} \land C \neq −∞)$
67	66 50	syl	$⊢ (((A \in ℝ^{} \land A \neq −∞) \land (B \in ℝ^{} \land B \neq −∞) \land (C \in ℝ^{*} \land C \neq −∞)) \land A = +∞) \to +∞ +_{𝑒} C = +∞$
68		simpl2l	$⊢ (((A \in ℝ^{} \land A \neq −∞) \land (B \in ℝ^{} \land B \neq −∞) \land (C \in ℝ^{} \land C \neq −∞)) \land A = +∞) \to B \in ℝ^{}$
69		simpl3l	$⊢ (((A \in ℝ^{} \land A \neq −∞) \land (B \in ℝ^{} \land B \neq −∞) \land (C \in ℝ^{} \land C \neq −∞)) \land A = +∞) \to C \in ℝ^{}$
70		xaddcl	$⊢ (B \in ℝ^{} \land C \in ℝ^{}) \to B +_{𝑒} C \in ℝ^{*}$
71	68 69 70	syl2anc	$⊢ (((A \in ℝ^{} \land A \neq −∞) \land (B \in ℝ^{} \land B \neq −∞) \land (C \in ℝ^{} \land C \neq −∞)) \land A = +∞) \to B +_{𝑒} C \in ℝ^{}$
72		simpl2	$⊢ (((A \in ℝ^{} \land A \neq −∞) \land (B \in ℝ^{} \land B \neq −∞) \land (C \in ℝ^{} \land C \neq −∞)) \land A = +∞) \to (B \in ℝ^{} \land B \neq −∞)$
73		xaddnemnf	$⊢ ((B \in ℝ^{} \land B \neq −∞) \land (C \in ℝ^{} \land C \neq −∞)) \to B +_{𝑒} C \neq −∞$
74	72 66 73	syl2anc	$⊢ (((A \in ℝ^{} \land A \neq −∞) \land (B \in ℝ^{} \land B \neq −∞) \land (C \in ℝ^{*} \land C \neq −∞)) \land A = +∞) \to B +_{𝑒} C \neq −∞$
75		xaddpnf2	$⊢ (B +_{𝑒} C \in ℝ^{*} \land B +_{𝑒} C \neq −∞) \to +∞ +_{𝑒} (B +_{𝑒} C) = +∞$
76	71 74 75	syl2anc	$⊢ (((A \in ℝ^{} \land A \neq −∞) \land (B \in ℝ^{} \land B \neq −∞) \land (C \in ℝ^{*} \land C \neq −∞)) \land A = +∞) \to +∞ +_{𝑒} (B +_{𝑒} C) = +∞$
77	67 76	eqtr4d	$⊢ (((A \in ℝ^{} \land A \neq −∞) \land (B \in ℝ^{} \land B \neq −∞) \land (C \in ℝ^{*} \land C \neq −∞)) \land A = +∞) \to +∞ +_{𝑒} C = +∞ +_{𝑒} (B +_{𝑒} C)$
78		simpr	$⊢ (((A \in ℝ^{} \land A \neq −∞) \land (B \in ℝ^{} \land B \neq −∞) \land (C \in ℝ^{*} \land C \neq −∞)) \land A = +∞) \to A = +∞$
79	78	oveq1d	$⊢ (((A \in ℝ^{} \land A \neq −∞) \land (B \in ℝ^{} \land B \neq −∞) \land (C \in ℝ^{*} \land C \neq −∞)) \land A = +∞) \to A +_{𝑒} B = +∞ +_{𝑒} B$
80		xaddpnf2	$⊢ (B \in ℝ^{*} \land B \neq −∞) \to +∞ +_{𝑒} B = +∞$
81	72 80	syl	$⊢ (((A \in ℝ^{} \land A \neq −∞) \land (B \in ℝ^{} \land B \neq −∞) \land (C \in ℝ^{*} \land C \neq −∞)) \land A = +∞) \to +∞ +_{𝑒} B = +∞$
82	79 81	eqtrd	$⊢ (((A \in ℝ^{} \land A \neq −∞) \land (B \in ℝ^{} \land B \neq −∞) \land (C \in ℝ^{*} \land C \neq −∞)) \land A = +∞) \to A +_{𝑒} B = +∞$
83	82	oveq1d	$⊢ (((A \in ℝ^{} \land A \neq −∞) \land (B \in ℝ^{} \land B \neq −∞) \land (C \in ℝ^{*} \land C \neq −∞)) \land A = +∞) \to (A +_{𝑒} B) +_{𝑒} C = +∞ +_{𝑒} C$
84	78	oveq1d	$⊢ (((A \in ℝ^{} \land A \neq −∞) \land (B \in ℝ^{} \land B \neq −∞) \land (C \in ℝ^{*} \land C \neq −∞)) \land A = +∞) \to A +_{𝑒} (B +_{𝑒} C) = +∞ +_{𝑒} (B +_{𝑒} C)$
85	77 83 84	3eqtr4d	$⊢ (((A \in ℝ^{} \land A \neq −∞) \land (B \in ℝ^{} \land B \neq −∞) \land (C \in ℝ^{*} \land C \neq −∞)) \land A = +∞) \to (A +_{𝑒} B) +_{𝑒} C = A +_{𝑒} (B +_{𝑒} C)$
86		simp1	$⊢ ((A \in ℝ^{} \land A \neq −∞) \land (B \in ℝ^{} \land B \neq −∞) \land (C \in ℝ^{} \land C \neq −∞)) \to (A \in ℝ^{} \land A \neq −∞)$
87		xrnemnf	$⊢ (A \in ℝ^{*} \land A \neq −∞) \leftrightarrow (A \in ℝ \lor A = +∞)$
88	86 87	sylib	$⊢ ((A \in ℝ^{} \land A \neq −∞) \land (B \in ℝ^{} \land B \neq −∞) \land (C \in ℝ^{*} \land C \neq −∞)) \to (A \in ℝ \lor A = +∞)$
89	65 85 88	mpjaodan	$⊢ ((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 xaddass

Proof