Step | Hyp | Ref
| Expression |
1 | | rpssre 12593 |
. . . 4
⊢
ℝ+ ⊆ ℝ |
2 | | eqid 2737 |
. . . . . . . . . . 11
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
3 | 2 | subcn 23763 |
. . . . . . . . . . . 12
⊢ −
∈ (((TopOpen‘ℂfld) ×t
(TopOpen‘ℂfld)) Cn
(TopOpen‘ℂfld)) |
4 | 3 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) →
− ∈ (((TopOpen‘ℂfld) ×t
(TopOpen‘ℂfld)) Cn
(TopOpen‘ℂfld))) |
5 | | ssid 3923 |
. . . . . . . . . . . . 13
⊢ ℂ
⊆ ℂ |
6 | | cncfmptid 23810 |
. . . . . . . . . . . . 13
⊢ ((ℂ
⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑝 ∈ ℂ ↦ 𝑝) ∈ (ℂ–cn→ℂ)) |
7 | 5, 5, 6 | mp2an 692 |
. . . . . . . . . . . 12
⊢ (𝑝 ∈ ℂ ↦ 𝑝) ∈ (ℂ–cn→ℂ) |
8 | 7 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) → (𝑝 ∈ ℂ ↦ 𝑝) ∈ (ℂ–cn→ℂ)) |
9 | | pntlem3.2 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐶 ∈
ℝ+) |
10 | 9 | adantr 484 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) → 𝐶 ∈
ℝ+) |
11 | 10 | rpcnd 12630 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) → 𝐶 ∈
ℂ) |
12 | 5 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) →
ℂ ⊆ ℂ) |
13 | | cncfmptc 23809 |
. . . . . . . . . . . . 13
⊢ ((𝐶 ∈ ℂ ∧ ℂ
⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑝 ∈ ℂ ↦ 𝐶) ∈ (ℂ–cn→ℂ)) |
14 | 11, 12, 12, 13 | syl3anc 1373 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) → (𝑝 ∈ ℂ ↦ 𝐶) ∈ (ℂ–cn→ℂ)) |
15 | | 3nn0 12108 |
. . . . . . . . . . . . . 14
⊢ 3 ∈
ℕ0 |
16 | 2 | expcn 23769 |
. . . . . . . . . . . . . 14
⊢ (3 ∈
ℕ0 → (𝑝 ∈ ℂ ↦ (𝑝↑3)) ∈
((TopOpen‘ℂfld) Cn
(TopOpen‘ℂfld))) |
17 | 15, 16 | mp1i 13 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) → (𝑝 ∈ ℂ ↦ (𝑝↑3)) ∈
((TopOpen‘ℂfld) Cn
(TopOpen‘ℂfld))) |
18 | 2 | cncfcn1 23808 |
. . . . . . . . . . . . 13
⊢
(ℂ–cn→ℂ) =
((TopOpen‘ℂfld) Cn
(TopOpen‘ℂfld)) |
19 | 17, 18 | eleqtrrdi 2849 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) → (𝑝 ∈ ℂ ↦ (𝑝↑3)) ∈
(ℂ–cn→ℂ)) |
20 | 14, 19 | mulcncf 24343 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) → (𝑝 ∈ ℂ ↦ (𝐶 · (𝑝↑3))) ∈ (ℂ–cn→ℂ)) |
21 | 2, 4, 8, 20 | cncfmpt2f 23812 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) → (𝑝 ∈ ℂ ↦ (𝑝 − (𝐶 · (𝑝↑3)))) ∈ (ℂ–cn→ℂ)) |
22 | | pntlem3.1 |
. . . . . . . . . . . . . . 15
⊢ 𝑇 = {𝑡 ∈ (0[,]𝐴) ∣ ∃𝑦 ∈ ℝ+ ∀𝑧 ∈ (𝑦[,)+∞)(abs‘((𝑅‘𝑧) / 𝑧)) ≤ 𝑡} |
23 | 22 | ssrab3 3995 |
. . . . . . . . . . . . . 14
⊢ 𝑇 ⊆ (0[,]𝐴) |
24 | | 0re 10835 |
. . . . . . . . . . . . . . 15
⊢ 0 ∈
ℝ |
25 | | pntlem3.a |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐴 ∈
ℝ+) |
26 | 25 | rpred 12628 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐴 ∈ ℝ) |
27 | | iccssre 13017 |
. . . . . . . . . . . . . . 15
⊢ ((0
∈ ℝ ∧ 𝐴
∈ ℝ) → (0[,]𝐴) ⊆ ℝ) |
28 | 24, 26, 27 | sylancr 590 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (0[,]𝐴) ⊆ ℝ) |
29 | 23, 28 | sstrid 3912 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑇 ⊆ ℝ) |
30 | | 0xr 10880 |
. . . . . . . . . . . . . . . 16
⊢ 0 ∈
ℝ* |
31 | 25 | rpxrd 12629 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐴 ∈
ℝ*) |
32 | 25 | rpge0d 12632 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 0 ≤ 𝐴) |
33 | | ubicc2 13053 |
. . . . . . . . . . . . . . . 16
⊢ ((0
∈ ℝ* ∧ 𝐴 ∈ ℝ* ∧ 0 ≤
𝐴) → 𝐴 ∈ (0[,]𝐴)) |
34 | 30, 31, 32, 33 | mp3an2i 1468 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐴 ∈ (0[,]𝐴)) |
35 | | 1rp 12590 |
. . . . . . . . . . . . . . . 16
⊢ 1 ∈
ℝ+ |
36 | | fveq2 6717 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 = 𝑧 → (𝑅‘𝑥) = (𝑅‘𝑧)) |
37 | | id 22 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 = 𝑧 → 𝑥 = 𝑧) |
38 | 36, 37 | oveq12d 7231 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 = 𝑧 → ((𝑅‘𝑥) / 𝑥) = ((𝑅‘𝑧) / 𝑧)) |
39 | 38 | fveq2d 6721 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = 𝑧 → (abs‘((𝑅‘𝑥) / 𝑥)) = (abs‘((𝑅‘𝑧) / 𝑧))) |
40 | 39 | breq1d 5063 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝑧 → ((abs‘((𝑅‘𝑥) / 𝑥)) ≤ 𝐴 ↔ (abs‘((𝑅‘𝑧) / 𝑧)) ≤ 𝐴)) |
41 | | pntlem3.A |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ∀𝑥 ∈ ℝ+
(abs‘((𝑅‘𝑥) / 𝑥)) ≤ 𝐴) |
42 | 41 | adantr 484 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑧 ∈ (1[,)+∞)) → ∀𝑥 ∈ ℝ+
(abs‘((𝑅‘𝑥) / 𝑥)) ≤ 𝐴) |
43 | | 1re 10833 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 1 ∈
ℝ |
44 | | elicopnf 13033 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (1 ∈
ℝ → (𝑧 ∈
(1[,)+∞) ↔ (𝑧
∈ ℝ ∧ 1 ≤ 𝑧))) |
45 | 43, 44 | mp1i 13 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝑧 ∈ (1[,)+∞) ↔ (𝑧 ∈ ℝ ∧ 1 ≤
𝑧))) |
46 | 45 | simprbda 502 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑧 ∈ (1[,)+∞)) → 𝑧 ∈
ℝ) |
47 | | 0red 10836 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑧 ∈ (1[,)+∞)) → 0 ∈
ℝ) |
48 | 43 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑧 ∈ (1[,)+∞)) → 1 ∈
ℝ) |
49 | | 0lt1 11354 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 0 <
1 |
50 | 49 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑧 ∈ (1[,)+∞)) → 0 <
1) |
51 | 45 | simplbda 503 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑧 ∈ (1[,)+∞)) → 1 ≤ 𝑧) |
52 | 47, 48, 46, 50, 51 | ltletrd 10992 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑧 ∈ (1[,)+∞)) → 0 < 𝑧) |
53 | 46, 52 | elrpd 12625 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑧 ∈ (1[,)+∞)) → 𝑧 ∈
ℝ+) |
54 | 40, 42, 53 | rspcdva 3539 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑧 ∈ (1[,)+∞)) →
(abs‘((𝑅‘𝑧) / 𝑧)) ≤ 𝐴) |
55 | 54 | ralrimiva 3105 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ∀𝑧 ∈ (1[,)+∞)(abs‘((𝑅‘𝑧) / 𝑧)) ≤ 𝐴) |
56 | | oveq1 7220 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 = 1 → (𝑦[,)+∞) =
(1[,)+∞)) |
57 | 56 | raleqdv 3325 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 = 1 → (∀𝑧 ∈ (𝑦[,)+∞)(abs‘((𝑅‘𝑧) / 𝑧)) ≤ 𝐴 ↔ ∀𝑧 ∈ (1[,)+∞)(abs‘((𝑅‘𝑧) / 𝑧)) ≤ 𝐴)) |
58 | 57 | rspcev 3537 |
. . . . . . . . . . . . . . . 16
⊢ ((1
∈ ℝ+ ∧ ∀𝑧 ∈ (1[,)+∞)(abs‘((𝑅‘𝑧) / 𝑧)) ≤ 𝐴) → ∃𝑦 ∈ ℝ+ ∀𝑧 ∈ (𝑦[,)+∞)(abs‘((𝑅‘𝑧) / 𝑧)) ≤ 𝐴) |
59 | 35, 55, 58 | sylancr 590 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ∃𝑦 ∈ ℝ+ ∀𝑧 ∈ (𝑦[,)+∞)(abs‘((𝑅‘𝑧) / 𝑧)) ≤ 𝐴) |
60 | | breq2 5057 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑡 = 𝐴 → ((abs‘((𝑅‘𝑧) / 𝑧)) ≤ 𝑡 ↔ (abs‘((𝑅‘𝑧) / 𝑧)) ≤ 𝐴)) |
61 | 60 | rexralbidv 3220 |
. . . . . . . . . . . . . . . 16
⊢ (𝑡 = 𝐴 → (∃𝑦 ∈ ℝ+ ∀𝑧 ∈ (𝑦[,)+∞)(abs‘((𝑅‘𝑧) / 𝑧)) ≤ 𝑡 ↔ ∃𝑦 ∈ ℝ+ ∀𝑧 ∈ (𝑦[,)+∞)(abs‘((𝑅‘𝑧) / 𝑧)) ≤ 𝐴)) |
62 | 61, 22 | elrab2 3605 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ 𝑇 ↔ (𝐴 ∈ (0[,]𝐴) ∧ ∃𝑦 ∈ ℝ+ ∀𝑧 ∈ (𝑦[,)+∞)(abs‘((𝑅‘𝑧) / 𝑧)) ≤ 𝐴)) |
63 | 34, 59, 62 | sylanbrc 586 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐴 ∈ 𝑇) |
64 | 63 | ne0d 4250 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑇 ≠ ∅) |
65 | | elicc2 13000 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((0
∈ ℝ ∧ 𝐴
∈ ℝ) → (𝑡
∈ (0[,]𝐴) ↔
(𝑡 ∈ ℝ ∧ 0
≤ 𝑡 ∧ 𝑡 ≤ 𝐴))) |
66 | 24, 26, 65 | sylancr 590 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝑡 ∈ (0[,]𝐴) ↔ (𝑡 ∈ ℝ ∧ 0 ≤ 𝑡 ∧ 𝑡 ≤ 𝐴))) |
67 | 66 | biimpa 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑡 ∈ (0[,]𝐴)) → (𝑡 ∈ ℝ ∧ 0 ≤ 𝑡 ∧ 𝑡 ≤ 𝐴)) |
68 | 67 | simp2d 1145 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑡 ∈ (0[,]𝐴)) → 0 ≤ 𝑡) |
69 | 68 | a1d 25 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑡 ∈ (0[,]𝐴)) → (∃𝑦 ∈ ℝ+ ∀𝑧 ∈ (𝑦[,)+∞)(abs‘((𝑅‘𝑧) / 𝑧)) ≤ 𝑡 → 0 ≤ 𝑡)) |
70 | 69 | ralrimiva 3105 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ∀𝑡 ∈ (0[,]𝐴)(∃𝑦 ∈ ℝ+ ∀𝑧 ∈ (𝑦[,)+∞)(abs‘((𝑅‘𝑧) / 𝑧)) ≤ 𝑡 → 0 ≤ 𝑡)) |
71 | 22 | raleqi 3323 |
. . . . . . . . . . . . . . . 16
⊢
(∀𝑤 ∈
𝑇 0 ≤ 𝑤 ↔ ∀𝑤 ∈ {𝑡 ∈ (0[,]𝐴) ∣ ∃𝑦 ∈ ℝ+ ∀𝑧 ∈ (𝑦[,)+∞)(abs‘((𝑅‘𝑧) / 𝑧)) ≤ 𝑡}0 ≤ 𝑤) |
72 | | breq2 5057 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑤 = 𝑡 → (0 ≤ 𝑤 ↔ 0 ≤ 𝑡)) |
73 | 72 | ralrab2 3612 |
. . . . . . . . . . . . . . . 16
⊢
(∀𝑤 ∈
{𝑡 ∈ (0[,]𝐴) ∣ ∃𝑦 ∈ ℝ+
∀𝑧 ∈ (𝑦[,)+∞)(abs‘((𝑅‘𝑧) / 𝑧)) ≤ 𝑡}0 ≤ 𝑤 ↔ ∀𝑡 ∈ (0[,]𝐴)(∃𝑦 ∈ ℝ+ ∀𝑧 ∈ (𝑦[,)+∞)(abs‘((𝑅‘𝑧) / 𝑧)) ≤ 𝑡 → 0 ≤ 𝑡)) |
74 | 71, 73 | bitri 278 |
. . . . . . . . . . . . . . 15
⊢
(∀𝑤 ∈
𝑇 0 ≤ 𝑤 ↔ ∀𝑡 ∈ (0[,]𝐴)(∃𝑦 ∈ ℝ+ ∀𝑧 ∈ (𝑦[,)+∞)(abs‘((𝑅‘𝑧) / 𝑧)) ≤ 𝑡 → 0 ≤ 𝑡)) |
75 | 70, 74 | sylibr 237 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ∀𝑤 ∈ 𝑇 0 ≤ 𝑤) |
76 | | breq1 5056 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 0 → (𝑥 ≤ 𝑤 ↔ 0 ≤ 𝑤)) |
77 | 76 | ralbidv 3118 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 0 → (∀𝑤 ∈ 𝑇 𝑥 ≤ 𝑤 ↔ ∀𝑤 ∈ 𝑇 0 ≤ 𝑤)) |
78 | 77 | rspcev 3537 |
. . . . . . . . . . . . . 14
⊢ ((0
∈ ℝ ∧ ∀𝑤 ∈ 𝑇 0 ≤ 𝑤) → ∃𝑥 ∈ ℝ ∀𝑤 ∈ 𝑇 𝑥 ≤ 𝑤) |
79 | 24, 75, 78 | sylancr 590 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑤 ∈ 𝑇 𝑥 ≤ 𝑤) |
80 | | infrecl 11814 |
. . . . . . . . . . . . 13
⊢ ((𝑇 ⊆ ℝ ∧ 𝑇 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑤 ∈ 𝑇 𝑥 ≤ 𝑤) → inf(𝑇, ℝ, < ) ∈
ℝ) |
81 | 29, 64, 79, 80 | syl3anc 1373 |
. . . . . . . . . . . 12
⊢ (𝜑 → inf(𝑇, ℝ, < ) ∈
ℝ) |
82 | 81 | recnd 10861 |
. . . . . . . . . . 11
⊢ (𝜑 → inf(𝑇, ℝ, < ) ∈
ℂ) |
83 | 82 | adantr 484 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) →
inf(𝑇, ℝ, < )
∈ ℂ) |
84 | | elrp 12588 |
. . . . . . . . . . . . . 14
⊢
(inf(𝑇, ℝ,
< ) ∈ ℝ+ ↔ (inf(𝑇, ℝ, < ) ∈ ℝ ∧ 0
< inf(𝑇, ℝ, <
))) |
85 | 84 | biimpri 231 |
. . . . . . . . . . . . 13
⊢
((inf(𝑇, ℝ,
< ) ∈ ℝ ∧ 0 < inf(𝑇, ℝ, < )) → inf(𝑇, ℝ, < ) ∈
ℝ+) |
86 | 81, 85 | sylan 583 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) →
inf(𝑇, ℝ, < )
∈ ℝ+) |
87 | | 3z 12210 |
. . . . . . . . . . . 12
⊢ 3 ∈
ℤ |
88 | | rpexpcl 13654 |
. . . . . . . . . . . 12
⊢
((inf(𝑇, ℝ,
< ) ∈ ℝ+ ∧ 3 ∈ ℤ) → (inf(𝑇, ℝ, < )↑3) ∈
ℝ+) |
89 | 86, 87, 88 | sylancl 589 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) →
(inf(𝑇, ℝ, <
)↑3) ∈ ℝ+) |
90 | 10, 89 | rpmulcld 12644 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) → (𝐶 · (inf(𝑇, ℝ, < )↑3)) ∈
ℝ+) |
91 | | cncfi 23791 |
. . . . . . . . . 10
⊢ (((𝑝 ∈ ℂ ↦ (𝑝 − (𝐶 · (𝑝↑3)))) ∈ (ℂ–cn→ℂ) ∧ inf(𝑇, ℝ, < ) ∈ ℂ ∧
(𝐶 · (inf(𝑇, ℝ, < )↑3))
∈ ℝ+) → ∃𝑠 ∈ ℝ+ ∀𝑢 ∈ ℂ
((abs‘(𝑢 −
inf(𝑇, ℝ, < )))
< 𝑠 →
(abs‘(((𝑝 ∈
ℂ ↦ (𝑝 −
(𝐶 · (𝑝↑3))))‘𝑢) − ((𝑝 ∈ ℂ ↦ (𝑝 − (𝐶 · (𝑝↑3))))‘inf(𝑇, ℝ, < )))) < (𝐶 · (inf(𝑇, ℝ, <
)↑3)))) |
92 | 21, 83, 90, 91 | syl3anc 1373 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) →
∃𝑠 ∈
ℝ+ ∀𝑢 ∈ ℂ ((abs‘(𝑢 − inf(𝑇, ℝ, < ))) < 𝑠 → (abs‘(((𝑝 ∈ ℂ ↦ (𝑝 − (𝐶 · (𝑝↑3))))‘𝑢) − ((𝑝 ∈ ℂ ↦ (𝑝 − (𝐶 · (𝑝↑3))))‘inf(𝑇, ℝ, < )))) < (𝐶 · (inf(𝑇, ℝ, <
)↑3)))) |
93 | 81 | ad2antrr 726 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+)
→ inf(𝑇, ℝ, <
) ∈ ℝ) |
94 | | rphalfcl 12613 |
. . . . . . . . . . . . . 14
⊢ (𝑠 ∈ ℝ+
→ (𝑠 / 2) ∈
ℝ+) |
95 | 94 | adantl 485 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+)
→ (𝑠 / 2) ∈
ℝ+) |
96 | 93, 95 | ltaddrpd 12661 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+)
→ inf(𝑇, ℝ, <
) < (inf(𝑇, ℝ,
< ) + (𝑠 /
2))) |
97 | 95 | rpred 12628 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+)
→ (𝑠 / 2) ∈
ℝ) |
98 | 93, 97 | readdcld 10862 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+)
→ (inf(𝑇, ℝ,
< ) + (𝑠 / 2)) ∈
ℝ) |
99 | 93, 98 | ltnled 10979 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+)
→ (inf(𝑇, ℝ,
< ) < (inf(𝑇,
ℝ, < ) + (𝑠 / 2))
↔ ¬ (inf(𝑇,
ℝ, < ) + (𝑠 / 2))
≤ inf(𝑇, ℝ, <
))) |
100 | 96, 99 | mpbid 235 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+)
→ ¬ (inf(𝑇,
ℝ, < ) + (𝑠 / 2))
≤ inf(𝑇, ℝ, <
)) |
101 | | ax-resscn 10786 |
. . . . . . . . . . . . . . 15
⊢ ℝ
⊆ ℂ |
102 | 29, 101 | sstrdi 3913 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑇 ⊆ ℂ) |
103 | 102 | ad2antrr 726 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+)
→ 𝑇 ⊆
ℂ) |
104 | | ssralv 3967 |
. . . . . . . . . . . . 13
⊢ (𝑇 ⊆ ℂ →
(∀𝑢 ∈ ℂ
((abs‘(𝑢 −
inf(𝑇, ℝ, < )))
< 𝑠 →
(abs‘(((𝑝 ∈
ℂ ↦ (𝑝 −
(𝐶 · (𝑝↑3))))‘𝑢) − ((𝑝 ∈ ℂ ↦ (𝑝 − (𝐶 · (𝑝↑3))))‘inf(𝑇, ℝ, < )))) < (𝐶 · (inf(𝑇, ℝ, < )↑3))) →
∀𝑢 ∈ 𝑇 ((abs‘(𝑢 − inf(𝑇, ℝ, < ))) < 𝑠 → (abs‘(((𝑝 ∈ ℂ ↦ (𝑝 − (𝐶 · (𝑝↑3))))‘𝑢) − ((𝑝 ∈ ℂ ↦ (𝑝 − (𝐶 · (𝑝↑3))))‘inf(𝑇, ℝ, < )))) < (𝐶 · (inf(𝑇, ℝ, <
)↑3))))) |
105 | 103, 104 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+)
→ (∀𝑢 ∈
ℂ ((abs‘(𝑢
− inf(𝑇, ℝ,
< ))) < 𝑠 →
(abs‘(((𝑝 ∈
ℂ ↦ (𝑝 −
(𝐶 · (𝑝↑3))))‘𝑢) − ((𝑝 ∈ ℂ ↦ (𝑝 − (𝐶 · (𝑝↑3))))‘inf(𝑇, ℝ, < )))) < (𝐶 · (inf(𝑇, ℝ, < )↑3))) →
∀𝑢 ∈ 𝑇 ((abs‘(𝑢 − inf(𝑇, ℝ, < ))) < 𝑠 → (abs‘(((𝑝 ∈ ℂ ↦ (𝑝 − (𝐶 · (𝑝↑3))))‘𝑢) − ((𝑝 ∈ ℂ ↦ (𝑝 − (𝐶 · (𝑝↑3))))‘inf(𝑇, ℝ, < )))) < (𝐶 · (inf(𝑇, ℝ, <
)↑3))))) |
106 | 29 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+)
→ 𝑇 ⊆
ℝ) |
107 | 106 | sselda 3901 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+)
∧ 𝑢 ∈ 𝑇) → 𝑢 ∈ ℝ) |
108 | 98 | adantr 484 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+)
∧ 𝑢 ∈ 𝑇) → (inf(𝑇, ℝ, < ) + (𝑠 / 2)) ∈ ℝ) |
109 | 107, 108 | ltnled 10979 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+)
∧ 𝑢 ∈ 𝑇) → (𝑢 < (inf(𝑇, ℝ, < ) + (𝑠 / 2)) ↔ ¬ (inf(𝑇, ℝ, < ) + (𝑠 / 2)) ≤ 𝑢)) |
110 | 81 | ad3antrrr 730 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+)
∧ 𝑢 ∈ 𝑇) → inf(𝑇, ℝ, < ) ∈
ℝ) |
111 | 97 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+)
∧ 𝑢 ∈ 𝑇) → (𝑠 / 2) ∈ ℝ) |
112 | 110, 111 | resubcld 11260 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+)
∧ 𝑢 ∈ 𝑇) → (inf(𝑇, ℝ, < ) − (𝑠 / 2)) ∈
ℝ) |
113 | 93, 95 | ltsubrpd 12660 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+)
→ (inf(𝑇, ℝ,
< ) − (𝑠 / 2))
< inf(𝑇, ℝ, <
)) |
114 | 113 | adantr 484 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+)
∧ 𝑢 ∈ 𝑇) → (inf(𝑇, ℝ, < ) − (𝑠 / 2)) < inf(𝑇, ℝ, <
)) |
115 | 29 | ad3antrrr 730 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+)
∧ 𝑢 ∈ 𝑇) → 𝑇 ⊆ ℝ) |
116 | 79 | ad3antrrr 730 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+)
∧ 𝑢 ∈ 𝑇) → ∃𝑥 ∈ ℝ ∀𝑤 ∈ 𝑇 𝑥 ≤ 𝑤) |
117 | | simpr 488 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+)
∧ 𝑢 ∈ 𝑇) → 𝑢 ∈ 𝑇) |
118 | | infrelb 11817 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑇 ⊆ ℝ ∧
∃𝑥 ∈ ℝ
∀𝑤 ∈ 𝑇 𝑥 ≤ 𝑤 ∧ 𝑢 ∈ 𝑇) → inf(𝑇, ℝ, < ) ≤ 𝑢) |
119 | 115, 116,
117, 118 | syl3anc 1373 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+)
∧ 𝑢 ∈ 𝑇) → inf(𝑇, ℝ, < ) ≤ 𝑢) |
120 | 112, 110,
107, 114, 119 | ltletrd 10992 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+)
∧ 𝑢 ∈ 𝑇) → (inf(𝑇, ℝ, < ) − (𝑠 / 2)) < 𝑢) |
121 | 107, 110,
111 | absdifltd 14997 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+)
∧ 𝑢 ∈ 𝑇) → ((abs‘(𝑢 − inf(𝑇, ℝ, < ))) < (𝑠 / 2) ↔ ((inf(𝑇, ℝ, < ) − (𝑠 / 2)) < 𝑢 ∧ 𝑢 < (inf(𝑇, ℝ, < ) + (𝑠 / 2))))) |
122 | 121 | biimprd 251 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+)
∧ 𝑢 ∈ 𝑇) → (((inf(𝑇, ℝ, < ) − (𝑠 / 2)) < 𝑢 ∧ 𝑢 < (inf(𝑇, ℝ, < ) + (𝑠 / 2))) → (abs‘(𝑢 − inf(𝑇, ℝ, < ))) < (𝑠 / 2))) |
123 | 120, 122 | mpand 695 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+)
∧ 𝑢 ∈ 𝑇) → (𝑢 < (inf(𝑇, ℝ, < ) + (𝑠 / 2)) → (abs‘(𝑢 − inf(𝑇, ℝ, < ))) < (𝑠 / 2))) |
124 | | rphalflt 12615 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑠 ∈ ℝ+
→ (𝑠 / 2) < 𝑠) |
125 | 124 | ad2antlr 727 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+)
∧ 𝑢 ∈ 𝑇) → (𝑠 / 2) < 𝑠) |
126 | 107, 110 | resubcld 11260 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+)
∧ 𝑢 ∈ 𝑇) → (𝑢 − inf(𝑇, ℝ, < )) ∈
ℝ) |
127 | 126 | recnd 10861 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+)
∧ 𝑢 ∈ 𝑇) → (𝑢 − inf(𝑇, ℝ, < )) ∈
ℂ) |
128 | 127 | abscld 15000 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+)
∧ 𝑢 ∈ 𝑇) → (abs‘(𝑢 − inf(𝑇, ℝ, < ))) ∈
ℝ) |
129 | | rpre 12594 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑠 ∈ ℝ+
→ 𝑠 ∈
ℝ) |
130 | 129 | ad2antlr 727 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+)
∧ 𝑢 ∈ 𝑇) → 𝑠 ∈ ℝ) |
131 | | lttr 10909 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((abs‘(𝑢
− inf(𝑇, ℝ,
< ))) ∈ ℝ ∧ (𝑠 / 2) ∈ ℝ ∧ 𝑠 ∈ ℝ) → (((abs‘(𝑢 − inf(𝑇, ℝ, < ))) < (𝑠 / 2) ∧ (𝑠 / 2) < 𝑠) → (abs‘(𝑢 − inf(𝑇, ℝ, < ))) < 𝑠)) |
132 | 128, 111,
130, 131 | syl3anc 1373 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+)
∧ 𝑢 ∈ 𝑇) → (((abs‘(𝑢 − inf(𝑇, ℝ, < ))) < (𝑠 / 2) ∧ (𝑠 / 2) < 𝑠) → (abs‘(𝑢 − inf(𝑇, ℝ, < ))) < 𝑠)) |
133 | 125, 132 | mpan2d 694 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+)
∧ 𝑢 ∈ 𝑇) → ((abs‘(𝑢 − inf(𝑇, ℝ, < ))) < (𝑠 / 2) → (abs‘(𝑢 − inf(𝑇, ℝ, < ))) < 𝑠)) |
134 | 123, 133 | syld 47 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+)
∧ 𝑢 ∈ 𝑇) → (𝑢 < (inf(𝑇, ℝ, < ) + (𝑠 / 2)) → (abs‘(𝑢 − inf(𝑇, ℝ, < ))) < 𝑠)) |
135 | 109, 134 | sylbird 263 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+)
∧ 𝑢 ∈ 𝑇) → (¬ (inf(𝑇, ℝ, < ) + (𝑠 / 2)) ≤ 𝑢 → (abs‘(𝑢 − inf(𝑇, ℝ, < ))) < 𝑠)) |
136 | 135 | con1d 147 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+)
∧ 𝑢 ∈ 𝑇) → (¬
(abs‘(𝑢 −
inf(𝑇, ℝ, < )))
< 𝑠 → (inf(𝑇, ℝ, < ) + (𝑠 / 2)) ≤ 𝑢)) |
137 | 107 | recnd 10861 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+)
∧ 𝑢 ∈ 𝑇) → 𝑢 ∈ ℂ) |
138 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑝 = 𝑢 → 𝑝 = 𝑢) |
139 | | oveq1 7220 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑝 = 𝑢 → (𝑝↑3) = (𝑢↑3)) |
140 | 139 | oveq2d 7229 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑝 = 𝑢 → (𝐶 · (𝑝↑3)) = (𝐶 · (𝑢↑3))) |
141 | 138, 140 | oveq12d 7231 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑝 = 𝑢 → (𝑝 − (𝐶 · (𝑝↑3))) = (𝑢 − (𝐶 · (𝑢↑3)))) |
142 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑝 ∈ ℂ ↦ (𝑝 − (𝐶 · (𝑝↑3)))) = (𝑝 ∈ ℂ ↦ (𝑝 − (𝐶 · (𝑝↑3)))) |
143 | | ovex 7246 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑢 − (𝐶 · (𝑢↑3))) ∈ V |
144 | 141, 142,
143 | fvmpt 6818 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑢 ∈ ℂ → ((𝑝 ∈ ℂ ↦ (𝑝 − (𝐶 · (𝑝↑3))))‘𝑢) = (𝑢 − (𝐶 · (𝑢↑3)))) |
145 | 137, 144 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+)
∧ 𝑢 ∈ 𝑇) → ((𝑝 ∈ ℂ ↦ (𝑝 − (𝐶 · (𝑝↑3))))‘𝑢) = (𝑢 − (𝐶 · (𝑢↑3)))) |
146 | 83 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+)
∧ 𝑢 ∈ 𝑇) → inf(𝑇, ℝ, < ) ∈
ℂ) |
147 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑝 = inf(𝑇, ℝ, < ) → 𝑝 = inf(𝑇, ℝ, < )) |
148 | | oveq1 7220 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑝 = inf(𝑇, ℝ, < ) → (𝑝↑3) = (inf(𝑇, ℝ, < )↑3)) |
149 | 148 | oveq2d 7229 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑝 = inf(𝑇, ℝ, < ) → (𝐶 · (𝑝↑3)) = (𝐶 · (inf(𝑇, ℝ, < )↑3))) |
150 | 147, 149 | oveq12d 7231 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑝 = inf(𝑇, ℝ, < ) → (𝑝 − (𝐶 · (𝑝↑3))) = (inf(𝑇, ℝ, < ) − (𝐶 · (inf(𝑇, ℝ, <
)↑3)))) |
151 | | ovex 7246 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(inf(𝑇, ℝ,
< ) − (𝐶 ·
(inf(𝑇, ℝ, <
)↑3))) ∈ V |
152 | 150, 142,
151 | fvmpt 6818 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(inf(𝑇, ℝ,
< ) ∈ ℂ → ((𝑝 ∈ ℂ ↦ (𝑝 − (𝐶 · (𝑝↑3))))‘inf(𝑇, ℝ, < )) = (inf(𝑇, ℝ, < ) − (𝐶 · (inf(𝑇, ℝ, <
)↑3)))) |
153 | 146, 152 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+)
∧ 𝑢 ∈ 𝑇) → ((𝑝 ∈ ℂ ↦ (𝑝 − (𝐶 · (𝑝↑3))))‘inf(𝑇, ℝ, < )) = (inf(𝑇, ℝ, < ) − (𝐶 · (inf(𝑇, ℝ, <
)↑3)))) |
154 | 145, 153 | oveq12d 7231 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+)
∧ 𝑢 ∈ 𝑇) → (((𝑝 ∈ ℂ ↦ (𝑝 − (𝐶 · (𝑝↑3))))‘𝑢) − ((𝑝 ∈ ℂ ↦ (𝑝 − (𝐶 · (𝑝↑3))))‘inf(𝑇, ℝ, < ))) = ((𝑢 − (𝐶 · (𝑢↑3))) − (inf(𝑇, ℝ, < ) − (𝐶 · (inf(𝑇, ℝ, <
)↑3))))) |
155 | 154 | fveq2d 6721 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+)
∧ 𝑢 ∈ 𝑇) → (abs‘(((𝑝 ∈ ℂ ↦ (𝑝 − (𝐶 · (𝑝↑3))))‘𝑢) − ((𝑝 ∈ ℂ ↦ (𝑝 − (𝐶 · (𝑝↑3))))‘inf(𝑇, ℝ, < )))) = (abs‘((𝑢 − (𝐶 · (𝑢↑3))) − (inf(𝑇, ℝ, < ) − (𝐶 · (inf(𝑇, ℝ, <
)↑3)))))) |
156 | 155 | breq1d 5063 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+)
∧ 𝑢 ∈ 𝑇) → ((abs‘(((𝑝 ∈ ℂ ↦ (𝑝 − (𝐶 · (𝑝↑3))))‘𝑢) − ((𝑝 ∈ ℂ ↦ (𝑝 − (𝐶 · (𝑝↑3))))‘inf(𝑇, ℝ, < )))) < (𝐶 · (inf(𝑇, ℝ, < )↑3)) ↔
(abs‘((𝑢 −
(𝐶 · (𝑢↑3))) − (inf(𝑇, ℝ, < ) − (𝐶 · (inf(𝑇, ℝ, < )↑3))))) < (𝐶 · (inf(𝑇, ℝ, <
)↑3)))) |
157 | 9 | rpred 12628 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 𝐶 ∈ ℝ) |
158 | 157 | ad3antrrr 730 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+)
∧ 𝑢 ∈ 𝑇) → 𝐶 ∈ ℝ) |
159 | | reexpcl 13652 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑢 ∈ ℝ ∧ 3 ∈
ℕ0) → (𝑢↑3) ∈ ℝ) |
160 | 107, 15, 159 | sylancl 589 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+)
∧ 𝑢 ∈ 𝑇) → (𝑢↑3) ∈ ℝ) |
161 | 158, 160 | remulcld 10863 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+)
∧ 𝑢 ∈ 𝑇) → (𝐶 · (𝑢↑3)) ∈ ℝ) |
162 | 107, 161 | resubcld 11260 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+)
∧ 𝑢 ∈ 𝑇) → (𝑢 − (𝐶 · (𝑢↑3))) ∈ ℝ) |
163 | 15 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+)
∧ 𝑢 ∈ 𝑇) → 3 ∈
ℕ0) |
164 | 110, 163 | reexpcld 13733 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+)
∧ 𝑢 ∈ 𝑇) → (inf(𝑇, ℝ, < )↑3) ∈
ℝ) |
165 | 158, 164 | remulcld 10863 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+)
∧ 𝑢 ∈ 𝑇) → (𝐶 · (inf(𝑇, ℝ, < )↑3)) ∈
ℝ) |
166 | 110, 165 | resubcld 11260 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+)
∧ 𝑢 ∈ 𝑇) → (inf(𝑇, ℝ, < ) − (𝐶 · (inf(𝑇, ℝ, < )↑3))) ∈
ℝ) |
167 | 162, 166,
165 | absdifltd 14997 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+)
∧ 𝑢 ∈ 𝑇) → ((abs‘((𝑢 − (𝐶 · (𝑢↑3))) − (inf(𝑇, ℝ, < ) − (𝐶 · (inf(𝑇, ℝ, < )↑3))))) < (𝐶 · (inf(𝑇, ℝ, < )↑3)) ↔
(((inf(𝑇, ℝ, < )
− (𝐶 ·
(inf(𝑇, ℝ, <
)↑3))) − (𝐶
· (inf(𝑇, ℝ,
< )↑3))) < (𝑢
− (𝐶 · (𝑢↑3))) ∧ (𝑢 − (𝐶 · (𝑢↑3))) < ((inf(𝑇, ℝ, < ) − (𝐶 · (inf(𝑇, ℝ, < )↑3))) + (𝐶 · (inf(𝑇, ℝ, <
)↑3)))))) |
168 | 165 | recnd 10861 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+)
∧ 𝑢 ∈ 𝑇) → (𝐶 · (inf(𝑇, ℝ, < )↑3)) ∈
ℂ) |
169 | 146, 168 | npcand 11193 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+)
∧ 𝑢 ∈ 𝑇) → ((inf(𝑇, ℝ, < ) − (𝐶 · (inf(𝑇, ℝ, < )↑3))) + (𝐶 · (inf(𝑇, ℝ, < )↑3))) = inf(𝑇, ℝ, <
)) |
170 | 169 | breq2d 5065 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+)
∧ 𝑢 ∈ 𝑇) → ((𝑢 − (𝐶 · (𝑢↑3))) < ((inf(𝑇, ℝ, < ) − (𝐶 · (inf(𝑇, ℝ, < )↑3))) + (𝐶 · (inf(𝑇, ℝ, < )↑3))) ↔ (𝑢 − (𝐶 · (𝑢↑3))) < inf(𝑇, ℝ, < ))) |
171 | | pntlem3.3 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑇) → (𝑢 − (𝐶 · (𝑢↑3))) ∈ 𝑇) |
172 | 171 | ad4ant14 752 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+)
∧ 𝑢 ∈ 𝑇) → (𝑢 − (𝐶 · (𝑢↑3))) ∈ 𝑇) |
173 | | infrelb 11817 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑇 ⊆ ℝ ∧
∃𝑥 ∈ ℝ
∀𝑤 ∈ 𝑇 𝑥 ≤ 𝑤 ∧ (𝑢 − (𝐶 · (𝑢↑3))) ∈ 𝑇) → inf(𝑇, ℝ, < ) ≤ (𝑢 − (𝐶 · (𝑢↑3)))) |
174 | 115, 116,
172, 173 | syl3anc 1373 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+)
∧ 𝑢 ∈ 𝑇) → inf(𝑇, ℝ, < ) ≤ (𝑢 − (𝐶 · (𝑢↑3)))) |
175 | 110, 162,
174 | lensymd 10983 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+)
∧ 𝑢 ∈ 𝑇) → ¬ (𝑢 − (𝐶 · (𝑢↑3))) < inf(𝑇, ℝ, < )) |
176 | 175 | pm2.21d 121 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+)
∧ 𝑢 ∈ 𝑇) → ((𝑢 − (𝐶 · (𝑢↑3))) < inf(𝑇, ℝ, < ) → (inf(𝑇, ℝ, < ) + (𝑠 / 2)) ≤ 𝑢)) |
177 | 170, 176 | sylbid 243 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+)
∧ 𝑢 ∈ 𝑇) → ((𝑢 − (𝐶 · (𝑢↑3))) < ((inf(𝑇, ℝ, < ) − (𝐶 · (inf(𝑇, ℝ, < )↑3))) + (𝐶 · (inf(𝑇, ℝ, < )↑3))) →
(inf(𝑇, ℝ, < ) +
(𝑠 / 2)) ≤ 𝑢)) |
178 | 177 | adantld 494 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+)
∧ 𝑢 ∈ 𝑇) → ((((inf(𝑇, ℝ, < ) − (𝐶 · (inf(𝑇, ℝ, < )↑3))) − (𝐶 · (inf(𝑇, ℝ, < )↑3))) < (𝑢 − (𝐶 · (𝑢↑3))) ∧ (𝑢 − (𝐶 · (𝑢↑3))) < ((inf(𝑇, ℝ, < ) − (𝐶 · (inf(𝑇, ℝ, < )↑3))) + (𝐶 · (inf(𝑇, ℝ, < )↑3)))) →
(inf(𝑇, ℝ, < ) +
(𝑠 / 2)) ≤ 𝑢)) |
179 | 167, 178 | sylbid 243 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+)
∧ 𝑢 ∈ 𝑇) → ((abs‘((𝑢 − (𝐶 · (𝑢↑3))) − (inf(𝑇, ℝ, < ) − (𝐶 · (inf(𝑇, ℝ, < )↑3))))) < (𝐶 · (inf(𝑇, ℝ, < )↑3)) → (inf(𝑇, ℝ, < ) + (𝑠 / 2)) ≤ 𝑢)) |
180 | 156, 179 | sylbid 243 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+)
∧ 𝑢 ∈ 𝑇) → ((abs‘(((𝑝 ∈ ℂ ↦ (𝑝 − (𝐶 · (𝑝↑3))))‘𝑢) − ((𝑝 ∈ ℂ ↦ (𝑝 − (𝐶 · (𝑝↑3))))‘inf(𝑇, ℝ, < )))) < (𝐶 · (inf(𝑇, ℝ, < )↑3)) → (inf(𝑇, ℝ, < ) + (𝑠 / 2)) ≤ 𝑢)) |
181 | 136, 180 | jad 190 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+)
∧ 𝑢 ∈ 𝑇) → (((abs‘(𝑢 − inf(𝑇, ℝ, < ))) < 𝑠 → (abs‘(((𝑝 ∈ ℂ ↦ (𝑝 − (𝐶 · (𝑝↑3))))‘𝑢) − ((𝑝 ∈ ℂ ↦ (𝑝 − (𝐶 · (𝑝↑3))))‘inf(𝑇, ℝ, < )))) < (𝐶 · (inf(𝑇, ℝ, < )↑3))) →
(inf(𝑇, ℝ, < ) +
(𝑠 / 2)) ≤ 𝑢)) |
182 | 181 | ralimdva 3100 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+)
→ (∀𝑢 ∈
𝑇 ((abs‘(𝑢 − inf(𝑇, ℝ, < ))) < 𝑠 → (abs‘(((𝑝 ∈ ℂ ↦ (𝑝 − (𝐶 · (𝑝↑3))))‘𝑢) − ((𝑝 ∈ ℂ ↦ (𝑝 − (𝐶 · (𝑝↑3))))‘inf(𝑇, ℝ, < )))) < (𝐶 · (inf(𝑇, ℝ, < )↑3))) →
∀𝑢 ∈ 𝑇 (inf(𝑇, ℝ, < ) + (𝑠 / 2)) ≤ 𝑢)) |
183 | 64 | ad2antrr 726 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+)
→ 𝑇 ≠
∅) |
184 | 79 | ad2antrr 726 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+)
→ ∃𝑥 ∈
ℝ ∀𝑤 ∈
𝑇 𝑥 ≤ 𝑤) |
185 | | infregelb 11816 |
. . . . . . . . . . . . . 14
⊢ (((𝑇 ⊆ ℝ ∧ 𝑇 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑤 ∈ 𝑇 𝑥 ≤ 𝑤) ∧ (inf(𝑇, ℝ, < ) + (𝑠 / 2)) ∈ ℝ) → ((inf(𝑇, ℝ, < ) + (𝑠 / 2)) ≤ inf(𝑇, ℝ, < ) ↔
∀𝑢 ∈ 𝑇 (inf(𝑇, ℝ, < ) + (𝑠 / 2)) ≤ 𝑢)) |
186 | 106, 183,
184, 98, 185 | syl31anc 1375 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+)
→ ((inf(𝑇, ℝ,
< ) + (𝑠 / 2)) ≤
inf(𝑇, ℝ, < )
↔ ∀𝑢 ∈
𝑇 (inf(𝑇, ℝ, < ) + (𝑠 / 2)) ≤ 𝑢)) |
187 | 182, 186 | sylibrd 262 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+)
→ (∀𝑢 ∈
𝑇 ((abs‘(𝑢 − inf(𝑇, ℝ, < ))) < 𝑠 → (abs‘(((𝑝 ∈ ℂ ↦ (𝑝 − (𝐶 · (𝑝↑3))))‘𝑢) − ((𝑝 ∈ ℂ ↦ (𝑝 − (𝐶 · (𝑝↑3))))‘inf(𝑇, ℝ, < )))) < (𝐶 · (inf(𝑇, ℝ, < )↑3))) →
(inf(𝑇, ℝ, < ) +
(𝑠 / 2)) ≤ inf(𝑇, ℝ, <
))) |
188 | 105, 187 | syld 47 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+)
→ (∀𝑢 ∈
ℂ ((abs‘(𝑢
− inf(𝑇, ℝ,
< ))) < 𝑠 →
(abs‘(((𝑝 ∈
ℂ ↦ (𝑝 −
(𝐶 · (𝑝↑3))))‘𝑢) − ((𝑝 ∈ ℂ ↦ (𝑝 − (𝐶 · (𝑝↑3))))‘inf(𝑇, ℝ, < )))) < (𝐶 · (inf(𝑇, ℝ, < )↑3))) →
(inf(𝑇, ℝ, < ) +
(𝑠 / 2)) ≤ inf(𝑇, ℝ, <
))) |
189 | 100, 188 | mtod 201 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+)
→ ¬ ∀𝑢
∈ ℂ ((abs‘(𝑢 − inf(𝑇, ℝ, < ))) < 𝑠 → (abs‘(((𝑝 ∈ ℂ ↦ (𝑝 − (𝐶 · (𝑝↑3))))‘𝑢) − ((𝑝 ∈ ℂ ↦ (𝑝 − (𝐶 · (𝑝↑3))))‘inf(𝑇, ℝ, < )))) < (𝐶 · (inf(𝑇, ℝ, <
)↑3)))) |
190 | 189 | nrexdv 3189 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) → ¬
∃𝑠 ∈
ℝ+ ∀𝑢 ∈ ℂ ((abs‘(𝑢 − inf(𝑇, ℝ, < ))) < 𝑠 → (abs‘(((𝑝 ∈ ℂ ↦ (𝑝 − (𝐶 · (𝑝↑3))))‘𝑢) − ((𝑝 ∈ ℂ ↦ (𝑝 − (𝐶 · (𝑝↑3))))‘inf(𝑇, ℝ, < )))) < (𝐶 · (inf(𝑇, ℝ, <
)↑3)))) |
191 | 92, 190 | pm2.65da 817 |
. . . . . . . 8
⊢ (𝜑 → ¬ 0 < inf(𝑇, ℝ, <
)) |
192 | 191 | adantr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ ℝ+) → ¬ 0
< inf(𝑇, ℝ, <
)) |
193 | 29 | adantr 484 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑠 ∈ ℝ+) → 𝑇 ⊆
ℝ) |
194 | 64 | adantr 484 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑠 ∈ ℝ+) → 𝑇 ≠ ∅) |
195 | 79 | adantr 484 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑠 ∈ ℝ+) →
∃𝑥 ∈ ℝ
∀𝑤 ∈ 𝑇 𝑥 ≤ 𝑤) |
196 | 129 | adantl 485 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑠 ∈ ℝ+) → 𝑠 ∈
ℝ) |
197 | | infregelb 11816 |
. . . . . . . . . 10
⊢ (((𝑇 ⊆ ℝ ∧ 𝑇 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑤 ∈ 𝑇 𝑥 ≤ 𝑤) ∧ 𝑠 ∈ ℝ) → (𝑠 ≤ inf(𝑇, ℝ, < ) ↔ ∀𝑤 ∈ 𝑇 𝑠 ≤ 𝑤)) |
198 | 193, 194,
195, 196, 197 | syl31anc 1375 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑠 ∈ ℝ+) → (𝑠 ≤ inf(𝑇, ℝ, < ) ↔ ∀𝑤 ∈ 𝑇 𝑠 ≤ 𝑤)) |
199 | 22 | raleqi 3323 |
. . . . . . . . . 10
⊢
(∀𝑤 ∈
𝑇 𝑠 ≤ 𝑤 ↔ ∀𝑤 ∈ {𝑡 ∈ (0[,]𝐴) ∣ ∃𝑦 ∈ ℝ+ ∀𝑧 ∈ (𝑦[,)+∞)(abs‘((𝑅‘𝑧) / 𝑧)) ≤ 𝑡}𝑠 ≤ 𝑤) |
200 | | breq2 5057 |
. . . . . . . . . . 11
⊢ (𝑤 = 𝑡 → (𝑠 ≤ 𝑤 ↔ 𝑠 ≤ 𝑡)) |
201 | 200 | ralrab2 3612 |
. . . . . . . . . 10
⊢
(∀𝑤 ∈
{𝑡 ∈ (0[,]𝐴) ∣ ∃𝑦 ∈ ℝ+
∀𝑧 ∈ (𝑦[,)+∞)(abs‘((𝑅‘𝑧) / 𝑧)) ≤ 𝑡}𝑠 ≤ 𝑤 ↔ ∀𝑡 ∈ (0[,]𝐴)(∃𝑦 ∈ ℝ+ ∀𝑧 ∈ (𝑦[,)+∞)(abs‘((𝑅‘𝑧) / 𝑧)) ≤ 𝑡 → 𝑠 ≤ 𝑡)) |
202 | 199, 201 | bitri 278 |
. . . . . . . . 9
⊢
(∀𝑤 ∈
𝑇 𝑠 ≤ 𝑤 ↔ ∀𝑡 ∈ (0[,]𝐴)(∃𝑦 ∈ ℝ+ ∀𝑧 ∈ (𝑦[,)+∞)(abs‘((𝑅‘𝑧) / 𝑧)) ≤ 𝑡 → 𝑠 ≤ 𝑡)) |
203 | 198, 202 | bitrdi 290 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑠 ∈ ℝ+) → (𝑠 ≤ inf(𝑇, ℝ, < ) ↔ ∀𝑡 ∈ (0[,]𝐴)(∃𝑦 ∈ ℝ+ ∀𝑧 ∈ (𝑦[,)+∞)(abs‘((𝑅‘𝑧) / 𝑧)) ≤ 𝑡 → 𝑠 ≤ 𝑡))) |
204 | | rpgt0 12598 |
. . . . . . . . . 10
⊢ (𝑠 ∈ ℝ+
→ 0 < 𝑠) |
205 | 204 | adantl 485 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑠 ∈ ℝ+) → 0 <
𝑠) |
206 | 81 | adantr 484 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑠 ∈ ℝ+) → inf(𝑇, ℝ, < ) ∈
ℝ) |
207 | | ltletr 10924 |
. . . . . . . . . 10
⊢ ((0
∈ ℝ ∧ 𝑠
∈ ℝ ∧ inf(𝑇,
ℝ, < ) ∈ ℝ) → ((0 < 𝑠 ∧ 𝑠 ≤ inf(𝑇, ℝ, < )) → 0 < inf(𝑇, ℝ, <
))) |
208 | 24, 196, 206, 207 | mp3an2i 1468 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑠 ∈ ℝ+) → ((0 <
𝑠 ∧ 𝑠 ≤ inf(𝑇, ℝ, < )) → 0 < inf(𝑇, ℝ, <
))) |
209 | 205, 208 | mpand 695 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑠 ∈ ℝ+) → (𝑠 ≤ inf(𝑇, ℝ, < ) → 0 < inf(𝑇, ℝ, <
))) |
210 | 203, 209 | sylbird 263 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ ℝ+) →
(∀𝑡 ∈
(0[,]𝐴)(∃𝑦 ∈ ℝ+
∀𝑧 ∈ (𝑦[,)+∞)(abs‘((𝑅‘𝑧) / 𝑧)) ≤ 𝑡 → 𝑠 ≤ 𝑡) → 0 < inf(𝑇, ℝ, < ))) |
211 | 192, 210 | mtod 201 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑠 ∈ ℝ+) → ¬
∀𝑡 ∈ (0[,]𝐴)(∃𝑦 ∈ ℝ+ ∀𝑧 ∈ (𝑦[,)+∞)(abs‘((𝑅‘𝑧) / 𝑧)) ≤ 𝑡 → 𝑠 ≤ 𝑡)) |
212 | | rexanali 3184 |
. . . . . 6
⊢
(∃𝑡 ∈
(0[,]𝐴)(∃𝑦 ∈ ℝ+
∀𝑧 ∈ (𝑦[,)+∞)(abs‘((𝑅‘𝑧) / 𝑧)) ≤ 𝑡 ∧ ¬ 𝑠 ≤ 𝑡) ↔ ¬ ∀𝑡 ∈ (0[,]𝐴)(∃𝑦 ∈ ℝ+ ∀𝑧 ∈ (𝑦[,)+∞)(abs‘((𝑅‘𝑧) / 𝑧)) ≤ 𝑡 → 𝑠 ≤ 𝑡)) |
213 | 211, 212 | sylibr 237 |
. . . . 5
⊢ ((𝜑 ∧ 𝑠 ∈ ℝ+) →
∃𝑡 ∈ (0[,]𝐴)(∃𝑦 ∈ ℝ+ ∀𝑧 ∈ (𝑦[,)+∞)(abs‘((𝑅‘𝑧) / 𝑧)) ≤ 𝑡 ∧ ¬ 𝑠 ≤ 𝑡)) |
214 | | fveq2 6717 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = 𝑥 → (𝑅‘𝑧) = (𝑅‘𝑥)) |
215 | | id 22 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = 𝑥 → 𝑧 = 𝑥) |
216 | 214, 215 | oveq12d 7231 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = 𝑥 → ((𝑅‘𝑧) / 𝑧) = ((𝑅‘𝑥) / 𝑥)) |
217 | 216 | fveq2d 6721 |
. . . . . . . . . . . . 13
⊢ (𝑧 = 𝑥 → (abs‘((𝑅‘𝑧) / 𝑧)) = (abs‘((𝑅‘𝑥) / 𝑥))) |
218 | 217 | breq1d 5063 |
. . . . . . . . . . . 12
⊢ (𝑧 = 𝑥 → ((abs‘((𝑅‘𝑧) / 𝑧)) ≤ 𝑡 ↔ (abs‘((𝑅‘𝑥) / 𝑥)) ≤ 𝑡)) |
219 | 218 | cbvralvw 3358 |
. . . . . . . . . . 11
⊢
(∀𝑧 ∈
(𝑦[,)+∞)(abs‘((𝑅‘𝑧) / 𝑧)) ≤ 𝑡 ↔ ∀𝑥 ∈ (𝑦[,)+∞)(abs‘((𝑅‘𝑥) / 𝑥)) ≤ 𝑡) |
220 | | rpre 12594 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ ℝ+
→ 𝑥 ∈
ℝ) |
221 | 220 | ad2antll 729 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ 𝑠 ∈ ℝ+)
∧ (𝑡 ∈ (0[,]𝐴) ∧ ¬ 𝑠 ≤ 𝑡)) ∧ 𝑦 ∈ ℝ+) ∧ (𝑦 ≤ 𝑥 ∧ 𝑥 ∈ ℝ+)) → 𝑥 ∈
ℝ) |
222 | | simprl 771 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ 𝑠 ∈ ℝ+)
∧ (𝑡 ∈ (0[,]𝐴) ∧ ¬ 𝑠 ≤ 𝑡)) ∧ 𝑦 ∈ ℝ+) ∧ (𝑦 ≤ 𝑥 ∧ 𝑥 ∈ ℝ+)) → 𝑦 ≤ 𝑥) |
223 | | simplr 769 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ 𝑠 ∈ ℝ+)
∧ (𝑡 ∈ (0[,]𝐴) ∧ ¬ 𝑠 ≤ 𝑡)) ∧ 𝑦 ∈ ℝ+) ∧ (𝑦 ≤ 𝑥 ∧ 𝑥 ∈ ℝ+)) → 𝑦 ∈
ℝ+) |
224 | 223 | rpred 12628 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧ 𝑠 ∈ ℝ+)
∧ (𝑡 ∈ (0[,]𝐴) ∧ ¬ 𝑠 ≤ 𝑡)) ∧ 𝑦 ∈ ℝ+) ∧ (𝑦 ≤ 𝑥 ∧ 𝑥 ∈ ℝ+)) → 𝑦 ∈
ℝ) |
225 | | elicopnf 13033 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈ ℝ → (𝑥 ∈ (𝑦[,)+∞) ↔ (𝑥 ∈ ℝ ∧ 𝑦 ≤ 𝑥))) |
226 | 224, 225 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ 𝑠 ∈ ℝ+)
∧ (𝑡 ∈ (0[,]𝐴) ∧ ¬ 𝑠 ≤ 𝑡)) ∧ 𝑦 ∈ ℝ+) ∧ (𝑦 ≤ 𝑥 ∧ 𝑥 ∈ ℝ+)) → (𝑥 ∈ (𝑦[,)+∞) ↔ (𝑥 ∈ ℝ ∧ 𝑦 ≤ 𝑥))) |
227 | 221, 222,
226 | mpbir2and 713 |
. . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ 𝑠 ∈ ℝ+)
∧ (𝑡 ∈ (0[,]𝐴) ∧ ¬ 𝑠 ≤ 𝑡)) ∧ 𝑦 ∈ ℝ+) ∧ (𝑦 ≤ 𝑥 ∧ 𝑥 ∈ ℝ+)) → 𝑥 ∈ (𝑦[,)+∞)) |
228 | | pntlem3.r |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 𝑅 = (𝑎 ∈ ℝ+ ↦
((ψ‘𝑎) −
𝑎)) |
229 | 228 | pntrval 26443 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 ∈ ℝ+
→ (𝑅‘𝑥) = ((ψ‘𝑥) − 𝑥)) |
230 | 229 | ad2antll 729 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝜑 ∧ 𝑠 ∈ ℝ+)
∧ (𝑡 ∈ (0[,]𝐴) ∧ ¬ 𝑠 ≤ 𝑡)) ∧ 𝑦 ∈ ℝ+) ∧ (𝑦 ≤ 𝑥 ∧ 𝑥 ∈ ℝ+)) → (𝑅‘𝑥) = ((ψ‘𝑥) − 𝑥)) |
231 | 230 | oveq1d 7228 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧ 𝑠 ∈ ℝ+)
∧ (𝑡 ∈ (0[,]𝐴) ∧ ¬ 𝑠 ≤ 𝑡)) ∧ 𝑦 ∈ ℝ+) ∧ (𝑦 ≤ 𝑥 ∧ 𝑥 ∈ ℝ+)) → ((𝑅‘𝑥) / 𝑥) = (((ψ‘𝑥) − 𝑥) / 𝑥)) |
232 | | chpcl 26006 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 ∈ ℝ →
(ψ‘𝑥) ∈
ℝ) |
233 | 221, 232 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝜑 ∧ 𝑠 ∈ ℝ+)
∧ (𝑡 ∈ (0[,]𝐴) ∧ ¬ 𝑠 ≤ 𝑡)) ∧ 𝑦 ∈ ℝ+) ∧ (𝑦 ≤ 𝑥 ∧ 𝑥 ∈ ℝ+)) →
(ψ‘𝑥) ∈
ℝ) |
234 | 233 | recnd 10861 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝜑 ∧ 𝑠 ∈ ℝ+)
∧ (𝑡 ∈ (0[,]𝐴) ∧ ¬ 𝑠 ≤ 𝑡)) ∧ 𝑦 ∈ ℝ+) ∧ (𝑦 ≤ 𝑥 ∧ 𝑥 ∈ ℝ+)) →
(ψ‘𝑥) ∈
ℂ) |
235 | | rpcn 12596 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 ∈ ℝ+
→ 𝑥 ∈
ℂ) |
236 | 235 | ad2antll 729 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝜑 ∧ 𝑠 ∈ ℝ+)
∧ (𝑡 ∈ (0[,]𝐴) ∧ ¬ 𝑠 ≤ 𝑡)) ∧ 𝑦 ∈ ℝ+) ∧ (𝑦 ≤ 𝑥 ∧ 𝑥 ∈ ℝ+)) → 𝑥 ∈
ℂ) |
237 | | rpne0 12602 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 ∈ ℝ+
→ 𝑥 ≠
0) |
238 | 237 | ad2antll 729 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝜑 ∧ 𝑠 ∈ ℝ+)
∧ (𝑡 ∈ (0[,]𝐴) ∧ ¬ 𝑠 ≤ 𝑡)) ∧ 𝑦 ∈ ℝ+) ∧ (𝑦 ≤ 𝑥 ∧ 𝑥 ∈ ℝ+)) → 𝑥 ≠ 0) |
239 | 234, 236,
236, 238 | divsubdird 11647 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧ 𝑠 ∈ ℝ+)
∧ (𝑡 ∈ (0[,]𝐴) ∧ ¬ 𝑠 ≤ 𝑡)) ∧ 𝑦 ∈ ℝ+) ∧ (𝑦 ≤ 𝑥 ∧ 𝑥 ∈ ℝ+)) →
(((ψ‘𝑥) −
𝑥) / 𝑥) = (((ψ‘𝑥) / 𝑥) − (𝑥 / 𝑥))) |
240 | 236, 238 | dividd 11606 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝜑 ∧ 𝑠 ∈ ℝ+)
∧ (𝑡 ∈ (0[,]𝐴) ∧ ¬ 𝑠 ≤ 𝑡)) ∧ 𝑦 ∈ ℝ+) ∧ (𝑦 ≤ 𝑥 ∧ 𝑥 ∈ ℝ+)) → (𝑥 / 𝑥) = 1) |
241 | 240 | oveq2d 7229 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧ 𝑠 ∈ ℝ+)
∧ (𝑡 ∈ (0[,]𝐴) ∧ ¬ 𝑠 ≤ 𝑡)) ∧ 𝑦 ∈ ℝ+) ∧ (𝑦 ≤ 𝑥 ∧ 𝑥 ∈ ℝ+)) →
(((ψ‘𝑥) / 𝑥) − (𝑥 / 𝑥)) = (((ψ‘𝑥) / 𝑥) − 1)) |
242 | 231, 239,
241 | 3eqtrrd 2782 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ 𝑠 ∈ ℝ+)
∧ (𝑡 ∈ (0[,]𝐴) ∧ ¬ 𝑠 ≤ 𝑡)) ∧ 𝑦 ∈ ℝ+) ∧ (𝑦 ≤ 𝑥 ∧ 𝑥 ∈ ℝ+)) →
(((ψ‘𝑥) / 𝑥) − 1) = ((𝑅‘𝑥) / 𝑥)) |
243 | 242 | fveq2d 6721 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧ 𝑠 ∈ ℝ+)
∧ (𝑡 ∈ (0[,]𝐴) ∧ ¬ 𝑠 ≤ 𝑡)) ∧ 𝑦 ∈ ℝ+) ∧ (𝑦 ≤ 𝑥 ∧ 𝑥 ∈ ℝ+)) →
(abs‘(((ψ‘𝑥) / 𝑥) − 1)) = (abs‘((𝑅‘𝑥) / 𝑥))) |
244 | 243 | breq1d 5063 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ 𝑠 ∈ ℝ+)
∧ (𝑡 ∈ (0[,]𝐴) ∧ ¬ 𝑠 ≤ 𝑡)) ∧ 𝑦 ∈ ℝ+) ∧ (𝑦 ≤ 𝑥 ∧ 𝑥 ∈ ℝ+)) →
((abs‘(((ψ‘𝑥) / 𝑥) − 1)) ≤ 𝑡 ↔ (abs‘((𝑅‘𝑥) / 𝑥)) ≤ 𝑡)) |
245 | | simprr 773 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑠 ∈ ℝ+) ∧ (𝑡 ∈ (0[,]𝐴) ∧ ¬ 𝑠 ≤ 𝑡)) → ¬ 𝑠 ≤ 𝑡) |
246 | 245 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ 𝑠 ∈ ℝ+)
∧ (𝑡 ∈ (0[,]𝐴) ∧ ¬ 𝑠 ≤ 𝑡)) ∧ 𝑦 ∈ ℝ+) ∧ (𝑦 ≤ 𝑥 ∧ 𝑥 ∈ ℝ+)) → ¬
𝑠 ≤ 𝑡) |
247 | 28 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑠 ∈ ℝ+) ∧ (𝑡 ∈ (0[,]𝐴) ∧ ¬ 𝑠 ≤ 𝑡)) → (0[,]𝐴) ⊆ ℝ) |
248 | 247 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝜑 ∧ 𝑠 ∈ ℝ+)
∧ (𝑡 ∈ (0[,]𝐴) ∧ ¬ 𝑠 ≤ 𝑡)) ∧ 𝑦 ∈ ℝ+) ∧ (𝑦 ≤ 𝑥 ∧ 𝑥 ∈ ℝ+)) →
(0[,]𝐴) ⊆
ℝ) |
249 | | simplrl 777 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑠 ∈ ℝ+) ∧ (𝑡 ∈ (0[,]𝐴) ∧ ¬ 𝑠 ≤ 𝑡)) ∧ 𝑦 ∈ ℝ+) → 𝑡 ∈ (0[,]𝐴)) |
250 | 249 | adantr 484 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝜑 ∧ 𝑠 ∈ ℝ+)
∧ (𝑡 ∈ (0[,]𝐴) ∧ ¬ 𝑠 ≤ 𝑡)) ∧ 𝑦 ∈ ℝ+) ∧ (𝑦 ≤ 𝑥 ∧ 𝑥 ∈ ℝ+)) → 𝑡 ∈ (0[,]𝐴)) |
251 | 248, 250 | sseldd 3902 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧ 𝑠 ∈ ℝ+)
∧ (𝑡 ∈ (0[,]𝐴) ∧ ¬ 𝑠 ≤ 𝑡)) ∧ 𝑦 ∈ ℝ+) ∧ (𝑦 ≤ 𝑥 ∧ 𝑥 ∈ ℝ+)) → 𝑡 ∈
ℝ) |
252 | | simp-4r 784 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝜑 ∧ 𝑠 ∈ ℝ+)
∧ (𝑡 ∈ (0[,]𝐴) ∧ ¬ 𝑠 ≤ 𝑡)) ∧ 𝑦 ∈ ℝ+) ∧ (𝑦 ≤ 𝑥 ∧ 𝑥 ∈ ℝ+)) → 𝑠 ∈
ℝ+) |
253 | 252 | rpred 12628 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧ 𝑠 ∈ ℝ+)
∧ (𝑡 ∈ (0[,]𝐴) ∧ ¬ 𝑠 ≤ 𝑡)) ∧ 𝑦 ∈ ℝ+) ∧ (𝑦 ≤ 𝑥 ∧ 𝑥 ∈ ℝ+)) → 𝑠 ∈
ℝ) |
254 | 251, 253 | ltnled 10979 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ 𝑠 ∈ ℝ+)
∧ (𝑡 ∈ (0[,]𝐴) ∧ ¬ 𝑠 ≤ 𝑡)) ∧ 𝑦 ∈ ℝ+) ∧ (𝑦 ≤ 𝑥 ∧ 𝑥 ∈ ℝ+)) → (𝑡 < 𝑠 ↔ ¬ 𝑠 ≤ 𝑡)) |
255 | 246, 254 | mpbird 260 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧ 𝑠 ∈ ℝ+)
∧ (𝑡 ∈ (0[,]𝐴) ∧ ¬ 𝑠 ≤ 𝑡)) ∧ 𝑦 ∈ ℝ+) ∧ (𝑦 ≤ 𝑥 ∧ 𝑥 ∈ ℝ+)) → 𝑡 < 𝑠) |
256 | 220, 232 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 ∈ ℝ+
→ (ψ‘𝑥)
∈ ℝ) |
257 | | rerpdivcl 12616 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((ψ‘𝑥)
∈ ℝ ∧ 𝑥
∈ ℝ+) → ((ψ‘𝑥) / 𝑥) ∈ ℝ) |
258 | 256, 257 | mpancom 688 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 ∈ ℝ+
→ ((ψ‘𝑥) /
𝑥) ∈
ℝ) |
259 | 258 | ad2antll 729 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝜑 ∧ 𝑠 ∈ ℝ+)
∧ (𝑡 ∈ (0[,]𝐴) ∧ ¬ 𝑠 ≤ 𝑡)) ∧ 𝑦 ∈ ℝ+) ∧ (𝑦 ≤ 𝑥 ∧ 𝑥 ∈ ℝ+)) →
((ψ‘𝑥) / 𝑥) ∈
ℝ) |
260 | | resubcl 11142 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((ψ‘𝑥) /
𝑥) ∈ ℝ ∧ 1
∈ ℝ) → (((ψ‘𝑥) / 𝑥) − 1) ∈ ℝ) |
261 | 259, 43, 260 | sylancl 589 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝜑 ∧ 𝑠 ∈ ℝ+)
∧ (𝑡 ∈ (0[,]𝐴) ∧ ¬ 𝑠 ≤ 𝑡)) ∧ 𝑦 ∈ ℝ+) ∧ (𝑦 ≤ 𝑥 ∧ 𝑥 ∈ ℝ+)) →
(((ψ‘𝑥) / 𝑥) − 1) ∈
ℝ) |
262 | 261 | recnd 10861 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧ 𝑠 ∈ ℝ+)
∧ (𝑡 ∈ (0[,]𝐴) ∧ ¬ 𝑠 ≤ 𝑡)) ∧ 𝑦 ∈ ℝ+) ∧ (𝑦 ≤ 𝑥 ∧ 𝑥 ∈ ℝ+)) →
(((ψ‘𝑥) / 𝑥) − 1) ∈
ℂ) |
263 | 262 | abscld 15000 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ 𝑠 ∈ ℝ+)
∧ (𝑡 ∈ (0[,]𝐴) ∧ ¬ 𝑠 ≤ 𝑡)) ∧ 𝑦 ∈ ℝ+) ∧ (𝑦 ≤ 𝑥 ∧ 𝑥 ∈ ℝ+)) →
(abs‘(((ψ‘𝑥) / 𝑥) − 1)) ∈
ℝ) |
264 | | lelttr 10923 |
. . . . . . . . . . . . . . . . . 18
⊢
(((abs‘(((ψ‘𝑥) / 𝑥) − 1)) ∈ ℝ ∧ 𝑡 ∈ ℝ ∧ 𝑠 ∈ ℝ) →
(((abs‘(((ψ‘𝑥) / 𝑥) − 1)) ≤ 𝑡 ∧ 𝑡 < 𝑠) → (abs‘(((ψ‘𝑥) / 𝑥) − 1)) < 𝑠)) |
265 | 263, 251,
253, 264 | syl3anc 1373 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧ 𝑠 ∈ ℝ+)
∧ (𝑡 ∈ (0[,]𝐴) ∧ ¬ 𝑠 ≤ 𝑡)) ∧ 𝑦 ∈ ℝ+) ∧ (𝑦 ≤ 𝑥 ∧ 𝑥 ∈ ℝ+)) →
(((abs‘(((ψ‘𝑥) / 𝑥) − 1)) ≤ 𝑡 ∧ 𝑡 < 𝑠) → (abs‘(((ψ‘𝑥) / 𝑥) − 1)) < 𝑠)) |
266 | 255, 265 | mpan2d 694 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ 𝑠 ∈ ℝ+)
∧ (𝑡 ∈ (0[,]𝐴) ∧ ¬ 𝑠 ≤ 𝑡)) ∧ 𝑦 ∈ ℝ+) ∧ (𝑦 ≤ 𝑥 ∧ 𝑥 ∈ ℝ+)) →
((abs‘(((ψ‘𝑥) / 𝑥) − 1)) ≤ 𝑡 → (abs‘(((ψ‘𝑥) / 𝑥) − 1)) < 𝑠)) |
267 | 244, 266 | sylbird 263 |
. . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ 𝑠 ∈ ℝ+)
∧ (𝑡 ∈ (0[,]𝐴) ∧ ¬ 𝑠 ≤ 𝑡)) ∧ 𝑦 ∈ ℝ+) ∧ (𝑦 ≤ 𝑥 ∧ 𝑥 ∈ ℝ+)) →
((abs‘((𝑅‘𝑥) / 𝑥)) ≤ 𝑡 → (abs‘(((ψ‘𝑥) / 𝑥) − 1)) < 𝑠)) |
268 | 227, 267 | embantd 59 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 𝑠 ∈ ℝ+)
∧ (𝑡 ∈ (0[,]𝐴) ∧ ¬ 𝑠 ≤ 𝑡)) ∧ 𝑦 ∈ ℝ+) ∧ (𝑦 ≤ 𝑥 ∧ 𝑥 ∈ ℝ+)) → ((𝑥 ∈ (𝑦[,)+∞) → (abs‘((𝑅‘𝑥) / 𝑥)) ≤ 𝑡) → (abs‘(((ψ‘𝑥) / 𝑥) − 1)) < 𝑠)) |
269 | 268 | exp32 424 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑠 ∈ ℝ+) ∧ (𝑡 ∈ (0[,]𝐴) ∧ ¬ 𝑠 ≤ 𝑡)) ∧ 𝑦 ∈ ℝ+) → (𝑦 ≤ 𝑥 → (𝑥 ∈ ℝ+ → ((𝑥 ∈ (𝑦[,)+∞) → (abs‘((𝑅‘𝑥) / 𝑥)) ≤ 𝑡) → (abs‘(((ψ‘𝑥) / 𝑥) − 1)) < 𝑠)))) |
270 | 269 | com24 95 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑠 ∈ ℝ+) ∧ (𝑡 ∈ (0[,]𝐴) ∧ ¬ 𝑠 ≤ 𝑡)) ∧ 𝑦 ∈ ℝ+) → ((𝑥 ∈ (𝑦[,)+∞) → (abs‘((𝑅‘𝑥) / 𝑥)) ≤ 𝑡) → (𝑥 ∈ ℝ+ → (𝑦 ≤ 𝑥 → (abs‘(((ψ‘𝑥) / 𝑥) − 1)) < 𝑠)))) |
271 | 270 | ralimdv2 3099 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑠 ∈ ℝ+) ∧ (𝑡 ∈ (0[,]𝐴) ∧ ¬ 𝑠 ≤ 𝑡)) ∧ 𝑦 ∈ ℝ+) →
(∀𝑥 ∈ (𝑦[,)+∞)(abs‘((𝑅‘𝑥) / 𝑥)) ≤ 𝑡 → ∀𝑥 ∈ ℝ+ (𝑦 ≤ 𝑥 → (abs‘(((ψ‘𝑥) / 𝑥) − 1)) < 𝑠))) |
272 | 219, 271 | syl5bi 245 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑠 ∈ ℝ+) ∧ (𝑡 ∈ (0[,]𝐴) ∧ ¬ 𝑠 ≤ 𝑡)) ∧ 𝑦 ∈ ℝ+) →
(∀𝑧 ∈ (𝑦[,)+∞)(abs‘((𝑅‘𝑧) / 𝑧)) ≤ 𝑡 → ∀𝑥 ∈ ℝ+ (𝑦 ≤ 𝑥 → (abs‘(((ψ‘𝑥) / 𝑥) − 1)) < 𝑠))) |
273 | 272 | reximdva 3193 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑠 ∈ ℝ+) ∧ (𝑡 ∈ (0[,]𝐴) ∧ ¬ 𝑠 ≤ 𝑡)) → (∃𝑦 ∈ ℝ+ ∀𝑧 ∈ (𝑦[,)+∞)(abs‘((𝑅‘𝑧) / 𝑧)) ≤ 𝑡 → ∃𝑦 ∈ ℝ+ ∀𝑥 ∈ ℝ+
(𝑦 ≤ 𝑥 → (abs‘(((ψ‘𝑥) / 𝑥) − 1)) < 𝑠))) |
274 | 273 | anassrs 471 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑠 ∈ ℝ+) ∧ 𝑡 ∈ (0[,]𝐴)) ∧ ¬ 𝑠 ≤ 𝑡) → (∃𝑦 ∈ ℝ+ ∀𝑧 ∈ (𝑦[,)+∞)(abs‘((𝑅‘𝑧) / 𝑧)) ≤ 𝑡 → ∃𝑦 ∈ ℝ+ ∀𝑥 ∈ ℝ+
(𝑦 ≤ 𝑥 → (abs‘(((ψ‘𝑥) / 𝑥) − 1)) < 𝑠))) |
275 | 274 | impancom 455 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑠 ∈ ℝ+) ∧ 𝑡 ∈ (0[,]𝐴)) ∧ ∃𝑦 ∈ ℝ+ ∀𝑧 ∈ (𝑦[,)+∞)(abs‘((𝑅‘𝑧) / 𝑧)) ≤ 𝑡) → (¬ 𝑠 ≤ 𝑡 → ∃𝑦 ∈ ℝ+ ∀𝑥 ∈ ℝ+
(𝑦 ≤ 𝑥 → (abs‘(((ψ‘𝑥) / 𝑥) − 1)) < 𝑠))) |
276 | 275 | expimpd 457 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑠 ∈ ℝ+) ∧ 𝑡 ∈ (0[,]𝐴)) → ((∃𝑦 ∈ ℝ+ ∀𝑧 ∈ (𝑦[,)+∞)(abs‘((𝑅‘𝑧) / 𝑧)) ≤ 𝑡 ∧ ¬ 𝑠 ≤ 𝑡) → ∃𝑦 ∈ ℝ+ ∀𝑥 ∈ ℝ+
(𝑦 ≤ 𝑥 → (abs‘(((ψ‘𝑥) / 𝑥) − 1)) < 𝑠))) |
277 | 276 | rexlimdva 3203 |
. . . . 5
⊢ ((𝜑 ∧ 𝑠 ∈ ℝ+) →
(∃𝑡 ∈ (0[,]𝐴)(∃𝑦 ∈ ℝ+ ∀𝑧 ∈ (𝑦[,)+∞)(abs‘((𝑅‘𝑧) / 𝑧)) ≤ 𝑡 ∧ ¬ 𝑠 ≤ 𝑡) → ∃𝑦 ∈ ℝ+ ∀𝑥 ∈ ℝ+
(𝑦 ≤ 𝑥 → (abs‘(((ψ‘𝑥) / 𝑥) − 1)) < 𝑠))) |
278 | 213, 277 | mpd 15 |
. . . 4
⊢ ((𝜑 ∧ 𝑠 ∈ ℝ+) →
∃𝑦 ∈
ℝ+ ∀𝑥 ∈ ℝ+ (𝑦 ≤ 𝑥 → (abs‘(((ψ‘𝑥) / 𝑥) − 1)) < 𝑠)) |
279 | | ssrexv 3968 |
. . . 4
⊢
(ℝ+ ⊆ ℝ → (∃𝑦 ∈ ℝ+ ∀𝑥 ∈ ℝ+
(𝑦 ≤ 𝑥 → (abs‘(((ψ‘𝑥) / 𝑥) − 1)) < 𝑠) → ∃𝑦 ∈ ℝ ∀𝑥 ∈ ℝ+ (𝑦 ≤ 𝑥 → (abs‘(((ψ‘𝑥) / 𝑥) − 1)) < 𝑠))) |
280 | 1, 278, 279 | mpsyl 68 |
. . 3
⊢ ((𝜑 ∧ 𝑠 ∈ ℝ+) →
∃𝑦 ∈ ℝ
∀𝑥 ∈
ℝ+ (𝑦 ≤
𝑥 →
(abs‘(((ψ‘𝑥) / 𝑥) − 1)) < 𝑠)) |
281 | 280 | ralrimiva 3105 |
. 2
⊢ (𝜑 → ∀𝑠 ∈ ℝ+ ∃𝑦 ∈ ℝ ∀𝑥 ∈ ℝ+
(𝑦 ≤ 𝑥 → (abs‘(((ψ‘𝑥) / 𝑥) − 1)) < 𝑠)) |
282 | 258 | recnd 10861 |
. . . . 5
⊢ (𝑥 ∈ ℝ+
→ ((ψ‘𝑥) /
𝑥) ∈
ℂ) |
283 | 282 | rgen 3071 |
. . . 4
⊢
∀𝑥 ∈
ℝ+ ((ψ‘𝑥) / 𝑥) ∈ ℂ |
284 | 283 | a1i 11 |
. . 3
⊢ (𝜑 → ∀𝑥 ∈ ℝ+
((ψ‘𝑥) / 𝑥) ∈
ℂ) |
285 | 1 | a1i 11 |
. . 3
⊢ (𝜑 → ℝ+
⊆ ℝ) |
286 | | 1cnd 10828 |
. . 3
⊢ (𝜑 → 1 ∈
ℂ) |
287 | 284, 285,
286 | rlim2 15057 |
. 2
⊢ (𝜑 → ((𝑥 ∈ ℝ+ ↦
((ψ‘𝑥) / 𝑥)) ⇝𝑟 1
↔ ∀𝑠 ∈
ℝ+ ∃𝑦 ∈ ℝ ∀𝑥 ∈ ℝ+ (𝑦 ≤ 𝑥 → (abs‘(((ψ‘𝑥) / 𝑥) − 1)) < 𝑠))) |
288 | 281, 287 | mpbird 260 |
1
⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦
((ψ‘𝑥) / 𝑥)) ⇝𝑟
1) |