Metamath Proof Explorer

Theorem xaddass

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
Assertion xaddass 
|- ( ( ( 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 )
4 addass 
 |-  ( ( 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 ) ) )
7 readdcl 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A + B ) e. RR )
8 rexadd 
 |-  ( ( ( 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 ) )
10 readdcl 
 |-  ( ( B e. RR /\ C e. RR ) -> ( B + C ) e. RR )
11 rexadd 
 |-  ( ( 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 ) ) )
15 rexadd 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A +e B ) = ( A + B ) )
16 15 adantr 
 |-  ( ( ( 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 ) )
18 rexadd 
 |-  ( ( B e. RR /\ C e. RR ) -> ( B +e C ) = ( B + C ) )
19 18 adantll 
 |-  ( ( ( 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 ) ) )
22 21 adantll 
 |-  ( ( ( ( ( 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* )
26 xaddcl 
 |-  ( ( 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* )
28 xaddnemnf 
 |-  ( ( ( A e. RR* /\ A =/= -oo ) /\ ( B e. RR* /\ B =/= -oo ) ) -> ( A +e B ) =/= -oo )
29 28 3adant3 
 |-  ( ( ( A e. RR* /\ A =/= -oo ) /\ ( B e. RR* /\ B =/= -oo ) /\ ( C e. RR* /\ C =/= -oo ) ) -> ( A +e B ) =/= -oo )
30 xaddpnf1 
 |-  ( ( ( 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 )
33 xaddpnf1 
 |-  ( ( A e. RR* /\ A =/= -oo ) -> ( A +e +oo ) = +oo )
34 33 3ad2ant1 
 |-  ( ( ( A e. RR* /\ A =/= -oo ) /\ ( B e. RR* /\ B =/= -oo ) /\ ( C e. RR* /\ C =/= -oo ) ) -> ( A +e +oo ) = +oo )
35 34 adantr 
 |-  ( ( ( ( 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 ) )
38 xaddpnf1 
 |-  ( ( B e. RR* /\ B =/= -oo ) -> ( B +e +oo ) = +oo )
39 38 3ad2ant2 
 |-  ( ( ( 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 ) ) )
43 42 adantlr 
 |-  ( ( ( ( ( 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 ) )
47 46 adantr 
 |-  ( ( ( ( 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 ) ) )
50 xaddpnf2 
 |-  ( ( C e. RR* /\ C =/= -oo ) -> ( +oo +e C ) = +oo )
51 50 3ad2ant3 
 |-  ( ( ( 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 ) )
53 52 adantr 
 |-  ( ( ( ( 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 ) ) )
61 60 adantlr 
 |-  ( ( ( ( ( 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* )
70 xaddcl 
 |-  ( ( 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 ) )
73 xaddnemnf 
 |-  ( ( ( 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 )
75 xaddpnf2 
 |-  ( ( ( 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 ) )
80 xaddpnf2 
 |-  ( ( 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 ) ) )