Users' Mathboxes Mathbox for Glauco Siliprandi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  limclner Structured version   Visualization version   GIF version

Theorem limclner 41495
Description: For a limit point, both from the left and from the right, of the domain, the limit of the function exits only if the left and the right limits are equal. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
Hypotheses
Ref Expression
limclner.k 𝐾 = (TopOpen‘ℂfld)
limclner.a (𝜑𝐴 ⊆ ℝ)
limclner.j 𝐽 = (topGen‘ran (,))
limclner.f (𝜑𝐹:𝐴⟶ℂ)
limclner.blp1 (𝜑𝐵 ∈ ((limPt‘𝐽)‘(𝐴 ∩ (-∞(,)𝐵))))
limclner.blp2 (𝜑𝐵 ∈ ((limPt‘𝐽)‘(𝐴 ∩ (𝐵(,)+∞))))
limclner.l (𝜑𝐿 ∈ ((𝐹 ↾ (-∞(,)𝐵)) lim 𝐵))
limclner.r (𝜑𝑅 ∈ ((𝐹 ↾ (𝐵(,)+∞)) lim 𝐵))
limclner.lner (𝜑𝐿𝑅)
Assertion
Ref Expression
limclner (𝜑 → (𝐹 lim 𝐵) = ∅)

Proof of Theorem limclner
Dummy variables 𝑎 𝑏 𝑢 𝑣 𝑧 𝑤 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 limccl 24160 . . . . . . . . . . . . 13 ((𝐹 ↾ (𝐵(,)+∞)) lim 𝐵) ⊆ ℂ
2 limclner.r . . . . . . . . . . . . 13 (𝜑𝑅 ∈ ((𝐹 ↾ (𝐵(,)+∞)) lim 𝐵))
31, 2sseldi 3893 . . . . . . . . . . . 12 (𝜑𝑅 ∈ ℂ)
43ad2antrr 722 . . . . . . . . . . 11 (((𝜑𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) → 𝑅 ∈ ℂ)
5 limccl 24160 . . . . . . . . . . . . 13 ((𝐹 ↾ (-∞(,)𝐵)) lim 𝐵) ⊆ ℂ
6 limclner.l . . . . . . . . . . . . 13 (𝜑𝐿 ∈ ((𝐹 ↾ (-∞(,)𝐵)) lim 𝐵))
75, 6sseldi 3893 . . . . . . . . . . . 12 (𝜑𝐿 ∈ ℂ)
87ad2antrr 722 . . . . . . . . . . 11 (((𝜑𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) → 𝐿 ∈ ℂ)
94, 8subcld 10851 . . . . . . . . . 10 (((𝜑𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) → (𝑅𝐿) ∈ ℂ)
10 limclner.lner . . . . . . . . . . . . 13 (𝜑𝐿𝑅)
1110necomd 3041 . . . . . . . . . . . 12 (𝜑𝑅𝐿)
1211ad2antrr 722 . . . . . . . . . . 11 (((𝜑𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) → 𝑅𝐿)
134, 8, 12subne0d 10860 . . . . . . . . . 10 (((𝜑𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) → (𝑅𝐿) ≠ 0)
149, 13absrpcld 14646 . . . . . . . . 9 (((𝜑𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) → (abs‘(𝑅𝐿)) ∈ ℝ+)
15 4re 11575 . . . . . . . . . . 11 4 ∈ ℝ
16 4pos 11598 . . . . . . . . . . 11 0 < 4
1715, 16elrpii 12246 . . . . . . . . . 10 4 ∈ ℝ+
1817a1i 11 . . . . . . . . 9 (((𝜑𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) → 4 ∈ ℝ+)
1914, 18rpdivcld 12302 . . . . . . . 8 (((𝜑𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) → ((abs‘(𝑅𝐿)) / 4) ∈ ℝ+)
20 nfv 1896 . . . . . . . . . . 11 𝑦(𝜑𝑥 ∈ ℂ)
21 nfra1 3188 . . . . . . . . . . 11 𝑦𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)
2220, 21nfan 1885 . . . . . . . . . 10 𝑦((𝜑𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦))
23 nfv 1896 . . . . . . . . . 10 𝑦(((abs‘(𝑅𝐿)) / 4) ∈ ℝ+ → ∃𝑎𝐴𝑏𝐴 (abs‘(𝑅𝐿)) < (4 · ((abs‘(𝑅𝐿)) / 4)))
2422, 23nfim 1882 . . . . . . . . 9 𝑦(((𝜑𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) → (((abs‘(𝑅𝐿)) / 4) ∈ ℝ+ → ∃𝑎𝐴𝑏𝐴 (abs‘(𝑅𝐿)) < (4 · ((abs‘(𝑅𝐿)) / 4))))
25 ovex 7055 . . . . . . . . 9 ((abs‘(𝑅𝐿)) / 4) ∈ V
26 eleq1 2872 . . . . . . . . . . 11 (𝑦 = ((abs‘(𝑅𝐿)) / 4) → (𝑦 ∈ ℝ+ ↔ ((abs‘(𝑅𝐿)) / 4) ∈ ℝ+))
27 oveq2 7031 . . . . . . . . . . . . 13 (𝑦 = ((abs‘(𝑅𝐿)) / 4) → (4 · 𝑦) = (4 · ((abs‘(𝑅𝐿)) / 4)))
2827breq2d 4980 . . . . . . . . . . . 12 (𝑦 = ((abs‘(𝑅𝐿)) / 4) → ((abs‘(𝑅𝐿)) < (4 · 𝑦) ↔ (abs‘(𝑅𝐿)) < (4 · ((abs‘(𝑅𝐿)) / 4))))
29282rexbidv 3265 . . . . . . . . . . 11 (𝑦 = ((abs‘(𝑅𝐿)) / 4) → (∃𝑎𝐴𝑏𝐴 (abs‘(𝑅𝐿)) < (4 · 𝑦) ↔ ∃𝑎𝐴𝑏𝐴 (abs‘(𝑅𝐿)) < (4 · ((abs‘(𝑅𝐿)) / 4))))
3026, 29imbi12d 346 . . . . . . . . . 10 (𝑦 = ((abs‘(𝑅𝐿)) / 4) → ((𝑦 ∈ ℝ+ → ∃𝑎𝐴𝑏𝐴 (abs‘(𝑅𝐿)) < (4 · 𝑦)) ↔ (((abs‘(𝑅𝐿)) / 4) ∈ ℝ+ → ∃𝑎𝐴𝑏𝐴 (abs‘(𝑅𝐿)) < (4 · ((abs‘(𝑅𝐿)) / 4)))))
3130imbi2d 342 . . . . . . . . 9 (𝑦 = ((abs‘(𝑅𝐿)) / 4) → ((((𝜑𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) → (𝑦 ∈ ℝ+ → ∃𝑎𝐴𝑏𝐴 (abs‘(𝑅𝐿)) < (4 · 𝑦))) ↔ (((𝜑𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) → (((abs‘(𝑅𝐿)) / 4) ∈ ℝ+ → ∃𝑎𝐴𝑏𝐴 (abs‘(𝑅𝐿)) < (4 · ((abs‘(𝑅𝐿)) / 4))))))
32 simpll 763 . . . . . . . . . . 11 ((((𝜑𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ 𝑦 ∈ ℝ+) → (𝜑𝑥 ∈ ℂ))
33 simpr 485 . . . . . . . . . . 11 ((((𝜑𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ 𝑦 ∈ ℝ+) → 𝑦 ∈ ℝ+)
34 rspa 3175 . . . . . . . . . . . 12 ((∀𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦) ∧ 𝑦 ∈ ℝ+) → ∃𝑧 ∈ ℝ+𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦))
3534adantll 710 . . . . . . . . . . 11 ((((𝜑𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ 𝑦 ∈ ℝ+) → ∃𝑧 ∈ ℝ+𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦))
36 limclner.f . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑𝐹:𝐴⟶ℂ)
37 fresin 6422 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝐹:𝐴⟶ℂ → (𝐹 ↾ (𝐵(,)+∞)):(𝐴 ∩ (𝐵(,)+∞))⟶ℂ)
3836, 37syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (𝐹 ↾ (𝐵(,)+∞)):(𝐴 ∩ (𝐵(,)+∞))⟶ℂ)
39 inss2 4132 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝐴 ∩ (𝐵(,)+∞)) ⊆ (𝐵(,)+∞)
40 ioosscn 41332 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝐵(,)+∞) ⊆ ℂ
4139, 40sstri 3904 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝐴 ∩ (𝐵(,)+∞)) ⊆ ℂ
4241a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (𝐴 ∩ (𝐵(,)+∞)) ⊆ ℂ)
43 limclner.j . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 𝐽 = (topGen‘ran (,))
44 retop 23057 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (topGen‘ran (,)) ∈ Top
4543, 44eqeltri 2881 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 𝐽 ∈ Top
46 inss2 4132 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝐴 ∩ (-∞(,)𝐵)) ⊆ (-∞(,)𝐵)
47 ioossre 12652 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (-∞(,)𝐵) ⊆ ℝ
4846, 47sstri 3904 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝐴 ∩ (-∞(,)𝐵)) ⊆ ℝ
49 uniretop 23058 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ℝ = (topGen‘ran (,))
5043unieqi 4760 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 𝐽 = (topGen‘ran (,))
5149, 50eqtr4i 2824 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ℝ = 𝐽
5251lpss 21438 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝐽 ∈ Top ∧ (𝐴 ∩ (-∞(,)𝐵)) ⊆ ℝ) → ((limPt‘𝐽)‘(𝐴 ∩ (-∞(,)𝐵))) ⊆ ℝ)
5345, 48, 52mp2an 688 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((limPt‘𝐽)‘(𝐴 ∩ (-∞(,)𝐵))) ⊆ ℝ
54 limclner.blp1 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑𝐵 ∈ ((limPt‘𝐽)‘(𝐴 ∩ (-∞(,)𝐵))))
5553, 54sseldi 3893 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑𝐵 ∈ ℝ)
5655recnd 10522 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑𝐵 ∈ ℂ)
5738, 42, 56ellimc3 24164 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (𝑅 ∈ ((𝐹 ↾ (𝐵(,)+∞)) lim 𝐵) ↔ (𝑅 ∈ ℂ ∧ ∀𝑦 ∈ ℝ+𝑣 ∈ ℝ+𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦))))
582, 57mpbid 233 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝑅 ∈ ℂ ∧ ∀𝑦 ∈ ℝ+𝑣 ∈ ℝ+𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)))
5958simprd 496 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ∀𝑦 ∈ ℝ+𝑣 ∈ ℝ+𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦))
6059r19.21bi 3177 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑦 ∈ ℝ+) → ∃𝑣 ∈ ℝ+𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦))
61603ad2ant1 1126 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) → ∃𝑣 ∈ ℝ+𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦))
62 simp11l 1277 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) → 𝜑)
63 simp12 1197 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) → 𝑧 ∈ ℝ+)
64 simp2 1130 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) → 𝑣 ∈ ℝ+)
65 breq2 4972 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑢 = if(𝑧𝑣, 𝑧, 𝑣) → ((abs‘(𝑏𝐵)) < 𝑢 ↔ (abs‘(𝑏𝐵)) < if(𝑧𝑣, 𝑧, 𝑣)))
6665rexbidv 3262 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑢 = if(𝑧𝑣, 𝑧, 𝑣) → (∃𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵})(abs‘(𝑏𝐵)) < 𝑢 ↔ ∃𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵})(abs‘(𝑏𝐵)) < if(𝑧𝑣, 𝑧, 𝑣)))
67 inss1 4131 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((limPt‘𝐾)‘(𝐴 ∩ (𝐵(,)+∞))) ∩ ℝ) ⊆ ((limPt‘𝐾)‘(𝐴 ∩ (𝐵(,)+∞)))
6867a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝜑 → (((limPt‘𝐾)‘(𝐴 ∩ (𝐵(,)+∞))) ∩ ℝ) ⊆ ((limPt‘𝐾)‘(𝐴 ∩ (𝐵(,)+∞))))
69 limclner.k . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 𝐾 = (TopOpen‘ℂfld)
7069cnfldtop 23079 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 𝐾 ∈ Top
7170a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝜑𝐾 ∈ Top)
72 ax-resscn 10447 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ℝ ⊆ ℂ
7372a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝜑 → ℝ ⊆ ℂ)
74 ioossre 12652 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝐵(,)+∞) ⊆ ℝ
7539, 74sstri 3904 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝐴 ∩ (𝐵(,)+∞)) ⊆ ℝ
7675a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝜑 → (𝐴 ∩ (𝐵(,)+∞)) ⊆ ℝ)
77 unicntop 23081 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ℂ = (TopOpen‘ℂfld)
7869unieqi 4760 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 𝐾 = (TopOpen‘ℂfld)
7977, 78eqtr4i 2824 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ℂ = 𝐾
8069tgioo2 23098 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (topGen‘ran (,)) = (𝐾t ℝ)
8143, 80eqtri 2821 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 𝐽 = (𝐾t ℝ)
8279, 81restlp 21479 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝐾 ∈ Top ∧ ℝ ⊆ ℂ ∧ (𝐴 ∩ (𝐵(,)+∞)) ⊆ ℝ) → ((limPt‘𝐽)‘(𝐴 ∩ (𝐵(,)+∞))) = (((limPt‘𝐾)‘(𝐴 ∩ (𝐵(,)+∞))) ∩ ℝ))
8371, 73, 76, 82syl3anc 1364 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝜑 → ((limPt‘𝐽)‘(𝐴 ∩ (𝐵(,)+∞))) = (((limPt‘𝐾)‘(𝐴 ∩ (𝐵(,)+∞))) ∩ ℝ))
8469eqcomi 2806 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (TopOpen‘ℂfld) = 𝐾
8584fveq2i 6548 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (limPt‘(TopOpen‘ℂfld)) = (limPt‘𝐾)
8685fveq1i 6546 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((limPt‘(TopOpen‘ℂfld))‘(𝐴 ∩ (𝐵(,)+∞))) = ((limPt‘𝐾)‘(𝐴 ∩ (𝐵(,)+∞)))
8786a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝜑 → ((limPt‘(TopOpen‘ℂfld))‘(𝐴 ∩ (𝐵(,)+∞))) = ((limPt‘𝐾)‘(𝐴 ∩ (𝐵(,)+∞))))
8868, 83, 873sstr4d 3941 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑 → ((limPt‘𝐽)‘(𝐴 ∩ (𝐵(,)+∞))) ⊆ ((limPt‘(TopOpen‘ℂfld))‘(𝐴 ∩ (𝐵(,)+∞))))
89 limclner.blp2 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑𝐵 ∈ ((limPt‘𝐽)‘(𝐴 ∩ (𝐵(,)+∞))))
9088, 89sseldd 3896 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑𝐵 ∈ ((limPt‘(TopOpen‘ℂfld))‘(𝐴 ∩ (𝐵(,)+∞))))
9142, 56islpcn 41483 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → (𝐵 ∈ ((limPt‘(TopOpen‘ℂfld))‘(𝐴 ∩ (𝐵(,)+∞))) ↔ ∀𝑢 ∈ ℝ+𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵})(abs‘(𝑏𝐵)) < 𝑢))
9290, 91mpbid 233 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → ∀𝑢 ∈ ℝ+𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵})(abs‘(𝑏𝐵)) < 𝑢)
93923ad2ant1 1126 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑧 ∈ ℝ+𝑣 ∈ ℝ+) → ∀𝑢 ∈ ℝ+𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵})(abs‘(𝑏𝐵)) < 𝑢)
94 ifcl 4431 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑧 ∈ ℝ+𝑣 ∈ ℝ+) → if(𝑧𝑣, 𝑧, 𝑣) ∈ ℝ+)
95943adant1 1123 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑧 ∈ ℝ+𝑣 ∈ ℝ+) → if(𝑧𝑣, 𝑧, 𝑣) ∈ ℝ+)
9666, 93, 95rspcdva 3567 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑧 ∈ ℝ+𝑣 ∈ ℝ+) → ∃𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵})(abs‘(𝑏𝐵)) < if(𝑧𝑣, 𝑧, 𝑣))
97 eldifi 4030 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵}) → 𝑏 ∈ (𝐴 ∩ (𝐵(,)+∞)))
9875, 97sseldi 3893 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵}) → 𝑏 ∈ ℝ)
9973sselda 3895 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝜑𝑏 ∈ ℝ) → 𝑏 ∈ ℂ)
10056adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝜑𝑏 ∈ ℝ) → 𝐵 ∈ ℂ)
10199, 100subcld 10851 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑𝑏 ∈ ℝ) → (𝑏𝐵) ∈ ℂ)
102101abscld 14634 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑𝑏 ∈ ℝ) → (abs‘(𝑏𝐵)) ∈ ℝ)
1031023ad2antl1 1178 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝜑𝑧 ∈ ℝ+𝑣 ∈ ℝ+) ∧ 𝑏 ∈ ℝ) → (abs‘(𝑏𝐵)) ∈ ℝ)
104103adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑𝑧 ∈ ℝ+𝑣 ∈ ℝ+) ∧ 𝑏 ∈ ℝ) ∧ (abs‘(𝑏𝐵)) < if(𝑧𝑣, 𝑧, 𝑣)) → (abs‘(𝑏𝐵)) ∈ ℝ)
10595rpred 12285 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑𝑧 ∈ ℝ+𝑣 ∈ ℝ+) → if(𝑧𝑣, 𝑧, 𝑣) ∈ ℝ)
106105ad2antrr 722 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑𝑧 ∈ ℝ+𝑣 ∈ ℝ+) ∧ 𝑏 ∈ ℝ) ∧ (abs‘(𝑏𝐵)) < if(𝑧𝑣, 𝑧, 𝑣)) → if(𝑧𝑣, 𝑧, 𝑣) ∈ ℝ)
107 rpre 12251 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑧 ∈ ℝ+𝑧 ∈ ℝ)
1081073ad2ant2 1127 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑𝑧 ∈ ℝ+𝑣 ∈ ℝ+) → 𝑧 ∈ ℝ)
109108ad2antrr 722 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑𝑧 ∈ ℝ+𝑣 ∈ ℝ+) ∧ 𝑏 ∈ ℝ) ∧ (abs‘(𝑏𝐵)) < if(𝑧𝑣, 𝑧, 𝑣)) → 𝑧 ∈ ℝ)
110 simpr 485 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑𝑧 ∈ ℝ+𝑣 ∈ ℝ+) ∧ 𝑏 ∈ ℝ) ∧ (abs‘(𝑏𝐵)) < if(𝑧𝑣, 𝑧, 𝑣)) → (abs‘(𝑏𝐵)) < if(𝑧𝑣, 𝑧, 𝑣))
111 rpre 12251 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑣 ∈ ℝ+𝑣 ∈ ℝ)
112 min1 12436 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑧 ∈ ℝ ∧ 𝑣 ∈ ℝ) → if(𝑧𝑣, 𝑧, 𝑣) ≤ 𝑧)
113107, 111, 112syl2an 595 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑧 ∈ ℝ+𝑣 ∈ ℝ+) → if(𝑧𝑣, 𝑧, 𝑣) ≤ 𝑧)
1141133adant1 1123 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑𝑧 ∈ ℝ+𝑣 ∈ ℝ+) → if(𝑧𝑣, 𝑧, 𝑣) ≤ 𝑧)
115114ad2antrr 722 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑𝑧 ∈ ℝ+𝑣 ∈ ℝ+) ∧ 𝑏 ∈ ℝ) ∧ (abs‘(𝑏𝐵)) < if(𝑧𝑣, 𝑧, 𝑣)) → if(𝑧𝑣, 𝑧, 𝑣) ≤ 𝑧)
116104, 106, 109, 110, 115ltletrd 10653 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑𝑧 ∈ ℝ+𝑣 ∈ ℝ+) ∧ 𝑏 ∈ ℝ) ∧ (abs‘(𝑏𝐵)) < if(𝑧𝑣, 𝑧, 𝑣)) → (abs‘(𝑏𝐵)) < 𝑧)
1171113ad2ant3 1128 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑𝑧 ∈ ℝ+𝑣 ∈ ℝ+) → 𝑣 ∈ ℝ)
118117ad2antrr 722 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑𝑧 ∈ ℝ+𝑣 ∈ ℝ+) ∧ 𝑏 ∈ ℝ) ∧ (abs‘(𝑏𝐵)) < if(𝑧𝑣, 𝑧, 𝑣)) → 𝑣 ∈ ℝ)
119109, 118min2d 41312 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑𝑧 ∈ ℝ+𝑣 ∈ ℝ+) ∧ 𝑏 ∈ ℝ) ∧ (abs‘(𝑏𝐵)) < if(𝑧𝑣, 𝑧, 𝑣)) → if(𝑧𝑣, 𝑧, 𝑣) ≤ 𝑣)
120104, 106, 118, 110, 119ltletrd 10653 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑𝑧 ∈ ℝ+𝑣 ∈ ℝ+) ∧ 𝑏 ∈ ℝ) ∧ (abs‘(𝑏𝐵)) < if(𝑧𝑣, 𝑧, 𝑣)) → (abs‘(𝑏𝐵)) < 𝑣)
121116, 120jca 512 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑𝑧 ∈ ℝ+𝑣 ∈ ℝ+) ∧ 𝑏 ∈ ℝ) ∧ (abs‘(𝑏𝐵)) < if(𝑧𝑣, 𝑧, 𝑣)) → ((abs‘(𝑏𝐵)) < 𝑧 ∧ (abs‘(𝑏𝐵)) < 𝑣))
122121ex 413 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑧 ∈ ℝ+𝑣 ∈ ℝ+) ∧ 𝑏 ∈ ℝ) → ((abs‘(𝑏𝐵)) < if(𝑧𝑣, 𝑧, 𝑣) → ((abs‘(𝑏𝐵)) < 𝑧 ∧ (abs‘(𝑏𝐵)) < 𝑣)))
12398, 122sylan2 592 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑧 ∈ ℝ+𝑣 ∈ ℝ+) ∧ 𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵})) → ((abs‘(𝑏𝐵)) < if(𝑧𝑣, 𝑧, 𝑣) → ((abs‘(𝑏𝐵)) < 𝑧 ∧ (abs‘(𝑏𝐵)) < 𝑣)))
124123reximdva 3239 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑧 ∈ ℝ+𝑣 ∈ ℝ+) → (∃𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵})(abs‘(𝑏𝐵)) < if(𝑧𝑣, 𝑧, 𝑣) → ∃𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵})((abs‘(𝑏𝐵)) < 𝑧 ∧ (abs‘(𝑏𝐵)) < 𝑣)))
12596, 124mpd 15 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑧 ∈ ℝ+𝑣 ∈ ℝ+) → ∃𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵})((abs‘(𝑏𝐵)) < 𝑧 ∧ (abs‘(𝑏𝐵)) < 𝑣))
12662, 63, 64, 125syl3anc 1364 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) → ∃𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵})((abs‘(𝑏𝐵)) < 𝑧 ∧ (abs‘(𝑏𝐵)) < 𝑣))
127 nfv 1896 . . . . . . . . . . . . . . . . . . . . . . 23 𝑏(((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦))
128 nfre1 3271 . . . . . . . . . . . . . . . . . . . . . . 23 𝑏𝑏𝐴 ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦)
12997elin1d 4102 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵}) → 𝑏𝐴)
1301293ad2ant2 1127 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) ∧ 𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵}) ∧ ((abs‘(𝑏𝐵)) < 𝑧 ∧ (abs‘(𝑏𝐵)) < 𝑣)) → 𝑏𝐴)
131 simp113 1297 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) ∧ 𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵}) ∧ ((abs‘(𝑏𝐵)) < 𝑧 ∧ (abs‘(𝑏𝐵)) < 𝑣)) → ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦))
132 eldifsni 4635 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵}) → 𝑏𝐵)
133132adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵}) ∧ ((abs‘(𝑏𝐵)) < 𝑧 ∧ (abs‘(𝑏𝐵)) < 𝑣)) → 𝑏𝐵)
134 simprl 767 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵}) ∧ ((abs‘(𝑏𝐵)) < 𝑧 ∧ (abs‘(𝑏𝐵)) < 𝑣)) → (abs‘(𝑏𝐵)) < 𝑧)
135133, 134jca 512 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵}) ∧ ((abs‘(𝑏𝐵)) < 𝑧 ∧ (abs‘(𝑏𝐵)) < 𝑣)) → (𝑏𝐵 ∧ (abs‘(𝑏𝐵)) < 𝑧))
1361353adant1 1123 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) ∧ 𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵}) ∧ ((abs‘(𝑏𝐵)) < 𝑧 ∧ (abs‘(𝑏𝐵)) < 𝑣)) → (𝑏𝐵 ∧ (abs‘(𝑏𝐵)) < 𝑧))
137 neeq1 3048 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑤 = 𝑏 → (𝑤𝐵𝑏𝐵))
138 fvoveq1 7046 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑤 = 𝑏 → (abs‘(𝑤𝐵)) = (abs‘(𝑏𝐵)))
139138breq1d 4978 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑤 = 𝑏 → ((abs‘(𝑤𝐵)) < 𝑧 ↔ (abs‘(𝑏𝐵)) < 𝑧))
140137, 139anbi12d 630 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑤 = 𝑏 → ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) ↔ (𝑏𝐵 ∧ (abs‘(𝑏𝐵)) < 𝑧)))
141140imbrov2fvoveq 7048 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑤 = 𝑏 → (((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦) ↔ ((𝑏𝐵 ∧ (abs‘(𝑏𝐵)) < 𝑧) → (abs‘((𝐹𝑏) − 𝑥)) < 𝑦)))
142141rspcva 3559 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑏𝐴 ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) → ((𝑏𝐵 ∧ (abs‘(𝑏𝐵)) < 𝑧) → (abs‘((𝐹𝑏) − 𝑥)) < 𝑦))
143142imp 407 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑏𝐴 ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ (𝑏𝐵 ∧ (abs‘(𝑏𝐵)) < 𝑧)) → (abs‘((𝐹𝑏) − 𝑥)) < 𝑦)
144130, 131, 136, 143syl21anc 834 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) ∧ 𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵}) ∧ ((abs‘(𝑏𝐵)) < 𝑧 ∧ (abs‘(𝑏𝐵)) < 𝑣)) → (abs‘((𝐹𝑏) − 𝑥)) < 𝑦)
145973ad2ant2 1127 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) ∧ 𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵}) ∧ ((abs‘(𝑏𝐵)) < 𝑧 ∧ (abs‘(𝑏𝐵)) < 𝑣)) → 𝑏 ∈ (𝐴 ∩ (𝐵(,)+∞)))
146623ad2ant1 1126 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) ∧ 𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵}) ∧ ((abs‘(𝑏𝐵)) < 𝑧 ∧ (abs‘(𝑏𝐵)) < 𝑣)) → 𝜑)
147 simp13 1198 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) ∧ 𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵}) ∧ ((abs‘(𝑏𝐵)) < 𝑧 ∧ (abs‘(𝑏𝐵)) < 𝑣)) → ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦))
148 nfv 1896 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 𝑤𝜑
149 nfra1 3188 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 𝑤𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)
150148, 149nfan 1885 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 𝑤(𝜑 ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦))
151 elinel2 4100 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞)) → 𝑤 ∈ (𝐵(,)+∞))
152151fvresd 6565 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞)) → ((𝐹 ↾ (𝐵(,)+∞))‘𝑤) = (𝐹𝑤))
153152eqcomd 2803 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞)) → (𝐹𝑤) = ((𝐹 ↾ (𝐵(,)+∞))‘𝑤))
154153fvoveq1d 7045 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞)) → (abs‘((𝐹𝑤) − 𝑅)) = (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)))
1551543ad2ant2 1127 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝜑 ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) ∧ 𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞)) ∧ (𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣)) → (abs‘((𝐹𝑤) − 𝑅)) = (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)))
156 rspa 3175 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦) ∧ 𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))) → ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦))
1571563impia 1110 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦) ∧ 𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞)) ∧ (𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣)) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)
1581573adant1l 1169 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝜑 ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) ∧ 𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞)) ∧ (𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣)) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)
159155, 158eqbrtrd 4990 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑 ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) ∧ 𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞)) ∧ (𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣)) → (abs‘((𝐹𝑤) − 𝑅)) < 𝑦)
1601593exp 1112 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑 ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) → (𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞)) → ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘((𝐹𝑤) − 𝑅)) < 𝑦)))
161150, 160ralrimi 3185 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑 ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) → ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘((𝐹𝑤) − 𝑅)) < 𝑦))
162146, 147, 161syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) ∧ 𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵}) ∧ ((abs‘(𝑏𝐵)) < 𝑧 ∧ (abs‘(𝑏𝐵)) < 𝑣)) → ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘((𝐹𝑤) − 𝑅)) < 𝑦))
163132anim1i 614 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵}) ∧ (abs‘(𝑏𝐵)) < 𝑣) → (𝑏𝐵 ∧ (abs‘(𝑏𝐵)) < 𝑣))
164163adantrl 712 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵}) ∧ ((abs‘(𝑏𝐵)) < 𝑧 ∧ (abs‘(𝑏𝐵)) < 𝑣)) → (𝑏𝐵 ∧ (abs‘(𝑏𝐵)) < 𝑣))
1651643adant1 1123 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) ∧ 𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵}) ∧ ((abs‘(𝑏𝐵)) < 𝑧 ∧ (abs‘(𝑏𝐵)) < 𝑣)) → (𝑏𝐵 ∧ (abs‘(𝑏𝐵)) < 𝑣))
166138breq1d 4978 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑤 = 𝑏 → ((abs‘(𝑤𝐵)) < 𝑣 ↔ (abs‘(𝑏𝐵)) < 𝑣))
167137, 166anbi12d 630 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑤 = 𝑏 → ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) ↔ (𝑏𝐵 ∧ (abs‘(𝑏𝐵)) < 𝑣)))
168167imbrov2fvoveq 7048 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑤 = 𝑏 → (((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘((𝐹𝑤) − 𝑅)) < 𝑦) ↔ ((𝑏𝐵 ∧ (abs‘(𝑏𝐵)) < 𝑣) → (abs‘((𝐹𝑏) − 𝑅)) < 𝑦)))
169168rspcva 3559 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑏 ∈ (𝐴 ∩ (𝐵(,)+∞)) ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘((𝐹𝑤) − 𝑅)) < 𝑦)) → ((𝑏𝐵 ∧ (abs‘(𝑏𝐵)) < 𝑣) → (abs‘((𝐹𝑏) − 𝑅)) < 𝑦))
170169imp 407 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑏 ∈ (𝐴 ∩ (𝐵(,)+∞)) ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘((𝐹𝑤) − 𝑅)) < 𝑦)) ∧ (𝑏𝐵 ∧ (abs‘(𝑏𝐵)) < 𝑣)) → (abs‘((𝐹𝑏) − 𝑅)) < 𝑦)
171145, 162, 165, 170syl21anc 834 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) ∧ 𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵}) ∧ ((abs‘(𝑏𝐵)) < 𝑧 ∧ (abs‘(𝑏𝐵)) < 𝑣)) → (abs‘((𝐹𝑏) − 𝑅)) < 𝑦)
172 rspe 3269 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑏𝐴 ∧ ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦)) → ∃𝑏𝐴 ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦))
173130, 144, 171, 172syl12anc 833 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) ∧ 𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵}) ∧ ((abs‘(𝑏𝐵)) < 𝑧 ∧ (abs‘(𝑏𝐵)) < 𝑣)) → ∃𝑏𝐴 ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦))
1741733exp 1112 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) → (𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵}) → (((abs‘(𝑏𝐵)) < 𝑧 ∧ (abs‘(𝑏𝐵)) < 𝑣) → ∃𝑏𝐴 ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦))))
175127, 128, 174rexlimd 3280 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) → (∃𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵})((abs‘(𝑏𝐵)) < 𝑧 ∧ (abs‘(𝑏𝐵)) < 𝑣) → ∃𝑏𝐴 ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦)))
176126, 175mpd 15 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) → ∃𝑏𝐴 ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦))
1771763exp 1112 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) → (𝑣 ∈ ℝ+ → (∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦) → ∃𝑏𝐴 ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦))))
178177rexlimdv 3248 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) → (∃𝑣 ∈ ℝ+𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦) → ∃𝑏𝐴 ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦)))
17961, 178mpd 15 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) → ∃𝑏𝐴 ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦))
1801793exp 1112 . . . . . . . . . . . . . . . . 17 ((𝜑𝑦 ∈ ℝ+) → (𝑧 ∈ ℝ+ → (∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦) → ∃𝑏𝐴 ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦))))
181180rexlimdv 3248 . . . . . . . . . . . . . . . 16 ((𝜑𝑦 ∈ ℝ+) → (∃𝑧 ∈ ℝ+𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦) → ∃𝑏𝐴 ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦)))
182181imp 407 . . . . . . . . . . . . . . 15 (((𝜑𝑦 ∈ ℝ+) ∧ ∃𝑧 ∈ ℝ+𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) → ∃𝑏𝐴 ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦))
183182adantllr 715 . . . . . . . . . . . . . 14 ((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ ∃𝑧 ∈ ℝ+𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) → ∃𝑏𝐴 ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦))
184183ad2antrr 722 . . . . . . . . . . . . 13 ((((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ ∃𝑧 ∈ ℝ+𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ 𝑎𝐴) ∧ ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)) → ∃𝑏𝐴 ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦))
1853ad6antr 732 . . . . . . . . . . . . . . . . . . 19 (((((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎𝐴) ∧ ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏𝐴) ∧ ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦)) → 𝑅 ∈ ℂ)
1867ad6antr 732 . . . . . . . . . . . . . . . . . . 19 (((((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎𝐴) ∧ ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏𝐴) ∧ ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦)) → 𝐿 ∈ ℂ)
187185, 186subcld 10851 . . . . . . . . . . . . . . . . . 18 (((((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎𝐴) ∧ ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏𝐴) ∧ ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦)) → (𝑅𝐿) ∈ ℂ)
188187abscld 14634 . . . . . . . . . . . . . . . . 17 (((((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎𝐴) ∧ ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏𝐴) ∧ ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦)) → (abs‘(𝑅𝐿)) ∈ ℝ)
189 simp-6l 783 . . . . . . . . . . . . . . . . . . . . . . 23 (((((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎𝐴) ∧ ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏𝐴) ∧ ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦)) → 𝜑)
190 simplr 765 . . . . . . . . . . . . . . . . . . . . . . 23 (((((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎𝐴) ∧ ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏𝐴) ∧ ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦)) → 𝑏𝐴)
19136ffvelrnda 6723 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑏𝐴) → (𝐹𝑏) ∈ ℂ)
192189, 190, 191syl2anc 584 . . . . . . . . . . . . . . . . . . . . . 22 (((((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎𝐴) ∧ ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏𝐴) ∧ ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦)) → (𝐹𝑏) ∈ ℂ)
193185, 192subcld 10851 . . . . . . . . . . . . . . . . . . . . 21 (((((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎𝐴) ∧ ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏𝐴) ∧ ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦)) → (𝑅 − (𝐹𝑏)) ∈ ℂ)
194193abscld 14634 . . . . . . . . . . . . . . . . . . . 20 (((((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎𝐴) ∧ ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏𝐴) ∧ ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦)) → (abs‘(𝑅 − (𝐹𝑏))) ∈ ℝ)
195 simp-6r 784 . . . . . . . . . . . . . . . . . . . . . 22 (((((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎𝐴) ∧ ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏𝐴) ∧ ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦)) → 𝑥 ∈ ℂ)
196192, 195subcld 10851 . . . . . . . . . . . . . . . . . . . . 21 (((((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎𝐴) ∧ ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏𝐴) ∧ ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦)) → ((𝐹𝑏) − 𝑥) ∈ ℂ)
197196abscld 14634 . . . . . . . . . . . . . . . . . . . 20 (((((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎𝐴) ∧ ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏𝐴) ∧ ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦)) → (abs‘((𝐹𝑏) − 𝑥)) ∈ ℝ)
198194, 197readdcld 10523 . . . . . . . . . . . . . . . . . . 19 (((((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎𝐴) ∧ ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏𝐴) ∧ ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦)) → ((abs‘(𝑅 − (𝐹𝑏))) + (abs‘((𝐹𝑏) − 𝑥))) ∈ ℝ)
199 simp-4r 780 . . . . . . . . . . . . . . . . . . . . . 22 (((((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎𝐴) ∧ ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏𝐴) ∧ ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦)) → 𝑎𝐴)
20036ffvelrnda 6723 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑎𝐴) → (𝐹𝑎) ∈ ℂ)
201189, 199, 200syl2anc 584 . . . . . . . . . . . . . . . . . . . . 21 (((((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎𝐴) ∧ ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏𝐴) ∧ ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦)) → (𝐹𝑎) ∈ ℂ)
202195, 201subcld 10851 . . . . . . . . . . . . . . . . . . . 20 (((((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎𝐴) ∧ ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏𝐴) ∧ ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦)) → (𝑥 − (𝐹𝑎)) ∈ ℂ)
203202abscld 14634 . . . . . . . . . . . . . . . . . . 19 (((((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎𝐴) ∧ ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏𝐴) ∧ ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦)) → (abs‘(𝑥 − (𝐹𝑎))) ∈ ℝ)
204198, 203readdcld 10523 . . . . . . . . . . . . . . . . . 18 (((((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎𝐴) ∧ ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏𝐴) ∧ ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦)) → (((abs‘(𝑅 − (𝐹𝑏))) + (abs‘((𝐹𝑏) − 𝑥))) + (abs‘(𝑥 − (𝐹𝑎)))) ∈ ℝ)
205201, 186subcld 10851 . . . . . . . . . . . . . . . . . . 19 (((((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎𝐴) ∧ ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏𝐴) ∧ ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦)) → ((𝐹𝑎) − 𝐿) ∈ ℂ)
206205abscld 14634 . . . . . . . . . . . . . . . . . 18 (((((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎𝐴) ∧ ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏𝐴) ∧ ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦)) → (abs‘((𝐹𝑎) − 𝐿)) ∈ ℝ)
207204, 206readdcld 10523 . . . . . . . . . . . . . . . . 17 (((((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎𝐴) ∧ ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏𝐴) ∧ ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦)) → ((((abs‘(𝑅 − (𝐹𝑏))) + (abs‘((𝐹𝑏) − 𝑥))) + (abs‘(𝑥 − (𝐹𝑎)))) + (abs‘((𝐹𝑎) − 𝐿))) ∈ ℝ)
20815a1i 11 . . . . . . . . . . . . . . . . . 18 (((((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎𝐴) ∧ ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏𝐴) ∧ ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦)) → 4 ∈ ℝ)
209 rpre 12251 . . . . . . . . . . . . . . . . . . 19 (𝑦 ∈ ℝ+𝑦 ∈ ℝ)
210209ad5antlr 731 . . . . . . . . . . . . . . . . . 18 (((((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎𝐴) ∧ ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏𝐴) ∧ ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦)) → 𝑦 ∈ ℝ)
211208, 210remulcld 10524 . . . . . . . . . . . . . . . . 17 (((((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎𝐴) ∧ ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏𝐴) ∧ ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦)) → (4 · 𝑦) ∈ ℝ)
212185, 192, 195, 201, 186absnpncan3d 41136 . . . . . . . . . . . . . . . . 17 (((((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎𝐴) ∧ ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏𝐴) ∧ ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦)) → (abs‘(𝑅𝐿)) ≤ ((((abs‘(𝑅 − (𝐹𝑏))) + (abs‘((𝐹𝑏) − 𝑥))) + (abs‘(𝑥 − (𝐹𝑎)))) + (abs‘((𝐹𝑎) − 𝐿))))
213185, 192abssubd 14651 . . . . . . . . . . . . . . . . . . 19 (((((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎𝐴) ∧ ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏𝐴) ∧ ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦)) → (abs‘(𝑅 − (𝐹𝑏))) = (abs‘((𝐹𝑏) − 𝑅)))
214 simprr 769 . . . . . . . . . . . . . . . . . . 19 (((((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎𝐴) ∧ ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏𝐴) ∧ ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦)) → (abs‘((𝐹𝑏) − 𝑅)) < 𝑦)
215213, 214eqbrtrd 4990 . . . . . . . . . . . . . . . . . 18 (((((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎𝐴) ∧ ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏𝐴) ∧ ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦)) → (abs‘(𝑅 − (𝐹𝑏))) < 𝑦)
216 simprl 767 . . . . . . . . . . . . . . . . . 18 (((((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎𝐴) ∧ ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏𝐴) ∧ ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦)) → (abs‘((𝐹𝑏) − 𝑥)) < 𝑦)
217 simp-5r 782 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎𝐴) ∧ ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏𝐴) → 𝑥 ∈ ℂ)
218200ad5ant14 754 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎𝐴) ∧ ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)) → (𝐹𝑎) ∈ ℂ)
219218adantr 481 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎𝐴) ∧ ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏𝐴) → (𝐹𝑎) ∈ ℂ)
220217, 219abssubd 14651 . . . . . . . . . . . . . . . . . . . 20 ((((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎𝐴) ∧ ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏𝐴) → (abs‘(𝑥 − (𝐹𝑎))) = (abs‘((𝐹𝑎) − 𝑥)))
221 simplrl 773 . . . . . . . . . . . . . . . . . . . 20 ((((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎𝐴) ∧ ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏𝐴) → (abs‘((𝐹𝑎) − 𝑥)) < 𝑦)
222220, 221eqbrtrd 4990 . . . . . . . . . . . . . . . . . . 19 ((((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎𝐴) ∧ ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏𝐴) → (abs‘(𝑥 − (𝐹𝑎))) < 𝑦)
223222adantr 481 . . . . . . . . . . . . . . . . . 18 (((((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎𝐴) ∧ ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏𝐴) ∧ ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦)) → (abs‘(𝑥 − (𝐹𝑎))) < 𝑦)
224 simplrr 774 . . . . . . . . . . . . . . . . . . 19 ((((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎𝐴) ∧ ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏𝐴) → (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)
225224adantr 481 . . . . . . . . . . . . . . . . . 18 (((((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎𝐴) ∧ ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏𝐴) ∧ ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦)) → (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)
226194, 197, 203, 206, 210, 215, 216, 223, 225lt4addmuld 41135 . . . . . . . . . . . . . . . . 17 (((((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎𝐴) ∧ ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏𝐴) ∧ ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦)) → ((((abs‘(𝑅 − (𝐹𝑏))) + (abs‘((𝐹𝑏) − 𝑥))) + (abs‘(𝑥 − (𝐹𝑎)))) + (abs‘((𝐹𝑎) − 𝐿))) < (4 · 𝑦))
227188, 207, 211, 212, 226lelttrd 10651 . . . . . . . . . . . . . . . 16 (((((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎𝐴) ∧ ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏𝐴) ∧ ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦)) → (abs‘(𝑅𝐿)) < (4 · 𝑦))
228227ex 413 . . . . . . . . . . . . . . 15 ((((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎𝐴) ∧ ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏𝐴) → (((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦) → (abs‘(𝑅𝐿)) < (4 · 𝑦)))
229228adantl3r 746 . . . . . . . . . . . . . 14 (((((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ ∃𝑧 ∈ ℝ+𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ 𝑎𝐴) ∧ ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏𝐴) → (((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦) → (abs‘(𝑅𝐿)) < (4 · 𝑦)))
230229reximdva 3239 . . . . . . . . . . . . 13 ((((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ ∃𝑧 ∈ ℝ+𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ 𝑎𝐴) ∧ ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)) → (∃𝑏𝐴 ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦) → ∃𝑏𝐴 (abs‘(𝑅𝐿)) < (4 · 𝑦)))
231184, 230mpd 15 . . . . . . . . . . . 12 ((((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ ∃𝑧 ∈ ℝ+𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ 𝑎𝐴) ∧ ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)) → ∃𝑏𝐴 (abs‘(𝑅𝐿)) < (4 · 𝑦))
232 fresin 6422 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐹:𝐴⟶ℂ → (𝐹 ↾ (-∞(,)𝐵)):(𝐴 ∩ (-∞(,)𝐵))⟶ℂ)
23336, 232syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝐹 ↾ (-∞(,)𝐵)):(𝐴 ∩ (-∞(,)𝐵))⟶ℂ)
234 ioosscn 41332 . . . . . . . . . . . . . . . . . . . . . . . 24 (-∞(,)𝐵) ⊆ ℂ
23546, 234sstri 3904 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐴 ∩ (-∞(,)𝐵)) ⊆ ℂ
236235a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝐴 ∩ (-∞(,)𝐵)) ⊆ ℂ)
237233, 236, 56ellimc3 24164 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝐿 ∈ ((𝐹 ↾ (-∞(,)𝐵)) lim 𝐵) ↔ (𝐿 ∈ ℂ ∧ ∀𝑦 ∈ ℝ+𝑣 ∈ ℝ+𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦))))
2386, 237mpbid 233 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝐿 ∈ ℂ ∧ ∀𝑦 ∈ ℝ+𝑣 ∈ ℝ+𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)))
239238simprd 496 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ∀𝑦 ∈ ℝ+𝑣 ∈ ℝ+𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦))
240239r19.21bi 3177 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑦 ∈ ℝ+) → ∃𝑣 ∈ ℝ+𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦))
2412403ad2ant1 1126 . . . . . . . . . . . . . . . . 17 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) → ∃𝑣 ∈ ℝ+𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦))
242 simp11l 1277 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) → 𝜑)
243 simp12 1197 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) → 𝑧 ∈ ℝ+)
244 simp2 1130 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) → 𝑣 ∈ ℝ+)
245 breq2 4972 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑢 = if(𝑧𝑣, 𝑧, 𝑣) → ((abs‘(𝑎𝐵)) < 𝑢 ↔ (abs‘(𝑎𝐵)) < if(𝑧𝑣, 𝑧, 𝑣)))
246245rexbidv 3262 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑢 = if(𝑧𝑣, 𝑧, 𝑣) → (∃𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵})(abs‘(𝑎𝐵)) < 𝑢 ↔ ∃𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵})(abs‘(𝑎𝐵)) < if(𝑧𝑣, 𝑧, 𝑣)))
247 inss1 4131 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((limPt‘𝐾)‘(𝐴 ∩ (-∞(,)𝐵))) ∩ ℝ) ⊆ ((limPt‘𝐾)‘(𝐴 ∩ (-∞(,)𝐵)))
248247a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → (((limPt‘𝐾)‘(𝐴 ∩ (-∞(,)𝐵))) ∩ ℝ) ⊆ ((limPt‘𝐾)‘(𝐴 ∩ (-∞(,)𝐵))))
24948a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑 → (𝐴 ∩ (-∞(,)𝐵)) ⊆ ℝ)
25079, 81restlp 21479 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝐾 ∈ Top ∧ ℝ ⊆ ℂ ∧ (𝐴 ∩ (-∞(,)𝐵)) ⊆ ℝ) → ((limPt‘𝐽)‘(𝐴 ∩ (-∞(,)𝐵))) = (((limPt‘𝐾)‘(𝐴 ∩ (-∞(,)𝐵))) ∩ ℝ))
25171, 73, 249, 250syl3anc 1364 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → ((limPt‘𝐽)‘(𝐴 ∩ (-∞(,)𝐵))) = (((limPt‘𝐾)‘(𝐴 ∩ (-∞(,)𝐵))) ∩ ℝ))
25285fveq1i 6546 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((limPt‘(TopOpen‘ℂfld))‘(𝐴 ∩ (-∞(,)𝐵))) = ((limPt‘𝐾)‘(𝐴 ∩ (-∞(,)𝐵)))
253252a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → ((limPt‘(TopOpen‘ℂfld))‘(𝐴 ∩ (-∞(,)𝐵))) = ((limPt‘𝐾)‘(𝐴 ∩ (-∞(,)𝐵))))
254248, 251, 2533sstr4d 3941 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → ((limPt‘𝐽)‘(𝐴 ∩ (-∞(,)𝐵))) ⊆ ((limPt‘(TopOpen‘ℂfld))‘(𝐴 ∩ (-∞(,)𝐵))))
255254, 54sseldd 3896 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑𝐵 ∈ ((limPt‘(TopOpen‘ℂfld))‘(𝐴 ∩ (-∞(,)𝐵))))
256236, 56islpcn 41483 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → (𝐵 ∈ ((limPt‘(TopOpen‘ℂfld))‘(𝐴 ∩ (-∞(,)𝐵))) ↔ ∀𝑢 ∈ ℝ+𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵})(abs‘(𝑎𝐵)) < 𝑢))
257255, 256mpbid 233 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → ∀𝑢 ∈ ℝ+𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵})(abs‘(𝑎𝐵)) < 𝑢)
2582573ad2ant1 1126 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑧 ∈ ℝ+𝑣 ∈ ℝ+) → ∀𝑢 ∈ ℝ+𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵})(abs‘(𝑎𝐵)) < 𝑢)
259246, 258, 95rspcdva 3567 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑧 ∈ ℝ+𝑣 ∈ ℝ+) → ∃𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵})(abs‘(𝑎𝐵)) < if(𝑧𝑣, 𝑧, 𝑣))
260 eldifi 4030 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵}) → 𝑎 ∈ (𝐴 ∩ (-∞(,)𝐵)))
26148, 260sseldi 3893 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵}) → 𝑎 ∈ ℝ)
26273sselda 3895 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑𝑎 ∈ ℝ) → 𝑎 ∈ ℂ)
26356adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑𝑎 ∈ ℝ) → 𝐵 ∈ ℂ)
264262, 263subcld 10851 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑𝑎 ∈ ℝ) → (𝑎𝐵) ∈ ℂ)
265264abscld 14634 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑎 ∈ ℝ) → (abs‘(𝑎𝐵)) ∈ ℝ)
2662653ad2antl1 1178 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑𝑧 ∈ ℝ+𝑣 ∈ ℝ+) ∧ 𝑎 ∈ ℝ) → (abs‘(𝑎𝐵)) ∈ ℝ)
267266adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑𝑧 ∈ ℝ+𝑣 ∈ ℝ+) ∧ 𝑎 ∈ ℝ) ∧ (abs‘(𝑎𝐵)) < if(𝑧𝑣, 𝑧, 𝑣)) → (abs‘(𝑎𝐵)) ∈ ℝ)
268105ad2antrr 722 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑𝑧 ∈ ℝ+𝑣 ∈ ℝ+) ∧ 𝑎 ∈ ℝ) ∧ (abs‘(𝑎𝐵)) < if(𝑧𝑣, 𝑧, 𝑣)) → if(𝑧𝑣, 𝑧, 𝑣) ∈ ℝ)
269108ad2antrr 722 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑𝑧 ∈ ℝ+𝑣 ∈ ℝ+) ∧ 𝑎 ∈ ℝ) ∧ (abs‘(𝑎𝐵)) < if(𝑧𝑣, 𝑧, 𝑣)) → 𝑧 ∈ ℝ)
270 simpr 485 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑𝑧 ∈ ℝ+𝑣 ∈ ℝ+) ∧ 𝑎 ∈ ℝ) ∧ (abs‘(𝑎𝐵)) < if(𝑧𝑣, 𝑧, 𝑣)) → (abs‘(𝑎𝐵)) < if(𝑧𝑣, 𝑧, 𝑣))
271114ad2antrr 722 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑𝑧 ∈ ℝ+𝑣 ∈ ℝ+) ∧ 𝑎 ∈ ℝ) ∧ (abs‘(𝑎𝐵)) < if(𝑧𝑣, 𝑧, 𝑣)) → if(𝑧𝑣, 𝑧, 𝑣) ≤ 𝑧)
272267, 268, 269, 270, 271ltletrd 10653 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑𝑧 ∈ ℝ+𝑣 ∈ ℝ+) ∧ 𝑎 ∈ ℝ) ∧ (abs‘(𝑎𝐵)) < if(𝑧𝑣, 𝑧, 𝑣)) → (abs‘(𝑎𝐵)) < 𝑧)
273117ad2antrr 722 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑𝑧 ∈ ℝ+𝑣 ∈ ℝ+) ∧ 𝑎 ∈ ℝ) ∧ (abs‘(𝑎𝐵)) < if(𝑧𝑣, 𝑧, 𝑣)) → 𝑣 ∈ ℝ)
274 min2 12437 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑧 ∈ ℝ ∧ 𝑣 ∈ ℝ) → if(𝑧𝑣, 𝑧, 𝑣) ≤ 𝑣)
275107, 111, 274syl2an 595 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑧 ∈ ℝ+𝑣 ∈ ℝ+) → if(𝑧𝑣, 𝑧, 𝑣) ≤ 𝑣)
2762753adant1 1123 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑧 ∈ ℝ+𝑣 ∈ ℝ+) → if(𝑧𝑣, 𝑧, 𝑣) ≤ 𝑣)
277276ad2antrr 722 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑𝑧 ∈ ℝ+𝑣 ∈ ℝ+) ∧ 𝑎 ∈ ℝ) ∧ (abs‘(𝑎𝐵)) < if(𝑧𝑣, 𝑧, 𝑣)) → if(𝑧𝑣, 𝑧, 𝑣) ≤ 𝑣)
278267, 268, 273, 270, 277ltletrd 10653 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑𝑧 ∈ ℝ+𝑣 ∈ ℝ+) ∧ 𝑎 ∈ ℝ) ∧ (abs‘(𝑎𝐵)) < if(𝑧𝑣, 𝑧, 𝑣)) → (abs‘(𝑎𝐵)) < 𝑣)
279272, 278jca 512 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑧 ∈ ℝ+𝑣 ∈ ℝ+) ∧ 𝑎 ∈ ℝ) ∧ (abs‘(𝑎𝐵)) < if(𝑧𝑣, 𝑧, 𝑣)) → ((abs‘(𝑎𝐵)) < 𝑧 ∧ (abs‘(𝑎𝐵)) < 𝑣))
280279ex 413 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑧 ∈ ℝ+𝑣 ∈ ℝ+) ∧ 𝑎 ∈ ℝ) → ((abs‘(𝑎𝐵)) < if(𝑧𝑣, 𝑧, 𝑣) → ((abs‘(𝑎𝐵)) < 𝑧 ∧ (abs‘(𝑎𝐵)) < 𝑣)))
281261, 280sylan2 592 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑧 ∈ ℝ+𝑣 ∈ ℝ+) ∧ 𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵})) → ((abs‘(𝑎𝐵)) < if(𝑧𝑣, 𝑧, 𝑣) → ((abs‘(𝑎𝐵)) < 𝑧 ∧ (abs‘(𝑎𝐵)) < 𝑣)))
282281reximdva 3239 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑧 ∈ ℝ+𝑣 ∈ ℝ+) → (∃𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵})(abs‘(𝑎𝐵)) < if(𝑧𝑣, 𝑧, 𝑣) → ∃𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵})((abs‘(𝑎𝐵)) < 𝑧 ∧ (abs‘(𝑎𝐵)) < 𝑣)))
283259, 282mpd 15 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑧 ∈ ℝ+𝑣 ∈ ℝ+) → ∃𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵})((abs‘(𝑎𝐵)) < 𝑧 ∧ (abs‘(𝑎𝐵)) < 𝑣))
284242, 243, 244, 283syl3anc 1364 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) → ∃𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵})((abs‘(𝑎𝐵)) < 𝑧 ∧ (abs‘(𝑎𝐵)) < 𝑣))
285 nfv 1896 . . . . . . . . . . . . . . . . . . . . 21 𝑎(((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦))
286 nfre1 3271 . . . . . . . . . . . . . . . . . . . . 21 𝑎𝑎𝐴 ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)
287260elin1d 4102 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵}) → 𝑎𝐴)
2882873ad2ant2 1127 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) ∧ 𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵}) ∧ ((abs‘(𝑎𝐵)) < 𝑧 ∧ (abs‘(𝑎𝐵)) < 𝑣)) → 𝑎𝐴)
289 simp113 1297 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) ∧ 𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵}) ∧ ((abs‘(𝑎𝐵)) < 𝑧 ∧ (abs‘(𝑎𝐵)) < 𝑣)) → ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦))
290 eldifsni 4635 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵}) → 𝑎𝐵)
291290adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵}) ∧ ((abs‘(𝑎𝐵)) < 𝑧 ∧ (abs‘(𝑎𝐵)) < 𝑣)) → 𝑎𝐵)
292 simprl 767 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵}) ∧ ((abs‘(𝑎𝐵)) < 𝑧 ∧ (abs‘(𝑎𝐵)) < 𝑣)) → (abs‘(𝑎𝐵)) < 𝑧)
293291, 292jca 512 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵}) ∧ ((abs‘(𝑎𝐵)) < 𝑧 ∧ (abs‘(𝑎𝐵)) < 𝑣)) → (𝑎𝐵 ∧ (abs‘(𝑎𝐵)) < 𝑧))
2942933adant1 1123 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) ∧ 𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵}) ∧ ((abs‘(𝑎𝐵)) < 𝑧 ∧ (abs‘(𝑎𝐵)) < 𝑣)) → (𝑎𝐵 ∧ (abs‘(𝑎𝐵)) < 𝑧))
295 neeq1 3048 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑤 = 𝑎 → (𝑤𝐵𝑎𝐵))
296 fvoveq1 7046 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑤 = 𝑎 → (abs‘(𝑤𝐵)) = (abs‘(𝑎𝐵)))
297296breq1d 4978 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑤 = 𝑎 → ((abs‘(𝑤𝐵)) < 𝑧 ↔ (abs‘(𝑎𝐵)) < 𝑧))
298295, 297anbi12d 630 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑤 = 𝑎 → ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) ↔ (𝑎𝐵 ∧ (abs‘(𝑎𝐵)) < 𝑧)))
299298imbrov2fvoveq 7048 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑤 = 𝑎 → (((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦) ↔ ((𝑎𝐵 ∧ (abs‘(𝑎𝐵)) < 𝑧) → (abs‘((𝐹𝑎) − 𝑥)) < 𝑦)))
300299rspcva 3559 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑎𝐴 ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) → ((𝑎𝐵 ∧ (abs‘(𝑎𝐵)) < 𝑧) → (abs‘((𝐹𝑎) − 𝑥)) < 𝑦))
301300imp 407 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑎𝐴 ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ (𝑎𝐵 ∧ (abs‘(𝑎𝐵)) < 𝑧)) → (abs‘((𝐹𝑎) − 𝑥)) < 𝑦)
302288, 289, 294, 301syl21anc 834 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) ∧ 𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵}) ∧ ((abs‘(𝑎𝐵)) < 𝑧 ∧ (abs‘(𝑎𝐵)) < 𝑣)) → (abs‘((𝐹𝑎) − 𝑥)) < 𝑦)
3032603ad2ant2 1127 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) ∧ 𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵}) ∧ ((abs‘(𝑎𝐵)) < 𝑧 ∧ (abs‘(𝑎𝐵)) < 𝑣)) → 𝑎 ∈ (𝐴 ∩ (-∞(,)𝐵)))
3042423ad2ant1 1126 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) ∧ 𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵}) ∧ ((abs‘(𝑎𝐵)) < 𝑧 ∧ (abs‘(𝑎𝐵)) < 𝑣)) → 𝜑)
305 simp13 1198 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) ∧ 𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵}) ∧ ((abs‘(𝑎𝐵)) < 𝑧 ∧ (abs‘(𝑎𝐵)) < 𝑣)) → ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦))
306 nfra1 3188 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 𝑤𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)
307148, 306nfan 1885 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝑤(𝜑 ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦))
308 elinel2 4100 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵)) → 𝑤 ∈ (-∞(,)𝐵))
309308fvresd 6565 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵)) → ((𝐹 ↾ (-∞(,)𝐵))‘𝑤) = (𝐹𝑤))
310309eqcomd 2803 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵)) → (𝐹𝑤) = ((𝐹 ↾ (-∞(,)𝐵))‘𝑤))
311310fvoveq1d 7045 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵)) → (abs‘((𝐹𝑤) − 𝐿)) = (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)))
3123113ad2ant2 1127 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑 ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) ∧ 𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵)) ∧ (𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣)) → (abs‘((𝐹𝑤) − 𝐿)) = (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)))
313 rspa 3175 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦) ∧ 𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))) → ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦))
3143133impia 1110 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦) ∧ 𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵)) ∧ (𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣)) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)
3153143adant1l 1169 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑 ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) ∧ 𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵)) ∧ (𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣)) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)
316312, 315eqbrtrd 4990 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑 ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) ∧ 𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵)) ∧ (𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣)) → (abs‘((𝐹𝑤) − 𝐿)) < 𝑦)
3173163exp 1112 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑 ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) → (𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵)) → ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘((𝐹𝑤) − 𝐿)) < 𝑦)))
318307, 317ralrimi 3185 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) → ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘((𝐹𝑤) − 𝐿)) < 𝑦))
319304, 305, 318syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) ∧ 𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵}) ∧ ((abs‘(𝑎𝐵)) < 𝑧 ∧ (abs‘(𝑎𝐵)) < 𝑣)) → ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘((𝐹𝑤) − 𝐿)) < 𝑦))
320290anim1i 614 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵}) ∧ (abs‘(𝑎𝐵)) < 𝑣) → (𝑎𝐵 ∧ (abs‘(𝑎𝐵)) < 𝑣))
321320adantrl 712 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵}) ∧ ((abs‘(𝑎𝐵)) < 𝑧 ∧ (abs‘(𝑎𝐵)) < 𝑣)) → (𝑎𝐵 ∧ (abs‘(𝑎𝐵)) < 𝑣))
3223213adant1 1123 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) ∧ 𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵}) ∧ ((abs‘(𝑎𝐵)) < 𝑧 ∧ (abs‘(𝑎𝐵)) < 𝑣)) → (𝑎𝐵 ∧ (abs‘(𝑎𝐵)) < 𝑣))
323296breq1d 4978 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑤 = 𝑎 → ((abs‘(𝑤𝐵)) < 𝑣 ↔ (abs‘(𝑎𝐵)) < 𝑣))
324295, 323anbi12d 630 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑤 = 𝑎 → ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) ↔ (𝑎𝐵 ∧ (abs‘(𝑎𝐵)) < 𝑣)))
325324imbrov2fvoveq 7048 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑤 = 𝑎 → (((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘((𝐹𝑤) − 𝐿)) < 𝑦) ↔ ((𝑎𝐵 ∧ (abs‘(𝑎𝐵)) < 𝑣) → (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)))
326325rspcva 3559 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑎 ∈ (𝐴 ∩ (-∞(,)𝐵)) ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘((𝐹𝑤) − 𝐿)) < 𝑦)) → ((𝑎𝐵 ∧ (abs‘(𝑎𝐵)) < 𝑣) → (abs‘((𝐹𝑎) − 𝐿)) < 𝑦))
327326imp 407 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑎 ∈ (𝐴 ∩ (-∞(,)𝐵)) ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘((𝐹𝑤) − 𝐿)) < 𝑦)) ∧ (𝑎𝐵 ∧ (abs‘(𝑎𝐵)) < 𝑣)) → (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)
328303, 319, 322, 327syl21anc 834 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) ∧ 𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵}) ∧ ((abs‘(𝑎𝐵)) < 𝑧 ∧ (abs‘(𝑎𝐵)) < 𝑣)) → (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)
329 rspe 3269 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑎𝐴 ∧ ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)) → ∃𝑎𝐴 ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦))
330288, 302, 328, 329syl12anc 833 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) ∧ 𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵}) ∧ ((abs‘(𝑎𝐵)) < 𝑧 ∧ (abs‘(𝑎𝐵)) < 𝑣)) → ∃𝑎𝐴 ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦))
3313303exp 1112 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) → (𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵}) → (((abs‘(𝑎𝐵)) < 𝑧 ∧ (abs‘(𝑎𝐵)) < 𝑣) → ∃𝑎𝐴 ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦))))
332285, 286, 331rexlimd 3280 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) → (∃𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵})((abs‘(𝑎𝐵)) < 𝑧 ∧ (abs‘(𝑎𝐵)) < 𝑣) → ∃𝑎𝐴 ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)))
333284, 332mpd 15 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) → ∃𝑎𝐴 ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦))
3343333exp 1112 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) → (𝑣 ∈ ℝ+ → (∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦) → ∃𝑎𝐴 ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦))))
335334rexlimdv 3248 . . . . . . . . . . . . . . . . 17 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) → (∃𝑣 ∈ ℝ+𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦) → ∃𝑎𝐴 ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)))
336241, 335mpd 15 . . . . . . . . . . . . . . . 16 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) → ∃𝑎𝐴 ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦))
3373363exp 1112 . . . . . . . . . . . . . . 15 ((𝜑𝑦 ∈ ℝ+) → (𝑧 ∈ ℝ+ → (∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦) → ∃𝑎𝐴 ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦))))
338337rexlimdv 3248 . . . . . . . . . . . . . 14 ((𝜑𝑦 ∈ ℝ+) → (∃𝑧 ∈ ℝ+𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦) → ∃𝑎𝐴 ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)))
339338imp 407 . . . . . . . . . . . . 13 (((𝜑𝑦 ∈ ℝ+) ∧ ∃𝑧 ∈ ℝ+𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) → ∃𝑎𝐴 ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦))
340339adantllr 715 . . . . . . . . . . . 12 ((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ ∃𝑧 ∈ ℝ+𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) → ∃𝑎𝐴 ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦))
341231, 340reximddv3 40980 . . . . . . . . . . 11 ((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ ∃𝑧 ∈ ℝ+𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) → ∃𝑎𝐴𝑏𝐴 (abs‘(𝑅𝐿)) < (4 · 𝑦))
34232, 33, 35, 341syl21anc 834 . . . . . . . . . 10 ((((𝜑𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ 𝑦 ∈ ℝ+) → ∃𝑎𝐴𝑏𝐴 (abs‘(𝑅𝐿)) < (4 · 𝑦))
343342ex 413 . . . . . . . . 9 (((𝜑𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) → (𝑦 ∈ ℝ+ → ∃𝑎𝐴𝑏𝐴 (abs‘(𝑅𝐿)) < (4 · 𝑦)))
34424, 25, 31, 343vtoclf 3504 . . . . . . . 8 (((𝜑𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) → (((abs‘(𝑅𝐿)) / 4) ∈ ℝ+ → ∃𝑎𝐴𝑏𝐴 (abs‘(𝑅𝐿)) < (4 · ((abs‘(𝑅𝐿)) / 4))))
34519, 344mpd 15 . . . . . . 7 (((𝜑𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) → ∃𝑎𝐴𝑏𝐴 (abs‘(𝑅𝐿)) < (4 · ((abs‘(𝑅𝐿)) / 4)))
346 simpr 485 . . . . . . . . . . . 12 ((𝜑 ∧ (abs‘(𝑅𝐿)) < (4 · ((abs‘(𝑅𝐿)) / 4))) → (abs‘(𝑅𝐿)) < (4 · ((abs‘(𝑅𝐿)) / 4)))
347 abssubrp 41103 . . . . . . . . . . . . . . . 16 ((𝑅 ∈ ℂ ∧ 𝐿 ∈ ℂ ∧ 𝑅𝐿) → (abs‘(𝑅𝐿)) ∈ ℝ+)
3483, 7, 11, 347syl3anc 1364 . . . . . . . . . . . . . . 15 (𝜑 → (abs‘(𝑅𝐿)) ∈ ℝ+)
349348rpcnd 12287 . . . . . . . . . . . . . 14 (𝜑 → (abs‘(𝑅𝐿)) ∈ ℂ)
350349adantr 481 . . . . . . . . . . . . 13 ((𝜑 ∧ (abs‘(𝑅𝐿)) < (4 · ((abs‘(𝑅𝐿)) / 4))) → (abs‘(𝑅𝐿)) ∈ ℂ)
351 4cn 11576 . . . . . . . . . . . . . 14 4 ∈ ℂ
352351a1i 11 . . . . . . . . . . . . 13 ((𝜑 ∧ (abs‘(𝑅𝐿)) < (4 · ((abs‘(𝑅𝐿)) / 4))) → 4 ∈ ℂ)
353 4ne0 11599 . . . . . . . . . . . . . 14 4 ≠ 0
354353a1i 11 . . . . . . . . . . . . 13 ((𝜑 ∧ (abs‘(𝑅𝐿)) < (4 · ((abs‘(𝑅𝐿)) / 4))) → 4 ≠ 0)
355350, 352, 354divcan2d 11272 . . . . . . . . . . . 12 ((𝜑 ∧ (abs‘(𝑅𝐿)) < (4 · ((abs‘(𝑅𝐿)) / 4))) → (4 · ((abs‘(𝑅𝐿)) / 4)) = (abs‘(𝑅𝐿)))
356346, 355breqtrd 4994 . . . . . . . . . . 11 ((𝜑 ∧ (abs‘(𝑅𝐿)) < (4 · ((abs‘(𝑅𝐿)) / 4))) → (abs‘(𝑅𝐿)) < (abs‘(𝑅𝐿)))
357356ex 413 . . . . . . . . . 10 (𝜑 → ((abs‘(𝑅𝐿)) < (4 · ((abs‘(𝑅𝐿)) / 4)) → (abs‘(𝑅𝐿)) < (abs‘(𝑅𝐿))))
358357a1d 25 . . . . . . . . 9 (𝜑 → ((𝑎𝐴𝑏𝐴) → ((abs‘(𝑅𝐿)) < (4 · ((abs‘(𝑅𝐿)) / 4)) → (abs‘(𝑅𝐿)) < (abs‘(𝑅𝐿)))))
359358ad2antrr 722 . . . . . . . 8 (((𝜑𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) → ((𝑎𝐴𝑏𝐴) → ((abs‘(𝑅𝐿)) < (4 · ((abs‘(𝑅𝐿)) / 4)) → (abs‘(𝑅𝐿)) < (abs‘(𝑅𝐿)))))
360359rexlimdvv 3258 . . . . . . 7 (((𝜑𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) → (∃𝑎𝐴𝑏𝐴 (abs‘(𝑅𝐿)) < (4 · ((abs‘(𝑅𝐿)) / 4)) → (abs‘(𝑅𝐿)) < (abs‘(𝑅𝐿))))
361345, 360mpd 15 . . . . . 6 (((𝜑𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) → (abs‘(𝑅𝐿)) < (abs‘(𝑅𝐿)))
3629abscld 14634 . . . . . . 7 (((𝜑𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) → (abs‘(𝑅𝐿)) ∈ ℝ)
363362ltnrd 10627 . . . . . 6 (((𝜑𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) → ¬ (abs‘(𝑅𝐿)) < (abs‘(𝑅𝐿)))
364361, 363pm2.65da 813 . . . . 5 ((𝜑𝑥 ∈ ℂ) → ¬ ∀𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦))
365364ex 413 . . . 4 (𝜑 → (𝑥 ∈ ℂ → ¬ ∀𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)))
366 imnan 400 . . . 4 ((𝑥 ∈ ℂ → ¬ ∀𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ↔ ¬ (𝑥 ∈ ℂ ∧ ∀𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)))
367365, 366sylib 219 . . 3 (𝜑 → ¬ (𝑥 ∈ ℂ ∧ ∀𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)))
368 limclner.a . . . . 5 (𝜑𝐴 ⊆ ℝ)
369368, 73sstrd 3905 . . . 4 (𝜑𝐴 ⊆ ℂ)
37036, 369, 56ellimc3 24164 . . 3 (𝜑 → (𝑥 ∈ (𝐹 lim 𝐵) ↔ (𝑥 ∈ ℂ ∧ ∀𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦))))
371367, 370mtbird 326 . 2 (𝜑 → ¬ 𝑥 ∈ (𝐹 lim 𝐵))
372371eq0rdv 4283 1 (𝜑 → (𝐹 lim 𝐵) = ∅)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 396  w3a 1080   = wceq 1525  wcel 2083  wne 2986  wral 3107  wrex 3108  cdif 3862  cin 3864  wss 3865  c0 4217  ifcif 4387  {csn 4478   cuni 4751   class class class wbr 4968  ran crn 5451  cres 5452  wf 6228  cfv 6232  (class class class)co 7023  cc 10388  cr 10389  0cc0 10390   + caddc 10393   · cmul 10395  +∞cpnf 10525  -∞cmnf 10526   < clt 10528  cle 10529  cmin 10723   / cdiv 11151  4c4 11548  +crp 12243  (,)cioo 12592  abscabs 14431  t crest 16527  TopOpenctopn 16528  topGenctg 16544  fldccnfld 20231  Topctop 21189  limPtclp 21430   lim climc 24147
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1781  ax-4 1795  ax-5 1892  ax-6 1951  ax-7 1996  ax-8 2085  ax-9 2093  ax-10 2114  ax-11 2128  ax-12 2143  ax-13 2346  ax-ext 2771  ax-rep 5088  ax-sep 5101  ax-nul 5108  ax-pow 5164  ax-pr 5228  ax-un 7326  ax-cnex 10446  ax-resscn 10447  ax-1cn 10448  ax-icn 10449  ax-addcl 10450  ax-addrcl 10451  ax-mulcl 10452  ax-mulrcl 10453  ax-mulcom 10454  ax-addass 10455  ax-mulass 10456  ax-distr 10457  ax-i2m1 10458  ax-1ne0 10459  ax-1rid 10460  ax-rnegex 10461  ax-rrecex 10462  ax-cnre 10463  ax-pre-lttri 10464  ax-pre-lttrn 10465  ax-pre-ltadd 10466  ax-pre-mulgt0 10467  ax-pre-sup 10468
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3or 1081  df-3an 1082  df-tru 1528  df-ex 1766  df-nf 1770  df-sb 2045  df-mo 2578  df-eu 2614  df-clab 2778  df-cleq 2790  df-clel 2865  df-nfc 2937  df-ne 2987  df-nel 3093  df-ral 3112  df-rex 3113  df-reu 3114  df-rmo 3115  df-rab 3116  df-v 3442  df-sbc 3712  df-csb 3818  df-dif 3868  df-un 3870  df-in 3872  df-ss 3880  df-pss 3882  df-nul 4218  df-if 4388  df-pw 4461  df-sn 4479  df-pr 4481  df-tp 4483  df-op 4485  df-uni 4752  df-int 4789  df-iun 4833  df-iin 4834  df-br 4969  df-opab 5031  df-mpt 5048  df-tr 5071  df-id 5355  df-eprel 5360  df-po 5369  df-so 5370  df-fr 5409  df-we 5411  df-xp 5456  df-rel 5457  df-cnv 5458  df-co 5459  df-dm 5460  df-rn 5461  df-res 5462  df-ima 5463  df-pred 6030  df-ord 6076  df-on 6077  df-lim 6078  df-suc 6079  df-iota 6196  df-fun 6234  df-fn 6235  df-f 6236  df-f1 6237  df-fo 6238  df-f1o 6239  df-fv 6240  df-riota 6984  df-ov 7026  df-oprab 7027  df-mpo 7028  df-om 7444  df-1st 7552  df-2nd 7553  df-wrecs 7805  df-recs 7867  df-rdg 7905  df-1o 7960  df-oadd 7964  df-er 8146  df-map 8265  df-pm 8266  df-en 8365  df-dom 8366  df-sdom 8367  df-fin 8368  df-fi 8728  df-sup 8759  df-inf 8760  df-pnf 10530  df-mnf 10531  df-xr 10532  df-ltxr 10533  df-le 10534  df-sub 10725  df-neg 10726  df-div 11152  df-nn 11493  df-2 11554  df-3 11555  df-4 11556  df-5 11557  df-6 11558  df-7 11559  df-8 11560  df-9 11561  df-n0 11752  df-z 11836  df-dec 11953  df-uz 12098  df-q 12202  df-rp 12244  df-xneg 12361  df-xadd 12362  df-xmul 12363  df-ioo 12596  df-fz 12747  df-seq 13224  df-exp 13284  df-cj 14296  df-re 14297  df-im 14298  df-sqrt 14432  df-abs 14433  df-struct 16318  df-ndx 16319  df-slot 16320  df-base 16322  df-plusg 16411  df-mulr 16412  df-starv 16413  df-tset 16417  df-ple 16418  df-ds 16420  df-unif 16421  df-rest 16529  df-topn 16530  df-topgen 16550  df-psmet 20223  df-xmet 20224  df-met 20225  df-bl 20226  df-mopn 20227  df-cnfld 20232  df-top 21190  df-topon 21207  df-topsp 21229  df-bases 21242  df-cld 21315  df-ntr 21316  df-cls 21317  df-nei 21394  df-lp 21432  df-cnp 21524  df-xms 22617  df-ms 22618  df-limc 24151
This theorem is referenced by:  limclr  41499  jumpncnp  41744
  Copyright terms: Public domain W3C validator