Proof of Theorem xrsdsreclblem
Step | Hyp | Ref
| Expression |
1 | | necom 3039 |
. . . . 5
⊢ (𝐴 ≠ 𝐵 ↔ 𝐵 ≠ 𝐴) |
2 | | xrleltne 12392 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐴
≤ 𝐵) → (𝐴 < 𝐵 ↔ 𝐵 ≠ 𝐴)) |
3 | | mnfxr 10551 |
. . . . . . . . . . . 12
⊢ -∞
∈ ℝ* |
4 | 3 | a1i 11 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐴
< 𝐵) ∧ (𝐵 +𝑒
-𝑒𝐴)
∈ ℝ) → -∞ ∈ ℝ*) |
5 | | simpl1 1184 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐴
< 𝐵) ∧ (𝐵 +𝑒
-𝑒𝐴)
∈ ℝ) → 𝐴
∈ ℝ*) |
6 | | simpl2 1185 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐴
< 𝐵) ∧ (𝐵 +𝑒
-𝑒𝐴)
∈ ℝ) → 𝐵
∈ ℝ*) |
7 | | pnfnre 10535 |
. . . . . . . . . . . . . 14
⊢ +∞
∉ ℝ |
8 | 7 | neli 3094 |
. . . . . . . . . . . . 13
⊢ ¬
+∞ ∈ ℝ |
9 | | mnfle 12383 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐴 ∈ ℝ*
→ -∞ ≤ 𝐴) |
10 | 5, 9 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐴
< 𝐵) ∧ (𝐵 +𝑒
-𝑒𝐴)
∈ ℝ) → -∞ ≤ 𝐴) |
11 | | simpl3 1186 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐴
< 𝐵) ∧ (𝐵 +𝑒
-𝑒𝐴)
∈ ℝ) → 𝐴
< 𝐵) |
12 | 4, 5, 6, 10, 11 | xrlelttrd 12407 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐴
< 𝐵) ∧ (𝐵 +𝑒
-𝑒𝐴)
∈ ℝ) → -∞ < 𝐵) |
13 | | xrltne 12410 |
. . . . . . . . . . . . . . . 16
⊢
((-∞ ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ -∞
< 𝐵) → 𝐵 ≠ -∞) |
14 | 4, 6, 12, 13 | syl3anc 1364 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐴
< 𝐵) ∧ (𝐵 +𝑒
-𝑒𝐴)
∈ ℝ) → 𝐵
≠ -∞) |
15 | | xaddpnf1 12473 |
. . . . . . . . . . . . . . 15
⊢ ((𝐵 ∈ ℝ*
∧ 𝐵 ≠ -∞)
→ (𝐵
+𝑒 +∞) = +∞) |
16 | 6, 14, 15 | syl2anc 584 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐴
< 𝐵) ∧ (𝐵 +𝑒
-𝑒𝐴)
∈ ℝ) → (𝐵
+𝑒 +∞) = +∞) |
17 | 16 | eleq1d 2869 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐴
< 𝐵) ∧ (𝐵 +𝑒
-𝑒𝐴)
∈ ℝ) → ((𝐵
+𝑒 +∞) ∈ ℝ ↔ +∞ ∈
ℝ)) |
18 | 8, 17 | mtbiri 328 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐴
< 𝐵) ∧ (𝐵 +𝑒
-𝑒𝐴)
∈ ℝ) → ¬ (𝐵 +𝑒 +∞) ∈
ℝ) |
19 | | ngtmnft 12413 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ ℝ*
→ (𝐴 = -∞ ↔
¬ -∞ < 𝐴)) |
20 | 5, 19 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐴
< 𝐵) ∧ (𝐵 +𝑒
-𝑒𝐴)
∈ ℝ) → (𝐴 =
-∞ ↔ ¬ -∞ < 𝐴)) |
21 | | simpr 485 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐴
< 𝐵) ∧ (𝐵 +𝑒
-𝑒𝐴)
∈ ℝ) → (𝐵
+𝑒 -𝑒𝐴) ∈ ℝ) |
22 | | xnegeq 12454 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐴 = -∞ →
-𝑒𝐴 =
-𝑒-∞) |
23 | | xnegmnf 12457 |
. . . . . . . . . . . . . . . . 17
⊢
-𝑒-∞ = +∞ |
24 | 22, 23 | syl6eq 2849 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 = -∞ →
-𝑒𝐴 =
+∞) |
25 | 24 | oveq2d 7039 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 = -∞ → (𝐵 +𝑒
-𝑒𝐴) =
(𝐵 +𝑒
+∞)) |
26 | 25 | eleq1d 2869 |
. . . . . . . . . . . . . 14
⊢ (𝐴 = -∞ → ((𝐵 +𝑒
-𝑒𝐴)
∈ ℝ ↔ (𝐵
+𝑒 +∞) ∈ ℝ)) |
27 | 21, 26 | syl5ibcom 246 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐴
< 𝐵) ∧ (𝐵 +𝑒
-𝑒𝐴)
∈ ℝ) → (𝐴 =
-∞ → (𝐵
+𝑒 +∞) ∈ ℝ)) |
28 | 20, 27 | sylbird 261 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐴
< 𝐵) ∧ (𝐵 +𝑒
-𝑒𝐴)
∈ ℝ) → (¬ -∞ < 𝐴 → (𝐵 +𝑒 +∞) ∈
ℝ)) |
29 | 18, 28 | mt3d 150 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐴
< 𝐵) ∧ (𝐵 +𝑒
-𝑒𝐴)
∈ ℝ) → -∞ < 𝐴) |
30 | | xrre2 12417 |
. . . . . . . . . . 11
⊢
(((-∞ ∈ ℝ* ∧ 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*)
∧ (-∞ < 𝐴
∧ 𝐴 < 𝐵)) → 𝐴 ∈ ℝ) |
31 | 4, 5, 6, 29, 11, 30 | syl32anc 1371 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐴
< 𝐵) ∧ (𝐵 +𝑒
-𝑒𝐴)
∈ ℝ) → 𝐴
∈ ℝ) |
32 | | pnfxr 10548 |
. . . . . . . . . . . 12
⊢ +∞
∈ ℝ* |
33 | 32 | a1i 11 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐴
< 𝐵) ∧ (𝐵 +𝑒
-𝑒𝐴)
∈ ℝ) → +∞ ∈ ℝ*) |
34 | 5 | xnegcld 12547 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐴
< 𝐵) ∧ (𝐵 +𝑒
-𝑒𝐴)
∈ ℝ) → -𝑒𝐴 ∈
ℝ*) |
35 | | xnegpnf 12456 |
. . . . . . . . . . . . . . . . 17
⊢
-𝑒+∞ = -∞ |
36 | | pnfge 12379 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝐵 ∈ ℝ*
→ 𝐵 ≤
+∞) |
37 | 6, 36 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐴
< 𝐵) ∧ (𝐵 +𝑒
-𝑒𝐴)
∈ ℝ) → 𝐵
≤ +∞) |
38 | 5, 6, 33, 11, 37 | xrltletrd 12408 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐴
< 𝐵) ∧ (𝐵 +𝑒
-𝑒𝐴)
∈ ℝ) → 𝐴
< +∞) |
39 | | xltnegi 12463 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐴 ∈ ℝ*
∧ +∞ ∈ ℝ* ∧ 𝐴 < +∞) →
-𝑒+∞ < -𝑒𝐴) |
40 | 5, 33, 38, 39 | syl3anc 1364 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐴
< 𝐵) ∧ (𝐵 +𝑒
-𝑒𝐴)
∈ ℝ) → -𝑒+∞ <
-𝑒𝐴) |
41 | 35, 40 | eqbrtrrid 5004 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐴
< 𝐵) ∧ (𝐵 +𝑒
-𝑒𝐴)
∈ ℝ) → -∞ < -𝑒𝐴) |
42 | | xrltne 12410 |
. . . . . . . . . . . . . . . 16
⊢
((-∞ ∈ ℝ* ∧ -𝑒𝐴 ∈ ℝ*
∧ -∞ < -𝑒𝐴) → -𝑒𝐴 ≠ -∞) |
43 | 4, 34, 41, 42 | syl3anc 1364 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐴
< 𝐵) ∧ (𝐵 +𝑒
-𝑒𝐴)
∈ ℝ) → -𝑒𝐴 ≠ -∞) |
44 | | xaddpnf2 12474 |
. . . . . . . . . . . . . . 15
⊢
((-𝑒𝐴 ∈ ℝ* ∧
-𝑒𝐴 ≠
-∞) → (+∞ +𝑒 -𝑒𝐴) = +∞) |
45 | 34, 43, 44 | syl2anc 584 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐴
< 𝐵) ∧ (𝐵 +𝑒
-𝑒𝐴)
∈ ℝ) → (+∞ +𝑒
-𝑒𝐴) =
+∞) |
46 | 45 | eleq1d 2869 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐴
< 𝐵) ∧ (𝐵 +𝑒
-𝑒𝐴)
∈ ℝ) → ((+∞ +𝑒
-𝑒𝐴)
∈ ℝ ↔ +∞ ∈ ℝ)) |
47 | 8, 46 | mtbiri 328 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐴
< 𝐵) ∧ (𝐵 +𝑒
-𝑒𝐴)
∈ ℝ) → ¬ (+∞ +𝑒
-𝑒𝐴)
∈ ℝ) |
48 | | nltpnft 12411 |
. . . . . . . . . . . . . 14
⊢ (𝐵 ∈ ℝ*
→ (𝐵 = +∞ ↔
¬ 𝐵 <
+∞)) |
49 | 6, 48 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐴
< 𝐵) ∧ (𝐵 +𝑒
-𝑒𝐴)
∈ ℝ) → (𝐵 =
+∞ ↔ ¬ 𝐵
< +∞)) |
50 | | oveq1 7030 |
. . . . . . . . . . . . . . 15
⊢ (𝐵 = +∞ → (𝐵 +𝑒
-𝑒𝐴) =
(+∞ +𝑒 -𝑒𝐴)) |
51 | 50 | eleq1d 2869 |
. . . . . . . . . . . . . 14
⊢ (𝐵 = +∞ → ((𝐵 +𝑒
-𝑒𝐴)
∈ ℝ ↔ (+∞ +𝑒
-𝑒𝐴)
∈ ℝ)) |
52 | 21, 51 | syl5ibcom 246 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐴
< 𝐵) ∧ (𝐵 +𝑒
-𝑒𝐴)
∈ ℝ) → (𝐵 =
+∞ → (+∞ +𝑒 -𝑒𝐴) ∈
ℝ)) |
53 | 49, 52 | sylbird 261 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐴
< 𝐵) ∧ (𝐵 +𝑒
-𝑒𝐴)
∈ ℝ) → (¬ 𝐵 < +∞ → (+∞
+𝑒 -𝑒𝐴) ∈ ℝ)) |
54 | 47, 53 | mt3d 150 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐴
< 𝐵) ∧ (𝐵 +𝑒
-𝑒𝐴)
∈ ℝ) → 𝐵
< +∞) |
55 | | xrre2 12417 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ +∞ ∈ ℝ*) ∧ (𝐴 < 𝐵 ∧ 𝐵 < +∞)) → 𝐵 ∈ ℝ) |
56 | 5, 6, 33, 11, 54, 55 | syl32anc 1371 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐴
< 𝐵) ∧ (𝐵 +𝑒
-𝑒𝐴)
∈ ℝ) → 𝐵
∈ ℝ) |
57 | 31, 56 | jca 512 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐴
< 𝐵) ∧ (𝐵 +𝑒
-𝑒𝐴)
∈ ℝ) → (𝐴
∈ ℝ ∧ 𝐵
∈ ℝ)) |
58 | 57 | ex 413 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐴
< 𝐵) → ((𝐵 +𝑒
-𝑒𝐴)
∈ ℝ → (𝐴
∈ ℝ ∧ 𝐵
∈ ℝ))) |
59 | 58 | 3expia 1114 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) → (𝐴 < 𝐵 → ((𝐵 +𝑒
-𝑒𝐴)
∈ ℝ → (𝐴
∈ ℝ ∧ 𝐵
∈ ℝ)))) |
60 | 59 | 3adant3 1125 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐴
≤ 𝐵) → (𝐴 < 𝐵 → ((𝐵 +𝑒
-𝑒𝐴)
∈ ℝ → (𝐴
∈ ℝ ∧ 𝐵
∈ ℝ)))) |
61 | 2, 60 | sylbird 261 |
. . . . 5
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐴
≤ 𝐵) → (𝐵 ≠ 𝐴 → ((𝐵 +𝑒
-𝑒𝐴)
∈ ℝ → (𝐴
∈ ℝ ∧ 𝐵
∈ ℝ)))) |
62 | 1, 61 | syl5bi 243 |
. . . 4
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐴
≤ 𝐵) → (𝐴 ≠ 𝐵 → ((𝐵 +𝑒
-𝑒𝐴)
∈ ℝ → (𝐴
∈ ℝ ∧ 𝐵
∈ ℝ)))) |
63 | 62 | 3exp 1112 |
. . 3
⊢ (𝐴 ∈ ℝ*
→ (𝐵 ∈
ℝ* → (𝐴 ≤ 𝐵 → (𝐴 ≠ 𝐵 → ((𝐵 +𝑒
-𝑒𝐴)
∈ ℝ → (𝐴
∈ ℝ ∧ 𝐵
∈ ℝ)))))) |
64 | 63 | com34 91 |
. 2
⊢ (𝐴 ∈ ℝ*
→ (𝐵 ∈
ℝ* → (𝐴 ≠ 𝐵 → (𝐴 ≤ 𝐵 → ((𝐵 +𝑒
-𝑒𝐴)
∈ ℝ → (𝐴
∈ ℝ ∧ 𝐵
∈ ℝ)))))) |
65 | 64 | 3imp1 1340 |
1
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐴
≠ 𝐵) ∧ 𝐴 ≤ 𝐵) → ((𝐵 +𝑒
-𝑒𝐴)
∈ ℝ → (𝐴
∈ ℝ ∧ 𝐵
∈ ℝ))) |