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

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