xmulcom

Description: Extended real multiplication is commutative. (Contributed by Mario Carneiro, 20-Aug-2015)

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

Proof

Step	Hyp	Ref	Expression
1		xmullem	$⊢ ((((A \in ℝ^{} \land B \in ℝ^{}) \land \neg (A = 0 \lor B = 0)) \land \neg (((0 < B \land A = +∞) \lor (B < 0 \land A = −∞)) \lor ((0 < A \land B = +∞) \lor (A < 0 \land B = −∞)))) \land \neg (((0 < B \land A = −∞) \lor (B < 0 \land A = +∞)) \lor ((0 < A \land B = −∞) \lor (A < 0 \land B = +∞)))) \to A \in ℝ$
2	1	recnd	$⊢ ((((A \in ℝ^{} \land B \in ℝ^{}) \land \neg (A = 0 \lor B = 0)) \land \neg (((0 < B \land A = +∞) \lor (B < 0 \land A = −∞)) \lor ((0 < A \land B = +∞) \lor (A < 0 \land B = −∞)))) \land \neg (((0 < B \land A = −∞) \lor (B < 0 \land A = +∞)) \lor ((0 < A \land B = −∞) \lor (A < 0 \land B = +∞)))) \to A \in ℂ$
3		ancom	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \leftrightarrow (B \in ℝ^{} \land A \in ℝ^{})$
4		orcom	$⊢ (A = 0 \lor B = 0) \leftrightarrow (B = 0 \lor A = 0)$
5	4	notbii	$⊢ \neg (A = 0 \lor B = 0) \leftrightarrow \neg (B = 0 \lor A = 0)$
6	3 5	anbi12i	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land \neg (A = 0 \lor B = 0)) \leftrightarrow ((B \in ℝ^{} \land A \in ℝ^{}) \land \neg (B = 0 \lor A = 0))$
7		orcom	$⊢ (((0 < B \land A = +∞) \lor (B < 0 \land A = −∞)) \lor ((0 < A \land B = +∞) \lor (A < 0 \land B = −∞))) \leftrightarrow (((0 < A \land B = +∞) \lor (A < 0 \land B = −∞)) \lor ((0 < B \land A = +∞) \lor (B < 0 \land A = −∞)))$
8	7	notbii	$⊢ \neg (((0 < B \land A = +∞) \lor (B < 0 \land A = −∞)) \lor ((0 < A \land B = +∞) \lor (A < 0 \land B = −∞))) \leftrightarrow \neg (((0 < A \land B = +∞) \lor (A < 0 \land B = −∞)) \lor ((0 < B \land A = +∞) \lor (B < 0 \land A = −∞)))$
9	6 8	anbi12i	$⊢ (((A \in ℝ^{} \land B \in ℝ^{}) \land \neg (A = 0 \lor B = 0)) \land \neg (((0 < B \land A = +∞) \lor (B < 0 \land A = −∞)) \lor ((0 < A \land B = +∞) \lor (A < 0 \land B = −∞)))) \leftrightarrow (((B \in ℝ^{} \land A \in ℝ^{}) \land \neg (B = 0 \lor A = 0)) \land \neg (((0 < A \land B = +∞) \lor (A < 0 \land B = −∞)) \lor ((0 < B \land A = +∞) \lor (B < 0 \land A = −∞))))$
10		orcom	$⊢ (((0 < B \land A = −∞) \lor (B < 0 \land A = +∞)) \lor ((0 < A \land B = −∞) \lor (A < 0 \land B = +∞))) \leftrightarrow (((0 < A \land B = −∞) \lor (A < 0 \land B = +∞)) \lor ((0 < B \land A = −∞) \lor (B < 0 \land A = +∞)))$
11	10	notbii	$⊢ \neg (((0 < B \land A = −∞) \lor (B < 0 \land A = +∞)) \lor ((0 < A \land B = −∞) \lor (A < 0 \land B = +∞))) \leftrightarrow \neg (((0 < A \land B = −∞) \lor (A < 0 \land B = +∞)) \lor ((0 < B \land A = −∞) \lor (B < 0 \land A = +∞)))$
12		xmullem	$⊢ ((((B \in ℝ^{} \land A \in ℝ^{}) \land \neg (B = 0 \lor A = 0)) \land \neg (((0 < A \land B = +∞) \lor (A < 0 \land B = −∞)) \lor ((0 < B \land A = +∞) \lor (B < 0 \land A = −∞)))) \land \neg (((0 < A \land B = −∞) \lor (A < 0 \land B = +∞)) \lor ((0 < B \land A = −∞) \lor (B < 0 \land A = +∞)))) \to B \in ℝ$
13	9 11 12	syl2anb	$⊢ ((((A \in ℝ^{} \land B \in ℝ^{}) \land \neg (A = 0 \lor B = 0)) \land \neg (((0 < B \land A = +∞) \lor (B < 0 \land A = −∞)) \lor ((0 < A \land B = +∞) \lor (A < 0 \land B = −∞)))) \land \neg (((0 < B \land A = −∞) \lor (B < 0 \land A = +∞)) \lor ((0 < A \land B = −∞) \lor (A < 0 \land B = +∞)))) \to B \in ℝ$
14	13	recnd	$⊢ ((((A \in ℝ^{} \land B \in ℝ^{}) \land \neg (A = 0 \lor B = 0)) \land \neg (((0 < B \land A = +∞) \lor (B < 0 \land A = −∞)) \lor ((0 < A \land B = +∞) \lor (A < 0 \land B = −∞)))) \land \neg (((0 < B \land A = −∞) \lor (B < 0 \land A = +∞)) \lor ((0 < A \land B = −∞) \lor (A < 0 \land B = +∞)))) \to B \in ℂ$
15	2 14	mulcomd	$⊢ ((((A \in ℝ^{} \land B \in ℝ^{}) \land \neg (A = 0 \lor B = 0)) \land \neg (((0 < B \land A = +∞) \lor (B < 0 \land A = −∞)) \lor ((0 < A \land B = +∞) \lor (A < 0 \land B = −∞)))) \land \neg (((0 < B \land A = −∞) \lor (B < 0 \land A = +∞)) \lor ((0 < A \land B = −∞) \lor (A < 0 \land B = +∞)))) \to A B = B A$
16	15	ifeq2da	$⊢ (((A \in ℝ^{} \land B \in ℝ^{}) \land \neg (A = 0 \lor B = 0)) \land \neg (((0 < B \land A = +∞) \lor (B < 0 \land A = −∞)) \lor ((0 < A \land B = +∞) \lor (A < 0 \land B = −∞)))) \to 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 = +∞))), −∞, B A)$
17	10	a1i	$⊢ (((A \in ℝ^{} \land B \in ℝ^{}) \land \neg (A = 0 \lor B = 0)) \land \neg (((0 < B \land A = +∞) \lor (B < 0 \land A = −∞)) \lor ((0 < A \land B = +∞) \lor (A < 0 \land B = −∞)))) \to ((((0 < B \land A = −∞) \lor (B < 0 \land A = +∞)) \lor ((0 < A \land B = −∞) \lor (A < 0 \land B = +∞))) \leftrightarrow (((0 < A \land B = −∞) \lor (A < 0 \land B = +∞)) \lor ((0 < B \land A = −∞) \lor (B < 0 \land A = +∞))))$
18	17	ifbid	$⊢ (((A \in ℝ^{} \land B \in ℝ^{}) \land \neg (A = 0 \lor B = 0)) \land \neg (((0 < B \land A = +∞) \lor (B < 0 \land A = −∞)) \lor ((0 < A \land B = +∞) \lor (A < 0 \land B = −∞)))) \to if ((((0 < B \land A = −∞) \lor (B < 0 \land A = +∞)) \lor ((0 < A \land B = −∞) \lor (A < 0 \land B = +∞))), −∞, B A) = if ((((0 < A \land B = −∞) \lor (A < 0 \land B = +∞)) \lor ((0 < B \land A = −∞) \lor (B < 0 \land A = +∞))), −∞, B A)$
19	16 18	eqtrd	$⊢ (((A \in ℝ^{} \land B \in ℝ^{}) \land \neg (A = 0 \lor B = 0)) \land \neg (((0 < B \land A = +∞) \lor (B < 0 \land A = −∞)) \lor ((0 < A \land B = +∞) \lor (A < 0 \land B = −∞)))) \to if ((((0 < B \land A = −∞) \lor (B < 0 \land A = +∞)) \lor ((0 < A \land B = −∞) \lor (A < 0 \land B = +∞))), −∞, A B) = if ((((0 < A \land B = −∞) \lor (A < 0 \land B = +∞)) \lor ((0 < B \land A = −∞) \lor (B < 0 \land A = +∞))), −∞, B A)$
20	19	ifeq2da	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land \neg (A = 0 \lor B = 0)) \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 = −∞))), +∞, if ((((0 < A \land B = −∞) \lor (A < 0 \land B = +∞)) \lor ((0 < B \land A = −∞) \lor (B < 0 \land A = +∞))), −∞, B A))$
21	7	a1i	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land \neg (A = 0 \lor B = 0)) \to ((((0 < B \land A = +∞) \lor (B < 0 \land A = −∞)) \lor ((0 < A \land B = +∞) \lor (A < 0 \land B = −∞))) \leftrightarrow (((0 < A \land B = +∞) \lor (A < 0 \land B = −∞)) \lor ((0 < B \land A = +∞) \lor (B < 0 \land A = −∞))))$
22	21	ifbid	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land \neg (A = 0 \lor B = 0)) \to if ((((0 < B \land A = +∞) \lor (B < 0 \land A = −∞)) \lor ((0 < A \land B = +∞) \lor (A < 0 \land B = −∞))), +∞, if ((((0 < A \land B = −∞) \lor (A < 0 \land B = +∞)) \lor ((0 < B \land A = −∞) \lor (B < 0 \land A = +∞))), −∞, B A)) = if ((((0 < A \land B = +∞) \lor (A < 0 \land B = −∞)) \lor ((0 < B \land A = +∞) \lor (B < 0 \land A = −∞))), +∞, if ((((0 < A \land B = −∞) \lor (A < 0 \land B = +∞)) \lor ((0 < B \land A = −∞) \lor (B < 0 \land A = +∞))), −∞, B A))$
23	20 22	eqtrd	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land \neg (A = 0 \lor B = 0)) \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 < A \land B = +∞) \lor (A < 0 \land B = −∞)) \lor ((0 < B \land A = +∞) \lor (B < 0 \land A = −∞))), +∞, if ((((0 < A \land B = −∞) \lor (A < 0 \land B = +∞)) \lor ((0 < B \land A = −∞) \lor (B < 0 \land A = +∞))), −∞, B A))$
24	23	ifeq2da	$⊢ (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, if ((((0 < A \land B = +∞) \lor (A < 0 \land B = −∞)) \lor ((0 < B \land A = +∞) \lor (B < 0 \land A = −∞))), +∞, if ((((0 < A \land B = −∞) \lor (A < 0 \land B = +∞)) \lor ((0 < B \land A = −∞) \lor (B < 0 \land A = +∞))), −∞, B A)))$
25	4	a1i	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to ((A = 0 \lor B = 0) \leftrightarrow (B = 0 \lor A = 0))$
26	25	ifbid	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to if ((A = 0 \lor B = 0), 0, if ((((0 < A \land B = +∞) \lor (A < 0 \land B = −∞)) \lor ((0 < B \land A = +∞) \lor (B < 0 \land A = −∞))), +∞, if ((((0 < A \land B = −∞) \lor (A < 0 \land B = +∞)) \lor ((0 < B \land A = −∞) \lor (B < 0 \land A = +∞))), −∞, B A))) = if ((B = 0 \lor A = 0), 0, if ((((0 < A \land B = +∞) \lor (A < 0 \land B = −∞)) \lor ((0 < B \land A = +∞) \lor (B < 0 \land A = −∞))), +∞, if ((((0 < A \land B = −∞) \lor (A < 0 \land B = +∞)) \lor ((0 < B \land A = −∞) \lor (B < 0 \land A = +∞))), −∞, B A)))$
27	24 26	eqtrd	$⊢ (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 ((B = 0 \lor A = 0), 0, if ((((0 < A \land B = +∞) \lor (A < 0 \land B = −∞)) \lor ((0 < B \land A = +∞) \lor (B < 0 \land A = −∞))), +∞, if ((((0 < A \land B = −∞) \lor (A < 0 \land B = +∞)) \lor ((0 < B \land A = −∞) \lor (B < 0 \land A = +∞))), −∞, B A)))$
28		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)))$
29		xmulval	$⊢ (B \in ℝ^{} \land A \in ℝ^{}) \to B \cdot_{𝑒} A = if ((B = 0 \lor A = 0), 0, if ((((0 < A \land B = +∞) \lor (A < 0 \land B = −∞)) \lor ((0 < B \land A = +∞) \lor (B < 0 \land A = −∞))), +∞, if ((((0 < A \land B = −∞) \lor (A < 0 \land B = +∞)) \lor ((0 < B \land A = −∞) \lor (B < 0 \land A = +∞))), −∞, B A)))$
30	29	ancoms	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to B \cdot_{𝑒} A = if ((B = 0 \lor A = 0), 0, if ((((0 < A \land B = +∞) \lor (A < 0 \land B = −∞)) \lor ((0 < B \land A = +∞) \lor (B < 0 \land A = −∞))), +∞, if ((((0 < A \land B = −∞) \lor (A < 0 \land B = +∞)) \lor ((0 < B \land A = −∞) \lor (B < 0 \land A = +∞))), −∞, B A)))$
31	27 28 30	3eqtr4d	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to A \cdot_{𝑒} B = B \cdot_{𝑒} A$

Metamath Proof Explorer

Theorem xmulcom

Proof