xmulval

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

		Ref	Expression
	Assertion	xmulval	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to A \cdot_{𝑒} B = if ((A = 0 \lor B = 0), 0, if ((((0 < B \land A = +∞) \lor (B < 0 \land A = −∞)) \lor ((0 < A \land B = +∞) \lor (A < 0 \land B = −∞))), +∞, if ((((0 < B \land A = −∞) \lor (B < 0 \land A = +∞)) \lor ((0 < A \land B = −∞) \lor (A < 0 \land B = +∞))), −∞, A B)))$

Proof

Step	Hyp	Ref	Expression
1		simpl	$⊢ (x = A \land y = B) \to x = A$
2	1	eqeq1d	$⊢ (x = A \land y = B) \to (x = 0 \leftrightarrow A = 0)$
3		simpr	$⊢ (x = A \land y = B) \to y = B$
4	3	eqeq1d	$⊢ (x = A \land y = B) \to (y = 0 \leftrightarrow B = 0)$
5	2 4	orbi12d	$⊢ (x = A \land y = B) \to ((x = 0 \lor y = 0) \leftrightarrow (A = 0 \lor B = 0))$
6	3	breq2d	$⊢ (x = A \land y = B) \to (0 < y \leftrightarrow 0 < B)$
7	1	eqeq1d	$⊢ (x = A \land y = B) \to (x = +∞ \leftrightarrow A = +∞)$
8	6 7	anbi12d	$⊢ (x = A \land y = B) \to ((0 < y \land x = +∞) \leftrightarrow (0 < B \land A = +∞))$
9	3	breq1d	$⊢ (x = A \land y = B) \to (y < 0 \leftrightarrow B < 0)$
10	1	eqeq1d	$⊢ (x = A \land y = B) \to (x = −∞ \leftrightarrow A = −∞)$
11	9 10	anbi12d	$⊢ (x = A \land y = B) \to ((y < 0 \land x = −∞) \leftrightarrow (B < 0 \land A = −∞))$
12	8 11	orbi12d	$⊢ (x = A \land y = B) \to (((0 < y \land x = +∞) \lor (y < 0 \land x = −∞)) \leftrightarrow ((0 < B \land A = +∞) \lor (B < 0 \land A = −∞)))$
13	1	breq2d	$⊢ (x = A \land y = B) \to (0 < x \leftrightarrow 0 < A)$
14	3	eqeq1d	$⊢ (x = A \land y = B) \to (y = +∞ \leftrightarrow B = +∞)$
15	13 14	anbi12d	$⊢ (x = A \land y = B) \to ((0 < x \land y = +∞) \leftrightarrow (0 < A \land B = +∞))$
16	1	breq1d	$⊢ (x = A \land y = B) \to (x < 0 \leftrightarrow A < 0)$
17	3	eqeq1d	$⊢ (x = A \land y = B) \to (y = −∞ \leftrightarrow B = −∞)$
18	16 17	anbi12d	$⊢ (x = A \land y = B) \to ((x < 0 \land y = −∞) \leftrightarrow (A < 0 \land B = −∞))$
19	15 18	orbi12d	$⊢ (x = A \land y = B) \to (((0 < x \land y = +∞) \lor (x < 0 \land y = −∞)) \leftrightarrow ((0 < A \land B = +∞) \lor (A < 0 \land B = −∞)))$
20	12 19	orbi12d	$⊢ (x = A \land y = B) \to ((((0 < y \land x = +∞) \lor (y < 0 \land x = −∞)) \lor ((0 < x \land y = +∞) \lor (x < 0 \land y = −∞))) \leftrightarrow (((0 < B \land A = +∞) \lor (B < 0 \land A = −∞)) \lor ((0 < A \land B = +∞) \lor (A < 0 \land B = −∞))))$
21	6 10	anbi12d	$⊢ (x = A \land y = B) \to ((0 < y \land x = −∞) \leftrightarrow (0 < B \land A = −∞))$
22	9 7	anbi12d	$⊢ (x = A \land y = B) \to ((y < 0 \land x = +∞) \leftrightarrow (B < 0 \land A = +∞))$
23	21 22	orbi12d	$⊢ (x = A \land y = B) \to (((0 < y \land x = −∞) \lor (y < 0 \land x = +∞)) \leftrightarrow ((0 < B \land A = −∞) \lor (B < 0 \land A = +∞)))$
24	13 17	anbi12d	$⊢ (x = A \land y = B) \to ((0 < x \land y = −∞) \leftrightarrow (0 < A \land B = −∞))$
25	16 14	anbi12d	$⊢ (x = A \land y = B) \to ((x < 0 \land y = +∞) \leftrightarrow (A < 0 \land B = +∞))$
26	24 25	orbi12d	$⊢ (x = A \land y = B) \to (((0 < x \land y = −∞) \lor (x < 0 \land y = +∞)) \leftrightarrow ((0 < A \land B = −∞) \lor (A < 0 \land B = +∞)))$
27	23 26	orbi12d	$⊢ (x = A \land y = B) \to ((((0 < y \land x = −∞) \lor (y < 0 \land x = +∞)) \lor ((0 < x \land y = −∞) \lor (x < 0 \land y = +∞))) \leftrightarrow (((0 < B \land A = −∞) \lor (B < 0 \land A = +∞)) \lor ((0 < A \land B = −∞) \lor (A < 0 \land B = +∞))))$
28		oveq12	$⊢ (x = A \land y = B) \to x y = A B$
29	27 28	ifbieq2d	$⊢ (x = A \land y = B) \to if ((((0 < y \land x = −∞) \lor (y < 0 \land x = +∞)) \lor ((0 < x \land y = −∞) \lor (x < 0 \land y = +∞))), −∞, x y) = if ((((0 < B \land A = −∞) \lor (B < 0 \land A = +∞)) \lor ((0 < A \land B = −∞) \lor (A < 0 \land B = +∞))), −∞, A B)$
30	20 29	ifbieq2d	$⊢ (x = A \land y = B) \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)) = if ((((0 < B \land A = +∞) \lor (B < 0 \land A = −∞)) \lor ((0 < A \land B = +∞) \lor (A < 0 \land B = −∞))), +∞, if ((((0 < B \land A = −∞) \lor (B < 0 \land A = +∞)) \lor ((0 < A \land B = −∞) \lor (A < 0 \land B = +∞))), −∞, A B))$
31	5 30	ifbieq2d	$⊢ (x = A \land y = B) \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))) = if ((A = 0 \lor B = 0), 0, if ((((0 < B \land A = +∞) \lor (B < 0 \land A = −∞)) \lor ((0 < A \land B = +∞) \lor (A < 0 \land B = −∞))), +∞, if ((((0 < B \land A = −∞) \lor (B < 0 \land A = +∞)) \lor ((0 < A \land B = −∞) \lor (A < 0 \land B = +∞))), −∞, A B)))$
32		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))))$
33		c0ex	$⊢ 0 \in V$
34		pnfex	$⊢ +∞ \in V$
35		mnfxr	$⊢ −∞ \in ℝ^{*}$
36	35	elexi	$⊢ −∞ \in V$
37		ovex	$⊢ A B \in V$
38	36 37	ifex	$⊢ if ((((0 < B \land A = −∞) \lor (B < 0 \land A = +∞)) \lor ((0 < A \land B = −∞) \lor (A < 0 \land B = +∞))), −∞, A B) \in V$
39	34 38	ifex	$⊢ if ((((0 < B \land A = +∞) \lor (B < 0 \land A = −∞)) \lor ((0 < A \land B = +∞) \lor (A < 0 \land B = −∞))), +∞, if ((((0 < B \land A = −∞) \lor (B < 0 \land A = +∞)) \lor ((0 < A \land B = −∞) \lor (A < 0 \land B = +∞))), −∞, A B)) \in V$
40	33 39	ifex	$⊢ if ((A = 0 \lor B = 0), 0, if ((((0 < B \land A = +∞) \lor (B < 0 \land A = −∞)) \lor ((0 < A \land B = +∞) \lor (A < 0 \land B = −∞))), +∞, if ((((0 < B \land A = −∞) \lor (B < 0 \land A = +∞)) \lor ((0 < A \land B = −∞) \lor (A < 0 \land B = +∞))), −∞, A B))) \in V$
41	31 32 40	ovmpoa	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to A \cdot_{𝑒} B = if ((A = 0 \lor B = 0), 0, if ((((0 < B \land A = +∞) \lor (B < 0 \land A = −∞)) \lor ((0 < A \land B = +∞) \lor (A < 0 \land B = −∞))), +∞, if ((((0 < B \land A = −∞) \lor (B < 0 \land A = +∞)) \lor ((0 < A \land B = −∞) \lor (A < 0 \land B = +∞))), −∞, A B)))$

Metamath Proof Explorer

Theorem xmulval

Proof