Metamath Proof Explorer

Theorem xrge0addass

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

Ref Expression
Assertion xrge0addass ⊢A∈0+∞∧B∈0+∞∧C∈0+∞→A+𝑒B+𝑒C=A+𝑒B+𝑒C

Proof

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