Step | Hyp | Ref
| Expression |
1 | | elxr 9775 |
. . 3
⊢ (𝐴 ∈ ℝ*
↔ (𝐴 ∈ ℝ
∨ 𝐴 = +∞ ∨
𝐴 =
-∞)) |
2 | | elxr 9775 |
. . . . . 6
⊢ (𝐵 ∈ ℝ*
↔ (𝐵 ∈ ℝ
∨ 𝐵 = +∞ ∨
𝐵 =
-∞)) |
3 | | ltneg 8418 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 ↔ -𝐵 < -𝐴)) |
4 | | rexneg 9829 |
. . . . . . . . . 10
⊢ (𝐵 ∈ ℝ →
-𝑒𝐵 =
-𝐵) |
5 | | rexneg 9829 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℝ →
-𝑒𝐴 =
-𝐴) |
6 | 4, 5 | breqan12rd 4020 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) →
(-𝑒𝐵
< -𝑒𝐴
↔ -𝐵 < -𝐴)) |
7 | 3, 6 | bitr4d 191 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 ↔ -𝑒𝐵 < -𝑒𝐴)) |
8 | 7 | biimpd 144 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 → -𝑒𝐵 < -𝑒𝐴)) |
9 | | xnegeq 9826 |
. . . . . . . . . . 11
⊢ (𝐵 = +∞ →
-𝑒𝐵 =
-𝑒+∞) |
10 | | xnegpnf 9827 |
. . . . . . . . . . 11
⊢
-𝑒+∞ = -∞ |
11 | 9, 10 | eqtrdi 2226 |
. . . . . . . . . 10
⊢ (𝐵 = +∞ →
-𝑒𝐵 =
-∞) |
12 | 11 | adantl 277 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = +∞) →
-𝑒𝐵 =
-∞) |
13 | | renegcl 8217 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ℝ → -𝐴 ∈
ℝ) |
14 | 5, 13 | eqeltrd 2254 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ℝ →
-𝑒𝐴
∈ ℝ) |
15 | | mnflt 9782 |
. . . . . . . . . . 11
⊢
(-𝑒𝐴 ∈ ℝ → -∞ <
-𝑒𝐴) |
16 | 14, 15 | syl 14 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℝ → -∞
< -𝑒𝐴) |
17 | 16 | adantr 276 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = +∞) → -∞
< -𝑒𝐴) |
18 | 12, 17 | eqbrtrd 4025 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = +∞) →
-𝑒𝐵 <
-𝑒𝐴) |
19 | 18 | a1d 22 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = +∞) → (𝐴 < 𝐵 → -𝑒𝐵 < -𝑒𝐴)) |
20 | | simpr 110 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = -∞) → 𝐵 = -∞) |
21 | 20 | breq2d 4015 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = -∞) → (𝐴 < 𝐵 ↔ 𝐴 < -∞)) |
22 | | rexr 8002 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ℝ → 𝐴 ∈
ℝ*) |
23 | | nltmnf 9787 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ℝ*
→ ¬ 𝐴 <
-∞) |
24 | 22, 23 | syl 14 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℝ → ¬
𝐴 <
-∞) |
25 | 24 | adantr 276 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = -∞) → ¬ 𝐴 < -∞) |
26 | 25 | pm2.21d 619 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = -∞) → (𝐴 < -∞ →
-𝑒𝐵 <
-𝑒𝐴)) |
27 | 21, 26 | sylbid 150 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = -∞) → (𝐴 < 𝐵 → -𝑒𝐵 < -𝑒𝐴)) |
28 | 8, 19, 27 | 3jaodan 1306 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∨ 𝐵 = +∞ ∨ 𝐵 = -∞)) → (𝐴 < 𝐵 → -𝑒𝐵 < -𝑒𝐴)) |
29 | 2, 28 | sylan2b 287 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ*)
→ (𝐴 < 𝐵 →
-𝑒𝐵 <
-𝑒𝐴)) |
30 | 29 | expimpd 363 |
. . . 4
⊢ (𝐴 ∈ ℝ → ((𝐵 ∈ ℝ*
∧ 𝐴 < 𝐵) →
-𝑒𝐵 <
-𝑒𝐴)) |
31 | | simpl 109 |
. . . . . . 7
⊢ ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ*)
→ 𝐴 =
+∞) |
32 | 31 | breq1d 4013 |
. . . . . 6
⊢ ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ*)
→ (𝐴 < 𝐵 ↔ +∞ < 𝐵)) |
33 | | pnfnlt 9786 |
. . . . . . . 8
⊢ (𝐵 ∈ ℝ*
→ ¬ +∞ < 𝐵) |
34 | 33 | adantl 277 |
. . . . . . 7
⊢ ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ*)
→ ¬ +∞ < 𝐵) |
35 | 34 | pm2.21d 619 |
. . . . . 6
⊢ ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ*)
→ (+∞ < 𝐵
→ -𝑒𝐵 < -𝑒𝐴)) |
36 | 32, 35 | sylbid 150 |
. . . . 5
⊢ ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ*)
→ (𝐴 < 𝐵 →
-𝑒𝐵 <
-𝑒𝐴)) |
37 | 36 | expimpd 363 |
. . . 4
⊢ (𝐴 = +∞ → ((𝐵 ∈ ℝ*
∧ 𝐴 < 𝐵) →
-𝑒𝐵 <
-𝑒𝐴)) |
38 | | breq1 4006 |
. . . . . 6
⊢ (𝐴 = -∞ → (𝐴 < 𝐵 ↔ -∞ < 𝐵)) |
39 | 38 | anbi2d 464 |
. . . . 5
⊢ (𝐴 = -∞ → ((𝐵 ∈ ℝ*
∧ 𝐴 < 𝐵) ↔ (𝐵 ∈ ℝ* ∧ -∞
< 𝐵))) |
40 | | renegcl 8217 |
. . . . . . . . . . 11
⊢ (𝐵 ∈ ℝ → -𝐵 ∈
ℝ) |
41 | 4, 40 | eqeltrd 2254 |
. . . . . . . . . 10
⊢ (𝐵 ∈ ℝ →
-𝑒𝐵
∈ ℝ) |
42 | 41 | adantr 276 |
. . . . . . . . 9
⊢ ((𝐵 ∈ ℝ ∧ -∞
< 𝐵) →
-𝑒𝐵
∈ ℝ) |
43 | | ltpnf 9779 |
. . . . . . . . 9
⊢
(-𝑒𝐵 ∈ ℝ →
-𝑒𝐵 <
+∞) |
44 | 42, 43 | syl 14 |
. . . . . . . 8
⊢ ((𝐵 ∈ ℝ ∧ -∞
< 𝐵) →
-𝑒𝐵 <
+∞) |
45 | 11 | adantr 276 |
. . . . . . . . 9
⊢ ((𝐵 = +∞ ∧ -∞ <
𝐵) →
-𝑒𝐵 =
-∞) |
46 | | mnfltpnf 9784 |
. . . . . . . . 9
⊢ -∞
< +∞ |
47 | 45, 46 | eqbrtrdi 4042 |
. . . . . . . 8
⊢ ((𝐵 = +∞ ∧ -∞ <
𝐵) →
-𝑒𝐵 <
+∞) |
48 | | breq2 4007 |
. . . . . . . . . 10
⊢ (𝐵 = -∞ → (-∞
< 𝐵 ↔ -∞ <
-∞)) |
49 | | mnfxr 8013 |
. . . . . . . . . . . 12
⊢ -∞
∈ ℝ* |
50 | | nltmnf 9787 |
. . . . . . . . . . . 12
⊢ (-∞
∈ ℝ* → ¬ -∞ <
-∞) |
51 | 49, 50 | ax-mp 5 |
. . . . . . . . . . 11
⊢ ¬
-∞ < -∞ |
52 | 51 | pm2.21i 646 |
. . . . . . . . . 10
⊢ (-∞
< -∞ → -𝑒𝐵 < +∞) |
53 | 48, 52 | syl6bi 163 |
. . . . . . . . 9
⊢ (𝐵 = -∞ → (-∞
< 𝐵 →
-𝑒𝐵 <
+∞)) |
54 | 53 | imp 124 |
. . . . . . . 8
⊢ ((𝐵 = -∞ ∧ -∞ <
𝐵) →
-𝑒𝐵 <
+∞) |
55 | 44, 47, 54 | 3jaoian 1305 |
. . . . . . 7
⊢ (((𝐵 ∈ ℝ ∨ 𝐵 = +∞ ∨ 𝐵 = -∞) ∧ -∞ <
𝐵) →
-𝑒𝐵 <
+∞) |
56 | 2, 55 | sylanb 284 |
. . . . . 6
⊢ ((𝐵 ∈ ℝ*
∧ -∞ < 𝐵)
→ -𝑒𝐵 < +∞) |
57 | | xnegeq 9826 |
. . . . . . . 8
⊢ (𝐴 = -∞ →
-𝑒𝐴 =
-𝑒-∞) |
58 | | xnegmnf 9828 |
. . . . . . . 8
⊢
-𝑒-∞ = +∞ |
59 | 57, 58 | eqtrdi 2226 |
. . . . . . 7
⊢ (𝐴 = -∞ →
-𝑒𝐴 =
+∞) |
60 | 59 | breq2d 4015 |
. . . . . 6
⊢ (𝐴 = -∞ →
(-𝑒𝐵
< -𝑒𝐴
↔ -𝑒𝐵 < +∞)) |
61 | 56, 60 | imbitrrid 156 |
. . . . 5
⊢ (𝐴 = -∞ → ((𝐵 ∈ ℝ*
∧ -∞ < 𝐵)
→ -𝑒𝐵 < -𝑒𝐴)) |
62 | 39, 61 | sylbid 150 |
. . . 4
⊢ (𝐴 = -∞ → ((𝐵 ∈ ℝ*
∧ 𝐴 < 𝐵) →
-𝑒𝐵 <
-𝑒𝐴)) |
63 | 30, 37, 62 | 3jaoi 1303 |
. . 3
⊢ ((𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞) → ((𝐵 ∈ ℝ*
∧ 𝐴 < 𝐵) →
-𝑒𝐵 <
-𝑒𝐴)) |
64 | 1, 63 | sylbi 121 |
. 2
⊢ (𝐴 ∈ ℝ*
→ ((𝐵 ∈
ℝ* ∧ 𝐴
< 𝐵) →
-𝑒𝐵 <
-𝑒𝐴)) |
65 | 64 | 3impib 1201 |
1
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐴
< 𝐵) →
-𝑒𝐵 <
-𝑒𝐴) |