xmullem2

		Ref	Expression
	Assertion	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 = +∞))))$

Proof

Step	Hyp	Ref	Expression
1		mnfnepnf	$⊢ −∞ \neq +∞$
2		eqeq1	$⊢ A = −∞ \to (A = +∞ \leftrightarrow −∞ = +∞)$
3	2	necon3bbid	$⊢ A = −∞ \to (\neg A = +∞ \leftrightarrow −∞ \neq +∞)$
4	1 3	mpbiri	$⊢ A = −∞ \to \neg A = +∞$
5	4	con2i	$⊢ A = +∞ \to \neg A = −∞$
6	5	adantl	$⊢ (0 < B \land A = +∞) \to \neg A = −∞$
7		0xr	$⊢ 0 \in ℝ^{*}$
8		nltmnf	$⊢ 0 \in ℝ^{*} \to \neg 0 < −∞$
9	7 8	ax-mp	$⊢ \neg 0 < −∞$
10		breq2	$⊢ A = −∞ \to (0 < A \leftrightarrow 0 < −∞)$
11	9 10	mtbiri	$⊢ A = −∞ \to \neg 0 < A$
12	11	con2i	$⊢ 0 < A \to \neg A = −∞$
13	12	adantr	$⊢ (0 < A \land B = +∞) \to \neg A = −∞$
14	6 13	jaoi	$⊢ ((0 < B \land A = +∞) \lor (0 < A \land B = +∞)) \to \neg A = −∞$
15	14	a1i	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to (((0 < B \land A = +∞) \lor (0 < A \land B = +∞)) \to \neg A = −∞)$
16		simpr	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to B \in ℝ^{*}$
17		xrltnsym	$⊢ (B \in ℝ^{} \land 0 \in ℝ^{}) \to (B < 0 \to \neg 0 < B)$
18	16 7 17	sylancl	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to (B < 0 \to \neg 0 < B)$
19	18	adantrd	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to ((B < 0 \land A = −∞) \to \neg 0 < B)$
20		breq2	$⊢ B = −∞ \to (0 < B \leftrightarrow 0 < −∞)$
21	9 20	mtbiri	$⊢ B = −∞ \to \neg 0 < B$
22	21	adantl	$⊢ (A < 0 \land B = −∞) \to \neg 0 < B$
23	22	a1i	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to ((A < 0 \land B = −∞) \to \neg 0 < B)$
24	19 23	jaod	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to (((B < 0 \land A = −∞) \lor (A < 0 \land B = −∞)) \to \neg 0 < B)$
25	15 24	orim12d	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to ((((0 < B \land A = +∞) \lor (0 < A \land B = +∞)) \lor ((B < 0 \land A = −∞) \lor (A < 0 \land B = −∞))) \to (\neg A = −∞ \lor \neg 0 < B))$
26		ianor	$⊢ \neg (0 < B \land A = −∞) \leftrightarrow (\neg 0 < B \lor \neg A = −∞)$
27		orcom	$⊢ (\neg 0 < B \lor \neg A = −∞) \leftrightarrow (\neg A = −∞ \lor \neg 0 < B)$
28	26 27	bitri	$⊢ \neg (0 < B \land A = −∞) \leftrightarrow (\neg A = −∞ \lor \neg 0 < B)$
29	25 28	imbitrrdi	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to ((((0 < B \land A = +∞) \lor (0 < A \land B = +∞)) \lor ((B < 0 \land A = −∞) \lor (A < 0 \land B = −∞))) \to \neg (0 < B \land A = −∞))$
30	18	con2d	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to (0 < B \to \neg B < 0)$
31	30	adantrd	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to ((0 < B \land A = +∞) \to \neg B < 0)$
32		pnfnlt	$⊢ 0 \in ℝ^{*} \to \neg +∞ < 0$
33	7 32	ax-mp	$⊢ \neg +∞ < 0$
34		simpr	$⊢ (0 < A \land B = +∞) \to B = +∞$
35	34	breq1d	$⊢ (0 < A \land B = +∞) \to (B < 0 \leftrightarrow +∞ < 0)$
36	33 35	mtbiri	$⊢ (0 < A \land B = +∞) \to \neg B < 0$
37	36	a1i	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to ((0 < A \land B = +∞) \to \neg B < 0)$
38	31 37	jaod	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to (((0 < B \land A = +∞) \lor (0 < A \land B = +∞)) \to \neg B < 0)$
39	4	a1i	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to (A = −∞ \to \neg A = +∞)$
40	39	adantld	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to ((B < 0 \land A = −∞) \to \neg A = +∞)$
41		breq1	$⊢ A = +∞ \to (A < 0 \leftrightarrow +∞ < 0)$
42	33 41	mtbiri	$⊢ A = +∞ \to \neg A < 0$
43	42	con2i	$⊢ A < 0 \to \neg A = +∞$
44	43	adantr	$⊢ (A < 0 \land B = −∞) \to \neg A = +∞$
45	44	a1i	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to ((A < 0 \land B = −∞) \to \neg A = +∞)$
46	40 45	jaod	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to (((B < 0 \land A = −∞) \lor (A < 0 \land B = −∞)) \to \neg A = +∞)$
47	38 46	orim12d	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to ((((0 < B \land A = +∞) \lor (0 < A \land B = +∞)) \lor ((B < 0 \land A = −∞) \lor (A < 0 \land B = −∞))) \to (\neg B < 0 \lor \neg A = +∞))$
48		ianor	$⊢ \neg (B < 0 \land A = +∞) \leftrightarrow (\neg B < 0 \lor \neg A = +∞)$
49	47 48	imbitrrdi	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to ((((0 < B \land A = +∞) \lor (0 < A \land B = +∞)) \lor ((B < 0 \land A = −∞) \lor (A < 0 \land B = −∞))) \to \neg (B < 0 \land A = +∞))$
50	29 49	jcad	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to ((((0 < B \land A = +∞) \lor (0 < A \land B = +∞)) \lor ((B < 0 \land A = −∞) \lor (A < 0 \land B = −∞))) \to (\neg (0 < B \land A = −∞) \land \neg (B < 0 \land A = +∞)))$
51		ioran	$⊢ \neg ((0 < B \land A = −∞) \lor (B < 0 \land A = +∞)) \leftrightarrow (\neg (0 < B \land A = −∞) \land \neg (B < 0 \land A = +∞))$
52	50 51	imbitrrdi	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to ((((0 < B \land A = +∞) \lor (0 < A \land B = +∞)) \lor ((B < 0 \land A = −∞) \lor (A < 0 \land B = −∞))) \to \neg ((0 < B \land A = −∞) \lor (B < 0 \land A = +∞)))$
53	21	con2i	$⊢ 0 < B \to \neg B = −∞$
54	53	adantr	$⊢ (0 < B \land A = +∞) \to \neg B = −∞$
55	54	a1i	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to ((0 < B \land A = +∞) \to \neg B = −∞)$
56		pnfnemnf	$⊢ +∞ \neq −∞$
57		eqeq1	$⊢ B = +∞ \to (B = −∞ \leftrightarrow +∞ = −∞)$
58	57	necon3bbid	$⊢ B = +∞ \to (\neg B = −∞ \leftrightarrow +∞ \neq −∞)$
59	56 58	mpbiri	$⊢ B = +∞ \to \neg B = −∞$
60	59	adantl	$⊢ (0 < A \land B = +∞) \to \neg B = −∞$
61	60	a1i	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to ((0 < A \land B = +∞) \to \neg B = −∞)$
62	55 61	jaod	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to (((0 < B \land A = +∞) \lor (0 < A \land B = +∞)) \to \neg B = −∞)$
63	11	adantl	$⊢ (B < 0 \land A = −∞) \to \neg 0 < A$
64	63	a1i	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to ((B < 0 \land A = −∞) \to \neg 0 < A)$
65		simpl	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to A \in ℝ^{*}$
66		xrltnsym	$⊢ (A \in ℝ^{} \land 0 \in ℝ^{}) \to (A < 0 \to \neg 0 < A)$
67	65 7 66	sylancl	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to (A < 0 \to \neg 0 < A)$
68	67	adantrd	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to ((A < 0 \land B = −∞) \to \neg 0 < A)$
69	64 68	jaod	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to (((B < 0 \land A = −∞) \lor (A < 0 \land B = −∞)) \to \neg 0 < A)$
70	62 69	orim12d	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to ((((0 < B \land A = +∞) \lor (0 < A \land B = +∞)) \lor ((B < 0 \land A = −∞) \lor (A < 0 \land B = −∞))) \to (\neg B = −∞ \lor \neg 0 < A))$
71		ianor	$⊢ \neg (0 < A \land B = −∞) \leftrightarrow (\neg 0 < A \lor \neg B = −∞)$
72		orcom	$⊢ (\neg 0 < A \lor \neg B = −∞) \leftrightarrow (\neg B = −∞ \lor \neg 0 < A)$
73	71 72	bitri	$⊢ \neg (0 < A \land B = −∞) \leftrightarrow (\neg B = −∞ \lor \neg 0 < A)$
74	70 73	imbitrrdi	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to ((((0 < B \land A = +∞) \lor (0 < A \land B = +∞)) \lor ((B < 0 \land A = −∞) \lor (A < 0 \land B = −∞))) \to \neg (0 < A \land B = −∞))$
75	42	adantl	$⊢ (0 < B \land A = +∞) \to \neg A < 0$
76	75	a1i	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to ((0 < B \land A = +∞) \to \neg A < 0)$
77	67	con2d	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to (0 < A \to \neg A < 0)$
78	77	adantrd	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to ((0 < A \land B = +∞) \to \neg A < 0)$
79	76 78	jaod	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to (((0 < B \land A = +∞) \lor (0 < A \land B = +∞)) \to \neg A < 0)$
80		breq1	$⊢ B = +∞ \to (B < 0 \leftrightarrow +∞ < 0)$
81	33 80	mtbiri	$⊢ B = +∞ \to \neg B < 0$
82	81	con2i	$⊢ B < 0 \to \neg B = +∞$
83	82	adantr	$⊢ (B < 0 \land A = −∞) \to \neg B = +∞$
84	59	con2i	$⊢ B = −∞ \to \neg B = +∞$
85	84	adantl	$⊢ (A < 0 \land B = −∞) \to \neg B = +∞$
86	83 85	jaoi	$⊢ ((B < 0 \land A = −∞) \lor (A < 0 \land B = −∞)) \to \neg B = +∞$
87	86	a1i	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to (((B < 0 \land A = −∞) \lor (A < 0 \land B = −∞)) \to \neg B = +∞)$
88	79 87	orim12d	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to ((((0 < B \land A = +∞) \lor (0 < A \land B = +∞)) \lor ((B < 0 \land A = −∞) \lor (A < 0 \land B = −∞))) \to (\neg A < 0 \lor \neg B = +∞))$
89		ianor	$⊢ \neg (A < 0 \land B = +∞) \leftrightarrow (\neg A < 0 \lor \neg B = +∞)$
90	88 89	imbitrrdi	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to ((((0 < B \land A = +∞) \lor (0 < A \land B = +∞)) \lor ((B < 0 \land A = −∞) \lor (A < 0 \land B = −∞))) \to \neg (A < 0 \land B = +∞))$
91	74 90	jcad	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to ((((0 < B \land A = +∞) \lor (0 < A \land B = +∞)) \lor ((B < 0 \land A = −∞) \lor (A < 0 \land B = −∞))) \to (\neg (0 < A \land B = −∞) \land \neg (A < 0 \land B = +∞)))$
92		ioran	$⊢ \neg ((0 < A \land B = −∞) \lor (A < 0 \land B = +∞)) \leftrightarrow (\neg (0 < A \land B = −∞) \land \neg (A < 0 \land B = +∞))$
93	91 92	imbitrrdi	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to ((((0 < B \land A = +∞) \lor (0 < A \land B = +∞)) \lor ((B < 0 \land A = −∞) \lor (A < 0 \land B = −∞))) \to \neg ((0 < A \land B = −∞) \lor (A < 0 \land B = +∞)))$
94	52 93	jcad	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to ((((0 < B \land A = +∞) \lor (0 < A \land B = +∞)) \lor ((B < 0 \land A = −∞) \lor (A < 0 \land B = −∞))) \to (\neg ((0 < B \land A = −∞) \lor (B < 0 \land A = +∞)) \land \neg ((0 < A \land B = −∞) \lor (A < 0 \land B = +∞))))$
95		or4	$⊢ (((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 (0 < A \land B = +∞)) \lor ((B < 0 \land A = −∞) \lor (A < 0 \land B = −∞)))$
96		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 = +∞)))$
97	94 95 96	3imtr4g	$⊢ (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 = +∞))))$

Metamath Proof Explorer

Theorem xmullem2

Proof