xadd4d

Description: Rearrangement of 4 terms in a sum for extended addition, analogous to add4d . (Contributed by Alexander van der Vekens, 21-Dec-2017)

	Ref	Expression
Hypotheses	xadd4d.1	$⊢ φ \to (A \in ℝ^{*} \land A \neq −∞)$
	xadd4d.2	$⊢ φ \to (B \in ℝ^{*} \land B \neq −∞)$
	xadd4d.3	$⊢ φ \to (C \in ℝ^{*} \land C \neq −∞)$
	xadd4d.4	$⊢ φ \to (D \in ℝ^{*} \land D \neq −∞)$
Assertion	xadd4d	$⊢ φ \to (A +_{𝑒} B) +_{𝑒} (C +_{𝑒} D) = (A +_{𝑒} C) +_{𝑒} (B +_{𝑒} D)$

Proof

Step	Hyp	Ref	Expression
1		xadd4d.1	$⊢ φ \to (A \in ℝ^{*} \land A \neq −∞)$
2		xadd4d.2	$⊢ φ \to (B \in ℝ^{*} \land B \neq −∞)$
3		xadd4d.3	$⊢ φ \to (C \in ℝ^{*} \land C \neq −∞)$
4		xadd4d.4	$⊢ φ \to (D \in ℝ^{*} \land D \neq −∞)$
5		xaddass	$⊢ ((C \in ℝ^{} \land C \neq −∞) \land (B \in ℝ^{} \land B \neq −∞) \land (D \in ℝ^{*} \land D \neq −∞)) \to (C +_{𝑒} B) +_{𝑒} D = C +_{𝑒} (B +_{𝑒} D)$
6	3 2 4 5	syl3anc	$⊢ φ \to (C +_{𝑒} B) +_{𝑒} D = C +_{𝑒} (B +_{𝑒} D)$
7	6	oveq2d	$⊢ φ \to A +_{𝑒} ((C +_{𝑒} B) +_{𝑒} D) = A +_{𝑒} (C +_{𝑒} (B +_{𝑒} D))$
8	3	simpld	$⊢ φ \to C \in ℝ^{*}$
9	4	simpld	$⊢ φ \to D \in ℝ^{*}$
10	8 9	xaddcld	$⊢ φ \to C +_{𝑒} D \in ℝ^{*}$
11		xaddnemnf	$⊢ ((C \in ℝ^{} \land C \neq −∞) \land (D \in ℝ^{} \land D \neq −∞)) \to C +_{𝑒} D \neq −∞$
12	3 4 11	syl2anc	$⊢ φ \to C +_{𝑒} D \neq −∞$
13		xaddass	$⊢ ((A \in ℝ^{} \land A \neq −∞) \land (B \in ℝ^{} \land B \neq −∞) \land (C +_{𝑒} D \in ℝ^{*} \land C +_{𝑒} D \neq −∞)) \to (A +_{𝑒} B) +_{𝑒} (C +_{𝑒} D) = A +_{𝑒} (B +_{𝑒} (C +_{𝑒} D))$
14	1 2 10 12 13	syl112anc	$⊢ φ \to (A +_{𝑒} B) +_{𝑒} (C +_{𝑒} D) = A +_{𝑒} (B +_{𝑒} (C +_{𝑒} D))$
15	2	simpld	$⊢ φ \to B \in ℝ^{*}$
16		xaddcom	$⊢ (C \in ℝ^{} \land B \in ℝ^{}) \to C +_{𝑒} B = B +_{𝑒} C$
17	8 15 16	syl2anc	$⊢ φ \to C +_{𝑒} B = B +_{𝑒} C$
18	17	oveq1d	$⊢ φ \to (C +_{𝑒} B) +_{𝑒} D = (B +_{𝑒} C) +_{𝑒} D$
19		xaddass	$⊢ ((B \in ℝ^{} \land B \neq −∞) \land (C \in ℝ^{} \land C \neq −∞) \land (D \in ℝ^{*} \land D \neq −∞)) \to (B +_{𝑒} C) +_{𝑒} D = B +_{𝑒} (C +_{𝑒} D)$
20	2 3 4 19	syl3anc	$⊢ φ \to (B +_{𝑒} C) +_{𝑒} D = B +_{𝑒} (C +_{𝑒} D)$
21	18 20	eqtr2d	$⊢ φ \to B +_{𝑒} (C +_{𝑒} D) = (C +_{𝑒} B) +_{𝑒} D$
22	21	oveq2d	$⊢ φ \to A +_{𝑒} (B +_{𝑒} (C +_{𝑒} D)) = A +_{𝑒} ((C +_{𝑒} B) +_{𝑒} D)$
23	14 22	eqtrd	$⊢ φ \to (A +_{𝑒} B) +_{𝑒} (C +_{𝑒} D) = A +_{𝑒} ((C +_{𝑒} B) +_{𝑒} D)$
24	15 9	xaddcld	$⊢ φ \to B +_{𝑒} D \in ℝ^{*}$
25		xaddnemnf	$⊢ ((B \in ℝ^{} \land B \neq −∞) \land (D \in ℝ^{} \land D \neq −∞)) \to B +_{𝑒} D \neq −∞$
26	2 4 25	syl2anc	$⊢ φ \to B +_{𝑒} D \neq −∞$
27		xaddass	$⊢ ((A \in ℝ^{} \land A \neq −∞) \land (C \in ℝ^{} \land C \neq −∞) \land (B +_{𝑒} D \in ℝ^{*} \land B +_{𝑒} D \neq −∞)) \to (A +_{𝑒} C) +_{𝑒} (B +_{𝑒} D) = A +_{𝑒} (C +_{𝑒} (B +_{𝑒} D))$
28	1 3 24 26 27	syl112anc	$⊢ φ \to (A +_{𝑒} C) +_{𝑒} (B +_{𝑒} D) = A +_{𝑒} (C +_{𝑒} (B +_{𝑒} D))$
29	7 23 28	3eqtr4d	$⊢ φ \to (A +_{𝑒} B) +_{𝑒} (C +_{𝑒} D) = (A +_{𝑒} C) +_{𝑒} (B +_{𝑒} D)$

Metamath Proof Explorer

Theorem xadd4d

Proof