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	|- ( ph -> A e. NN0* )
	xnn0add4d.2	|- ( ph -> B e. NN0* )
	xnn0add4d.3	|- ( ph -> C e. NN0* )
	xnn0add4d.4	|- ( ph -> D e. NN0* )
Assertion	xnn0add4d	|- ( ph -> ( ( A +e B ) +e ( C +e D ) ) = ( ( A +e C ) +e ( B +e D ) ) )

Proof

Step	Hyp	Ref	Expression
1		xnn0add4d.1	|- ( ph -> A e. NN0* )
2		xnn0add4d.2	|- ( ph -> B e. NN0* )
3		xnn0add4d.3	|- ( ph -> C e. NN0* )
4		xnn0add4d.4	|- ( ph -> D e. NN0* )
5		xnn0xrnemnf	|- ( A e. NN0* -> ( A e. RR* /\ A =/= -oo ) )
6	1 5	syl	|- ( ph -> ( A e. RR* /\ A =/= -oo ) )
7		xnn0xrnemnf	|- ( B e. NN0* -> ( B e. RR* /\ B =/= -oo ) )
8	2 7	syl	|- ( ph -> ( B e. RR* /\ B =/= -oo ) )
9		xnn0xrnemnf	|- ( C e. NN0* -> ( C e. RR* /\ C =/= -oo ) )
10	3 9	syl	|- ( ph -> ( C e. RR* /\ C =/= -oo ) )
11		xnn0xrnemnf	|- ( D e. NN0* -> ( D e. RR* /\ D =/= -oo ) )
12	4 11	syl	|- ( ph -> ( D e. RR* /\ D =/= -oo ) )
13	6 8 10 12	xadd4d	|- ( ph -> ( ( A +e B ) +e ( C +e D ) ) = ( ( A +e C ) +e ( B +e D ) ) )