Metamath Proof Explorer

Theorem xrge0addass

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

Ref Expression
Assertion xrge0addass ( ( 𝐴 ∈ ( 0 [,] +∞ ) ∧ 𝐵 ∈ ( 0 [,] +∞ ) ∧ 𝐶 ∈ ( 0 [,] +∞ ) ) → ( ( 𝐴 +𝑒 𝐵 ) +𝑒 𝐶 ) = ( 𝐴 +𝑒 ( 𝐵 +𝑒 𝐶 ) ) )

Proof

Step Hyp Ref Expression
1 iccssxr ⊢ ( 0 [,] +∞ ) ⊆ ℝ*
2 simp1 ⊢ ( ( 𝐴 ∈ ( 0 [,] +∞ ) ∧ 𝐵 ∈ ( 0 [,] +∞ ) ∧ 𝐶 ∈ ( 0 [,] +∞ ) ) → 𝐴 ∈ ( 0 [,] +∞ ) )
3 1 2 sselid ⊢ ( ( 𝐴 ∈ ( 0 [,] +∞ ) ∧ 𝐵 ∈ ( 0 [,] +∞ ) ∧ 𝐶 ∈ ( 0 [,] +∞ ) ) → 𝐴 ∈ ℝ* )
4 0xr ⊢ 0 ∈ ℝ*
5 4 a1i ⊢ ( ( 𝐴 ∈ ( 0 [,] +∞ ) ∧ 𝐵 ∈ ( 0 [,] +∞ ) ∧ 𝐶 ∈ ( 0 [,] +∞ ) ) → 0 ∈ ℝ* )
6 pnfxr ⊢ +∞ ∈ ℝ*
7 6 a1i ⊢ ( ( 𝐴 ∈ ( 0 [,] +∞ ) ∧ 𝐵 ∈ ( 0 [,] +∞ ) ∧ 𝐶 ∈ ( 0 [,] +∞ ) ) → +∞ ∈ ℝ* )
8 elicc4 ⊢ ( ( 0 ∈ ℝ* ∧ +∞ ∈ ℝ* ∧ 𝐴 ∈ ℝ* ) → ( 𝐴 ∈ ( 0 [,] +∞ ) ↔ ( 0 ≤ 𝐴 ∧ 𝐴 ≤ +∞ ) ) )
9 5 7 3 8 syl3anc ⊢ ( ( 𝐴 ∈ ( 0 [,] +∞ ) ∧ 𝐵 ∈ ( 0 [,] +∞ ) ∧ 𝐶 ∈ ( 0 [,] +∞ ) ) → ( 𝐴 ∈ ( 0 [,] +∞ ) ↔ ( 0 ≤ 𝐴 ∧ 𝐴 ≤ +∞ ) ) )
10 2 9 mpbid ⊢ ( ( 𝐴 ∈ ( 0 [,] +∞ ) ∧ 𝐵 ∈ ( 0 [,] +∞ ) ∧ 𝐶 ∈ ( 0 [,] +∞ ) ) → ( 0 ≤ 𝐴 ∧ 𝐴 ≤ +∞ ) )
11 10 simpld ⊢ ( ( 𝐴 ∈ ( 0 [,] +∞ ) ∧ 𝐵 ∈ ( 0 [,] +∞ ) ∧ 𝐶 ∈ ( 0 [,] +∞ ) ) → 0 ≤ 𝐴 )
12 ge0nemnf ⊢ ( ( 𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴 ) → 𝐴 ≠ -∞ )
13 3 11 12 syl2anc ⊢ ( ( 𝐴 ∈ ( 0 [,] +∞ ) ∧ 𝐵 ∈ ( 0 [,] +∞ ) ∧ 𝐶 ∈ ( 0 [,] +∞ ) ) → 𝐴 ≠ -∞ )
14 simp2 ⊢ ( ( 𝐴 ∈ ( 0 [,] +∞ ) ∧ 𝐵 ∈ ( 0 [,] +∞ ) ∧ 𝐶 ∈ ( 0 [,] +∞ ) ) → 𝐵 ∈ ( 0 [,] +∞ ) )
15 1 14 sselid ⊢ ( ( 𝐴 ∈ ( 0 [,] +∞ ) ∧ 𝐵 ∈ ( 0 [,] +∞ ) ∧ 𝐶 ∈ ( 0 [,] +∞ ) ) → 𝐵 ∈ ℝ* )
16 elicc4 ⊢ ( ( 0 ∈ ℝ* ∧ +∞ ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 𝐵 ∈ ( 0 [,] +∞ ) ↔ ( 0 ≤ 𝐵 ∧ 𝐵 ≤ +∞ ) ) )
17 5 7 15 16 syl3anc ⊢ ( ( 𝐴 ∈ ( 0 [,] +∞ ) ∧ 𝐵 ∈ ( 0 [,] +∞ ) ∧ 𝐶 ∈ ( 0 [,] +∞ ) ) → ( 𝐵 ∈ ( 0 [,] +∞ ) ↔ ( 0 ≤ 𝐵 ∧ 𝐵 ≤ +∞ ) ) )
18 14 17 mpbid ⊢ ( ( 𝐴 ∈ ( 0 [,] +∞ ) ∧ 𝐵 ∈ ( 0 [,] +∞ ) ∧ 𝐶 ∈ ( 0 [,] +∞ ) ) → ( 0 ≤ 𝐵 ∧ 𝐵 ≤ +∞ ) )
19 18 simpld ⊢ ( ( 𝐴 ∈ ( 0 [,] +∞ ) ∧ 𝐵 ∈ ( 0 [,] +∞ ) ∧ 𝐶 ∈ ( 0 [,] +∞ ) ) → 0 ≤ 𝐵 )
20 ge0nemnf ⊢ ( ( 𝐵 ∈ ℝ* ∧ 0 ≤ 𝐵 ) → 𝐵 ≠ -∞ )
21 15 19 20 syl2anc ⊢ ( ( 𝐴 ∈ ( 0 [,] +∞ ) ∧ 𝐵 ∈ ( 0 [,] +∞ ) ∧ 𝐶 ∈ ( 0 [,] +∞ ) ) → 𝐵 ≠ -∞ )
22 simp3 ⊢ ( ( 𝐴 ∈ ( 0 [,] +∞ ) ∧ 𝐵 ∈ ( 0 [,] +∞ ) ∧ 𝐶 ∈ ( 0 [,] +∞ ) ) → 𝐶 ∈ ( 0 [,] +∞ ) )
23 1 22 sselid ⊢ ( ( 𝐴 ∈ ( 0 [,] +∞ ) ∧ 𝐵 ∈ ( 0 [,] +∞ ) ∧ 𝐶 ∈ ( 0 [,] +∞ ) ) → 𝐶 ∈ ℝ* )
24 elicc4 ⊢ ( ( 0 ∈ ℝ* ∧ +∞ ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) → ( 𝐶 ∈ ( 0 [,] +∞ ) ↔ ( 0 ≤ 𝐶 ∧ 𝐶 ≤ +∞ ) ) )
25 5 7 23 24 syl3anc ⊢ ( ( 𝐴 ∈ ( 0 [,] +∞ ) ∧ 𝐵 ∈ ( 0 [,] +∞ ) ∧ 𝐶 ∈ ( 0 [,] +∞ ) ) → ( 𝐶 ∈ ( 0 [,] +∞ ) ↔ ( 0 ≤ 𝐶 ∧ 𝐶 ≤ +∞ ) ) )
26 22 25 mpbid ⊢ ( ( 𝐴 ∈ ( 0 [,] +∞ ) ∧ 𝐵 ∈ ( 0 [,] +∞ ) ∧ 𝐶 ∈ ( 0 [,] +∞ ) ) → ( 0 ≤ 𝐶 ∧ 𝐶 ≤ +∞ ) )
27 26 simpld ⊢ ( ( 𝐴 ∈ ( 0 [,] +∞ ) ∧ 𝐵 ∈ ( 0 [,] +∞ ) ∧ 𝐶 ∈ ( 0 [,] +∞ ) ) → 0 ≤ 𝐶 )
28 ge0nemnf ⊢ ( ( 𝐶 ∈ ℝ* ∧ 0 ≤ 𝐶 ) → 𝐶 ≠ -∞ )
29 23 27 28 syl2anc ⊢ ( ( 𝐴 ∈ ( 0 [,] +∞ ) ∧ 𝐵 ∈ ( 0 [,] +∞ ) ∧ 𝐶 ∈ ( 0 [,] +∞ ) ) → 𝐶 ≠ -∞ )
30 xaddass ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐴 ≠ -∞ ) ∧ ( 𝐵 ∈ ℝ* ∧ 𝐵 ≠ -∞ ) ∧ ( 𝐶 ∈ ℝ* ∧ 𝐶 ≠ -∞ ) ) → ( ( 𝐴 +𝑒 𝐵 ) +𝑒 𝐶 ) = ( 𝐴 +𝑒 ( 𝐵 +𝑒 𝐶 ) ) )
31 3 13 15 21 23 29 30 syl222anc ⊢ ( ( 𝐴 ∈ ( 0 [,] +∞ ) ∧ 𝐵 ∈ ( 0 [,] +∞ ) ∧ 𝐶 ∈ ( 0 [,] +∞ ) ) → ( ( 𝐴 +𝑒 𝐵 ) +𝑒 𝐶 ) = ( 𝐴 +𝑒 ( 𝐵 +𝑒 𝐶 ) ) )