xaddf

Description: The extended real addition operation is closed in extended reals. (Contributed by Mario Carneiro, 21-Aug-2015)

		Ref	Expression
	Assertion	xaddf	$⊢ +_{𝑒} : ℝ^{} \times ℝ^{} ⟶ ℝ^{*}$

Proof

Step	Hyp	Ref	Expression
1		0xr	$⊢ 0 \in ℝ^{*}$
2		pnfxr	$⊢ +∞ \in ℝ^{*}$
3	1 2	ifcli	$⊢ if (y = −∞, 0, +∞) \in ℝ^{*}$
4	3	a1i	$⊢ ((x \in ℝ^{} \land y \in ℝ^{}) \land x = +∞) \to if (y = −∞, 0, +∞) \in ℝ^{*}$
5		mnfxr	$⊢ −∞ \in ℝ^{*}$
6	1 5	ifcli	$⊢ if (y = +∞, 0, −∞) \in ℝ^{*}$
7	6	a1i	$⊢ (((x \in ℝ^{} \land y \in ℝ^{}) \land \neg x = +∞) \land x = −∞) \to if (y = +∞, 0, −∞) \in ℝ^{*}$
8	2	a1i	$⊢ (((x \in ℝ^{} \land (\neg x = +∞ \land \neg x = −∞)) \land y \in ℝ^{}) \land y = +∞) \to +∞ \in ℝ^{*}$
9	5	a1i	$⊢ ((((x \in ℝ^{} \land (\neg x = +∞ \land \neg x = −∞)) \land y \in ℝ^{}) \land \neg y = +∞) \land y = −∞) \to −∞ \in ℝ^{*}$
10		ioran	$⊢ \neg (x = +∞ \lor x = −∞) \leftrightarrow (\neg x = +∞ \land \neg x = −∞)$
11		elxr	$⊢ x \in ℝ^{*} \leftrightarrow (x \in ℝ \lor x = +∞ \lor x = −∞)$
12		3orass	$⊢ (x \in ℝ \lor x = +∞ \lor x = −∞) \leftrightarrow (x \in ℝ \lor (x = +∞ \lor x = −∞))$
13	11 12	sylbb	$⊢ x \in ℝ^{*} \to (x \in ℝ \lor (x = +∞ \lor x = −∞))$
14	13	ord	$⊢ x \in ℝ^{*} \to (\neg x \in ℝ \to (x = +∞ \lor x = −∞))$
15	14	con1d	$⊢ x \in ℝ^{*} \to (\neg (x = +∞ \lor x = −∞) \to x \in ℝ)$
16	15	imp	$⊢ (x \in ℝ^{*} \land \neg (x = +∞ \lor x = −∞)) \to x \in ℝ$
17	10 16	sylan2br	$⊢ (x \in ℝ^{*} \land (\neg x = +∞ \land \neg x = −∞)) \to x \in ℝ$
18		ioran	$⊢ \neg (y = +∞ \lor y = −∞) \leftrightarrow (\neg y = +∞ \land \neg y = −∞)$
19		elxr	$⊢ y \in ℝ^{*} \leftrightarrow (y \in ℝ \lor y = +∞ \lor y = −∞)$
20		3orass	$⊢ (y \in ℝ \lor y = +∞ \lor y = −∞) \leftrightarrow (y \in ℝ \lor (y = +∞ \lor y = −∞))$
21	19 20	sylbb	$⊢ y \in ℝ^{*} \to (y \in ℝ \lor (y = +∞ \lor y = −∞))$
22	21	ord	$⊢ y \in ℝ^{*} \to (\neg y \in ℝ \to (y = +∞ \lor y = −∞))$
23	22	con1d	$⊢ y \in ℝ^{*} \to (\neg (y = +∞ \lor y = −∞) \to y \in ℝ)$
24	23	imp	$⊢ (y \in ℝ^{*} \land \neg (y = +∞ \lor y = −∞)) \to y \in ℝ$
25	18 24	sylan2br	$⊢ (y \in ℝ^{*} \land (\neg y = +∞ \land \neg y = −∞)) \to y \in ℝ$
26		readdcl	$⊢ (x \in ℝ \land y \in ℝ) \to x + y \in ℝ$
27	17 25 26	syl2an	$⊢ ((x \in ℝ^{} \land (\neg x = +∞ \land \neg x = −∞)) \land (y \in ℝ^{} \land (\neg y = +∞ \land \neg y = −∞))) \to x + y \in ℝ$
28	27	rexrd	$⊢ ((x \in ℝ^{} \land (\neg x = +∞ \land \neg x = −∞)) \land (y \in ℝ^{} \land (\neg y = +∞ \land \neg y = −∞))) \to x + y \in ℝ^{*}$
29	28	anassrs	$⊢ (((x \in ℝ^{} \land (\neg x = +∞ \land \neg x = −∞)) \land y \in ℝ^{}) \land (\neg y = +∞ \land \neg y = −∞)) \to x + y \in ℝ^{*}$
30	29	anassrs	$⊢ ((((x \in ℝ^{} \land (\neg x = +∞ \land \neg x = −∞)) \land y \in ℝ^{}) \land \neg y = +∞) \land \neg y = −∞) \to x + y \in ℝ^{*}$
31	9 30	ifclda	$⊢ (((x \in ℝ^{} \land (\neg x = +∞ \land \neg x = −∞)) \land y \in ℝ^{}) \land \neg y = +∞) \to if (y = −∞, −∞, x + y) \in ℝ^{*}$
32	8 31	ifclda	$⊢ ((x \in ℝ^{} \land (\neg x = +∞ \land \neg x = −∞)) \land y \in ℝ^{}) \to if (y = +∞, +∞, if (y = −∞, −∞, x + y)) \in ℝ^{*}$
33	32	an32s	$⊢ ((x \in ℝ^{} \land y \in ℝ^{}) \land (\neg x = +∞ \land \neg x = −∞)) \to if (y = +∞, +∞, if (y = −∞, −∞, x + y)) \in ℝ^{*}$
34	33	anassrs	$⊢ (((x \in ℝ^{} \land y \in ℝ^{}) \land \neg x = +∞) \land \neg x = −∞) \to if (y = +∞, +∞, if (y = −∞, −∞, x + y)) \in ℝ^{*}$
35	7 34	ifclda	$⊢ ((x \in ℝ^{} \land y \in ℝ^{}) \land \neg x = +∞) \to if (x = −∞, if (y = +∞, 0, −∞), if (y = +∞, +∞, if (y = −∞, −∞, x + y))) \in ℝ^{*}$
36	4 35	ifclda	$⊢ (x \in ℝ^{} \land y \in ℝ^{}) \to if (x = +∞, if (y = −∞, 0, +∞), if (x = −∞, if (y = +∞, 0, −∞), if (y = +∞, +∞, if (y = −∞, −∞, x + y)))) \in ℝ^{*}$
37	36	rgen2	$⊢ \forall x \in ℝ^{} \forall y \in ℝ^{} if (x = +∞, if (y = −∞, 0, +∞), if (x = −∞, if (y = +∞, 0, −∞), if (y = +∞, +∞, if (y = −∞, −∞, x + y)))) \in ℝ^{*}$
38		df-xadd	$⊢ +_{𝑒} = (x \in ℝ^{}, y \in ℝ^{} ⟼ if (x = +∞, if (y = −∞, 0, +∞), if (x = −∞, if (y = +∞, 0, −∞), if (y = +∞, +∞, if (y = −∞, −∞, x + y)))))$
39	38	fmpo	$⊢ \forall x \in ℝ^{} \forall y \in ℝ^{} if (x = +∞, if (y = −∞, 0, +∞), if (x = −∞, if (y = +∞, 0, −∞), if (y = +∞, +∞, if (y = −∞, −∞, x + y)))) \in ℝ^{} \leftrightarrow +_{𝑒} : ℝ^{} \times ℝ^{} ⟶ ℝ^{}$
40	37 39	mpbi	$⊢ +_{𝑒} : ℝ^{} \times ℝ^{} ⟶ ℝ^{*}$

Metamath Proof Explorer

Theorem xaddf

Proof