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