xmulneg1

Description: Extended real version of mulneg1 . (Contributed by Mario Carneiro, 20-Aug-2015)

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

Proof

Step	Hyp	Ref	Expression
1		xneg0	$⊢ - 0 = 0$
2	1	eqeq2i	$⊢ - A = - 0 \leftrightarrow - A = 0$
3		0xr	$⊢ 0 \in ℝ^{*}$
4		xneg11	$⊢ (A \in ℝ^{} \land 0 \in ℝ^{}) \to (- A = - 0 \leftrightarrow A = 0)$
5	3 4	mpan2	$⊢ A \in ℝ^{*} \to (- A = - 0 \leftrightarrow A = 0)$
6	2 5	bitr3id	$⊢ A \in ℝ^{*} \to (- A = 0 \leftrightarrow A = 0)$
7	6	adantr	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to (- A = 0 \leftrightarrow A = 0)$
8	7	orbi1d	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to ((- A = 0 \lor B = 0) \leftrightarrow (A = 0 \lor B = 0))$
9	8	ifbid	$⊢ (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 < 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)))$
10		xnegpnf	$⊢ - +∞ = −∞$
11	10	eqeq2i	$⊢ - A = - +∞ \leftrightarrow - A = −∞$
12		simpll	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land \neg (A = 0 \lor B = 0)) \to A \in ℝ^{*}$
13		pnfxr	$⊢ +∞ \in ℝ^{*}$
14		xneg11	$⊢ (A \in ℝ^{} \land +∞ \in ℝ^{}) \to (- A = - +∞ \leftrightarrow A = +∞)$
15	12 13 14	sylancl	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land \neg (A = 0 \lor B = 0)) \to (- A = - +∞ \leftrightarrow A = +∞)$
16	11 15	bitr3id	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land \neg (A = 0 \lor B = 0)) \to (- A = −∞ \leftrightarrow A = +∞)$
17	16	anbi2d	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land \neg (A = 0 \lor B = 0)) \to ((0 < B \land - A = −∞) \leftrightarrow (0 < B \land A = +∞))$
18		xnegmnf	$⊢ - −∞ = +∞$
19	18	eqeq2i	$⊢ - A = - −∞ \leftrightarrow - A = +∞$
20		mnfxr	$⊢ −∞ \in ℝ^{*}$
21		xneg11	$⊢ (A \in ℝ^{} \land −∞ \in ℝ^{}) \to (- A = - −∞ \leftrightarrow A = −∞)$
22	12 20 21	sylancl	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land \neg (A = 0 \lor B = 0)) \to (- A = - −∞ \leftrightarrow A = −∞)$
23	19 22	bitr3id	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land \neg (A = 0 \lor B = 0)) \to (- A = +∞ \leftrightarrow A = −∞)$
24	23	anbi2d	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land \neg (A = 0 \lor B = 0)) \to ((B < 0 \land - A = +∞) \leftrightarrow (B < 0 \land A = −∞))$
25	17 24	orbi12d	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land \neg (A = 0 \lor B = 0)) \to (((0 < B \land - A = −∞) \lor (B < 0 \land - A = +∞)) \leftrightarrow ((0 < B \land A = +∞) \lor (B < 0 \land A = −∞)))$
26		xlt0neg1	$⊢ A \in ℝ^{*} \to (A < 0 \leftrightarrow 0 < - A)$
27	26	ad2antrr	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land \neg (A = 0 \lor B = 0)) \to (A < 0 \leftrightarrow 0 < - A)$
28	27	bicomd	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land \neg (A = 0 \lor B = 0)) \to (0 < - A \leftrightarrow A < 0)$
29	28	anbi1d	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land \neg (A = 0 \lor B = 0)) \to ((0 < - A \land B = −∞) \leftrightarrow (A < 0 \land B = −∞))$
30		xlt0neg2	$⊢ A \in ℝ^{*} \to (0 < A \leftrightarrow - A < 0)$
31	30	ad2antrr	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land \neg (A = 0 \lor B = 0)) \to (0 < A \leftrightarrow - A < 0)$
32	31	bicomd	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land \neg (A = 0 \lor B = 0)) \to (- A < 0 \leftrightarrow 0 < A)$
33	32	anbi1d	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land \neg (A = 0 \lor B = 0)) \to ((- A < 0 \land B = +∞) \leftrightarrow (0 < A \land B = +∞))$
34	29 33	orbi12d	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land \neg (A = 0 \lor B = 0)) \to (((0 < - A \land B = −∞) \lor (- A < 0 \land B = +∞)) \leftrightarrow ((A < 0 \land B = −∞) \lor (0 < A \land B = +∞)))$
35		orcom	$⊢ ((A < 0 \land B = −∞) \lor (0 < A \land B = +∞)) \leftrightarrow ((0 < A \land B = +∞) \lor (A < 0 \land B = −∞))$
36	34 35	bitrdi	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land \neg (A = 0 \lor B = 0)) \to (((0 < - A \land B = −∞) \lor (- A < 0 \land B = +∞)) \leftrightarrow ((0 < A \land B = +∞) \lor (A < 0 \land B = −∞)))$
37	25 36	orbi12d	$⊢ ((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 < B \land A = +∞) \lor (B < 0 \land A = −∞)) \lor ((0 < A \land B = +∞) \lor (A < 0 \land B = −∞))))$
38	37	biimpar	$⊢ (((A \in ℝ^{} \land B \in ℝ^{}) \land \neg (A = 0 \lor B = 0)) \land (((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 = +∞)))$
39	38	iftrued	$⊢ (((A \in ℝ^{} \land B \in ℝ^{}) \land \neg (A = 0 \lor B = 0)) \land (((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) = −∞$
40		xmullem2	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to ((((0 < B \land A = +∞) \lor (B < 0 \land A = −∞)) \lor ((0 < A \land B = +∞) \lor (A < 0 \land B = −∞))) \to \neg (((0 < B \land A = −∞) \lor (B < 0 \land A = +∞)) \lor ((0 < A \land B = −∞) \lor (A < 0 \land B = +∞))))$
41	40	adantr	$⊢ ((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 = −∞))) \to \neg (((0 < B \land A = −∞) \lor (B < 0 \land A = +∞)) \lor ((0 < A \land B = −∞) \lor (A < 0 \land B = +∞))))$
42	23	anbi2d	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land \neg (A = 0 \lor B = 0)) \to ((0 < B \land - A = +∞) \leftrightarrow (0 < B \land A = −∞))$
43	16	anbi2d	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land \neg (A = 0 \lor B = 0)) \to ((B < 0 \land - A = −∞) \leftrightarrow (B < 0 \land A = +∞))$
44	42 43	orbi12d	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land \neg (A = 0 \lor B = 0)) \to (((0 < B \land - A = +∞) \lor (B < 0 \land - A = −∞)) \leftrightarrow ((0 < B \land A = −∞) \lor (B < 0 \land A = +∞)))$
45	28	anbi1d	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land \neg (A = 0 \lor B = 0)) \to ((0 < - A \land B = +∞) \leftrightarrow (A < 0 \land B = +∞))$
46	32	anbi1d	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land \neg (A = 0 \lor B = 0)) \to ((- A < 0 \land B = −∞) \leftrightarrow (0 < A \land B = −∞))$
47	45 46	orbi12d	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land \neg (A = 0 \lor B = 0)) \to (((0 < - A \land B = +∞) \lor (- A < 0 \land B = −∞)) \leftrightarrow ((A < 0 \land B = +∞) \lor (0 < A \land B = −∞)))$
48		orcom	$⊢ ((A < 0 \land B = +∞) \lor (0 < A \land B = −∞)) \leftrightarrow ((0 < A \land B = −∞) \lor (A < 0 \land B = +∞))$
49	47 48	bitrdi	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land \neg (A = 0 \lor B = 0)) \to (((0 < - A \land B = +∞) \lor (- A < 0 \land B = −∞)) \leftrightarrow ((0 < A \land B = −∞) \lor (A < 0 \land B = +∞)))$
50	44 49	orbi12d	$⊢ ((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 < B \land A = −∞) \lor (B < 0 \land A = +∞)) \lor ((0 < A \land B = −∞) \lor (A < 0 \land B = +∞))))$
51	50	notbid	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land \neg (A = 0 \lor B = 0)) \to (\neg (((0 < B \land - A = +∞) \lor (B < 0 \land - A = −∞)) \lor ((0 < - A \land B = +∞) \lor (- A < 0 \land B = −∞))) \leftrightarrow \neg (((0 < B \land A = −∞) \lor (B < 0 \land A = +∞)) \lor ((0 < A \land B = −∞) \lor (A < 0 \land B = +∞))))$
52	41 51	sylibrd	$⊢ ((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 = −∞))) \to \neg (((0 < B \land - A = +∞) \lor (B < 0 \land - A = −∞)) \lor ((0 < - A \land B = +∞) \lor (- A < 0 \land B = −∞))))$
53	52	imp	$⊢ (((A \in ℝ^{} \land B \in ℝ^{}) \land \neg (A = 0 \lor B = 0)) \land (((0 < B \land A = +∞) \lor (B < 0 \land A = −∞)) \lor ((0 < A \land B = +∞) \lor (A < 0 \land B = −∞)))) \to \neg (((0 < B \land - A = +∞) \lor (B < 0 \land - A = −∞)) \lor ((0 < - A \land B = +∞) \lor (- A < 0 \land B = −∞)))$
54	53	iffalsed	$⊢ (((A \in ℝ^{} \land B \in ℝ^{}) \land \neg (A = 0 \lor B = 0)) \land (((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 = −∞))), +∞, 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)$
55		iftrue	$⊢ (((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 = −∞))), +∞, if ((((0 < B \land A = −∞) \lor (B < 0 \land A = +∞)) \lor ((0 < A \land B = −∞) \lor (A < 0 \land B = +∞))), −∞, A B)) = +∞$
56	55	adantl	$⊢ (((A \in ℝ^{} \land B \in ℝ^{}) \land \neg (A = 0 \lor B = 0)) \land (((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 = −∞))), +∞, if ((((0 < B \land A = −∞) \lor (B < 0 \land A = +∞)) \lor ((0 < A \land B = −∞) \lor (A < 0 \land B = +∞))), −∞, A B)) = +∞$
57		xnegeq	$⊢ 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)) = +∞ \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)) = - +∞$
58	56 57	syl	$⊢ (((A \in ℝ^{} \land B \in ℝ^{}) \land \neg (A = 0 \lor B = 0)) \land (((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 = −∞))), +∞, if ((((0 < B \land A = −∞) \lor (B < 0 \land A = +∞)) \lor ((0 < A \land B = −∞) \lor (A < 0 \land B = +∞))), −∞, A B)) = - +∞$
59	58 10	eqtrdi	$⊢ (((A \in ℝ^{} \land B \in ℝ^{}) \land \neg (A = 0 \lor B = 0)) \land (((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 = −∞))), +∞, if ((((0 < B \land A = −∞) \lor (B < 0 \land A = +∞)) \lor ((0 < A \land B = −∞) \lor (A < 0 \land B = +∞))), −∞, A B)) = −∞$
60	39 54 59	3eqtr4d	$⊢ (((A \in ℝ^{} \land B \in ℝ^{}) \land \neg (A = 0 \lor B = 0)) \land (((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 = −∞))), +∞, 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 < B \land A = −∞) \lor (B < 0 \land A = +∞)) \lor ((0 < A \land B = −∞) \lor (A < 0 \land B = +∞))), −∞, A B))$
61	50	biimpar	$⊢ (((A \in ℝ^{} \land B \in ℝ^{}) \land \neg (A = 0 \lor B = 0)) \land (((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 = −∞)))$
62	61	iftrued	$⊢ (((A \in ℝ^{} \land B \in ℝ^{}) \land \neg (A = 0 \lor B = 0)) \land (((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 = −∞))), +∞, if ((((0 < B \land - A = −∞) \lor (B < 0 \land - A = +∞)) \lor ((0 < - A \land B = −∞) \lor (- A < 0 \land B = +∞))), −∞, (- A) B)) = +∞$
63	41	con2d	$⊢ ((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 = +∞))) \to \neg (((0 < B \land A = +∞) \lor (B < 0 \land A = −∞)) \lor ((0 < A \land B = +∞) \lor (A < 0 \land B = −∞))))$
64	63	imp	$⊢ (((A \in ℝ^{} \land B \in ℝ^{}) \land \neg (A = 0 \lor B = 0)) \land (((0 < B \land A = −∞) \lor (B < 0 \land A = +∞)) \lor ((0 < A \land B = −∞) \lor (A < 0 \land B = +∞)))) \to \neg (((0 < B \land A = +∞) \lor (B < 0 \land A = −∞)) \lor ((0 < A \land B = +∞) \lor (A < 0 \land B = −∞)))$
65	64	iffalsed	$⊢ (((A \in ℝ^{} \land B \in ℝ^{}) \land \neg (A = 0 \lor B = 0)) \land (((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 = −∞))), +∞, 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)$
66		iftrue	$⊢ (((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) = −∞$
67	66	adantl	$⊢ (((A \in ℝ^{} \land B \in ℝ^{}) \land \neg (A = 0 \lor B = 0)) \land (((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) = −∞$
68	65 67	eqtrd	$⊢ (((A \in ℝ^{} \land B \in ℝ^{}) \land \neg (A = 0 \lor B = 0)) \land (((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 = −∞))), +∞, if ((((0 < B \land A = −∞) \lor (B < 0 \land A = +∞)) \lor ((0 < A \land B = −∞) \lor (A < 0 \land B = +∞))), −∞, A B)) = −∞$
69		xnegeq	$⊢ 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)) = −∞ \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)) = - −∞$
70	68 69	syl	$⊢ (((A \in ℝ^{} \land B \in ℝ^{}) \land \neg (A = 0 \lor B = 0)) \land (((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 = −∞))), +∞, if ((((0 < B \land A = −∞) \lor (B < 0 \land A = +∞)) \lor ((0 < A \land B = −∞) \lor (A < 0 \land B = +∞))), −∞, A B)) = - −∞$
71	70 18	eqtrdi	$⊢ (((A \in ℝ^{} \land B \in ℝ^{}) \land \neg (A = 0 \lor B = 0)) \land (((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 = −∞))), +∞, if ((((0 < B \land A = −∞) \lor (B < 0 \land A = +∞)) \lor ((0 < A \land B = −∞) \lor (A < 0 \land B = +∞))), −∞, A B)) = +∞$
72	62 71	eqtr4d	$⊢ (((A \in ℝ^{} \land B \in ℝ^{}) \land \neg (A = 0 \lor B = 0)) \land (((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 = −∞))), +∞, 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 < B \land A = −∞) \lor (B < 0 \land A = +∞)) \lor ((0 < A \land B = −∞) \lor (A < 0 \land B = +∞))), −∞, A B))$
73	72	adantlr	$⊢ ((((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 (((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 = −∞))), +∞, 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 < B \land A = −∞) \lor (B < 0 \land A = +∞)) \lor ((0 < A \land B = −∞) \lor (A < 0 \land B = +∞))), −∞, A B))$
74	37	notbid	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land \neg (A = 0 \lor B = 0)) \to (\neg (((0 < B \land - A = −∞) \lor (B < 0 \land - A = +∞)) \lor ((0 < - A \land B = −∞) \lor (- A < 0 \land B = +∞))) \leftrightarrow \neg (((0 < B \land A = +∞) \lor (B < 0 \land A = −∞)) \lor ((0 < A \land B = +∞) \lor (A < 0 \land B = −∞))))$
75	74	biimpar	$⊢ (((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 \neg (((0 < B \land - A = −∞) \lor (B < 0 \land - A = +∞)) \lor ((0 < - A \land B = −∞) \lor (- A < 0 \land B = +∞)))$
76	75	adantr	$⊢ ((((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 \neg (((0 < B \land - A = −∞) \lor (B < 0 \land - A = +∞)) \lor ((0 < - A \land B = −∞) \lor (- A < 0 \land B = +∞)))$
77	76	iffalsed	$⊢ ((((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 if ((((0 < B \land - A = −∞) \lor (B < 0 \land - A = +∞)) \lor ((0 < - A \land B = −∞) \lor (- A < 0 \land B = +∞))), −∞, (- A) B) = (- A) B$
78	51	biimpar	$⊢ (((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 \neg (((0 < B \land - A = +∞) \lor (B < 0 \land - A = −∞)) \lor ((0 < - A \land B = +∞) \lor (- A < 0 \land B = −∞)))$
79	78	adantlr	$⊢ ((((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 \neg (((0 < B \land - A = +∞) \lor (B < 0 \land - A = −∞)) \lor ((0 < - A \land B = +∞) \lor (- A < 0 \land B = −∞)))$
80	79	iffalsed	$⊢ ((((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 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)$
81		iffalse	$⊢ \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 = −∞))), +∞, 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)$
82	81	ad2antlr	$⊢ ((((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 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)$
83		iffalse	$⊢ \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) = A B$
84	83	adantl	$⊢ ((((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 if ((((0 < B \land A = −∞) \lor (B < 0 \land A = +∞)) \lor ((0 < A \land B = −∞) \lor (A < 0 \land B = +∞))), −∞, A B) = A B$
85	82 84	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 = −∞)))) \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 = −∞))), +∞, if ((((0 < B \land A = −∞) \lor (B < 0 \land A = +∞)) \lor ((0 < A \land B = −∞) \lor (A < 0 \land B = +∞))), −∞, A B)) = A B$
86		xnegeq	$⊢ 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 \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$
87	85 86	syl	$⊢ ((((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 - 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$
88		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 ℝ$
89	88	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 ℂ$
90		ancom	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \leftrightarrow (B \in ℝ^{} \land A \in ℝ^{})$
91		orcom	$⊢ (A = 0 \lor B = 0) \leftrightarrow (B = 0 \lor A = 0)$
92	91	notbii	$⊢ \neg (A = 0 \lor B = 0) \leftrightarrow \neg (B = 0 \lor A = 0)$
93	90 92	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))$
94		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 = −∞)))$
95	94	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 = −∞)))$
96	93 95	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 = −∞))))$
97		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 = +∞)))$
98	97	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 = +∞)))$
99		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 ℝ$
100	96 98 99	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 ℝ$
101	100	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 ℂ$
102	89 101	mulneg1d	$⊢ ((((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 = - A B$
103		rexneg	$⊢ A \in ℝ \to - A = - A$
104	88 103	syl	$⊢ ((((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 = - A$
105	104	oveq1d	$⊢ ((((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 = (- A) B$
106	88 100	remulcld	$⊢ ((((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 \in ℝ$
107		rexneg	$⊢ A B \in ℝ \to - A B = - A B$
108	106 107	syl	$⊢ ((((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 = - A B$
109	102 105 108	3eqtr4d	$⊢ ((((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 = - A B$
110	87 109	eqtr4d	$⊢ ((((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 - 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$
111	77 80 110	3eqtr4d	$⊢ ((((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 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 < B \land A = −∞) \lor (B < 0 \land A = +∞)) \lor ((0 < A \land B = −∞) \lor (A < 0 \land B = +∞))), −∞, A B))$
112	73 111	pm2.61dan	$⊢ (((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 = −∞))), +∞, 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 < B \land A = −∞) \lor (B < 0 \land A = +∞)) \lor ((0 < A \land B = −∞) \lor (A < 0 \land B = +∞))), −∞, A B))$
113	60 112	pm2.61dan	$⊢ ((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 < B \land A = −∞) \lor (B < 0 \land A = +∞)) \lor ((0 < A \land B = −∞) \lor (A < 0 \land B = +∞))), −∞, A B))$
114	113	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 < 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)))$
115	9 114	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 ((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)))$
116		xnegeq	$⊢ 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))) = 0 \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))) = - 0$
117	116 1	eqtrdi	$⊢ 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))) = 0 \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))) = 0$
118		xnegeq	$⊢ 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 ((((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)) \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 ((((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))$
119	117 118	ifsb	$⊢ - 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 < 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)))$
120	115 119	eqtr4di	$⊢ (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 < 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)))$
121		xnegcl	$⊢ A \in ℝ^{} \to - A \in ℝ^{}$
122		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)))$
123	121 122	sylan	$⊢ (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)))$
124		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)))$
125		xnegeq	$⊢ 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))) \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)))$
126	124 125	syl	$⊢ (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)))$
127	120 123 126	3eqtr4d	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to (- A) \cdot_{𝑒} B = - (A \cdot_{𝑒} B)$

Metamath Proof Explorer

Theorem xmulneg1

Proof