Step | Hyp | Ref
| Expression |
1 | | dvfsum.s |
. . . . . . 7
⊢ 𝑆 = (𝑇(,)+∞) |
2 | | ioossre 12996 |
. . . . . . 7
⊢ (𝑇(,)+∞) ⊆
ℝ |
3 | 1, 2 | eqsstri 3935 |
. . . . . 6
⊢ 𝑆 ⊆
ℝ |
4 | | dvfsumrlim2.1 |
. . . . . 6
⊢ (𝜑 → 𝑋 ∈ 𝑆) |
5 | 3, 4 | sseldi 3899 |
. . . . 5
⊢ (𝜑 → 𝑋 ∈ ℝ) |
6 | 5 | rexrd 10883 |
. . . 4
⊢ (𝜑 → 𝑋 ∈
ℝ*) |
7 | 5 | renepnfd 10884 |
. . . 4
⊢ (𝜑 → 𝑋 ≠ +∞) |
8 | | icopnfsup 13438 |
. . . 4
⊢ ((𝑋 ∈ ℝ*
∧ 𝑋 ≠ +∞)
→ sup((𝑋[,)+∞),
ℝ*, < ) = +∞) |
9 | 6, 7, 8 | syl2anc 587 |
. . 3
⊢ (𝜑 → sup((𝑋[,)+∞), ℝ*, < ) =
+∞) |
10 | 9 | adantr 484 |
. 2
⊢ ((𝜑 ∧ 𝐺 ⇝𝑟 𝐿) → sup((𝑋[,)+∞), ℝ*, < ) =
+∞) |
11 | | dvfsum.z |
. . . . . . . 8
⊢ 𝑍 =
(ℤ≥‘𝑀) |
12 | | dvfsum.m |
. . . . . . . 8
⊢ (𝜑 → 𝑀 ∈ ℤ) |
13 | | dvfsum.d |
. . . . . . . 8
⊢ (𝜑 → 𝐷 ∈ ℝ) |
14 | | dvfsum.md |
. . . . . . . 8
⊢ (𝜑 → 𝑀 ≤ (𝐷 + 1)) |
15 | | dvfsum.t |
. . . . . . . 8
⊢ (𝜑 → 𝑇 ∈ ℝ) |
16 | | dvfsum.a |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐴 ∈ ℝ) |
17 | | dvfsum.b1 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐵 ∈ 𝑉) |
18 | | dvfsum.b2 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑍) → 𝐵 ∈ ℝ) |
19 | | dvfsum.b3 |
. . . . . . . 8
⊢ (𝜑 → (ℝ D (𝑥 ∈ 𝑆 ↦ 𝐴)) = (𝑥 ∈ 𝑆 ↦ 𝐵)) |
20 | | dvfsum.c |
. . . . . . . 8
⊢ (𝑥 = 𝑘 → 𝐵 = 𝐶) |
21 | | dvfsumrlim.g |
. . . . . . . 8
⊢ 𝐺 = (𝑥 ∈ 𝑆 ↦ (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))𝐶 − 𝐴)) |
22 | 1, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21 | dvfsumrlimf 24922 |
. . . . . . 7
⊢ (𝜑 → 𝐺:𝑆⟶ℝ) |
23 | 22 | ad2antrr 726 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐺 ⇝𝑟 𝐿) ∧ 𝑦 ∈ (𝑋[,)+∞)) → 𝐺:𝑆⟶ℝ) |
24 | 4 | ad2antrr 726 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐺 ⇝𝑟 𝐿) ∧ 𝑦 ∈ (𝑋[,)+∞)) → 𝑋 ∈ 𝑆) |
25 | 23, 24 | ffvelrnd 6905 |
. . . . 5
⊢ (((𝜑 ∧ 𝐺 ⇝𝑟 𝐿) ∧ 𝑦 ∈ (𝑋[,)+∞)) → (𝐺‘𝑋) ∈ ℝ) |
26 | 25 | recnd 10861 |
. . . 4
⊢ (((𝜑 ∧ 𝐺 ⇝𝑟 𝐿) ∧ 𝑦 ∈ (𝑋[,)+∞)) → (𝐺‘𝑋) ∈ ℂ) |
27 | 15 | rexrd 10883 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑇 ∈
ℝ*) |
28 | 4, 1 | eleqtrdi 2848 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑋 ∈ (𝑇(,)+∞)) |
29 | | elioopnf 13031 |
. . . . . . . . . . . . 13
⊢ (𝑇 ∈ ℝ*
→ (𝑋 ∈ (𝑇(,)+∞) ↔ (𝑋 ∈ ℝ ∧ 𝑇 < 𝑋))) |
30 | 27, 29 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑋 ∈ (𝑇(,)+∞) ↔ (𝑋 ∈ ℝ ∧ 𝑇 < 𝑋))) |
31 | 28, 30 | mpbid 235 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑋 ∈ ℝ ∧ 𝑇 < 𝑋)) |
32 | 31 | simprd 499 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑇 < 𝑋) |
33 | | df-ioo 12939 |
. . . . . . . . . . 11
⊢ (,) =
(𝑢 ∈
ℝ*, 𝑣
∈ ℝ* ↦ {𝑤 ∈ ℝ* ∣ (𝑢 < 𝑤 ∧ 𝑤 < 𝑣)}) |
34 | | df-ico 12941 |
. . . . . . . . . . 11
⊢ [,) =
(𝑢 ∈
ℝ*, 𝑣
∈ ℝ* ↦ {𝑤 ∈ ℝ* ∣ (𝑢 ≤ 𝑤 ∧ 𝑤 < 𝑣)}) |
35 | | xrltletr 12747 |
. . . . . . . . . . 11
⊢ ((𝑇 ∈ ℝ*
∧ 𝑋 ∈
ℝ* ∧ 𝑧
∈ ℝ*) → ((𝑇 < 𝑋 ∧ 𝑋 ≤ 𝑧) → 𝑇 < 𝑧)) |
36 | 33, 34, 35 | ixxss1 12953 |
. . . . . . . . . 10
⊢ ((𝑇 ∈ ℝ*
∧ 𝑇 < 𝑋) → (𝑋[,)+∞) ⊆ (𝑇(,)+∞)) |
37 | 27, 32, 36 | syl2anc 587 |
. . . . . . . . 9
⊢ (𝜑 → (𝑋[,)+∞) ⊆ (𝑇(,)+∞)) |
38 | 37, 1 | sseqtrrdi 3952 |
. . . . . . . 8
⊢ (𝜑 → (𝑋[,)+∞) ⊆ 𝑆) |
39 | 38 | adantr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐺 ⇝𝑟 𝐿) → (𝑋[,)+∞) ⊆ 𝑆) |
40 | 39 | sselda 3901 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐺 ⇝𝑟 𝐿) ∧ 𝑦 ∈ (𝑋[,)+∞)) → 𝑦 ∈ 𝑆) |
41 | 23, 40 | ffvelrnd 6905 |
. . . . 5
⊢ (((𝜑 ∧ 𝐺 ⇝𝑟 𝐿) ∧ 𝑦 ∈ (𝑋[,)+∞)) → (𝐺‘𝑦) ∈ ℝ) |
42 | 41 | recnd 10861 |
. . . 4
⊢ (((𝜑 ∧ 𝐺 ⇝𝑟 𝐿) ∧ 𝑦 ∈ (𝑋[,)+∞)) → (𝐺‘𝑦) ∈ ℂ) |
43 | 26, 42 | subcld 11189 |
. . 3
⊢ (((𝜑 ∧ 𝐺 ⇝𝑟 𝐿) ∧ 𝑦 ∈ (𝑋[,)+∞)) → ((𝐺‘𝑋) − (𝐺‘𝑦)) ∈ ℂ) |
44 | | pnfxr 10887 |
. . . . . . 7
⊢ +∞
∈ ℝ* |
45 | | icossre 13016 |
. . . . . . 7
⊢ ((𝑋 ∈ ℝ ∧ +∞
∈ ℝ*) → (𝑋[,)+∞) ⊆
ℝ) |
46 | 5, 44, 45 | sylancl 589 |
. . . . . 6
⊢ (𝜑 → (𝑋[,)+∞) ⊆
ℝ) |
47 | 46 | adantr 484 |
. . . . 5
⊢ ((𝜑 ∧ 𝐺 ⇝𝑟 𝐿) → (𝑋[,)+∞) ⊆
ℝ) |
48 | | rlimf 15062 |
. . . . . . . 8
⊢ (𝐺 ⇝𝑟
𝐿 → 𝐺:dom 𝐺⟶ℂ) |
49 | 48 | adantl 485 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐺 ⇝𝑟 𝐿) → 𝐺:dom 𝐺⟶ℂ) |
50 | | ovex 7246 |
. . . . . . . . 9
⊢
(Σ𝑘 ∈
(𝑀...(⌊‘𝑥))𝐶 − 𝐴) ∈ V |
51 | 50, 21 | dmmpti 6522 |
. . . . . . . 8
⊢ dom 𝐺 = 𝑆 |
52 | 51 | feq2i 6537 |
. . . . . . 7
⊢ (𝐺:dom 𝐺⟶ℂ ↔ 𝐺:𝑆⟶ℂ) |
53 | 49, 52 | sylib 221 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐺 ⇝𝑟 𝐿) → 𝐺:𝑆⟶ℂ) |
54 | 4 | adantr 484 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐺 ⇝𝑟 𝐿) → 𝑋 ∈ 𝑆) |
55 | 53, 54 | ffvelrnd 6905 |
. . . . 5
⊢ ((𝜑 ∧ 𝐺 ⇝𝑟 𝐿) → (𝐺‘𝑋) ∈ ℂ) |
56 | | rlimconst 15105 |
. . . . 5
⊢ (((𝑋[,)+∞) ⊆ ℝ
∧ (𝐺‘𝑋) ∈ ℂ) → (𝑦 ∈ (𝑋[,)+∞) ↦ (𝐺‘𝑋)) ⇝𝑟 (𝐺‘𝑋)) |
57 | 47, 55, 56 | syl2anc 587 |
. . . 4
⊢ ((𝜑 ∧ 𝐺 ⇝𝑟 𝐿) → (𝑦 ∈ (𝑋[,)+∞) ↦ (𝐺‘𝑋)) ⇝𝑟 (𝐺‘𝑋)) |
58 | 53 | feqmptd 6780 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐺 ⇝𝑟 𝐿) → 𝐺 = (𝑦 ∈ 𝑆 ↦ (𝐺‘𝑦))) |
59 | | simpr 488 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐺 ⇝𝑟 𝐿) → 𝐺 ⇝𝑟 𝐿) |
60 | 58, 59 | eqbrtrrd 5077 |
. . . . 5
⊢ ((𝜑 ∧ 𝐺 ⇝𝑟 𝐿) → (𝑦 ∈ 𝑆 ↦ (𝐺‘𝑦)) ⇝𝑟 𝐿) |
61 | 39, 60 | rlimres2 15122 |
. . . 4
⊢ ((𝜑 ∧ 𝐺 ⇝𝑟 𝐿) → (𝑦 ∈ (𝑋[,)+∞) ↦ (𝐺‘𝑦)) ⇝𝑟 𝐿) |
62 | 26, 42, 57, 61 | rlimsub 15206 |
. . 3
⊢ ((𝜑 ∧ 𝐺 ⇝𝑟 𝐿) → (𝑦 ∈ (𝑋[,)+∞) ↦ ((𝐺‘𝑋) − (𝐺‘𝑦))) ⇝𝑟 ((𝐺‘𝑋) − 𝐿)) |
63 | 43, 62 | rlimabs 15170 |
. 2
⊢ ((𝜑 ∧ 𝐺 ⇝𝑟 𝐿) → (𝑦 ∈ (𝑋[,)+∞) ↦ (abs‘((𝐺‘𝑋) − (𝐺‘𝑦)))) ⇝𝑟
(abs‘((𝐺‘𝑋) − 𝐿))) |
64 | 3 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → 𝑆 ⊆ ℝ) |
65 | 64, 16, 17, 19 | dvmptrecl 24921 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐵 ∈ ℝ) |
66 | 65 | ralrimiva 3105 |
. . . . . 6
⊢ (𝜑 → ∀𝑥 ∈ 𝑆 𝐵 ∈ ℝ) |
67 | | nfcsb1v 3836 |
. . . . . . . 8
⊢
Ⅎ𝑥⦋𝑋 / 𝑥⦌𝐵 |
68 | 67 | nfel1 2920 |
. . . . . . 7
⊢
Ⅎ𝑥⦋𝑋 / 𝑥⦌𝐵 ∈ ℝ |
69 | | csbeq1a 3825 |
. . . . . . . 8
⊢ (𝑥 = 𝑋 → 𝐵 = ⦋𝑋 / 𝑥⦌𝐵) |
70 | 69 | eleq1d 2822 |
. . . . . . 7
⊢ (𝑥 = 𝑋 → (𝐵 ∈ ℝ ↔ ⦋𝑋 / 𝑥⦌𝐵 ∈ ℝ)) |
71 | 68, 70 | rspc 3525 |
. . . . . 6
⊢ (𝑋 ∈ 𝑆 → (∀𝑥 ∈ 𝑆 𝐵 ∈ ℝ → ⦋𝑋 / 𝑥⦌𝐵 ∈ ℝ)) |
72 | 4, 66, 71 | sylc 65 |
. . . . 5
⊢ (𝜑 → ⦋𝑋 / 𝑥⦌𝐵 ∈ ℝ) |
73 | 72 | recnd 10861 |
. . . 4
⊢ (𝜑 → ⦋𝑋 / 𝑥⦌𝐵 ∈ ℂ) |
74 | | rlimconst 15105 |
. . . 4
⊢ (((𝑋[,)+∞) ⊆ ℝ
∧ ⦋𝑋 /
𝑥⦌𝐵 ∈ ℂ) → (𝑦 ∈ (𝑋[,)+∞) ↦ ⦋𝑋 / 𝑥⦌𝐵) ⇝𝑟
⦋𝑋 / 𝑥⦌𝐵) |
75 | 46, 73, 74 | syl2anc 587 |
. . 3
⊢ (𝜑 → (𝑦 ∈ (𝑋[,)+∞) ↦ ⦋𝑋 / 𝑥⦌𝐵) ⇝𝑟
⦋𝑋 / 𝑥⦌𝐵) |
76 | 75 | adantr 484 |
. 2
⊢ ((𝜑 ∧ 𝐺 ⇝𝑟 𝐿) → (𝑦 ∈ (𝑋[,)+∞) ↦ ⦋𝑋 / 𝑥⦌𝐵) ⇝𝑟
⦋𝑋 / 𝑥⦌𝐵) |
77 | 43 | abscld 15000 |
. 2
⊢ (((𝜑 ∧ 𝐺 ⇝𝑟 𝐿) ∧ 𝑦 ∈ (𝑋[,)+∞)) → (abs‘((𝐺‘𝑋) − (𝐺‘𝑦))) ∈ ℝ) |
78 | 72 | ad2antrr 726 |
. 2
⊢ (((𝜑 ∧ 𝐺 ⇝𝑟 𝐿) ∧ 𝑦 ∈ (𝑋[,)+∞)) → ⦋𝑋 / 𝑥⦌𝐵 ∈ ℝ) |
79 | 26, 42 | abssubd 15017 |
. . 3
⊢ (((𝜑 ∧ 𝐺 ⇝𝑟 𝐿) ∧ 𝑦 ∈ (𝑋[,)+∞)) → (abs‘((𝐺‘𝑋) − (𝐺‘𝑦))) = (abs‘((𝐺‘𝑦) − (𝐺‘𝑋)))) |
80 | 12 | adantr 484 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋[,)+∞)) → 𝑀 ∈ ℤ) |
81 | 13 | adantr 484 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋[,)+∞)) → 𝐷 ∈ ℝ) |
82 | 14 | adantr 484 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋[,)+∞)) → 𝑀 ≤ (𝐷 + 1)) |
83 | 15 | adantr 484 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋[,)+∞)) → 𝑇 ∈ ℝ) |
84 | 16 | adantlr 715 |
. . . . 5
⊢ (((𝜑 ∧ 𝑦 ∈ (𝑋[,)+∞)) ∧ 𝑥 ∈ 𝑆) → 𝐴 ∈ ℝ) |
85 | 17 | adantlr 715 |
. . . . 5
⊢ (((𝜑 ∧ 𝑦 ∈ (𝑋[,)+∞)) ∧ 𝑥 ∈ 𝑆) → 𝐵 ∈ 𝑉) |
86 | 18 | adantlr 715 |
. . . . 5
⊢ (((𝜑 ∧ 𝑦 ∈ (𝑋[,)+∞)) ∧ 𝑥 ∈ 𝑍) → 𝐵 ∈ ℝ) |
87 | 19 | adantr 484 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋[,)+∞)) → (ℝ D (𝑥 ∈ 𝑆 ↦ 𝐴)) = (𝑥 ∈ 𝑆 ↦ 𝐵)) |
88 | 44 | a1i 11 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋[,)+∞)) → +∞ ∈
ℝ*) |
89 | | 3simpa 1150 |
. . . . . . 7
⊢ ((𝐷 ≤ 𝑥 ∧ 𝑥 ≤ 𝑘 ∧ 𝑘 ≤ +∞) → (𝐷 ≤ 𝑥 ∧ 𝑥 ≤ 𝑘)) |
90 | | dvfsumrlim.l |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) ∧ (𝐷 ≤ 𝑥 ∧ 𝑥 ≤ 𝑘)) → 𝐶 ≤ 𝐵) |
91 | 89, 90 | syl3an3 1167 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) ∧ (𝐷 ≤ 𝑥 ∧ 𝑥 ≤ 𝑘 ∧ 𝑘 ≤ +∞)) → 𝐶 ≤ 𝐵) |
92 | 91 | 3adant1r 1179 |
. . . . 5
⊢ (((𝜑 ∧ 𝑦 ∈ (𝑋[,)+∞)) ∧ (𝑥 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) ∧ (𝐷 ≤ 𝑥 ∧ 𝑥 ≤ 𝑘 ∧ 𝑘 ≤ +∞)) → 𝐶 ≤ 𝐵) |
93 | | dvfsumrlim.k |
. . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ 𝑆 ↦ 𝐵) ⇝𝑟
0) |
94 | 1, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 90, 21, 93 | dvfsumrlimge0 24927 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝐷 ≤ 𝑥)) → 0 ≤ 𝐵) |
95 | 94 | 3adantr3 1173 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝐷 ≤ 𝑥 ∧ 𝑥 ≤ +∞)) → 0 ≤ 𝐵) |
96 | 95 | adantlr 715 |
. . . . 5
⊢ (((𝜑 ∧ 𝑦 ∈ (𝑋[,)+∞)) ∧ (𝑥 ∈ 𝑆 ∧ 𝐷 ≤ 𝑥 ∧ 𝑥 ≤ +∞)) → 0 ≤ 𝐵) |
97 | 4 | adantr 484 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋[,)+∞)) → 𝑋 ∈ 𝑆) |
98 | 38 | sselda 3901 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋[,)+∞)) → 𝑦 ∈ 𝑆) |
99 | | dvfsumrlim2.2 |
. . . . . 6
⊢ (𝜑 → 𝐷 ≤ 𝑋) |
100 | 99 | adantr 484 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋[,)+∞)) → 𝐷 ≤ 𝑋) |
101 | | elicopnf 13033 |
. . . . . . 7
⊢ (𝑋 ∈ ℝ → (𝑦 ∈ (𝑋[,)+∞) ↔ (𝑦 ∈ ℝ ∧ 𝑋 ≤ 𝑦))) |
102 | 5, 101 | syl 17 |
. . . . . 6
⊢ (𝜑 → (𝑦 ∈ (𝑋[,)+∞) ↔ (𝑦 ∈ ℝ ∧ 𝑋 ≤ 𝑦))) |
103 | 102 | simplbda 503 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋[,)+∞)) → 𝑋 ≤ 𝑦) |
104 | 102 | simprbda 502 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋[,)+∞)) → 𝑦 ∈ ℝ) |
105 | 104 | rexrd 10883 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋[,)+∞)) → 𝑦 ∈ ℝ*) |
106 | | pnfge 12722 |
. . . . . 6
⊢ (𝑦 ∈ ℝ*
→ 𝑦 ≤
+∞) |
107 | 105, 106 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋[,)+∞)) → 𝑦 ≤ +∞) |
108 | 1, 11, 80, 81, 82, 83, 84, 85, 86, 87, 20, 88, 92, 21, 96, 97, 98, 100, 103, 107 | dvfsumlem4 24926 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋[,)+∞)) → (abs‘((𝐺‘𝑦) − (𝐺‘𝑋))) ≤ ⦋𝑋 / 𝑥⦌𝐵) |
109 | 108 | adantlr 715 |
. . 3
⊢ (((𝜑 ∧ 𝐺 ⇝𝑟 𝐿) ∧ 𝑦 ∈ (𝑋[,)+∞)) → (abs‘((𝐺‘𝑦) − (𝐺‘𝑋))) ≤ ⦋𝑋 / 𝑥⦌𝐵) |
110 | 79, 109 | eqbrtrd 5075 |
. 2
⊢ (((𝜑 ∧ 𝐺 ⇝𝑟 𝐿) ∧ 𝑦 ∈ (𝑋[,)+∞)) → (abs‘((𝐺‘𝑋) − (𝐺‘𝑦))) ≤ ⦋𝑋 / 𝑥⦌𝐵) |
111 | 10, 63, 76, 77, 78, 110 | rlimle 15211 |
1
⊢ ((𝜑 ∧ 𝐺 ⇝𝑟 𝐿) → (abs‘((𝐺‘𝑋) − 𝐿)) ≤ ⦋𝑋 / 𝑥⦌𝐵) |