Step | Hyp | Ref
| Expression |
1 | | limccl 23445 |
. . . . . . . . . . . . 13
⊢ ((𝐹 ↾ (𝐵(,)+∞)) limℂ 𝐵) ⊆
ℂ |
2 | | limclner.r |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑅 ∈ ((𝐹 ↾ (𝐵(,)+∞)) limℂ 𝐵)) |
3 | 1, 2 | sseldi 3566 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑅 ∈ ℂ) |
4 | 3 | ad2antrr 758 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+
∃𝑧 ∈
ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) → 𝑅 ∈ ℂ) |
5 | | limccl 23445 |
. . . . . . . . . . . . 13
⊢ ((𝐹 ↾ (-∞(,)𝐵)) limℂ 𝐵) ⊆
ℂ |
6 | | limclner.l |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐿 ∈ ((𝐹 ↾ (-∞(,)𝐵)) limℂ 𝐵)) |
7 | 5, 6 | sseldi 3566 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐿 ∈ ℂ) |
8 | 7 | ad2antrr 758 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+
∃𝑧 ∈
ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) → 𝐿 ∈ ℂ) |
9 | 4, 8 | subcld 10271 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+
∃𝑧 ∈
ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) → (𝑅 − 𝐿) ∈ ℂ) |
10 | | limclner.lner |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐿 ≠ 𝑅) |
11 | 10 | necomd 2837 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑅 ≠ 𝐿) |
12 | 11 | ad2antrr 758 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+
∃𝑧 ∈
ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) → 𝑅 ≠ 𝐿) |
13 | 4, 8, 12 | subne0d 10280 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+
∃𝑧 ∈
ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) → (𝑅 − 𝐿) ≠ 0) |
14 | 9, 13 | absrpcld 14035 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+
∃𝑧 ∈
ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) → (abs‘(𝑅 − 𝐿)) ∈
ℝ+) |
15 | | 4re 10974 |
. . . . . . . . . . 11
⊢ 4 ∈
ℝ |
16 | | 4pos 10993 |
. . . . . . . . . . 11
⊢ 0 <
4 |
17 | 15, 16 | elrpii 11711 |
. . . . . . . . . 10
⊢ 4 ∈
ℝ+ |
18 | 17 | a1i 11 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+
∃𝑧 ∈
ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) → 4 ∈
ℝ+) |
19 | 14, 18 | rpdivcld 11765 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+
∃𝑧 ∈
ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) → ((abs‘(𝑅 − 𝐿)) / 4) ∈
ℝ+) |
20 | | nfv 1830 |
. . . . . . . . . . 11
⊢
Ⅎ𝑦(𝜑 ∧ 𝑥 ∈ ℂ) |
21 | | nfra1 2925 |
. . . . . . . . . . 11
⊢
Ⅎ𝑦∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+
∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦) |
22 | 20, 21 | nfan 1816 |
. . . . . . . . . 10
⊢
Ⅎ𝑦((𝜑 ∧ 𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+
∃𝑧 ∈
ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) |
23 | | nfv 1830 |
. . . . . . . . . 10
⊢
Ⅎ𝑦(((abs‘(𝑅 − 𝐿)) / 4) ∈ ℝ+ →
∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐴 (abs‘(𝑅 − 𝐿)) < (4 · ((abs‘(𝑅 − 𝐿)) / 4))) |
24 | 22, 23 | nfim 1813 |
. . . . . . . . 9
⊢
Ⅎ𝑦(((𝜑 ∧ 𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+
∃𝑧 ∈
ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) → (((abs‘(𝑅 − 𝐿)) / 4) ∈ ℝ+ →
∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐴 (abs‘(𝑅 − 𝐿)) < (4 · ((abs‘(𝑅 − 𝐿)) / 4)))) |
25 | | ovex 6577 |
. . . . . . . . 9
⊢
((abs‘(𝑅
− 𝐿)) / 4) ∈
V |
26 | | eleq1 2676 |
. . . . . . . . . . 11
⊢ (𝑦 = ((abs‘(𝑅 − 𝐿)) / 4) → (𝑦 ∈ ℝ+ ↔
((abs‘(𝑅 −
𝐿)) / 4) ∈
ℝ+)) |
27 | | oveq2 6557 |
. . . . . . . . . . . . 13
⊢ (𝑦 = ((abs‘(𝑅 − 𝐿)) / 4) → (4 · 𝑦) = (4 ·
((abs‘(𝑅 −
𝐿)) / 4))) |
28 | 27 | breq2d 4595 |
. . . . . . . . . . . 12
⊢ (𝑦 = ((abs‘(𝑅 − 𝐿)) / 4) → ((abs‘(𝑅 − 𝐿)) < (4 · 𝑦) ↔ (abs‘(𝑅 − 𝐿)) < (4 · ((abs‘(𝑅 − 𝐿)) / 4)))) |
29 | 28 | 2rexbidv 3039 |
. . . . . . . . . . 11
⊢ (𝑦 = ((abs‘(𝑅 − 𝐿)) / 4) → (∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐴 (abs‘(𝑅 − 𝐿)) < (4 · 𝑦) ↔ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐴 (abs‘(𝑅 − 𝐿)) < (4 · ((abs‘(𝑅 − 𝐿)) / 4)))) |
30 | 26, 29 | imbi12d 333 |
. . . . . . . . . 10
⊢ (𝑦 = ((abs‘(𝑅 − 𝐿)) / 4) → ((𝑦 ∈ ℝ+ →
∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐴 (abs‘(𝑅 − 𝐿)) < (4 · 𝑦)) ↔ (((abs‘(𝑅 − 𝐿)) / 4) ∈ ℝ+ →
∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐴 (abs‘(𝑅 − 𝐿)) < (4 · ((abs‘(𝑅 − 𝐿)) / 4))))) |
31 | 30 | imbi2d 329 |
. . . . . . . . 9
⊢ (𝑦 = ((abs‘(𝑅 − 𝐿)) / 4) → ((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+
∃𝑧 ∈
ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) → (𝑦 ∈ ℝ+ →
∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐴 (abs‘(𝑅 − 𝐿)) < (4 · 𝑦))) ↔ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+
∃𝑧 ∈
ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) → (((abs‘(𝑅 − 𝐿)) / 4) ∈ ℝ+ →
∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐴 (abs‘(𝑅 − 𝐿)) < (4 · ((abs‘(𝑅 − 𝐿)) / 4)))))) |
32 | | simpll 786 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+
∃𝑧 ∈
ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑦 ∈ ℝ+) → (𝜑 ∧ 𝑥 ∈ ℂ)) |
33 | | simpr 476 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+
∃𝑧 ∈
ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑦 ∈ ℝ+) → 𝑦 ∈
ℝ+) |
34 | | rspa 2914 |
. . . . . . . . . . . 12
⊢
((∀𝑦 ∈
ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦) ∧ 𝑦 ∈ ℝ+) →
∃𝑧 ∈
ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) |
35 | 34 | adantll 746 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+
∃𝑧 ∈
ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑦 ∈ ℝ+) →
∃𝑧 ∈
ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) |
36 | | limclner.f |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → 𝐹:𝐴⟶ℂ) |
37 | | fresin 5986 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝐹:𝐴⟶ℂ → (𝐹 ↾ (-∞(,)𝐵)):(𝐴 ∩ (-∞(,)𝐵))⟶ℂ) |
38 | 36, 37 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → (𝐹 ↾ (-∞(,)𝐵)):(𝐴 ∩ (-∞(,)𝐵))⟶ℂ) |
39 | | inss2 3796 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝐴 ∩ (-∞(,)𝐵)) ⊆ (-∞(,)𝐵) |
40 | | ioosscn 38563 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(-∞(,)𝐵)
⊆ ℂ |
41 | 39, 40 | sstri 3577 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝐴 ∩ (-∞(,)𝐵)) ⊆
ℂ |
42 | 41 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → (𝐴 ∩ (-∞(,)𝐵)) ⊆ ℂ) |
43 | | limclner.j |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ 𝐽 = (topGen‘ran
(,)) |
44 | | retop 22375 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(topGen‘ran (,)) ∈ Top |
45 | 43, 44 | eqeltri 2684 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ 𝐽 ∈ Top |
46 | | ioossre 12106 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(-∞(,)𝐵)
⊆ ℝ |
47 | 39, 46 | sstri 3577 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝐴 ∩ (-∞(,)𝐵)) ⊆
ℝ |
48 | | uniretop 22376 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ℝ =
∪ (topGen‘ran (,)) |
49 | 43 | unieqi 4381 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ∪ 𝐽 =
∪ (topGen‘ran (,)) |
50 | 48, 49 | eqtr4i 2635 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ℝ =
∪ 𝐽 |
51 | 50 | lpss 20756 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝐽 ∈ Top ∧ (𝐴 ∩ (-∞(,)𝐵)) ⊆ ℝ) →
((limPt‘𝐽)‘(𝐴 ∩ (-∞(,)𝐵))) ⊆ ℝ) |
52 | 45, 47, 51 | mp2an 704 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((limPt‘𝐽)‘(𝐴 ∩ (-∞(,)𝐵))) ⊆ ℝ |
53 | | limclner.blp1 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → 𝐵 ∈ ((limPt‘𝐽)‘(𝐴 ∩ (-∞(,)𝐵)))) |
54 | 52, 53 | sseldi 3566 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → 𝐵 ∈ ℝ) |
55 | 54 | recnd 9947 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → 𝐵 ∈ ℂ) |
56 | 38, 42, 55 | ellimc3 23449 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (𝐿 ∈ ((𝐹 ↾ (-∞(,)𝐵)) limℂ 𝐵) ↔ (𝐿 ∈ ℂ ∧ ∀𝑦 ∈ ℝ+
∃𝑣 ∈
ℝ+ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)))) |
57 | 6, 56 | mpbid 221 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝐿 ∈ ℂ ∧ ∀𝑦 ∈ ℝ+
∃𝑣 ∈
ℝ+ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦))) |
58 | 57 | simprd 478 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ∀𝑦 ∈ ℝ+ ∃𝑣 ∈ ℝ+
∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) |
59 | 58 | r19.21bi 2916 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) →
∃𝑣 ∈
ℝ+ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) |
60 | 59 | 3ad2ant1 1075 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+
∧ ∀𝑤 ∈
𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) → ∃𝑣 ∈ ℝ+ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) |
61 | | simp11l 1165 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+
∧ ∀𝑤 ∈
𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧
∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) → 𝜑) |
62 | | simp12 1085 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+
∧ ∀𝑤 ∈
𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧
∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) → 𝑧 ∈ ℝ+) |
63 | | simp2 1055 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+
∧ ∀𝑤 ∈
𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧
∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) → 𝑣 ∈ ℝ+) |
64 | | ifcl 4080 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑧 ∈ ℝ+
∧ 𝑣 ∈
ℝ+) → if(𝑧 ≤ 𝑣, 𝑧, 𝑣) ∈
ℝ+) |
65 | 64 | 3adant1 1072 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+)
→ if(𝑧 ≤ 𝑣, 𝑧, 𝑣) ∈
ℝ+) |
66 | | inss1 3795 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(((limPt‘𝐾)‘(𝐴 ∩ (-∞(,)𝐵))) ∩ ℝ) ⊆
((limPt‘𝐾)‘(𝐴 ∩ (-∞(,)𝐵))) |
67 | 66 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝜑 → (((limPt‘𝐾)‘(𝐴 ∩ (-∞(,)𝐵))) ∩ ℝ) ⊆
((limPt‘𝐾)‘(𝐴 ∩ (-∞(,)𝐵)))) |
68 | | limclner.k |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ 𝐾 =
(TopOpen‘ℂfld) |
69 | 68 | cnfldtop 22397 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ 𝐾 ∈ Top |
70 | 69 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝜑 → 𝐾 ∈ Top) |
71 | | ax-resscn 9872 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ℝ
⊆ ℂ |
72 | 71 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝜑 → ℝ ⊆
ℂ) |
73 | 47 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝜑 → (𝐴 ∩ (-∞(,)𝐵)) ⊆ ℝ) |
74 | | unicntop 38230 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ℂ =
∪
(TopOpen‘ℂfld) |
75 | 68 | unieqi 4381 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ∪ 𝐾 =
∪
(TopOpen‘ℂfld) |
76 | 74, 75 | eqtr4i 2635 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ℂ =
∪ 𝐾 |
77 | 68 | tgioo2 22414 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
(topGen‘ran (,)) = (𝐾 ↾t
ℝ) |
78 | 43, 77 | eqtri 2632 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ 𝐽 = (𝐾 ↾t
ℝ) |
79 | 76, 78 | restlp 20797 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝐾 ∈ Top ∧ ℝ
⊆ ℂ ∧ (𝐴
∩ (-∞(,)𝐵))
⊆ ℝ) → ((limPt‘𝐽)‘(𝐴 ∩ (-∞(,)𝐵))) = (((limPt‘𝐾)‘(𝐴 ∩ (-∞(,)𝐵))) ∩ ℝ)) |
80 | 70, 72, 73, 79 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝜑 → ((limPt‘𝐽)‘(𝐴 ∩ (-∞(,)𝐵))) = (((limPt‘𝐾)‘(𝐴 ∩ (-∞(,)𝐵))) ∩ ℝ)) |
81 | 68 | eqcomi 2619 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
(TopOpen‘ℂfld) = 𝐾 |
82 | 81 | fveq2i 6106 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
(limPt‘(TopOpen‘ℂfld)) = (limPt‘𝐾) |
83 | 82 | fveq1i 6104 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
((limPt‘(TopOpen‘ℂfld))‘(𝐴 ∩ (-∞(,)𝐵))) = ((limPt‘𝐾)‘(𝐴 ∩ (-∞(,)𝐵))) |
84 | 83 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝜑 →
((limPt‘(TopOpen‘ℂfld))‘(𝐴 ∩ (-∞(,)𝐵))) = ((limPt‘𝐾)‘(𝐴 ∩ (-∞(,)𝐵)))) |
85 | 67, 80, 84 | 3sstr4d 3611 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → ((limPt‘𝐽)‘(𝐴 ∩ (-∞(,)𝐵))) ⊆
((limPt‘(TopOpen‘ℂfld))‘(𝐴 ∩ (-∞(,)𝐵)))) |
86 | 85, 53 | sseldd 3569 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → 𝐵 ∈
((limPt‘(TopOpen‘ℂfld))‘(𝐴 ∩ (-∞(,)𝐵)))) |
87 | 42, 55 | islpcn 38706 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → (𝐵 ∈
((limPt‘(TopOpen‘ℂfld))‘(𝐴 ∩ (-∞(,)𝐵))) ↔ ∀𝑢 ∈ ℝ+ ∃𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵})(abs‘(𝑎 − 𝐵)) < 𝑢)) |
88 | 86, 87 | mpbid 221 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → ∀𝑢 ∈ ℝ+ ∃𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵})(abs‘(𝑎 − 𝐵)) < 𝑢) |
89 | 88 | 3ad2ant1 1075 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+)
→ ∀𝑢 ∈
ℝ+ ∃𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵})(abs‘(𝑎 − 𝐵)) < 𝑢) |
90 | | breq2 4587 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑢 = if(𝑧 ≤ 𝑣, 𝑧, 𝑣) → ((abs‘(𝑎 − 𝐵)) < 𝑢 ↔ (abs‘(𝑎 − 𝐵)) < if(𝑧 ≤ 𝑣, 𝑧, 𝑣))) |
91 | 90 | rexbidv 3034 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑢 = if(𝑧 ≤ 𝑣, 𝑧, 𝑣) → (∃𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵})(abs‘(𝑎 − 𝐵)) < 𝑢 ↔ ∃𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵})(abs‘(𝑎 − 𝐵)) < if(𝑧 ≤ 𝑣, 𝑧, 𝑣))) |
92 | 91 | rspcva 3280 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((if(𝑧 ≤ 𝑣, 𝑧, 𝑣) ∈ ℝ+ ∧
∀𝑢 ∈
ℝ+ ∃𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵})(abs‘(𝑎 − 𝐵)) < 𝑢) → ∃𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵})(abs‘(𝑎 − 𝐵)) < if(𝑧 ≤ 𝑣, 𝑧, 𝑣)) |
93 | 65, 89, 92 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+)
→ ∃𝑎 ∈
((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵})(abs‘(𝑎 − 𝐵)) < if(𝑧 ≤ 𝑣, 𝑧, 𝑣)) |
94 | | eldifi 3694 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵}) → 𝑎 ∈ (𝐴 ∩ (-∞(,)𝐵))) |
95 | 47, 94 | sseldi 3566 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵}) → 𝑎 ∈ ℝ) |
96 | 72 | sselda 3568 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝜑 ∧ 𝑎 ∈ ℝ) → 𝑎 ∈ ℂ) |
97 | 55 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝜑 ∧ 𝑎 ∈ ℝ) → 𝐵 ∈ ℂ) |
98 | 96, 97 | subcld 10271 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝜑 ∧ 𝑎 ∈ ℝ) → (𝑎 − 𝐵) ∈ ℂ) |
99 | 98 | abscld 14023 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝜑 ∧ 𝑎 ∈ ℝ) → (abs‘(𝑎 − 𝐵)) ∈ ℝ) |
100 | 99 | 3ad2antl1 1216 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+)
∧ 𝑎 ∈ ℝ)
→ (abs‘(𝑎
− 𝐵)) ∈
ℝ) |
101 | 100 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+)
∧ 𝑎 ∈ ℝ)
∧ (abs‘(𝑎 −
𝐵)) < if(𝑧 ≤ 𝑣, 𝑧, 𝑣)) → (abs‘(𝑎 − 𝐵)) ∈ ℝ) |
102 | 65 | rpred 11748 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+)
→ if(𝑧 ≤ 𝑣, 𝑧, 𝑣) ∈ ℝ) |
103 | 102 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+)
∧ 𝑎 ∈ ℝ)
∧ (abs‘(𝑎 −
𝐵)) < if(𝑧 ≤ 𝑣, 𝑧, 𝑣)) → if(𝑧 ≤ 𝑣, 𝑧, 𝑣) ∈ ℝ) |
104 | | rpre 11715 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑧 ∈ ℝ+
→ 𝑧 ∈
ℝ) |
105 | 104 | 3ad2ant2 1076 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+)
→ 𝑧 ∈
ℝ) |
106 | 105 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+)
∧ 𝑎 ∈ ℝ)
∧ (abs‘(𝑎 −
𝐵)) < if(𝑧 ≤ 𝑣, 𝑧, 𝑣)) → 𝑧 ∈ ℝ) |
107 | | simpr 476 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+)
∧ 𝑎 ∈ ℝ)
∧ (abs‘(𝑎 −
𝐵)) < if(𝑧 ≤ 𝑣, 𝑧, 𝑣)) → (abs‘(𝑎 − 𝐵)) < if(𝑧 ≤ 𝑣, 𝑧, 𝑣)) |
108 | | rpre 11715 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑣 ∈ ℝ+
→ 𝑣 ∈
ℝ) |
109 | | min1 11894 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝑧 ∈ ℝ ∧ 𝑣 ∈ ℝ) → if(𝑧 ≤ 𝑣, 𝑧, 𝑣) ≤ 𝑧) |
110 | 104, 108,
109 | syl2an 493 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑧 ∈ ℝ+
∧ 𝑣 ∈
ℝ+) → if(𝑧 ≤ 𝑣, 𝑧, 𝑣) ≤ 𝑧) |
111 | 110 | 3adant1 1072 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+)
→ if(𝑧 ≤ 𝑣, 𝑧, 𝑣) ≤ 𝑧) |
112 | 111 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+)
∧ 𝑎 ∈ ℝ)
∧ (abs‘(𝑎 −
𝐵)) < if(𝑧 ≤ 𝑣, 𝑧, 𝑣)) → if(𝑧 ≤ 𝑣, 𝑧, 𝑣) ≤ 𝑧) |
113 | 101, 103,
106, 107, 112 | ltletrd 10076 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+)
∧ 𝑎 ∈ ℝ)
∧ (abs‘(𝑎 −
𝐵)) < if(𝑧 ≤ 𝑣, 𝑧, 𝑣)) → (abs‘(𝑎 − 𝐵)) < 𝑧) |
114 | 108 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑧 ∈ ℝ+
∧ 𝑣 ∈
ℝ+) → 𝑣 ∈ ℝ) |
115 | 114 | 3adant1 1072 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+)
→ 𝑣 ∈
ℝ) |
116 | 115 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+)
∧ 𝑎 ∈ ℝ)
∧ (abs‘(𝑎 −
𝐵)) < if(𝑧 ≤ 𝑣, 𝑧, 𝑣)) → 𝑣 ∈ ℝ) |
117 | | min2 11895 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝑧 ∈ ℝ ∧ 𝑣 ∈ ℝ) → if(𝑧 ≤ 𝑣, 𝑧, 𝑣) ≤ 𝑣) |
118 | 104, 108,
117 | syl2an 493 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑧 ∈ ℝ+
∧ 𝑣 ∈
ℝ+) → if(𝑧 ≤ 𝑣, 𝑧, 𝑣) ≤ 𝑣) |
119 | 118 | 3adant1 1072 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+)
→ if(𝑧 ≤ 𝑣, 𝑧, 𝑣) ≤ 𝑣) |
120 | 119 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+)
∧ 𝑎 ∈ ℝ)
∧ (abs‘(𝑎 −
𝐵)) < if(𝑧 ≤ 𝑣, 𝑧, 𝑣)) → if(𝑧 ≤ 𝑣, 𝑧, 𝑣) ≤ 𝑣) |
121 | 101, 103,
116, 107, 120 | ltletrd 10076 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+)
∧ 𝑎 ∈ ℝ)
∧ (abs‘(𝑎 −
𝐵)) < if(𝑧 ≤ 𝑣, 𝑧, 𝑣)) → (abs‘(𝑎 − 𝐵)) < 𝑣) |
122 | 113, 121 | jca 553 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+)
∧ 𝑎 ∈ ℝ)
∧ (abs‘(𝑎 −
𝐵)) < if(𝑧 ≤ 𝑣, 𝑧, 𝑣)) → ((abs‘(𝑎 − 𝐵)) < 𝑧 ∧ (abs‘(𝑎 − 𝐵)) < 𝑣)) |
123 | 122 | ex 449 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+)
∧ 𝑎 ∈ ℝ)
→ ((abs‘(𝑎
− 𝐵)) < if(𝑧 ≤ 𝑣, 𝑧, 𝑣) → ((abs‘(𝑎 − 𝐵)) < 𝑧 ∧ (abs‘(𝑎 − 𝐵)) < 𝑣))) |
124 | 95, 123 | sylan2 490 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+)
∧ 𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵})) → ((abs‘(𝑎 − 𝐵)) < if(𝑧 ≤ 𝑣, 𝑧, 𝑣) → ((abs‘(𝑎 − 𝐵)) < 𝑧 ∧ (abs‘(𝑎 − 𝐵)) < 𝑣))) |
125 | 124 | reximdva 3000 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+)
→ (∃𝑎 ∈
((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵})(abs‘(𝑎 − 𝐵)) < if(𝑧 ≤ 𝑣, 𝑧, 𝑣) → ∃𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵})((abs‘(𝑎 − 𝐵)) < 𝑧 ∧ (abs‘(𝑎 − 𝐵)) < 𝑣))) |
126 | 93, 125 | mpd 15 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+)
→ ∃𝑎 ∈
((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵})((abs‘(𝑎 − 𝐵)) < 𝑧 ∧ (abs‘(𝑎 − 𝐵)) < 𝑣)) |
127 | 61, 62, 63, 126 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+
∧ ∀𝑤 ∈
𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧
∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) → ∃𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵})((abs‘(𝑎 − 𝐵)) < 𝑧 ∧ (abs‘(𝑎 − 𝐵)) < 𝑣)) |
128 | | nfv 1830 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
Ⅎ𝑎(((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+
∧ ∀𝑤 ∈
𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧
∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) |
129 | | nfre1 2988 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
Ⅎ𝑎∃𝑎 ∈ 𝐴 ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦) |
130 | | inss1 3795 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝐴 ∩ (-∞(,)𝐵)) ⊆ 𝐴 |
131 | 130, 94 | sseldi 3566 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵}) → 𝑎 ∈ 𝐴) |
132 | 131 | 3ad2ant2 1076 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑧 ∈
ℝ+ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧
∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) ∧ 𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵}) ∧ ((abs‘(𝑎 − 𝐵)) < 𝑧 ∧ (abs‘(𝑎 − 𝐵)) < 𝑣)) → 𝑎 ∈ 𝐴) |
133 | | simp113 1185 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑧 ∈
ℝ+ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧
∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) ∧ 𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵}) ∧ ((abs‘(𝑎 − 𝐵)) < 𝑧 ∧ (abs‘(𝑎 − 𝐵)) < 𝑣)) → ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) |
134 | | eldifsni 4261 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵}) → 𝑎 ≠ 𝐵) |
135 | 134 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵}) ∧ ((abs‘(𝑎 − 𝐵)) < 𝑧 ∧ (abs‘(𝑎 − 𝐵)) < 𝑣)) → 𝑎 ≠ 𝐵) |
136 | | simprl 790 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵}) ∧ ((abs‘(𝑎 − 𝐵)) < 𝑧 ∧ (abs‘(𝑎 − 𝐵)) < 𝑣)) → (abs‘(𝑎 − 𝐵)) < 𝑧) |
137 | 135, 136 | jca 553 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵}) ∧ ((abs‘(𝑎 − 𝐵)) < 𝑧 ∧ (abs‘(𝑎 − 𝐵)) < 𝑣)) → (𝑎 ≠ 𝐵 ∧ (abs‘(𝑎 − 𝐵)) < 𝑧)) |
138 | 137 | 3adant1 1072 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑧 ∈
ℝ+ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧
∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) ∧ 𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵}) ∧ ((abs‘(𝑎 − 𝐵)) < 𝑧 ∧ (abs‘(𝑎 − 𝐵)) < 𝑣)) → (𝑎 ≠ 𝐵 ∧ (abs‘(𝑎 − 𝐵)) < 𝑧)) |
139 | | neeq1 2844 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑤 = 𝑎 → (𝑤 ≠ 𝐵 ↔ 𝑎 ≠ 𝐵)) |
140 | | oveq1 6556 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑤 = 𝑎 → (𝑤 − 𝐵) = (𝑎 − 𝐵)) |
141 | 140 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑤 = 𝑎 → (abs‘(𝑤 − 𝐵)) = (abs‘(𝑎 − 𝐵))) |
142 | 141 | breq1d 4593 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑤 = 𝑎 → ((abs‘(𝑤 − 𝐵)) < 𝑧 ↔ (abs‘(𝑎 − 𝐵)) < 𝑧)) |
143 | 139, 142 | anbi12d 743 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑤 = 𝑎 → ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) ↔ (𝑎 ≠ 𝐵 ∧ (abs‘(𝑎 − 𝐵)) < 𝑧))) |
144 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑤 = 𝑎 → (𝐹‘𝑤) = (𝐹‘𝑎)) |
145 | 144 | oveq1d 6564 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑤 = 𝑎 → ((𝐹‘𝑤) − 𝑥) = ((𝐹‘𝑎) − 𝑥)) |
146 | 145 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑤 = 𝑎 → (abs‘((𝐹‘𝑤) − 𝑥)) = (abs‘((𝐹‘𝑎) − 𝑥))) |
147 | 146 | breq1d 4593 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑤 = 𝑎 → ((abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦 ↔ (abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦)) |
148 | 143, 147 | imbi12d 333 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑤 = 𝑎 → (((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦) ↔ ((𝑎 ≠ 𝐵 ∧ (abs‘(𝑎 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦))) |
149 | 148 | rspcva 3280 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑎 ∈ 𝐴 ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) → ((𝑎 ≠ 𝐵 ∧ (abs‘(𝑎 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦)) |
150 | 149 | imp 444 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑎 ∈ 𝐴 ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ (𝑎 ≠ 𝐵 ∧ (abs‘(𝑎 − 𝐵)) < 𝑧)) → (abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦) |
151 | 132, 133,
138, 150 | syl21anc 1317 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑧 ∈
ℝ+ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧
∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) ∧ 𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵}) ∧ ((abs‘(𝑎 − 𝐵)) < 𝑧 ∧ (abs‘(𝑎 − 𝐵)) < 𝑣)) → (abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦) |
152 | 94 | 3ad2ant2 1076 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑧 ∈
ℝ+ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧
∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) ∧ 𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵}) ∧ ((abs‘(𝑎 − 𝐵)) < 𝑧 ∧ (abs‘(𝑎 − 𝐵)) < 𝑣)) → 𝑎 ∈ (𝐴 ∩ (-∞(,)𝐵))) |
153 | 61 | 3ad2ant1 1075 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑧 ∈
ℝ+ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧
∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) ∧ 𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵}) ∧ ((abs‘(𝑎 − 𝐵)) < 𝑧 ∧ (abs‘(𝑎 − 𝐵)) < 𝑣)) → 𝜑) |
154 | | simp13 1086 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑧 ∈
ℝ+ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧
∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) ∧ 𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵}) ∧ ((abs‘(𝑎 − 𝐵)) < 𝑧 ∧ (abs‘(𝑎 − 𝐵)) < 𝑣)) → ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) |
155 | | nfv 1830 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
Ⅎ𝑤𝜑 |
156 | | nfra1 2925 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
Ⅎ𝑤∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦) |
157 | 155, 156 | nfan 1816 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
Ⅎ𝑤(𝜑 ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) |
158 | | elinel2 3762 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵)) → 𝑤 ∈ (-∞(,)𝐵)) |
159 | | fvres 6117 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑤 ∈ (-∞(,)𝐵) → ((𝐹 ↾ (-∞(,)𝐵))‘𝑤) = (𝐹‘𝑤)) |
160 | 158, 159 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵)) → ((𝐹 ↾ (-∞(,)𝐵))‘𝑤) = (𝐹‘𝑤)) |
161 | 160 | eqcomd 2616 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵)) → (𝐹‘𝑤) = ((𝐹 ↾ (-∞(,)𝐵))‘𝑤)) |
162 | 161 | oveq1d 6564 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵)) → ((𝐹‘𝑤) − 𝐿) = (((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) |
163 | 162 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵)) → (abs‘((𝐹‘𝑤) − 𝐿)) = (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿))) |
164 | 163 | 3ad2ant2 1076 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝜑 ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) ∧ 𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵)) ∧ (𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣)) → (abs‘((𝐹‘𝑤) − 𝐿)) = (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿))) |
165 | | rspa 2914 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
((∀𝑤 ∈
(𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦) ∧ 𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))) → ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) |
166 | 165 | 3impia 1253 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
((∀𝑤 ∈
(𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦) ∧ 𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵)) ∧ (𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣)) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦) |
167 | 166 | 3adant1l 1310 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝜑 ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) ∧ 𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵)) ∧ (𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣)) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦) |
168 | 164, 167 | eqbrtrd 4605 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝜑 ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) ∧ 𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵)) ∧ (𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣)) → (abs‘((𝐹‘𝑤) − 𝐿)) < 𝑦) |
169 | 168 | 3exp 1256 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) → (𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵)) → ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘((𝐹‘𝑤) − 𝐿)) < 𝑦))) |
170 | 157, 169 | ralrimi 2940 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) → ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘((𝐹‘𝑤) − 𝐿)) < 𝑦)) |
171 | 153, 154,
170 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑧 ∈
ℝ+ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧
∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) ∧ 𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵}) ∧ ((abs‘(𝑎 − 𝐵)) < 𝑧 ∧ (abs‘(𝑎 − 𝐵)) < 𝑣)) → ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘((𝐹‘𝑤) − 𝐿)) < 𝑦)) |
172 | 134 | anim1i 590 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵}) ∧ (abs‘(𝑎 − 𝐵)) < 𝑣) → (𝑎 ≠ 𝐵 ∧ (abs‘(𝑎 − 𝐵)) < 𝑣)) |
173 | 172 | adantrl 748 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵}) ∧ ((abs‘(𝑎 − 𝐵)) < 𝑧 ∧ (abs‘(𝑎 − 𝐵)) < 𝑣)) → (𝑎 ≠ 𝐵 ∧ (abs‘(𝑎 − 𝐵)) < 𝑣)) |
174 | 173 | 3adant1 1072 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑧 ∈
ℝ+ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧
∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) ∧ 𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵}) ∧ ((abs‘(𝑎 − 𝐵)) < 𝑧 ∧ (abs‘(𝑎 − 𝐵)) < 𝑣)) → (𝑎 ≠ 𝐵 ∧ (abs‘(𝑎 − 𝐵)) < 𝑣)) |
175 | 141 | breq1d 4593 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑤 = 𝑎 → ((abs‘(𝑤 − 𝐵)) < 𝑣 ↔ (abs‘(𝑎 − 𝐵)) < 𝑣)) |
176 | 139, 175 | anbi12d 743 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑤 = 𝑎 → ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) ↔ (𝑎 ≠ 𝐵 ∧ (abs‘(𝑎 − 𝐵)) < 𝑣))) |
177 | 144 | oveq1d 6564 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑤 = 𝑎 → ((𝐹‘𝑤) − 𝐿) = ((𝐹‘𝑎) − 𝐿)) |
178 | 177 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑤 = 𝑎 → (abs‘((𝐹‘𝑤) − 𝐿)) = (abs‘((𝐹‘𝑎) − 𝐿))) |
179 | 178 | breq1d 4593 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑤 = 𝑎 → ((abs‘((𝐹‘𝑤) − 𝐿)) < 𝑦 ↔ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) |
180 | 176, 179 | imbi12d 333 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑤 = 𝑎 → (((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘((𝐹‘𝑤) − 𝐿)) < 𝑦) ↔ ((𝑎 ≠ 𝐵 ∧ (abs‘(𝑎 − 𝐵)) < 𝑣) → (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦))) |
181 | 180 | rspcva 3280 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑎 ∈ (𝐴 ∩ (-∞(,)𝐵)) ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘((𝐹‘𝑤) − 𝐿)) < 𝑦)) → ((𝑎 ≠ 𝐵 ∧ (abs‘(𝑎 − 𝐵)) < 𝑣) → (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) |
182 | 181 | imp 444 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑎 ∈ (𝐴 ∩ (-∞(,)𝐵)) ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘((𝐹‘𝑤) − 𝐿)) < 𝑦)) ∧ (𝑎 ≠ 𝐵 ∧ (abs‘(𝑎 − 𝐵)) < 𝑣)) → (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦) |
183 | 152, 171,
174, 182 | syl21anc 1317 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑧 ∈
ℝ+ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧
∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) ∧ 𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵}) ∧ ((abs‘(𝑎 − 𝐵)) < 𝑧 ∧ (abs‘(𝑎 − 𝐵)) < 𝑣)) → (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦) |
184 | | rspe 2986 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑎 ∈ 𝐴 ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) → ∃𝑎 ∈ 𝐴 ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) |
185 | 132, 151,
183, 184 | syl12anc 1316 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑧 ∈
ℝ+ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧
∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) ∧ 𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵}) ∧ ((abs‘(𝑎 − 𝐵)) < 𝑧 ∧ (abs‘(𝑎 − 𝐵)) < 𝑣)) → ∃𝑎 ∈ 𝐴 ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) |
186 | 185 | 3exp 1256 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+
∧ ∀𝑤 ∈
𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧
∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) → (𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵}) → (((abs‘(𝑎 − 𝐵)) < 𝑧 ∧ (abs‘(𝑎 − 𝐵)) < 𝑣) → ∃𝑎 ∈ 𝐴 ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)))) |
187 | 128, 129,
186 | rexlimd 3008 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+
∧ ∀𝑤 ∈
𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧
∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) → (∃𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵})((abs‘(𝑎 − 𝐵)) < 𝑧 ∧ (abs‘(𝑎 − 𝐵)) < 𝑣) → ∃𝑎 ∈ 𝐴 ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦))) |
188 | 127, 187 | mpd 15 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+
∧ ∀𝑤 ∈
𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧
∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) → ∃𝑎 ∈ 𝐴 ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) |
189 | 188 | 3exp 1256 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+
∧ ∀𝑤 ∈
𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) → (𝑣 ∈ ℝ+ →
(∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦) → ∃𝑎 ∈ 𝐴 ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)))) |
190 | 189 | rexlimdv 3012 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+
∧ ∀𝑤 ∈
𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) → (∃𝑣 ∈ ℝ+ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦) → ∃𝑎 ∈ 𝐴 ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦))) |
191 | 60, 190 | mpd 15 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+
∧ ∀𝑤 ∈
𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) → ∃𝑎 ∈ 𝐴 ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) |
192 | 191 | 3exp 1256 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) → (𝑧 ∈ ℝ+
→ (∀𝑤 ∈
𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦) → ∃𝑎 ∈ 𝐴 ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)))) |
193 | 192 | rexlimdv 3012 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) →
(∃𝑧 ∈
ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦) → ∃𝑎 ∈ 𝐴 ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦))) |
194 | 193 | imp 444 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧
∃𝑧 ∈
ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) → ∃𝑎 ∈ 𝐴 ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) |
195 | 194 | adantllr 751 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧
∃𝑧 ∈
ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) → ∃𝑎 ∈ 𝐴 ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) |
196 | | fresin 5986 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝐹:𝐴⟶ℂ → (𝐹 ↾ (𝐵(,)+∞)):(𝐴 ∩ (𝐵(,)+∞))⟶ℂ) |
197 | 36, 196 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → (𝐹 ↾ (𝐵(,)+∞)):(𝐴 ∩ (𝐵(,)+∞))⟶ℂ) |
198 | | inss2 3796 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝐴 ∩ (𝐵(,)+∞)) ⊆ (𝐵(,)+∞) |
199 | | ioosscn 38563 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝐵(,)+∞) ⊆
ℂ |
200 | 198, 199 | sstri 3577 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝐴 ∩ (𝐵(,)+∞)) ⊆
ℂ |
201 | 200 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → (𝐴 ∩ (𝐵(,)+∞)) ⊆
ℂ) |
202 | 197, 201,
55 | ellimc3 23449 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → (𝑅 ∈ ((𝐹 ↾ (𝐵(,)+∞)) limℂ 𝐵) ↔ (𝑅 ∈ ℂ ∧ ∀𝑦 ∈ ℝ+
∃𝑣 ∈
ℝ+ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)))) |
203 | 2, 202 | mpbid 221 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → (𝑅 ∈ ℂ ∧ ∀𝑦 ∈ ℝ+
∃𝑣 ∈
ℝ+ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦))) |
204 | 203 | simprd 478 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → ∀𝑦 ∈ ℝ+ ∃𝑣 ∈ ℝ+
∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) |
205 | 204 | r19.21bi 2916 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) →
∃𝑣 ∈
ℝ+ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) |
206 | 205 | 3ad2ant1 1075 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+
∧ ∀𝑤 ∈
𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) → ∃𝑣 ∈ ℝ+ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) |
207 | | simp11l 1165 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+
∧ ∀𝑤 ∈
𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧
∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) → 𝜑) |
208 | | simp12 1085 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+
∧ ∀𝑤 ∈
𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧
∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) → 𝑧 ∈ ℝ+) |
209 | | simp2 1055 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+
∧ ∀𝑤 ∈
𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧
∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) → 𝑣 ∈ ℝ+) |
210 | | inss1 3795 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
(((limPt‘𝐾)‘(𝐴 ∩ (𝐵(,)+∞))) ∩ ℝ) ⊆
((limPt‘𝐾)‘(𝐴 ∩ (𝐵(,)+∞))) |
211 | 210 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝜑 → (((limPt‘𝐾)‘(𝐴 ∩ (𝐵(,)+∞))) ∩ ℝ) ⊆
((limPt‘𝐾)‘(𝐴 ∩ (𝐵(,)+∞)))) |
212 | | ioossre 12106 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝐵(,)+∞) ⊆
ℝ |
213 | 198, 212 | sstri 3577 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝐴 ∩ (𝐵(,)+∞)) ⊆
ℝ |
214 | 213 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝜑 → (𝐴 ∩ (𝐵(,)+∞)) ⊆
ℝ) |
215 | 76, 78 | restlp 20797 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝐾 ∈ Top ∧ ℝ
⊆ ℂ ∧ (𝐴
∩ (𝐵(,)+∞))
⊆ ℝ) → ((limPt‘𝐽)‘(𝐴 ∩ (𝐵(,)+∞))) = (((limPt‘𝐾)‘(𝐴 ∩ (𝐵(,)+∞))) ∩
ℝ)) |
216 | 70, 72, 214, 215 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝜑 → ((limPt‘𝐽)‘(𝐴 ∩ (𝐵(,)+∞))) = (((limPt‘𝐾)‘(𝐴 ∩ (𝐵(,)+∞))) ∩
ℝ)) |
217 | 82 | fveq1i 6104 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
((limPt‘(TopOpen‘ℂfld))‘(𝐴 ∩ (𝐵(,)+∞))) = ((limPt‘𝐾)‘(𝐴 ∩ (𝐵(,)+∞))) |
218 | 217 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝜑 →
((limPt‘(TopOpen‘ℂfld))‘(𝐴 ∩ (𝐵(,)+∞))) = ((limPt‘𝐾)‘(𝐴 ∩ (𝐵(,)+∞)))) |
219 | 211, 216,
218 | 3sstr4d 3611 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝜑 → ((limPt‘𝐽)‘(𝐴 ∩ (𝐵(,)+∞))) ⊆
((limPt‘(TopOpen‘ℂfld))‘(𝐴 ∩ (𝐵(,)+∞)))) |
220 | | limclner.blp2 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝜑 → 𝐵 ∈ ((limPt‘𝐽)‘(𝐴 ∩ (𝐵(,)+∞)))) |
221 | 219, 220 | sseldd 3569 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝜑 → 𝐵 ∈
((limPt‘(TopOpen‘ℂfld))‘(𝐴 ∩ (𝐵(,)+∞)))) |
222 | 201, 55 | islpcn 38706 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝜑 → (𝐵 ∈
((limPt‘(TopOpen‘ℂfld))‘(𝐴 ∩ (𝐵(,)+∞))) ↔ ∀𝑢 ∈ ℝ+
∃𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵})(abs‘(𝑏 − 𝐵)) < 𝑢)) |
223 | 221, 222 | mpbid 221 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝜑 → ∀𝑢 ∈ ℝ+ ∃𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵})(abs‘(𝑏 − 𝐵)) < 𝑢) |
224 | 223 | 3ad2ant1 1075 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+)
→ ∀𝑢 ∈
ℝ+ ∃𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵})(abs‘(𝑏 − 𝐵)) < 𝑢) |
225 | | breq2 4587 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑢 = if(𝑧 ≤ 𝑣, 𝑧, 𝑣) → ((abs‘(𝑏 − 𝐵)) < 𝑢 ↔ (abs‘(𝑏 − 𝐵)) < if(𝑧 ≤ 𝑣, 𝑧, 𝑣))) |
226 | 225 | rexbidv 3034 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑢 = if(𝑧 ≤ 𝑣, 𝑧, 𝑣) → (∃𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵})(abs‘(𝑏 − 𝐵)) < 𝑢 ↔ ∃𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵})(abs‘(𝑏 − 𝐵)) < if(𝑧 ≤ 𝑣, 𝑧, 𝑣))) |
227 | 226 | rspcva 3280 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
((if(𝑧 ≤ 𝑣, 𝑧, 𝑣) ∈ ℝ+ ∧
∀𝑢 ∈
ℝ+ ∃𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵})(abs‘(𝑏 − 𝐵)) < 𝑢) → ∃𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵})(abs‘(𝑏 − 𝐵)) < if(𝑧 ≤ 𝑣, 𝑧, 𝑣)) |
228 | 65, 224, 227 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+)
→ ∃𝑏 ∈
((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵})(abs‘(𝑏 − 𝐵)) < if(𝑧 ≤ 𝑣, 𝑧, 𝑣)) |
229 | | eldifi 3694 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵}) → 𝑏 ∈ (𝐴 ∩ (𝐵(,)+∞))) |
230 | 213, 229 | sseldi 3566 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵}) → 𝑏 ∈ ℝ) |
231 | 72 | sselda 3568 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ ((𝜑 ∧ 𝑏 ∈ ℝ) → 𝑏 ∈ ℂ) |
232 | 55 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ ((𝜑 ∧ 𝑏 ∈ ℝ) → 𝐵 ∈ ℂ) |
233 | 231, 232 | subcld 10271 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝜑 ∧ 𝑏 ∈ ℝ) → (𝑏 − 𝐵) ∈ ℂ) |
234 | 233 | abscld 14023 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝜑 ∧ 𝑏 ∈ ℝ) → (abs‘(𝑏 − 𝐵)) ∈ ℝ) |
235 | 234 | 3ad2antl1 1216 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (((𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+)
∧ 𝑏 ∈ ℝ)
→ (abs‘(𝑏
− 𝐵)) ∈
ℝ) |
236 | 235 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((((𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+)
∧ 𝑏 ∈ ℝ)
∧ (abs‘(𝑏 −
𝐵)) < if(𝑧 ≤ 𝑣, 𝑧, 𝑣)) → (abs‘(𝑏 − 𝐵)) ∈ ℝ) |
237 | 102 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((((𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+)
∧ 𝑏 ∈ ℝ)
∧ (abs‘(𝑏 −
𝐵)) < if(𝑧 ≤ 𝑣, 𝑧, 𝑣)) → if(𝑧 ≤ 𝑣, 𝑧, 𝑣) ∈ ℝ) |
238 | 105 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((((𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+)
∧ 𝑏 ∈ ℝ)
∧ (abs‘(𝑏 −
𝐵)) < if(𝑧 ≤ 𝑣, 𝑧, 𝑣)) → 𝑧 ∈ ℝ) |
239 | | simpr 476 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((((𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+)
∧ 𝑏 ∈ ℝ)
∧ (abs‘(𝑏 −
𝐵)) < if(𝑧 ≤ 𝑣, 𝑧, 𝑣)) → (abs‘(𝑏 − 𝐵)) < if(𝑧 ≤ 𝑣, 𝑧, 𝑣)) |
240 | 111 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((((𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+)
∧ 𝑏 ∈ ℝ)
∧ (abs‘(𝑏 −
𝐵)) < if(𝑧 ≤ 𝑣, 𝑧, 𝑣)) → if(𝑧 ≤ 𝑣, 𝑧, 𝑣) ≤ 𝑧) |
241 | 236, 237,
238, 239, 240 | ltletrd 10076 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((((𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+)
∧ 𝑏 ∈ ℝ)
∧ (abs‘(𝑏 −
𝐵)) < if(𝑧 ≤ 𝑣, 𝑧, 𝑣)) → (abs‘(𝑏 − 𝐵)) < 𝑧) |
242 | 115 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((((𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+)
∧ 𝑏 ∈ ℝ)
∧ (abs‘(𝑏 −
𝐵)) < if(𝑧 ≤ 𝑣, 𝑧, 𝑣)) → 𝑣 ∈ ℝ) |
243 | 238, 242,
117 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((((𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+)
∧ 𝑏 ∈ ℝ)
∧ (abs‘(𝑏 −
𝐵)) < if(𝑧 ≤ 𝑣, 𝑧, 𝑣)) → if(𝑧 ≤ 𝑣, 𝑧, 𝑣) ≤ 𝑣) |
244 | 236, 237,
242, 239, 243 | ltletrd 10076 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((((𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+)
∧ 𝑏 ∈ ℝ)
∧ (abs‘(𝑏 −
𝐵)) < if(𝑧 ≤ 𝑣, 𝑧, 𝑣)) → (abs‘(𝑏 − 𝐵)) < 𝑣) |
245 | 241, 244 | jca 553 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((((𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+)
∧ 𝑏 ∈ ℝ)
∧ (abs‘(𝑏 −
𝐵)) < if(𝑧 ≤ 𝑣, 𝑧, 𝑣)) → ((abs‘(𝑏 − 𝐵)) < 𝑧 ∧ (abs‘(𝑏 − 𝐵)) < 𝑣)) |
246 | 245 | ex 449 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+)
∧ 𝑏 ∈ ℝ)
→ ((abs‘(𝑏
− 𝐵)) < if(𝑧 ≤ 𝑣, 𝑧, 𝑣) → ((abs‘(𝑏 − 𝐵)) < 𝑧 ∧ (abs‘(𝑏 − 𝐵)) < 𝑣))) |
247 | 230, 246 | sylan2 490 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+)
∧ 𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵})) → ((abs‘(𝑏 − 𝐵)) < if(𝑧 ≤ 𝑣, 𝑧, 𝑣) → ((abs‘(𝑏 − 𝐵)) < 𝑧 ∧ (abs‘(𝑏 − 𝐵)) < 𝑣))) |
248 | 247 | reximdva 3000 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+)
→ (∃𝑏 ∈
((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵})(abs‘(𝑏 − 𝐵)) < if(𝑧 ≤ 𝑣, 𝑧, 𝑣) → ∃𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵})((abs‘(𝑏 − 𝐵)) < 𝑧 ∧ (abs‘(𝑏 − 𝐵)) < 𝑣))) |
249 | 228, 248 | mpd 15 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+)
→ ∃𝑏 ∈
((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵})((abs‘(𝑏 − 𝐵)) < 𝑧 ∧ (abs‘(𝑏 − 𝐵)) < 𝑣)) |
250 | 207, 208,
209, 249 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+
∧ ∀𝑤 ∈
𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧
∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) → ∃𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵})((abs‘(𝑏 − 𝐵)) < 𝑧 ∧ (abs‘(𝑏 − 𝐵)) < 𝑣)) |
251 | | nfv 1830 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
Ⅎ𝑏(((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+
∧ ∀𝑤 ∈
𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧
∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) |
252 | | nfre1 2988 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
Ⅎ𝑏∃𝑏 ∈ 𝐴 ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦) |
253 | | inss1 3795 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝐴 ∩ (𝐵(,)+∞)) ⊆ 𝐴 |
254 | 253, 229 | sseldi 3566 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵}) → 𝑏 ∈ 𝐴) |
255 | 254 | 3ad2ant2 1076 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑧 ∈
ℝ+ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧
∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) ∧ 𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵}) ∧ ((abs‘(𝑏 − 𝐵)) < 𝑧 ∧ (abs‘(𝑏 − 𝐵)) < 𝑣)) → 𝑏 ∈ 𝐴) |
256 | | simp113 1185 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑧 ∈
ℝ+ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧
∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) ∧ 𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵}) ∧ ((abs‘(𝑏 − 𝐵)) < 𝑧 ∧ (abs‘(𝑏 − 𝐵)) < 𝑣)) → ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) |
257 | | eldifsni 4261 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵}) → 𝑏 ≠ 𝐵) |
258 | 257 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵}) ∧ ((abs‘(𝑏 − 𝐵)) < 𝑧 ∧ (abs‘(𝑏 − 𝐵)) < 𝑣)) → 𝑏 ≠ 𝐵) |
259 | | simprl 790 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵}) ∧ ((abs‘(𝑏 − 𝐵)) < 𝑧 ∧ (abs‘(𝑏 − 𝐵)) < 𝑣)) → (abs‘(𝑏 − 𝐵)) < 𝑧) |
260 | 258, 259 | jca 553 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵}) ∧ ((abs‘(𝑏 − 𝐵)) < 𝑧 ∧ (abs‘(𝑏 − 𝐵)) < 𝑣)) → (𝑏 ≠ 𝐵 ∧ (abs‘(𝑏 − 𝐵)) < 𝑧)) |
261 | 260 | 3adant1 1072 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑧 ∈
ℝ+ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧
∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) ∧ 𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵}) ∧ ((abs‘(𝑏 − 𝐵)) < 𝑧 ∧ (abs‘(𝑏 − 𝐵)) < 𝑣)) → (𝑏 ≠ 𝐵 ∧ (abs‘(𝑏 − 𝐵)) < 𝑧)) |
262 | | neeq1 2844 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑤 = 𝑏 → (𝑤 ≠ 𝐵 ↔ 𝑏 ≠ 𝐵)) |
263 | | oveq1 6556 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑤 = 𝑏 → (𝑤 − 𝐵) = (𝑏 − 𝐵)) |
264 | 263 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑤 = 𝑏 → (abs‘(𝑤 − 𝐵)) = (abs‘(𝑏 − 𝐵))) |
265 | 264 | breq1d 4593 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑤 = 𝑏 → ((abs‘(𝑤 − 𝐵)) < 𝑧 ↔ (abs‘(𝑏 − 𝐵)) < 𝑧)) |
266 | 262, 265 | anbi12d 743 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑤 = 𝑏 → ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) ↔ (𝑏 ≠ 𝐵 ∧ (abs‘(𝑏 − 𝐵)) < 𝑧))) |
267 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑤 = 𝑏 → (𝐹‘𝑤) = (𝐹‘𝑏)) |
268 | 267 | oveq1d 6564 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑤 = 𝑏 → ((𝐹‘𝑤) − 𝑥) = ((𝐹‘𝑏) − 𝑥)) |
269 | 268 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑤 = 𝑏 → (abs‘((𝐹‘𝑤) − 𝑥)) = (abs‘((𝐹‘𝑏) − 𝑥))) |
270 | 269 | breq1d 4593 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑤 = 𝑏 → ((abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦 ↔ (abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦)) |
271 | 266, 270 | imbi12d 333 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑤 = 𝑏 → (((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦) ↔ ((𝑏 ≠ 𝐵 ∧ (abs‘(𝑏 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦))) |
272 | 271 | rspcva 3280 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑏 ∈ 𝐴 ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) → ((𝑏 ≠ 𝐵 ∧ (abs‘(𝑏 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦)) |
273 | 272 | imp 444 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝑏 ∈ 𝐴 ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ (𝑏 ≠ 𝐵 ∧ (abs‘(𝑏 − 𝐵)) < 𝑧)) → (abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦) |
274 | 255, 256,
261, 273 | syl21anc 1317 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑧 ∈
ℝ+ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧
∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) ∧ 𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵}) ∧ ((abs‘(𝑏 − 𝐵)) < 𝑧 ∧ (abs‘(𝑏 − 𝐵)) < 𝑣)) → (abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦) |
275 | 229 | 3ad2ant2 1076 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑧 ∈
ℝ+ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧
∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) ∧ 𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵}) ∧ ((abs‘(𝑏 − 𝐵)) < 𝑧 ∧ (abs‘(𝑏 − 𝐵)) < 𝑣)) → 𝑏 ∈ (𝐴 ∩ (𝐵(,)+∞))) |
276 | 207 | 3ad2ant1 1075 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
(((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑧 ∈
ℝ+ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧
∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) ∧ 𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵}) ∧ ((abs‘(𝑏 − 𝐵)) < 𝑧 ∧ (abs‘(𝑏 − 𝐵)) < 𝑣)) → 𝜑) |
277 | | simp13 1086 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
(((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑧 ∈
ℝ+ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧
∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) ∧ 𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵}) ∧ ((abs‘(𝑏 − 𝐵)) < 𝑧 ∧ (abs‘(𝑏 − 𝐵)) < 𝑣)) → ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) |
278 | | nfra1 2925 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
Ⅎ𝑤∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦) |
279 | 155, 278 | nfan 1816 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
Ⅎ𝑤(𝜑 ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) |
280 | | elinel2 3762 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞)) → 𝑤 ∈ (𝐵(,)+∞)) |
281 | | fvres 6117 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (𝑤 ∈ (𝐵(,)+∞) → ((𝐹 ↾ (𝐵(,)+∞))‘𝑤) = (𝐹‘𝑤)) |
282 | 280, 281 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞)) → ((𝐹 ↾ (𝐵(,)+∞))‘𝑤) = (𝐹‘𝑤)) |
283 | 282 | eqcomd 2616 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞)) → (𝐹‘𝑤) = ((𝐹 ↾ (𝐵(,)+∞))‘𝑤)) |
284 | 283 | oveq1d 6564 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞)) → ((𝐹‘𝑤) − 𝑅) = (((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) |
285 | 284 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞)) → (abs‘((𝐹‘𝑤) − 𝑅)) = (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅))) |
286 | 285 | 3ad2ant2 1076 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (((𝜑 ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) ∧ 𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞)) ∧ (𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣)) → (abs‘((𝐹‘𝑤) − 𝑅)) = (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅))) |
287 | | rspa 2914 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢
((∀𝑤 ∈
(𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦) ∧ 𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))) → ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) |
288 | 287 | 3impia 1253 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢
((∀𝑤 ∈
(𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦) ∧ 𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞)) ∧ (𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣)) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦) |
289 | 288 | 3adant1l 1310 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (((𝜑 ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) ∧ 𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞)) ∧ (𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣)) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦) |
290 | 286, 289 | eqbrtrd 4605 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (((𝜑 ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) ∧ 𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞)) ∧ (𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣)) → (abs‘((𝐹‘𝑤) − 𝑅)) < 𝑦) |
291 | 290 | 3exp 1256 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝜑 ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) → (𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞)) → ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘((𝐹‘𝑤) − 𝑅)) < 𝑦))) |
292 | 279, 291 | ralrimi 2940 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝜑 ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) → ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘((𝐹‘𝑤) − 𝑅)) < 𝑦)) |
293 | 276, 277,
292 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑧 ∈
ℝ+ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧
∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) ∧ 𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵}) ∧ ((abs‘(𝑏 − 𝐵)) < 𝑧 ∧ (abs‘(𝑏 − 𝐵)) < 𝑣)) → ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘((𝐹‘𝑤) − 𝑅)) < 𝑦)) |
294 | 257 | anim1i 590 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵}) ∧ (abs‘(𝑏 − 𝐵)) < 𝑣) → (𝑏 ≠ 𝐵 ∧ (abs‘(𝑏 − 𝐵)) < 𝑣)) |
295 | 294 | adantrl 748 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵}) ∧ ((abs‘(𝑏 − 𝐵)) < 𝑧 ∧ (abs‘(𝑏 − 𝐵)) < 𝑣)) → (𝑏 ≠ 𝐵 ∧ (abs‘(𝑏 − 𝐵)) < 𝑣)) |
296 | 295 | 3adant1 1072 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑧 ∈
ℝ+ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧
∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) ∧ 𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵}) ∧ ((abs‘(𝑏 − 𝐵)) < 𝑧 ∧ (abs‘(𝑏 − 𝐵)) < 𝑣)) → (𝑏 ≠ 𝐵 ∧ (abs‘(𝑏 − 𝐵)) < 𝑣)) |
297 | 264 | breq1d 4593 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑤 = 𝑏 → ((abs‘(𝑤 − 𝐵)) < 𝑣 ↔ (abs‘(𝑏 − 𝐵)) < 𝑣)) |
298 | 262, 297 | anbi12d 743 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑤 = 𝑏 → ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) ↔ (𝑏 ≠ 𝐵 ∧ (abs‘(𝑏 − 𝐵)) < 𝑣))) |
299 | 267 | oveq1d 6564 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑤 = 𝑏 → ((𝐹‘𝑤) − 𝑅) = ((𝐹‘𝑏) − 𝑅)) |
300 | 299 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑤 = 𝑏 → (abs‘((𝐹‘𝑤) − 𝑅)) = (abs‘((𝐹‘𝑏) − 𝑅))) |
301 | 300 | breq1d 4593 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑤 = 𝑏 → ((abs‘((𝐹‘𝑤) − 𝑅)) < 𝑦 ↔ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)) |
302 | 298, 301 | imbi12d 333 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑤 = 𝑏 → (((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘((𝐹‘𝑤) − 𝑅)) < 𝑦) ↔ ((𝑏 ≠ 𝐵 ∧ (abs‘(𝑏 − 𝐵)) < 𝑣) → (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦))) |
303 | 302 | rspcva 3280 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑏 ∈ (𝐴 ∩ (𝐵(,)+∞)) ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘((𝐹‘𝑤) − 𝑅)) < 𝑦)) → ((𝑏 ≠ 𝐵 ∧ (abs‘(𝑏 − 𝐵)) < 𝑣) → (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)) |
304 | 303 | imp 444 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝑏 ∈ (𝐴 ∩ (𝐵(,)+∞)) ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘((𝐹‘𝑤) − 𝑅)) < 𝑦)) ∧ (𝑏 ≠ 𝐵 ∧ (abs‘(𝑏 − 𝐵)) < 𝑣)) → (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦) |
305 | 275, 293,
296, 304 | syl21anc 1317 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑧 ∈
ℝ+ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧
∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) ∧ 𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵}) ∧ ((abs‘(𝑏 − 𝐵)) < 𝑧 ∧ (abs‘(𝑏 − 𝐵)) < 𝑣)) → (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦) |
306 | | rspe 2986 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑏 ∈ 𝐴 ∧ ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)) → ∃𝑏 ∈ 𝐴 ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)) |
307 | 255, 274,
305, 306 | syl12anc 1316 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑧 ∈
ℝ+ ∧ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧
∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) ∧ 𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵}) ∧ ((abs‘(𝑏 − 𝐵)) < 𝑧 ∧ (abs‘(𝑏 − 𝐵)) < 𝑣)) → ∃𝑏 ∈ 𝐴 ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)) |
308 | 307 | 3exp 1256 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+
∧ ∀𝑤 ∈
𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧
∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) → (𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵}) → (((abs‘(𝑏 − 𝐵)) < 𝑧 ∧ (abs‘(𝑏 − 𝐵)) < 𝑣) → ∃𝑏 ∈ 𝐴 ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)))) |
309 | 251, 252,
308 | rexlimd 3008 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+
∧ ∀𝑤 ∈
𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧
∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) → (∃𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵})((abs‘(𝑏 − 𝐵)) < 𝑧 ∧ (abs‘(𝑏 − 𝐵)) < 𝑣) → ∃𝑏 ∈ 𝐴 ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦))) |
310 | 250, 309 | mpd 15 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+
∧ ∀𝑤 ∈
𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧
∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) → ∃𝑏 ∈ 𝐴 ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)) |
311 | 310 | 3exp 1256 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+
∧ ∀𝑤 ∈
𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) → (𝑣 ∈ ℝ+ →
(∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦) → ∃𝑏 ∈ 𝐴 ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)))) |
312 | 311 | rexlimdv 3012 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+
∧ ∀𝑤 ∈
𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) → (∃𝑣 ∈ ℝ+ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦) → ∃𝑏 ∈ 𝐴 ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦))) |
313 | 206, 312 | mpd 15 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+
∧ ∀𝑤 ∈
𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) → ∃𝑏 ∈ 𝐴 ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)) |
314 | 313 | 3exp 1256 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) → (𝑧 ∈ ℝ+
→ (∀𝑤 ∈
𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦) → ∃𝑏 ∈ 𝐴 ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)))) |
315 | 314 | rexlimdv 3012 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) →
(∃𝑧 ∈
ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦) → ∃𝑏 ∈ 𝐴 ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦))) |
316 | 315 | imp 444 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧
∃𝑧 ∈
ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) → ∃𝑏 ∈ 𝐴 ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)) |
317 | 316 | adantllr 751 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧
∃𝑧 ∈
ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) → ∃𝑏 ∈ 𝐴 ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)) |
318 | 317 | ad2antrr 758 |
. . . . . . . . . . . . . . 15
⊢
((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+)
∧ ∃𝑧 ∈
ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) → ∃𝑏 ∈ 𝐴 ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)) |
319 | 3 | ad6antr 768 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+)
∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)) → 𝑅 ∈ ℂ) |
320 | 7 | ad6antr 768 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+)
∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)) → 𝐿 ∈ ℂ) |
321 | 319, 320 | subcld 10271 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+)
∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)) → (𝑅 − 𝐿) ∈ ℂ) |
322 | 321 | abscld 14023 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+)
∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)) → (abs‘(𝑅 − 𝐿)) ∈ ℝ) |
323 | | simp-6l 806 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+)
∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)) → 𝜑) |
324 | | simplr 788 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+)
∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)) → 𝑏 ∈ 𝐴) |
325 | 36 | ffvelrnda 6267 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐴) → (𝐹‘𝑏) ∈ ℂ) |
326 | 323, 324,
325 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+)
∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)) → (𝐹‘𝑏) ∈ ℂ) |
327 | 319, 326 | subcld 10271 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+)
∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)) → (𝑅 − (𝐹‘𝑏)) ∈ ℂ) |
328 | 327 | abscld 14023 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+)
∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)) → (abs‘(𝑅 − (𝐹‘𝑏))) ∈ ℝ) |
329 | | simp-6r 807 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+)
∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)) → 𝑥 ∈ ℂ) |
330 | 326, 329 | subcld 10271 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+)
∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)) → ((𝐹‘𝑏) − 𝑥) ∈ ℂ) |
331 | 330 | abscld 14023 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+)
∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)) → (abs‘((𝐹‘𝑏) − 𝑥)) ∈ ℝ) |
332 | 328, 331 | readdcld 9948 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+)
∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)) → ((abs‘(𝑅 − (𝐹‘𝑏))) + (abs‘((𝐹‘𝑏) − 𝑥))) ∈ ℝ) |
333 | | simp-4r 803 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+)
∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)) → 𝑎 ∈ 𝐴) |
334 | 36 | ffvelrnda 6267 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → (𝐹‘𝑎) ∈ ℂ) |
335 | 323, 333,
334 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+)
∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)) → (𝐹‘𝑎) ∈ ℂ) |
336 | 329, 335 | subcld 10271 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+)
∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)) → (𝑥 − (𝐹‘𝑎)) ∈ ℂ) |
337 | 336 | abscld 14023 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+)
∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)) → (abs‘(𝑥 − (𝐹‘𝑎))) ∈ ℝ) |
338 | 332, 337 | readdcld 9948 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+)
∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)) → (((abs‘(𝑅 − (𝐹‘𝑏))) + (abs‘((𝐹‘𝑏) − 𝑥))) + (abs‘(𝑥 − (𝐹‘𝑎)))) ∈ ℝ) |
339 | 335, 320 | subcld 10271 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+)
∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)) → ((𝐹‘𝑎) − 𝐿) ∈ ℂ) |
340 | 339 | abscld 14023 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+)
∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)) → (abs‘((𝐹‘𝑎) − 𝐿)) ∈ ℝ) |
341 | 338, 340 | readdcld 9948 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+)
∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)) → ((((abs‘(𝑅 − (𝐹‘𝑏))) + (abs‘((𝐹‘𝑏) − 𝑥))) + (abs‘(𝑥 − (𝐹‘𝑎)))) + (abs‘((𝐹‘𝑎) − 𝐿))) ∈ ℝ) |
342 | 15 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+)
∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)) → 4 ∈ ℝ) |
343 | | rpre 11715 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑦 ∈ ℝ+
→ 𝑦 ∈
ℝ) |
344 | 343 | ad5antlr 767 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+)
∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)) → 𝑦 ∈ ℝ) |
345 | 342, 344 | remulcld 9949 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+)
∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)) → (4 · 𝑦) ∈ ℝ) |
346 | 319, 326,
329, 335, 320 | absnpncan3d 38462 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+)
∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)) → (abs‘(𝑅 − 𝐿)) ≤ ((((abs‘(𝑅 − (𝐹‘𝑏))) + (abs‘((𝐹‘𝑏) − 𝑥))) + (abs‘(𝑥 − (𝐹‘𝑎)))) + (abs‘((𝐹‘𝑎) − 𝐿)))) |
347 | 319, 326 | abssubd 14040 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+)
∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)) → (abs‘(𝑅 − (𝐹‘𝑏))) = (abs‘((𝐹‘𝑏) − 𝑅))) |
348 | | simprr 792 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+)
∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)) → (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦) |
349 | 347, 348 | eqbrtrd 4605 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+)
∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)) → (abs‘(𝑅 − (𝐹‘𝑏))) < 𝑦) |
350 | | simprl 790 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+)
∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)) → (abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦) |
351 | | simp-5r 805 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+)
∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) → 𝑥 ∈ ℂ) |
352 | | simp-4l 802 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+)
∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) → 𝜑) |
353 | | simplr 788 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+)
∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) → 𝑎 ∈ 𝐴) |
354 | 352, 353,
334 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+)
∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) → (𝐹‘𝑎) ∈ ℂ) |
355 | 354 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+)
∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) → (𝐹‘𝑎) ∈ ℂ) |
356 | 351, 355 | abssubd 14040 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+)
∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) → (abs‘(𝑥 − (𝐹‘𝑎))) = (abs‘((𝐹‘𝑎) − 𝑥))) |
357 | | simplrl 796 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+)
∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) → (abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦) |
358 | 356, 357 | eqbrtrd 4605 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+)
∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) → (abs‘(𝑥 − (𝐹‘𝑎))) < 𝑦) |
359 | 358 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+)
∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)) → (abs‘(𝑥 − (𝐹‘𝑎))) < 𝑦) |
360 | | simplrr 797 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+)
∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) → (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦) |
361 | 360 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+)
∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)) → (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦) |
362 | 328, 331,
337, 340, 344, 349, 350, 359, 361 | lt4addmuld 38461 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+)
∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)) → ((((abs‘(𝑅 − (𝐹‘𝑏))) + (abs‘((𝐹‘𝑏) − 𝑥))) + (abs‘(𝑥 − (𝐹‘𝑎)))) + (abs‘((𝐹‘𝑎) − 𝐿))) < (4 · 𝑦)) |
363 | 322, 341,
345, 346, 362 | lelttrd 10074 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+)
∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦)) → (abs‘(𝑅 − 𝐿)) < (4 · 𝑦)) |
364 | 363 | ex 449 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+)
∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) → (((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦) → (abs‘(𝑅 − 𝐿)) < (4 · 𝑦))) |
365 | 364 | adantlllr 38222 |
. . . . . . . . . . . . . . . 16
⊢
(((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+)
∧ ∃𝑧 ∈
ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) → (((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦) → (abs‘(𝑅 − 𝐿)) < (4 · 𝑦))) |
366 | 365 | reximdva 3000 |
. . . . . . . . . . . . . . 15
⊢
((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+)
∧ ∃𝑧 ∈
ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) → (∃𝑏 ∈ 𝐴 ((abs‘((𝐹‘𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑏) − 𝑅)) < 𝑦) → ∃𝑏 ∈ 𝐴 (abs‘(𝑅 − 𝐿)) < (4 · 𝑦))) |
367 | 318, 366 | mpd 15 |
. . . . . . . . . . . . . 14
⊢
((((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+)
∧ ∃𝑧 ∈
ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑎 ∈ 𝐴) ∧ ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦)) → ∃𝑏 ∈ 𝐴 (abs‘(𝑅 − 𝐿)) < (4 · 𝑦)) |
368 | 367 | ex 449 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+)
∧ ∃𝑧 ∈
ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑎 ∈ 𝐴) → (((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦) → ∃𝑏 ∈ 𝐴 (abs‘(𝑅 − 𝐿)) < (4 · 𝑦))) |
369 | 368 | reximdva 3000 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧
∃𝑧 ∈
ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) → (∃𝑎 ∈ 𝐴 ((abs‘((𝐹‘𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹‘𝑎) − 𝐿)) < 𝑦) → ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐴 (abs‘(𝑅 − 𝐿)) < (4 · 𝑦))) |
370 | 195, 369 | mpd 15 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧
∃𝑧 ∈
ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) → ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐴 (abs‘(𝑅 − 𝐿)) < (4 · 𝑦)) |
371 | 32, 33, 35, 370 | syl21anc 1317 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+
∃𝑧 ∈
ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ∧ 𝑦 ∈ ℝ+) →
∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐴 (abs‘(𝑅 − 𝐿)) < (4 · 𝑦)) |
372 | 371 | ex 449 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+
∃𝑧 ∈
ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) → (𝑦 ∈ ℝ+ →
∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐴 (abs‘(𝑅 − 𝐿)) < (4 · 𝑦))) |
373 | 24, 25, 31, 372 | vtoclf 3231 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+
∃𝑧 ∈
ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) → (((abs‘(𝑅 − 𝐿)) / 4) ∈ ℝ+ →
∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐴 (abs‘(𝑅 − 𝐿)) < (4 · ((abs‘(𝑅 − 𝐿)) / 4)))) |
374 | 19, 373 | mpd 15 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+
∃𝑧 ∈
ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) → ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐴 (abs‘(𝑅 − 𝐿)) < (4 · ((abs‘(𝑅 − 𝐿)) / 4))) |
375 | | simpr 476 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (abs‘(𝑅 − 𝐿)) < (4 · ((abs‘(𝑅 − 𝐿)) / 4))) → (abs‘(𝑅 − 𝐿)) < (4 · ((abs‘(𝑅 − 𝐿)) / 4))) |
376 | | abssubrp 38428 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑅 ∈ ℂ ∧ 𝐿 ∈ ℂ ∧ 𝑅 ≠ 𝐿) → (abs‘(𝑅 − 𝐿)) ∈
ℝ+) |
377 | 3, 7, 11, 376 | syl3anc 1318 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (abs‘(𝑅 − 𝐿)) ∈
ℝ+) |
378 | 377 | rpcnd 11750 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (abs‘(𝑅 − 𝐿)) ∈ ℂ) |
379 | 378 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (abs‘(𝑅 − 𝐿)) < (4 · ((abs‘(𝑅 − 𝐿)) / 4))) → (abs‘(𝑅 − 𝐿)) ∈ ℂ) |
380 | | 4cn 10975 |
. . . . . . . . . . . . . 14
⊢ 4 ∈
ℂ |
381 | 380 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (abs‘(𝑅 − 𝐿)) < (4 · ((abs‘(𝑅 − 𝐿)) / 4))) → 4 ∈
ℂ) |
382 | | 4ne0 10994 |
. . . . . . . . . . . . . 14
⊢ 4 ≠
0 |
383 | 382 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (abs‘(𝑅 − 𝐿)) < (4 · ((abs‘(𝑅 − 𝐿)) / 4))) → 4 ≠ 0) |
384 | 379, 381,
383 | divcan2d 10682 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (abs‘(𝑅 − 𝐿)) < (4 · ((abs‘(𝑅 − 𝐿)) / 4))) → (4 ·
((abs‘(𝑅 −
𝐿)) / 4)) =
(abs‘(𝑅 − 𝐿))) |
385 | 375, 384 | breqtrd 4609 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (abs‘(𝑅 − 𝐿)) < (4 · ((abs‘(𝑅 − 𝐿)) / 4))) → (abs‘(𝑅 − 𝐿)) < (abs‘(𝑅 − 𝐿))) |
386 | 385 | ex 449 |
. . . . . . . . . 10
⊢ (𝜑 → ((abs‘(𝑅 − 𝐿)) < (4 · ((abs‘(𝑅 − 𝐿)) / 4)) → (abs‘(𝑅 − 𝐿)) < (abs‘(𝑅 − 𝐿)))) |
387 | 386 | a1d 25 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) → ((abs‘(𝑅 − 𝐿)) < (4 · ((abs‘(𝑅 − 𝐿)) / 4)) → (abs‘(𝑅 − 𝐿)) < (abs‘(𝑅 − 𝐿))))) |
388 | 387 | ad2antrr 758 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+
∃𝑧 ∈
ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) → ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) → ((abs‘(𝑅 − 𝐿)) < (4 · ((abs‘(𝑅 − 𝐿)) / 4)) → (abs‘(𝑅 − 𝐿)) < (abs‘(𝑅 − 𝐿))))) |
389 | 388 | rexlimdvv 3019 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+
∃𝑧 ∈
ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) → (∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐴 (abs‘(𝑅 − 𝐿)) < (4 · ((abs‘(𝑅 − 𝐿)) / 4)) → (abs‘(𝑅 − 𝐿)) < (abs‘(𝑅 − 𝐿)))) |
390 | 374, 389 | mpd 15 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+
∃𝑧 ∈
ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) → (abs‘(𝑅 − 𝐿)) < (abs‘(𝑅 − 𝐿))) |
391 | 9 | abscld 14023 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+
∃𝑧 ∈
ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) → (abs‘(𝑅 − 𝐿)) ∈ ℝ) |
392 | 391 | ltnrd 10050 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+
∃𝑧 ∈
ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) → ¬ (abs‘(𝑅 − 𝐿)) < (abs‘(𝑅 − 𝐿))) |
393 | 390, 392 | pm2.65da 598 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → ¬ ∀𝑦 ∈ ℝ+
∃𝑧 ∈
ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) |
394 | 393 | ex 449 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ ℂ → ¬ ∀𝑦 ∈ ℝ+
∃𝑧 ∈
ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦))) |
395 | | imnan 437 |
. . . 4
⊢ ((𝑥 ∈ ℂ → ¬
∀𝑦 ∈
ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)) ↔ ¬ (𝑥 ∈ ℂ ∧ ∀𝑦 ∈ ℝ+
∃𝑧 ∈
ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦))) |
396 | 394, 395 | sylib 207 |
. . 3
⊢ (𝜑 → ¬ (𝑥 ∈ ℂ ∧ ∀𝑦 ∈ ℝ+
∃𝑧 ∈
ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦))) |
397 | | limclner.a |
. . . . 5
⊢ (𝜑 → 𝐴 ⊆ ℝ) |
398 | 397, 72 | sstrd 3578 |
. . . 4
⊢ (𝜑 → 𝐴 ⊆ ℂ) |
399 | 36, 398, 55 | ellimc3 23449 |
. . 3
⊢ (𝜑 → (𝑥 ∈ (𝐹 limℂ 𝐵) ↔ (𝑥 ∈ ℂ ∧ ∀𝑦 ∈ ℝ+
∃𝑧 ∈
ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤 ≠ 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑧) → (abs‘((𝐹‘𝑤) − 𝑥)) < 𝑦)))) |
400 | 396, 399 | mtbird 314 |
. 2
⊢ (𝜑 → ¬ 𝑥 ∈ (𝐹 limℂ 𝐵)) |
401 | 400 | eq0rdv 3931 |
1
⊢ (𝜑 → (𝐹 limℂ 𝐵) = ∅) |