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 39310
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 23558 . . . . . . . . . . . . 13 ((𝐹 ↾ (𝐵(,)+∞)) lim 𝐵) ⊆ ℂ
2 limclner.r . . . . . . . . . . . . 13 (𝜑𝑅 ∈ ((𝐹 ↾ (𝐵(,)+∞)) lim 𝐵))
31, 2sseldi 3585 . . . . . . . . . . . 12 (𝜑𝑅 ∈ ℂ)
43ad2antrr 761 . . . . . . . . . . 11 (((𝜑𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) → 𝑅 ∈ ℂ)
5 limccl 23558 . . . . . . . . . . . . 13 ((𝐹 ↾ (-∞(,)𝐵)) lim 𝐵) ⊆ ℂ
6 limclner.l . . . . . . . . . . . . 13 (𝜑𝐿 ∈ ((𝐹 ↾ (-∞(,)𝐵)) lim 𝐵))
75, 6sseldi 3585 . . . . . . . . . . . 12 (𝜑𝐿 ∈ ℂ)
87ad2antrr 761 . . . . . . . . . . 11 (((𝜑𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) → 𝐿 ∈ ℂ)
94, 8subcld 10343 . . . . . . . . . 10 (((𝜑𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) → (𝑅𝐿) ∈ ℂ)
10 limclner.lner . . . . . . . . . . . . 13 (𝜑𝐿𝑅)
1110necomd 2845 . . . . . . . . . . . 12 (𝜑𝑅𝐿)
1211ad2antrr 761 . . . . . . . . . . 11 (((𝜑𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) → 𝑅𝐿)
134, 8, 12subne0d 10352 . . . . . . . . . 10 (((𝜑𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) → (𝑅𝐿) ≠ 0)
149, 13absrpcld 14128 . . . . . . . . 9 (((𝜑𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) → (abs‘(𝑅𝐿)) ∈ ℝ+)
15 4re 11048 . . . . . . . . . . 11 4 ∈ ℝ
16 4pos 11067 . . . . . . . . . . 11 0 < 4
1715, 16elrpii 11786 . . . . . . . . . 10 4 ∈ ℝ+
1817a1i 11 . . . . . . . . 9 (((𝜑𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) → 4 ∈ ℝ+)
1914, 18rpdivcld 11840 . . . . . . . 8 (((𝜑𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) → ((abs‘(𝑅𝐿)) / 4) ∈ ℝ+)
20 nfv 1840 . . . . . . . . . . 11 𝑦(𝜑𝑥 ∈ ℂ)
21 nfra1 2936 . . . . . . . . . . 11 𝑦𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)
2220, 21nfan 1825 . . . . . . . . . 10 𝑦((𝜑𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦))
23 nfv 1840 . . . . . . . . . 10 𝑦(((abs‘(𝑅𝐿)) / 4) ∈ ℝ+ → ∃𝑎𝐴𝑏𝐴 (abs‘(𝑅𝐿)) < (4 · ((abs‘(𝑅𝐿)) / 4)))
2422, 23nfim 1822 . . . . . . . . 9 𝑦(((𝜑𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) → (((abs‘(𝑅𝐿)) / 4) ∈ ℝ+ → ∃𝑎𝐴𝑏𝐴 (abs‘(𝑅𝐿)) < (4 · ((abs‘(𝑅𝐿)) / 4))))
25 ovex 6638 . . . . . . . . 9 ((abs‘(𝑅𝐿)) / 4) ∈ V
26 eleq1 2686 . . . . . . . . . . 11 (𝑦 = ((abs‘(𝑅𝐿)) / 4) → (𝑦 ∈ ℝ+ ↔ ((abs‘(𝑅𝐿)) / 4) ∈ ℝ+))
27 oveq2 6618 . . . . . . . . . . . . 13 (𝑦 = ((abs‘(𝑅𝐿)) / 4) → (4 · 𝑦) = (4 · ((abs‘(𝑅𝐿)) / 4)))
2827breq2d 4630 . . . . . . . . . . . 12 (𝑦 = ((abs‘(𝑅𝐿)) / 4) → ((abs‘(𝑅𝐿)) < (4 · 𝑦) ↔ (abs‘(𝑅𝐿)) < (4 · ((abs‘(𝑅𝐿)) / 4))))
29282rexbidv 3051 . . . . . . . . . . 11 (𝑦 = ((abs‘(𝑅𝐿)) / 4) → (∃𝑎𝐴𝑏𝐴 (abs‘(𝑅𝐿)) < (4 · 𝑦) ↔ ∃𝑎𝐴𝑏𝐴 (abs‘(𝑅𝐿)) < (4 · ((abs‘(𝑅𝐿)) / 4))))
3026, 29imbi12d 334 . . . . . . . . . 10 (𝑦 = ((abs‘(𝑅𝐿)) / 4) → ((𝑦 ∈ ℝ+ → ∃𝑎𝐴𝑏𝐴 (abs‘(𝑅𝐿)) < (4 · 𝑦)) ↔ (((abs‘(𝑅𝐿)) / 4) ∈ ℝ+ → ∃𝑎𝐴𝑏𝐴 (abs‘(𝑅𝐿)) < (4 · ((abs‘(𝑅𝐿)) / 4)))))
3130imbi2d 330 . . . . . . . . 9 (𝑦 = ((abs‘(𝑅𝐿)) / 4) → ((((𝜑𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) → (𝑦 ∈ ℝ+ → ∃𝑎𝐴𝑏𝐴 (abs‘(𝑅𝐿)) < (4 · 𝑦))) ↔ (((𝜑𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) → (((abs‘(𝑅𝐿)) / 4) ∈ ℝ+ → ∃𝑎𝐴𝑏𝐴 (abs‘(𝑅𝐿)) < (4 · ((abs‘(𝑅𝐿)) / 4))))))
32 simpll 789 . . . . . . . . . . 11 ((((𝜑𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ 𝑦 ∈ ℝ+) → (𝜑𝑥 ∈ ℂ))
33 simpr 477 . . . . . . . . . . 11 ((((𝜑𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ 𝑦 ∈ ℝ+) → 𝑦 ∈ ℝ+)
34 rspa 2925 . . . . . . . . . . . 12 ((∀𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦) ∧ 𝑦 ∈ ℝ+) → ∃𝑧 ∈ ℝ+𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦))
3534adantll 749 . . . . . . . . . . 11 ((((𝜑𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ 𝑦 ∈ ℝ+) → ∃𝑧 ∈ ℝ+𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦))
36 limclner.f . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑𝐹:𝐴⟶ℂ)
37 fresin 6035 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐹:𝐴⟶ℂ → (𝐹 ↾ (-∞(,)𝐵)):(𝐴 ∩ (-∞(,)𝐵))⟶ℂ)
3836, 37syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝐹 ↾ (-∞(,)𝐵)):(𝐴 ∩ (-∞(,)𝐵))⟶ℂ)
39 inss2 3817 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝐴 ∩ (-∞(,)𝐵)) ⊆ (-∞(,)𝐵)
40 ioosscn 39150 . . . . . . . . . . . . . . . . . . . . . . . 24 (-∞(,)𝐵) ⊆ ℂ
4139, 40sstri 3596 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐴 ∩ (-∞(,)𝐵)) ⊆ ℂ
4241a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝐴 ∩ (-∞(,)𝐵)) ⊆ ℂ)
43 limclner.j . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝐽 = (topGen‘ran (,))
44 retop 22484 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (topGen‘ran (,)) ∈ Top
4543, 44eqeltri 2694 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝐽 ∈ Top
46 ioossre 12184 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (-∞(,)𝐵) ⊆ ℝ
4739, 46sstri 3596 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝐴 ∩ (-∞(,)𝐵)) ⊆ ℝ
48 uniretop 22485 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ℝ = (topGen‘ran (,))
4943unieqi 4416 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 𝐽 = (topGen‘ran (,))
5048, 49eqtr4i 2646 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ℝ = 𝐽
5150lpss 20865 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐽 ∈ Top ∧ (𝐴 ∩ (-∞(,)𝐵)) ⊆ ℝ) → ((limPt‘𝐽)‘(𝐴 ∩ (-∞(,)𝐵))) ⊆ ℝ)
5245, 47, 51mp2an 707 . . . . . . . . . . . . . . . . . . . . . . . 24 ((limPt‘𝐽)‘(𝐴 ∩ (-∞(,)𝐵))) ⊆ ℝ
53 limclner.blp1 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑𝐵 ∈ ((limPt‘𝐽)‘(𝐴 ∩ (-∞(,)𝐵))))
5452, 53sseldi 3585 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑𝐵 ∈ ℝ)
5554recnd 10019 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑𝐵 ∈ ℂ)
5638, 42, 55ellimc3 23562 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝐿 ∈ ((𝐹 ↾ (-∞(,)𝐵)) lim 𝐵) ↔ (𝐿 ∈ ℂ ∧ ∀𝑦 ∈ ℝ+𝑣 ∈ ℝ+𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦))))
576, 56mpbid 222 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝐿 ∈ ℂ ∧ ∀𝑦 ∈ ℝ+𝑣 ∈ ℝ+𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)))
5857simprd 479 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ∀𝑦 ∈ ℝ+𝑣 ∈ ℝ+𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦))
5958r19.21bi 2927 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑦 ∈ ℝ+) → ∃𝑣 ∈ ℝ+𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦))
60593ad2ant1 1080 . . . . . . . . . . . . . . . . 17 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) → ∃𝑣 ∈ ℝ+𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦))
61 simp11l 1170 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) → 𝜑)
62 simp12 1090 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) → 𝑧 ∈ ℝ+)
63 simp2 1060 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) → 𝑣 ∈ ℝ+)
64 ifcl 4107 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑧 ∈ ℝ+𝑣 ∈ ℝ+) → if(𝑧𝑣, 𝑧, 𝑣) ∈ ℝ+)
65643adant1 1077 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑧 ∈ ℝ+𝑣 ∈ ℝ+) → if(𝑧𝑣, 𝑧, 𝑣) ∈ ℝ+)
66 inss1 3816 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((limPt‘𝐾)‘(𝐴 ∩ (-∞(,)𝐵))) ∩ ℝ) ⊆ ((limPt‘𝐾)‘(𝐴 ∩ (-∞(,)𝐵)))
6766a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → (((limPt‘𝐾)‘(𝐴 ∩ (-∞(,)𝐵))) ∩ ℝ) ⊆ ((limPt‘𝐾)‘(𝐴 ∩ (-∞(,)𝐵))))
68 limclner.k . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 𝐾 = (TopOpen‘ℂfld)
6968cnfldtop 22506 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 𝐾 ∈ Top
7069a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑𝐾 ∈ Top)
71 ax-resscn 9944 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ℝ ⊆ ℂ
7271a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑 → ℝ ⊆ ℂ)
7347a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑 → (𝐴 ∩ (-∞(,)𝐵)) ⊆ ℝ)
74 unicntop 22508 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ℂ = (TopOpen‘ℂfld)
7568unieqi 4416 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 𝐾 = (TopOpen‘ℂfld)
7674, 75eqtr4i 2646 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ℂ = 𝐾
7768tgioo2 22525 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (topGen‘ran (,)) = (𝐾t ℝ)
7843, 77eqtri 2643 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 𝐽 = (𝐾t ℝ)
7976, 78restlp 20906 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝐾 ∈ Top ∧ ℝ ⊆ ℂ ∧ (𝐴 ∩ (-∞(,)𝐵)) ⊆ ℝ) → ((limPt‘𝐽)‘(𝐴 ∩ (-∞(,)𝐵))) = (((limPt‘𝐾)‘(𝐴 ∩ (-∞(,)𝐵))) ∩ ℝ))
8070, 72, 73, 79syl3anc 1323 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → ((limPt‘𝐽)‘(𝐴 ∩ (-∞(,)𝐵))) = (((limPt‘𝐾)‘(𝐴 ∩ (-∞(,)𝐵))) ∩ ℝ))
8168eqcomi 2630 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (TopOpen‘ℂfld) = 𝐾
8281fveq2i 6156 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (limPt‘(TopOpen‘ℂfld)) = (limPt‘𝐾)
8382fveq1i 6154 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((limPt‘(TopOpen‘ℂfld))‘(𝐴 ∩ (-∞(,)𝐵))) = ((limPt‘𝐾)‘(𝐴 ∩ (-∞(,)𝐵)))
8483a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → ((limPt‘(TopOpen‘ℂfld))‘(𝐴 ∩ (-∞(,)𝐵))) = ((limPt‘𝐾)‘(𝐴 ∩ (-∞(,)𝐵))))
8567, 80, 843sstr4d 3632 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → ((limPt‘𝐽)‘(𝐴 ∩ (-∞(,)𝐵))) ⊆ ((limPt‘(TopOpen‘ℂfld))‘(𝐴 ∩ (-∞(,)𝐵))))
8685, 53sseldd 3588 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑𝐵 ∈ ((limPt‘(TopOpen‘ℂfld))‘(𝐴 ∩ (-∞(,)𝐵))))
8742, 55islpcn 39298 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → (𝐵 ∈ ((limPt‘(TopOpen‘ℂfld))‘(𝐴 ∩ (-∞(,)𝐵))) ↔ ∀𝑢 ∈ ℝ+𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵})(abs‘(𝑎𝐵)) < 𝑢))
8886, 87mpbid 222 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → ∀𝑢 ∈ ℝ+𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵})(abs‘(𝑎𝐵)) < 𝑢)
89883ad2ant1 1080 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑧 ∈ ℝ+𝑣 ∈ ℝ+) → ∀𝑢 ∈ ℝ+𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵})(abs‘(𝑎𝐵)) < 𝑢)
90 breq2 4622 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑢 = if(𝑧𝑣, 𝑧, 𝑣) → ((abs‘(𝑎𝐵)) < 𝑢 ↔ (abs‘(𝑎𝐵)) < if(𝑧𝑣, 𝑧, 𝑣)))
9190rexbidv 3046 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑢 = if(𝑧𝑣, 𝑧, 𝑣) → (∃𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵})(abs‘(𝑎𝐵)) < 𝑢 ↔ ∃𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵})(abs‘(𝑎𝐵)) < if(𝑧𝑣, 𝑧, 𝑣)))
9291rspcva 3296 . . . . . . . . . . . . . . . . . . . . . . 23 ((if(𝑧𝑣, 𝑧, 𝑣) ∈ ℝ+ ∧ ∀𝑢 ∈ ℝ+𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵})(abs‘(𝑎𝐵)) < 𝑢) → ∃𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵})(abs‘(𝑎𝐵)) < if(𝑧𝑣, 𝑧, 𝑣))
9365, 89, 92syl2anc 692 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑧 ∈ ℝ+𝑣 ∈ ℝ+) → ∃𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵})(abs‘(𝑎𝐵)) < if(𝑧𝑣, 𝑧, 𝑣))
94 eldifi 3715 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵}) → 𝑎 ∈ (𝐴 ∩ (-∞(,)𝐵)))
9547, 94sseldi 3585 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵}) → 𝑎 ∈ ℝ)
9672sselda 3587 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑𝑎 ∈ ℝ) → 𝑎 ∈ ℂ)
9755adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑𝑎 ∈ ℝ) → 𝐵 ∈ ℂ)
9896, 97subcld 10343 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑𝑎 ∈ ℝ) → (𝑎𝐵) ∈ ℂ)
9998abscld 14116 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑎 ∈ ℝ) → (abs‘(𝑎𝐵)) ∈ ℝ)
100993ad2antl1 1221 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑𝑧 ∈ ℝ+𝑣 ∈ ℝ+) ∧ 𝑎 ∈ ℝ) → (abs‘(𝑎𝐵)) ∈ ℝ)
101100adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑𝑧 ∈ ℝ+𝑣 ∈ ℝ+) ∧ 𝑎 ∈ ℝ) ∧ (abs‘(𝑎𝐵)) < if(𝑧𝑣, 𝑧, 𝑣)) → (abs‘(𝑎𝐵)) ∈ ℝ)
10265rpred 11823 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑧 ∈ ℝ+𝑣 ∈ ℝ+) → if(𝑧𝑣, 𝑧, 𝑣) ∈ ℝ)
103102ad2antrr 761 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑𝑧 ∈ ℝ+𝑣 ∈ ℝ+) ∧ 𝑎 ∈ ℝ) ∧ (abs‘(𝑎𝐵)) < if(𝑧𝑣, 𝑧, 𝑣)) → if(𝑧𝑣, 𝑧, 𝑣) ∈ ℝ)
104 rpre 11790 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑧 ∈ ℝ+𝑧 ∈ ℝ)
1051043ad2ant2 1081 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑧 ∈ ℝ+𝑣 ∈ ℝ+) → 𝑧 ∈ ℝ)
106105ad2antrr 761 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑𝑧 ∈ ℝ+𝑣 ∈ ℝ+) ∧ 𝑎 ∈ ℝ) ∧ (abs‘(𝑎𝐵)) < if(𝑧𝑣, 𝑧, 𝑣)) → 𝑧 ∈ ℝ)
107 simpr 477 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑𝑧 ∈ ℝ+𝑣 ∈ ℝ+) ∧ 𝑎 ∈ ℝ) ∧ (abs‘(𝑎𝐵)) < if(𝑧𝑣, 𝑧, 𝑣)) → (abs‘(𝑎𝐵)) < if(𝑧𝑣, 𝑧, 𝑣))
108 rpre 11790 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑣 ∈ ℝ+𝑣 ∈ ℝ)
109 min1 11970 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑧 ∈ ℝ ∧ 𝑣 ∈ ℝ) → if(𝑧𝑣, 𝑧, 𝑣) ≤ 𝑧)
110104, 108, 109syl2an 494 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑧 ∈ ℝ+𝑣 ∈ ℝ+) → if(𝑧𝑣, 𝑧, 𝑣) ≤ 𝑧)
1111103adant1 1077 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑧 ∈ ℝ+𝑣 ∈ ℝ+) → if(𝑧𝑣, 𝑧, 𝑣) ≤ 𝑧)
112111ad2antrr 761 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑𝑧 ∈ ℝ+𝑣 ∈ ℝ+) ∧ 𝑎 ∈ ℝ) ∧ (abs‘(𝑎𝐵)) < if(𝑧𝑣, 𝑧, 𝑣)) → if(𝑧𝑣, 𝑧, 𝑣) ≤ 𝑧)
113101, 103, 106, 107, 112ltletrd 10148 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑𝑧 ∈ ℝ+𝑣 ∈ ℝ+) ∧ 𝑎 ∈ ℝ) ∧ (abs‘(𝑎𝐵)) < if(𝑧𝑣, 𝑧, 𝑣)) → (abs‘(𝑎𝐵)) < 𝑧)
114108adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑧 ∈ ℝ+𝑣 ∈ ℝ+) → 𝑣 ∈ ℝ)
1151143adant1 1077 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑧 ∈ ℝ+𝑣 ∈ ℝ+) → 𝑣 ∈ ℝ)
116115ad2antrr 761 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑𝑧 ∈ ℝ+𝑣 ∈ ℝ+) ∧ 𝑎 ∈ ℝ) ∧ (abs‘(𝑎𝐵)) < if(𝑧𝑣, 𝑧, 𝑣)) → 𝑣 ∈ ℝ)
117 min2 11971 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑧 ∈ ℝ ∧ 𝑣 ∈ ℝ) → if(𝑧𝑣, 𝑧, 𝑣) ≤ 𝑣)
118104, 108, 117syl2an 494 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑧 ∈ ℝ+𝑣 ∈ ℝ+) → if(𝑧𝑣, 𝑧, 𝑣) ≤ 𝑣)
1191183adant1 1077 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑧 ∈ ℝ+𝑣 ∈ ℝ+) → if(𝑧𝑣, 𝑧, 𝑣) ≤ 𝑣)
120119ad2antrr 761 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑𝑧 ∈ ℝ+𝑣 ∈ ℝ+) ∧ 𝑎 ∈ ℝ) ∧ (abs‘(𝑎𝐵)) < if(𝑧𝑣, 𝑧, 𝑣)) → if(𝑧𝑣, 𝑧, 𝑣) ≤ 𝑣)
121101, 103, 116, 107, 120ltletrd 10148 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑𝑧 ∈ ℝ+𝑣 ∈ ℝ+) ∧ 𝑎 ∈ ℝ) ∧ (abs‘(𝑎𝐵)) < if(𝑧𝑣, 𝑧, 𝑣)) → (abs‘(𝑎𝐵)) < 𝑣)
122113, 121jca 554 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑧 ∈ ℝ+𝑣 ∈ ℝ+) ∧ 𝑎 ∈ ℝ) ∧ (abs‘(𝑎𝐵)) < if(𝑧𝑣, 𝑧, 𝑣)) → ((abs‘(𝑎𝐵)) < 𝑧 ∧ (abs‘(𝑎𝐵)) < 𝑣))
123122ex 450 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑧 ∈ ℝ+𝑣 ∈ ℝ+) ∧ 𝑎 ∈ ℝ) → ((abs‘(𝑎𝐵)) < if(𝑧𝑣, 𝑧, 𝑣) → ((abs‘(𝑎𝐵)) < 𝑧 ∧ (abs‘(𝑎𝐵)) < 𝑣)))
12495, 123sylan2 491 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑧 ∈ ℝ+𝑣 ∈ ℝ+) ∧ 𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵})) → ((abs‘(𝑎𝐵)) < if(𝑧𝑣, 𝑧, 𝑣) → ((abs‘(𝑎𝐵)) < 𝑧 ∧ (abs‘(𝑎𝐵)) < 𝑣)))
125124reximdva 3012 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑧 ∈ ℝ+𝑣 ∈ ℝ+) → (∃𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵})(abs‘(𝑎𝐵)) < if(𝑧𝑣, 𝑧, 𝑣) → ∃𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵})((abs‘(𝑎𝐵)) < 𝑧 ∧ (abs‘(𝑎𝐵)) < 𝑣)))
12693, 125mpd 15 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑧 ∈ ℝ+𝑣 ∈ ℝ+) → ∃𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵})((abs‘(𝑎𝐵)) < 𝑧 ∧ (abs‘(𝑎𝐵)) < 𝑣))
12761, 62, 63, 126syl3anc 1323 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) → ∃𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵})((abs‘(𝑎𝐵)) < 𝑧 ∧ (abs‘(𝑎𝐵)) < 𝑣))
128 nfv 1840 . . . . . . . . . . . . . . . . . . . . 21 𝑎(((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦))
129 nfre1 3000 . . . . . . . . . . . . . . . . . . . . 21 𝑎𝑎𝐴 ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)
130 inss1 3816 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝐴 ∩ (-∞(,)𝐵)) ⊆ 𝐴
131130, 94sseldi 3585 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵}) → 𝑎𝐴)
1321313ad2ant2 1081 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) ∧ 𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵}) ∧ ((abs‘(𝑎𝐵)) < 𝑧 ∧ (abs‘(𝑎𝐵)) < 𝑣)) → 𝑎𝐴)
133 simp113 1190 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) ∧ 𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵}) ∧ ((abs‘(𝑎𝐵)) < 𝑧 ∧ (abs‘(𝑎𝐵)) < 𝑣)) → ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦))
134 eldifsni 4294 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵}) → 𝑎𝐵)
135134adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵}) ∧ ((abs‘(𝑎𝐵)) < 𝑧 ∧ (abs‘(𝑎𝐵)) < 𝑣)) → 𝑎𝐵)
136 simprl 793 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵}) ∧ ((abs‘(𝑎𝐵)) < 𝑧 ∧ (abs‘(𝑎𝐵)) < 𝑣)) → (abs‘(𝑎𝐵)) < 𝑧)
137135, 136jca 554 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵}) ∧ ((abs‘(𝑎𝐵)) < 𝑧 ∧ (abs‘(𝑎𝐵)) < 𝑣)) → (𝑎𝐵 ∧ (abs‘(𝑎𝐵)) < 𝑧))
1381373adant1 1077 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) ∧ 𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵}) ∧ ((abs‘(𝑎𝐵)) < 𝑧 ∧ (abs‘(𝑎𝐵)) < 𝑣)) → (𝑎𝐵 ∧ (abs‘(𝑎𝐵)) < 𝑧))
139 neeq1 2852 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑤 = 𝑎 → (𝑤𝐵𝑎𝐵))
140 oveq1 6617 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑤 = 𝑎 → (𝑤𝐵) = (𝑎𝐵))
141140fveq2d 6157 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑤 = 𝑎 → (abs‘(𝑤𝐵)) = (abs‘(𝑎𝐵)))
142141breq1d 4628 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑤 = 𝑎 → ((abs‘(𝑤𝐵)) < 𝑧 ↔ (abs‘(𝑎𝐵)) < 𝑧))
143139, 142anbi12d 746 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑤 = 𝑎 → ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) ↔ (𝑎𝐵 ∧ (abs‘(𝑎𝐵)) < 𝑧)))
144 fveq2 6153 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑤 = 𝑎 → (𝐹𝑤) = (𝐹𝑎))
145144oveq1d 6625 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑤 = 𝑎 → ((𝐹𝑤) − 𝑥) = ((𝐹𝑎) − 𝑥))
146145fveq2d 6157 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑤 = 𝑎 → (abs‘((𝐹𝑤) − 𝑥)) = (abs‘((𝐹𝑎) − 𝑥)))
147146breq1d 4628 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑤 = 𝑎 → ((abs‘((𝐹𝑤) − 𝑥)) < 𝑦 ↔ (abs‘((𝐹𝑎) − 𝑥)) < 𝑦))
148143, 147imbi12d 334 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑤 = 𝑎 → (((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦) ↔ ((𝑎𝐵 ∧ (abs‘(𝑎𝐵)) < 𝑧) → (abs‘((𝐹𝑎) − 𝑥)) < 𝑦)))
149148rspcva 3296 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑎𝐴 ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) → ((𝑎𝐵 ∧ (abs‘(𝑎𝐵)) < 𝑧) → (abs‘((𝐹𝑎) − 𝑥)) < 𝑦))
150149imp 445 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑎𝐴 ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ (𝑎𝐵 ∧ (abs‘(𝑎𝐵)) < 𝑧)) → (abs‘((𝐹𝑎) − 𝑥)) < 𝑦)
151132, 133, 138, 150syl21anc 1322 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) ∧ 𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵}) ∧ ((abs‘(𝑎𝐵)) < 𝑧 ∧ (abs‘(𝑎𝐵)) < 𝑣)) → (abs‘((𝐹𝑎) − 𝑥)) < 𝑦)
152943ad2ant2 1081 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) ∧ 𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵}) ∧ ((abs‘(𝑎𝐵)) < 𝑧 ∧ (abs‘(𝑎𝐵)) < 𝑣)) → 𝑎 ∈ (𝐴 ∩ (-∞(,)𝐵)))
153613ad2ant1 1080 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) ∧ 𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵}) ∧ ((abs‘(𝑎𝐵)) < 𝑧 ∧ (abs‘(𝑎𝐵)) < 𝑣)) → 𝜑)
154 simp13 1091 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) ∧ 𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵}) ∧ ((abs‘(𝑎𝐵)) < 𝑧 ∧ (abs‘(𝑎𝐵)) < 𝑣)) → ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦))
155 nfv 1840 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 𝑤𝜑
156 nfra1 2936 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 𝑤𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)
157155, 156nfan 1825 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝑤(𝜑 ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦))
158 elinel2 3783 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵)) → 𝑤 ∈ (-∞(,)𝐵))
159 fvres 6169 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑤 ∈ (-∞(,)𝐵) → ((𝐹 ↾ (-∞(,)𝐵))‘𝑤) = (𝐹𝑤))
160158, 159syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵)) → ((𝐹 ↾ (-∞(,)𝐵))‘𝑤) = (𝐹𝑤))
161160eqcomd 2627 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵)) → (𝐹𝑤) = ((𝐹 ↾ (-∞(,)𝐵))‘𝑤))
162161oveq1d 6625 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵)) → ((𝐹𝑤) − 𝐿) = (((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿))
163162fveq2d 6157 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵)) → (abs‘((𝐹𝑤) − 𝐿)) = (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)))
1641633ad2ant2 1081 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑 ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) ∧ 𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵)) ∧ (𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣)) → (abs‘((𝐹𝑤) − 𝐿)) = (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)))
165 rspa 2925 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦) ∧ 𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))) → ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦))
1661653impia 1258 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦) ∧ 𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵)) ∧ (𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣)) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)
1671663adant1l 1315 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑 ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) ∧ 𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵)) ∧ (𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣)) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)
168164, 167eqbrtrd 4640 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑 ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) ∧ 𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵)) ∧ (𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣)) → (abs‘((𝐹𝑤) − 𝐿)) < 𝑦)
1691683exp 1261 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑 ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) → (𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵)) → ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘((𝐹𝑤) − 𝐿)) < 𝑦)))
170157, 169ralrimi 2952 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) → ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘((𝐹𝑤) − 𝐿)) < 𝑦))
171153, 154, 170syl2anc 692 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) ∧ 𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵}) ∧ ((abs‘(𝑎𝐵)) < 𝑧 ∧ (abs‘(𝑎𝐵)) < 𝑣)) → ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘((𝐹𝑤) − 𝐿)) < 𝑦))
172134anim1i 591 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵}) ∧ (abs‘(𝑎𝐵)) < 𝑣) → (𝑎𝐵 ∧ (abs‘(𝑎𝐵)) < 𝑣))
173172adantrl 751 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵}) ∧ ((abs‘(𝑎𝐵)) < 𝑧 ∧ (abs‘(𝑎𝐵)) < 𝑣)) → (𝑎𝐵 ∧ (abs‘(𝑎𝐵)) < 𝑣))
1741733adant1 1077 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) ∧ 𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵}) ∧ ((abs‘(𝑎𝐵)) < 𝑧 ∧ (abs‘(𝑎𝐵)) < 𝑣)) → (𝑎𝐵 ∧ (abs‘(𝑎𝐵)) < 𝑣))
175141breq1d 4628 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑤 = 𝑎 → ((abs‘(𝑤𝐵)) < 𝑣 ↔ (abs‘(𝑎𝐵)) < 𝑣))
176139, 175anbi12d 746 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑤 = 𝑎 → ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) ↔ (𝑎𝐵 ∧ (abs‘(𝑎𝐵)) < 𝑣)))
177144oveq1d 6625 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑤 = 𝑎 → ((𝐹𝑤) − 𝐿) = ((𝐹𝑎) − 𝐿))
178177fveq2d 6157 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑤 = 𝑎 → (abs‘((𝐹𝑤) − 𝐿)) = (abs‘((𝐹𝑎) − 𝐿)))
179178breq1d 4628 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑤 = 𝑎 → ((abs‘((𝐹𝑤) − 𝐿)) < 𝑦 ↔ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦))
180176, 179imbi12d 334 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑤 = 𝑎 → (((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘((𝐹𝑤) − 𝐿)) < 𝑦) ↔ ((𝑎𝐵 ∧ (abs‘(𝑎𝐵)) < 𝑣) → (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)))
181180rspcva 3296 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑎 ∈ (𝐴 ∩ (-∞(,)𝐵)) ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘((𝐹𝑤) − 𝐿)) < 𝑦)) → ((𝑎𝐵 ∧ (abs‘(𝑎𝐵)) < 𝑣) → (abs‘((𝐹𝑎) − 𝐿)) < 𝑦))
182181imp 445 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑎 ∈ (𝐴 ∩ (-∞(,)𝐵)) ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘((𝐹𝑤) − 𝐿)) < 𝑦)) ∧ (𝑎𝐵 ∧ (abs‘(𝑎𝐵)) < 𝑣)) → (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)
183152, 171, 174, 182syl21anc 1322 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) ∧ 𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵}) ∧ ((abs‘(𝑎𝐵)) < 𝑧 ∧ (abs‘(𝑎𝐵)) < 𝑣)) → (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)
184 rspe 2998 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑎𝐴 ∧ ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)) → ∃𝑎𝐴 ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦))
185132, 151, 183, 184syl12anc 1321 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) ∧ 𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵}) ∧ ((abs‘(𝑎𝐵)) < 𝑧 ∧ (abs‘(𝑎𝐵)) < 𝑣)) → ∃𝑎𝐴 ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦))
1861853exp 1261 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) → (𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵}) → (((abs‘(𝑎𝐵)) < 𝑧 ∧ (abs‘(𝑎𝐵)) < 𝑣) → ∃𝑎𝐴 ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦))))
187128, 129, 186rexlimd 3020 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) → (∃𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵})((abs‘(𝑎𝐵)) < 𝑧 ∧ (abs‘(𝑎𝐵)) < 𝑣) → ∃𝑎𝐴 ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)))
188127, 187mpd 15 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) → ∃𝑎𝐴 ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦))
1891883exp 1261 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) → (𝑣 ∈ ℝ+ → (∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦) → ∃𝑎𝐴 ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦))))
190189rexlimdv 3024 . . . . . . . . . . . . . . . . 17 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) → (∃𝑣 ∈ ℝ+𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦) → ∃𝑎𝐴 ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)))
19160, 190mpd 15 . . . . . . . . . . . . . . . 16 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) → ∃𝑎𝐴 ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦))
1921913exp 1261 . . . . . . . . . . . . . . 15 ((𝜑𝑦 ∈ ℝ+) → (𝑧 ∈ ℝ+ → (∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦) → ∃𝑎𝐴 ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦))))
193192rexlimdv 3024 . . . . . . . . . . . . . 14 ((𝜑𝑦 ∈ ℝ+) → (∃𝑧 ∈ ℝ+𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦) → ∃𝑎𝐴 ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)))
194193imp 445 . . . . . . . . . . . . 13 (((𝜑𝑦 ∈ ℝ+) ∧ ∃𝑧 ∈ ℝ+𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) → ∃𝑎𝐴 ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦))
195194adantllr 754 . . . . . . . . . . . 12 ((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ ∃𝑧 ∈ ℝ+𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) → ∃𝑎𝐴 ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦))
196 fresin 6035 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝐹:𝐴⟶ℂ → (𝐹 ↾ (𝐵(,)+∞)):(𝐴 ∩ (𝐵(,)+∞))⟶ℂ)
19736, 196syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → (𝐹 ↾ (𝐵(,)+∞)):(𝐴 ∩ (𝐵(,)+∞))⟶ℂ)
198 inss2 3817 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝐴 ∩ (𝐵(,)+∞)) ⊆ (𝐵(,)+∞)
199 ioosscn 39150 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝐵(,)+∞) ⊆ ℂ
200198, 199sstri 3596 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝐴 ∩ (𝐵(,)+∞)) ⊆ ℂ
201200a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → (𝐴 ∩ (𝐵(,)+∞)) ⊆ ℂ)
202197, 201, 55ellimc3 23562 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → (𝑅 ∈ ((𝐹 ↾ (𝐵(,)+∞)) lim 𝐵) ↔ (𝑅 ∈ ℂ ∧ ∀𝑦 ∈ ℝ+𝑣 ∈ ℝ+𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦))))
2032, 202mpbid 222 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (𝑅 ∈ ℂ ∧ ∀𝑦 ∈ ℝ+𝑣 ∈ ℝ+𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)))
204203simprd 479 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → ∀𝑦 ∈ ℝ+𝑣 ∈ ℝ+𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦))
205204r19.21bi 2927 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑦 ∈ ℝ+) → ∃𝑣 ∈ ℝ+𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦))
2062053ad2ant1 1080 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) → ∃𝑣 ∈ ℝ+𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦))
207 simp11l 1170 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) → 𝜑)
208 simp12 1090 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) → 𝑧 ∈ ℝ+)
209 simp2 1060 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) → 𝑣 ∈ ℝ+)
210 inss1 3816 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((limPt‘𝐾)‘(𝐴 ∩ (𝐵(,)+∞))) ∩ ℝ) ⊆ ((limPt‘𝐾)‘(𝐴 ∩ (𝐵(,)+∞)))
211210a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝜑 → (((limPt‘𝐾)‘(𝐴 ∩ (𝐵(,)+∞))) ∩ ℝ) ⊆ ((limPt‘𝐾)‘(𝐴 ∩ (𝐵(,)+∞))))
212 ioossre 12184 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝐵(,)+∞) ⊆ ℝ
213198, 212sstri 3596 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝐴 ∩ (𝐵(,)+∞)) ⊆ ℝ
214213a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝜑 → (𝐴 ∩ (𝐵(,)+∞)) ⊆ ℝ)
21576, 78restlp 20906 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝐾 ∈ Top ∧ ℝ ⊆ ℂ ∧ (𝐴 ∩ (𝐵(,)+∞)) ⊆ ℝ) → ((limPt‘𝐽)‘(𝐴 ∩ (𝐵(,)+∞))) = (((limPt‘𝐾)‘(𝐴 ∩ (𝐵(,)+∞))) ∩ ℝ))
21670, 72, 214, 215syl3anc 1323 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝜑 → ((limPt‘𝐽)‘(𝐴 ∩ (𝐵(,)+∞))) = (((limPt‘𝐾)‘(𝐴 ∩ (𝐵(,)+∞))) ∩ ℝ))
21782fveq1i 6154 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((limPt‘(TopOpen‘ℂfld))‘(𝐴 ∩ (𝐵(,)+∞))) = ((limPt‘𝐾)‘(𝐴 ∩ (𝐵(,)+∞)))
218217a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝜑 → ((limPt‘(TopOpen‘ℂfld))‘(𝐴 ∩ (𝐵(,)+∞))) = ((limPt‘𝐾)‘(𝐴 ∩ (𝐵(,)+∞))))
219211, 216, 2183sstr4d 3632 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝜑 → ((limPt‘𝐽)‘(𝐴 ∩ (𝐵(,)+∞))) ⊆ ((limPt‘(TopOpen‘ℂfld))‘(𝐴 ∩ (𝐵(,)+∞))))
220 limclner.blp2 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝜑𝐵 ∈ ((limPt‘𝐽)‘(𝐴 ∩ (𝐵(,)+∞))))
221219, 220sseldd 3588 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝜑𝐵 ∈ ((limPt‘(TopOpen‘ℂfld))‘(𝐴 ∩ (𝐵(,)+∞))))
222201, 55islpcn 39298 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝜑 → (𝐵 ∈ ((limPt‘(TopOpen‘ℂfld))‘(𝐴 ∩ (𝐵(,)+∞))) ↔ ∀𝑢 ∈ ℝ+𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵})(abs‘(𝑏𝐵)) < 𝑢))
223221, 222mpbid 222 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑 → ∀𝑢 ∈ ℝ+𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵})(abs‘(𝑏𝐵)) < 𝑢)
2242233ad2ant1 1080 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑧 ∈ ℝ+𝑣 ∈ ℝ+) → ∀𝑢 ∈ ℝ+𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵})(abs‘(𝑏𝐵)) < 𝑢)
225 breq2 4622 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑢 = if(𝑧𝑣, 𝑧, 𝑣) → ((abs‘(𝑏𝐵)) < 𝑢 ↔ (abs‘(𝑏𝐵)) < if(𝑧𝑣, 𝑧, 𝑣)))
226225rexbidv 3046 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑢 = if(𝑧𝑣, 𝑧, 𝑣) → (∃𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵})(abs‘(𝑏𝐵)) < 𝑢 ↔ ∃𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵})(abs‘(𝑏𝐵)) < if(𝑧𝑣, 𝑧, 𝑣)))
227226rspcva 3296 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((if(𝑧𝑣, 𝑧, 𝑣) ∈ ℝ+ ∧ ∀𝑢 ∈ ℝ+𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵})(abs‘(𝑏𝐵)) < 𝑢) → ∃𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵})(abs‘(𝑏𝐵)) < if(𝑧𝑣, 𝑧, 𝑣))
22865, 224, 227syl2anc 692 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑧 ∈ ℝ+𝑣 ∈ ℝ+) → ∃𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵})(abs‘(𝑏𝐵)) < if(𝑧𝑣, 𝑧, 𝑣))
229 eldifi 3715 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵}) → 𝑏 ∈ (𝐴 ∩ (𝐵(,)+∞)))
230213, 229sseldi 3585 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵}) → 𝑏 ∈ ℝ)
23172sselda 3587 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝜑𝑏 ∈ ℝ) → 𝑏 ∈ ℂ)
23255adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝜑𝑏 ∈ ℝ) → 𝐵 ∈ ℂ)
233231, 232subcld 10343 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝜑𝑏 ∈ ℝ) → (𝑏𝐵) ∈ ℂ)
234233abscld 14116 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝜑𝑏 ∈ ℝ) → (abs‘(𝑏𝐵)) ∈ ℝ)
2352343ad2antl1 1221 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝜑𝑧 ∈ ℝ+𝑣 ∈ ℝ+) ∧ 𝑏 ∈ ℝ) → (abs‘(𝑏𝐵)) ∈ ℝ)
236235adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝜑𝑧 ∈ ℝ+𝑣 ∈ ℝ+) ∧ 𝑏 ∈ ℝ) ∧ (abs‘(𝑏𝐵)) < if(𝑧𝑣, 𝑧, 𝑣)) → (abs‘(𝑏𝐵)) ∈ ℝ)
237102ad2antrr 761 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝜑𝑧 ∈ ℝ+𝑣 ∈ ℝ+) ∧ 𝑏 ∈ ℝ) ∧ (abs‘(𝑏𝐵)) < if(𝑧𝑣, 𝑧, 𝑣)) → if(𝑧𝑣, 𝑧, 𝑣) ∈ ℝ)
238105ad2antrr 761 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝜑𝑧 ∈ ℝ+𝑣 ∈ ℝ+) ∧ 𝑏 ∈ ℝ) ∧ (abs‘(𝑏𝐵)) < if(𝑧𝑣, 𝑧, 𝑣)) → 𝑧 ∈ ℝ)
239 simpr 477 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝜑𝑧 ∈ ℝ+𝑣 ∈ ℝ+) ∧ 𝑏 ∈ ℝ) ∧ (abs‘(𝑏𝐵)) < if(𝑧𝑣, 𝑧, 𝑣)) → (abs‘(𝑏𝐵)) < if(𝑧𝑣, 𝑧, 𝑣))
240111ad2antrr 761 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝜑𝑧 ∈ ℝ+𝑣 ∈ ℝ+) ∧ 𝑏 ∈ ℝ) ∧ (abs‘(𝑏𝐵)) < if(𝑧𝑣, 𝑧, 𝑣)) → if(𝑧𝑣, 𝑧, 𝑣) ≤ 𝑧)
241236, 237, 238, 239, 240ltletrd 10148 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝜑𝑧 ∈ ℝ+𝑣 ∈ ℝ+) ∧ 𝑏 ∈ ℝ) ∧ (abs‘(𝑏𝐵)) < if(𝑧𝑣, 𝑧, 𝑣)) → (abs‘(𝑏𝐵)) < 𝑧)
242115ad2antrr 761 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝜑𝑧 ∈ ℝ+𝑣 ∈ ℝ+) ∧ 𝑏 ∈ ℝ) ∧ (abs‘(𝑏𝐵)) < if(𝑧𝑣, 𝑧, 𝑣)) → 𝑣 ∈ ℝ)
243238, 242, 117syl2anc 692 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝜑𝑧 ∈ ℝ+𝑣 ∈ ℝ+) ∧ 𝑏 ∈ ℝ) ∧ (abs‘(𝑏𝐵)) < if(𝑧𝑣, 𝑧, 𝑣)) → if(𝑧𝑣, 𝑧, 𝑣) ≤ 𝑣)
244236, 237, 242, 239, 243ltletrd 10148 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝜑𝑧 ∈ ℝ+𝑣 ∈ ℝ+) ∧ 𝑏 ∈ ℝ) ∧ (abs‘(𝑏𝐵)) < if(𝑧𝑣, 𝑧, 𝑣)) → (abs‘(𝑏𝐵)) < 𝑣)
245241, 244jca 554 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑𝑧 ∈ ℝ+𝑣 ∈ ℝ+) ∧ 𝑏 ∈ ℝ) ∧ (abs‘(𝑏𝐵)) < if(𝑧𝑣, 𝑧, 𝑣)) → ((abs‘(𝑏𝐵)) < 𝑧 ∧ (abs‘(𝑏𝐵)) < 𝑣))
246245ex 450 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑𝑧 ∈ ℝ+𝑣 ∈ ℝ+) ∧ 𝑏 ∈ ℝ) → ((abs‘(𝑏𝐵)) < if(𝑧𝑣, 𝑧, 𝑣) → ((abs‘(𝑏𝐵)) < 𝑧 ∧ (abs‘(𝑏𝐵)) < 𝑣)))
247230, 246sylan2 491 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑧 ∈ ℝ+𝑣 ∈ ℝ+) ∧ 𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵})) → ((abs‘(𝑏𝐵)) < if(𝑧𝑣, 𝑧, 𝑣) → ((abs‘(𝑏𝐵)) < 𝑧 ∧ (abs‘(𝑏𝐵)) < 𝑣)))
248247reximdva 3012 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑧 ∈ ℝ+𝑣 ∈ ℝ+) → (∃𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵})(abs‘(𝑏𝐵)) < if(𝑧𝑣, 𝑧, 𝑣) → ∃𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵})((abs‘(𝑏𝐵)) < 𝑧 ∧ (abs‘(𝑏𝐵)) < 𝑣)))
249228, 248mpd 15 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑧 ∈ ℝ+𝑣 ∈ ℝ+) → ∃𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵})((abs‘(𝑏𝐵)) < 𝑧 ∧ (abs‘(𝑏𝐵)) < 𝑣))
250207, 208, 209, 249syl3anc 1323 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) → ∃𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵})((abs‘(𝑏𝐵)) < 𝑧 ∧ (abs‘(𝑏𝐵)) < 𝑣))
251 nfv 1840 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑏(((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦))
252 nfre1 3000 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑏𝑏𝐴 ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦)
253 inss1 3816 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝐴 ∩ (𝐵(,)+∞)) ⊆ 𝐴
254253, 229sseldi 3585 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵}) → 𝑏𝐴)
2552543ad2ant2 1081 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) ∧ 𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵}) ∧ ((abs‘(𝑏𝐵)) < 𝑧 ∧ (abs‘(𝑏𝐵)) < 𝑣)) → 𝑏𝐴)
256 simp113 1190 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) ∧ 𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵}) ∧ ((abs‘(𝑏𝐵)) < 𝑧 ∧ (abs‘(𝑏𝐵)) < 𝑣)) → ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦))
257 eldifsni 4294 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵}) → 𝑏𝐵)
258257adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵}) ∧ ((abs‘(𝑏𝐵)) < 𝑧 ∧ (abs‘(𝑏𝐵)) < 𝑣)) → 𝑏𝐵)
259 simprl 793 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵}) ∧ ((abs‘(𝑏𝐵)) < 𝑧 ∧ (abs‘(𝑏𝐵)) < 𝑣)) → (abs‘(𝑏𝐵)) < 𝑧)
260258, 259jca 554 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵}) ∧ ((abs‘(𝑏𝐵)) < 𝑧 ∧ (abs‘(𝑏𝐵)) < 𝑣)) → (𝑏𝐵 ∧ (abs‘(𝑏𝐵)) < 𝑧))
2612603adant1 1077 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) ∧ 𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵}) ∧ ((abs‘(𝑏𝐵)) < 𝑧 ∧ (abs‘(𝑏𝐵)) < 𝑣)) → (𝑏𝐵 ∧ (abs‘(𝑏𝐵)) < 𝑧))
262 neeq1 2852 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑤 = 𝑏 → (𝑤𝐵𝑏𝐵))
263 oveq1 6617 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑤 = 𝑏 → (𝑤𝐵) = (𝑏𝐵))
264263fveq2d 6157 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑤 = 𝑏 → (abs‘(𝑤𝐵)) = (abs‘(𝑏𝐵)))
265264breq1d 4628 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑤 = 𝑏 → ((abs‘(𝑤𝐵)) < 𝑧 ↔ (abs‘(𝑏𝐵)) < 𝑧))
266262, 265anbi12d 746 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑤 = 𝑏 → ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) ↔ (𝑏𝐵 ∧ (abs‘(𝑏𝐵)) < 𝑧)))
267 fveq2 6153 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑤 = 𝑏 → (𝐹𝑤) = (𝐹𝑏))
268267oveq1d 6625 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑤 = 𝑏 → ((𝐹𝑤) − 𝑥) = ((𝐹𝑏) − 𝑥))
269268fveq2d 6157 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑤 = 𝑏 → (abs‘((𝐹𝑤) − 𝑥)) = (abs‘((𝐹𝑏) − 𝑥)))
270269breq1d 4628 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑤 = 𝑏 → ((abs‘((𝐹𝑤) − 𝑥)) < 𝑦 ↔ (abs‘((𝐹𝑏) − 𝑥)) < 𝑦))
271266, 270imbi12d 334 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑤 = 𝑏 → (((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦) ↔ ((𝑏𝐵 ∧ (abs‘(𝑏𝐵)) < 𝑧) → (abs‘((𝐹𝑏) − 𝑥)) < 𝑦)))
272271rspcva 3296 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑏𝐴 ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) → ((𝑏𝐵 ∧ (abs‘(𝑏𝐵)) < 𝑧) → (abs‘((𝐹𝑏) − 𝑥)) < 𝑦))
273272imp 445 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝑏𝐴 ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ (𝑏𝐵 ∧ (abs‘(𝑏𝐵)) < 𝑧)) → (abs‘((𝐹𝑏) − 𝑥)) < 𝑦)
274255, 256, 261, 273syl21anc 1322 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) ∧ 𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵}) ∧ ((abs‘(𝑏𝐵)) < 𝑧 ∧ (abs‘(𝑏𝐵)) < 𝑣)) → (abs‘((𝐹𝑏) − 𝑥)) < 𝑦)
2752293ad2ant2 1081 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) ∧ 𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵}) ∧ ((abs‘(𝑏𝐵)) < 𝑧 ∧ (abs‘(𝑏𝐵)) < 𝑣)) → 𝑏 ∈ (𝐴 ∩ (𝐵(,)+∞)))
2762073ad2ant1 1080 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) ∧ 𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵}) ∧ ((abs‘(𝑏𝐵)) < 𝑧 ∧ (abs‘(𝑏𝐵)) < 𝑣)) → 𝜑)
277 simp13 1091 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) ∧ 𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵}) ∧ ((abs‘(𝑏𝐵)) < 𝑧 ∧ (abs‘(𝑏𝐵)) < 𝑣)) → ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦))
278 nfra1 2936 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 𝑤𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)
279155, 278nfan 1825 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 𝑤(𝜑 ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦))
280 elinel2 3783 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞)) → 𝑤 ∈ (𝐵(,)+∞))
281 fvres 6169 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑤 ∈ (𝐵(,)+∞) → ((𝐹 ↾ (𝐵(,)+∞))‘𝑤) = (𝐹𝑤))
282280, 281syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞)) → ((𝐹 ↾ (𝐵(,)+∞))‘𝑤) = (𝐹𝑤))
283282eqcomd 2627 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞)) → (𝐹𝑤) = ((𝐹 ↾ (𝐵(,)+∞))‘𝑤))
284283oveq1d 6625 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞)) → ((𝐹𝑤) − 𝑅) = (((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅))
285284fveq2d 6157 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞)) → (abs‘((𝐹𝑤) − 𝑅)) = (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)))
2862853ad2ant2 1081 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝜑 ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) ∧ 𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞)) ∧ (𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣)) → (abs‘((𝐹𝑤) − 𝑅)) = (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)))
287 rspa 2925 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦) ∧ 𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))) → ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦))
2882873impia 1258 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦) ∧ 𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞)) ∧ (𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣)) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)
2892883adant1l 1315 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝜑 ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) ∧ 𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞)) ∧ (𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣)) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)
290286, 289eqbrtrd 4640 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝜑 ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) ∧ 𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞)) ∧ (𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣)) → (abs‘((𝐹𝑤) − 𝑅)) < 𝑦)
2912903exp 1261 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑 ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) → (𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞)) → ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘((𝐹𝑤) − 𝑅)) < 𝑦)))
292279, 291ralrimi 2952 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑 ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) → ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘((𝐹𝑤) − 𝑅)) < 𝑦))
293276, 277, 292syl2anc 692 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) ∧ 𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵}) ∧ ((abs‘(𝑏𝐵)) < 𝑧 ∧ (abs‘(𝑏𝐵)) < 𝑣)) → ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘((𝐹𝑤) − 𝑅)) < 𝑦))
294257anim1i 591 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵}) ∧ (abs‘(𝑏𝐵)) < 𝑣) → (𝑏𝐵 ∧ (abs‘(𝑏𝐵)) < 𝑣))
295294adantrl 751 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵}) ∧ ((abs‘(𝑏𝐵)) < 𝑧 ∧ (abs‘(𝑏𝐵)) < 𝑣)) → (𝑏𝐵 ∧ (abs‘(𝑏𝐵)) < 𝑣))
2962953adant1 1077 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) ∧ 𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵}) ∧ ((abs‘(𝑏𝐵)) < 𝑧 ∧ (abs‘(𝑏𝐵)) < 𝑣)) → (𝑏𝐵 ∧ (abs‘(𝑏𝐵)) < 𝑣))
297264breq1d 4628 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑤 = 𝑏 → ((abs‘(𝑤𝐵)) < 𝑣 ↔ (abs‘(𝑏𝐵)) < 𝑣))
298262, 297anbi12d 746 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑤 = 𝑏 → ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) ↔ (𝑏𝐵 ∧ (abs‘(𝑏𝐵)) < 𝑣)))
299267oveq1d 6625 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑤 = 𝑏 → ((𝐹𝑤) − 𝑅) = ((𝐹𝑏) − 𝑅))
300299fveq2d 6157 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑤 = 𝑏 → (abs‘((𝐹𝑤) − 𝑅)) = (abs‘((𝐹𝑏) − 𝑅)))
301300breq1d 4628 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑤 = 𝑏 → ((abs‘((𝐹𝑤) − 𝑅)) < 𝑦 ↔ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦))
302298, 301imbi12d 334 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑤 = 𝑏 → (((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘((𝐹𝑤) − 𝑅)) < 𝑦) ↔ ((𝑏𝐵 ∧ (abs‘(𝑏𝐵)) < 𝑣) → (abs‘((𝐹𝑏) − 𝑅)) < 𝑦)))
303302rspcva 3296 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑏 ∈ (𝐴 ∩ (𝐵(,)+∞)) ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘((𝐹𝑤) − 𝑅)) < 𝑦)) → ((𝑏𝐵 ∧ (abs‘(𝑏𝐵)) < 𝑣) → (abs‘((𝐹𝑏) − 𝑅)) < 𝑦))
304303imp 445 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝑏 ∈ (𝐴 ∩ (𝐵(,)+∞)) ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘((𝐹𝑤) − 𝑅)) < 𝑦)) ∧ (𝑏𝐵 ∧ (abs‘(𝑏𝐵)) < 𝑣)) → (abs‘((𝐹𝑏) − 𝑅)) < 𝑦)
305275, 293, 296, 304syl21anc 1322 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) ∧ 𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵}) ∧ ((abs‘(𝑏𝐵)) < 𝑧 ∧ (abs‘(𝑏𝐵)) < 𝑣)) → (abs‘((𝐹𝑏) − 𝑅)) < 𝑦)
306 rspe 2998 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑏𝐴 ∧ ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦)) → ∃𝑏𝐴 ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦))
307255, 274, 305, 306syl12anc 1321 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) ∧ 𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵}) ∧ ((abs‘(𝑏𝐵)) < 𝑧 ∧ (abs‘(𝑏𝐵)) < 𝑣)) → ∃𝑏𝐴 ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦))
3083073exp 1261 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) → (𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵}) → (((abs‘(𝑏𝐵)) < 𝑧 ∧ (abs‘(𝑏𝐵)) < 𝑣) → ∃𝑏𝐴 ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦))))
309251, 252, 308rexlimd 3020 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) → (∃𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵})((abs‘(𝑏𝐵)) < 𝑧 ∧ (abs‘(𝑏𝐵)) < 𝑣) → ∃𝑏𝐴 ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦)))
310250, 309mpd 15 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) → ∃𝑏𝐴 ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦))
3113103exp 1261 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) → (𝑣 ∈ ℝ+ → (∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦) → ∃𝑏𝐴 ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦))))
312311rexlimdv 3024 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) → (∃𝑣 ∈ ℝ+𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦) → ∃𝑏𝐴 ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦)))
313206, 312mpd 15 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) → ∃𝑏𝐴 ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦))
3143133exp 1261 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑦 ∈ ℝ+) → (𝑧 ∈ ℝ+ → (∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦) → ∃𝑏𝐴 ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦))))
315314rexlimdv 3024 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑦 ∈ ℝ+) → (∃𝑧 ∈ ℝ+𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦) → ∃𝑏𝐴 ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦)))
316315imp 445 . . . . . . . . . . . . . . . . 17 (((𝜑𝑦 ∈ ℝ+) ∧ ∃𝑧 ∈ ℝ+𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) → ∃𝑏𝐴 ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦))
317316adantllr 754 . . . . . . . . . . . . . . . 16 ((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ ∃𝑧 ∈ ℝ+𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) → ∃𝑏𝐴 ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦))
318317ad2antrr 761 . . . . . . . . . . . . . . 15 ((((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ ∃𝑧 ∈ ℝ+𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ 𝑎𝐴) ∧ ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)) → ∃𝑏𝐴 ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦))
3193ad6antr 771 . . . . . . . . . . . . . . . . . . . . 21 (((((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎𝐴) ∧ ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏𝐴) ∧ ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦)) → 𝑅 ∈ ℂ)
3207ad6antr 771 . . . . . . . . . . . . . . . . . . . . 21 (((((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎𝐴) ∧ ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏𝐴) ∧ ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦)) → 𝐿 ∈ ℂ)
321319, 320subcld 10343 . . . . . . . . . . . . . . . . . . . 20 (((((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎𝐴) ∧ ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏𝐴) ∧ ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦)) → (𝑅𝐿) ∈ ℂ)
322321abscld 14116 . . . . . . . . . . . . . . . . . . 19 (((((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎𝐴) ∧ ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏𝐴) ∧ ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦)) → (abs‘(𝑅𝐿)) ∈ ℝ)
323 simp-6l 809 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎𝐴) ∧ ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏𝐴) ∧ ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦)) → 𝜑)
324 simplr 791 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎𝐴) ∧ ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏𝐴) ∧ ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦)) → 𝑏𝐴)
32536ffvelrnda 6320 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑏𝐴) → (𝐹𝑏) ∈ ℂ)
326323, 324, 325syl2anc 692 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎𝐴) ∧ ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏𝐴) ∧ ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦)) → (𝐹𝑏) ∈ ℂ)
327319, 326subcld 10343 . . . . . . . . . . . . . . . . . . . . . . 23 (((((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎𝐴) ∧ ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏𝐴) ∧ ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦)) → (𝑅 − (𝐹𝑏)) ∈ ℂ)
328327abscld 14116 . . . . . . . . . . . . . . . . . . . . . 22 (((((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎𝐴) ∧ ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏𝐴) ∧ ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦)) → (abs‘(𝑅 − (𝐹𝑏))) ∈ ℝ)
329 simp-6r 810 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎𝐴) ∧ ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏𝐴) ∧ ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦)) → 𝑥 ∈ ℂ)
330326, 329subcld 10343 . . . . . . . . . . . . . . . . . . . . . . 23 (((((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎𝐴) ∧ ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏𝐴) ∧ ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦)) → ((𝐹𝑏) − 𝑥) ∈ ℂ)
331330abscld 14116 . . . . . . . . . . . . . . . . . . . . . 22 (((((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎𝐴) ∧ ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏𝐴) ∧ ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦)) → (abs‘((𝐹𝑏) − 𝑥)) ∈ ℝ)
332328, 331readdcld 10020 . . . . . . . . . . . . . . . . . . . . 21 (((((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎𝐴) ∧ ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏𝐴) ∧ ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦)) → ((abs‘(𝑅 − (𝐹𝑏))) + (abs‘((𝐹𝑏) − 𝑥))) ∈ ℝ)
333 simp-4r 806 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎𝐴) ∧ ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏𝐴) ∧ ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦)) → 𝑎𝐴)
33436ffvelrnda 6320 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑎𝐴) → (𝐹𝑎) ∈ ℂ)
335323, 333, 334syl2anc 692 . . . . . . . . . . . . . . . . . . . . . . 23 (((((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎𝐴) ∧ ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏𝐴) ∧ ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦)) → (𝐹𝑎) ∈ ℂ)
336329, 335subcld 10343 . . . . . . . . . . . . . . . . . . . . . 22 (((((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎𝐴) ∧ ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏𝐴) ∧ ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦)) → (𝑥 − (𝐹𝑎)) ∈ ℂ)
337336abscld 14116 . . . . . . . . . . . . . . . . . . . . 21 (((((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎𝐴) ∧ ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏𝐴) ∧ ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦)) → (abs‘(𝑥 − (𝐹𝑎))) ∈ ℝ)
338332, 337readdcld 10020 . . . . . . . . . . . . . . . . . . . 20 (((((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎𝐴) ∧ ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏𝐴) ∧ ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦)) → (((abs‘(𝑅 − (𝐹𝑏))) + (abs‘((𝐹𝑏) − 𝑥))) + (abs‘(𝑥 − (𝐹𝑎)))) ∈ ℝ)
339335, 320subcld 10343 . . . . . . . . . . . . . . . . . . . . 21 (((((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎𝐴) ∧ ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏𝐴) ∧ ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦)) → ((𝐹𝑎) − 𝐿) ∈ ℂ)
340339abscld 14116 . . . . . . . . . . . . . . . . . . . 20 (((((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎𝐴) ∧ ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏𝐴) ∧ ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦)) → (abs‘((𝐹𝑎) − 𝐿)) ∈ ℝ)
341338, 340readdcld 10020 . . . . . . . . . . . . . . . . . . 19 (((((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎𝐴) ∧ ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏𝐴) ∧ ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦)) → ((((abs‘(𝑅 − (𝐹𝑏))) + (abs‘((𝐹𝑏) − 𝑥))) + (abs‘(𝑥 − (𝐹𝑎)))) + (abs‘((𝐹𝑎) − 𝐿))) ∈ ℝ)
34215a1i 11 . . . . . . . . . . . . . . . . . . . 20 (((((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎𝐴) ∧ ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏𝐴) ∧ ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦)) → 4 ∈ ℝ)
343 rpre 11790 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 ∈ ℝ+𝑦 ∈ ℝ)
344343ad5antlr 770 . . . . . . . . . . . . . . . . . . . 20 (((((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎𝐴) ∧ ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏𝐴) ∧ ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦)) → 𝑦 ∈ ℝ)
345342, 344remulcld 10021 . . . . . . . . . . . . . . . . . . 19 (((((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎𝐴) ∧ ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏𝐴) ∧ ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦)) → (4 · 𝑦) ∈ ℝ)
346319, 326, 329, 335, 320absnpncan3d 39008 . . . . . . . . . . . . . . . . . . 19 (((((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎𝐴) ∧ ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏𝐴) ∧ ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦)) → (abs‘(𝑅𝐿)) ≤ ((((abs‘(𝑅 − (𝐹𝑏))) + (abs‘((𝐹𝑏) − 𝑥))) + (abs‘(𝑥 − (𝐹𝑎)))) + (abs‘((𝐹𝑎) − 𝐿))))
347319, 326abssubd 14133 . . . . . . . . . . . . . . . . . . . . 21 (((((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎𝐴) ∧ ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏𝐴) ∧ ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦)) → (abs‘(𝑅 − (𝐹𝑏))) = (abs‘((𝐹𝑏) − 𝑅)))
348 simprr 795 . . . . . . . . . . . . . . . . . . . . 21 (((((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎𝐴) ∧ ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏𝐴) ∧ ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦)) → (abs‘((𝐹𝑏) − 𝑅)) < 𝑦)
349347, 348eqbrtrd 4640 . . . . . . . . . . . . . . . . . . . 20 (((((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎𝐴) ∧ ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏𝐴) ∧ ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦)) → (abs‘(𝑅 − (𝐹𝑏))) < 𝑦)
350 simprl 793 . . . . . . . . . . . . . . . . . . . 20 (((((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎𝐴) ∧ ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏𝐴) ∧ ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦)) → (abs‘((𝐹𝑏) − 𝑥)) < 𝑦)
351 simp-5r 808 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎𝐴) ∧ ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏𝐴) → 𝑥 ∈ ℂ)
352 simp-4l 805 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎𝐴) ∧ ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)) → 𝜑)
353 simplr 791 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎𝐴) ∧ ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)) → 𝑎𝐴)
354352, 353, 334syl2anc 692 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎𝐴) ∧ ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)) → (𝐹𝑎) ∈ ℂ)
355354adantr 481 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎𝐴) ∧ ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏𝐴) → (𝐹𝑎) ∈ ℂ)
356351, 355abssubd 14133 . . . . . . . . . . . . . . . . . . . . . 22 ((((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎𝐴) ∧ ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏𝐴) → (abs‘(𝑥 − (𝐹𝑎))) = (abs‘((𝐹𝑎) − 𝑥)))
357 simplrl 799 . . . . . . . . . . . . . . . . . . . . . 22 ((((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎𝐴) ∧ ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏𝐴) → (abs‘((𝐹𝑎) − 𝑥)) < 𝑦)
358356, 357eqbrtrd 4640 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎𝐴) ∧ ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏𝐴) → (abs‘(𝑥 − (𝐹𝑎))) < 𝑦)
359358adantr 481 . . . . . . . . . . . . . . . . . . . 20 (((((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎𝐴) ∧ ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏𝐴) ∧ ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦)) → (abs‘(𝑥 − (𝐹𝑎))) < 𝑦)
360 simplrr 800 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎𝐴) ∧ ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏𝐴) → (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)
361360adantr 481 . . . . . . . . . . . . . . . . . . . 20 (((((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎𝐴) ∧ ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏𝐴) ∧ ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦)) → (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)
362328, 331, 337, 340, 344, 349, 350, 359, 361lt4addmuld 39007 . . . . . . . . . . . . . . . . . . 19 (((((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎𝐴) ∧ ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏𝐴) ∧ ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦)) → ((((abs‘(𝑅 − (𝐹𝑏))) + (abs‘((𝐹𝑏) − 𝑥))) + (abs‘(𝑥 − (𝐹𝑎)))) + (abs‘((𝐹𝑎) − 𝐿))) < (4 · 𝑦))
363322, 341, 345, 346, 362lelttrd 10146 . . . . . . . . . . . . . . . . . 18 (((((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎𝐴) ∧ ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏𝐴) ∧ ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦)) → (abs‘(𝑅𝐿)) < (4 · 𝑦))
364363ex 450 . . . . . . . . . . . . . . . . 17 ((((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎𝐴) ∧ ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏𝐴) → (((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦) → (abs‘(𝑅𝐿)) < (4 · 𝑦)))
365364adantlllr 38709 . . . . . . . . . . . . . . . 16 (((((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ ∃𝑧 ∈ ℝ+𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ 𝑎𝐴) ∧ ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏𝐴) → (((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦) → (abs‘(𝑅𝐿)) < (4 · 𝑦)))
366365reximdva 3012 . . . . . . . . . . . . . . 15 ((((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ ∃𝑧 ∈ ℝ+𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ 𝑎𝐴) ∧ ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)) → (∃𝑏𝐴 ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦) → ∃𝑏𝐴 (abs‘(𝑅𝐿)) < (4 · 𝑦)))
367318, 366mpd 15 . . . . . . . . . . . . . 14 ((((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ ∃𝑧 ∈ ℝ+𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ 𝑎𝐴) ∧ ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)) → ∃𝑏𝐴 (abs‘(𝑅𝐿)) < (4 · 𝑦))
368367ex 450 . . . . . . . . . . . . 13 (((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ ∃𝑧 ∈ ℝ+𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ 𝑎𝐴) → (((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦) → ∃𝑏𝐴 (abs‘(𝑅𝐿)) < (4 · 𝑦)))
369368reximdva 3012 . . . . . . . . . . . 12 ((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ ∃𝑧 ∈ ℝ+𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) → (∃𝑎𝐴 ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦) → ∃𝑎𝐴𝑏𝐴 (abs‘(𝑅𝐿)) < (4 · 𝑦)))
370195, 369mpd 15 . . . . . . . . . . 11 ((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ ∃𝑧 ∈ ℝ+𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) → ∃𝑎𝐴𝑏𝐴 (abs‘(𝑅𝐿)) < (4 · 𝑦))
37132, 33, 35, 370syl21anc 1322 . . . . . . . . . 10 ((((𝜑𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ 𝑦 ∈ ℝ+) → ∃𝑎𝐴𝑏𝐴 (abs‘(𝑅𝐿)) < (4 · 𝑦))
372371ex 450 . . . . . . . . 9 (((𝜑𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) → (𝑦 ∈ ℝ+ → ∃𝑎𝐴𝑏𝐴 (abs‘(𝑅𝐿)) < (4 · 𝑦)))
37324, 25, 31, 372vtoclf 3247 . . . . . . . 8 (((𝜑𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) → (((abs‘(𝑅𝐿)) / 4) ∈ ℝ+ → ∃𝑎𝐴𝑏𝐴 (abs‘(𝑅𝐿)) < (4 · ((abs‘(𝑅𝐿)) / 4))))
37419, 373mpd 15 . . . . . . 7 (((𝜑𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) → ∃𝑎𝐴𝑏𝐴 (abs‘(𝑅𝐿)) < (4 · ((abs‘(𝑅𝐿)) / 4)))
375 simpr 477 . . . . . . . . . . . 12 ((𝜑 ∧ (abs‘(𝑅𝐿)) < (4 · ((abs‘(𝑅𝐿)) / 4))) → (abs‘(𝑅𝐿)) < (4 · ((abs‘(𝑅𝐿)) / 4)))
376 abssubrp 38974 . . . . . . . . . . . . . . . 16 ((𝑅 ∈ ℂ ∧ 𝐿 ∈ ℂ ∧ 𝑅𝐿) → (abs‘(𝑅𝐿)) ∈ ℝ+)
3773, 7, 11, 376syl3anc 1323 . . . . . . . . . . . . . . 15 (𝜑 → (abs‘(𝑅𝐿)) ∈ ℝ+)
378377rpcnd 11825 . . . . . . . . . . . . . 14 (𝜑 → (abs‘(𝑅𝐿)) ∈ ℂ)
379378adantr 481 . . . . . . . . . . . . 13 ((𝜑 ∧ (abs‘(𝑅𝐿)) < (4 · ((abs‘(𝑅𝐿)) / 4))) → (abs‘(𝑅𝐿)) ∈ ℂ)
380 4cn 11049 . . . . . . . . . . . . . 14 4 ∈ ℂ
381380a1i 11 . . . . . . . . . . . . 13 ((𝜑 ∧ (abs‘(𝑅𝐿)) < (4 · ((abs‘(𝑅𝐿)) / 4))) → 4 ∈ ℂ)
382 4ne0 11068 . . . . . . . . . . . . . 14 4 ≠ 0
383382a1i 11 . . . . . . . . . . . . 13 ((𝜑 ∧ (abs‘(𝑅𝐿)) < (4 · ((abs‘(𝑅𝐿)) / 4))) → 4 ≠ 0)
384379, 381, 383divcan2d 10754 . . . . . . . . . . . 12 ((𝜑 ∧ (abs‘(𝑅𝐿)) < (4 · ((abs‘(𝑅𝐿)) / 4))) → (4 · ((abs‘(𝑅𝐿)) / 4)) = (abs‘(𝑅𝐿)))
385375, 384breqtrd 4644 . . . . . . . . . . 11 ((𝜑 ∧ (abs‘(𝑅𝐿)) < (4 · ((abs‘(𝑅𝐿)) / 4))) → (abs‘(𝑅𝐿)) < (abs‘(𝑅𝐿)))
386385ex 450 . . . . . . . . . 10 (𝜑 → ((abs‘(𝑅𝐿)) < (4 · ((abs‘(𝑅𝐿)) / 4)) → (abs‘(𝑅𝐿)) < (abs‘(𝑅𝐿))))
387386a1d 25 . . . . . . . . 9 (𝜑 → ((𝑎𝐴𝑏𝐴) → ((abs‘(𝑅𝐿)) < (4 · ((abs‘(𝑅𝐿)) / 4)) → (abs‘(𝑅𝐿)) < (abs‘(𝑅𝐿)))))
388387ad2antrr 761 . . . . . . . 8 (((𝜑𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) → ((𝑎𝐴𝑏𝐴) → ((abs‘(𝑅𝐿)) < (4 · ((abs‘(𝑅𝐿)) / 4)) → (abs‘(𝑅𝐿)) < (abs‘(𝑅𝐿)))))
389388rexlimdvv 3031 . . . . . . 7 (((𝜑𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) → (∃𝑎𝐴𝑏𝐴 (abs‘(𝑅𝐿)) < (4 · ((abs‘(𝑅𝐿)) / 4)) → (abs‘(𝑅𝐿)) < (abs‘(𝑅𝐿))))
390374, 389mpd 15 . . . . . 6 (((𝜑𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) → (abs‘(𝑅𝐿)) < (abs‘(𝑅𝐿)))
3919abscld 14116 . . . . . . 7 (((𝜑𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) → (abs‘(𝑅𝐿)) ∈ ℝ)
392391ltnrd 10122 . . . . . 6 (((𝜑𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) → ¬ (abs‘(𝑅𝐿)) < (abs‘(𝑅𝐿)))
393390, 392pm2.65da 599 . . . . 5 ((𝜑𝑥 ∈ ℂ) → ¬ ∀𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦))
394393ex 450 . . . 4 (𝜑 → (𝑥 ∈ ℂ → ¬ ∀𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)))
395 imnan 438 . . . 4 ((𝑥 ∈ ℂ → ¬ ∀𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ↔ ¬ (𝑥 ∈ ℂ ∧ ∀𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)))
396394, 395sylib 208 . . 3 (𝜑 → ¬ (𝑥 ∈ ℂ ∧ ∀𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)))
397 limclner.a . . . . 5 (𝜑𝐴 ⊆ ℝ)
398397, 72sstrd 3597 . . . 4 (𝜑𝐴 ⊆ ℂ)
39936, 398, 55ellimc3 23562 . . 3 (𝜑 → (𝑥 ∈ (𝐹 lim 𝐵) ↔ (𝑥 ∈ ℂ ∧ ∀𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦))))
400396, 399mtbird 315 . 2 (𝜑 → ¬ 𝑥 ∈ (𝐹 lim 𝐵))
401400eq0rdv 3956 1 (𝜑 → (𝐹 lim 𝐵) = ∅)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 384  w3a 1036   = wceq 1480  wcel 1987  wne 2790  wral 2907  wrex 2908  cdif 3556  cin 3558  wss 3559  c0 3896  ifcif 4063  {csn 4153   cuni 4407   class class class wbr 4618  ran crn 5080  cres 5081  wf 5848  cfv 5852  (class class class)co 6610  cc 9885  cr 9886  0cc0 9887   + caddc 9890   · cmul 9892  +∞cpnf 10022  -∞cmnf 10023   < clt 10025  cle 10026  cmin 10217   / cdiv 10635  4c4 11023  +crp 11783  (,)cioo 12124  abscabs 13915  t crest 16009  TopOpenctopn 16010  topGenctg 16026  fldccnfld 19674  Topctop 20626  limPtclp 20857   lim climc 23545
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-rep 4736  ax-sep 4746  ax-nul 4754  ax-pow 4808  ax-pr 4872  ax-un 6909  ax-cnex 9943  ax-resscn 9944  ax-1cn 9945  ax-icn 9946  ax-addcl 9947  ax-addrcl 9948  ax-mulcl 9949  ax-mulrcl 9950  ax-mulcom 9951  ax-addass 9952  ax-mulass 9953  ax-distr 9954  ax-i2m1 9955  ax-1ne0 9956  ax-1rid 9957  ax-rnegex 9958  ax-rrecex 9959  ax-cnre 9960  ax-pre-lttri 9961  ax-pre-lttrn 9962  ax-pre-ltadd 9963  ax-pre-mulgt0 9964  ax-pre-sup 9965
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-nel 2894  df-ral 2912  df-rex 2913  df-reu 2914  df-rmo 2915  df-rab 2916  df-v 3191  df-sbc 3422  df-csb 3519  df-dif 3562  df-un 3564  df-in 3566  df-ss 3573  df-pss 3575  df-nul 3897  df-if 4064  df-pw 4137  df-sn 4154  df-pr 4156  df-tp 4158  df-op 4160  df-uni 4408  df-int 4446  df-iun 4492  df-iin 4493  df-br 4619  df-opab 4679  df-mpt 4680  df-tr 4718  df-eprel 4990  df-id 4994  df-po 5000  df-so 5001  df-fr 5038  df-we 5040  df-xp 5085  df-rel 5086  df-cnv 5087  df-co 5088  df-dm 5089  df-rn 5090  df-res 5091  df-ima 5092  df-pred 5644  df-ord 5690  df-on 5691  df-lim 5692  df-suc 5693  df-iota 5815  df-fun 5854  df-fn 5855  df-f 5856  df-f1 5857  df-fo 5858  df-f1o 5859  df-fv 5860  df-riota 6571  df-ov 6613  df-oprab 6614  df-mpt2 6615  df-om 7020  df-1st 7120  df-2nd 7121  df-wrecs 7359  df-recs 7420  df-rdg 7458  df-1o 7512  df-oadd 7516  df-er 7694  df-map 7811  df-pm 7812  df-en 7907  df-dom 7908  df-sdom 7909  df-fin 7910  df-fi 8268  df-sup 8299  df-inf 8300  df-pnf 10027  df-mnf 10028  df-xr 10029  df-ltxr 10030  df-le 10031  df-sub 10219  df-neg 10220  df-div 10636  df-nn 10972  df-2 11030  df-3 11031  df-4 11032  df-5 11033  df-6 11034  df-7 11035  df-8 11036  df-9 11037  df-n0 11244  df-z 11329  df-dec 11445  df-uz 11639  df-q 11740  df-rp 11784  df-xneg 11897  df-xadd 11898  df-xmul 11899  df-ioo 12128  df-fz 12276  df-seq 12749  df-exp 12808  df-cj 13780  df-re 13781  df-im 13782  df-sqrt 13916  df-abs 13917  df-struct 15790  df-ndx 15791  df-slot 15792  df-base 15793  df-plusg 15882  df-mulr 15883  df-starv 15884  df-tset 15888  df-ple 15889  df-ds 15892  df-unif 15893  df-rest 16011  df-topn 16012  df-topgen 16032  df-psmet 19666  df-xmet 19667  df-met 19668  df-bl 19669  df-mopn 19670  df-cnfld 19675  df-top 20627  df-topon 20644  df-topsp 20657  df-bases 20670  df-cld 20742  df-ntr 20743  df-cls 20744  df-nei 20821  df-lp 20859  df-cnp 20951  df-xms 22044  df-ms 22045  df-limc 23549
This theorem is referenced by:  limclr  39314  jumpncnp  39437
  Copyright terms: Public domain W3C validator