Metamath Proof Explorer

Theorem xaddval

Description: Value of the extended real addition operation. (Contributed by Mario Carneiro, 20-Aug-2015)

Ref Expression
Assertion xaddval ⊢ A ∈ ℝ * ∧ B ∈ ℝ * → A + 𝑒 B = if A = +∞ if B = −∞ 0 +∞ if A = −∞ if B = +∞ 0 −∞ if B = +∞ +∞ if B = −∞ −∞ A + B

Proof

Step Hyp Ref Expression
1 simpl ⊢ x = A ∧ y = B → x = A
2 1 eqeq1d ⊢ x = A ∧ y = B → x = +∞ ↔ A = +∞
3 simpr ⊢ x = A ∧ y = B → y = B
4 3 eqeq1d ⊢ x = A ∧ y = B → y = −∞ ↔ B = −∞
5 4 ifbid ⊢ x = A ∧ y = B → if y = −∞ 0 +∞ = if B = −∞ 0 +∞
6 1 eqeq1d ⊢ x = A ∧ y = B → x = −∞ ↔ A = −∞
7 3 eqeq1d ⊢ x = A ∧ y = B → y = +∞ ↔ B = +∞
8 7 ifbid ⊢ x = A ∧ y = B → if y = +∞ 0 −∞ = if B = +∞ 0 −∞
9 oveq12 ⊢ x = A ∧ y = B → x + y = A + B
10 4 9 ifbieq2d ⊢ x = A ∧ y = B → if y = −∞ −∞ x + y = if B = −∞ −∞ A + B
11 7 10 ifbieq2d ⊢ x = A ∧ y = B → if y = +∞ +∞ if y = −∞ −∞ x + y = if B = +∞ +∞ if B = −∞ −∞ A + B
12 6 8 11 ifbieq12d ⊢ x = A ∧ y = B → if x = −∞ if y = +∞ 0 −∞ if y = +∞ +∞ if y = −∞ −∞ x + y = if A = −∞ if B = +∞ 0 −∞ if B = +∞ +∞ if B = −∞ −∞ A + B
13 2 5 12 ifbieq12d ⊢ x = A ∧ y = B → if x = +∞ if y = −∞ 0 +∞ if x = −∞ if y = +∞ 0 −∞ if y = +∞ +∞ if y = −∞ −∞ x + y = if A = +∞ if B = −∞ 0 +∞ if A = −∞ if B = +∞ 0 −∞ if B = +∞ +∞ if B = −∞ −∞ A + B
14 df-xadd ⊢ + 𝑒 = x ∈ ℝ * , y ∈ ℝ * ⟼ if x = +∞ if y = −∞ 0 +∞ if x = −∞ if y = +∞ 0 −∞ if y = +∞ +∞ if y = −∞ −∞ x + y
15 c0ex ⊢ 0 ∈ V
16 pnfex ⊢ +∞ ∈ V
17 15 16 ifex ⊢ if B = −∞ 0 +∞ ∈ V
18 mnfxr ⊢ −∞ ∈ ℝ *
19 18 elexi ⊢ −∞ ∈ V
20 15 19 ifex ⊢ if B = +∞ 0 −∞ ∈ V
21 ovex ⊢ A + B ∈ V
22 19 21 ifex ⊢ if B = −∞ −∞ A + B ∈ V
23 16 22 ifex ⊢ if B = +∞ +∞ if B = −∞ −∞ A + B ∈ V
24 20 23 ifex ⊢ if A = −∞ if B = +∞ 0 −∞ if B = +∞ +∞ if B = −∞ −∞ A + B ∈ V
25 17 24 ifex ⊢ if A = +∞ if B = −∞ 0 +∞ if A = −∞ if B = +∞ 0 −∞ if B = +∞ +∞ if B = −∞ −∞ A + B ∈ V
26 13 14 25 ovmpoa ⊢ A ∈ ℝ * ∧ B ∈ ℝ * → A + 𝑒 B = if A = +∞ if B = −∞ 0 +∞ if A = −∞ if B = +∞ 0 −∞ if B = +∞ +∞ if B = −∞ −∞ A + B