df-xmul

Description: Define multiplication over extended real numbers. (Contributed by Mario Carneiro, 20-Aug-2015)

		Ref	Expression
	Assertion	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))))$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cxmu	$class \cdot_{𝑒}$
1		vx	$setvar x$
2		cxr	$class ℝ^{*}$
3		vy	$setvar y$
4	1	cv	$setvar x$
5		cc0	$class 0$
6	4 5	wceq	$wff x = 0$
7	3	cv	$setvar y$
8	7 5	wceq	$wff y = 0$
9	6 8	wo	$wff (x = 0 \lor y = 0)$
10		clt	$class <$
11	5 7 10	wbr	$wff 0 < y$
12		cpnf	$class +∞$
13	4 12	wceq	$wff x = +∞$
14	11 13	wa	$wff (0 < y \land x = +∞)$
15	7 5 10	wbr	$wff y < 0$
16		cmnf	$class −∞$
17	4 16	wceq	$wff x = −∞$
18	15 17	wa	$wff (y < 0 \land x = −∞)$
19	14 18	wo	$wff ((0 < y \land x = +∞) \lor (y < 0 \land x = −∞))$
20	5 4 10	wbr	$wff 0 < x$
21	7 12	wceq	$wff y = +∞$
22	20 21	wa	$wff (0 < x \land y = +∞)$
23	4 5 10	wbr	$wff x < 0$
24	7 16	wceq	$wff y = −∞$
25	23 24	wa	$wff (x < 0 \land y = −∞)$
26	22 25	wo	$wff ((0 < x \land y = +∞) \lor (x < 0 \land y = −∞))$
27	19 26	wo	$wff (((0 < y \land x = +∞) \lor (y < 0 \land x = −∞)) \lor ((0 < x \land y = +∞) \lor (x < 0 \land y = −∞)))$
28	11 17	wa	$wff (0 < y \land x = −∞)$
29	15 13	wa	$wff (y < 0 \land x = +∞)$
30	28 29	wo	$wff ((0 < y \land x = −∞) \lor (y < 0 \land x = +∞))$
31	20 24	wa	$wff (0 < x \land y = −∞)$
32	23 21	wa	$wff (x < 0 \land y = +∞)$
33	31 32	wo	$wff ((0 < x \land y = −∞) \lor (x < 0 \land y = +∞))$
34	30 33	wo	$wff (((0 < y \land x = −∞) \lor (y < 0 \land x = +∞)) \lor ((0 < x \land y = −∞) \lor (x < 0 \land y = +∞)))$
35		cmul	$class \times$
36	4 7 35	co	$class x y$
37	34 16 36	cif	$class if ((((0 < y \land x = −∞) \lor (y < 0 \land x = +∞)) \lor ((0 < x \land y = −∞) \lor (x < 0 \land y = +∞))), −∞, x y)$
38	27 12 37	cif	$class 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))$
39	9 5 38	cif	$class 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)))$
40	1 3 2 2 39	cmpo	$class (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))))$
41	0 40	wceq	$wff \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))))$

Metamath Proof Explorer

Definition df-xmul

Detailed syntax breakdown