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

Metamath Proof Explorer

Theorem xnn0add4d

Description: Rearrangement of 4 terms in a sum for extended addition of extended nonnegative integers, analogous to xadd4d . (Contributed by AV, 12-Dec-2020)

		Ref	Expression
	Hypotheses	xnn0add4d.1	$⊢ φ \to A \in ℕ_{0}^{*}$
		xnn0add4d.2	$⊢ φ \to B \in ℕ_{0}^{*}$
		xnn0add4d.3	$⊢ φ \to C \in ℕ_{0}^{*}$
		xnn0add4d.4	$⊢ φ \to D \in ℕ_{0}^{*}$
	Assertion	xnn0add4d	$⊢ φ \to (A +_{𝑒} B) +_{𝑒} (C +_{𝑒} D) = (A +_{𝑒} C) +_{𝑒} (B +_{𝑒} D)$

Proof

Step	Hyp	Ref	Expression
1		xnn0add4d.1	$⊢ φ \to A \in ℕ_{0}^{*}$
2		xnn0add4d.2	$⊢ φ \to B \in ℕ_{0}^{*}$
3		xnn0add4d.3	$⊢ φ \to C \in ℕ_{0}^{*}$
4		xnn0add4d.4	$⊢ φ \to D \in ℕ_{0}^{*}$
5		xnn0xrnemnf	$⊢ A \in ℕ_{0}^{} \to (A \in ℝ^{} \land A \neq −∞)$
6	1 5	syl	$⊢ φ \to (A \in ℝ^{*} \land A \neq −∞)$
7		xnn0xrnemnf	$⊢ B \in ℕ_{0}^{} \to (B \in ℝ^{} \land B \neq −∞)$
8	2 7	syl	$⊢ φ \to (B \in ℝ^{*} \land B \neq −∞)$
9		xnn0xrnemnf	$⊢ C \in ℕ_{0}^{} \to (C \in ℝ^{} \land C \neq −∞)$
10	3 9	syl	$⊢ φ \to (C \in ℝ^{*} \land C \neq −∞)$
11		xnn0xrnemnf	$⊢ D \in ℕ_{0}^{} \to (D \in ℝ^{} \land D \neq −∞)$
12	4 11	syl	$⊢ φ \to (D \in ℝ^{*} \land D \neq −∞)$
13	6 8 10 12	xadd4d	$⊢ φ \to (A +_{𝑒} B) +_{𝑒} (C +_{𝑒} D) = (A +_{𝑒} C) +_{𝑒} (B +_{𝑒} D)$