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	⊢ ( 𝜑 → 𝐴 ∈ ℕ₀^* )
		xnn0add4d.2	⊢ ( 𝜑 → 𝐵 ∈ ℕ₀^* )
		xnn0add4d.3	⊢ ( 𝜑 → 𝐶 ∈ ℕ₀^* )
		xnn0add4d.4	⊢ ( 𝜑 → 𝐷 ∈ ℕ₀^* )
	Assertion	xnn0add4d	⊢ ( 𝜑 → ( ( 𝐴 +_𝑒 𝐵 ) +_𝑒 ( 𝐶 +_𝑒 𝐷 ) ) = ( ( 𝐴 +_𝑒 𝐶 ) +_𝑒 ( 𝐵 +_𝑒 𝐷 ) ) )

Proof

Step	Hyp	Ref	Expression
1		xnn0add4d.1	⊢ ( 𝜑 → 𝐴 ∈ ℕ₀^* )
2		xnn0add4d.2	⊢ ( 𝜑 → 𝐵 ∈ ℕ₀^* )
3		xnn0add4d.3	⊢ ( 𝜑 → 𝐶 ∈ ℕ₀^* )
4		xnn0add4d.4	⊢ ( 𝜑 → 𝐷 ∈ ℕ₀^* )
5		xnn0xrnemnf	⊢ ( 𝐴 ∈ ℕ₀^* → ( 𝐴 ∈ ℝ^* ∧ 𝐴 ≠ -∞ ) )
6	1 5	syl	⊢ ( 𝜑 → ( 𝐴 ∈ ℝ^* ∧ 𝐴 ≠ -∞ ) )
7		xnn0xrnemnf	⊢ ( 𝐵 ∈ ℕ₀^* → ( 𝐵 ∈ ℝ^* ∧ 𝐵 ≠ -∞ ) )
8	2 7	syl	⊢ ( 𝜑 → ( 𝐵 ∈ ℝ^* ∧ 𝐵 ≠ -∞ ) )
9		xnn0xrnemnf	⊢ ( 𝐶 ∈ ℕ₀^* → ( 𝐶 ∈ ℝ^* ∧ 𝐶 ≠ -∞ ) )
10	3 9	syl	⊢ ( 𝜑 → ( 𝐶 ∈ ℝ^* ∧ 𝐶 ≠ -∞ ) )
11		xnn0xrnemnf	⊢ ( 𝐷 ∈ ℕ₀^* → ( 𝐷 ∈ ℝ^* ∧ 𝐷 ≠ -∞ ) )
12	4 11	syl	⊢ ( 𝜑 → ( 𝐷 ∈ ℝ^* ∧ 𝐷 ≠ -∞ ) )
13	6 8 10 12	xadd4d	⊢ ( 𝜑 → ( ( 𝐴 +_𝑒 𝐵 ) +_𝑒 ( 𝐶 +_𝑒 𝐷 ) ) = ( ( 𝐴 +_𝑒 𝐶 ) +_𝑒 ( 𝐵 +_𝑒 𝐷 ) ) )