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=ifA=+∞ifB=−∞0+∞ifA=−∞ifB=+∞0−∞ifB=+∞+∞ifB=−∞−∞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→ify=−∞0+∞=ifB=−∞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→ify=+∞0−∞=ifB=+∞0−∞
9 oveq12 ⊢x=A∧y=B→x+y=A+B
10 4 9 ifbieq2d ⊢x=A∧y=B→ify=−∞−∞x+y=ifB=−∞−∞A+B
11 7 10 ifbieq2d ⊢x=A∧y=B→ify=+∞+∞ify=−∞−∞x+y=ifB=+∞+∞ifB=−∞−∞A+B
12 6 8 11 ifbieq12d ⊢x=A∧y=B→ifx=−∞ify=+∞0−∞ify=+∞+∞ify=−∞−∞x+y=ifA=−∞ifB=+∞0−∞ifB=+∞+∞ifB=−∞−∞A+B
13 2 5 12 ifbieq12d ⊢x=A∧y=B→ifx=+∞ify=−∞0+∞ifx=−∞ify=+∞0−∞ify=+∞+∞ify=−∞−∞x+y=ifA=+∞ifB=−∞0+∞ifA=−∞ifB=+∞0−∞ifB=+∞+∞ifB=−∞−∞A+B
14 df-xadd ⊢+𝑒=x∈ℝ*,y∈ℝ*⟼ifx=+∞ify=−∞0+∞ifx=−∞ify=+∞0−∞ify=+∞+∞ify=−∞−∞x+y
15 c0ex ⊢0∈V
16 pnfex ⊢+∞∈V
17 15 16 ifex ⊢ifB=−∞0+∞∈V
18 mnfxr ⊢−∞∈ℝ*
19 18 elexi ⊢−∞∈V
20 15 19 ifex ⊢ifB=+∞0−∞∈V
21 ovex ⊢A+B∈V
22 19 21 ifex ⊢ifB=−∞−∞A+B∈V
23 16 22 ifex ⊢ifB=+∞+∞ifB=−∞−∞A+B∈V
24 20 23 ifex ⊢ifA=−∞ifB=+∞0−∞ifB=+∞+∞ifB=−∞−∞A+B∈V
25 17 24 ifex ⊢ifA=+∞ifB=−∞0+∞ifA=−∞ifB=+∞0−∞ifB=+∞+∞ifB=−∞−∞A+B∈V
26 13 14 25 ovmpoa ⊢A∈ℝ*∧B∈ℝ*→A+𝑒B=ifA=+∞ifB=−∞0+∞ifA=−∞ifB=+∞0−∞ifB=+∞+∞ifB=−∞−∞A+B