Step | Hyp | Ref
| Expression |
1 | | breq2 3993 |
. . . . . . . . . 10
⊢ (𝑒 = ((abs‘(𝑥 − 𝑦)) / 2) → ((abs‘((𝐹‘𝑧) − 𝑥)) < 𝑒 ↔ (abs‘((𝐹‘𝑧) − 𝑥)) < ((abs‘(𝑥 − 𝑦)) / 2))) |
2 | 1 | imbi2d 229 |
. . . . . . . . 9
⊢ (𝑒 = ((abs‘(𝑥 − 𝑦)) / 2) → (((𝑧 # 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑑) → (abs‘((𝐹‘𝑧) − 𝑥)) < 𝑒) ↔ ((𝑧 # 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑑) → (abs‘((𝐹‘𝑧) − 𝑥)) < ((abs‘(𝑥 − 𝑦)) / 2)))) |
3 | 2 | rexralbidv 2496 |
. . . . . . . 8
⊢ (𝑒 = ((abs‘(𝑥 − 𝑦)) / 2) → (∃𝑑 ∈ ℝ+ ∀𝑧 ∈ 𝐴 ((𝑧 # 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑑) → (abs‘((𝐹‘𝑧) − 𝑥)) < 𝑒) ↔ ∃𝑑 ∈ ℝ+ ∀𝑧 ∈ 𝐴 ((𝑧 # 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑑) → (abs‘((𝐹‘𝑧) − 𝑥)) < ((abs‘(𝑥 − 𝑦)) / 2)))) |
4 | | limcflf.f |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐹:𝐴⟶ℂ) |
5 | | limcflf.a |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐴 ⊆ ℂ) |
6 | | limcimo.b |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐵 ∈ ℂ) |
7 | 4, 5, 6 | ellimc3ap 13424 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑥 ∈ (𝐹 limℂ 𝐵) ↔ (𝑥 ∈ ℂ ∧ ∀𝑒 ∈ ℝ+
∃𝑑 ∈
ℝ+ ∀𝑧 ∈ 𝐴 ((𝑧 # 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑑) → (abs‘((𝐹‘𝑧) − 𝑥)) < 𝑒)))) |
8 | 7 | biimpa 294 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐹 limℂ 𝐵)) → (𝑥 ∈ ℂ ∧ ∀𝑒 ∈ ℝ+
∃𝑑 ∈
ℝ+ ∀𝑧 ∈ 𝐴 ((𝑧 # 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑑) → (abs‘((𝐹‘𝑧) − 𝑥)) < 𝑒))) |
9 | 8 | adantrr 476 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ (𝐹 limℂ 𝐵) ∧ 𝑦 ∈ (𝐹 limℂ 𝐵))) → (𝑥 ∈ ℂ ∧ ∀𝑒 ∈ ℝ+
∃𝑑 ∈
ℝ+ ∀𝑧 ∈ 𝐴 ((𝑧 # 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑑) → (abs‘((𝐹‘𝑧) − 𝑥)) < 𝑒))) |
10 | 9 | simprd 113 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ (𝐹 limℂ 𝐵) ∧ 𝑦 ∈ (𝐹 limℂ 𝐵))) → ∀𝑒 ∈ ℝ+ ∃𝑑 ∈ ℝ+
∀𝑧 ∈ 𝐴 ((𝑧 # 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑑) → (abs‘((𝐹‘𝑧) − 𝑥)) < 𝑒)) |
11 | 10 | adantr 274 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 ∈ (𝐹 limℂ 𝐵) ∧ 𝑦 ∈ (𝐹 limℂ 𝐵))) ∧ 𝑥 # 𝑦) → ∀𝑒 ∈ ℝ+ ∃𝑑 ∈ ℝ+
∀𝑧 ∈ 𝐴 ((𝑧 # 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑑) → (abs‘((𝐹‘𝑧) − 𝑥)) < 𝑒)) |
12 | 9 | simpld 111 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑥 ∈ (𝐹 limℂ 𝐵) ∧ 𝑦 ∈ (𝐹 limℂ 𝐵))) → 𝑥 ∈ ℂ) |
13 | 12 | adantr 274 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ∈ (𝐹 limℂ 𝐵) ∧ 𝑦 ∈ (𝐹 limℂ 𝐵))) ∧ 𝑥 # 𝑦) → 𝑥 ∈ ℂ) |
14 | 4, 5, 6 | ellimc3ap 13424 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑦 ∈ (𝐹 limℂ 𝐵) ↔ (𝑦 ∈ ℂ ∧ ∀𝑓 ∈ ℝ+
∃𝑔 ∈
ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤 # 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑔) → (abs‘((𝐹‘𝑤) − 𝑦)) < 𝑓)))) |
15 | 14 | biimpa 294 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐹 limℂ 𝐵)) → (𝑦 ∈ ℂ ∧ ∀𝑓 ∈ ℝ+
∃𝑔 ∈
ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤 # 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑔) → (abs‘((𝐹‘𝑤) − 𝑦)) < 𝑓))) |
16 | 15 | adantrl 475 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑥 ∈ (𝐹 limℂ 𝐵) ∧ 𝑦 ∈ (𝐹 limℂ 𝐵))) → (𝑦 ∈ ℂ ∧ ∀𝑓 ∈ ℝ+
∃𝑔 ∈
ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤 # 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑔) → (abs‘((𝐹‘𝑤) − 𝑦)) < 𝑓))) |
17 | 16 | simpld 111 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑥 ∈ (𝐹 limℂ 𝐵) ∧ 𝑦 ∈ (𝐹 limℂ 𝐵))) → 𝑦 ∈ ℂ) |
18 | 17 | adantr 274 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ∈ (𝐹 limℂ 𝐵) ∧ 𝑦 ∈ (𝐹 limℂ 𝐵))) ∧ 𝑥 # 𝑦) → 𝑦 ∈ ℂ) |
19 | 13, 18 | subcld 8230 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ∈ (𝐹 limℂ 𝐵) ∧ 𝑦 ∈ (𝐹 limℂ 𝐵))) ∧ 𝑥 # 𝑦) → (𝑥 − 𝑦) ∈ ℂ) |
20 | | simpr 109 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ∈ (𝐹 limℂ 𝐵) ∧ 𝑦 ∈ (𝐹 limℂ 𝐵))) ∧ 𝑥 # 𝑦) → 𝑥 # 𝑦) |
21 | 13, 18, 20 | subap0d 8563 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ∈ (𝐹 limℂ 𝐵) ∧ 𝑦 ∈ (𝐹 limℂ 𝐵))) ∧ 𝑥 # 𝑦) → (𝑥 − 𝑦) # 0) |
22 | 19, 21 | absrpclapd 11152 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ (𝐹 limℂ 𝐵) ∧ 𝑦 ∈ (𝐹 limℂ 𝐵))) ∧ 𝑥 # 𝑦) → (abs‘(𝑥 − 𝑦)) ∈
ℝ+) |
23 | 22 | rphalfcld 9666 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 ∈ (𝐹 limℂ 𝐵) ∧ 𝑦 ∈ (𝐹 limℂ 𝐵))) ∧ 𝑥 # 𝑦) → ((abs‘(𝑥 − 𝑦)) / 2) ∈
ℝ+) |
24 | 3, 11, 23 | rspcdva 2839 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑥 ∈ (𝐹 limℂ 𝐵) ∧ 𝑦 ∈ (𝐹 limℂ 𝐵))) ∧ 𝑥 # 𝑦) → ∃𝑑 ∈ ℝ+ ∀𝑧 ∈ 𝐴 ((𝑧 # 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑑) → (abs‘((𝐹‘𝑧) − 𝑥)) < ((abs‘(𝑥 − 𝑦)) / 2))) |
25 | | breq2 3993 |
. . . . . . . . . . . 12
⊢ (𝑓 = ((abs‘(𝑥 − 𝑦)) / 2) → ((abs‘((𝐹‘𝑤) − 𝑦)) < 𝑓 ↔ (abs‘((𝐹‘𝑤) − 𝑦)) < ((abs‘(𝑥 − 𝑦)) / 2))) |
26 | 25 | imbi2d 229 |
. . . . . . . . . . 11
⊢ (𝑓 = ((abs‘(𝑥 − 𝑦)) / 2) → (((𝑤 # 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑔) → (abs‘((𝐹‘𝑤) − 𝑦)) < 𝑓) ↔ ((𝑤 # 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑔) → (abs‘((𝐹‘𝑤) − 𝑦)) < ((abs‘(𝑥 − 𝑦)) / 2)))) |
27 | 26 | rexralbidv 2496 |
. . . . . . . . . 10
⊢ (𝑓 = ((abs‘(𝑥 − 𝑦)) / 2) → (∃𝑔 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤 # 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑔) → (abs‘((𝐹‘𝑤) − 𝑦)) < 𝑓) ↔ ∃𝑔 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤 # 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑔) → (abs‘((𝐹‘𝑤) − 𝑦)) < ((abs‘(𝑥 − 𝑦)) / 2)))) |
28 | 16 | simprd 113 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ (𝐹 limℂ 𝐵) ∧ 𝑦 ∈ (𝐹 limℂ 𝐵))) → ∀𝑓 ∈ ℝ+ ∃𝑔 ∈ ℝ+
∀𝑤 ∈ 𝐴 ((𝑤 # 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑔) → (abs‘((𝐹‘𝑤) − 𝑦)) < 𝑓)) |
29 | 28 | adantr 274 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ∈ (𝐹 limℂ 𝐵) ∧ 𝑦 ∈ (𝐹 limℂ 𝐵))) ∧ 𝑥 # 𝑦) → ∀𝑓 ∈ ℝ+ ∃𝑔 ∈ ℝ+
∀𝑤 ∈ 𝐴 ((𝑤 # 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑔) → (abs‘((𝐹‘𝑤) − 𝑦)) < 𝑓)) |
30 | 27, 29, 23 | rspcdva 2839 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ (𝐹 limℂ 𝐵) ∧ 𝑦 ∈ (𝐹 limℂ 𝐵))) ∧ 𝑥 # 𝑦) → ∃𝑔 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤 # 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑔) → (abs‘((𝐹‘𝑤) − 𝑦)) < ((abs‘(𝑥 − 𝑦)) / 2))) |
31 | 30 | adantr 274 |
. . . . . . . 8
⊢ ((((𝜑 ∧ (𝑥 ∈ (𝐹 limℂ 𝐵) ∧ 𝑦 ∈ (𝐹 limℂ 𝐵))) ∧ 𝑥 # 𝑦) ∧ (𝑑 ∈ ℝ+ ∧
∀𝑧 ∈ 𝐴 ((𝑧 # 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑑) → (abs‘((𝐹‘𝑧) − 𝑥)) < ((abs‘(𝑥 − 𝑦)) / 2)))) → ∃𝑔 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤 # 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑔) → (abs‘((𝐹‘𝑤) − 𝑦)) < ((abs‘(𝑥 − 𝑦)) / 2))) |
32 | 4 | ad4antr 491 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ (𝑥 ∈ (𝐹 limℂ 𝐵) ∧ 𝑦 ∈ (𝐹 limℂ 𝐵))) ∧ 𝑥 # 𝑦) ∧ (𝑑 ∈ ℝ+ ∧
∀𝑧 ∈ 𝐴 ((𝑧 # 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑑) → (abs‘((𝐹‘𝑧) − 𝑥)) < ((abs‘(𝑥 − 𝑦)) / 2)))) ∧ (𝑔 ∈ ℝ+ ∧
∀𝑤 ∈ 𝐴 ((𝑤 # 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑔) → (abs‘((𝐹‘𝑤) − 𝑦)) < ((abs‘(𝑥 − 𝑦)) / 2)))) → 𝐹:𝐴⟶ℂ) |
33 | 5 | ad4antr 491 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ (𝑥 ∈ (𝐹 limℂ 𝐵) ∧ 𝑦 ∈ (𝐹 limℂ 𝐵))) ∧ 𝑥 # 𝑦) ∧ (𝑑 ∈ ℝ+ ∧
∀𝑧 ∈ 𝐴 ((𝑧 # 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑑) → (abs‘((𝐹‘𝑧) − 𝑥)) < ((abs‘(𝑥 − 𝑦)) / 2)))) ∧ (𝑔 ∈ ℝ+ ∧
∀𝑤 ∈ 𝐴 ((𝑤 # 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑔) → (abs‘((𝐹‘𝑤) − 𝑦)) < ((abs‘(𝑥 − 𝑦)) / 2)))) → 𝐴 ⊆ ℂ) |
34 | 6 | ad4antr 491 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ (𝑥 ∈ (𝐹 limℂ 𝐵) ∧ 𝑦 ∈ (𝐹 limℂ 𝐵))) ∧ 𝑥 # 𝑦) ∧ (𝑑 ∈ ℝ+ ∧
∀𝑧 ∈ 𝐴 ((𝑧 # 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑑) → (abs‘((𝐹‘𝑧) − 𝑥)) < ((abs‘(𝑥 − 𝑦)) / 2)))) ∧ (𝑔 ∈ ℝ+ ∧
∀𝑤 ∈ 𝐴 ((𝑤 # 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑔) → (abs‘((𝐹‘𝑤) − 𝑦)) < ((abs‘(𝑥 − 𝑦)) / 2)))) → 𝐵 ∈ ℂ) |
35 | | limcimo.bc |
. . . . . . . . . 10
⊢ (𝜑 → 𝐵 ∈ 𝐶) |
36 | 35 | ad4antr 491 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ (𝑥 ∈ (𝐹 limℂ 𝐵) ∧ 𝑦 ∈ (𝐹 limℂ 𝐵))) ∧ 𝑥 # 𝑦) ∧ (𝑑 ∈ ℝ+ ∧
∀𝑧 ∈ 𝐴 ((𝑧 # 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑑) → (abs‘((𝐹‘𝑧) − 𝑥)) < ((abs‘(𝑥 − 𝑦)) / 2)))) ∧ (𝑔 ∈ ℝ+ ∧
∀𝑤 ∈ 𝐴 ((𝑤 # 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑔) → (abs‘((𝐹‘𝑤) − 𝑦)) < ((abs‘(𝑥 − 𝑦)) / 2)))) → 𝐵 ∈ 𝐶) |
37 | | limcimo.bs |
. . . . . . . . . 10
⊢ (𝜑 → 𝐵 ∈ 𝑆) |
38 | 37 | ad4antr 491 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ (𝑥 ∈ (𝐹 limℂ 𝐵) ∧ 𝑦 ∈ (𝐹 limℂ 𝐵))) ∧ 𝑥 # 𝑦) ∧ (𝑑 ∈ ℝ+ ∧
∀𝑧 ∈ 𝐴 ((𝑧 # 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑑) → (abs‘((𝐹‘𝑧) − 𝑥)) < ((abs‘(𝑥 − 𝑦)) / 2)))) ∧ (𝑔 ∈ ℝ+ ∧
∀𝑤 ∈ 𝐴 ((𝑤 # 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑔) → (abs‘((𝐹‘𝑤) − 𝑦)) < ((abs‘(𝑥 − 𝑦)) / 2)))) → 𝐵 ∈ 𝑆) |
39 | | limcimo.c |
. . . . . . . . . 10
⊢ (𝜑 → 𝐶 ∈ (𝐾 ↾t 𝑆)) |
40 | 39 | ad4antr 491 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ (𝑥 ∈ (𝐹 limℂ 𝐵) ∧ 𝑦 ∈ (𝐹 limℂ 𝐵))) ∧ 𝑥 # 𝑦) ∧ (𝑑 ∈ ℝ+ ∧
∀𝑧 ∈ 𝐴 ((𝑧 # 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑑) → (abs‘((𝐹‘𝑧) − 𝑥)) < ((abs‘(𝑥 − 𝑦)) / 2)))) ∧ (𝑔 ∈ ℝ+ ∧
∀𝑤 ∈ 𝐴 ((𝑤 # 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑔) → (abs‘((𝐹‘𝑤) − 𝑦)) < ((abs‘(𝑥 − 𝑦)) / 2)))) → 𝐶 ∈ (𝐾 ↾t 𝑆)) |
41 | | limcimo.s |
. . . . . . . . . 10
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ}) |
42 | 41 | ad4antr 491 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ (𝑥 ∈ (𝐹 limℂ 𝐵) ∧ 𝑦 ∈ (𝐹 limℂ 𝐵))) ∧ 𝑥 # 𝑦) ∧ (𝑑 ∈ ℝ+ ∧
∀𝑧 ∈ 𝐴 ((𝑧 # 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑑) → (abs‘((𝐹‘𝑧) − 𝑥)) < ((abs‘(𝑥 − 𝑦)) / 2)))) ∧ (𝑔 ∈ ℝ+ ∧
∀𝑤 ∈ 𝐴 ((𝑤 # 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑔) → (abs‘((𝐹‘𝑤) − 𝑦)) < ((abs‘(𝑥 − 𝑦)) / 2)))) → 𝑆 ∈ {ℝ, ℂ}) |
43 | | limcimo.ca |
. . . . . . . . . 10
⊢ (𝜑 → {𝑞 ∈ 𝐶 ∣ 𝑞 # 𝐵} ⊆ 𝐴) |
44 | 43 | ad4antr 491 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ (𝑥 ∈ (𝐹 limℂ 𝐵) ∧ 𝑦 ∈ (𝐹 limℂ 𝐵))) ∧ 𝑥 # 𝑦) ∧ (𝑑 ∈ ℝ+ ∧
∀𝑧 ∈ 𝐴 ((𝑧 # 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑑) → (abs‘((𝐹‘𝑧) − 𝑥)) < ((abs‘(𝑥 − 𝑦)) / 2)))) ∧ (𝑔 ∈ ℝ+ ∧
∀𝑤 ∈ 𝐴 ((𝑤 # 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑔) → (abs‘((𝐹‘𝑤) − 𝑦)) < ((abs‘(𝑥 − 𝑦)) / 2)))) → {𝑞 ∈ 𝐶 ∣ 𝑞 # 𝐵} ⊆ 𝐴) |
45 | | limcflfcntop.k |
. . . . . . . . 9
⊢ 𝐾 = (MetOpen‘(abs ∘
− )) |
46 | | simplrl 530 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ (𝑥 ∈ (𝐹 limℂ 𝐵) ∧ 𝑦 ∈ (𝐹 limℂ 𝐵))) ∧ 𝑥 # 𝑦) ∧ (𝑑 ∈ ℝ+ ∧
∀𝑧 ∈ 𝐴 ((𝑧 # 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑑) → (abs‘((𝐹‘𝑧) − 𝑥)) < ((abs‘(𝑥 − 𝑦)) / 2)))) ∧ (𝑔 ∈ ℝ+ ∧
∀𝑤 ∈ 𝐴 ((𝑤 # 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑔) → (abs‘((𝐹‘𝑤) − 𝑦)) < ((abs‘(𝑥 − 𝑦)) / 2)))) → 𝑑 ∈ ℝ+) |
47 | | simprl 526 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ (𝐹 limℂ 𝐵) ∧ 𝑦 ∈ (𝐹 limℂ 𝐵))) → 𝑥 ∈ (𝐹 limℂ 𝐵)) |
48 | 47 | ad3antrrr 489 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ (𝑥 ∈ (𝐹 limℂ 𝐵) ∧ 𝑦 ∈ (𝐹 limℂ 𝐵))) ∧ 𝑥 # 𝑦) ∧ (𝑑 ∈ ℝ+ ∧
∀𝑧 ∈ 𝐴 ((𝑧 # 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑑) → (abs‘((𝐹‘𝑧) − 𝑥)) < ((abs‘(𝑥 − 𝑦)) / 2)))) ∧ (𝑔 ∈ ℝ+ ∧
∀𝑤 ∈ 𝐴 ((𝑤 # 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑔) → (abs‘((𝐹‘𝑤) − 𝑦)) < ((abs‘(𝑥 − 𝑦)) / 2)))) → 𝑥 ∈ (𝐹 limℂ 𝐵)) |
49 | | simprr 527 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ (𝐹 limℂ 𝐵) ∧ 𝑦 ∈ (𝐹 limℂ 𝐵))) → 𝑦 ∈ (𝐹 limℂ 𝐵)) |
50 | 49 | ad3antrrr 489 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ (𝑥 ∈ (𝐹 limℂ 𝐵) ∧ 𝑦 ∈ (𝐹 limℂ 𝐵))) ∧ 𝑥 # 𝑦) ∧ (𝑑 ∈ ℝ+ ∧
∀𝑧 ∈ 𝐴 ((𝑧 # 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑑) → (abs‘((𝐹‘𝑧) − 𝑥)) < ((abs‘(𝑥 − 𝑦)) / 2)))) ∧ (𝑔 ∈ ℝ+ ∧
∀𝑤 ∈ 𝐴 ((𝑤 # 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑔) → (abs‘((𝐹‘𝑤) − 𝑦)) < ((abs‘(𝑥 − 𝑦)) / 2)))) → 𝑦 ∈ (𝐹 limℂ 𝐵)) |
51 | | simplrr 531 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ (𝑥 ∈ (𝐹 limℂ 𝐵) ∧ 𝑦 ∈ (𝐹 limℂ 𝐵))) ∧ 𝑥 # 𝑦) ∧ (𝑑 ∈ ℝ+ ∧
∀𝑧 ∈ 𝐴 ((𝑧 # 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑑) → (abs‘((𝐹‘𝑧) − 𝑥)) < ((abs‘(𝑥 − 𝑦)) / 2)))) ∧ (𝑔 ∈ ℝ+ ∧
∀𝑤 ∈ 𝐴 ((𝑤 # 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑔) → (abs‘((𝐹‘𝑤) − 𝑦)) < ((abs‘(𝑥 − 𝑦)) / 2)))) → ∀𝑧 ∈ 𝐴 ((𝑧 # 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑑) → (abs‘((𝐹‘𝑧) − 𝑥)) < ((abs‘(𝑥 − 𝑦)) / 2))) |
52 | | simprl 526 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ (𝑥 ∈ (𝐹 limℂ 𝐵) ∧ 𝑦 ∈ (𝐹 limℂ 𝐵))) ∧ 𝑥 # 𝑦) ∧ (𝑑 ∈ ℝ+ ∧
∀𝑧 ∈ 𝐴 ((𝑧 # 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑑) → (abs‘((𝐹‘𝑧) − 𝑥)) < ((abs‘(𝑥 − 𝑦)) / 2)))) ∧ (𝑔 ∈ ℝ+ ∧
∀𝑤 ∈ 𝐴 ((𝑤 # 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑔) → (abs‘((𝐹‘𝑤) − 𝑦)) < ((abs‘(𝑥 − 𝑦)) / 2)))) → 𝑔 ∈ ℝ+) |
53 | | simprr 527 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ (𝑥 ∈ (𝐹 limℂ 𝐵) ∧ 𝑦 ∈ (𝐹 limℂ 𝐵))) ∧ 𝑥 # 𝑦) ∧ (𝑑 ∈ ℝ+ ∧
∀𝑧 ∈ 𝐴 ((𝑧 # 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑑) → (abs‘((𝐹‘𝑧) − 𝑥)) < ((abs‘(𝑥 − 𝑦)) / 2)))) ∧ (𝑔 ∈ ℝ+ ∧
∀𝑤 ∈ 𝐴 ((𝑤 # 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑔) → (abs‘((𝐹‘𝑤) − 𝑦)) < ((abs‘(𝑥 − 𝑦)) / 2)))) → ∀𝑤 ∈ 𝐴 ((𝑤 # 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑔) → (abs‘((𝐹‘𝑤) − 𝑦)) < ((abs‘(𝑥 − 𝑦)) / 2))) |
54 | 32, 33, 34, 36, 38, 40, 42, 44, 45, 46, 48, 50, 51, 52, 53 | limcimolemlt 13427 |
. . . . . . . 8
⊢
(((((𝜑 ∧ (𝑥 ∈ (𝐹 limℂ 𝐵) ∧ 𝑦 ∈ (𝐹 limℂ 𝐵))) ∧ 𝑥 # 𝑦) ∧ (𝑑 ∈ ℝ+ ∧
∀𝑧 ∈ 𝐴 ((𝑧 # 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑑) → (abs‘((𝐹‘𝑧) − 𝑥)) < ((abs‘(𝑥 − 𝑦)) / 2)))) ∧ (𝑔 ∈ ℝ+ ∧
∀𝑤 ∈ 𝐴 ((𝑤 # 𝐵 ∧ (abs‘(𝑤 − 𝐵)) < 𝑔) → (abs‘((𝐹‘𝑤) − 𝑦)) < ((abs‘(𝑥 − 𝑦)) / 2)))) → (abs‘(𝑥 − 𝑦)) < (abs‘(𝑥 − 𝑦))) |
55 | 31, 54 | rexlimddv 2592 |
. . . . . . 7
⊢ ((((𝜑 ∧ (𝑥 ∈ (𝐹 limℂ 𝐵) ∧ 𝑦 ∈ (𝐹 limℂ 𝐵))) ∧ 𝑥 # 𝑦) ∧ (𝑑 ∈ ℝ+ ∧
∀𝑧 ∈ 𝐴 ((𝑧 # 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑑) → (abs‘((𝐹‘𝑧) − 𝑥)) < ((abs‘(𝑥 − 𝑦)) / 2)))) → (abs‘(𝑥 − 𝑦)) < (abs‘(𝑥 − 𝑦))) |
56 | 24, 55 | rexlimddv 2592 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑥 ∈ (𝐹 limℂ 𝐵) ∧ 𝑦 ∈ (𝐹 limℂ 𝐵))) ∧ 𝑥 # 𝑦) → (abs‘(𝑥 − 𝑦)) < (abs‘(𝑥 − 𝑦))) |
57 | 22 | rpred 9653 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑥 ∈ (𝐹 limℂ 𝐵) ∧ 𝑦 ∈ (𝐹 limℂ 𝐵))) ∧ 𝑥 # 𝑦) → (abs‘(𝑥 − 𝑦)) ∈ ℝ) |
58 | 57 | ltnrd 8031 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑥 ∈ (𝐹 limℂ 𝐵) ∧ 𝑦 ∈ (𝐹 limℂ 𝐵))) ∧ 𝑥 # 𝑦) → ¬ (abs‘(𝑥 − 𝑦)) < (abs‘(𝑥 − 𝑦))) |
59 | 56, 58 | pm2.65da 656 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ (𝐹 limℂ 𝐵) ∧ 𝑦 ∈ (𝐹 limℂ 𝐵))) → ¬ 𝑥 # 𝑦) |
60 | | apti 8541 |
. . . . . 6
⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝑥 = 𝑦 ↔ ¬ 𝑥 # 𝑦)) |
61 | 12, 17, 60 | syl2anc 409 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ (𝐹 limℂ 𝐵) ∧ 𝑦 ∈ (𝐹 limℂ 𝐵))) → (𝑥 = 𝑦 ↔ ¬ 𝑥 # 𝑦)) |
62 | 59, 61 | mpbird 166 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ (𝐹 limℂ 𝐵) ∧ 𝑦 ∈ (𝐹 limℂ 𝐵))) → 𝑥 = 𝑦) |
63 | 62 | ex 114 |
. . 3
⊢ (𝜑 → ((𝑥 ∈ (𝐹 limℂ 𝐵) ∧ 𝑦 ∈ (𝐹 limℂ 𝐵)) → 𝑥 = 𝑦)) |
64 | 63 | alrimivv 1868 |
. 2
⊢ (𝜑 → ∀𝑥∀𝑦((𝑥 ∈ (𝐹 limℂ 𝐵) ∧ 𝑦 ∈ (𝐹 limℂ 𝐵)) → 𝑥 = 𝑦)) |
65 | | eleq1w 2231 |
. . 3
⊢ (𝑥 = 𝑦 → (𝑥 ∈ (𝐹 limℂ 𝐵) ↔ 𝑦 ∈ (𝐹 limℂ 𝐵))) |
66 | 65 | mo4 2080 |
. 2
⊢
(∃*𝑥 𝑥 ∈ (𝐹 limℂ 𝐵) ↔ ∀𝑥∀𝑦((𝑥 ∈ (𝐹 limℂ 𝐵) ∧ 𝑦 ∈ (𝐹 limℂ 𝐵)) → 𝑥 = 𝑦)) |
67 | 64, 66 | sylibr 133 |
1
⊢ (𝜑 → ∃*𝑥 𝑥 ∈ (𝐹 limℂ 𝐵)) |