# Metamath Proof Explorer

Description: Associativity of extended real addition. The correct condition here is "it is not the case that both +oo and -oo appear as one of A , B , C , i.e. -. { +oo , -oo } C_ { A , B , C } ", but this condition is difficult to work with, so we break the theorem into two parts: this one, where -oo is not present in A , B , C , and xaddass2 , where +oo is not present. (Contributed by Mario Carneiro, 20-Aug-2015)

Ref Expression
`|- ( ( ( A e. RR* /\ A =/= -oo ) /\ ( B e. RR* /\ B =/= -oo ) /\ ( C e. RR* /\ C =/= -oo ) ) -> ( ( A +e B ) +e C ) = ( A +e ( B +e C ) ) )`

### Proof

Step Hyp Ref Expression
1 recn
` |-  ( A e. RR -> A e. CC )`
2 recn
` |-  ( B e. RR -> B e. CC )`
3 recn
` |-  ( C e. RR -> C e. CC )`
` |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A + B ) + C ) = ( A + ( B + C ) ) )`
5 1 2 3 4 syl3an
` |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( A + B ) + C ) = ( A + ( B + C ) ) )`
6 5 3expa
` |-  ( ( ( A e. RR /\ B e. RR ) /\ C e. RR ) -> ( ( A + B ) + C ) = ( A + ( B + C ) ) )`
` |-  ( ( A e. RR /\ B e. RR ) -> ( A + B ) e. RR )`
` |-  ( ( ( A + B ) e. RR /\ C e. RR ) -> ( ( A + B ) +e C ) = ( ( A + B ) + C ) )`
9 7 8 sylan
` |-  ( ( ( A e. RR /\ B e. RR ) /\ C e. RR ) -> ( ( A + B ) +e C ) = ( ( A + B ) + C ) )`
` |-  ( ( B e. RR /\ C e. RR ) -> ( B + C ) e. RR )`
` |-  ( ( A e. RR /\ ( B + C ) e. RR ) -> ( A +e ( B + C ) ) = ( A + ( B + C ) ) )`
12 10 11 sylan2
` |-  ( ( A e. RR /\ ( B e. RR /\ C e. RR ) ) -> ( A +e ( B + C ) ) = ( A + ( B + C ) ) )`
13 12 anassrs
` |-  ( ( ( A e. RR /\ B e. RR ) /\ C e. RR ) -> ( A +e ( B + C ) ) = ( A + ( B + C ) ) )`
14 6 9 13 3eqtr4d
` |-  ( ( ( A e. RR /\ B e. RR ) /\ C e. RR ) -> ( ( A + B ) +e C ) = ( A +e ( B + C ) ) )`
` |-  ( ( A e. RR /\ B e. RR ) -> ( A +e B ) = ( A + B ) )`
` |-  ( ( ( A e. RR /\ B e. RR ) /\ C e. RR ) -> ( A +e B ) = ( A + B ) )`
17 16 oveq1d
` |-  ( ( ( A e. RR /\ B e. RR ) /\ C e. RR ) -> ( ( A +e B ) +e C ) = ( ( A + B ) +e C ) )`
` |-  ( ( B e. RR /\ C e. RR ) -> ( B +e C ) = ( B + C ) )`
` |-  ( ( ( A e. RR /\ B e. RR ) /\ C e. RR ) -> ( B +e C ) = ( B + C ) )`
20 19 oveq2d
` |-  ( ( ( A e. RR /\ B e. RR ) /\ C e. RR ) -> ( A +e ( B +e C ) ) = ( A +e ( B + C ) ) )`
21 14 17 20 3eqtr4d
` |-  ( ( ( A e. RR /\ B e. RR ) /\ C e. RR ) -> ( ( A +e B ) +e C ) = ( A +e ( B +e C ) ) )`
` |-  ( ( ( ( ( A e. RR* /\ A =/= -oo ) /\ ( B e. RR* /\ B =/= -oo ) /\ ( C e. RR* /\ C =/= -oo ) ) /\ ( A e. RR /\ B e. RR ) ) /\ C e. RR ) -> ( ( A +e B ) +e C ) = ( A +e ( B +e C ) ) )`
23 oveq2
` |-  ( C = +oo -> ( ( A +e B ) +e C ) = ( ( A +e B ) +e +oo ) )`
24 simp1l
` |-  ( ( ( A e. RR* /\ A =/= -oo ) /\ ( B e. RR* /\ B =/= -oo ) /\ ( C e. RR* /\ C =/= -oo ) ) -> A e. RR* )`
25 simp2l
` |-  ( ( ( A e. RR* /\ A =/= -oo ) /\ ( B e. RR* /\ B =/= -oo ) /\ ( C e. RR* /\ C =/= -oo ) ) -> B e. RR* )`
` |-  ( ( A e. RR* /\ B e. RR* ) -> ( A +e B ) e. RR* )`
27 24 25 26 syl2anc
` |-  ( ( ( A e. RR* /\ A =/= -oo ) /\ ( B e. RR* /\ B =/= -oo ) /\ ( C e. RR* /\ C =/= -oo ) ) -> ( A +e B ) e. RR* )`
` |-  ( ( ( A e. RR* /\ A =/= -oo ) /\ ( B e. RR* /\ B =/= -oo ) ) -> ( A +e B ) =/= -oo )`
` |-  ( ( ( A e. RR* /\ A =/= -oo ) /\ ( B e. RR* /\ B =/= -oo ) /\ ( C e. RR* /\ C =/= -oo ) ) -> ( A +e B ) =/= -oo )`
` |-  ( ( ( A +e B ) e. RR* /\ ( A +e B ) =/= -oo ) -> ( ( A +e B ) +e +oo ) = +oo )`
31 27 29 30 syl2anc
` |-  ( ( ( A e. RR* /\ A =/= -oo ) /\ ( B e. RR* /\ B =/= -oo ) /\ ( C e. RR* /\ C =/= -oo ) ) -> ( ( A +e B ) +e +oo ) = +oo )`
32 23 31 sylan9eqr
` |-  ( ( ( ( A e. RR* /\ A =/= -oo ) /\ ( B e. RR* /\ B =/= -oo ) /\ ( C e. RR* /\ C =/= -oo ) ) /\ C = +oo ) -> ( ( A +e B ) +e C ) = +oo )`
` |-  ( ( A e. RR* /\ A =/= -oo ) -> ( A +e +oo ) = +oo )`
` |-  ( ( ( A e. RR* /\ A =/= -oo ) /\ ( B e. RR* /\ B =/= -oo ) /\ ( C e. RR* /\ C =/= -oo ) ) -> ( A +e +oo ) = +oo )`
` |-  ( ( ( ( A e. RR* /\ A =/= -oo ) /\ ( B e. RR* /\ B =/= -oo ) /\ ( C e. RR* /\ C =/= -oo ) ) /\ C = +oo ) -> ( A +e +oo ) = +oo )`
36 32 35 eqtr4d
` |-  ( ( ( ( A e. RR* /\ A =/= -oo ) /\ ( B e. RR* /\ B =/= -oo ) /\ ( C e. RR* /\ C =/= -oo ) ) /\ C = +oo ) -> ( ( A +e B ) +e C ) = ( A +e +oo ) )`
37 oveq2
` |-  ( C = +oo -> ( B +e C ) = ( B +e +oo ) )`
` |-  ( ( B e. RR* /\ B =/= -oo ) -> ( B +e +oo ) = +oo )`
` |-  ( ( ( A e. RR* /\ A =/= -oo ) /\ ( B e. RR* /\ B =/= -oo ) /\ ( C e. RR* /\ C =/= -oo ) ) -> ( B +e +oo ) = +oo )`
40 37 39 sylan9eqr
` |-  ( ( ( ( A e. RR* /\ A =/= -oo ) /\ ( B e. RR* /\ B =/= -oo ) /\ ( C e. RR* /\ C =/= -oo ) ) /\ C = +oo ) -> ( B +e C ) = +oo )`
41 40 oveq2d
` |-  ( ( ( ( A e. RR* /\ A =/= -oo ) /\ ( B e. RR* /\ B =/= -oo ) /\ ( C e. RR* /\ C =/= -oo ) ) /\ C = +oo ) -> ( A +e ( B +e C ) ) = ( A +e +oo ) )`
42 36 41 eqtr4d
` |-  ( ( ( ( A e. RR* /\ A =/= -oo ) /\ ( B e. RR* /\ B =/= -oo ) /\ ( C e. RR* /\ C =/= -oo ) ) /\ C = +oo ) -> ( ( A +e B ) +e C ) = ( A +e ( B +e C ) ) )`
` |-  ( ( ( ( ( A e. RR* /\ A =/= -oo ) /\ ( B e. RR* /\ B =/= -oo ) /\ ( C e. RR* /\ C =/= -oo ) ) /\ ( A e. RR /\ B e. RR ) ) /\ C = +oo ) -> ( ( A +e B ) +e C ) = ( A +e ( B +e C ) ) )`
44 simp3
` |-  ( ( ( A e. RR* /\ A =/= -oo ) /\ ( B e. RR* /\ B =/= -oo ) /\ ( C e. RR* /\ C =/= -oo ) ) -> ( C e. RR* /\ C =/= -oo ) )`
45 xrnemnf
` |-  ( ( C e. RR* /\ C =/= -oo ) <-> ( C e. RR \/ C = +oo ) )`
46 44 45 sylib
` |-  ( ( ( A e. RR* /\ A =/= -oo ) /\ ( B e. RR* /\ B =/= -oo ) /\ ( C e. RR* /\ C =/= -oo ) ) -> ( C e. RR \/ C = +oo ) )`
` |-  ( ( ( ( A e. RR* /\ A =/= -oo ) /\ ( B e. RR* /\ B =/= -oo ) /\ ( C e. RR* /\ C =/= -oo ) ) /\ ( A e. RR /\ B e. RR ) ) -> ( C e. RR \/ C = +oo ) )`
48 22 43 47 mpjaodan
` |-  ( ( ( ( A e. RR* /\ A =/= -oo ) /\ ( B e. RR* /\ B =/= -oo ) /\ ( C e. RR* /\ C =/= -oo ) ) /\ ( A e. RR /\ B e. RR ) ) -> ( ( A +e B ) +e C ) = ( A +e ( B +e C ) ) )`
49 48 anassrs
` |-  ( ( ( ( ( A e. RR* /\ A =/= -oo ) /\ ( B e. RR* /\ B =/= -oo ) /\ ( C e. RR* /\ C =/= -oo ) ) /\ A e. RR ) /\ B e. RR ) -> ( ( A +e B ) +e C ) = ( A +e ( B +e C ) ) )`
` |-  ( ( C e. RR* /\ C =/= -oo ) -> ( +oo +e C ) = +oo )`
` |-  ( ( ( A e. RR* /\ A =/= -oo ) /\ ( B e. RR* /\ B =/= -oo ) /\ ( C e. RR* /\ C =/= -oo ) ) -> ( +oo +e C ) = +oo )`
52 51 34 eqtr4d
` |-  ( ( ( A e. RR* /\ A =/= -oo ) /\ ( B e. RR* /\ B =/= -oo ) /\ ( C e. RR* /\ C =/= -oo ) ) -> ( +oo +e C ) = ( A +e +oo ) )`
` |-  ( ( ( ( A e. RR* /\ A =/= -oo ) /\ ( B e. RR* /\ B =/= -oo ) /\ ( C e. RR* /\ C =/= -oo ) ) /\ B = +oo ) -> ( +oo +e C ) = ( A +e +oo ) )`
54 oveq2
` |-  ( B = +oo -> ( A +e B ) = ( A +e +oo ) )`
55 54 34 sylan9eqr
` |-  ( ( ( ( A e. RR* /\ A =/= -oo ) /\ ( B e. RR* /\ B =/= -oo ) /\ ( C e. RR* /\ C =/= -oo ) ) /\ B = +oo ) -> ( A +e B ) = +oo )`
56 55 oveq1d
` |-  ( ( ( ( A e. RR* /\ A =/= -oo ) /\ ( B e. RR* /\ B =/= -oo ) /\ ( C e. RR* /\ C =/= -oo ) ) /\ B = +oo ) -> ( ( A +e B ) +e C ) = ( +oo +e C ) )`
57 oveq1
` |-  ( B = +oo -> ( B +e C ) = ( +oo +e C ) )`
58 57 51 sylan9eqr
` |-  ( ( ( ( A e. RR* /\ A =/= -oo ) /\ ( B e. RR* /\ B =/= -oo ) /\ ( C e. RR* /\ C =/= -oo ) ) /\ B = +oo ) -> ( B +e C ) = +oo )`
59 58 oveq2d
` |-  ( ( ( ( A e. RR* /\ A =/= -oo ) /\ ( B e. RR* /\ B =/= -oo ) /\ ( C e. RR* /\ C =/= -oo ) ) /\ B = +oo ) -> ( A +e ( B +e C ) ) = ( A +e +oo ) )`
60 53 56 59 3eqtr4d
` |-  ( ( ( ( A e. RR* /\ A =/= -oo ) /\ ( B e. RR* /\ B =/= -oo ) /\ ( C e. RR* /\ C =/= -oo ) ) /\ B = +oo ) -> ( ( A +e B ) +e C ) = ( A +e ( B +e C ) ) )`
` |-  ( ( ( ( ( A e. RR* /\ A =/= -oo ) /\ ( B e. RR* /\ B =/= -oo ) /\ ( C e. RR* /\ C =/= -oo ) ) /\ A e. RR ) /\ B = +oo ) -> ( ( A +e B ) +e C ) = ( A +e ( B +e C ) ) )`
62 simpl2
` |-  ( ( ( ( A e. RR* /\ A =/= -oo ) /\ ( B e. RR* /\ B =/= -oo ) /\ ( C e. RR* /\ C =/= -oo ) ) /\ A e. RR ) -> ( B e. RR* /\ B =/= -oo ) )`
63 xrnemnf
` |-  ( ( B e. RR* /\ B =/= -oo ) <-> ( B e. RR \/ B = +oo ) )`
64 62 63 sylib
` |-  ( ( ( ( A e. RR* /\ A =/= -oo ) /\ ( B e. RR* /\ B =/= -oo ) /\ ( C e. RR* /\ C =/= -oo ) ) /\ A e. RR ) -> ( B e. RR \/ B = +oo ) )`
65 49 61 64 mpjaodan
` |-  ( ( ( ( A e. RR* /\ A =/= -oo ) /\ ( B e. RR* /\ B =/= -oo ) /\ ( C e. RR* /\ C =/= -oo ) ) /\ A e. RR ) -> ( ( A +e B ) +e C ) = ( A +e ( B +e C ) ) )`
66 simpl3
` |-  ( ( ( ( A e. RR* /\ A =/= -oo ) /\ ( B e. RR* /\ B =/= -oo ) /\ ( C e. RR* /\ C =/= -oo ) ) /\ A = +oo ) -> ( C e. RR* /\ C =/= -oo ) )`
67 66 50 syl
` |-  ( ( ( ( A e. RR* /\ A =/= -oo ) /\ ( B e. RR* /\ B =/= -oo ) /\ ( C e. RR* /\ C =/= -oo ) ) /\ A = +oo ) -> ( +oo +e C ) = +oo )`
68 simpl2l
` |-  ( ( ( ( A e. RR* /\ A =/= -oo ) /\ ( B e. RR* /\ B =/= -oo ) /\ ( C e. RR* /\ C =/= -oo ) ) /\ A = +oo ) -> B e. RR* )`
69 simpl3l
` |-  ( ( ( ( A e. RR* /\ A =/= -oo ) /\ ( B e. RR* /\ B =/= -oo ) /\ ( C e. RR* /\ C =/= -oo ) ) /\ A = +oo ) -> C e. RR* )`
` |-  ( ( B e. RR* /\ C e. RR* ) -> ( B +e C ) e. RR* )`
71 68 69 70 syl2anc
` |-  ( ( ( ( A e. RR* /\ A =/= -oo ) /\ ( B e. RR* /\ B =/= -oo ) /\ ( C e. RR* /\ C =/= -oo ) ) /\ A = +oo ) -> ( B +e C ) e. RR* )`
72 simpl2
` |-  ( ( ( ( A e. RR* /\ A =/= -oo ) /\ ( B e. RR* /\ B =/= -oo ) /\ ( C e. RR* /\ C =/= -oo ) ) /\ A = +oo ) -> ( B e. RR* /\ B =/= -oo ) )`
` |-  ( ( ( B e. RR* /\ B =/= -oo ) /\ ( C e. RR* /\ C =/= -oo ) ) -> ( B +e C ) =/= -oo )`
74 72 66 73 syl2anc
` |-  ( ( ( ( A e. RR* /\ A =/= -oo ) /\ ( B e. RR* /\ B =/= -oo ) /\ ( C e. RR* /\ C =/= -oo ) ) /\ A = +oo ) -> ( B +e C ) =/= -oo )`
` |-  ( ( ( B +e C ) e. RR* /\ ( B +e C ) =/= -oo ) -> ( +oo +e ( B +e C ) ) = +oo )`
76 71 74 75 syl2anc
` |-  ( ( ( ( A e. RR* /\ A =/= -oo ) /\ ( B e. RR* /\ B =/= -oo ) /\ ( C e. RR* /\ C =/= -oo ) ) /\ A = +oo ) -> ( +oo +e ( B +e C ) ) = +oo )`
77 67 76 eqtr4d
` |-  ( ( ( ( A e. RR* /\ A =/= -oo ) /\ ( B e. RR* /\ B =/= -oo ) /\ ( C e. RR* /\ C =/= -oo ) ) /\ A = +oo ) -> ( +oo +e C ) = ( +oo +e ( B +e C ) ) )`
78 simpr
` |-  ( ( ( ( A e. RR* /\ A =/= -oo ) /\ ( B e. RR* /\ B =/= -oo ) /\ ( C e. RR* /\ C =/= -oo ) ) /\ A = +oo ) -> A = +oo )`
79 78 oveq1d
` |-  ( ( ( ( A e. RR* /\ A =/= -oo ) /\ ( B e. RR* /\ B =/= -oo ) /\ ( C e. RR* /\ C =/= -oo ) ) /\ A = +oo ) -> ( A +e B ) = ( +oo +e B ) )`
` |-  ( ( B e. RR* /\ B =/= -oo ) -> ( +oo +e B ) = +oo )`
81 72 80 syl
` |-  ( ( ( ( A e. RR* /\ A =/= -oo ) /\ ( B e. RR* /\ B =/= -oo ) /\ ( C e. RR* /\ C =/= -oo ) ) /\ A = +oo ) -> ( +oo +e B ) = +oo )`
82 79 81 eqtrd
` |-  ( ( ( ( A e. RR* /\ A =/= -oo ) /\ ( B e. RR* /\ B =/= -oo ) /\ ( C e. RR* /\ C =/= -oo ) ) /\ A = +oo ) -> ( A +e B ) = +oo )`
83 82 oveq1d
` |-  ( ( ( ( A e. RR* /\ A =/= -oo ) /\ ( B e. RR* /\ B =/= -oo ) /\ ( C e. RR* /\ C =/= -oo ) ) /\ A = +oo ) -> ( ( A +e B ) +e C ) = ( +oo +e C ) )`
84 78 oveq1d
` |-  ( ( ( ( A e. RR* /\ A =/= -oo ) /\ ( B e. RR* /\ B =/= -oo ) /\ ( C e. RR* /\ C =/= -oo ) ) /\ A = +oo ) -> ( A +e ( B +e C ) ) = ( +oo +e ( B +e C ) ) )`
85 77 83 84 3eqtr4d
` |-  ( ( ( ( A e. RR* /\ A =/= -oo ) /\ ( B e. RR* /\ B =/= -oo ) /\ ( C e. RR* /\ C =/= -oo ) ) /\ A = +oo ) -> ( ( A +e B ) +e C ) = ( A +e ( B +e C ) ) )`
86 simp1
` |-  ( ( ( A e. RR* /\ A =/= -oo ) /\ ( B e. RR* /\ B =/= -oo ) /\ ( C e. RR* /\ C =/= -oo ) ) -> ( A e. RR* /\ A =/= -oo ) )`
87 xrnemnf
` |-  ( ( A e. RR* /\ A =/= -oo ) <-> ( A e. RR \/ A = +oo ) )`
88 86 87 sylib
` |-  ( ( ( A e. RR* /\ A =/= -oo ) /\ ( B e. RR* /\ B =/= -oo ) /\ ( C e. RR* /\ C =/= -oo ) ) -> ( A e. RR \/ A = +oo ) )`
89 65 85 88 mpjaodan
` |-  ( ( ( A e. RR* /\ A =/= -oo ) /\ ( B e. RR* /\ B =/= -oo ) /\ ( C e. RR* /\ C =/= -oo ) ) -> ( ( A +e B ) +e C ) = ( A +e ( B +e C ) ) )`