xmullem

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

Proof

Step	Hyp	Ref	Expression
1		ioran	$⊢ \neg (A = 0 \lor B = 0) \leftrightarrow (\neg A = 0 \land \neg B = 0)$
2	1	anbi2i	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land \neg (A = 0 \lor B = 0)) \leftrightarrow ((A \in ℝ^{} \land B \in ℝ^{}) \land (\neg A = 0 \land \neg B = 0))$
3		ioran	$⊢ \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 = −∞)) \land \neg ((0 < A \land B = +∞) \lor (A < 0 \land B = −∞)))$
4		ioran	$⊢ \neg ((0 < B \land A = +∞) \lor (B < 0 \land A = −∞)) \leftrightarrow (\neg (0 < B \land A = +∞) \land \neg (B < 0 \land A = −∞))$
5		ioran	$⊢ \neg ((0 < A \land B = +∞) \lor (A < 0 \land B = −∞)) \leftrightarrow (\neg (0 < A \land B = +∞) \land \neg (A < 0 \land B = −∞))$
6	4 5	anbi12i	$⊢ (\neg ((0 < B \land A = +∞) \lor (B < 0 \land A = −∞)) \land \neg ((0 < A \land B = +∞) \lor (A < 0 \land B = −∞))) \leftrightarrow ((\neg (0 < B \land A = +∞) \land \neg (B < 0 \land A = −∞)) \land (\neg (0 < A \land B = +∞) \land \neg (A < 0 \land B = −∞)))$
7	3 6	bitri	$⊢ \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 = +∞) \land \neg (B < 0 \land A = −∞)) \land (\neg (0 < A \land B = +∞) \land \neg (A < 0 \land B = −∞)))$
8		ioran	$⊢ \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 = +∞)) \land \neg ((0 < A \land B = −∞) \lor (A < 0 \land B = +∞)))$
9		ioran	$⊢ \neg ((0 < B \land A = −∞) \lor (B < 0 \land A = +∞)) \leftrightarrow (\neg (0 < B \land A = −∞) \land \neg (B < 0 \land A = +∞))$
10		ioran	$⊢ \neg ((0 < A \land B = −∞) \lor (A < 0 \land B = +∞)) \leftrightarrow (\neg (0 < A \land B = −∞) \land \neg (A < 0 \land B = +∞))$
11	9 10	anbi12i	$⊢ (\neg ((0 < B \land A = −∞) \lor (B < 0 \land A = +∞)) \land \neg ((0 < A \land B = −∞) \lor (A < 0 \land B = +∞))) \leftrightarrow ((\neg (0 < B \land A = −∞) \land \neg (B < 0 \land A = +∞)) \land (\neg (0 < A \land B = −∞) \land \neg (A < 0 \land B = +∞)))$
12	8 11	bitri	$⊢ \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 = −∞) \land \neg (B < 0 \land A = +∞)) \land (\neg (0 < A \land B = −∞) \land \neg (A < 0 \land B = +∞)))$
13	7 12	anbi12i	$⊢ (\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 = +∞)))) \leftrightarrow (((\neg (0 < B \land A = +∞) \land \neg (B < 0 \land A = −∞)) \land (\neg (0 < A \land B = +∞) \land \neg (A < 0 \land B = −∞))) \land ((\neg (0 < B \land A = −∞) \land \neg (B < 0 \land A = +∞)) \land (\neg (0 < A \land B = −∞) \land \neg (A < 0 \land B = +∞))))$
14		simplll	$⊢ (((A \in ℝ^{} \land B \in ℝ^{}) \land (\neg A = 0 \land \neg B = 0)) \land (((\neg (0 < B \land A = +∞) \land \neg (B < 0 \land A = −∞)) \land (\neg (0 < A \land B = +∞) \land \neg (A < 0 \land B = −∞))) \land ((\neg (0 < B \land A = −∞) \land \neg (B < 0 \land A = +∞)) \land (\neg (0 < A \land B = −∞) \land \neg (A < 0 \land B = +∞))))) \to A \in ℝ^{*}$
15		elxr	$⊢ A \in ℝ^{*} \leftrightarrow (A \in ℝ \lor A = +∞ \lor A = −∞)$
16	14 15	sylib	$⊢ (((A \in ℝ^{} \land B \in ℝ^{}) \land (\neg A = 0 \land \neg B = 0)) \land (((\neg (0 < B \land A = +∞) \land \neg (B < 0 \land A = −∞)) \land (\neg (0 < A \land B = +∞) \land \neg (A < 0 \land B = −∞))) \land ((\neg (0 < B \land A = −∞) \land \neg (B < 0 \land A = +∞)) \land (\neg (0 < A \land B = −∞) \land \neg (A < 0 \land B = +∞))))) \to (A \in ℝ \lor A = +∞ \lor A = −∞)$
17		idd	$⊢ (((A \in ℝ^{} \land B \in ℝ^{}) \land (\neg A = 0 \land \neg B = 0)) \land (((\neg (0 < B \land A = +∞) \land \neg (B < 0 \land A = −∞)) \land (\neg (0 < A \land B = +∞) \land \neg (A < 0 \land B = −∞))) \land ((\neg (0 < B \land A = −∞) \land \neg (B < 0 \land A = +∞)) \land (\neg (0 < A \land B = −∞) \land \neg (A < 0 \land B = +∞))))) \to (A \in ℝ \to A \in ℝ)$
18		simprlr	$⊢ (((\neg (0 < B \land A = +∞) \land \neg (B < 0 \land A = −∞)) \land (\neg (0 < A \land B = +∞) \land \neg (A < 0 \land B = −∞))) \land ((\neg (0 < B \land A = −∞) \land \neg (B < 0 \land A = +∞)) \land (\neg (0 < A \land B = −∞) \land \neg (A < 0 \land B = +∞)))) \to \neg (B < 0 \land A = +∞)$
19	18	adantl	$⊢ (((A \in ℝ^{} \land B \in ℝ^{}) \land (\neg A = 0 \land \neg B = 0)) \land (((\neg (0 < B \land A = +∞) \land \neg (B < 0 \land A = −∞)) \land (\neg (0 < A \land B = +∞) \land \neg (A < 0 \land B = −∞))) \land ((\neg (0 < B \land A = −∞) \land \neg (B < 0 \land A = +∞)) \land (\neg (0 < A \land B = −∞) \land \neg (A < 0 \land B = +∞))))) \to \neg (B < 0 \land A = +∞)$
20	19	pm2.21d	$⊢ (((A \in ℝ^{} \land B \in ℝ^{}) \land (\neg A = 0 \land \neg B = 0)) \land (((\neg (0 < B \land A = +∞) \land \neg (B < 0 \land A = −∞)) \land (\neg (0 < A \land B = +∞) \land \neg (A < 0 \land B = −∞))) \land ((\neg (0 < B \land A = −∞) \land \neg (B < 0 \land A = +∞)) \land (\neg (0 < A \land B = −∞) \land \neg (A < 0 \land B = +∞))))) \to ((B < 0 \land A = +∞) \to A \in ℝ)$
21	20	expdimp	$⊢ ((((A \in ℝ^{} \land B \in ℝ^{}) \land (\neg A = 0 \land \neg B = 0)) \land (((\neg (0 < B \land A = +∞) \land \neg (B < 0 \land A = −∞)) \land (\neg (0 < A \land B = +∞) \land \neg (A < 0 \land B = −∞))) \land ((\neg (0 < B \land A = −∞) \land \neg (B < 0 \land A = +∞)) \land (\neg (0 < A \land B = −∞) \land \neg (A < 0 \land B = +∞))))) \land B < 0) \to (A = +∞ \to A \in ℝ)$
22		simplrr	$⊢ (((A \in ℝ^{} \land B \in ℝ^{}) \land (\neg A = 0 \land \neg B = 0)) \land (((\neg (0 < B \land A = +∞) \land \neg (B < 0 \land A = −∞)) \land (\neg (0 < A \land B = +∞) \land \neg (A < 0 \land B = −∞))) \land ((\neg (0 < B \land A = −∞) \land \neg (B < 0 \land A = +∞)) \land (\neg (0 < A \land B = −∞) \land \neg (A < 0 \land B = +∞))))) \to \neg B = 0$
23	22	pm2.21d	$⊢ (((A \in ℝ^{} \land B \in ℝ^{}) \land (\neg A = 0 \land \neg B = 0)) \land (((\neg (0 < B \land A = +∞) \land \neg (B < 0 \land A = −∞)) \land (\neg (0 < A \land B = +∞) \land \neg (A < 0 \land B = −∞))) \land ((\neg (0 < B \land A = −∞) \land \neg (B < 0 \land A = +∞)) \land (\neg (0 < A \land B = −∞) \land \neg (A < 0 \land B = +∞))))) \to (B = 0 \to (A = +∞ \to A \in ℝ))$
24	23	imp	$⊢ ((((A \in ℝ^{} \land B \in ℝ^{}) \land (\neg A = 0 \land \neg B = 0)) \land (((\neg (0 < B \land A = +∞) \land \neg (B < 0 \land A = −∞)) \land (\neg (0 < A \land B = +∞) \land \neg (A < 0 \land B = −∞))) \land ((\neg (0 < B \land A = −∞) \land \neg (B < 0 \land A = +∞)) \land (\neg (0 < A \land B = −∞) \land \neg (A < 0 \land B = +∞))))) \land B = 0) \to (A = +∞ \to A \in ℝ)$
25		simplll	$⊢ (((\neg (0 < B \land A = +∞) \land \neg (B < 0 \land A = −∞)) \land (\neg (0 < A \land B = +∞) \land \neg (A < 0 \land B = −∞))) \land ((\neg (0 < B \land A = −∞) \land \neg (B < 0 \land A = +∞)) \land (\neg (0 < A \land B = −∞) \land \neg (A < 0 \land B = +∞)))) \to \neg (0 < B \land A = +∞)$
26	25	adantl	$⊢ (((A \in ℝ^{} \land B \in ℝ^{}) \land (\neg A = 0 \land \neg B = 0)) \land (((\neg (0 < B \land A = +∞) \land \neg (B < 0 \land A = −∞)) \land (\neg (0 < A \land B = +∞) \land \neg (A < 0 \land B = −∞))) \land ((\neg (0 < B \land A = −∞) \land \neg (B < 0 \land A = +∞)) \land (\neg (0 < A \land B = −∞) \land \neg (A < 0 \land B = +∞))))) \to \neg (0 < B \land A = +∞)$
27	26	pm2.21d	$⊢ (((A \in ℝ^{} \land B \in ℝ^{}) \land (\neg A = 0 \land \neg B = 0)) \land (((\neg (0 < B \land A = +∞) \land \neg (B < 0 \land A = −∞)) \land (\neg (0 < A \land B = +∞) \land \neg (A < 0 \land B = −∞))) \land ((\neg (0 < B \land A = −∞) \land \neg (B < 0 \land A = +∞)) \land (\neg (0 < A \land B = −∞) \land \neg (A < 0 \land B = +∞))))) \to ((0 < B \land A = +∞) \to A \in ℝ)$
28	27	expdimp	$⊢ ((((A \in ℝ^{} \land B \in ℝ^{}) \land (\neg A = 0 \land \neg B = 0)) \land (((\neg (0 < B \land A = +∞) \land \neg (B < 0 \land A = −∞)) \land (\neg (0 < A \land B = +∞) \land \neg (A < 0 \land B = −∞))) \land ((\neg (0 < B \land A = −∞) \land \neg (B < 0 \land A = +∞)) \land (\neg (0 < A \land B = −∞) \land \neg (A < 0 \land B = +∞))))) \land 0 < B) \to (A = +∞ \to A \in ℝ)$
29		simpllr	$⊢ (((A \in ℝ^{} \land B \in ℝ^{}) \land (\neg A = 0 \land \neg B = 0)) \land (((\neg (0 < B \land A = +∞) \land \neg (B < 0 \land A = −∞)) \land (\neg (0 < A \land B = +∞) \land \neg (A < 0 \land B = −∞))) \land ((\neg (0 < B \land A = −∞) \land \neg (B < 0 \land A = +∞)) \land (\neg (0 < A \land B = −∞) \land \neg (A < 0 \land B = +∞))))) \to B \in ℝ^{*}$
30		0xr	$⊢ 0 \in ℝ^{*}$
31		xrltso	$⊢ < Or ℝ^{*}$
32		solin	$⊢ (< Or ℝ^{} \land (B \in ℝ^{} \land 0 \in ℝ^{*})) \to (B < 0 \lor B = 0 \lor 0 < B)$
33	31 32	mpan	$⊢ (B \in ℝ^{} \land 0 \in ℝ^{}) \to (B < 0 \lor B = 0 \lor 0 < B)$
34	29 30 33	sylancl	$⊢ (((A \in ℝ^{} \land B \in ℝ^{}) \land (\neg A = 0 \land \neg B = 0)) \land (((\neg (0 < B \land A = +∞) \land \neg (B < 0 \land A = −∞)) \land (\neg (0 < A \land B = +∞) \land \neg (A < 0 \land B = −∞))) \land ((\neg (0 < B \land A = −∞) \land \neg (B < 0 \land A = +∞)) \land (\neg (0 < A \land B = −∞) \land \neg (A < 0 \land B = +∞))))) \to (B < 0 \lor B = 0 \lor 0 < B)$
35	21 24 28 34	mpjao3dan	$⊢ (((A \in ℝ^{} \land B \in ℝ^{}) \land (\neg A = 0 \land \neg B = 0)) \land (((\neg (0 < B \land A = +∞) \land \neg (B < 0 \land A = −∞)) \land (\neg (0 < A \land B = +∞) \land \neg (A < 0 \land B = −∞))) \land ((\neg (0 < B \land A = −∞) \land \neg (B < 0 \land A = +∞)) \land (\neg (0 < A \land B = −∞) \land \neg (A < 0 \land B = +∞))))) \to (A = +∞ \to A \in ℝ)$
36		simpllr	$⊢ (((\neg (0 < B \land A = +∞) \land \neg (B < 0 \land A = −∞)) \land (\neg (0 < A \land B = +∞) \land \neg (A < 0 \land B = −∞))) \land ((\neg (0 < B \land A = −∞) \land \neg (B < 0 \land A = +∞)) \land (\neg (0 < A \land B = −∞) \land \neg (A < 0 \land B = +∞)))) \to \neg (B < 0 \land A = −∞)$
37	36	adantl	$⊢ (((A \in ℝ^{} \land B \in ℝ^{}) \land (\neg A = 0 \land \neg B = 0)) \land (((\neg (0 < B \land A = +∞) \land \neg (B < 0 \land A = −∞)) \land (\neg (0 < A \land B = +∞) \land \neg (A < 0 \land B = −∞))) \land ((\neg (0 < B \land A = −∞) \land \neg (B < 0 \land A = +∞)) \land (\neg (0 < A \land B = −∞) \land \neg (A < 0 \land B = +∞))))) \to \neg (B < 0 \land A = −∞)$
38	37	pm2.21d	$⊢ (((A \in ℝ^{} \land B \in ℝ^{}) \land (\neg A = 0 \land \neg B = 0)) \land (((\neg (0 < B \land A = +∞) \land \neg (B < 0 \land A = −∞)) \land (\neg (0 < A \land B = +∞) \land \neg (A < 0 \land B = −∞))) \land ((\neg (0 < B \land A = −∞) \land \neg (B < 0 \land A = +∞)) \land (\neg (0 < A \land B = −∞) \land \neg (A < 0 \land B = +∞))))) \to ((B < 0 \land A = −∞) \to A \in ℝ)$
39	38	expdimp	$⊢ ((((A \in ℝ^{} \land B \in ℝ^{}) \land (\neg A = 0 \land \neg B = 0)) \land (((\neg (0 < B \land A = +∞) \land \neg (B < 0 \land A = −∞)) \land (\neg (0 < A \land B = +∞) \land \neg (A < 0 \land B = −∞))) \land ((\neg (0 < B \land A = −∞) \land \neg (B < 0 \land A = +∞)) \land (\neg (0 < A \land B = −∞) \land \neg (A < 0 \land B = +∞))))) \land B < 0) \to (A = −∞ \to A \in ℝ)$
40	22	pm2.21d	$⊢ (((A \in ℝ^{} \land B \in ℝ^{}) \land (\neg A = 0 \land \neg B = 0)) \land (((\neg (0 < B \land A = +∞) \land \neg (B < 0 \land A = −∞)) \land (\neg (0 < A \land B = +∞) \land \neg (A < 0 \land B = −∞))) \land ((\neg (0 < B \land A = −∞) \land \neg (B < 0 \land A = +∞)) \land (\neg (0 < A \land B = −∞) \land \neg (A < 0 \land B = +∞))))) \to (B = 0 \to (A = −∞ \to A \in ℝ))$
41	40	imp	$⊢ ((((A \in ℝ^{} \land B \in ℝ^{}) \land (\neg A = 0 \land \neg B = 0)) \land (((\neg (0 < B \land A = +∞) \land \neg (B < 0 \land A = −∞)) \land (\neg (0 < A \land B = +∞) \land \neg (A < 0 \land B = −∞))) \land ((\neg (0 < B \land A = −∞) \land \neg (B < 0 \land A = +∞)) \land (\neg (0 < A \land B = −∞) \land \neg (A < 0 \land B = +∞))))) \land B = 0) \to (A = −∞ \to A \in ℝ)$
42		simprll	$⊢ (((\neg (0 < B \land A = +∞) \land \neg (B < 0 \land A = −∞)) \land (\neg (0 < A \land B = +∞) \land \neg (A < 0 \land B = −∞))) \land ((\neg (0 < B \land A = −∞) \land \neg (B < 0 \land A = +∞)) \land (\neg (0 < A \land B = −∞) \land \neg (A < 0 \land B = +∞)))) \to \neg (0 < B \land A = −∞)$
43	42	adantl	$⊢ (((A \in ℝ^{} \land B \in ℝ^{}) \land (\neg A = 0 \land \neg B = 0)) \land (((\neg (0 < B \land A = +∞) \land \neg (B < 0 \land A = −∞)) \land (\neg (0 < A \land B = +∞) \land \neg (A < 0 \land B = −∞))) \land ((\neg (0 < B \land A = −∞) \land \neg (B < 0 \land A = +∞)) \land (\neg (0 < A \land B = −∞) \land \neg (A < 0 \land B = +∞))))) \to \neg (0 < B \land A = −∞)$
44	43	pm2.21d	$⊢ (((A \in ℝ^{} \land B \in ℝ^{}) \land (\neg A = 0 \land \neg B = 0)) \land (((\neg (0 < B \land A = +∞) \land \neg (B < 0 \land A = −∞)) \land (\neg (0 < A \land B = +∞) \land \neg (A < 0 \land B = −∞))) \land ((\neg (0 < B \land A = −∞) \land \neg (B < 0 \land A = +∞)) \land (\neg (0 < A \land B = −∞) \land \neg (A < 0 \land B = +∞))))) \to ((0 < B \land A = −∞) \to A \in ℝ)$
45	44	expdimp	$⊢ ((((A \in ℝ^{} \land B \in ℝ^{}) \land (\neg A = 0 \land \neg B = 0)) \land (((\neg (0 < B \land A = +∞) \land \neg (B < 0 \land A = −∞)) \land (\neg (0 < A \land B = +∞) \land \neg (A < 0 \land B = −∞))) \land ((\neg (0 < B \land A = −∞) \land \neg (B < 0 \land A = +∞)) \land (\neg (0 < A \land B = −∞) \land \neg (A < 0 \land B = +∞))))) \land 0 < B) \to (A = −∞ \to A \in ℝ)$
46	39 41 45 34	mpjao3dan	$⊢ (((A \in ℝ^{} \land B \in ℝ^{}) \land (\neg A = 0 \land \neg B = 0)) \land (((\neg (0 < B \land A = +∞) \land \neg (B < 0 \land A = −∞)) \land (\neg (0 < A \land B = +∞) \land \neg (A < 0 \land B = −∞))) \land ((\neg (0 < B \land A = −∞) \land \neg (B < 0 \land A = +∞)) \land (\neg (0 < A \land B = −∞) \land \neg (A < 0 \land B = +∞))))) \to (A = −∞ \to A \in ℝ)$
47	17 35 46	3jaod	$⊢ (((A \in ℝ^{} \land B \in ℝ^{}) \land (\neg A = 0 \land \neg B = 0)) \land (((\neg (0 < B \land A = +∞) \land \neg (B < 0 \land A = −∞)) \land (\neg (0 < A \land B = +∞) \land \neg (A < 0 \land B = −∞))) \land ((\neg (0 < B \land A = −∞) \land \neg (B < 0 \land A = +∞)) \land (\neg (0 < A \land B = −∞) \land \neg (A < 0 \land B = +∞))))) \to ((A \in ℝ \lor A = +∞ \lor A = −∞) \to A \in ℝ)$
48	16 47	mpd	$⊢ (((A \in ℝ^{} \land B \in ℝ^{}) \land (\neg A = 0 \land \neg B = 0)) \land (((\neg (0 < B \land A = +∞) \land \neg (B < 0 \land A = −∞)) \land (\neg (0 < A \land B = +∞) \land \neg (A < 0 \land B = −∞))) \land ((\neg (0 < B \land A = −∞) \land \neg (B < 0 \land A = +∞)) \land (\neg (0 < A \land B = −∞) \land \neg (A < 0 \land B = +∞))))) \to A \in ℝ$
49	2 13 48	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 A \in ℝ$
50	49	anassrs	$⊢ ((((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 ℝ$

Metamath Proof Explorer

Theorem xmullem

Proof