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

Theorem limclner 42308
 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 24485 . . . . . . . . . . . . 13 ((𝐹 ↾ (𝐵(,)+∞)) lim 𝐵) ⊆ ℂ
2 limclner.r . . . . . . . . . . . . 13 (𝜑𝑅 ∈ ((𝐹 ↾ (𝐵(,)+∞)) lim 𝐵))
31, 2sseldi 3913 . . . . . . . . . . . 12 (𝜑𝑅 ∈ ℂ)
43ad2antrr 725 . . . . . . . . . . 11 (((𝜑𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) → 𝑅 ∈ ℂ)
5 limccl 24485 . . . . . . . . . . . . 13 ((𝐹 ↾ (-∞(,)𝐵)) lim 𝐵) ⊆ ℂ
6 limclner.l . . . . . . . . . . . . 13 (𝜑𝐿 ∈ ((𝐹 ↾ (-∞(,)𝐵)) lim 𝐵))
75, 6sseldi 3913 . . . . . . . . . . . 12 (𝜑𝐿 ∈ ℂ)
87ad2antrr 725 . . . . . . . . . . 11 (((𝜑𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) → 𝐿 ∈ ℂ)
94, 8subcld 10988 . . . . . . . . . 10 (((𝜑𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) → (𝑅𝐿) ∈ ℂ)
10 limclner.lner . . . . . . . . . . . . 13 (𝜑𝐿𝑅)
1110necomd 3042 . . . . . . . . . . . 12 (𝜑𝑅𝐿)
1211ad2antrr 725 . . . . . . . . . . 11 (((𝜑𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) → 𝑅𝐿)
134, 8, 12subne0d 10997 . . . . . . . . . 10 (((𝜑𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) → (𝑅𝐿) ≠ 0)
149, 13absrpcld 14802 . . . . . . . . 9 (((𝜑𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) → (abs‘(𝑅𝐿)) ∈ ℝ+)
15 4re 11711 . . . . . . . . . . 11 4 ∈ ℝ
16 4pos 11734 . . . . . . . . . . 11 0 < 4
1715, 16elrpii 12382 . . . . . . . . . 10 4 ∈ ℝ+
1817a1i 11 . . . . . . . . 9 (((𝜑𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) → 4 ∈ ℝ+)
1914, 18rpdivcld 12438 . . . . . . . 8 (((𝜑𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) → ((abs‘(𝑅𝐿)) / 4) ∈ ℝ+)
20 nfv 1915 . . . . . . . . . . 11 𝑦(𝜑𝑥 ∈ ℂ)
21 nfra1 3183 . . . . . . . . . . 11 𝑦𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)
2220, 21nfan 1900 . . . . . . . . . 10 𝑦((𝜑𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦))
23 nfv 1915 . . . . . . . . . 10 𝑦(((abs‘(𝑅𝐿)) / 4) ∈ ℝ+ → ∃𝑎𝐴𝑏𝐴 (abs‘(𝑅𝐿)) < (4 · ((abs‘(𝑅𝐿)) / 4)))
2422, 23nfim 1897 . . . . . . . . 9 𝑦(((𝜑𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) → (((abs‘(𝑅𝐿)) / 4) ∈ ℝ+ → ∃𝑎𝐴𝑏𝐴 (abs‘(𝑅𝐿)) < (4 · ((abs‘(𝑅𝐿)) / 4))))
25 ovex 7168 . . . . . . . . 9 ((abs‘(𝑅𝐿)) / 4) ∈ V
26 eleq1 2877 . . . . . . . . . . 11 (𝑦 = ((abs‘(𝑅𝐿)) / 4) → (𝑦 ∈ ℝ+ ↔ ((abs‘(𝑅𝐿)) / 4) ∈ ℝ+))
27 oveq2 7143 . . . . . . . . . . . . 13 (𝑦 = ((abs‘(𝑅𝐿)) / 4) → (4 · 𝑦) = (4 · ((abs‘(𝑅𝐿)) / 4)))
2827breq2d 5042 . . . . . . . . . . . 12 (𝑦 = ((abs‘(𝑅𝐿)) / 4) → ((abs‘(𝑅𝐿)) < (4 · 𝑦) ↔ (abs‘(𝑅𝐿)) < (4 · ((abs‘(𝑅𝐿)) / 4))))
29282rexbidv 3259 . . . . . . . . . . 11 (𝑦 = ((abs‘(𝑅𝐿)) / 4) → (∃𝑎𝐴𝑏𝐴 (abs‘(𝑅𝐿)) < (4 · 𝑦) ↔ ∃𝑎𝐴𝑏𝐴 (abs‘(𝑅𝐿)) < (4 · ((abs‘(𝑅𝐿)) / 4))))
3026, 29imbi12d 348 . . . . . . . . . 10 (𝑦 = ((abs‘(𝑅𝐿)) / 4) → ((𝑦 ∈ ℝ+ → ∃𝑎𝐴𝑏𝐴 (abs‘(𝑅𝐿)) < (4 · 𝑦)) ↔ (((abs‘(𝑅𝐿)) / 4) ∈ ℝ+ → ∃𝑎𝐴𝑏𝐴 (abs‘(𝑅𝐿)) < (4 · ((abs‘(𝑅𝐿)) / 4)))))
3130imbi2d 344 . . . . . . . . 9 (𝑦 = ((abs‘(𝑅𝐿)) / 4) → ((((𝜑𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) → (𝑦 ∈ ℝ+ → ∃𝑎𝐴𝑏𝐴 (abs‘(𝑅𝐿)) < (4 · 𝑦))) ↔ (((𝜑𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) → (((abs‘(𝑅𝐿)) / 4) ∈ ℝ+ → ∃𝑎𝐴𝑏𝐴 (abs‘(𝑅𝐿)) < (4 · ((abs‘(𝑅𝐿)) / 4))))))
32 simpll 766 . . . . . . . . . . 11 ((((𝜑𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ 𝑦 ∈ ℝ+) → (𝜑𝑥 ∈ ℂ))
33 simpr 488 . . . . . . . . . . 11 ((((𝜑𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ 𝑦 ∈ ℝ+) → 𝑦 ∈ ℝ+)
34 rspa 3171 . . . . . . . . . . . 12 ((∀𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦) ∧ 𝑦 ∈ ℝ+) → ∃𝑧 ∈ ℝ+𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦))
3534adantll 713 . . . . . . . . . . 11 ((((𝜑𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ 𝑦 ∈ ℝ+) → ∃𝑧 ∈ ℝ+𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦))
36 limclner.f . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑𝐹:𝐴⟶ℂ)
37 fresin 6521 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝐹:𝐴⟶ℂ → (𝐹 ↾ (𝐵(,)+∞)):(𝐴 ∩ (𝐵(,)+∞))⟶ℂ)
3836, 37syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (𝐹 ↾ (𝐵(,)+∞)):(𝐴 ∩ (𝐵(,)+∞))⟶ℂ)
39 inss2 4156 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝐴 ∩ (𝐵(,)+∞)) ⊆ (𝐵(,)+∞)
40 ioosscn 12789 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝐵(,)+∞) ⊆ ℂ
4139, 40sstri 3924 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝐴 ∩ (𝐵(,)+∞)) ⊆ ℂ
4241a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (𝐴 ∩ (𝐵(,)+∞)) ⊆ ℂ)
43 limclner.j . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 𝐽 = (topGen‘ran (,))
44 retop 23374 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (topGen‘ran (,)) ∈ Top
4543, 44eqeltri 2886 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 𝐽 ∈ Top
46 inss2 4156 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝐴 ∩ (-∞(,)𝐵)) ⊆ (-∞(,)𝐵)
47 ioossre 12788 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (-∞(,)𝐵) ⊆ ℝ
4846, 47sstri 3924 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝐴 ∩ (-∞(,)𝐵)) ⊆ ℝ
49 uniretop 23375 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ℝ = (topGen‘ran (,))
5043unieqi 4813 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 𝐽 = (topGen‘ran (,))
5149, 50eqtr4i 2824 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ℝ = 𝐽
5251lpss 21754 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝐽 ∈ Top ∧ (𝐴 ∩ (-∞(,)𝐵)) ⊆ ℝ) → ((limPt‘𝐽)‘(𝐴 ∩ (-∞(,)𝐵))) ⊆ ℝ)
5345, 48, 52mp2an 691 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((limPt‘𝐽)‘(𝐴 ∩ (-∞(,)𝐵))) ⊆ ℝ
54 limclner.blp1 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑𝐵 ∈ ((limPt‘𝐽)‘(𝐴 ∩ (-∞(,)𝐵))))
5553, 54sseldi 3913 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑𝐵 ∈ ℝ)
5655recnd 10660 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑𝐵 ∈ ℂ)
5738, 42, 56ellimc3 24489 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (𝑅 ∈ ((𝐹 ↾ (𝐵(,)+∞)) lim 𝐵) ↔ (𝑅 ∈ ℂ ∧ ∀𝑦 ∈ ℝ+𝑣 ∈ ℝ+𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦))))
582, 57mpbid 235 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝑅 ∈ ℂ ∧ ∀𝑦 ∈ ℝ+𝑣 ∈ ℝ+𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)))
5958simprd 499 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ∀𝑦 ∈ ℝ+𝑣 ∈ ℝ+𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦))
6059r19.21bi 3173 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑦 ∈ ℝ+) → ∃𝑣 ∈ ℝ+𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦))
61603ad2ant1 1130 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) → ∃𝑣 ∈ ℝ+𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦))
62 simp11l 1281 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) → 𝜑)
63 simp12 1201 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) → 𝑧 ∈ ℝ+)
64 simp2 1134 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) → 𝑣 ∈ ℝ+)
65 breq2 5034 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑢 = if(𝑧𝑣, 𝑧, 𝑣) → ((abs‘(𝑏𝐵)) < 𝑢 ↔ (abs‘(𝑏𝐵)) < if(𝑧𝑣, 𝑧, 𝑣)))
6665rexbidv 3256 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑢 = if(𝑧𝑣, 𝑧, 𝑣) → (∃𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵})(abs‘(𝑏𝐵)) < 𝑢 ↔ ∃𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵})(abs‘(𝑏𝐵)) < if(𝑧𝑣, 𝑧, 𝑣)))
67 inss1 4155 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((limPt‘𝐾)‘(𝐴 ∩ (𝐵(,)+∞))) ∩ ℝ) ⊆ ((limPt‘𝐾)‘(𝐴 ∩ (𝐵(,)+∞)))
6867a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝜑 → (((limPt‘𝐾)‘(𝐴 ∩ (𝐵(,)+∞))) ∩ ℝ) ⊆ ((limPt‘𝐾)‘(𝐴 ∩ (𝐵(,)+∞))))
69 limclner.k . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 𝐾 = (TopOpen‘ℂfld)
7069cnfldtop 23396 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 𝐾 ∈ Top
7170a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝜑𝐾 ∈ Top)
72 ax-resscn 10585 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ℝ ⊆ ℂ
7372a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝜑 → ℝ ⊆ ℂ)
74 ioossre 12788 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝐵(,)+∞) ⊆ ℝ
7539, 74sstri 3924 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝐴 ∩ (𝐵(,)+∞)) ⊆ ℝ
7675a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝜑 → (𝐴 ∩ (𝐵(,)+∞)) ⊆ ℝ)
77 unicntop 23398 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ℂ = (TopOpen‘ℂfld)
7869unieqi 4813 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 𝐾 = (TopOpen‘ℂfld)
7977, 78eqtr4i 2824 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ℂ = 𝐾
8069tgioo2 23415 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (topGen‘ran (,)) = (𝐾t ℝ)
8143, 80eqtri 2821 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 𝐽 = (𝐾t ℝ)
8279, 81restlp 21795 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝐾 ∈ Top ∧ ℝ ⊆ ℂ ∧ (𝐴 ∩ (𝐵(,)+∞)) ⊆ ℝ) → ((limPt‘𝐽)‘(𝐴 ∩ (𝐵(,)+∞))) = (((limPt‘𝐾)‘(𝐴 ∩ (𝐵(,)+∞))) ∩ ℝ))
8371, 73, 76, 82syl3anc 1368 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝜑 → ((limPt‘𝐽)‘(𝐴 ∩ (𝐵(,)+∞))) = (((limPt‘𝐾)‘(𝐴 ∩ (𝐵(,)+∞))) ∩ ℝ))
8469eqcomi 2807 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (TopOpen‘ℂfld) = 𝐾
8584fveq2i 6648 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (limPt‘(TopOpen‘ℂfld)) = (limPt‘𝐾)
8685fveq1i 6646 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((limPt‘(TopOpen‘ℂfld))‘(𝐴 ∩ (𝐵(,)+∞))) = ((limPt‘𝐾)‘(𝐴 ∩ (𝐵(,)+∞)))
8786a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝜑 → ((limPt‘(TopOpen‘ℂfld))‘(𝐴 ∩ (𝐵(,)+∞))) = ((limPt‘𝐾)‘(𝐴 ∩ (𝐵(,)+∞))))
8868, 83, 873sstr4d 3962 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑 → ((limPt‘𝐽)‘(𝐴 ∩ (𝐵(,)+∞))) ⊆ ((limPt‘(TopOpen‘ℂfld))‘(𝐴 ∩ (𝐵(,)+∞))))
89 limclner.blp2 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑𝐵 ∈ ((limPt‘𝐽)‘(𝐴 ∩ (𝐵(,)+∞))))
9088, 89sseldd 3916 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑𝐵 ∈ ((limPt‘(TopOpen‘ℂfld))‘(𝐴 ∩ (𝐵(,)+∞))))
9142, 56islpcn 42296 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → (𝐵 ∈ ((limPt‘(TopOpen‘ℂfld))‘(𝐴 ∩ (𝐵(,)+∞))) ↔ ∀𝑢 ∈ ℝ+𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵})(abs‘(𝑏𝐵)) < 𝑢))
9290, 91mpbid 235 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → ∀𝑢 ∈ ℝ+𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵})(abs‘(𝑏𝐵)) < 𝑢)
93923ad2ant1 1130 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑧 ∈ ℝ+𝑣 ∈ ℝ+) → ∀𝑢 ∈ ℝ+𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵})(abs‘(𝑏𝐵)) < 𝑢)
94 ifcl 4469 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑧 ∈ ℝ+𝑣 ∈ ℝ+) → if(𝑧𝑣, 𝑧, 𝑣) ∈ ℝ+)
95943adant1 1127 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑧 ∈ ℝ+𝑣 ∈ ℝ+) → if(𝑧𝑣, 𝑧, 𝑣) ∈ ℝ+)
9666, 93, 95rspcdva 3573 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑧 ∈ ℝ+𝑣 ∈ ℝ+) → ∃𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵})(abs‘(𝑏𝐵)) < if(𝑧𝑣, 𝑧, 𝑣))
97 eldifi 4054 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵}) → 𝑏 ∈ (𝐴 ∩ (𝐵(,)+∞)))
9875, 97sseldi 3913 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵}) → 𝑏 ∈ ℝ)
9973sselda 3915 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝜑𝑏 ∈ ℝ) → 𝑏 ∈ ℂ)
10056adantr 484 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝜑𝑏 ∈ ℝ) → 𝐵 ∈ ℂ)
10199, 100subcld 10988 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑𝑏 ∈ ℝ) → (𝑏𝐵) ∈ ℂ)
102101abscld 14790 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑𝑏 ∈ ℝ) → (abs‘(𝑏𝐵)) ∈ ℝ)
1031023ad2antl1 1182 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝜑𝑧 ∈ ℝ+𝑣 ∈ ℝ+) ∧ 𝑏 ∈ ℝ) → (abs‘(𝑏𝐵)) ∈ ℝ)
104103adantr 484 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑𝑧 ∈ ℝ+𝑣 ∈ ℝ+) ∧ 𝑏 ∈ ℝ) ∧ (abs‘(𝑏𝐵)) < if(𝑧𝑣, 𝑧, 𝑣)) → (abs‘(𝑏𝐵)) ∈ ℝ)
10595rpred 12421 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑𝑧 ∈ ℝ+𝑣 ∈ ℝ+) → if(𝑧𝑣, 𝑧, 𝑣) ∈ ℝ)
106105ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑𝑧 ∈ ℝ+𝑣 ∈ ℝ+) ∧ 𝑏 ∈ ℝ) ∧ (abs‘(𝑏𝐵)) < if(𝑧𝑣, 𝑧, 𝑣)) → if(𝑧𝑣, 𝑧, 𝑣) ∈ ℝ)
107 rpre 12387 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑧 ∈ ℝ+𝑧 ∈ ℝ)
1081073ad2ant2 1131 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑𝑧 ∈ ℝ+𝑣 ∈ ℝ+) → 𝑧 ∈ ℝ)
109108ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑𝑧 ∈ ℝ+𝑣 ∈ ℝ+) ∧ 𝑏 ∈ ℝ) ∧ (abs‘(𝑏𝐵)) < if(𝑧𝑣, 𝑧, 𝑣)) → 𝑧 ∈ ℝ)
110 simpr 488 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑𝑧 ∈ ℝ+𝑣 ∈ ℝ+) ∧ 𝑏 ∈ ℝ) ∧ (abs‘(𝑏𝐵)) < if(𝑧𝑣, 𝑧, 𝑣)) → (abs‘(𝑏𝐵)) < if(𝑧𝑣, 𝑧, 𝑣))
111 rpre 12387 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑣 ∈ ℝ+𝑣 ∈ ℝ)
112 min1 12572 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑧 ∈ ℝ ∧ 𝑣 ∈ ℝ) → if(𝑧𝑣, 𝑧, 𝑣) ≤ 𝑧)
113107, 111, 112syl2an 598 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑧 ∈ ℝ+𝑣 ∈ ℝ+) → if(𝑧𝑣, 𝑧, 𝑣) ≤ 𝑧)
1141133adant1 1127 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑𝑧 ∈ ℝ+𝑣 ∈ ℝ+) → if(𝑧𝑣, 𝑧, 𝑣) ≤ 𝑧)
115114ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑𝑧 ∈ ℝ+𝑣 ∈ ℝ+) ∧ 𝑏 ∈ ℝ) ∧ (abs‘(𝑏𝐵)) < if(𝑧𝑣, 𝑧, 𝑣)) → if(𝑧𝑣, 𝑧, 𝑣) ≤ 𝑧)
116104, 106, 109, 110, 115ltletrd 10791 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑𝑧 ∈ ℝ+𝑣 ∈ ℝ+) ∧ 𝑏 ∈ ℝ) ∧ (abs‘(𝑏𝐵)) < if(𝑧𝑣, 𝑧, 𝑣)) → (abs‘(𝑏𝐵)) < 𝑧)
1171113ad2ant3 1132 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑𝑧 ∈ ℝ+𝑣 ∈ ℝ+) → 𝑣 ∈ ℝ)
118117ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑𝑧 ∈ ℝ+𝑣 ∈ ℝ+) ∧ 𝑏 ∈ ℝ) ∧ (abs‘(𝑏𝐵)) < if(𝑧𝑣, 𝑧, 𝑣)) → 𝑣 ∈ ℝ)
119109, 118min2d 42127 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑𝑧 ∈ ℝ+𝑣 ∈ ℝ+) ∧ 𝑏 ∈ ℝ) ∧ (abs‘(𝑏𝐵)) < if(𝑧𝑣, 𝑧, 𝑣)) → if(𝑧𝑣, 𝑧, 𝑣) ≤ 𝑣)
120104, 106, 118, 110, 119ltletrd 10791 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑𝑧 ∈ ℝ+𝑣 ∈ ℝ+) ∧ 𝑏 ∈ ℝ) ∧ (abs‘(𝑏𝐵)) < if(𝑧𝑣, 𝑧, 𝑣)) → (abs‘(𝑏𝐵)) < 𝑣)
121116, 120jca 515 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑𝑧 ∈ ℝ+𝑣 ∈ ℝ+) ∧ 𝑏 ∈ ℝ) ∧ (abs‘(𝑏𝐵)) < if(𝑧𝑣, 𝑧, 𝑣)) → ((abs‘(𝑏𝐵)) < 𝑧 ∧ (abs‘(𝑏𝐵)) < 𝑣))
122121ex 416 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑧 ∈ ℝ+𝑣 ∈ ℝ+) ∧ 𝑏 ∈ ℝ) → ((abs‘(𝑏𝐵)) < if(𝑧𝑣, 𝑧, 𝑣) → ((abs‘(𝑏𝐵)) < 𝑧 ∧ (abs‘(𝑏𝐵)) < 𝑣)))
12398, 122sylan2 595 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑧 ∈ ℝ+𝑣 ∈ ℝ+) ∧ 𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵})) → ((abs‘(𝑏𝐵)) < if(𝑧𝑣, 𝑧, 𝑣) → ((abs‘(𝑏𝐵)) < 𝑧 ∧ (abs‘(𝑏𝐵)) < 𝑣)))
124123reximdva 3233 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑧 ∈ ℝ+𝑣 ∈ ℝ+) → (∃𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵})(abs‘(𝑏𝐵)) < if(𝑧𝑣, 𝑧, 𝑣) → ∃𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵})((abs‘(𝑏𝐵)) < 𝑧 ∧ (abs‘(𝑏𝐵)) < 𝑣)))
12596, 124mpd 15 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑧 ∈ ℝ+𝑣 ∈ ℝ+) → ∃𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵})((abs‘(𝑏𝐵)) < 𝑧 ∧ (abs‘(𝑏𝐵)) < 𝑣))
12662, 63, 64, 125syl3anc 1368 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) → ∃𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵})((abs‘(𝑏𝐵)) < 𝑧 ∧ (abs‘(𝑏𝐵)) < 𝑣))
127 nfv 1915 . . . . . . . . . . . . . . . . . . . . . . 23 𝑏(((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦))
128 nfre1 3265 . . . . . . . . . . . . . . . . . . . . . . 23 𝑏𝑏𝐴 ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦)
12997elin1d 4125 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵}) → 𝑏𝐴)
1301293ad2ant2 1131 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) ∧ 𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵}) ∧ ((abs‘(𝑏𝐵)) < 𝑧 ∧ (abs‘(𝑏𝐵)) < 𝑣)) → 𝑏𝐴)
131 simp113 1301 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) ∧ 𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵}) ∧ ((abs‘(𝑏𝐵)) < 𝑧 ∧ (abs‘(𝑏𝐵)) < 𝑣)) → ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦))
132 eldifsni 4683 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵}) → 𝑏𝐵)
133132adantr 484 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵}) ∧ ((abs‘(𝑏𝐵)) < 𝑧 ∧ (abs‘(𝑏𝐵)) < 𝑣)) → 𝑏𝐵)
134 simprl 770 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵}) ∧ ((abs‘(𝑏𝐵)) < 𝑧 ∧ (abs‘(𝑏𝐵)) < 𝑣)) → (abs‘(𝑏𝐵)) < 𝑧)
135133, 134jca 515 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵}) ∧ ((abs‘(𝑏𝐵)) < 𝑧 ∧ (abs‘(𝑏𝐵)) < 𝑣)) → (𝑏𝐵 ∧ (abs‘(𝑏𝐵)) < 𝑧))
1361353adant1 1127 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) ∧ 𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵}) ∧ ((abs‘(𝑏𝐵)) < 𝑧 ∧ (abs‘(𝑏𝐵)) < 𝑣)) → (𝑏𝐵 ∧ (abs‘(𝑏𝐵)) < 𝑧))
137 neeq1 3049 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑤 = 𝑏 → (𝑤𝐵𝑏𝐵))
138 fvoveq1 7158 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑤 = 𝑏 → (abs‘(𝑤𝐵)) = (abs‘(𝑏𝐵)))
139138breq1d 5040 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑤 = 𝑏 → ((abs‘(𝑤𝐵)) < 𝑧 ↔ (abs‘(𝑏𝐵)) < 𝑧))
140137, 139anbi12d 633 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑤 = 𝑏 → ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) ↔ (𝑏𝐵 ∧ (abs‘(𝑏𝐵)) < 𝑧)))
141140imbrov2fvoveq 7160 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑤 = 𝑏 → (((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦) ↔ ((𝑏𝐵 ∧ (abs‘(𝑏𝐵)) < 𝑧) → (abs‘((𝐹𝑏) − 𝑥)) < 𝑦)))
142141rspcva 3569 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑏𝐴 ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) → ((𝑏𝐵 ∧ (abs‘(𝑏𝐵)) < 𝑧) → (abs‘((𝐹𝑏) − 𝑥)) < 𝑦))
143142imp 410 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑏𝐴 ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ (𝑏𝐵 ∧ (abs‘(𝑏𝐵)) < 𝑧)) → (abs‘((𝐹𝑏) − 𝑥)) < 𝑦)
144130, 131, 136, 143syl21anc 836 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) ∧ 𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵}) ∧ ((abs‘(𝑏𝐵)) < 𝑧 ∧ (abs‘(𝑏𝐵)) < 𝑣)) → (abs‘((𝐹𝑏) − 𝑥)) < 𝑦)
145973ad2ant2 1131 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) ∧ 𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵}) ∧ ((abs‘(𝑏𝐵)) < 𝑧 ∧ (abs‘(𝑏𝐵)) < 𝑣)) → 𝑏 ∈ (𝐴 ∩ (𝐵(,)+∞)))
146623ad2ant1 1130 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) ∧ 𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵}) ∧ ((abs‘(𝑏𝐵)) < 𝑧 ∧ (abs‘(𝑏𝐵)) < 𝑣)) → 𝜑)
147 simp13 1202 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) ∧ 𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵}) ∧ ((abs‘(𝑏𝐵)) < 𝑧 ∧ (abs‘(𝑏𝐵)) < 𝑣)) → ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦))
148 nfv 1915 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 𝑤𝜑
149 nfra1 3183 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 𝑤𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)
150148, 149nfan 1900 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 𝑤(𝜑 ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦))
151 elinel2 4123 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞)) → 𝑤 ∈ (𝐵(,)+∞))
152151fvresd 6665 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞)) → ((𝐹 ↾ (𝐵(,)+∞))‘𝑤) = (𝐹𝑤))
153152eqcomd 2804 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞)) → (𝐹𝑤) = ((𝐹 ↾ (𝐵(,)+∞))‘𝑤))
154153fvoveq1d 7157 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞)) → (abs‘((𝐹𝑤) − 𝑅)) = (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)))
1551543ad2ant2 1131 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝜑 ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) ∧ 𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞)) ∧ (𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣)) → (abs‘((𝐹𝑤) − 𝑅)) = (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)))
156 rspa 3171 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦) ∧ 𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))) → ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦))
1571563impia 1114 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦) ∧ 𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞)) ∧ (𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣)) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)
1581573adant1l 1173 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝜑 ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) ∧ 𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞)) ∧ (𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣)) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)
159155, 158eqbrtrd 5052 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑 ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) ∧ 𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞)) ∧ (𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣)) → (abs‘((𝐹𝑤) − 𝑅)) < 𝑦)
1601593exp 1116 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑 ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) → (𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞)) → ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘((𝐹𝑤) − 𝑅)) < 𝑦)))
161150, 160ralrimi 3180 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑 ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) → ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘((𝐹𝑤) − 𝑅)) < 𝑦))
162146, 147, 161syl2anc 587 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) ∧ 𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵}) ∧ ((abs‘(𝑏𝐵)) < 𝑧 ∧ (abs‘(𝑏𝐵)) < 𝑣)) → ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘((𝐹𝑤) − 𝑅)) < 𝑦))
163132anim1i 617 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵}) ∧ (abs‘(𝑏𝐵)) < 𝑣) → (𝑏𝐵 ∧ (abs‘(𝑏𝐵)) < 𝑣))
164163adantrl 715 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵}) ∧ ((abs‘(𝑏𝐵)) < 𝑧 ∧ (abs‘(𝑏𝐵)) < 𝑣)) → (𝑏𝐵 ∧ (abs‘(𝑏𝐵)) < 𝑣))
1651643adant1 1127 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) ∧ 𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵}) ∧ ((abs‘(𝑏𝐵)) < 𝑧 ∧ (abs‘(𝑏𝐵)) < 𝑣)) → (𝑏𝐵 ∧ (abs‘(𝑏𝐵)) < 𝑣))
166138breq1d 5040 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑤 = 𝑏 → ((abs‘(𝑤𝐵)) < 𝑣 ↔ (abs‘(𝑏𝐵)) < 𝑣))
167137, 166anbi12d 633 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑤 = 𝑏 → ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) ↔ (𝑏𝐵 ∧ (abs‘(𝑏𝐵)) < 𝑣)))
168167imbrov2fvoveq 7160 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑤 = 𝑏 → (((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘((𝐹𝑤) − 𝑅)) < 𝑦) ↔ ((𝑏𝐵 ∧ (abs‘(𝑏𝐵)) < 𝑣) → (abs‘((𝐹𝑏) − 𝑅)) < 𝑦)))
169168rspcva 3569 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑏 ∈ (𝐴 ∩ (𝐵(,)+∞)) ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘((𝐹𝑤) − 𝑅)) < 𝑦)) → ((𝑏𝐵 ∧ (abs‘(𝑏𝐵)) < 𝑣) → (abs‘((𝐹𝑏) − 𝑅)) < 𝑦))
170169imp 410 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑏 ∈ (𝐴 ∩ (𝐵(,)+∞)) ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘((𝐹𝑤) − 𝑅)) < 𝑦)) ∧ (𝑏𝐵 ∧ (abs‘(𝑏𝐵)) < 𝑣)) → (abs‘((𝐹𝑏) − 𝑅)) < 𝑦)
171145, 162, 165, 170syl21anc 836 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) ∧ 𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵}) ∧ ((abs‘(𝑏𝐵)) < 𝑧 ∧ (abs‘(𝑏𝐵)) < 𝑣)) → (abs‘((𝐹𝑏) − 𝑅)) < 𝑦)
172 rspe 3263 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑏𝐴 ∧ ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦)) → ∃𝑏𝐴 ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦))
173130, 144, 171, 172syl12anc 835 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) ∧ 𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵}) ∧ ((abs‘(𝑏𝐵)) < 𝑧 ∧ (abs‘(𝑏𝐵)) < 𝑣)) → ∃𝑏𝐴 ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦))
1741733exp 1116 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) → (𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵}) → (((abs‘(𝑏𝐵)) < 𝑧 ∧ (abs‘(𝑏𝐵)) < 𝑣) → ∃𝑏𝐴 ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦))))
175127, 128, 174rexlimd 3276 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) → (∃𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵})((abs‘(𝑏𝐵)) < 𝑧 ∧ (abs‘(𝑏𝐵)) < 𝑣) → ∃𝑏𝐴 ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦)))
176126, 175mpd 15 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) → ∃𝑏𝐴 ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦))
1771763exp 1116 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) → (𝑣 ∈ ℝ+ → (∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦) → ∃𝑏𝐴 ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦))))
178177rexlimdv 3242 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) → (∃𝑣 ∈ ℝ+𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦) → ∃𝑏𝐴 ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦)))
17961, 178mpd 15 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) → ∃𝑏𝐴 ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦))
1801793exp 1116 . . . . . . . . . . . . . . . . 17 ((𝜑𝑦 ∈ ℝ+) → (𝑧 ∈ ℝ+ → (∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦) → ∃𝑏𝐴 ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦))))
181180rexlimdv 3242 . . . . . . . . . . . . . . . 16 ((𝜑𝑦 ∈ ℝ+) → (∃𝑧 ∈ ℝ+𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦) → ∃𝑏𝐴 ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦)))
182181imp 410 . . . . . . . . . . . . . . 15 (((𝜑𝑦 ∈ ℝ+) ∧ ∃𝑧 ∈ ℝ+𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) → ∃𝑏𝐴 ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦))
183182adantllr 718 . . . . . . . . . . . . . 14 ((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ ∃𝑧 ∈ ℝ+𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) → ∃𝑏𝐴 ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦))
184183ad2antrr 725 . . . . . . . . . . . . 13 ((((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ ∃𝑧 ∈ ℝ+𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ 𝑎𝐴) ∧ ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)) → ∃𝑏𝐴 ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦))
1853ad6antr 735 . . . . . . . . . . . . . . . . . . 19 (((((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎𝐴) ∧ ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏𝐴) ∧ ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦)) → 𝑅 ∈ ℂ)
1867ad6antr 735 . . . . . . . . . . . . . . . . . . 19 (((((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎𝐴) ∧ ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏𝐴) ∧ ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦)) → 𝐿 ∈ ℂ)
187185, 186subcld 10988 . . . . . . . . . . . . . . . . . 18 (((((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎𝐴) ∧ ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏𝐴) ∧ ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦)) → (𝑅𝐿) ∈ ℂ)
188187abscld 14790 . . . . . . . . . . . . . . . . 17 (((((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎𝐴) ∧ ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏𝐴) ∧ ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦)) → (abs‘(𝑅𝐿)) ∈ ℝ)
189 simp-6l 786 . . . . . . . . . . . . . . . . . . . . . . 23 (((((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎𝐴) ∧ ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏𝐴) ∧ ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦)) → 𝜑)
190 simplr 768 . . . . . . . . . . . . . . . . . . . . . . 23 (((((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎𝐴) ∧ ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏𝐴) ∧ ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦)) → 𝑏𝐴)
19136ffvelrnda 6828 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑏𝐴) → (𝐹𝑏) ∈ ℂ)
192189, 190, 191syl2anc 587 . . . . . . . . . . . . . . . . . . . . . 22 (((((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎𝐴) ∧ ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏𝐴) ∧ ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦)) → (𝐹𝑏) ∈ ℂ)
193185, 192subcld 10988 . . . . . . . . . . . . . . . . . . . . 21 (((((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎𝐴) ∧ ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏𝐴) ∧ ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦)) → (𝑅 − (𝐹𝑏)) ∈ ℂ)
194193abscld 14790 . . . . . . . . . . . . . . . . . . . 20 (((((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎𝐴) ∧ ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏𝐴) ∧ ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦)) → (abs‘(𝑅 − (𝐹𝑏))) ∈ ℝ)
195 simp-6r 787 . . . . . . . . . . . . . . . . . . . . . 22 (((((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎𝐴) ∧ ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏𝐴) ∧ ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦)) → 𝑥 ∈ ℂ)
196192, 195subcld 10988 . . . . . . . . . . . . . . . . . . . . 21 (((((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎𝐴) ∧ ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏𝐴) ∧ ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦)) → ((𝐹𝑏) − 𝑥) ∈ ℂ)
197196abscld 14790 . . . . . . . . . . . . . . . . . . . 20 (((((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎𝐴) ∧ ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏𝐴) ∧ ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦)) → (abs‘((𝐹𝑏) − 𝑥)) ∈ ℝ)
198194, 197readdcld 10661 . . . . . . . . . . . . . . . . . . 19 (((((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎𝐴) ∧ ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏𝐴) ∧ ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦)) → ((abs‘(𝑅 − (𝐹𝑏))) + (abs‘((𝐹𝑏) − 𝑥))) ∈ ℝ)
199 simp-4r 783 . . . . . . . . . . . . . . . . . . . . . 22 (((((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎𝐴) ∧ ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏𝐴) ∧ ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦)) → 𝑎𝐴)
20036ffvelrnda 6828 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑎𝐴) → (𝐹𝑎) ∈ ℂ)
201189, 199, 200syl2anc 587 . . . . . . . . . . . . . . . . . . . . 21 (((((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎𝐴) ∧ ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏𝐴) ∧ ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦)) → (𝐹𝑎) ∈ ℂ)
202195, 201subcld 10988 . . . . . . . . . . . . . . . . . . . 20 (((((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎𝐴) ∧ ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏𝐴) ∧ ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦)) → (𝑥 − (𝐹𝑎)) ∈ ℂ)
203202abscld 14790 . . . . . . . . . . . . . . . . . . 19 (((((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎𝐴) ∧ ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏𝐴) ∧ ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦)) → (abs‘(𝑥 − (𝐹𝑎))) ∈ ℝ)
204198, 203readdcld 10661 . . . . . . . . . . . . . . . . . 18 (((((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎𝐴) ∧ ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏𝐴) ∧ ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦)) → (((abs‘(𝑅 − (𝐹𝑏))) + (abs‘((𝐹𝑏) − 𝑥))) + (abs‘(𝑥 − (𝐹𝑎)))) ∈ ℝ)
205201, 186subcld 10988 . . . . . . . . . . . . . . . . . . 19 (((((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎𝐴) ∧ ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏𝐴) ∧ ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦)) → ((𝐹𝑎) − 𝐿) ∈ ℂ)
206205abscld 14790 . . . . . . . . . . . . . . . . . 18 (((((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎𝐴) ∧ ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏𝐴) ∧ ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦)) → (abs‘((𝐹𝑎) − 𝐿)) ∈ ℝ)
207204, 206readdcld 10661 . . . . . . . . . . . . . . . . 17 (((((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎𝐴) ∧ ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏𝐴) ∧ ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦)) → ((((abs‘(𝑅 − (𝐹𝑏))) + (abs‘((𝐹𝑏) − 𝑥))) + (abs‘(𝑥 − (𝐹𝑎)))) + (abs‘((𝐹𝑎) − 𝐿))) ∈ ℝ)
20815a1i 11 . . . . . . . . . . . . . . . . . 18 (((((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎𝐴) ∧ ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏𝐴) ∧ ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦)) → 4 ∈ ℝ)
209 rpre 12387 . . . . . . . . . . . . . . . . . . 19 (𝑦 ∈ ℝ+𝑦 ∈ ℝ)
210209ad5antlr 734 . . . . . . . . . . . . . . . . . 18 (((((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎𝐴) ∧ ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏𝐴) ∧ ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦)) → 𝑦 ∈ ℝ)
211208, 210remulcld 10662 . . . . . . . . . . . . . . . . 17 (((((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎𝐴) ∧ ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏𝐴) ∧ ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦)) → (4 · 𝑦) ∈ ℝ)
212185, 192, 195, 201, 186absnpncan3d 41954 . . . . . . . . . . . . . . . . 17 (((((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎𝐴) ∧ ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏𝐴) ∧ ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦)) → (abs‘(𝑅𝐿)) ≤ ((((abs‘(𝑅 − (𝐹𝑏))) + (abs‘((𝐹𝑏) − 𝑥))) + (abs‘(𝑥 − (𝐹𝑎)))) + (abs‘((𝐹𝑎) − 𝐿))))
213185, 192abssubd 14807 . . . . . . . . . . . . . . . . . . 19 (((((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎𝐴) ∧ ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏𝐴) ∧ ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦)) → (abs‘(𝑅 − (𝐹𝑏))) = (abs‘((𝐹𝑏) − 𝑅)))
214 simprr 772 . . . . . . . . . . . . . . . . . . 19 (((((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎𝐴) ∧ ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏𝐴) ∧ ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦)) → (abs‘((𝐹𝑏) − 𝑅)) < 𝑦)
215213, 214eqbrtrd 5052 . . . . . . . . . . . . . . . . . 18 (((((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎𝐴) ∧ ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏𝐴) ∧ ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦)) → (abs‘(𝑅 − (𝐹𝑏))) < 𝑦)
216 simprl 770 . . . . . . . . . . . . . . . . . 18 (((((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎𝐴) ∧ ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏𝐴) ∧ ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦)) → (abs‘((𝐹𝑏) − 𝑥)) < 𝑦)
217 simp-5r 785 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎𝐴) ∧ ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏𝐴) → 𝑥 ∈ ℂ)
218200ad5ant14 757 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎𝐴) ∧ ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)) → (𝐹𝑎) ∈ ℂ)
219218adantr 484 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎𝐴) ∧ ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏𝐴) → (𝐹𝑎) ∈ ℂ)
220217, 219abssubd 14807 . . . . . . . . . . . . . . . . . . . 20 ((((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎𝐴) ∧ ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏𝐴) → (abs‘(𝑥 − (𝐹𝑎))) = (abs‘((𝐹𝑎) − 𝑥)))
221 simplrl 776 . . . . . . . . . . . . . . . . . . . 20 ((((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎𝐴) ∧ ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏𝐴) → (abs‘((𝐹𝑎) − 𝑥)) < 𝑦)
222220, 221eqbrtrd 5052 . . . . . . . . . . . . . . . . . . 19 ((((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎𝐴) ∧ ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏𝐴) → (abs‘(𝑥 − (𝐹𝑎))) < 𝑦)
223222adantr 484 . . . . . . . . . . . . . . . . . 18 (((((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎𝐴) ∧ ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏𝐴) ∧ ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦)) → (abs‘(𝑥 − (𝐹𝑎))) < 𝑦)
224 simplrr 777 . . . . . . . . . . . . . . . . . . 19 ((((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎𝐴) ∧ ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏𝐴) → (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)
225224adantr 484 . . . . . . . . . . . . . . . . . 18 (((((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎𝐴) ∧ ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏𝐴) ∧ ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦)) → (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)
226194, 197, 203, 206, 210, 215, 216, 223, 225lt4addmuld 41953 . . . . . . . . . . . . . . . . 17 (((((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎𝐴) ∧ ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏𝐴) ∧ ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦)) → ((((abs‘(𝑅 − (𝐹𝑏))) + (abs‘((𝐹𝑏) − 𝑥))) + (abs‘(𝑥 − (𝐹𝑎)))) + (abs‘((𝐹𝑎) − 𝐿))) < (4 · 𝑦))
227188, 207, 211, 212, 226lelttrd 10789 . . . . . . . . . . . . . . . 16 (((((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎𝐴) ∧ ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏𝐴) ∧ ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦)) → (abs‘(𝑅𝐿)) < (4 · 𝑦))
228227ex 416 . . . . . . . . . . . . . . 15 ((((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎𝐴) ∧ ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏𝐴) → (((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦) → (abs‘(𝑅𝐿)) < (4 · 𝑦)))
229228adantl3r 749 . . . . . . . . . . . . . 14 (((((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ ∃𝑧 ∈ ℝ+𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ 𝑎𝐴) ∧ ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏𝐴) → (((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦) → (abs‘(𝑅𝐿)) < (4 · 𝑦)))
230229reximdva 3233 . . . . . . . . . . . . 13 ((((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ ∃𝑧 ∈ ℝ+𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ 𝑎𝐴) ∧ ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)) → (∃𝑏𝐴 ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦) → ∃𝑏𝐴 (abs‘(𝑅𝐿)) < (4 · 𝑦)))
231184, 230mpd 15 . . . . . . . . . . . 12 ((((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ ∃𝑧 ∈ ℝ+𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ 𝑎𝐴) ∧ ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)) → ∃𝑏𝐴 (abs‘(𝑅𝐿)) < (4 · 𝑦))
232 fresin 6521 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐹:𝐴⟶ℂ → (𝐹 ↾ (-∞(,)𝐵)):(𝐴 ∩ (-∞(,)𝐵))⟶ℂ)
23336, 232syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝐹 ↾ (-∞(,)𝐵)):(𝐴 ∩ (-∞(,)𝐵))⟶ℂ)
234 ioosscn 12789 . . . . . . . . . . . . . . . . . . . . . . . 24 (-∞(,)𝐵) ⊆ ℂ
23546, 234sstri 3924 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐴 ∩ (-∞(,)𝐵)) ⊆ ℂ
236235a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝐴 ∩ (-∞(,)𝐵)) ⊆ ℂ)
237233, 236, 56ellimc3 24489 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝐿 ∈ ((𝐹 ↾ (-∞(,)𝐵)) lim 𝐵) ↔ (𝐿 ∈ ℂ ∧ ∀𝑦 ∈ ℝ+𝑣 ∈ ℝ+𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦))))
2386, 237mpbid 235 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝐿 ∈ ℂ ∧ ∀𝑦 ∈ ℝ+𝑣 ∈ ℝ+𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)))
239238simprd 499 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ∀𝑦 ∈ ℝ+𝑣 ∈ ℝ+𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦))
240239r19.21bi 3173 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑦 ∈ ℝ+) → ∃𝑣 ∈ ℝ+𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦))
2412403ad2ant1 1130 . . . . . . . . . . . . . . . . 17 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) → ∃𝑣 ∈ ℝ+𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦))
242 simp11l 1281 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) → 𝜑)
243 simp12 1201 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) → 𝑧 ∈ ℝ+)
244 simp2 1134 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) → 𝑣 ∈ ℝ+)
245 breq2 5034 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑢 = if(𝑧𝑣, 𝑧, 𝑣) → ((abs‘(𝑎𝐵)) < 𝑢 ↔ (abs‘(𝑎𝐵)) < if(𝑧𝑣, 𝑧, 𝑣)))
246245rexbidv 3256 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑢 = if(𝑧𝑣, 𝑧, 𝑣) → (∃𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵})(abs‘(𝑎𝐵)) < 𝑢 ↔ ∃𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵})(abs‘(𝑎𝐵)) < if(𝑧𝑣, 𝑧, 𝑣)))
247 inss1 4155 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((limPt‘𝐾)‘(𝐴 ∩ (-∞(,)𝐵))) ∩ ℝ) ⊆ ((limPt‘𝐾)‘(𝐴 ∩ (-∞(,)𝐵)))
248247a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → (((limPt‘𝐾)‘(𝐴 ∩ (-∞(,)𝐵))) ∩ ℝ) ⊆ ((limPt‘𝐾)‘(𝐴 ∩ (-∞(,)𝐵))))
24948a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑 → (𝐴 ∩ (-∞(,)𝐵)) ⊆ ℝ)
25079, 81restlp 21795 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝐾 ∈ Top ∧ ℝ ⊆ ℂ ∧ (𝐴 ∩ (-∞(,)𝐵)) ⊆ ℝ) → ((limPt‘𝐽)‘(𝐴 ∩ (-∞(,)𝐵))) = (((limPt‘𝐾)‘(𝐴 ∩ (-∞(,)𝐵))) ∩ ℝ))
25171, 73, 249, 250syl3anc 1368 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → ((limPt‘𝐽)‘(𝐴 ∩ (-∞(,)𝐵))) = (((limPt‘𝐾)‘(𝐴 ∩ (-∞(,)𝐵))) ∩ ℝ))
25285fveq1i 6646 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((limPt‘(TopOpen‘ℂfld))‘(𝐴 ∩ (-∞(,)𝐵))) = ((limPt‘𝐾)‘(𝐴 ∩ (-∞(,)𝐵)))
253252a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → ((limPt‘(TopOpen‘ℂfld))‘(𝐴 ∩ (-∞(,)𝐵))) = ((limPt‘𝐾)‘(𝐴 ∩ (-∞(,)𝐵))))
254248, 251, 2533sstr4d 3962 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → ((limPt‘𝐽)‘(𝐴 ∩ (-∞(,)𝐵))) ⊆ ((limPt‘(TopOpen‘ℂfld))‘(𝐴 ∩ (-∞(,)𝐵))))
255254, 54sseldd 3916 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑𝐵 ∈ ((limPt‘(TopOpen‘ℂfld))‘(𝐴 ∩ (-∞(,)𝐵))))
256236, 56islpcn 42296 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → (𝐵 ∈ ((limPt‘(TopOpen‘ℂfld))‘(𝐴 ∩ (-∞(,)𝐵))) ↔ ∀𝑢 ∈ ℝ+𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵})(abs‘(𝑎𝐵)) < 𝑢))
257255, 256mpbid 235 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → ∀𝑢 ∈ ℝ+𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵})(abs‘(𝑎𝐵)) < 𝑢)
2582573ad2ant1 1130 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑧 ∈ ℝ+𝑣 ∈ ℝ+) → ∀𝑢 ∈ ℝ+𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵})(abs‘(𝑎𝐵)) < 𝑢)
259246, 258, 95rspcdva 3573 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑧 ∈ ℝ+𝑣 ∈ ℝ+) → ∃𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵})(abs‘(𝑎𝐵)) < if(𝑧𝑣, 𝑧, 𝑣))
260 eldifi 4054 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵}) → 𝑎 ∈ (𝐴 ∩ (-∞(,)𝐵)))
26148, 260sseldi 3913 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵}) → 𝑎 ∈ ℝ)
26273sselda 3915 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑𝑎 ∈ ℝ) → 𝑎 ∈ ℂ)
26356adantr 484 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑𝑎 ∈ ℝ) → 𝐵 ∈ ℂ)
264262, 263subcld 10988 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑𝑎 ∈ ℝ) → (𝑎𝐵) ∈ ℂ)
265264abscld 14790 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑎 ∈ ℝ) → (abs‘(𝑎𝐵)) ∈ ℝ)
2662653ad2antl1 1182 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑𝑧 ∈ ℝ+𝑣 ∈ ℝ+) ∧ 𝑎 ∈ ℝ) → (abs‘(𝑎𝐵)) ∈ ℝ)
267266adantr 484 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑𝑧 ∈ ℝ+𝑣 ∈ ℝ+) ∧ 𝑎 ∈ ℝ) ∧ (abs‘(𝑎𝐵)) < if(𝑧𝑣, 𝑧, 𝑣)) → (abs‘(𝑎𝐵)) ∈ ℝ)
268105ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑𝑧 ∈ ℝ+𝑣 ∈ ℝ+) ∧ 𝑎 ∈ ℝ) ∧ (abs‘(𝑎𝐵)) < if(𝑧𝑣, 𝑧, 𝑣)) → if(𝑧𝑣, 𝑧, 𝑣) ∈ ℝ)
269108ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑𝑧 ∈ ℝ+𝑣 ∈ ℝ+) ∧ 𝑎 ∈ ℝ) ∧ (abs‘(𝑎𝐵)) < if(𝑧𝑣, 𝑧, 𝑣)) → 𝑧 ∈ ℝ)
270 simpr 488 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑𝑧 ∈ ℝ+𝑣 ∈ ℝ+) ∧ 𝑎 ∈ ℝ) ∧ (abs‘(𝑎𝐵)) < if(𝑧𝑣, 𝑧, 𝑣)) → (abs‘(𝑎𝐵)) < if(𝑧𝑣, 𝑧, 𝑣))
271114ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑𝑧 ∈ ℝ+𝑣 ∈ ℝ+) ∧ 𝑎 ∈ ℝ) ∧ (abs‘(𝑎𝐵)) < if(𝑧𝑣, 𝑧, 𝑣)) → if(𝑧𝑣, 𝑧, 𝑣) ≤ 𝑧)
272267, 268, 269, 270, 271ltletrd 10791 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑𝑧 ∈ ℝ+𝑣 ∈ ℝ+) ∧ 𝑎 ∈ ℝ) ∧ (abs‘(𝑎𝐵)) < if(𝑧𝑣, 𝑧, 𝑣)) → (abs‘(𝑎𝐵)) < 𝑧)
273117ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑𝑧 ∈ ℝ+𝑣 ∈ ℝ+) ∧ 𝑎 ∈ ℝ) ∧ (abs‘(𝑎𝐵)) < if(𝑧𝑣, 𝑧, 𝑣)) → 𝑣 ∈ ℝ)
274 min2 12573 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑧 ∈ ℝ ∧ 𝑣 ∈ ℝ) → if(𝑧𝑣, 𝑧, 𝑣) ≤ 𝑣)
275107, 111, 274syl2an 598 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑧 ∈ ℝ+𝑣 ∈ ℝ+) → if(𝑧𝑣, 𝑧, 𝑣) ≤ 𝑣)
2762753adant1 1127 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑧 ∈ ℝ+𝑣 ∈ ℝ+) → if(𝑧𝑣, 𝑧, 𝑣) ≤ 𝑣)
277276ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑𝑧 ∈ ℝ+𝑣 ∈ ℝ+) ∧ 𝑎 ∈ ℝ) ∧ (abs‘(𝑎𝐵)) < if(𝑧𝑣, 𝑧, 𝑣)) → if(𝑧𝑣, 𝑧, 𝑣) ≤ 𝑣)
278267, 268, 273, 270, 277ltletrd 10791 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑𝑧 ∈ ℝ+𝑣 ∈ ℝ+) ∧ 𝑎 ∈ ℝ) ∧ (abs‘(𝑎𝐵)) < if(𝑧𝑣, 𝑧, 𝑣)) → (abs‘(𝑎𝐵)) < 𝑣)
279272, 278jca 515 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑧 ∈ ℝ+𝑣 ∈ ℝ+) ∧ 𝑎 ∈ ℝ) ∧ (abs‘(𝑎𝐵)) < if(𝑧𝑣, 𝑧, 𝑣)) → ((abs‘(𝑎𝐵)) < 𝑧 ∧ (abs‘(𝑎𝐵)) < 𝑣))
280279ex 416 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑧 ∈ ℝ+𝑣 ∈ ℝ+) ∧ 𝑎 ∈ ℝ) → ((abs‘(𝑎𝐵)) < if(𝑧𝑣, 𝑧, 𝑣) → ((abs‘(𝑎𝐵)) < 𝑧 ∧ (abs‘(𝑎𝐵)) < 𝑣)))
281261, 280sylan2 595 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑧 ∈ ℝ+𝑣 ∈ ℝ+) ∧ 𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵})) → ((abs‘(𝑎𝐵)) < if(𝑧𝑣, 𝑧, 𝑣) → ((abs‘(𝑎𝐵)) < 𝑧 ∧ (abs‘(𝑎𝐵)) < 𝑣)))
282281reximdva 3233 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑧 ∈ ℝ+𝑣 ∈ ℝ+) → (∃𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵})(abs‘(𝑎𝐵)) < if(𝑧𝑣, 𝑧, 𝑣) → ∃𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵})((abs‘(𝑎𝐵)) < 𝑧 ∧ (abs‘(𝑎𝐵)) < 𝑣)))
283259, 282mpd 15 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑧 ∈ ℝ+𝑣 ∈ ℝ+) → ∃𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵})((abs‘(𝑎𝐵)) < 𝑧 ∧ (abs‘(𝑎𝐵)) < 𝑣))
284242, 243, 244, 283syl3anc 1368 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) → ∃𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵})((abs‘(𝑎𝐵)) < 𝑧 ∧ (abs‘(𝑎𝐵)) < 𝑣))
285 nfv 1915 . . . . . . . . . . . . . . . . . . . . 21 𝑎(((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦))
286 nfre1 3265 . . . . . . . . . . . . . . . . . . . . 21 𝑎𝑎𝐴 ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)
287260elin1d 4125 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵}) → 𝑎𝐴)
2882873ad2ant2 1131 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) ∧ 𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵}) ∧ ((abs‘(𝑎𝐵)) < 𝑧 ∧ (abs‘(𝑎𝐵)) < 𝑣)) → 𝑎𝐴)
289 simp113 1301 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) ∧ 𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵}) ∧ ((abs‘(𝑎𝐵)) < 𝑧 ∧ (abs‘(𝑎𝐵)) < 𝑣)) → ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦))
290 eldifsni 4683 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵}) → 𝑎𝐵)
291290adantr 484 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵}) ∧ ((abs‘(𝑎𝐵)) < 𝑧 ∧ (abs‘(𝑎𝐵)) < 𝑣)) → 𝑎𝐵)
292 simprl 770 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵}) ∧ ((abs‘(𝑎𝐵)) < 𝑧 ∧ (abs‘(𝑎𝐵)) < 𝑣)) → (abs‘(𝑎𝐵)) < 𝑧)
293291, 292jca 515 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵}) ∧ ((abs‘(𝑎𝐵)) < 𝑧 ∧ (abs‘(𝑎𝐵)) < 𝑣)) → (𝑎𝐵 ∧ (abs‘(𝑎𝐵)) < 𝑧))
2942933adant1 1127 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) ∧ 𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵}) ∧ ((abs‘(𝑎𝐵)) < 𝑧 ∧ (abs‘(𝑎𝐵)) < 𝑣)) → (𝑎𝐵 ∧ (abs‘(𝑎𝐵)) < 𝑧))
295 neeq1 3049 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑤 = 𝑎 → (𝑤𝐵𝑎𝐵))
296 fvoveq1 7158 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑤 = 𝑎 → (abs‘(𝑤𝐵)) = (abs‘(𝑎𝐵)))
297296breq1d 5040 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑤 = 𝑎 → ((abs‘(𝑤𝐵)) < 𝑧 ↔ (abs‘(𝑎𝐵)) < 𝑧))
298295, 297anbi12d 633 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑤 = 𝑎 → ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) ↔ (𝑎𝐵 ∧ (abs‘(𝑎𝐵)) < 𝑧)))
299298imbrov2fvoveq 7160 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑤 = 𝑎 → (((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦) ↔ ((𝑎𝐵 ∧ (abs‘(𝑎𝐵)) < 𝑧) → (abs‘((𝐹𝑎) − 𝑥)) < 𝑦)))
300299rspcva 3569 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑎𝐴 ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) → ((𝑎𝐵 ∧ (abs‘(𝑎𝐵)) < 𝑧) → (abs‘((𝐹𝑎) − 𝑥)) < 𝑦))
301300imp 410 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑎𝐴 ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ (𝑎𝐵 ∧ (abs‘(𝑎𝐵)) < 𝑧)) → (abs‘((𝐹𝑎) − 𝑥)) < 𝑦)
302288, 289, 294, 301syl21anc 836 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) ∧ 𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵}) ∧ ((abs‘(𝑎𝐵)) < 𝑧 ∧ (abs‘(𝑎𝐵)) < 𝑣)) → (abs‘((𝐹𝑎) − 𝑥)) < 𝑦)
3032603ad2ant2 1131 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) ∧ 𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵}) ∧ ((abs‘(𝑎𝐵)) < 𝑧 ∧ (abs‘(𝑎𝐵)) < 𝑣)) → 𝑎 ∈ (𝐴 ∩ (-∞(,)𝐵)))
3042423ad2ant1 1130 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) ∧ 𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵}) ∧ ((abs‘(𝑎𝐵)) < 𝑧 ∧ (abs‘(𝑎𝐵)) < 𝑣)) → 𝜑)
305 simp13 1202 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) ∧ 𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵}) ∧ ((abs‘(𝑎𝐵)) < 𝑧 ∧ (abs‘(𝑎𝐵)) < 𝑣)) → ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦))
306 nfra1 3183 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 𝑤𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)
307148, 306nfan 1900 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝑤(𝜑 ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦))
308 elinel2 4123 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵)) → 𝑤 ∈ (-∞(,)𝐵))
309308fvresd 6665 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵)) → ((𝐹 ↾ (-∞(,)𝐵))‘𝑤) = (𝐹𝑤))
310309eqcomd 2804 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵)) → (𝐹𝑤) = ((𝐹 ↾ (-∞(,)𝐵))‘𝑤))
311310fvoveq1d 7157 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵)) → (abs‘((𝐹𝑤) − 𝐿)) = (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)))
3123113ad2ant2 1131 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑 ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) ∧ 𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵)) ∧ (𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣)) → (abs‘((𝐹𝑤) − 𝐿)) = (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)))
313 rspa 3171 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦) ∧ 𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))) → ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦))
3143133impia 1114 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦) ∧ 𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵)) ∧ (𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣)) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)
3153143adant1l 1173 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑 ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) ∧ 𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵)) ∧ (𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣)) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)
316312, 315eqbrtrd 5052 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑 ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) ∧ 𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵)) ∧ (𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣)) → (abs‘((𝐹𝑤) − 𝐿)) < 𝑦)
3173163exp 1116 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑 ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) → (𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵)) → ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘((𝐹𝑤) − 𝐿)) < 𝑦)))
318307, 317ralrimi 3180 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) → ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘((𝐹𝑤) − 𝐿)) < 𝑦))
319304, 305, 318syl2anc 587 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) ∧ 𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵}) ∧ ((abs‘(𝑎𝐵)) < 𝑧 ∧ (abs‘(𝑎𝐵)) < 𝑣)) → ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘((𝐹𝑤) − 𝐿)) < 𝑦))
320290anim1i 617 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵}) ∧ (abs‘(𝑎𝐵)) < 𝑣) → (𝑎𝐵 ∧ (abs‘(𝑎𝐵)) < 𝑣))
321320adantrl 715 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵}) ∧ ((abs‘(𝑎𝐵)) < 𝑧 ∧ (abs‘(𝑎𝐵)) < 𝑣)) → (𝑎𝐵 ∧ (abs‘(𝑎𝐵)) < 𝑣))
3223213adant1 1127 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) ∧ 𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵}) ∧ ((abs‘(𝑎𝐵)) < 𝑧 ∧ (abs‘(𝑎𝐵)) < 𝑣)) → (𝑎𝐵 ∧ (abs‘(𝑎𝐵)) < 𝑣))
323296breq1d 5040 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑤 = 𝑎 → ((abs‘(𝑤𝐵)) < 𝑣 ↔ (abs‘(𝑎𝐵)) < 𝑣))
324295, 323anbi12d 633 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑤 = 𝑎 → ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) ↔ (𝑎𝐵 ∧ (abs‘(𝑎𝐵)) < 𝑣)))
325324imbrov2fvoveq 7160 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑤 = 𝑎 → (((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘((𝐹𝑤) − 𝐿)) < 𝑦) ↔ ((𝑎𝐵 ∧ (abs‘(𝑎𝐵)) < 𝑣) → (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)))
326325rspcva 3569 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑎 ∈ (𝐴 ∩ (-∞(,)𝐵)) ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘((𝐹𝑤) − 𝐿)) < 𝑦)) → ((𝑎𝐵 ∧ (abs‘(𝑎𝐵)) < 𝑣) → (abs‘((𝐹𝑎) − 𝐿)) < 𝑦))
327326imp 410 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑎 ∈ (𝐴 ∩ (-∞(,)𝐵)) ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘((𝐹𝑤) − 𝐿)) < 𝑦)) ∧ (𝑎𝐵 ∧ (abs‘(𝑎𝐵)) < 𝑣)) → (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)
328303, 319, 322, 327syl21anc 836 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) ∧ 𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵}) ∧ ((abs‘(𝑎𝐵)) < 𝑧 ∧ (abs‘(𝑎𝐵)) < 𝑣)) → (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)
329 rspe 3263 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑎𝐴 ∧ ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)) → ∃𝑎𝐴 ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦))
330288, 302, 328, 329syl12anc 835 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) ∧ 𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵}) ∧ ((abs‘(𝑎𝐵)) < 𝑧 ∧ (abs‘(𝑎𝐵)) < 𝑣)) → ∃𝑎𝐴 ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦))
3313303exp 1116 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) → (𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵}) → (((abs‘(𝑎𝐵)) < 𝑧 ∧ (abs‘(𝑎𝐵)) < 𝑣) → ∃𝑎𝐴 ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦))))
332285, 286, 331rexlimd 3276 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) → (∃𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵})((abs‘(𝑎𝐵)) < 𝑧 ∧ (abs‘(𝑎𝐵)) < 𝑣) → ∃𝑎𝐴 ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)))
333284, 332mpd 15 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) → ∃𝑎𝐴 ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦))
3343333exp 1116 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) → (𝑣 ∈ ℝ+ → (∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦) → ∃𝑎𝐴 ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦))))
335334rexlimdv 3242 . . . . . . . . . . . . . . . . 17 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) → (∃𝑣 ∈ ℝ+𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦) → ∃𝑎𝐴 ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)))
336241, 335mpd 15 . . . . . . . . . . . . . . . 16 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) → ∃𝑎𝐴 ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦))
3373363exp 1116 . . . . . . . . . . . . . . 15 ((𝜑𝑦 ∈ ℝ+) → (𝑧 ∈ ℝ+ → (∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦) → ∃𝑎𝐴 ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦))))
338337rexlimdv 3242 . . . . . . . . . . . . . 14 ((𝜑𝑦 ∈ ℝ+) → (∃𝑧 ∈ ℝ+𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦) → ∃𝑎𝐴 ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)))
339338imp 410 . . . . . . . . . . . . 13 (((𝜑𝑦 ∈ ℝ+) ∧ ∃𝑧 ∈ ℝ+𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) → ∃𝑎𝐴 ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦))
340339adantllr 718 . . . . . . . . . . . 12 ((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ ∃𝑧 ∈ ℝ+𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) → ∃𝑎𝐴 ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦))
341231, 340reximddv3 41803 . . . . . . . . . . 11 ((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ ∃𝑧 ∈ ℝ+𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) → ∃𝑎𝐴𝑏𝐴 (abs‘(𝑅𝐿)) < (4 · 𝑦))
34232, 33, 35, 341syl21anc 836 . . . . . . . . . 10 ((((𝜑𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ 𝑦 ∈ ℝ+) → ∃𝑎𝐴𝑏𝐴 (abs‘(𝑅𝐿)) < (4 · 𝑦))
343342ex 416 . . . . . . . . 9 (((𝜑𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) → (𝑦 ∈ ℝ+ → ∃𝑎𝐴𝑏𝐴 (abs‘(𝑅𝐿)) < (4 · 𝑦)))
34424, 25, 31, 343vtoclf 3506 . . . . . . . 8 (((𝜑𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) → (((abs‘(𝑅𝐿)) / 4) ∈ ℝ+ → ∃𝑎𝐴𝑏𝐴 (abs‘(𝑅𝐿)) < (4 · ((abs‘(𝑅𝐿)) / 4))))
34519, 344mpd 15 . . . . . . 7 (((𝜑𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) → ∃𝑎𝐴𝑏𝐴 (abs‘(𝑅𝐿)) < (4 · ((abs‘(𝑅𝐿)) / 4)))
346 simpr 488 . . . . . . . . . . . 12 ((𝜑 ∧ (abs‘(𝑅𝐿)) < (4 · ((abs‘(𝑅𝐿)) / 4))) → (abs‘(𝑅𝐿)) < (4 · ((abs‘(𝑅𝐿)) / 4)))
347 abssubrp 41921 . . . . . . . . . . . . . . . 16 ((𝑅 ∈ ℂ ∧ 𝐿 ∈ ℂ ∧ 𝑅𝐿) → (abs‘(𝑅𝐿)) ∈ ℝ+)
3483, 7, 11, 347syl3anc 1368 . . . . . . . . . . . . . . 15 (𝜑 → (abs‘(𝑅𝐿)) ∈ ℝ+)
349348rpcnd 12423 . . . . . . . . . . . . . 14 (𝜑 → (abs‘(𝑅𝐿)) ∈ ℂ)
350349adantr 484 . . . . . . . . . . . . 13 ((𝜑 ∧ (abs‘(𝑅𝐿)) < (4 · ((abs‘(𝑅𝐿)) / 4))) → (abs‘(𝑅𝐿)) ∈ ℂ)
351 4cn 11712 . . . . . . . . . . . . . 14 4 ∈ ℂ
352351a1i 11 . . . . . . . . . . . . 13 ((𝜑 ∧ (abs‘(𝑅𝐿)) < (4 · ((abs‘(𝑅𝐿)) / 4))) → 4 ∈ ℂ)
353 4ne0 11735 . . . . . . . . . . . . . 14 4 ≠ 0
354353a1i 11 . . . . . . . . . . . . 13 ((𝜑 ∧ (abs‘(𝑅𝐿)) < (4 · ((abs‘(𝑅𝐿)) / 4))) → 4 ≠ 0)
355350, 352, 354divcan2d 11409 . . . . . . . . . . . 12 ((𝜑 ∧ (abs‘(𝑅𝐿)) < (4 · ((abs‘(𝑅𝐿)) / 4))) → (4 · ((abs‘(𝑅𝐿)) / 4)) = (abs‘(𝑅𝐿)))
356346, 355breqtrd 5056 . . . . . . . . . . 11 ((𝜑 ∧ (abs‘(𝑅𝐿)) < (4 · ((abs‘(𝑅𝐿)) / 4))) → (abs‘(𝑅𝐿)) < (abs‘(𝑅𝐿)))
357356ex 416 . . . . . . . . . 10 (𝜑 → ((abs‘(𝑅𝐿)) < (4 · ((abs‘(𝑅𝐿)) / 4)) → (abs‘(𝑅𝐿)) < (abs‘(𝑅𝐿))))
358357a1d 25 . . . . . . . . 9 (𝜑 → ((𝑎𝐴𝑏𝐴) → ((abs‘(𝑅𝐿)) < (4 · ((abs‘(𝑅𝐿)) / 4)) → (abs‘(𝑅𝐿)) < (abs‘(𝑅𝐿)))))
359358ad2antrr 725 . . . . . . . 8 (((𝜑𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) → ((𝑎𝐴𝑏𝐴) → ((abs‘(𝑅𝐿)) < (4 · ((abs‘(𝑅𝐿)) / 4)) → (abs‘(𝑅𝐿)) < (abs‘(𝑅𝐿)))))
360359rexlimdvv 3252 . . . . . . 7 (((𝜑𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) → (∃𝑎𝐴𝑏𝐴 (abs‘(𝑅𝐿)) < (4 · ((abs‘(𝑅𝐿)) / 4)) → (abs‘(𝑅𝐿)) < (abs‘(𝑅𝐿))))
361345, 360mpd 15 . . . . . 6 (((𝜑𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) → (abs‘(𝑅𝐿)) < (abs‘(𝑅𝐿)))
3629abscld 14790 . . . . . . 7 (((𝜑𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) → (abs‘(𝑅𝐿)) ∈ ℝ)
363362ltnrd 10765 . . . . . 6 (((𝜑𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) → ¬ (abs‘(𝑅𝐿)) < (abs‘(𝑅𝐿)))
364361, 363pm2.65da 816 . . . . 5 ((𝜑𝑥 ∈ ℂ) → ¬ ∀𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦))
365364ex 416 . . . 4 (𝜑 → (𝑥 ∈ ℂ → ¬ ∀𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)))
366 imnan 403 . . . 4 ((𝑥 ∈ ℂ → ¬ ∀𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ↔ ¬ (𝑥 ∈ ℂ ∧ ∀𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)))
367365, 366sylib 221 . . 3 (𝜑 → ¬ (𝑥 ∈ ℂ ∧ ∀𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)))
368 limclner.a . . . . 5 (𝜑𝐴 ⊆ ℝ)
369368, 73sstrd 3925 . . . 4 (𝜑𝐴 ⊆ ℂ)
37036, 369, 56ellimc3 24489 . . 3 (𝜑 → (𝑥 ∈ (𝐹 lim 𝐵) ↔ (𝑥 ∈ ℂ ∧ ∀𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦))))
371367, 370mtbird 328 . 2 (𝜑 → ¬ 𝑥 ∈ (𝐹 lim 𝐵))
372371eq0rdv 4312 1 (𝜑 → (𝐹 lim 𝐵) = ∅)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 399   ∧ w3a 1084   = wceq 1538   ∈ wcel 2111   ≠ wne 2987  ∀wral 3106  ∃wrex 3107   ∖ cdif 3878   ∩ cin 3880   ⊆ wss 3881  ∅c0 4243  ifcif 4425  {csn 4525  ∪ cuni 4800   class class class wbr 5030  ran crn 5520   ↾ cres 5521  ⟶wf 6320  ‘cfv 6324  (class class class)co 7135  ℂcc 10526  ℝcr 10527  0cc0 10528   + caddc 10531   · cmul 10533  +∞cpnf 10663  -∞cmnf 10664   < clt 10666   ≤ cle 10667   − cmin 10861   / cdiv 11288  4c4 11684  ℝ+crp 12379  (,)cioo 12728  abscabs 14587   ↾t crest 16688  TopOpenctopn 16689  topGenctg 16705  ℂfldccnfld 20094  Topctop 21505  limPtclp 21746   limℂ climc 24472 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-rep 5154  ax-sep 5167  ax-nul 5174  ax-pow 5231  ax-pr 5295  ax-un 7443  ax-cnex 10584  ax-resscn 10585  ax-1cn 10586  ax-icn 10587  ax-addcl 10588  ax-addrcl 10589  ax-mulcl 10590  ax-mulrcl 10591  ax-mulcom 10592  ax-addass 10593  ax-mulass 10594  ax-distr 10595  ax-i2m1 10596  ax-1ne0 10597  ax-1rid 10598  ax-rnegex 10599  ax-rrecex 10600  ax-cnre 10601  ax-pre-lttri 10602  ax-pre-lttrn 10603  ax-pre-ltadd 10604  ax-pre-mulgt0 10605  ax-pre-sup 10606 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-nel 3092  df-ral 3111  df-rex 3112  df-reu 3113  df-rmo 3114  df-rab 3115  df-v 3443  df-sbc 3721  df-csb 3829  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-pss 3900  df-nul 4244  df-if 4426  df-pw 4499  df-sn 4526  df-pr 4528  df-tp 4530  df-op 4532  df-uni 4801  df-int 4839  df-iun 4883  df-iin 4884  df-br 5031  df-opab 5093  df-mpt 5111  df-tr 5137  df-id 5425  df-eprel 5430  df-po 5438  df-so 5439  df-fr 5478  df-we 5480  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-rn 5530  df-res 5531  df-ima 5532  df-pred 6116  df-ord 6162  df-on 6163  df-lim 6164  df-suc 6165  df-iota 6283  df-fun 6326  df-fn 6327  df-f 6328  df-f1 6329  df-fo 6330  df-f1o 6331  df-fv 6332  df-riota 7093  df-ov 7138  df-oprab 7139  df-mpo 7140  df-om 7563  df-1st 7673  df-2nd 7674  df-wrecs 7932  df-recs 7993  df-rdg 8031  df-1o 8087  df-oadd 8091  df-er 8274  df-map 8393  df-pm 8394  df-en 8495  df-dom 8496  df-sdom 8497  df-fin 8498  df-fi 8861  df-sup 8892  df-inf 8893  df-pnf 10668  df-mnf 10669  df-xr 10670  df-ltxr 10671  df-le 10672  df-sub 10863  df-neg 10864  df-div 11289  df-nn 11628  df-2 11690  df-3 11691  df-4 11692  df-5 11693  df-6 11694  df-7 11695  df-8 11696  df-9 11697  df-n0 11888  df-z 11972  df-dec 12089  df-uz 12234  df-q 12339  df-rp 12380  df-xneg 12497  df-xadd 12498  df-xmul 12499  df-ioo 12732  df-fz 12888  df-seq 13367  df-exp 13428  df-cj 14452  df-re 14453  df-im 14454  df-sqrt 14588  df-abs 14589  df-struct 16479  df-ndx 16480  df-slot 16481  df-base 16483  df-plusg 16572  df-mulr 16573  df-starv 16574  df-tset 16578  df-ple 16579  df-ds 16581  df-unif 16582  df-rest 16690  df-topn 16691  df-topgen 16711  df-psmet 20086  df-xmet 20087  df-met 20088  df-bl 20089  df-mopn 20090  df-cnfld 20095  df-top 21506  df-topon 21523  df-topsp 21545  df-bases 21558  df-cld 21631  df-ntr 21632  df-cls 21633  df-nei 21710  df-lp 21748  df-cnp 21840  df-xms 22934  df-ms 22935  df-limc 24476 This theorem is referenced by:  limclr  42312  jumpncnp  42555
 Copyright terms: Public domain W3C validator