Metamath Proof Explorer

Theorem xrge0addass

Description: Associativity of extended nonnegative real addition. (Contributed by Thierry Arnoux, 8-Jun-2017)

Ref Expression
Assertion xrge0addass 
|- ( ( A e. ( 0 [,] +oo ) /\ B e. ( 0 [,] +oo ) /\ C e. ( 0 [,] +oo ) ) -> ( ( A +e B ) +e C ) = ( A +e ( B +e C ) ) )

Proof

Step Hyp Ref Expression
1 iccssxr 
 |-  ( 0 [,] +oo ) C_ RR*
2 simp1 
 |-  ( ( A e. ( 0 [,] +oo ) /\ B e. ( 0 [,] +oo ) /\ C e. ( 0 [,] +oo ) ) -> A e. ( 0 [,] +oo ) )
3 1 2 sselid 
 |-  ( ( A e. ( 0 [,] +oo ) /\ B e. ( 0 [,] +oo ) /\ C e. ( 0 [,] +oo ) ) -> A e. RR* )
4 0xr 
 |-  0 e. RR*
5 4 a1i 
 |-  ( ( A e. ( 0 [,] +oo ) /\ B e. ( 0 [,] +oo ) /\ C e. ( 0 [,] +oo ) ) -> 0 e. RR* )
6 pnfxr 
 |-  +oo e. RR*
7 6 a1i 
 |-  ( ( A e. ( 0 [,] +oo ) /\ B e. ( 0 [,] +oo ) /\ C e. ( 0 [,] +oo ) ) -> +oo e. RR* )
8 elicc4 
 |-  ( ( 0 e. RR* /\ +oo e. RR* /\ A e. RR* ) -> ( A e. ( 0 [,] +oo ) <-> ( 0 <_ A /\ A <_ +oo ) ) )
9 5 7 3 8 syl3anc 
 |-  ( ( A e. ( 0 [,] +oo ) /\ B e. ( 0 [,] +oo ) /\ C e. ( 0 [,] +oo ) ) -> ( A e. ( 0 [,] +oo ) <-> ( 0 <_ A /\ A <_ +oo ) ) )
10 2 9 mpbid 
 |-  ( ( A e. ( 0 [,] +oo ) /\ B e. ( 0 [,] +oo ) /\ C e. ( 0 [,] +oo ) ) -> ( 0 <_ A /\ A <_ +oo ) )
11 10 simpld 
 |-  ( ( A e. ( 0 [,] +oo ) /\ B e. ( 0 [,] +oo ) /\ C e. ( 0 [,] +oo ) ) -> 0 <_ A )
12 ge0nemnf 
 |-  ( ( A e. RR* /\ 0 <_ A ) -> A =/= -oo )
13 3 11 12 syl2anc 
 |-  ( ( A e. ( 0 [,] +oo ) /\ B e. ( 0 [,] +oo ) /\ C e. ( 0 [,] +oo ) ) -> A =/= -oo )
14 simp2 
 |-  ( ( A e. ( 0 [,] +oo ) /\ B e. ( 0 [,] +oo ) /\ C e. ( 0 [,] +oo ) ) -> B e. ( 0 [,] +oo ) )
15 1 14 sselid 
 |-  ( ( A e. ( 0 [,] +oo ) /\ B e. ( 0 [,] +oo ) /\ C e. ( 0 [,] +oo ) ) -> B e. RR* )
16 elicc4 
 |-  ( ( 0 e. RR* /\ +oo e. RR* /\ B e. RR* ) -> ( B e. ( 0 [,] +oo ) <-> ( 0 <_ B /\ B <_ +oo ) ) )
17 5 7 15 16 syl3anc 
 |-  ( ( A e. ( 0 [,] +oo ) /\ B e. ( 0 [,] +oo ) /\ C e. ( 0 [,] +oo ) ) -> ( B e. ( 0 [,] +oo ) <-> ( 0 <_ B /\ B <_ +oo ) ) )
18 14 17 mpbid 
 |-  ( ( A e. ( 0 [,] +oo ) /\ B e. ( 0 [,] +oo ) /\ C e. ( 0 [,] +oo ) ) -> ( 0 <_ B /\ B <_ +oo ) )
19 18 simpld 
 |-  ( ( A e. ( 0 [,] +oo ) /\ B e. ( 0 [,] +oo ) /\ C e. ( 0 [,] +oo ) ) -> 0 <_ B )
20 ge0nemnf 
 |-  ( ( B e. RR* /\ 0 <_ B ) -> B =/= -oo )
21 15 19 20 syl2anc 
 |-  ( ( A e. ( 0 [,] +oo ) /\ B e. ( 0 [,] +oo ) /\ C e. ( 0 [,] +oo ) ) -> B =/= -oo )
22 simp3 
 |-  ( ( A e. ( 0 [,] +oo ) /\ B e. ( 0 [,] +oo ) /\ C e. ( 0 [,] +oo ) ) -> C e. ( 0 [,] +oo ) )
23 1 22 sselid 
 |-  ( ( A e. ( 0 [,] +oo ) /\ B e. ( 0 [,] +oo ) /\ C e. ( 0 [,] +oo ) ) -> C e. RR* )
24 elicc4 
 |-  ( ( 0 e. RR* /\ +oo e. RR* /\ C e. RR* ) -> ( C e. ( 0 [,] +oo ) <-> ( 0 <_ C /\ C <_ +oo ) ) )
25 5 7 23 24 syl3anc 
 |-  ( ( A e. ( 0 [,] +oo ) /\ B e. ( 0 [,] +oo ) /\ C e. ( 0 [,] +oo ) ) -> ( C e. ( 0 [,] +oo ) <-> ( 0 <_ C /\ C <_ +oo ) ) )
26 22 25 mpbid 
 |-  ( ( A e. ( 0 [,] +oo ) /\ B e. ( 0 [,] +oo ) /\ C e. ( 0 [,] +oo ) ) -> ( 0 <_ C /\ C <_ +oo ) )
27 26 simpld 
 |-  ( ( A e. ( 0 [,] +oo ) /\ B e. ( 0 [,] +oo ) /\ C e. ( 0 [,] +oo ) ) -> 0 <_ C )
28 ge0nemnf 
 |-  ( ( C e. RR* /\ 0 <_ C ) -> C =/= -oo )
29 23 27 28 syl2anc 
 |-  ( ( A e. ( 0 [,] +oo ) /\ B e. ( 0 [,] +oo ) /\ C e. ( 0 [,] +oo ) ) -> C =/= -oo )
30 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 ) ) )
31 3 13 15 21 23 29 30 syl222anc 
 |-  ( ( A e. ( 0 [,] +oo ) /\ B e. ( 0 [,] +oo ) /\ C e. ( 0 [,] +oo ) ) -> ( ( A +e B ) +e C ) = ( A +e ( B +e C ) ) )