Proof of Theorem xsubge0
Step | Hyp | Ref
| Expression |
1 | | elxr 11826 |
. 2
⊢ (𝐵 ∈ ℝ*
↔ (𝐵 ∈ ℝ
∨ 𝐵 = +∞ ∨
𝐵 =
-∞)) |
2 | | 0xr 9965 |
. . . . . 6
⊢ 0 ∈
ℝ* |
3 | 2 | a1i 11 |
. . . . 5
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈ ℝ)
→ 0 ∈ ℝ*) |
4 | | rexr 9964 |
. . . . . 6
⊢ (𝐵 ∈ ℝ → 𝐵 ∈
ℝ*) |
5 | | xnegcl 11918 |
. . . . . . 7
⊢ (𝐵 ∈ ℝ*
→ -𝑒𝐵 ∈
ℝ*) |
6 | | xaddcl 11944 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ*
∧ -𝑒𝐵 ∈ ℝ*) → (𝐴 +𝑒
-𝑒𝐵)
∈ ℝ*) |
7 | 5, 6 | sylan2 490 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) → (𝐴 +𝑒
-𝑒𝐵)
∈ ℝ*) |
8 | 4, 7 | sylan2 490 |
. . . . 5
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈ ℝ)
→ (𝐴
+𝑒 -𝑒𝐵) ∈
ℝ*) |
9 | | simpr 476 |
. . . . 5
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈ ℝ)
→ 𝐵 ∈
ℝ) |
10 | | xleadd1 11957 |
. . . . 5
⊢ ((0
∈ ℝ* ∧ (𝐴 +𝑒
-𝑒𝐵)
∈ ℝ* ∧ 𝐵 ∈ ℝ) → (0 ≤ (𝐴 +𝑒
-𝑒𝐵)
↔ (0 +𝑒 𝐵) ≤ ((𝐴 +𝑒
-𝑒𝐵)
+𝑒 𝐵))) |
11 | 3, 8, 9, 10 | syl3anc 1318 |
. . . 4
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈ ℝ)
→ (0 ≤ (𝐴
+𝑒 -𝑒𝐵) ↔ (0 +𝑒 𝐵) ≤ ((𝐴 +𝑒
-𝑒𝐵)
+𝑒 𝐵))) |
12 | 4 | adantl 481 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈ ℝ)
→ 𝐵 ∈
ℝ*) |
13 | | xaddid2 11947 |
. . . . . 6
⊢ (𝐵 ∈ ℝ*
→ (0 +𝑒 𝐵) = 𝐵) |
14 | 12, 13 | syl 17 |
. . . . 5
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈ ℝ)
→ (0 +𝑒 𝐵) = 𝐵) |
15 | | xnpcan 11954 |
. . . . 5
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈ ℝ)
→ ((𝐴
+𝑒 -𝑒𝐵) +𝑒 𝐵) = 𝐴) |
16 | 14, 15 | breq12d 4596 |
. . . 4
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈ ℝ)
→ ((0 +𝑒 𝐵) ≤ ((𝐴 +𝑒
-𝑒𝐵)
+𝑒 𝐵)
↔ 𝐵 ≤ 𝐴)) |
17 | 11, 16 | bitrd 267 |
. . 3
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈ ℝ)
→ (0 ≤ (𝐴
+𝑒 -𝑒𝐵) ↔ 𝐵 ≤ 𝐴)) |
18 | | pnfxr 9971 |
. . . . . . 7
⊢ +∞
∈ ℝ* |
19 | | xrletri3 11861 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ*
∧ +∞ ∈ ℝ*) → (𝐴 = +∞ ↔ (𝐴 ≤ +∞ ∧ +∞ ≤ 𝐴))) |
20 | 18, 19 | mpan2 703 |
. . . . . 6
⊢ (𝐴 ∈ ℝ*
→ (𝐴 = +∞ ↔
(𝐴 ≤ +∞ ∧
+∞ ≤ 𝐴))) |
21 | | mnflt0 11835 |
. . . . . . . . . . 11
⊢ -∞
< 0 |
22 | | mnfxr 9975 |
. . . . . . . . . . . 12
⊢ -∞
∈ ℝ* |
23 | | xrltnle 9984 |
. . . . . . . . . . . 12
⊢
((-∞ ∈ ℝ* ∧ 0 ∈
ℝ*) → (-∞ < 0 ↔ ¬ 0 ≤
-∞)) |
24 | 22, 2, 23 | mp2an 704 |
. . . . . . . . . . 11
⊢ (-∞
< 0 ↔ ¬ 0 ≤ -∞) |
25 | 21, 24 | mpbi 219 |
. . . . . . . . . 10
⊢ ¬ 0
≤ -∞ |
26 | | xaddmnf1 11933 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ*
∧ 𝐴 ≠ +∞)
→ (𝐴
+𝑒 -∞) = -∞) |
27 | 26 | breq2d 4595 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ*
∧ 𝐴 ≠ +∞)
→ (0 ≤ (𝐴
+𝑒 -∞) ↔ 0 ≤ -∞)) |
28 | 25, 27 | mtbiri 316 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ*
∧ 𝐴 ≠ +∞)
→ ¬ 0 ≤ (𝐴
+𝑒 -∞)) |
29 | 28 | ex 449 |
. . . . . . . 8
⊢ (𝐴 ∈ ℝ*
→ (𝐴 ≠ +∞
→ ¬ 0 ≤ (𝐴
+𝑒 -∞))) |
30 | 29 | necon4ad 2801 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ*
→ (0 ≤ (𝐴
+𝑒 -∞) → 𝐴 = +∞)) |
31 | | 0le0 10987 |
. . . . . . . 8
⊢ 0 ≤
0 |
32 | | oveq1 6556 |
. . . . . . . . 9
⊢ (𝐴 = +∞ → (𝐴 +𝑒 -∞)
= (+∞ +𝑒 -∞)) |
33 | | pnfaddmnf 11935 |
. . . . . . . . 9
⊢ (+∞
+𝑒 -∞) = 0 |
34 | 32, 33 | syl6eq 2660 |
. . . . . . . 8
⊢ (𝐴 = +∞ → (𝐴 +𝑒 -∞)
= 0) |
35 | 31, 34 | syl5breqr 4621 |
. . . . . . 7
⊢ (𝐴 = +∞ → 0 ≤ (𝐴 +𝑒
-∞)) |
36 | 30, 35 | impbid1 214 |
. . . . . 6
⊢ (𝐴 ∈ ℝ*
→ (0 ≤ (𝐴
+𝑒 -∞) ↔ 𝐴 = +∞)) |
37 | | pnfge 11840 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ*
→ 𝐴 ≤
+∞) |
38 | 37 | biantrurd 528 |
. . . . . 6
⊢ (𝐴 ∈ ℝ*
→ (+∞ ≤ 𝐴
↔ (𝐴 ≤ +∞
∧ +∞ ≤ 𝐴))) |
39 | 20, 36, 38 | 3bitr4d 299 |
. . . . 5
⊢ (𝐴 ∈ ℝ*
→ (0 ≤ (𝐴
+𝑒 -∞) ↔ +∞ ≤ 𝐴)) |
40 | 39 | adantr 480 |
. . . 4
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 = +∞) →
(0 ≤ (𝐴
+𝑒 -∞) ↔ +∞ ≤ 𝐴)) |
41 | | xnegeq 11912 |
. . . . . . . 8
⊢ (𝐵 = +∞ →
-𝑒𝐵 =
-𝑒+∞) |
42 | | xnegpnf 11914 |
. . . . . . . 8
⊢
-𝑒+∞ = -∞ |
43 | 41, 42 | syl6eq 2660 |
. . . . . . 7
⊢ (𝐵 = +∞ →
-𝑒𝐵 =
-∞) |
44 | 43 | adantl 481 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 = +∞) →
-𝑒𝐵 =
-∞) |
45 | 44 | oveq2d 6565 |
. . . . 5
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 = +∞) →
(𝐴 +𝑒
-𝑒𝐵) =
(𝐴 +𝑒
-∞)) |
46 | 45 | breq2d 4595 |
. . . 4
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 = +∞) →
(0 ≤ (𝐴
+𝑒 -𝑒𝐵) ↔ 0 ≤ (𝐴 +𝑒
-∞))) |
47 | | breq1 4586 |
. . . . 5
⊢ (𝐵 = +∞ → (𝐵 ≤ 𝐴 ↔ +∞ ≤ 𝐴)) |
48 | 47 | adantl 481 |
. . . 4
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 = +∞) →
(𝐵 ≤ 𝐴 ↔ +∞ ≤ 𝐴)) |
49 | 40, 46, 48 | 3bitr4d 299 |
. . 3
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 = +∞) →
(0 ≤ (𝐴
+𝑒 -𝑒𝐵) ↔ 𝐵 ≤ 𝐴)) |
50 | | oveq1 6556 |
. . . . . . . . . 10
⊢ (𝐴 = -∞ → (𝐴 +𝑒 +∞)
= (-∞ +𝑒 +∞)) |
51 | | mnfaddpnf 11936 |
. . . . . . . . . 10
⊢ (-∞
+𝑒 +∞) = 0 |
52 | 50, 51 | syl6eq 2660 |
. . . . . . . . 9
⊢ (𝐴 = -∞ → (𝐴 +𝑒 +∞)
= 0) |
53 | 52 | adantl 481 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ*
∧ 𝐴 = -∞) →
(𝐴 +𝑒
+∞) = 0) |
54 | 31, 53 | syl5breqr 4621 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ*
∧ 𝐴 = -∞) →
0 ≤ (𝐴
+𝑒 +∞)) |
55 | | 0lepnf 11842 |
. . . . . . . 8
⊢ 0 ≤
+∞ |
56 | | xaddpnf1 11931 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ*
∧ 𝐴 ≠ -∞)
→ (𝐴
+𝑒 +∞) = +∞) |
57 | 55, 56 | syl5breqr 4621 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ*
∧ 𝐴 ≠ -∞)
→ 0 ≤ (𝐴
+𝑒 +∞)) |
58 | 54, 57 | pm2.61dane 2869 |
. . . . . 6
⊢ (𝐴 ∈ ℝ*
→ 0 ≤ (𝐴
+𝑒 +∞)) |
59 | | mnfle 11845 |
. . . . . 6
⊢ (𝐴 ∈ ℝ*
→ -∞ ≤ 𝐴) |
60 | 58, 59 | 2thd 254 |
. . . . 5
⊢ (𝐴 ∈ ℝ*
→ (0 ≤ (𝐴
+𝑒 +∞) ↔ -∞ ≤ 𝐴)) |
61 | 60 | adantr 480 |
. . . 4
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 = -∞) →
(0 ≤ (𝐴
+𝑒 +∞) ↔ -∞ ≤ 𝐴)) |
62 | | xnegeq 11912 |
. . . . . . . 8
⊢ (𝐵 = -∞ →
-𝑒𝐵 =
-𝑒-∞) |
63 | | xnegmnf 11915 |
. . . . . . . 8
⊢
-𝑒-∞ = +∞ |
64 | 62, 63 | syl6eq 2660 |
. . . . . . 7
⊢ (𝐵 = -∞ →
-𝑒𝐵 =
+∞) |
65 | 64 | adantl 481 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 = -∞) →
-𝑒𝐵 =
+∞) |
66 | 65 | oveq2d 6565 |
. . . . 5
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 = -∞) →
(𝐴 +𝑒
-𝑒𝐵) =
(𝐴 +𝑒
+∞)) |
67 | 66 | breq2d 4595 |
. . . 4
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 = -∞) →
(0 ≤ (𝐴
+𝑒 -𝑒𝐵) ↔ 0 ≤ (𝐴 +𝑒
+∞))) |
68 | | breq1 4586 |
. . . . 5
⊢ (𝐵 = -∞ → (𝐵 ≤ 𝐴 ↔ -∞ ≤ 𝐴)) |
69 | 68 | adantl 481 |
. . . 4
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 = -∞) →
(𝐵 ≤ 𝐴 ↔ -∞ ≤ 𝐴)) |
70 | 61, 67, 69 | 3bitr4d 299 |
. . 3
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 = -∞) →
(0 ≤ (𝐴
+𝑒 -𝑒𝐵) ↔ 𝐵 ≤ 𝐴)) |
71 | 17, 49, 70 | 3jaodan 1386 |
. 2
⊢ ((𝐴 ∈ ℝ*
∧ (𝐵 ∈ ℝ
∨ 𝐵 = +∞ ∨
𝐵 = -∞)) → (0
≤ (𝐴
+𝑒 -𝑒𝐵) ↔ 𝐵 ≤ 𝐴)) |
72 | 1, 71 | sylan2b 491 |
1
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) → (0 ≤ (𝐴 +𝑒
-𝑒𝐵)
↔ 𝐵 ≤ 𝐴)) |