Proof of Theorem infleinflem2
Step | Hyp | Ref
| Expression |
1 | | infleinflem2.r |
. . . 4
⊢ (𝜑 → 𝑅 ∈ ℝ) |
2 | 1 | adantr 481 |
. . 3
⊢ ((𝜑 ∧ 𝑍 = -∞) → 𝑅 ∈ ℝ) |
3 | | simpr 477 |
. . 3
⊢ ((𝜑 ∧ 𝑍 = -∞) → 𝑍 = -∞) |
4 | | simpr 477 |
. . . 4
⊢ ((𝑅 ∈ ℝ ∧ 𝑍 = -∞) → 𝑍 = -∞) |
5 | | mnflt 11957 |
. . . . 5
⊢ (𝑅 ∈ ℝ → -∞
< 𝑅) |
6 | 5 | adantr 481 |
. . . 4
⊢ ((𝑅 ∈ ℝ ∧ 𝑍 = -∞) → -∞
< 𝑅) |
7 | 4, 6 | eqbrtrd 4675 |
. . 3
⊢ ((𝑅 ∈ ℝ ∧ 𝑍 = -∞) → 𝑍 < 𝑅) |
8 | 2, 3, 7 | syl2anc 693 |
. 2
⊢ ((𝜑 ∧ 𝑍 = -∞) → 𝑍 < 𝑅) |
9 | | simpl 473 |
. . 3
⊢ ((𝜑 ∧ ¬ 𝑍 = -∞) → 𝜑) |
10 | | neqne 2802 |
. . . 4
⊢ (¬
𝑍 = -∞ → 𝑍 ≠ -∞) |
11 | 10 | adantl 482 |
. . 3
⊢ ((𝜑 ∧ ¬ 𝑍 = -∞) → 𝑍 ≠ -∞) |
12 | 1 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝑍 ≠ -∞) → 𝑅 ∈ ℝ) |
13 | | id 22 |
. . . . . . . 8
⊢ (𝜑 → 𝜑) |
14 | | infleinflem2.x |
. . . . . . . 8
⊢ (𝜑 → 𝑋 ∈ 𝐵) |
15 | | infleinflem2.b |
. . . . . . . . 9
⊢ (𝜑 → 𝐵 ⊆
ℝ*) |
16 | 15 | sselda 3603 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑋 ∈ 𝐵) → 𝑋 ∈
ℝ*) |
17 | 13, 14, 16 | syl2anc 693 |
. . . . . . 7
⊢ (𝜑 → 𝑋 ∈
ℝ*) |
18 | 17 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑍 ≠ -∞) → 𝑋 ∈
ℝ*) |
19 | | infleinflem2.z |
. . . . . . . . . 10
⊢ (𝜑 → 𝑍 ∈ 𝐴) |
20 | | infleinflem2.a |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐴 ⊆
ℝ*) |
21 | 20 | sselda 3603 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑍 ∈ 𝐴) → 𝑍 ∈
ℝ*) |
22 | 13, 19, 21 | syl2anc 693 |
. . . . . . . . 9
⊢ (𝜑 → 𝑍 ∈
ℝ*) |
23 | 22 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑍 ≠ -∞) → 𝑍 ∈
ℝ*) |
24 | | simpr 477 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑍 ≠ -∞) → 𝑍 ≠ -∞) |
25 | | pnfxr 10092 |
. . . . . . . . . . 11
⊢ +∞
∈ ℝ* |
26 | 25 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → +∞ ∈
ℝ*) |
27 | | peano2rem 10348 |
. . . . . . . . . . . . 13
⊢ (𝑅 ∈ ℝ → (𝑅 − 1) ∈
ℝ) |
28 | 27 | rexrd 10089 |
. . . . . . . . . . . 12
⊢ (𝑅 ∈ ℝ → (𝑅 − 1) ∈
ℝ*) |
29 | 1, 28 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑅 − 1) ∈
ℝ*) |
30 | 15, 14 | sseldd 3604 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑋 ∈
ℝ*) |
31 | | id 22 |
. . . . . . . . . . . . . 14
⊢ (𝑋 ∈ ℝ*
→ 𝑋 ∈
ℝ*) |
32 | | 1re 10039 |
. . . . . . . . . . . . . . . 16
⊢ 1 ∈
ℝ |
33 | 32 | rexri 10097 |
. . . . . . . . . . . . . . 15
⊢ 1 ∈
ℝ* |
34 | 33 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝑋 ∈ ℝ*
→ 1 ∈ ℝ*) |
35 | 31, 34 | xaddcld 12131 |
. . . . . . . . . . . . 13
⊢ (𝑋 ∈ ℝ*
→ (𝑋
+𝑒 1) ∈ ℝ*) |
36 | 30, 35 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑋 +𝑒 1) ∈
ℝ*) |
37 | | infleinflem2.l |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑍 ≤ (𝑋 +𝑒 1)) |
38 | | infleinflem2.t |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑋 < (𝑅 − 2)) |
39 | | oveq1 6657 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑋 = -∞ → (𝑋 +𝑒 1) =
(-∞ +𝑒 1)) |
40 | | renepnf 10087 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (1 ∈
ℝ → 1 ≠ +∞) |
41 | 32, 40 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 1 ≠
+∞ |
42 | | xaddmnf2 12060 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((1
∈ ℝ* ∧ 1 ≠ +∞) → (-∞
+𝑒 1) = -∞) |
43 | 33, 41, 42 | mp2an 708 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (-∞
+𝑒 1) = -∞ |
44 | 43 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑋 = -∞ → (-∞
+𝑒 1) = -∞) |
45 | 39, 44 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑋 = -∞ → (𝑋 +𝑒 1) =
-∞) |
46 | 45 | adantl 482 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑅 ∈ ℝ ∧ 𝑋 = -∞) → (𝑋 +𝑒 1) =
-∞) |
47 | 27 | mnfltd 11958 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑅 ∈ ℝ → -∞
< (𝑅 −
1)) |
48 | 47 | adantr 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑅 ∈ ℝ ∧ 𝑋 = -∞) → -∞
< (𝑅 −
1)) |
49 | 46, 48 | eqbrtrd 4675 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑅 ∈ ℝ ∧ 𝑋 = -∞) → (𝑋 +𝑒 1) <
(𝑅 −
1)) |
50 | 49 | adantlr 751 |
. . . . . . . . . . . . . . 15
⊢ (((𝑅 ∈ ℝ ∧ 𝑋 ∈ ℝ*)
∧ 𝑋 = -∞) →
(𝑋 +𝑒 1)
< (𝑅 −
1)) |
51 | 50 | 3adantl3 1219 |
. . . . . . . . . . . . . 14
⊢ (((𝑅 ∈ ℝ ∧ 𝑋 ∈ ℝ*
∧ 𝑋 < (𝑅 − 2)) ∧ 𝑋 = -∞) → (𝑋 +𝑒 1) <
(𝑅 −
1)) |
52 | | simpl 473 |
. . . . . . . . . . . . . . 15
⊢ (((𝑅 ∈ ℝ ∧ 𝑋 ∈ ℝ*
∧ 𝑋 < (𝑅 − 2)) ∧ ¬ 𝑋 = -∞) → (𝑅 ∈ ℝ ∧ 𝑋 ∈ ℝ*
∧ 𝑋 < (𝑅 − 2))) |
53 | | simpl2 1065 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑅 ∈ ℝ ∧ 𝑋 ∈ ℝ*
∧ 𝑋 < (𝑅 − 2)) ∧ ¬ 𝑋 = -∞) → 𝑋 ∈
ℝ*) |
54 | | neqne 2802 |
. . . . . . . . . . . . . . . . 17
⊢ (¬
𝑋 = -∞ → 𝑋 ≠ -∞) |
55 | 54 | adantl 482 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑅 ∈ ℝ ∧ 𝑋 ∈ ℝ*
∧ 𝑋 < (𝑅 − 2)) ∧ ¬ 𝑋 = -∞) → 𝑋 ≠ -∞) |
56 | | simp2 1062 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑅 ∈ ℝ ∧ 𝑋 ∈ ℝ*
∧ 𝑋 < (𝑅 − 2)) → 𝑋 ∈
ℝ*) |
57 | 25 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑅 ∈ ℝ ∧ 𝑋 ∈ ℝ*
∧ 𝑋 < (𝑅 − 2)) → +∞
∈ ℝ*) |
58 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑅 ∈ ℝ → 𝑅 ∈
ℝ) |
59 | | 2re 11090 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 2 ∈
ℝ |
60 | 59 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑅 ∈ ℝ → 2 ∈
ℝ) |
61 | 58, 60 | resubcld 10458 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑅 ∈ ℝ → (𝑅 − 2) ∈
ℝ) |
62 | 61 | rexrd 10089 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑅 ∈ ℝ → (𝑅 − 2) ∈
ℝ*) |
63 | 62 | 3ad2ant1 1082 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑅 ∈ ℝ ∧ 𝑋 ∈ ℝ*
∧ 𝑋 < (𝑅 − 2)) → (𝑅 − 2) ∈
ℝ*) |
64 | | simp3 1063 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑅 ∈ ℝ ∧ 𝑋 ∈ ℝ*
∧ 𝑋 < (𝑅 − 2)) → 𝑋 < (𝑅 − 2)) |
65 | 61 | ltpnfd 11955 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑅 ∈ ℝ → (𝑅 − 2) <
+∞) |
66 | 65 | 3ad2ant1 1082 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑅 ∈ ℝ ∧ 𝑋 ∈ ℝ*
∧ 𝑋 < (𝑅 − 2)) → (𝑅 − 2) <
+∞) |
67 | 56, 63, 57, 64, 66 | xrlttrd 11990 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑅 ∈ ℝ ∧ 𝑋 ∈ ℝ*
∧ 𝑋 < (𝑅 − 2)) → 𝑋 < +∞) |
68 | 56, 57, 67 | xrltned 39573 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑅 ∈ ℝ ∧ 𝑋 ∈ ℝ*
∧ 𝑋 < (𝑅 − 2)) → 𝑋 ≠ +∞) |
69 | 68 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑅 ∈ ℝ ∧ 𝑋 ∈ ℝ*
∧ 𝑋 < (𝑅 − 2)) ∧ ¬ 𝑋 = -∞) → 𝑋 ≠ +∞) |
70 | 53, 55, 69 | xrred 39581 |
. . . . . . . . . . . . . . 15
⊢ (((𝑅 ∈ ℝ ∧ 𝑋 ∈ ℝ*
∧ 𝑋 < (𝑅 − 2)) ∧ ¬ 𝑋 = -∞) → 𝑋 ∈
ℝ) |
71 | | id 22 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑋 ∈ ℝ → 𝑋 ∈
ℝ) |
72 | 71 | ad2antlr 763 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑅 ∈ ℝ ∧ 𝑋 ∈ ℝ) ∧ 𝑋 < (𝑅 − 2)) → 𝑋 ∈ ℝ) |
73 | 61 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑅 ∈ ℝ ∧ 𝑋 ∈ ℝ) ∧ 𝑋 < (𝑅 − 2)) → (𝑅 − 2) ∈ ℝ) |
74 | | 1red 10055 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑋 ∈ ℝ → 1 ∈
ℝ) |
75 | 72, 74 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑅 ∈ ℝ ∧ 𝑋 ∈ ℝ) ∧ 𝑋 < (𝑅 − 2)) → 1 ∈
ℝ) |
76 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑅 ∈ ℝ ∧ 𝑋 ∈ ℝ) ∧ 𝑋 < (𝑅 − 2)) → 𝑋 < (𝑅 − 2)) |
77 | 72, 73, 75, 76 | ltadd1dd 10638 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑅 ∈ ℝ ∧ 𝑋 ∈ ℝ) ∧ 𝑋 < (𝑅 − 2)) → (𝑋 + 1) < ((𝑅 − 2) + 1)) |
78 | | recn 10026 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑅 ∈ ℝ → 𝑅 ∈
ℂ) |
79 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑅 ∈ ℂ → 𝑅 ∈
ℂ) |
80 | | 2cnd 11093 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑅 ∈ ℂ → 2 ∈
ℂ) |
81 | | 1cnd 10056 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑅 ∈ ℂ → 1 ∈
ℂ) |
82 | 79, 80, 81 | subsubd 10420 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑅 ∈ ℂ → (𝑅 − (2 − 1)) =
((𝑅 − 2) +
1)) |
83 | | 2m1e1 11135 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (2
− 1) = 1 |
84 | 83 | oveq2i 6661 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑅 − (2 − 1)) = (𝑅 − 1) |
85 | 84 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑅 ∈ ℂ → (𝑅 − (2 − 1)) = (𝑅 − 1)) |
86 | 82, 85 | eqtr3d 2658 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑅 ∈ ℂ → ((𝑅 − 2) + 1) = (𝑅 − 1)) |
87 | 78, 86 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑅 ∈ ℝ → ((𝑅 − 2) + 1) = (𝑅 − 1)) |
88 | 87 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑅 ∈ ℝ ∧ 𝑋 ∈ ℝ) ∧ 𝑋 < (𝑅 − 2)) → ((𝑅 − 2) + 1) = (𝑅 − 1)) |
89 | 77, 88 | breqtrd 4679 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑅 ∈ ℝ ∧ 𝑋 ∈ ℝ) ∧ 𝑋 < (𝑅 − 2)) → (𝑋 + 1) < (𝑅 − 1)) |
90 | 71, 74 | rexaddd 12065 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑋 ∈ ℝ → (𝑋 +𝑒 1) =
(𝑋 + 1)) |
91 | 90 | breq1d 4663 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑋 ∈ ℝ → ((𝑋 +𝑒 1) <
(𝑅 − 1) ↔ (𝑋 + 1) < (𝑅 − 1))) |
92 | 91 | ad2antlr 763 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑅 ∈ ℝ ∧ 𝑋 ∈ ℝ) ∧ 𝑋 < (𝑅 − 2)) → ((𝑋 +𝑒 1) < (𝑅 − 1) ↔ (𝑋 + 1) < (𝑅 − 1))) |
93 | 89, 92 | mpbird 247 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑅 ∈ ℝ ∧ 𝑋 ∈ ℝ) ∧ 𝑋 < (𝑅 − 2)) → (𝑋 +𝑒 1) < (𝑅 − 1)) |
94 | 93 | an32s 846 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑅 ∈ ℝ ∧ 𝑋 < (𝑅 − 2)) ∧ 𝑋 ∈ ℝ) → (𝑋 +𝑒 1) < (𝑅 − 1)) |
95 | 94 | 3adantl2 1218 |
. . . . . . . . . . . . . . 15
⊢ (((𝑅 ∈ ℝ ∧ 𝑋 ∈ ℝ*
∧ 𝑋 < (𝑅 − 2)) ∧ 𝑋 ∈ ℝ) → (𝑋 +𝑒 1) <
(𝑅 −
1)) |
96 | 52, 70, 95 | syl2anc 693 |
. . . . . . . . . . . . . 14
⊢ (((𝑅 ∈ ℝ ∧ 𝑋 ∈ ℝ*
∧ 𝑋 < (𝑅 − 2)) ∧ ¬ 𝑋 = -∞) → (𝑋 +𝑒 1) <
(𝑅 −
1)) |
97 | 51, 96 | pm2.61dan 832 |
. . . . . . . . . . . . 13
⊢ ((𝑅 ∈ ℝ ∧ 𝑋 ∈ ℝ*
∧ 𝑋 < (𝑅 − 2)) → (𝑋 +𝑒 1) <
(𝑅 −
1)) |
98 | 1, 30, 38, 97 | syl3anc 1326 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑋 +𝑒 1) < (𝑅 − 1)) |
99 | 22, 36, 29, 37, 98 | xrlelttrd 11991 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑍 < (𝑅 − 1)) |
100 | 27 | ltpnfd 11955 |
. . . . . . . . . . . 12
⊢ (𝑅 ∈ ℝ → (𝑅 − 1) <
+∞) |
101 | 1, 100 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑅 − 1) < +∞) |
102 | 22, 29, 26, 99, 101 | xrlttrd 11990 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑍 < +∞) |
103 | 22, 26, 102 | xrltned 39573 |
. . . . . . . . 9
⊢ (𝜑 → 𝑍 ≠ +∞) |
104 | 103 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑍 ≠ -∞) → 𝑍 ≠ +∞) |
105 | 23, 24, 104 | xrred 39581 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑍 ≠ -∞) → 𝑍 ∈ ℝ) |
106 | 37 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑍 ≠ -∞) → 𝑍 ≤ (𝑋 +𝑒 1)) |
107 | | simpl3 1066 |
. . . . . . . . 9
⊢ (((𝑍 ∈ ℝ ∧ 𝑋 ∈ ℝ*
∧ 𝑍 ≤ (𝑋 +𝑒 1)) ∧
𝑋 = -∞) → 𝑍 ≤ (𝑋 +𝑒 1)) |
108 | 45 | adantl 482 |
. . . . . . . . . . . 12
⊢ ((𝑍 ∈ ℝ ∧ 𝑋 = -∞) → (𝑋 +𝑒 1) =
-∞) |
109 | | mnflt 11957 |
. . . . . . . . . . . . 13
⊢ (𝑍 ∈ ℝ → -∞
< 𝑍) |
110 | 109 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝑍 ∈ ℝ ∧ 𝑋 = -∞) → -∞
< 𝑍) |
111 | 108, 110 | eqbrtrd 4675 |
. . . . . . . . . . 11
⊢ ((𝑍 ∈ ℝ ∧ 𝑋 = -∞) → (𝑋 +𝑒 1) <
𝑍) |
112 | | mnfxr 10096 |
. . . . . . . . . . . . 13
⊢ -∞
∈ ℝ* |
113 | 108, 112 | syl6eqel 2709 |
. . . . . . . . . . . 12
⊢ ((𝑍 ∈ ℝ ∧ 𝑋 = -∞) → (𝑋 +𝑒 1) ∈
ℝ*) |
114 | | rexr 10085 |
. . . . . . . . . . . . 13
⊢ (𝑍 ∈ ℝ → 𝑍 ∈
ℝ*) |
115 | 114 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝑍 ∈ ℝ ∧ 𝑋 = -∞) → 𝑍 ∈
ℝ*) |
116 | 113, 115 | xrltnled 39579 |
. . . . . . . . . . 11
⊢ ((𝑍 ∈ ℝ ∧ 𝑋 = -∞) → ((𝑋 +𝑒 1) <
𝑍 ↔ ¬ 𝑍 ≤ (𝑋 +𝑒 1))) |
117 | 111, 116 | mpbid 222 |
. . . . . . . . . 10
⊢ ((𝑍 ∈ ℝ ∧ 𝑋 = -∞) → ¬ 𝑍 ≤ (𝑋 +𝑒 1)) |
118 | 117 | 3ad2antl1 1223 |
. . . . . . . . 9
⊢ (((𝑍 ∈ ℝ ∧ 𝑋 ∈ ℝ*
∧ 𝑍 ≤ (𝑋 +𝑒 1)) ∧
𝑋 = -∞) → ¬
𝑍 ≤ (𝑋 +𝑒 1)) |
119 | 107, 118 | pm2.65da 600 |
. . . . . . . 8
⊢ ((𝑍 ∈ ℝ ∧ 𝑋 ∈ ℝ*
∧ 𝑍 ≤ (𝑋 +𝑒 1))
→ ¬ 𝑋 =
-∞) |
120 | 119 | neqned 2801 |
. . . . . . 7
⊢ ((𝑍 ∈ ℝ ∧ 𝑋 ∈ ℝ*
∧ 𝑍 ≤ (𝑋 +𝑒 1))
→ 𝑋 ≠
-∞) |
121 | 105, 18, 106, 120 | syl3anc 1326 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑍 ≠ -∞) → 𝑋 ≠ -∞) |
122 | 1, 17, 38, 68 | syl3anc 1326 |
. . . . . . 7
⊢ (𝜑 → 𝑋 ≠ +∞) |
123 | 122 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑍 ≠ -∞) → 𝑋 ≠ +∞) |
124 | 18, 121, 123 | xrred 39581 |
. . . . 5
⊢ ((𝜑 ∧ 𝑍 ≠ -∞) → 𝑋 ∈ ℝ) |
125 | 38 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝑍 ≠ -∞) → 𝑋 < (𝑅 − 2)) |
126 | 12, 124, 125 | jca31 557 |
. . . 4
⊢ ((𝜑 ∧ 𝑍 ≠ -∞) → ((𝑅 ∈ ℝ ∧ 𝑋 ∈ ℝ) ∧ 𝑋 < (𝑅 − 2))) |
127 | | simplr 792 |
. . . . 5
⊢
(((((𝑅 ∈
ℝ ∧ 𝑋 ∈
ℝ) ∧ 𝑋 <
(𝑅 − 2)) ∧ 𝑍 ∈ ℝ) ∧ 𝑍 ≤ (𝑋 +𝑒 1)) → 𝑍 ∈
ℝ) |
128 | | simp-4r 807 |
. . . . . 6
⊢
(((((𝑅 ∈
ℝ ∧ 𝑋 ∈
ℝ) ∧ 𝑋 <
(𝑅 − 2)) ∧ 𝑍 ∈ ℝ) ∧ 𝑍 ≤ (𝑋 +𝑒 1)) → 𝑋 ∈
ℝ) |
129 | 71, 74 | readdcld 10069 |
. . . . . . 7
⊢ (𝑋 ∈ ℝ → (𝑋 + 1) ∈
ℝ) |
130 | 90, 129 | eqeltrd 2701 |
. . . . . 6
⊢ (𝑋 ∈ ℝ → (𝑋 +𝑒 1) ∈
ℝ) |
131 | 128, 130 | syl 17 |
. . . . 5
⊢
(((((𝑅 ∈
ℝ ∧ 𝑋 ∈
ℝ) ∧ 𝑋 <
(𝑅 − 2)) ∧ 𝑍 ∈ ℝ) ∧ 𝑍 ≤ (𝑋 +𝑒 1)) → (𝑋 +𝑒 1) ∈
ℝ) |
132 | 58 | ad4antr 768 |
. . . . 5
⊢
(((((𝑅 ∈
ℝ ∧ 𝑋 ∈
ℝ) ∧ 𝑋 <
(𝑅 − 2)) ∧ 𝑍 ∈ ℝ) ∧ 𝑍 ≤ (𝑋 +𝑒 1)) → 𝑅 ∈
ℝ) |
133 | | simpr 477 |
. . . . 5
⊢
(((((𝑅 ∈
ℝ ∧ 𝑋 ∈
ℝ) ∧ 𝑋 <
(𝑅 − 2)) ∧ 𝑍 ∈ ℝ) ∧ 𝑍 ≤ (𝑋 +𝑒 1)) → 𝑍 ≤ (𝑋 +𝑒 1)) |
134 | 130 | ad3antlr 767 |
. . . . . . 7
⊢ ((((𝑅 ∈ ℝ ∧ 𝑋 ∈ ℝ) ∧ 𝑋 < (𝑅 − 2)) ∧ 𝑍 ∈ ℝ) → (𝑋 +𝑒 1) ∈
ℝ) |
135 | 27 | ad3antrrr 766 |
. . . . . . 7
⊢ ((((𝑅 ∈ ℝ ∧ 𝑋 ∈ ℝ) ∧ 𝑋 < (𝑅 − 2)) ∧ 𝑍 ∈ ℝ) → (𝑅 − 1) ∈ ℝ) |
136 | 58 | ad3antrrr 766 |
. . . . . . 7
⊢ ((((𝑅 ∈ ℝ ∧ 𝑋 ∈ ℝ) ∧ 𝑋 < (𝑅 − 2)) ∧ 𝑍 ∈ ℝ) → 𝑅 ∈ ℝ) |
137 | 93 | adantr 481 |
. . . . . . 7
⊢ ((((𝑅 ∈ ℝ ∧ 𝑋 ∈ ℝ) ∧ 𝑋 < (𝑅 − 2)) ∧ 𝑍 ∈ ℝ) → (𝑋 +𝑒 1) < (𝑅 − 1)) |
138 | 136 | ltm1d 10956 |
. . . . . . 7
⊢ ((((𝑅 ∈ ℝ ∧ 𝑋 ∈ ℝ) ∧ 𝑋 < (𝑅 − 2)) ∧ 𝑍 ∈ ℝ) → (𝑅 − 1) < 𝑅) |
139 | 134, 135,
136, 137, 138 | lttrd 10198 |
. . . . . 6
⊢ ((((𝑅 ∈ ℝ ∧ 𝑋 ∈ ℝ) ∧ 𝑋 < (𝑅 − 2)) ∧ 𝑍 ∈ ℝ) → (𝑋 +𝑒 1) < 𝑅) |
140 | 139 | adantr 481 |
. . . . 5
⊢
(((((𝑅 ∈
ℝ ∧ 𝑋 ∈
ℝ) ∧ 𝑋 <
(𝑅 − 2)) ∧ 𝑍 ∈ ℝ) ∧ 𝑍 ≤ (𝑋 +𝑒 1)) → (𝑋 +𝑒 1) <
𝑅) |
141 | 127, 131,
132, 133, 140 | lelttrd 10195 |
. . . 4
⊢
(((((𝑅 ∈
ℝ ∧ 𝑋 ∈
ℝ) ∧ 𝑋 <
(𝑅 − 2)) ∧ 𝑍 ∈ ℝ) ∧ 𝑍 ≤ (𝑋 +𝑒 1)) → 𝑍 < 𝑅) |
142 | 126, 105,
106, 141 | syl21anc 1325 |
. . 3
⊢ ((𝜑 ∧ 𝑍 ≠ -∞) → 𝑍 < 𝑅) |
143 | 9, 11, 142 | syl2anc 693 |
. 2
⊢ ((𝜑 ∧ ¬ 𝑍 = -∞) → 𝑍 < 𝑅) |
144 | 8, 143 | pm2.61dan 832 |
1
⊢ (𝜑 → 𝑍 < 𝑅) |