# Metamath Proof Explorer

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

Ref Expression
Assertion xaddval ${⊢}\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)\to {A}{+}_{𝑒}{B}=if\left({A}=\mathrm{+\infty },if\left({B}=\mathrm{-\infty },0,\mathrm{+\infty }\right),if\left({A}=\mathrm{-\infty },if\left({B}=\mathrm{+\infty },0,\mathrm{-\infty }\right),if\left({B}=\mathrm{+\infty },\mathrm{+\infty },if\left({B}=\mathrm{-\infty },\mathrm{-\infty },{A}+{B}\right)\right)\right)\right)$

### Proof

Step Hyp Ref Expression
1 simpl ${⊢}\left({x}={A}\wedge {y}={B}\right)\to {x}={A}$
2 1 eqeq1d ${⊢}\left({x}={A}\wedge {y}={B}\right)\to \left({x}=\mathrm{+\infty }↔{A}=\mathrm{+\infty }\right)$
3 simpr ${⊢}\left({x}={A}\wedge {y}={B}\right)\to {y}={B}$
4 3 eqeq1d ${⊢}\left({x}={A}\wedge {y}={B}\right)\to \left({y}=\mathrm{-\infty }↔{B}=\mathrm{-\infty }\right)$
5 4 ifbid ${⊢}\left({x}={A}\wedge {y}={B}\right)\to if\left({y}=\mathrm{-\infty },0,\mathrm{+\infty }\right)=if\left({B}=\mathrm{-\infty },0,\mathrm{+\infty }\right)$
6 1 eqeq1d ${⊢}\left({x}={A}\wedge {y}={B}\right)\to \left({x}=\mathrm{-\infty }↔{A}=\mathrm{-\infty }\right)$
7 3 eqeq1d ${⊢}\left({x}={A}\wedge {y}={B}\right)\to \left({y}=\mathrm{+\infty }↔{B}=\mathrm{+\infty }\right)$
8 7 ifbid ${⊢}\left({x}={A}\wedge {y}={B}\right)\to if\left({y}=\mathrm{+\infty },0,\mathrm{-\infty }\right)=if\left({B}=\mathrm{+\infty },0,\mathrm{-\infty }\right)$
9 oveq12 ${⊢}\left({x}={A}\wedge {y}={B}\right)\to {x}+{y}={A}+{B}$
10 4 9 ifbieq2d ${⊢}\left({x}={A}\wedge {y}={B}\right)\to if\left({y}=\mathrm{-\infty },\mathrm{-\infty },{x}+{y}\right)=if\left({B}=\mathrm{-\infty },\mathrm{-\infty },{A}+{B}\right)$
11 7 10 ifbieq2d ${⊢}\left({x}={A}\wedge {y}={B}\right)\to if\left({y}=\mathrm{+\infty },\mathrm{+\infty },if\left({y}=\mathrm{-\infty },\mathrm{-\infty },{x}+{y}\right)\right)=if\left({B}=\mathrm{+\infty },\mathrm{+\infty },if\left({B}=\mathrm{-\infty },\mathrm{-\infty },{A}+{B}\right)\right)$
12 6 8 11 ifbieq12d ${⊢}\left({x}={A}\wedge {y}={B}\right)\to if\left({x}=\mathrm{-\infty },if\left({y}=\mathrm{+\infty },0,\mathrm{-\infty }\right),if\left({y}=\mathrm{+\infty },\mathrm{+\infty },if\left({y}=\mathrm{-\infty },\mathrm{-\infty },{x}+{y}\right)\right)\right)=if\left({A}=\mathrm{-\infty },if\left({B}=\mathrm{+\infty },0,\mathrm{-\infty }\right),if\left({B}=\mathrm{+\infty },\mathrm{+\infty },if\left({B}=\mathrm{-\infty },\mathrm{-\infty },{A}+{B}\right)\right)\right)$
13 2 5 12 ifbieq12d ${⊢}\left({x}={A}\wedge {y}={B}\right)\to if\left({x}=\mathrm{+\infty },if\left({y}=\mathrm{-\infty },0,\mathrm{+\infty }\right),if\left({x}=\mathrm{-\infty },if\left({y}=\mathrm{+\infty },0,\mathrm{-\infty }\right),if\left({y}=\mathrm{+\infty },\mathrm{+\infty },if\left({y}=\mathrm{-\infty },\mathrm{-\infty },{x}+{y}\right)\right)\right)\right)=if\left({A}=\mathrm{+\infty },if\left({B}=\mathrm{-\infty },0,\mathrm{+\infty }\right),if\left({A}=\mathrm{-\infty },if\left({B}=\mathrm{+\infty },0,\mathrm{-\infty }\right),if\left({B}=\mathrm{+\infty },\mathrm{+\infty },if\left({B}=\mathrm{-\infty },\mathrm{-\infty },{A}+{B}\right)\right)\right)\right)$
14 df-xadd ${⊢}{+}_{𝑒}=\left({x}\in {ℝ}^{*},{y}\in {ℝ}^{*}⟼if\left({x}=\mathrm{+\infty },if\left({y}=\mathrm{-\infty },0,\mathrm{+\infty }\right),if\left({x}=\mathrm{-\infty },if\left({y}=\mathrm{+\infty },0,\mathrm{-\infty }\right),if\left({y}=\mathrm{+\infty },\mathrm{+\infty },if\left({y}=\mathrm{-\infty },\mathrm{-\infty },{x}+{y}\right)\right)\right)\right)\right)$
15 c0ex ${⊢}0\in \mathrm{V}$
16 pnfex ${⊢}\mathrm{+\infty }\in \mathrm{V}$
17 15 16 ifex ${⊢}if\left({B}=\mathrm{-\infty },0,\mathrm{+\infty }\right)\in \mathrm{V}$
18 mnfxr ${⊢}\mathrm{-\infty }\in {ℝ}^{*}$
19 18 elexi ${⊢}\mathrm{-\infty }\in \mathrm{V}$
20 15 19 ifex ${⊢}if\left({B}=\mathrm{+\infty },0,\mathrm{-\infty }\right)\in \mathrm{V}$
21 ovex ${⊢}{A}+{B}\in \mathrm{V}$
22 19 21 ifex ${⊢}if\left({B}=\mathrm{-\infty },\mathrm{-\infty },{A}+{B}\right)\in \mathrm{V}$
23 16 22 ifex ${⊢}if\left({B}=\mathrm{+\infty },\mathrm{+\infty },if\left({B}=\mathrm{-\infty },\mathrm{-\infty },{A}+{B}\right)\right)\in \mathrm{V}$
24 20 23 ifex ${⊢}if\left({A}=\mathrm{-\infty },if\left({B}=\mathrm{+\infty },0,\mathrm{-\infty }\right),if\left({B}=\mathrm{+\infty },\mathrm{+\infty },if\left({B}=\mathrm{-\infty },\mathrm{-\infty },{A}+{B}\right)\right)\right)\in \mathrm{V}$
25 17 24 ifex ${⊢}if\left({A}=\mathrm{+\infty },if\left({B}=\mathrm{-\infty },0,\mathrm{+\infty }\right),if\left({A}=\mathrm{-\infty },if\left({B}=\mathrm{+\infty },0,\mathrm{-\infty }\right),if\left({B}=\mathrm{+\infty },\mathrm{+\infty },if\left({B}=\mathrm{-\infty },\mathrm{-\infty },{A}+{B}\right)\right)\right)\right)\in \mathrm{V}$
26 13 14 25 ovmpoa ${⊢}\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)\to {A}{+}_{𝑒}{B}=if\left({A}=\mathrm{+\infty },if\left({B}=\mathrm{-\infty },0,\mathrm{+\infty }\right),if\left({A}=\mathrm{-\infty },if\left({B}=\mathrm{+\infty },0,\mathrm{-\infty }\right),if\left({B}=\mathrm{+\infty },\mathrm{+\infty },if\left({B}=\mathrm{-\infty },\mathrm{-\infty },{A}+{B}\right)\right)\right)\right)$