This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 biimtrdi ⊢ ( 𝐵 = -∞ → ( -∞ < 𝐵 → -𝑒 𝐵 < +∞ ) )
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 imbitrrid ⊢ ( 𝐴 = -∞ → ( ( 𝐵 ∈ ℝ* ∧ -∞ < 𝐵 ) → -𝑒 𝐵 < -𝑒 𝐴 ) )
60 38 59 sylbid ⊢ ( 𝐴 = -∞ → ( ( 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵 ) → -𝑒 𝐵 < -𝑒 𝐴 ) )
61 29 36 60 3jaoi ⊢ ( ( 𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞ ) → ( ( 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵 ) → -𝑒 𝐵 < -𝑒 𝐴 ) )
62 1 61 sylbi ⊢ ( 𝐴 ∈ ℝ* → ( ( 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵 ) → -𝑒 𝐵 < -𝑒 𝐴 ) )
63 62 3impib ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵 ) → -𝑒 𝐵 < -𝑒 𝐴 )