xmulf

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

		Ref	Expression
	Assertion	xmulf	$⊢ \cdot_{𝑒} : ℝ^{} \times ℝ^{} ⟶ ℝ^{*}$

Proof

Step	Hyp	Ref	Expression
1		0xr	$⊢ 0 \in ℝ^{*}$
2	1	a1i	$⊢ ((x \in ℝ^{} \land y \in ℝ^{}) \land (x = 0 \lor y = 0)) \to 0 \in ℝ^{*}$
3		pnfxr	$⊢ +∞ \in ℝ^{*}$
4	3	a1i	$⊢ (((x \in ℝ^{} \land y \in ℝ^{}) \land \neg (x = 0 \lor y = 0)) \land (((0 < y \land x = +∞) \lor (y < 0 \land x = −∞)) \lor ((0 < x \land y = +∞) \lor (x < 0 \land y = −∞)))) \to +∞ \in ℝ^{*}$
5		mnfxr	$⊢ −∞ \in ℝ^{*}$
6	5	a1i	$⊢ ((((x \in ℝ^{} \land y \in ℝ^{}) \land \neg (x = 0 \lor y = 0)) \land \neg (((0 < y \land x = +∞) \lor (y < 0 \land x = −∞)) \lor ((0 < x \land y = +∞) \lor (x < 0 \land y = −∞)))) \land (((0 < y \land x = −∞) \lor (y < 0 \land x = +∞)) \lor ((0 < x \land y = −∞) \lor (x < 0 \land y = +∞)))) \to −∞ \in ℝ^{*}$
7		xmullem	$⊢ ((((x \in ℝ^{} \land y \in ℝ^{}) \land \neg (x = 0 \lor y = 0)) \land \neg (((0 < y \land x = +∞) \lor (y < 0 \land x = −∞)) \lor ((0 < x \land y = +∞) \lor (x < 0 \land y = −∞)))) \land \neg (((0 < y \land x = −∞) \lor (y < 0 \land x = +∞)) \lor ((0 < x \land y = −∞) \lor (x < 0 \land y = +∞)))) \to x \in ℝ$
8		ancom	$⊢ (x \in ℝ^{} \land y \in ℝ^{}) \leftrightarrow (y \in ℝ^{} \land x \in ℝ^{})$
9		orcom	$⊢ (x = 0 \lor y = 0) \leftrightarrow (y = 0 \lor x = 0)$
10	9	notbii	$⊢ \neg (x = 0 \lor y = 0) \leftrightarrow \neg (y = 0 \lor x = 0)$
11	8 10	anbi12i	$⊢ ((x \in ℝ^{} \land y \in ℝ^{}) \land \neg (x = 0 \lor y = 0)) \leftrightarrow ((y \in ℝ^{} \land x \in ℝ^{}) \land \neg (y = 0 \lor x = 0))$
12		orcom	$⊢ (((0 < y \land x = +∞) \lor (y < 0 \land x = −∞)) \lor ((0 < x \land y = +∞) \lor (x < 0 \land y = −∞))) \leftrightarrow (((0 < x \land y = +∞) \lor (x < 0 \land y = −∞)) \lor ((0 < y \land x = +∞) \lor (y < 0 \land x = −∞)))$
13	12	notbii	$⊢ \neg (((0 < y \land x = +∞) \lor (y < 0 \land x = −∞)) \lor ((0 < x \land y = +∞) \lor (x < 0 \land y = −∞))) \leftrightarrow \neg (((0 < x \land y = +∞) \lor (x < 0 \land y = −∞)) \lor ((0 < y \land x = +∞) \lor (y < 0 \land x = −∞)))$
14	11 13	anbi12i	$⊢ (((x \in ℝ^{} \land y \in ℝ^{}) \land \neg (x = 0 \lor y = 0)) \land \neg (((0 < y \land x = +∞) \lor (y < 0 \land x = −∞)) \lor ((0 < x \land y = +∞) \lor (x < 0 \land y = −∞)))) \leftrightarrow (((y \in ℝ^{} \land x \in ℝ^{}) \land \neg (y = 0 \lor x = 0)) \land \neg (((0 < x \land y = +∞) \lor (x < 0 \land y = −∞)) \lor ((0 < y \land x = +∞) \lor (y < 0 \land x = −∞))))$
15		orcom	$⊢ (((0 < y \land x = −∞) \lor (y < 0 \land x = +∞)) \lor ((0 < x \land y = −∞) \lor (x < 0 \land y = +∞))) \leftrightarrow (((0 < x \land y = −∞) \lor (x < 0 \land y = +∞)) \lor ((0 < y \land x = −∞) \lor (y < 0 \land x = +∞)))$
16	15	notbii	$⊢ \neg (((0 < y \land x = −∞) \lor (y < 0 \land x = +∞)) \lor ((0 < x \land y = −∞) \lor (x < 0 \land y = +∞))) \leftrightarrow \neg (((0 < x \land y = −∞) \lor (x < 0 \land y = +∞)) \lor ((0 < y \land x = −∞) \lor (y < 0 \land x = +∞)))$
17		xmullem	$⊢ ((((y \in ℝ^{} \land x \in ℝ^{}) \land \neg (y = 0 \lor x = 0)) \land \neg (((0 < x \land y = +∞) \lor (x < 0 \land y = −∞)) \lor ((0 < y \land x = +∞) \lor (y < 0 \land x = −∞)))) \land \neg (((0 < x \land y = −∞) \lor (x < 0 \land y = +∞)) \lor ((0 < y \land x = −∞) \lor (y < 0 \land x = +∞)))) \to y \in ℝ$
18	14 16 17	syl2anb	$⊢ ((((x \in ℝ^{} \land y \in ℝ^{}) \land \neg (x = 0 \lor y = 0)) \land \neg (((0 < y \land x = +∞) \lor (y < 0 \land x = −∞)) \lor ((0 < x \land y = +∞) \lor (x < 0 \land y = −∞)))) \land \neg (((0 < y \land x = −∞) \lor (y < 0 \land x = +∞)) \lor ((0 < x \land y = −∞) \lor (x < 0 \land y = +∞)))) \to y \in ℝ$
19	7 18	remulcld	$⊢ ((((x \in ℝ^{} \land y \in ℝ^{}) \land \neg (x = 0 \lor y = 0)) \land \neg (((0 < y \land x = +∞) \lor (y < 0 \land x = −∞)) \lor ((0 < x \land y = +∞) \lor (x < 0 \land y = −∞)))) \land \neg (((0 < y \land x = −∞) \lor (y < 0 \land x = +∞)) \lor ((0 < x \land y = −∞) \lor (x < 0 \land y = +∞)))) \to x y \in ℝ$
20	19	rexrd	$⊢ ((((x \in ℝ^{} \land y \in ℝ^{}) \land \neg (x = 0 \lor y = 0)) \land \neg (((0 < y \land x = +∞) \lor (y < 0 \land x = −∞)) \lor ((0 < x \land y = +∞) \lor (x < 0 \land y = −∞)))) \land \neg (((0 < y \land x = −∞) \lor (y < 0 \land x = +∞)) \lor ((0 < x \land y = −∞) \lor (x < 0 \land y = +∞)))) \to x y \in ℝ^{*}$
21	6 20	ifclda	$⊢ (((x \in ℝ^{} \land y \in ℝ^{}) \land \neg (x = 0 \lor y = 0)) \land \neg (((0 < y \land x = +∞) \lor (y < 0 \land x = −∞)) \lor ((0 < x \land y = +∞) \lor (x < 0 \land y = −∞)))) \to if ((((0 < y \land x = −∞) \lor (y < 0 \land x = +∞)) \lor ((0 < x \land y = −∞) \lor (x < 0 \land y = +∞))), −∞, x y) \in ℝ^{*}$
22	4 21	ifclda	$⊢ ((x \in ℝ^{} \land y \in ℝ^{}) \land \neg (x = 0 \lor y = 0)) \to if ((((0 < y \land x = +∞) \lor (y < 0 \land x = −∞)) \lor ((0 < x \land y = +∞) \lor (x < 0 \land y = −∞))), +∞, if ((((0 < y \land x = −∞) \lor (y < 0 \land x = +∞)) \lor ((0 < x \land y = −∞) \lor (x < 0 \land y = +∞))), −∞, x y)) \in ℝ^{*}$
23	2 22	ifclda	$⊢ (x \in ℝ^{} \land y \in ℝ^{}) \to if ((x = 0 \lor y = 0), 0, if ((((0 < y \land x = +∞) \lor (y < 0 \land x = −∞)) \lor ((0 < x \land y = +∞) \lor (x < 0 \land y = −∞))), +∞, if ((((0 < y \land x = −∞) \lor (y < 0 \land x = +∞)) \lor ((0 < x \land y = −∞) \lor (x < 0 \land y = +∞))), −∞, x y))) \in ℝ^{*}$
24	23	rgen2	$⊢ \forall x \in ℝ^{} \forall y \in ℝ^{} if ((x = 0 \lor y = 0), 0, if ((((0 < y \land x = +∞) \lor (y < 0 \land x = −∞)) \lor ((0 < x \land y = +∞) \lor (x < 0 \land y = −∞))), +∞, if ((((0 < y \land x = −∞) \lor (y < 0 \land x = +∞)) \lor ((0 < x \land y = −∞) \lor (x < 0 \land y = +∞))), −∞, x y))) \in ℝ^{*}$
25		df-xmul	$⊢ \cdot_{𝑒} = (x \in ℝ^{}, y \in ℝ^{} ⟼ if ((x = 0 \lor y = 0), 0, if ((((0 < y \land x = +∞) \lor (y < 0 \land x = −∞)) \lor ((0 < x \land y = +∞) \lor (x < 0 \land y = −∞))), +∞, if ((((0 < y \land x = −∞) \lor (y < 0 \land x = +∞)) \lor ((0 < x \land y = −∞) \lor (x < 0 \land y = +∞))), −∞, x y))))$
26	25	fmpo	$⊢ \forall x \in ℝ^{} \forall y \in ℝ^{} if ((x = 0 \lor y = 0), 0, if ((((0 < y \land x = +∞) \lor (y < 0 \land x = −∞)) \lor ((0 < x \land y = +∞) \lor (x < 0 \land y = −∞))), +∞, if ((((0 < y \land x = −∞) \lor (y < 0 \land x = +∞)) \lor ((0 < x \land y = −∞) \lor (x < 0 \land y = +∞))), −∞, x y))) \in ℝ^{} \leftrightarrow \cdot_{𝑒} : ℝ^{} \times ℝ^{} ⟶ ℝ^{}$
27	24 26	mpbi	$⊢ \cdot_{𝑒} : ℝ^{} \times ℝ^{} ⟶ ℝ^{*}$

Metamath Proof Explorer

Theorem xmulf

Proof