rexmul

Description: The extended real multiplication when both arguments are real. (Contributed by Mario Carneiro, 20-Aug-2015)

		Ref	Expression
	Assertion	rexmul	$⊢ (A \in ℝ \land B \in ℝ) \to A \cdot_{𝑒} B = A B$

Proof

Step	Hyp	Ref	Expression
1		renepnf	$⊢ A \in ℝ \to A \neq +∞$
2	1	adantr	$⊢ (A \in ℝ \land B \in ℝ) \to A \neq +∞$
3	2	necon2bi	$⊢ A = +∞ \to \neg (A \in ℝ \land B \in ℝ)$
4	3	adantl	$⊢ (0 < B \land A = +∞) \to \neg (A \in ℝ \land B \in ℝ)$
5		renemnf	$⊢ A \in ℝ \to A \neq −∞$
6	5	adantr	$⊢ (A \in ℝ \land B \in ℝ) \to A \neq −∞$
7	6	necon2bi	$⊢ A = −∞ \to \neg (A \in ℝ \land B \in ℝ)$
8	7	adantl	$⊢ (B < 0 \land A = −∞) \to \neg (A \in ℝ \land B \in ℝ)$
9	4 8	jaoi	$⊢ ((0 < B \land A = +∞) \lor (B < 0 \land A = −∞)) \to \neg (A \in ℝ \land B \in ℝ)$
10		renepnf	$⊢ B \in ℝ \to B \neq +∞$
11	10	adantl	$⊢ (A \in ℝ \land B \in ℝ) \to B \neq +∞$
12	11	necon2bi	$⊢ B = +∞ \to \neg (A \in ℝ \land B \in ℝ)$
13	12	adantl	$⊢ (0 < A \land B = +∞) \to \neg (A \in ℝ \land B \in ℝ)$
14		renemnf	$⊢ B \in ℝ \to B \neq −∞$
15	14	adantl	$⊢ (A \in ℝ \land B \in ℝ) \to B \neq −∞$
16	15	necon2bi	$⊢ B = −∞ \to \neg (A \in ℝ \land B \in ℝ)$
17	16	adantl	$⊢ (A < 0 \land B = −∞) \to \neg (A \in ℝ \land B \in ℝ)$
18	13 17	jaoi	$⊢ ((0 < A \land B = +∞) \lor (A < 0 \land B = −∞)) \to \neg (A \in ℝ \land B \in ℝ)$
19	9 18	jaoi	$⊢ (((0 < B \land A = +∞) \lor (B < 0 \land A = −∞)) \lor ((0 < A \land B = +∞) \lor (A < 0 \land B = −∞))) \to \neg (A \in ℝ \land B \in ℝ)$
20	19	con2i	$⊢ (A \in ℝ \land B \in ℝ) \to \neg (((0 < B \land A = +∞) \lor (B < 0 \land A = −∞)) \lor ((0 < A \land B = +∞) \lor (A < 0 \land B = −∞)))$
21	20	iffalsed	$⊢ (A \in ℝ \land B \in ℝ) \to 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)) = if ((((0 < B \land A = −∞) \lor (B < 0 \land A = +∞)) \lor ((0 < A \land B = −∞) \lor (A < 0 \land B = +∞))), −∞, A B)$
22	7	adantl	$⊢ (0 < B \land A = −∞) \to \neg (A \in ℝ \land B \in ℝ)$
23	3	adantl	$⊢ (B < 0 \land A = +∞) \to \neg (A \in ℝ \land B \in ℝ)$
24	22 23	jaoi	$⊢ ((0 < B \land A = −∞) \lor (B < 0 \land A = +∞)) \to \neg (A \in ℝ \land B \in ℝ)$
25	16	adantl	$⊢ (0 < A \land B = −∞) \to \neg (A \in ℝ \land B \in ℝ)$
26	12	adantl	$⊢ (A < 0 \land B = +∞) \to \neg (A \in ℝ \land B \in ℝ)$
27	25 26	jaoi	$⊢ ((0 < A \land B = −∞) \lor (A < 0 \land B = +∞)) \to \neg (A \in ℝ \land B \in ℝ)$
28	24 27	jaoi	$⊢ (((0 < B \land A = −∞) \lor (B < 0 \land A = +∞)) \lor ((0 < A \land B = −∞) \lor (A < 0 \land B = +∞))) \to \neg (A \in ℝ \land B \in ℝ)$
29	28	con2i	$⊢ (A \in ℝ \land B \in ℝ) \to \neg (((0 < B \land A = −∞) \lor (B < 0 \land A = +∞)) \lor ((0 < A \land B = −∞) \lor (A < 0 \land B = +∞)))$
30	29	iffalsed	$⊢ (A \in ℝ \land B \in ℝ) \to if ((((0 < B \land A = −∞) \lor (B < 0 \land A = +∞)) \lor ((0 < A \land B = −∞) \lor (A < 0 \land B = +∞))), −∞, A B) = A B$
31	21 30	eqtrd	$⊢ (A \in ℝ \land B \in ℝ) \to 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)) = A B$
32	31	ifeq2d	$⊢ (A \in ℝ \land B \in ℝ) \to 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))) = if ((A = 0 \lor B = 0), 0, A B)$
33		rexr	$⊢ A \in ℝ \to A \in ℝ^{*}$
34		rexr	$⊢ B \in ℝ \to B \in ℝ^{*}$
35		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)))$
36	33 34 35	syl2an	$⊢ (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)))$
37		ifid	$⊢ if ((A = 0 \lor B = 0), A B, A B) = A B$
38		oveq1	$⊢ A = 0 \to A B = 0 \cdot B$
39		mul02lem2	$⊢ B \in ℝ \to 0 \cdot B = 0$
40	39	adantl	$⊢ (A \in ℝ \land B \in ℝ) \to 0 \cdot B = 0$
41	38 40	sylan9eqr	$⊢ ((A \in ℝ \land B \in ℝ) \land A = 0) \to A B = 0$
42		oveq2	$⊢ B = 0 \to A B = A \cdot 0$
43		recn	$⊢ A \in ℝ \to A \in ℂ$
44	43	mul01d	$⊢ A \in ℝ \to A \cdot 0 = 0$
45	44	adantr	$⊢ (A \in ℝ \land B \in ℝ) \to A \cdot 0 = 0$
46	42 45	sylan9eqr	$⊢ ((A \in ℝ \land B \in ℝ) \land B = 0) \to A B = 0$
47	41 46	jaodan	$⊢ ((A \in ℝ \land B \in ℝ) \land (A = 0 \lor B = 0)) \to A B = 0$
48	47	ifeq1da	$⊢ (A \in ℝ \land B \in ℝ) \to if ((A = 0 \lor B = 0), A B, A B) = if ((A = 0 \lor B = 0), 0, A B)$
49	37 48	syl5eqr	$⊢ (A \in ℝ \land B \in ℝ) \to A B = if ((A = 0 \lor B = 0), 0, A B)$
50	32 36 49	3eqtr4d	$⊢ (A \in ℝ \land B \in ℝ) \to A \cdot_{𝑒} B = A B$

Metamath Proof Explorer

Theorem rexmul

Proof