xltnegi

Description: Forward direction of xltneg . (Contributed by Mario Carneiro, 20-Aug-2015)

		Ref	Expression
	Assertion	xltnegi	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land A < B) \to - B < - A$

Proof

Step	Hyp	Ref	Expression
1		elxr	$⊢ A \in ℝ^{*} \leftrightarrow (A \in ℝ \lor A = +∞ \lor A = −∞)$
2		elxr	$⊢ B \in ℝ^{*} \leftrightarrow (B \in ℝ \lor B = +∞ \lor B = −∞)$
3		ltneg	$⊢ (A \in ℝ \land B \in ℝ) \to (A < B \leftrightarrow - B < - A)$
4		rexneg	$⊢ B \in ℝ \to - B = - B$
5		rexneg	$⊢ A \in ℝ \to - A = - A$
6	4 5	breqan12rd	$⊢ (A \in ℝ \land B \in ℝ) \to (- B < - A \leftrightarrow - B < - A)$
7	3 6	bitr4d	$⊢ (A \in ℝ \land B \in ℝ) \to (A < B \leftrightarrow - B < - A)$
8	7	biimpd	$⊢ (A \in ℝ \land B \in ℝ) \to (A < B \to - B < - A)$
9		xnegeq	$⊢ B = +∞ \to - B = - +∞$
10		xnegpnf	$⊢ - +∞ = −∞$
11	9 10	eqtrdi	$⊢ B = +∞ \to - B = −∞$
12	11	adantl	$⊢ (A \in ℝ \land B = +∞) \to - B = −∞$
13		renegcl	$⊢ A \in ℝ \to - A \in ℝ$
14	5 13	eqeltrd	$⊢ A \in ℝ \to - A \in ℝ$
15	14	mnfltd	$⊢ A \in ℝ \to −∞ < - A$
16	15	adantr	$⊢ (A \in ℝ \land B = +∞) \to −∞ < - A$
17	12 16	eqbrtrd	$⊢ (A \in ℝ \land B = +∞) \to - B < - A$
18	17	a1d	$⊢ (A \in ℝ \land B = +∞) \to (A < B \to - B < - A)$
19		simpr	$⊢ (A \in ℝ \land B = −∞) \to B = −∞$
20	19	breq2d	$⊢ (A \in ℝ \land B = −∞) \to (A < B \leftrightarrow A < −∞)$
21		rexr	$⊢ A \in ℝ \to A \in ℝ^{*}$
22		nltmnf	$⊢ A \in ℝ^{*} \to \neg A < −∞$
23	21 22	syl	$⊢ A \in ℝ \to \neg A < −∞$
24	23	adantr	$⊢ (A \in ℝ \land B = −∞) \to \neg A < −∞$
25	24	pm2.21d	$⊢ (A \in ℝ \land B = −∞) \to (A < −∞ \to - B < - A)$
26	20 25	sylbid	$⊢ (A \in ℝ \land B = −∞) \to (A < B \to - B < - A)$
27	8 18 26	3jaodan	$⊢ (A \in ℝ \land (B \in ℝ \lor B = +∞ \lor B = −∞)) \to (A < B \to - B < - A)$
28	2 27	sylan2b	$⊢ (A \in ℝ \land B \in ℝ^{*}) \to (A < B \to - B < - A)$
29	28	expimpd	$⊢ A \in ℝ \to ((B \in ℝ^{*} \land A < B) \to - B < - A)$
30		simpl	$⊢ (A = +∞ \land B \in ℝ^{*}) \to A = +∞$
31	30	breq1d	$⊢ (A = +∞ \land B \in ℝ^{*}) \to (A < B \leftrightarrow +∞ < B)$
32		pnfnlt	$⊢ B \in ℝ^{*} \to \neg +∞ < B$
33	32	adantl	$⊢ (A = +∞ \land B \in ℝ^{*}) \to \neg +∞ < B$
34	33	pm2.21d	$⊢ (A = +∞ \land B \in ℝ^{*}) \to (+∞ < B \to - B < - A)$
35	31 34	sylbid	$⊢ (A = +∞ \land B \in ℝ^{*}) \to (A < B \to - B < - A)$
36	35	expimpd	$⊢ A = +∞ \to ((B \in ℝ^{*} \land A < B) \to - B < - A)$
37		breq1	$⊢ A = −∞ \to (A < B \leftrightarrow −∞ < B)$
38	37	anbi2d	$⊢ A = −∞ \to ((B \in ℝ^{} \land A < B) \leftrightarrow (B \in ℝ^{} \land −∞ < B))$
39		renegcl	$⊢ B \in ℝ \to - B \in ℝ$
40	4 39	eqeltrd	$⊢ B \in ℝ \to - B \in ℝ$
41	40	adantr	$⊢ (B \in ℝ \land −∞ < B) \to - B \in ℝ$
42	41	ltpnfd	$⊢ (B \in ℝ \land −∞ < B) \to - B < +∞$
43	11	adantr	$⊢ (B = +∞ \land −∞ < B) \to - B = −∞$
44		mnfltpnf	$⊢ −∞ < +∞$
45	43 44	eqbrtrdi	$⊢ (B = +∞ \land −∞ < B) \to - B < +∞$
46		breq2	$⊢ B = −∞ \to (−∞ < B \leftrightarrow −∞ < −∞)$
47		mnfxr	$⊢ −∞ \in ℝ^{*}$
48		nltmnf	$⊢ −∞ \in ℝ^{*} \to \neg −∞ < −∞$
49	47 48	ax-mp	$⊢ \neg −∞ < −∞$
50	49	pm2.21i	$⊢ −∞ < −∞ \to - B < +∞$
51	46 50	syl6bi	$⊢ B = −∞ \to (−∞ < B \to - B < +∞)$
52	51	imp	$⊢ (B = −∞ \land −∞ < B) \to - B < +∞$
53	42 45 52	3jaoian	$⊢ ((B \in ℝ \lor B = +∞ \lor B = −∞) \land −∞ < B) \to - B < +∞$
54	2 53	sylanb	$⊢ (B \in ℝ^{*} \land −∞ < B) \to - B < +∞$
55		xnegeq	$⊢ A = −∞ \to - A = - −∞$
56		xnegmnf	$⊢ - −∞ = +∞$
57	55 56	eqtrdi	$⊢ A = −∞ \to - A = +∞$
58	57	breq2d	$⊢ A = −∞ \to (- B < - A \leftrightarrow - B < +∞)$
59	54 58	syl5ibr	$⊢ A = −∞ \to ((B \in ℝ^{*} \land −∞ < B) \to - B < - A)$
60	38 59	sylbid	$⊢ A = −∞ \to ((B \in ℝ^{*} \land A < B) \to - B < - A)$
61	29 36 60	3jaoi	$⊢ (A \in ℝ \lor A = +∞ \lor A = −∞) \to ((B \in ℝ^{*} \land A < B) \to - B < - A)$
62	1 61	sylbi	$⊢ A \in ℝ^{} \to ((B \in ℝ^{} \land A < B) \to - B < - A)$
63	62	3impib	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land A < B) \to - B < - A$

Metamath Proof Explorer

Theorem xltnegi

Proof