Metamath Proof Explorer

Theorem 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 ⊢ ( 𝜑 → ( 𝐴 ∈ ℝ* ∧ 𝐴 ≠ -∞ ) )
xadd4d.2 ⊢ ( 𝜑 → ( 𝐵 ∈ ℝ* ∧ 𝐵 ≠ -∞ ) )
xadd4d.3 ⊢ ( 𝜑 → ( 𝐶 ∈ ℝ* ∧ 𝐶 ≠ -∞ ) )
xadd4d.4 ⊢ ( 𝜑 → ( 𝐷 ∈ ℝ* ∧ 𝐷 ≠ -∞ ) )
Assertion xadd4d ( 𝜑 → ( ( 𝐴 +𝑒 𝐵 ) +𝑒 ( 𝐶 +𝑒 𝐷 ) ) = ( ( 𝐴 +𝑒 𝐶 ) +𝑒 ( 𝐵 +𝑒 𝐷 ) ) )

Proof

Step Hyp Ref Expression
1 xadd4d.1 ⊢ ( 𝜑 → ( 𝐴 ∈ ℝ* ∧ 𝐴 ≠ -∞ ) )
2 xadd4d.2 ⊢ ( 𝜑 → ( 𝐵 ∈ ℝ* ∧ 𝐵 ≠ -∞ ) )
3 xadd4d.3 ⊢ ( 𝜑 → ( 𝐶 ∈ ℝ* ∧ 𝐶 ≠ -∞ ) )
4 xadd4d.4 ⊢ ( 𝜑 → ( 𝐷 ∈ ℝ* ∧ 𝐷 ≠ -∞ ) )
5 xaddass ⊢ ( ( ( 𝐶 ∈ ℝ* ∧ 𝐶 ≠ -∞ ) ∧ ( 𝐵 ∈ ℝ* ∧ 𝐵 ≠ -∞ ) ∧ ( 𝐷 ∈ ℝ* ∧ 𝐷 ≠ -∞ ) ) → ( ( 𝐶 +𝑒 𝐵 ) +𝑒 𝐷 ) = ( 𝐶 +𝑒 ( 𝐵 +𝑒 𝐷 ) ) )
6 3 2 4 5 syl3anc ⊢ ( 𝜑 → ( ( 𝐶 +𝑒 𝐵 ) +𝑒 𝐷 ) = ( 𝐶 +𝑒 ( 𝐵 +𝑒 𝐷 ) ) )
7 6 oveq2d ⊢ ( 𝜑 → ( 𝐴 +𝑒 ( ( 𝐶 +𝑒 𝐵 ) +𝑒 𝐷 ) ) = ( 𝐴 +𝑒 ( 𝐶 +𝑒 ( 𝐵 +𝑒 𝐷 ) ) ) )
8 3 simpld ⊢ ( 𝜑 → 𝐶 ∈ ℝ* )
9 4 simpld ⊢ ( 𝜑 → 𝐷 ∈ ℝ* )
10 8 9 xaddcld ⊢ ( 𝜑 → ( 𝐶 +𝑒 𝐷 ) ∈ ℝ* )
11 xaddnemnf ⊢ ( ( ( 𝐶 ∈ ℝ* ∧ 𝐶 ≠ -∞ ) ∧ ( 𝐷 ∈ ℝ* ∧ 𝐷 ≠ -∞ ) ) → ( 𝐶 +𝑒 𝐷 ) ≠ -∞ )
12 3 4 11 syl2anc ⊢ ( 𝜑 → ( 𝐶 +𝑒 𝐷 ) ≠ -∞ )
13 xaddass ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐴 ≠ -∞ ) ∧ ( 𝐵 ∈ ℝ* ∧ 𝐵 ≠ -∞ ) ∧ ( ( 𝐶 +𝑒 𝐷 ) ∈ ℝ* ∧ ( 𝐶 +𝑒 𝐷 ) ≠ -∞ ) ) → ( ( 𝐴 +𝑒 𝐵 ) +𝑒 ( 𝐶 +𝑒 𝐷 ) ) = ( 𝐴 +𝑒 ( 𝐵 +𝑒 ( 𝐶 +𝑒 𝐷 ) ) ) )
14 1 2 10 12 13 syl112anc ⊢ ( 𝜑 → ( ( 𝐴 +𝑒 𝐵 ) +𝑒 ( 𝐶 +𝑒 𝐷 ) ) = ( 𝐴 +𝑒 ( 𝐵 +𝑒 ( 𝐶 +𝑒 𝐷 ) ) ) )
15 2 simpld ⊢ ( 𝜑 → 𝐵 ∈ ℝ* )
16 xaddcom ⊢ ( ( 𝐶 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 𝐶 +𝑒 𝐵 ) = ( 𝐵 +𝑒 𝐶 ) )
17 8 15 16 syl2anc ⊢ ( 𝜑 → ( 𝐶 +𝑒 𝐵 ) = ( 𝐵 +𝑒 𝐶 ) )
18 17 oveq1d ⊢ ( 𝜑 → ( ( 𝐶 +𝑒 𝐵 ) +𝑒 𝐷 ) = ( ( 𝐵 +𝑒 𝐶 ) +𝑒 𝐷 ) )
19 xaddass ⊢ ( ( ( 𝐵 ∈ ℝ* ∧ 𝐵 ≠ -∞ ) ∧ ( 𝐶 ∈ ℝ* ∧ 𝐶 ≠ -∞ ) ∧ ( 𝐷 ∈ ℝ* ∧ 𝐷 ≠ -∞ ) ) → ( ( 𝐵 +𝑒 𝐶 ) +𝑒 𝐷 ) = ( 𝐵 +𝑒 ( 𝐶 +𝑒 𝐷 ) ) )
20 2 3 4 19 syl3anc ⊢ ( 𝜑 → ( ( 𝐵 +𝑒 𝐶 ) +𝑒 𝐷 ) = ( 𝐵 +𝑒 ( 𝐶 +𝑒 𝐷 ) ) )
21 18 20 eqtr2d ⊢ ( 𝜑 → ( 𝐵 +𝑒 ( 𝐶 +𝑒 𝐷 ) ) = ( ( 𝐶 +𝑒 𝐵 ) +𝑒 𝐷 ) )
22 21 oveq2d ⊢ ( 𝜑 → ( 𝐴 +𝑒 ( 𝐵 +𝑒 ( 𝐶 +𝑒 𝐷 ) ) ) = ( 𝐴 +𝑒 ( ( 𝐶 +𝑒 𝐵 ) +𝑒 𝐷 ) ) )
23 14 22 eqtrd ⊢ ( 𝜑 → ( ( 𝐴 +𝑒 𝐵 ) +𝑒 ( 𝐶 +𝑒 𝐷 ) ) = ( 𝐴 +𝑒 ( ( 𝐶 +𝑒 𝐵 ) +𝑒 𝐷 ) ) )
24 15 9 xaddcld ⊢ ( 𝜑 → ( 𝐵 +𝑒 𝐷 ) ∈ ℝ* )
25 xaddnemnf ⊢ ( ( ( 𝐵 ∈ ℝ* ∧ 𝐵 ≠ -∞ ) ∧ ( 𝐷 ∈ ℝ* ∧ 𝐷 ≠ -∞ ) ) → ( 𝐵 +𝑒 𝐷 ) ≠ -∞ )
26 2 4 25 syl2anc ⊢ ( 𝜑 → ( 𝐵 +𝑒 𝐷 ) ≠ -∞ )
27 xaddass ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐴 ≠ -∞ ) ∧ ( 𝐶 ∈ ℝ* ∧ 𝐶 ≠ -∞ ) ∧ ( ( 𝐵 +𝑒 𝐷 ) ∈ ℝ* ∧ ( 𝐵 +𝑒 𝐷 ) ≠ -∞ ) ) → ( ( 𝐴 +𝑒 𝐶 ) +𝑒 ( 𝐵 +𝑒 𝐷 ) ) = ( 𝐴 +𝑒 ( 𝐶 +𝑒 ( 𝐵 +𝑒 𝐷 ) ) ) )
28 1 3 24 26 27 syl112anc ⊢ ( 𝜑 → ( ( 𝐴 +𝑒 𝐶 ) +𝑒 ( 𝐵 +𝑒 𝐷 ) ) = ( 𝐴 +𝑒 ( 𝐶 +𝑒 ( 𝐵 +𝑒 𝐷 ) ) ) )
29 7 23 28 3eqtr4d ⊢ ( 𝜑 → ( ( 𝐴 +𝑒 𝐵 ) +𝑒 ( 𝐶 +𝑒 𝐷 ) ) = ( ( 𝐴 +𝑒 𝐶 ) +𝑒 ( 𝐵 +𝑒 𝐷 ) ) )