| Step | Hyp | Ref
| Expression |
| 1 | | limcrecl.4 |
. . 3
⊢ (𝜑 → 𝐿 ∈ (𝐹 limℂ 𝐵)) |
| 2 | 1 | adantr 480 |
. 2
⊢ ((𝜑 ∧ ¬ 𝐿 ∈ ℝ) → 𝐿 ∈ (𝐹 limℂ 𝐵)) |
| 3 | | limccl 25910 |
. . . . . . . . . 10
⊢ (𝐹 limℂ 𝐵) ⊆
ℂ |
| 4 | 3, 1 | sselid 3981 |
. . . . . . . . 9
⊢ (𝜑 → 𝐿 ∈ ℂ) |
| 5 | 4 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ ¬ 𝐿 ∈ ℝ) → 𝐿 ∈ ℂ) |
| 6 | | simpr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ ¬ 𝐿 ∈ ℝ) → ¬ 𝐿 ∈
ℝ) |
| 7 | 5, 6 | eldifd 3962 |
. . . . . . 7
⊢ ((𝜑 ∧ ¬ 𝐿 ∈ ℝ) → 𝐿 ∈ (ℂ ∖
ℝ)) |
| 8 | 7 | dstregt0 45293 |
. . . . . 6
⊢ ((𝜑 ∧ ¬ 𝐿 ∈ ℝ) → ∃𝑥 ∈ ℝ+
∀𝑤 ∈ ℝ
𝑥 < (abs‘(𝐿 − 𝑤))) |
| 9 | | cnxmet 24793 |
. . . . . . . . . . . . . 14
⊢ (abs
∘ − ) ∈ (∞Met‘ℂ) |
| 10 | 9 | a1i 11 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ ¬
𝐿 ∈ ℝ) ∧
𝑥 ∈
ℝ+) ∧ ∀𝑤 ∈ ℝ 𝑥 < (abs‘(𝐿 − 𝑤))) ∧ 𝑦 ∈ ℝ+) → (abs
∘ − ) ∈ (∞Met‘ℂ)) |
| 11 | | limcrecl.2 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐴 ⊆ ℂ) |
| 12 | 11 | ad4antr 732 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ ¬
𝐿 ∈ ℝ) ∧
𝑥 ∈
ℝ+) ∧ ∀𝑤 ∈ ℝ 𝑥 < (abs‘(𝐿 − 𝑤))) ∧ 𝑦 ∈ ℝ+) → 𝐴 ⊆
ℂ) |
| 13 | 12 | ssdifssd 4147 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ ¬
𝐿 ∈ ℝ) ∧
𝑥 ∈
ℝ+) ∧ ∀𝑤 ∈ ℝ 𝑥 < (abs‘(𝐿 − 𝑤))) ∧ 𝑦 ∈ ℝ+) → (𝐴 ∖ {𝐵}) ⊆ ℂ) |
| 14 | | limcrecl.3 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐵 ∈
((limPt‘(TopOpen‘ℂfld))‘𝐴)) |
| 15 | | eqid 2737 |
. . . . . . . . . . . . . . . . . 18
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
| 16 | 15 | cnfldtop 24804 |
. . . . . . . . . . . . . . . . 17
⊢
(TopOpen‘ℂfld) ∈ Top |
| 17 | 16 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 →
(TopOpen‘ℂfld) ∈ Top) |
| 18 | | unicntop 24806 |
. . . . . . . . . . . . . . . . 17
⊢ ℂ =
∪
(TopOpen‘ℂfld) |
| 19 | 11, 18 | sseqtrdi 4024 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐴 ⊆ ∪
(TopOpen‘ℂfld)) |
| 20 | | eqid 2737 |
. . . . . . . . . . . . . . . . 17
⊢ ∪ (TopOpen‘ℂfld) = ∪ (TopOpen‘ℂfld) |
| 21 | 20 | lpdifsn 23151 |
. . . . . . . . . . . . . . . 16
⊢
(((TopOpen‘ℂfld) ∈ Top ∧ 𝐴 ⊆ ∪ (TopOpen‘ℂfld)) → (𝐵 ∈
((limPt‘(TopOpen‘ℂfld))‘𝐴) ↔ 𝐵 ∈
((limPt‘(TopOpen‘ℂfld))‘(𝐴 ∖ {𝐵})))) |
| 22 | 17, 19, 21 | syl2anc 584 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐵 ∈
((limPt‘(TopOpen‘ℂfld))‘𝐴) ↔ 𝐵 ∈
((limPt‘(TopOpen‘ℂfld))‘(𝐴 ∖ {𝐵})))) |
| 23 | 14, 22 | mpbid 232 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐵 ∈
((limPt‘(TopOpen‘ℂfld))‘(𝐴 ∖ {𝐵}))) |
| 24 | 23 | ad4antr 732 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ ¬
𝐿 ∈ ℝ) ∧
𝑥 ∈
ℝ+) ∧ ∀𝑤 ∈ ℝ 𝑥 < (abs‘(𝐿 − 𝑤))) ∧ 𝑦 ∈ ℝ+) → 𝐵 ∈
((limPt‘(TopOpen‘ℂfld))‘(𝐴 ∖ {𝐵}))) |
| 25 | | simpr 484 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ ¬
𝐿 ∈ ℝ) ∧
𝑥 ∈
ℝ+) ∧ ∀𝑤 ∈ ℝ 𝑥 < (abs‘(𝐿 − 𝑤))) ∧ 𝑦 ∈ ℝ+) → 𝑦 ∈
ℝ+) |
| 26 | 15 | cnfldtopn 24802 |
. . . . . . . . . . . . . 14
⊢
(TopOpen‘ℂfld) = (MetOpen‘(abs ∘
− )) |
| 27 | 26 | lpbl 24516 |
. . . . . . . . . . . . 13
⊢ ((((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ (𝐴 ∖ {𝐵}) ⊆ ℂ ∧ 𝐵 ∈
((limPt‘(TopOpen‘ℂfld))‘(𝐴 ∖ {𝐵}))) ∧ 𝑦 ∈ ℝ+) →
∃𝑧 ∈ (𝐴 ∖ {𝐵})𝑧 ∈ (𝐵(ball‘(abs ∘ − ))𝑦)) |
| 28 | 10, 13, 24, 25, 27 | syl31anc 1375 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ ¬
𝐿 ∈ ℝ) ∧
𝑥 ∈
ℝ+) ∧ ∀𝑤 ∈ ℝ 𝑥 < (abs‘(𝐿 − 𝑤))) ∧ 𝑦 ∈ ℝ+) →
∃𝑧 ∈ (𝐴 ∖ {𝐵})𝑧 ∈ (𝐵(ball‘(abs ∘ − ))𝑦)) |
| 29 | | eldif 3961 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 ∈ (𝐴 ∖ {𝐵}) ↔ (𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ∈ {𝐵})) |
| 30 | 29 | anbi1i 624 |
. . . . . . . . . . . . . 14
⊢ ((𝑧 ∈ (𝐴 ∖ {𝐵}) ∧ 𝑧 ∈ (𝐵(ball‘(abs ∘ − ))𝑦)) ↔ ((𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ∈ {𝐵}) ∧ 𝑧 ∈ (𝐵(ball‘(abs ∘ − ))𝑦))) |
| 31 | | anass 468 |
. . . . . . . . . . . . . 14
⊢ (((𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ∈ {𝐵}) ∧ 𝑧 ∈ (𝐵(ball‘(abs ∘ − ))𝑦)) ↔ (𝑧 ∈ 𝐴 ∧ (¬ 𝑧 ∈ {𝐵} ∧ 𝑧 ∈ (𝐵(ball‘(abs ∘ − ))𝑦)))) |
| 32 | 30, 31 | bitri 275 |
. . . . . . . . . . . . 13
⊢ ((𝑧 ∈ (𝐴 ∖ {𝐵}) ∧ 𝑧 ∈ (𝐵(ball‘(abs ∘ − ))𝑦)) ↔ (𝑧 ∈ 𝐴 ∧ (¬ 𝑧 ∈ {𝐵} ∧ 𝑧 ∈ (𝐵(ball‘(abs ∘ − ))𝑦)))) |
| 33 | 32 | rexbii2 3090 |
. . . . . . . . . . . 12
⊢
(∃𝑧 ∈
(𝐴 ∖ {𝐵})𝑧 ∈ (𝐵(ball‘(abs ∘ − ))𝑦) ↔ ∃𝑧 ∈ 𝐴 (¬ 𝑧 ∈ {𝐵} ∧ 𝑧 ∈ (𝐵(ball‘(abs ∘ − ))𝑦))) |
| 34 | 28, 33 | sylib 218 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ ¬
𝐿 ∈ ℝ) ∧
𝑥 ∈
ℝ+) ∧ ∀𝑤 ∈ ℝ 𝑥 < (abs‘(𝐿 − 𝑤))) ∧ 𝑦 ∈ ℝ+) →
∃𝑧 ∈ 𝐴 (¬ 𝑧 ∈ {𝐵} ∧ 𝑧 ∈ (𝐵(ball‘(abs ∘ − ))𝑦))) |
| 35 | | simprl 771 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝜑 ∧ ¬
𝐿 ∈ ℝ) ∧
𝑥 ∈
ℝ+) ∧ ∀𝑤 ∈ ℝ 𝑥 < (abs‘(𝐿 − 𝑤))) ∧ 𝑦 ∈ ℝ+) ∧ (¬
𝑧 ∈ {𝐵} ∧ 𝑧 ∈ (𝐵(ball‘(abs ∘ − ))𝑦))) → ¬ 𝑧 ∈ {𝐵}) |
| 36 | | velsn 4642 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑧 ∈ {𝐵} ↔ 𝑧 = 𝐵) |
| 37 | 36 | necon3bbii 2988 |
. . . . . . . . . . . . . . . . 17
⊢ (¬
𝑧 ∈ {𝐵} ↔ 𝑧 ≠ 𝐵) |
| 38 | 35, 37 | sylib 218 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝜑 ∧ ¬
𝐿 ∈ ℝ) ∧
𝑥 ∈
ℝ+) ∧ ∀𝑤 ∈ ℝ 𝑥 < (abs‘(𝐿 − 𝑤))) ∧ 𝑦 ∈ ℝ+) ∧ (¬
𝑧 ∈ {𝐵} ∧ 𝑧 ∈ (𝐵(ball‘(abs ∘ − ))𝑦))) → 𝑧 ≠ 𝐵) |
| 39 | | simp-5l 785 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝜑 ∧ ¬
𝐿 ∈ ℝ) ∧
𝑥 ∈
ℝ+) ∧ ∀𝑤 ∈ ℝ 𝑥 < (abs‘(𝐿 − 𝑤))) ∧ 𝑦 ∈ ℝ+) ∧ (¬
𝑧 ∈ {𝐵} ∧ 𝑧 ∈ (𝐵(ball‘(abs ∘ − ))𝑦))) → 𝜑) |
| 40 | | simplr 769 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝜑 ∧ ¬
𝐿 ∈ ℝ) ∧
𝑥 ∈
ℝ+) ∧ ∀𝑤 ∈ ℝ 𝑥 < (abs‘(𝐿 − 𝑤))) ∧ 𝑦 ∈ ℝ+) ∧ (¬
𝑧 ∈ {𝐵} ∧ 𝑧 ∈ (𝐵(ball‘(abs ∘ − ))𝑦))) → 𝑦 ∈ ℝ+) |
| 41 | | simprr 773 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝜑 ∧ ¬
𝐿 ∈ ℝ) ∧
𝑥 ∈
ℝ+) ∧ ∀𝑤 ∈ ℝ 𝑥 < (abs‘(𝐿 − 𝑤))) ∧ 𝑦 ∈ ℝ+) ∧ (¬
𝑧 ∈ {𝐵} ∧ 𝑧 ∈ (𝐵(ball‘(abs ∘ − ))𝑦))) → 𝑧 ∈ (𝐵(ball‘(abs ∘ − ))𝑦)) |
| 42 | | simp3 1139 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+ ∧ 𝑧 ∈ (𝐵(ball‘(abs ∘ − ))𝑦)) → 𝑧 ∈ (𝐵(ball‘(abs ∘ − ))𝑦)) |
| 43 | 9 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+ ∧ 𝑧 ∈ (𝐵(ball‘(abs ∘ − ))𝑦)) → (abs ∘ − )
∈ (∞Met‘ℂ)) |
| 44 | 18 | lpss 23150 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((TopOpen‘ℂfld) ∈ Top ∧ 𝐴 ⊆ ℂ) →
((limPt‘(TopOpen‘ℂfld))‘𝐴) ⊆ ℂ) |
| 45 | 17, 11, 44 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 →
((limPt‘(TopOpen‘ℂfld))‘𝐴) ⊆ ℂ) |
| 46 | 45, 14 | sseldd 3984 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → 𝐵 ∈ ℂ) |
| 47 | 46 | 3ad2ant1 1134 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+ ∧ 𝑧 ∈ (𝐵(ball‘(abs ∘ − ))𝑦)) → 𝐵 ∈ ℂ) |
| 48 | | rpxr 13044 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑦 ∈ ℝ+
→ 𝑦 ∈
ℝ*) |
| 49 | 48 | 3ad2ant2 1135 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+ ∧ 𝑧 ∈ (𝐵(ball‘(abs ∘ − ))𝑦)) → 𝑦 ∈ ℝ*) |
| 50 | | elbl 24398 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 𝐵 ∈ ℂ ∧ 𝑦 ∈ ℝ*) → (𝑧 ∈ (𝐵(ball‘(abs ∘ − ))𝑦) ↔ (𝑧 ∈ ℂ ∧ (𝐵(abs ∘ − )𝑧) < 𝑦))) |
| 51 | 43, 47, 49, 50 | syl3anc 1373 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+ ∧ 𝑧 ∈ (𝐵(ball‘(abs ∘ − ))𝑦)) → (𝑧 ∈ (𝐵(ball‘(abs ∘ − ))𝑦) ↔ (𝑧 ∈ ℂ ∧ (𝐵(abs ∘ − )𝑧) < 𝑦))) |
| 52 | 42, 51 | mpbid 232 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+ ∧ 𝑧 ∈ (𝐵(ball‘(abs ∘ − ))𝑦)) → (𝑧 ∈ ℂ ∧ (𝐵(abs ∘ − )𝑧) < 𝑦)) |
| 53 | 52 | simpld 494 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+ ∧ 𝑧 ∈ (𝐵(ball‘(abs ∘ − ))𝑦)) → 𝑧 ∈ ℂ) |
| 54 | 53, 47 | abssubd 15492 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+ ∧ 𝑧 ∈ (𝐵(ball‘(abs ∘ − ))𝑦)) → (abs‘(𝑧 − 𝐵)) = (abs‘(𝐵 − 𝑧))) |
| 55 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (abs
∘ − ) = (abs ∘ − ) |
| 56 | 55 | cnmetdval 24791 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐵 ∈ ℂ ∧ 𝑧 ∈ ℂ) → (𝐵(abs ∘ − )𝑧) = (abs‘(𝐵 − 𝑧))) |
| 57 | 47, 53, 56 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+ ∧ 𝑧 ∈ (𝐵(ball‘(abs ∘ − ))𝑦)) → (𝐵(abs ∘ − )𝑧) = (abs‘(𝐵 − 𝑧))) |
| 58 | 52 | simprd 495 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+ ∧ 𝑧 ∈ (𝐵(ball‘(abs ∘ − ))𝑦)) → (𝐵(abs ∘ − )𝑧) < 𝑦) |
| 59 | 57, 58 | eqbrtrrd 5167 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+ ∧ 𝑧 ∈ (𝐵(ball‘(abs ∘ − ))𝑦)) → (abs‘(𝐵 − 𝑧)) < 𝑦) |
| 60 | 54, 59 | eqbrtrd 5165 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+ ∧ 𝑧 ∈ (𝐵(ball‘(abs ∘ − ))𝑦)) → (abs‘(𝑧 − 𝐵)) < 𝑦) |
| 61 | 39, 40, 41, 60 | syl3anc 1373 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝜑 ∧ ¬
𝐿 ∈ ℝ) ∧
𝑥 ∈
ℝ+) ∧ ∀𝑤 ∈ ℝ 𝑥 < (abs‘(𝐿 − 𝑤))) ∧ 𝑦 ∈ ℝ+) ∧ (¬
𝑧 ∈ {𝐵} ∧ 𝑧 ∈ (𝐵(ball‘(abs ∘ − ))𝑦))) → (abs‘(𝑧 − 𝐵)) < 𝑦) |
| 62 | 38, 61 | jca 511 |
. . . . . . . . . . . . . . 15
⊢
((((((𝜑 ∧ ¬
𝐿 ∈ ℝ) ∧
𝑥 ∈
ℝ+) ∧ ∀𝑤 ∈ ℝ 𝑥 < (abs‘(𝐿 − 𝑤))) ∧ 𝑦 ∈ ℝ+) ∧ (¬
𝑧 ∈ {𝐵} ∧ 𝑧 ∈ (𝐵(ball‘(abs ∘ − ))𝑦))) → (𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑦)) |
| 63 | 62 | adantlr 715 |
. . . . . . . . . . . . . 14
⊢
(((((((𝜑 ∧ ¬
𝐿 ∈ ℝ) ∧
𝑥 ∈
ℝ+) ∧ ∀𝑤 ∈ ℝ 𝑥 < (abs‘(𝐿 − 𝑤))) ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ 𝐴) ∧ (¬ 𝑧 ∈ {𝐵} ∧ 𝑧 ∈ (𝐵(ball‘(abs ∘ − ))𝑦))) → (𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑦)) |
| 64 | 39 | adantlr 715 |
. . . . . . . . . . . . . . . 16
⊢
(((((((𝜑 ∧ ¬
𝐿 ∈ ℝ) ∧
𝑥 ∈
ℝ+) ∧ ∀𝑤 ∈ ℝ 𝑥 < (abs‘(𝐿 − 𝑤))) ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ 𝐴) ∧ (¬ 𝑧 ∈ {𝐵} ∧ 𝑧 ∈ (𝐵(ball‘(abs ∘ − ))𝑦))) → 𝜑) |
| 65 | | simplr 769 |
. . . . . . . . . . . . . . . 16
⊢
(((((((𝜑 ∧ ¬
𝐿 ∈ ℝ) ∧
𝑥 ∈
ℝ+) ∧ ∀𝑤 ∈ ℝ 𝑥 < (abs‘(𝐿 − 𝑤))) ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ 𝐴) ∧ (¬ 𝑧 ∈ {𝐵} ∧ 𝑧 ∈ (𝐵(ball‘(abs ∘ − ))𝑦))) → 𝑧 ∈ 𝐴) |
| 66 | 64, 65 | jca 511 |
. . . . . . . . . . . . . . 15
⊢
(((((((𝜑 ∧ ¬
𝐿 ∈ ℝ) ∧
𝑥 ∈
ℝ+) ∧ ∀𝑤 ∈ ℝ 𝑥 < (abs‘(𝐿 − 𝑤))) ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ 𝐴) ∧ (¬ 𝑧 ∈ {𝐵} ∧ 𝑧 ∈ (𝐵(ball‘(abs ∘ − ))𝑦))) → (𝜑 ∧ 𝑧 ∈ 𝐴)) |
| 67 | | simp-5r 786 |
. . . . . . . . . . . . . . 15
⊢
(((((((𝜑 ∧ ¬
𝐿 ∈ ℝ) ∧
𝑥 ∈
ℝ+) ∧ ∀𝑤 ∈ ℝ 𝑥 < (abs‘(𝐿 − 𝑤))) ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ 𝐴) ∧ (¬ 𝑧 ∈ {𝐵} ∧ 𝑧 ∈ (𝐵(ball‘(abs ∘ − ))𝑦))) → 𝑥 ∈ ℝ+) |
| 68 | | simp-4r 784 |
. . . . . . . . . . . . . . 15
⊢
(((((((𝜑 ∧ ¬
𝐿 ∈ ℝ) ∧
𝑥 ∈
ℝ+) ∧ ∀𝑤 ∈ ℝ 𝑥 < (abs‘(𝐿 − 𝑤))) ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ 𝐴) ∧ (¬ 𝑧 ∈ {𝐵} ∧ 𝑧 ∈ (𝐵(ball‘(abs ∘ − ))𝑦))) → ∀𝑤 ∈ ℝ 𝑥 < (abs‘(𝐿 − 𝑤))) |
| 69 | | rpre 13043 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ ℝ+
→ 𝑥 ∈
ℝ) |
| 70 | 69 | ad2antlr 727 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑥 ∈ ℝ+) ∧
∀𝑤 ∈ ℝ
𝑥 < (abs‘(𝐿 − 𝑤))) → 𝑥 ∈ ℝ) |
| 71 | | limcrecl.1 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 𝐹:𝐴⟶ℝ) |
| 72 | 71 | ffvelcdmda 7104 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → (𝐹‘𝑧) ∈ ℝ) |
| 73 | 72 | recnd 11289 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → (𝐹‘𝑧) ∈ ℂ) |
| 74 | 73 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑥 ∈ ℝ+) ∧
∀𝑤 ∈ ℝ
𝑥 < (abs‘(𝐿 − 𝑤))) → (𝐹‘𝑧) ∈ ℂ) |
| 75 | 4 | ad3antrrr 730 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑥 ∈ ℝ+) ∧
∀𝑤 ∈ ℝ
𝑥 < (abs‘(𝐿 − 𝑤))) → 𝐿 ∈ ℂ) |
| 76 | 74, 75 | subcld 11620 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑥 ∈ ℝ+) ∧
∀𝑤 ∈ ℝ
𝑥 < (abs‘(𝐿 − 𝑤))) → ((𝐹‘𝑧) − 𝐿) ∈ ℂ) |
| 77 | 76 | abscld 15475 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑥 ∈ ℝ+) ∧
∀𝑤 ∈ ℝ
𝑥 < (abs‘(𝐿 − 𝑤))) → (abs‘((𝐹‘𝑧) − 𝐿)) ∈ ℝ) |
| 78 | 72 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ ∀𝑤 ∈ ℝ 𝑥 < (abs‘(𝐿 − 𝑤))) → (𝐹‘𝑧) ∈ ℝ) |
| 79 | | nfv 1914 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
Ⅎ𝑤𝜑 |
| 80 | | nfra1 3284 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
Ⅎ𝑤∀𝑤 ∈ ℝ 𝑥 < (abs‘(𝐿 − 𝑤)) |
| 81 | 79, 80 | nfan 1899 |
. . . . . . . . . . . . . . . . . . . 20
⊢
Ⅎ𝑤(𝜑 ∧ ∀𝑤 ∈ ℝ 𝑥 < (abs‘(𝐿 − 𝑤))) |
| 82 | | rspa 3248 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((∀𝑤 ∈
ℝ 𝑥 <
(abs‘(𝐿 − 𝑤)) ∧ 𝑤 ∈ ℝ) → 𝑥 < (abs‘(𝐿 − 𝑤))) |
| 83 | 82 | adantll 714 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ ∀𝑤 ∈ ℝ 𝑥 < (abs‘(𝐿 − 𝑤))) ∧ 𝑤 ∈ ℝ) → 𝑥 < (abs‘(𝐿 − 𝑤))) |
| 84 | 4 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑤 ∈ ℝ) → 𝐿 ∈ ℂ) |
| 85 | | ax-resscn 11212 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ℝ
⊆ ℂ |
| 86 | 85 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → ℝ ⊆
ℂ) |
| 87 | 86 | sselda 3983 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑤 ∈ ℝ) → 𝑤 ∈ ℂ) |
| 88 | 84, 87 | abssubd 15492 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑤 ∈ ℝ) → (abs‘(𝐿 − 𝑤)) = (abs‘(𝑤 − 𝐿))) |
| 89 | 88 | adantlr 715 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ ∀𝑤 ∈ ℝ 𝑥 < (abs‘(𝐿 − 𝑤))) ∧ 𝑤 ∈ ℝ) → (abs‘(𝐿 − 𝑤)) = (abs‘(𝑤 − 𝐿))) |
| 90 | 83, 89 | breqtrd 5169 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ ∀𝑤 ∈ ℝ 𝑥 < (abs‘(𝐿 − 𝑤))) ∧ 𝑤 ∈ ℝ) → 𝑥 < (abs‘(𝑤 − 𝐿))) |
| 91 | 90 | ex 412 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ ∀𝑤 ∈ ℝ 𝑥 < (abs‘(𝐿 − 𝑤))) → (𝑤 ∈ ℝ → 𝑥 < (abs‘(𝑤 − 𝐿)))) |
| 92 | 81, 91 | ralrimi 3257 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ ∀𝑤 ∈ ℝ 𝑥 < (abs‘(𝐿 − 𝑤))) → ∀𝑤 ∈ ℝ 𝑥 < (abs‘(𝑤 − 𝐿))) |
| 93 | 92 | adantlr 715 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ ∀𝑤 ∈ ℝ 𝑥 < (abs‘(𝐿 − 𝑤))) → ∀𝑤 ∈ ℝ 𝑥 < (abs‘(𝑤 − 𝐿))) |
| 94 | | fvoveq1 7454 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑤 = (𝐹‘𝑧) → (abs‘(𝑤 − 𝐿)) = (abs‘((𝐹‘𝑧) − 𝐿))) |
| 95 | 94 | breq2d 5155 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑤 = (𝐹‘𝑧) → (𝑥 < (abs‘(𝑤 − 𝐿)) ↔ 𝑥 < (abs‘((𝐹‘𝑧) − 𝐿)))) |
| 96 | 95 | rspcv 3618 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐹‘𝑧) ∈ ℝ → (∀𝑤 ∈ ℝ 𝑥 < (abs‘(𝑤 − 𝐿)) → 𝑥 < (abs‘((𝐹‘𝑧) − 𝐿)))) |
| 97 | 78, 93, 96 | sylc 65 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ ∀𝑤 ∈ ℝ 𝑥 < (abs‘(𝐿 − 𝑤))) → 𝑥 < (abs‘((𝐹‘𝑧) − 𝐿))) |
| 98 | 97 | adantlr 715 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑥 ∈ ℝ+) ∧
∀𝑤 ∈ ℝ
𝑥 < (abs‘(𝐿 − 𝑤))) → 𝑥 < (abs‘((𝐹‘𝑧) − 𝐿))) |
| 99 | 70, 77, 98 | ltnsymd 11410 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑥 ∈ ℝ+) ∧
∀𝑤 ∈ ℝ
𝑥 < (abs‘(𝐿 − 𝑤))) → ¬ (abs‘((𝐹‘𝑧) − 𝐿)) < 𝑥) |
| 100 | 66, 67, 68, 99 | syl21anc 838 |
. . . . . . . . . . . . . 14
⊢
(((((((𝜑 ∧ ¬
𝐿 ∈ ℝ) ∧
𝑥 ∈
ℝ+) ∧ ∀𝑤 ∈ ℝ 𝑥 < (abs‘(𝐿 − 𝑤))) ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ 𝐴) ∧ (¬ 𝑧 ∈ {𝐵} ∧ 𝑧 ∈ (𝐵(ball‘(abs ∘ − ))𝑦))) → ¬
(abs‘((𝐹‘𝑧) − 𝐿)) < 𝑥) |
| 101 | 63, 100 | jcnd 163 |
. . . . . . . . . . . . 13
⊢
(((((((𝜑 ∧ ¬
𝐿 ∈ ℝ) ∧
𝑥 ∈
ℝ+) ∧ ∀𝑤 ∈ ℝ 𝑥 < (abs‘(𝐿 − 𝑤))) ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ 𝐴) ∧ (¬ 𝑧 ∈ {𝐵} ∧ 𝑧 ∈ (𝐵(ball‘(abs ∘ − ))𝑦))) → ¬ ((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑦) → (abs‘((𝐹‘𝑧) − 𝐿)) < 𝑥)) |
| 102 | 101 | ex 412 |
. . . . . . . . . . . 12
⊢
((((((𝜑 ∧ ¬
𝐿 ∈ ℝ) ∧
𝑥 ∈
ℝ+) ∧ ∀𝑤 ∈ ℝ 𝑥 < (abs‘(𝐿 − 𝑤))) ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ 𝐴) → ((¬ 𝑧 ∈ {𝐵} ∧ 𝑧 ∈ (𝐵(ball‘(abs ∘ − ))𝑦)) → ¬ ((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑦) → (abs‘((𝐹‘𝑧) − 𝐿)) < 𝑥))) |
| 103 | 102 | reximdva 3168 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ ¬
𝐿 ∈ ℝ) ∧
𝑥 ∈
ℝ+) ∧ ∀𝑤 ∈ ℝ 𝑥 < (abs‘(𝐿 − 𝑤))) ∧ 𝑦 ∈ ℝ+) →
(∃𝑧 ∈ 𝐴 (¬ 𝑧 ∈ {𝐵} ∧ 𝑧 ∈ (𝐵(ball‘(abs ∘ − ))𝑦)) → ∃𝑧 ∈ 𝐴 ¬ ((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑦) → (abs‘((𝐹‘𝑧) − 𝐿)) < 𝑥))) |
| 104 | 34, 103 | mpd 15 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ ¬
𝐿 ∈ ℝ) ∧
𝑥 ∈
ℝ+) ∧ ∀𝑤 ∈ ℝ 𝑥 < (abs‘(𝐿 − 𝑤))) ∧ 𝑦 ∈ ℝ+) →
∃𝑧 ∈ 𝐴 ¬ ((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑦) → (abs‘((𝐹‘𝑧) − 𝐿)) < 𝑥)) |
| 105 | | rexnal 3100 |
. . . . . . . . . 10
⊢
(∃𝑧 ∈
𝐴 ¬ ((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑦) → (abs‘((𝐹‘𝑧) − 𝐿)) < 𝑥) ↔ ¬ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑦) → (abs‘((𝐹‘𝑧) − 𝐿)) < 𝑥)) |
| 106 | 104, 105 | sylib 218 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ ¬
𝐿 ∈ ℝ) ∧
𝑥 ∈
ℝ+) ∧ ∀𝑤 ∈ ℝ 𝑥 < (abs‘(𝐿 − 𝑤))) ∧ 𝑦 ∈ ℝ+) → ¬
∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑦) → (abs‘((𝐹‘𝑧) − 𝐿)) < 𝑥)) |
| 107 | 106 | nrexdv 3149 |
. . . . . . . 8
⊢ ((((𝜑 ∧ ¬ 𝐿 ∈ ℝ) ∧ 𝑥 ∈ ℝ+) ∧
∀𝑤 ∈ ℝ
𝑥 < (abs‘(𝐿 − 𝑤))) → ¬ ∃𝑦 ∈ ℝ+ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑦) → (abs‘((𝐹‘𝑧) − 𝐿)) < 𝑥)) |
| 108 | 107 | ex 412 |
. . . . . . 7
⊢ (((𝜑 ∧ ¬ 𝐿 ∈ ℝ) ∧ 𝑥 ∈ ℝ+) →
(∀𝑤 ∈ ℝ
𝑥 < (abs‘(𝐿 − 𝑤)) → ¬ ∃𝑦 ∈ ℝ+ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑦) → (abs‘((𝐹‘𝑧) − 𝐿)) < 𝑥))) |
| 109 | 108 | reximdva 3168 |
. . . . . 6
⊢ ((𝜑 ∧ ¬ 𝐿 ∈ ℝ) → (∃𝑥 ∈ ℝ+
∀𝑤 ∈ ℝ
𝑥 < (abs‘(𝐿 − 𝑤)) → ∃𝑥 ∈ ℝ+ ¬
∃𝑦 ∈
ℝ+ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑦) → (abs‘((𝐹‘𝑧) − 𝐿)) < 𝑥))) |
| 110 | 8, 109 | mpd 15 |
. . . . 5
⊢ ((𝜑 ∧ ¬ 𝐿 ∈ ℝ) → ∃𝑥 ∈ ℝ+
¬ ∃𝑦 ∈
ℝ+ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑦) → (abs‘((𝐹‘𝑧) − 𝐿)) < 𝑥)) |
| 111 | | rexnal 3100 |
. . . . 5
⊢
(∃𝑥 ∈
ℝ+ ¬ ∃𝑦 ∈ ℝ+ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑦) → (abs‘((𝐹‘𝑧) − 𝐿)) < 𝑥) ↔ ¬ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ ℝ+
∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑦) → (abs‘((𝐹‘𝑧) − 𝐿)) < 𝑥)) |
| 112 | 110, 111 | sylib 218 |
. . . 4
⊢ ((𝜑 ∧ ¬ 𝐿 ∈ ℝ) → ¬ ∀𝑥 ∈ ℝ+
∃𝑦 ∈
ℝ+ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑦) → (abs‘((𝐹‘𝑧) − 𝐿)) < 𝑥)) |
| 113 | 112 | intnand 488 |
. . 3
⊢ ((𝜑 ∧ ¬ 𝐿 ∈ ℝ) → ¬ (𝐿 ∈ ℂ ∧
∀𝑥 ∈
ℝ+ ∃𝑦 ∈ ℝ+ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑦) → (abs‘((𝐹‘𝑧) − 𝐿)) < 𝑥))) |
| 114 | 71, 86 | fssd 6753 |
. . . . 5
⊢ (𝜑 → 𝐹:𝐴⟶ℂ) |
| 115 | 114, 11, 46 | ellimc3 25914 |
. . . 4
⊢ (𝜑 → (𝐿 ∈ (𝐹 limℂ 𝐵) ↔ (𝐿 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+
∃𝑦 ∈
ℝ+ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑦) → (abs‘((𝐹‘𝑧) − 𝐿)) < 𝑥)))) |
| 116 | 115 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ ¬ 𝐿 ∈ ℝ) → (𝐿 ∈ (𝐹 limℂ 𝐵) ↔ (𝐿 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+
∃𝑦 ∈
ℝ+ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑦) → (abs‘((𝐹‘𝑧) − 𝐿)) < 𝑥)))) |
| 117 | 113, 116 | mtbird 325 |
. 2
⊢ ((𝜑 ∧ ¬ 𝐿 ∈ ℝ) → ¬ 𝐿 ∈ (𝐹 limℂ 𝐵)) |
| 118 | 2, 117 | condan 818 |
1
⊢ (𝜑 → 𝐿 ∈ ℝ) |