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	|- ( ph -> ( A e. RR* /\ A =/= -oo ) )
	xadd4d.2	|- ( ph -> ( B e. RR* /\ B =/= -oo ) )
	xadd4d.3	|- ( ph -> ( C e. RR* /\ C =/= -oo ) )
	xadd4d.4	|- ( ph -> ( D e. RR* /\ D =/= -oo ) )
Assertion	xadd4d	|- ( ph -> ( ( A +e B ) +e ( C +e D ) ) = ( ( A +e C ) +e ( B +e D ) ) )

Proof

Step	Hyp	Ref	Expression
1		xadd4d.1	|- ( ph -> ( A e. RR* /\ A =/= -oo ) )
2		xadd4d.2	|- ( ph -> ( B e. RR* /\ B =/= -oo ) )
3		xadd4d.3	|- ( ph -> ( C e. RR* /\ C =/= -oo ) )
4		xadd4d.4	|- ( ph -> ( D e. RR* /\ D =/= -oo ) )
5		xaddass	|- ( ( ( C e. RR* /\ C =/= -oo ) /\ ( B e. RR* /\ B =/= -oo ) /\ ( D e. RR* /\ D =/= -oo ) ) -> ( ( C +e B ) +e D ) = ( C +e ( B +e D ) ) )
6	3 2 4 5	syl3anc	|- ( ph -> ( ( C +e B ) +e D ) = ( C +e ( B +e D ) ) )
7	6	oveq2d	|- ( ph -> ( A +e ( ( C +e B ) +e D ) ) = ( A +e ( C +e ( B +e D ) ) ) )
8	3	simpld	|- ( ph -> C e. RR* )
9	4	simpld	|- ( ph -> D e. RR* )
10	8 9	xaddcld	|- ( ph -> ( C +e D ) e. RR* )
11		xaddnemnf	|- ( ( ( C e. RR* /\ C =/= -oo ) /\ ( D e. RR* /\ D =/= -oo ) ) -> ( C +e D ) =/= -oo )
12	3 4 11	syl2anc	|- ( ph -> ( C +e D ) =/= -oo )
13		xaddass	|- ( ( ( A e. RR* /\ A =/= -oo ) /\ ( B e. RR* /\ B =/= -oo ) /\ ( ( C +e D ) e. RR* /\ ( C +e D ) =/= -oo ) ) -> ( ( A +e B ) +e ( C +e D ) ) = ( A +e ( B +e ( C +e D ) ) ) )
14	1 2 10 12 13	syl112anc	|- ( ph -> ( ( A +e B ) +e ( C +e D ) ) = ( A +e ( B +e ( C +e D ) ) ) )
15	2	simpld	|- ( ph -> B e. RR* )
16		xaddcom	|- ( ( C e. RR* /\ B e. RR* ) -> ( C +e B ) = ( B +e C ) )
17	8 15 16	syl2anc	|- ( ph -> ( C +e B ) = ( B +e C ) )
18	17	oveq1d	|- ( ph -> ( ( C +e B ) +e D ) = ( ( B +e C ) +e D ) )
19		xaddass	|- ( ( ( B e. RR* /\ B =/= -oo ) /\ ( C e. RR* /\ C =/= -oo ) /\ ( D e. RR* /\ D =/= -oo ) ) -> ( ( B +e C ) +e D ) = ( B +e ( C +e D ) ) )
20	2 3 4 19	syl3anc	|- ( ph -> ( ( B +e C ) +e D ) = ( B +e ( C +e D ) ) )
21	18 20	eqtr2d	|- ( ph -> ( B +e ( C +e D ) ) = ( ( C +e B ) +e D ) )
22	21	oveq2d	|- ( ph -> ( A +e ( B +e ( C +e D ) ) ) = ( A +e ( ( C +e B ) +e D ) ) )
23	14 22	eqtrd	|- ( ph -> ( ( A +e B ) +e ( C +e D ) ) = ( A +e ( ( C +e B ) +e D ) ) )
24	15 9	xaddcld	|- ( ph -> ( B +e D ) e. RR* )
25		xaddnemnf	|- ( ( ( B e. RR* /\ B =/= -oo ) /\ ( D e. RR* /\ D =/= -oo ) ) -> ( B +e D ) =/= -oo )
26	2 4 25	syl2anc	|- ( ph -> ( B +e D ) =/= -oo )
27		xaddass	|- ( ( ( A e. RR* /\ A =/= -oo ) /\ ( C e. RR* /\ C =/= -oo ) /\ ( ( B +e D ) e. RR* /\ ( B +e D ) =/= -oo ) ) -> ( ( A +e C ) +e ( B +e D ) ) = ( A +e ( C +e ( B +e D ) ) ) )
28	1 3 24 26 27	syl112anc	|- ( ph -> ( ( A +e C ) +e ( B +e D ) ) = ( A +e ( C +e ( B +e D ) ) ) )
29	7 23 28	3eqtr4d	|- ( ph -> ( ( A +e B ) +e ( C +e D ) ) = ( ( A +e C ) +e ( B +e D ) ) )