This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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	\|- ( 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 ) ) )