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	$$⊢\phi \to A\in {\mathbb{N}}_0^{*}$$
	xnn0add4d.2	$$⊢\phi \to B\in {\mathbb{N}}_0^{*}$$
	xnn0add4d.3	$$⊢\phi \to C\in {\mathbb{N}}_0^{*}$$
	xnn0add4d.4	$$⊢\phi \to D\in {\mathbb{N}}_0^{*}$$
Assertion	xnn0add4d	$$⊢\phi \to \left(A{+}_{𝑒}B\right){+}_{𝑒}\left(C{+}_{𝑒}D\right)=\left(A{+}_{𝑒}C\right){+}_{𝑒}\left(B{+}_{𝑒}D\right)$$

Proof

Step	Hyp	Ref	Expression
1		xnn0add4d.1	$$⊢\phi \to A\in {\mathbb{N}}_0^{*}$$
2		xnn0add4d.2	$$⊢\phi \to B\in {\mathbb{N}}_0^{*}$$
3		xnn0add4d.3	$$⊢\phi \to C\in {\mathbb{N}}_0^{*}$$
4		xnn0add4d.4	$$⊢\phi \to D\in {\mathbb{N}}_0^{*}$$
5		xnn0xrnemnf	$$⊢A\in {\mathbb{N}}_0^{*}\to \left(A\in {ℝ}^{*}\wedge A\ne \mathrm{-\infty }\right)$$
6	1 5	syl	$$⊢\phi \to \left(A\in {ℝ}^{*}\wedge A\ne \mathrm{-\infty }\right)$$
7		xnn0xrnemnf	$$⊢B\in {\mathbb{N}}_0^{*}\to \left(B\in {ℝ}^{*}\wedge B\ne \mathrm{-\infty }\right)$$
8	2 7	syl	$$⊢\phi \to \left(B\in {ℝ}^{*}\wedge B\ne \mathrm{-\infty }\right)$$
9		xnn0xrnemnf	$$⊢C\in {\mathbb{N}}_0^{*}\to \left(C\in {ℝ}^{*}\wedge C\ne \mathrm{-\infty }\right)$$
10	3 9	syl	$$⊢\phi \to \left(C\in {ℝ}^{*}\wedge C\ne \mathrm{-\infty }\right)$$
11		xnn0xrnemnf	$$⊢D\in {\mathbb{N}}_0^{*}\to \left(D\in {ℝ}^{*}\wedge D\ne \mathrm{-\infty }\right)$$
12	4 11	syl	$$⊢\phi \to \left(D\in {ℝ}^{*}\wedge D\ne \mathrm{-\infty }\right)$$
13	6 8 10 12	xadd4d	$$⊢\phi \to \left(A{+}_{𝑒}B\right){+}_{𝑒}\left(C{+}_{𝑒}D\right)=\left(A{+}_{𝑒}C\right){+}_{𝑒}\left(B{+}_{𝑒}D\right)$$