Theorem xltnegi

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

	Ref	Expression
Assertion	xltnegi	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵 ) → -𝑒 𝐵 < -𝑒 𝐴 )

Proof

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