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 40401
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 23859 . . . . . . . . . . . . 13 ((𝐹 ↾ (𝐵(,)+∞)) lim 𝐵) ⊆ ℂ
2 limclner.r . . . . . . . . . . . . 13 (𝜑𝑅 ∈ ((𝐹 ↾ (𝐵(,)+∞)) lim 𝐵))
31, 2sseldi 3750 . . . . . . . . . . . 12 (𝜑𝑅 ∈ ℂ)
43ad2antrr 705 . . . . . . . . . . 11 (((𝜑𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) → 𝑅 ∈ ℂ)
5 limccl 23859 . . . . . . . . . . . . 13 ((𝐹 ↾ (-∞(,)𝐵)) lim 𝐵) ⊆ ℂ
6 limclner.l . . . . . . . . . . . . 13 (𝜑𝐿 ∈ ((𝐹 ↾ (-∞(,)𝐵)) lim 𝐵))
75, 6sseldi 3750 . . . . . . . . . . . 12 (𝜑𝐿 ∈ ℂ)
87ad2antrr 705 . . . . . . . . . . 11 (((𝜑𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) → 𝐿 ∈ ℂ)
94, 8subcld 10594 . . . . . . . . . 10 (((𝜑𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) → (𝑅𝐿) ∈ ℂ)
10 limclner.lner . . . . . . . . . . . . 13 (𝜑𝐿𝑅)
1110necomd 2998 . . . . . . . . . . . 12 (𝜑𝑅𝐿)
1211ad2antrr 705 . . . . . . . . . . 11 (((𝜑𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) → 𝑅𝐿)
134, 8, 12subne0d 10603 . . . . . . . . . 10 (((𝜑𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) → (𝑅𝐿) ≠ 0)
149, 13absrpcld 14395 . . . . . . . . 9 (((𝜑𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) → (abs‘(𝑅𝐿)) ∈ ℝ+)
15 4re 11299 . . . . . . . . . . 11 4 ∈ ℝ
16 4pos 11318 . . . . . . . . . . 11 0 < 4
1715, 16elrpii 12038 . . . . . . . . . 10 4 ∈ ℝ+
1817a1i 11 . . . . . . . . 9 (((𝜑𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) → 4 ∈ ℝ+)
1914, 18rpdivcld 12092 . . . . . . . 8 (((𝜑𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) → ((abs‘(𝑅𝐿)) / 4) ∈ ℝ+)
20 nfv 1995 . . . . . . . . . . 11 𝑦(𝜑𝑥 ∈ ℂ)
21 nfra1 3090 . . . . . . . . . . 11 𝑦𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)
2220, 21nfan 1980 . . . . . . . . . 10 𝑦((𝜑𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦))
23 nfv 1995 . . . . . . . . . 10 𝑦(((abs‘(𝑅𝐿)) / 4) ∈ ℝ+ → ∃𝑎𝐴𝑏𝐴 (abs‘(𝑅𝐿)) < (4 · ((abs‘(𝑅𝐿)) / 4)))
2422, 23nfim 1977 . . . . . . . . 9 𝑦(((𝜑𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) → (((abs‘(𝑅𝐿)) / 4) ∈ ℝ+ → ∃𝑎𝐴𝑏𝐴 (abs‘(𝑅𝐿)) < (4 · ((abs‘(𝑅𝐿)) / 4))))
25 ovex 6823 . . . . . . . . 9 ((abs‘(𝑅𝐿)) / 4) ∈ V
26 eleq1 2838 . . . . . . . . . . 11 (𝑦 = ((abs‘(𝑅𝐿)) / 4) → (𝑦 ∈ ℝ+ ↔ ((abs‘(𝑅𝐿)) / 4) ∈ ℝ+))
27 oveq2 6801 . . . . . . . . . . . . 13 (𝑦 = ((abs‘(𝑅𝐿)) / 4) → (4 · 𝑦) = (4 · ((abs‘(𝑅𝐿)) / 4)))
2827breq2d 4798 . . . . . . . . . . . 12 (𝑦 = ((abs‘(𝑅𝐿)) / 4) → ((abs‘(𝑅𝐿)) < (4 · 𝑦) ↔ (abs‘(𝑅𝐿)) < (4 · ((abs‘(𝑅𝐿)) / 4))))
29282rexbidv 3205 . . . . . . . . . . 11 (𝑦 = ((abs‘(𝑅𝐿)) / 4) → (∃𝑎𝐴𝑏𝐴 (abs‘(𝑅𝐿)) < (4 · 𝑦) ↔ ∃𝑎𝐴𝑏𝐴 (abs‘(𝑅𝐿)) < (4 · ((abs‘(𝑅𝐿)) / 4))))
3026, 29imbi12d 333 . . . . . . . . . 10 (𝑦 = ((abs‘(𝑅𝐿)) / 4) → ((𝑦 ∈ ℝ+ → ∃𝑎𝐴𝑏𝐴 (abs‘(𝑅𝐿)) < (4 · 𝑦)) ↔ (((abs‘(𝑅𝐿)) / 4) ∈ ℝ+ → ∃𝑎𝐴𝑏𝐴 (abs‘(𝑅𝐿)) < (4 · ((abs‘(𝑅𝐿)) / 4)))))
3130imbi2d 329 . . . . . . . . 9 (𝑦 = ((abs‘(𝑅𝐿)) / 4) → ((((𝜑𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) → (𝑦 ∈ ℝ+ → ∃𝑎𝐴𝑏𝐴 (abs‘(𝑅𝐿)) < (4 · 𝑦))) ↔ (((𝜑𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) → (((abs‘(𝑅𝐿)) / 4) ∈ ℝ+ → ∃𝑎𝐴𝑏𝐴 (abs‘(𝑅𝐿)) < (4 · ((abs‘(𝑅𝐿)) / 4))))))
32 simpll 750 . . . . . . . . . . 11 ((((𝜑𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ 𝑦 ∈ ℝ+) → (𝜑𝑥 ∈ ℂ))
33 simpr 471 . . . . . . . . . . 11 ((((𝜑𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ 𝑦 ∈ ℝ+) → 𝑦 ∈ ℝ+)
34 rspa 3079 . . . . . . . . . . . 12 ((∀𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦) ∧ 𝑦 ∈ ℝ+) → ∃𝑧 ∈ ℝ+𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦))
3534adantll 693 . . . . . . . . . . 11 ((((𝜑𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ 𝑦 ∈ ℝ+) → ∃𝑧 ∈ ℝ+𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦))
36 limclner.f . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑𝐹:𝐴⟶ℂ)
37 fresin 6213 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐹:𝐴⟶ℂ → (𝐹 ↾ (-∞(,)𝐵)):(𝐴 ∩ (-∞(,)𝐵))⟶ℂ)
3836, 37syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝐹 ↾ (-∞(,)𝐵)):(𝐴 ∩ (-∞(,)𝐵))⟶ℂ)
39 inss2 3982 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝐴 ∩ (-∞(,)𝐵)) ⊆ (-∞(,)𝐵)
40 ioosscn 40237 . . . . . . . . . . . . . . . . . . . . . . . 24 (-∞(,)𝐵) ⊆ ℂ
4139, 40sstri 3761 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐴 ∩ (-∞(,)𝐵)) ⊆ ℂ
4241a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝐴 ∩ (-∞(,)𝐵)) ⊆ ℂ)
43 limclner.j . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝐽 = (topGen‘ran (,))
44 retop 22785 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (topGen‘ran (,)) ∈ Top
4543, 44eqeltri 2846 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝐽 ∈ Top
46 ioossre 12440 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (-∞(,)𝐵) ⊆ ℝ
4739, 46sstri 3761 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝐴 ∩ (-∞(,)𝐵)) ⊆ ℝ
48 uniretop 22786 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ℝ = (topGen‘ran (,))
4943unieqi 4583 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 𝐽 = (topGen‘ran (,))
5048, 49eqtr4i 2796 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ℝ = 𝐽
5150lpss 21167 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐽 ∈ Top ∧ (𝐴 ∩ (-∞(,)𝐵)) ⊆ ℝ) → ((limPt‘𝐽)‘(𝐴 ∩ (-∞(,)𝐵))) ⊆ ℝ)
5245, 47, 51mp2an 672 . . . . . . . . . . . . . . . . . . . . . . . 24 ((limPt‘𝐽)‘(𝐴 ∩ (-∞(,)𝐵))) ⊆ ℝ
53 limclner.blp1 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑𝐵 ∈ ((limPt‘𝐽)‘(𝐴 ∩ (-∞(,)𝐵))))
5452, 53sseldi 3750 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑𝐵 ∈ ℝ)
5554recnd 10270 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑𝐵 ∈ ℂ)
5638, 42, 55ellimc3 23863 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝐿 ∈ ((𝐹 ↾ (-∞(,)𝐵)) lim 𝐵) ↔ (𝐿 ∈ ℂ ∧ ∀𝑦 ∈ ℝ+𝑣 ∈ ℝ+𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦))))
576, 56mpbid 222 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝐿 ∈ ℂ ∧ ∀𝑦 ∈ ℝ+𝑣 ∈ ℝ+𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)))
5857simprd 483 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ∀𝑦 ∈ ℝ+𝑣 ∈ ℝ+𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦))
5958r19.21bi 3081 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑦 ∈ ℝ+) → ∃𝑣 ∈ ℝ+𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦))
60593ad2ant1 1127 . . . . . . . . . . . . . . . . 17 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) → ∃𝑣 ∈ ℝ+𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦))
61 simp11l 1368 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) → 𝜑)
62 simp12 1246 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) → 𝑧 ∈ ℝ+)
63 simp2 1131 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) → 𝑣 ∈ ℝ+)
64 ifcl 4269 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑧 ∈ ℝ+𝑣 ∈ ℝ+) → if(𝑧𝑣, 𝑧, 𝑣) ∈ ℝ+)
65643adant1 1124 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑧 ∈ ℝ+𝑣 ∈ ℝ+) → if(𝑧𝑣, 𝑧, 𝑣) ∈ ℝ+)
66 inss1 3981 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((limPt‘𝐾)‘(𝐴 ∩ (-∞(,)𝐵))) ∩ ℝ) ⊆ ((limPt‘𝐾)‘(𝐴 ∩ (-∞(,)𝐵)))
6766a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → (((limPt‘𝐾)‘(𝐴 ∩ (-∞(,)𝐵))) ∩ ℝ) ⊆ ((limPt‘𝐾)‘(𝐴 ∩ (-∞(,)𝐵))))
68 limclner.k . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 𝐾 = (TopOpen‘ℂfld)
6968cnfldtop 22807 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 𝐾 ∈ Top
7069a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑𝐾 ∈ Top)
71 ax-resscn 10195 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ℝ ⊆ ℂ
7271a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑 → ℝ ⊆ ℂ)
7347a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑 → (𝐴 ∩ (-∞(,)𝐵)) ⊆ ℝ)
74 unicntop 22809 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ℂ = (TopOpen‘ℂfld)
7568unieqi 4583 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 𝐾 = (TopOpen‘ℂfld)
7674, 75eqtr4i 2796 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ℂ = 𝐾
7768tgioo2 22826 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (topGen‘ran (,)) = (𝐾t ℝ)
7843, 77eqtri 2793 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 𝐽 = (𝐾t ℝ)
7976, 78restlp 21208 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝐾 ∈ Top ∧ ℝ ⊆ ℂ ∧ (𝐴 ∩ (-∞(,)𝐵)) ⊆ ℝ) → ((limPt‘𝐽)‘(𝐴 ∩ (-∞(,)𝐵))) = (((limPt‘𝐾)‘(𝐴 ∩ (-∞(,)𝐵))) ∩ ℝ))
8070, 72, 73, 79syl3anc 1476 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → ((limPt‘𝐽)‘(𝐴 ∩ (-∞(,)𝐵))) = (((limPt‘𝐾)‘(𝐴 ∩ (-∞(,)𝐵))) ∩ ℝ))
8168eqcomi 2780 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (TopOpen‘ℂfld) = 𝐾
8281fveq2i 6335 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (limPt‘(TopOpen‘ℂfld)) = (limPt‘𝐾)
8382fveq1i 6333 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((limPt‘(TopOpen‘ℂfld))‘(𝐴 ∩ (-∞(,)𝐵))) = ((limPt‘𝐾)‘(𝐴 ∩ (-∞(,)𝐵)))
8483a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → ((limPt‘(TopOpen‘ℂfld))‘(𝐴 ∩ (-∞(,)𝐵))) = ((limPt‘𝐾)‘(𝐴 ∩ (-∞(,)𝐵))))
8567, 80, 843sstr4d 3797 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → ((limPt‘𝐽)‘(𝐴 ∩ (-∞(,)𝐵))) ⊆ ((limPt‘(TopOpen‘ℂfld))‘(𝐴 ∩ (-∞(,)𝐵))))
8685, 53sseldd 3753 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑𝐵 ∈ ((limPt‘(TopOpen‘ℂfld))‘(𝐴 ∩ (-∞(,)𝐵))))
8742, 55islpcn 40389 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → (𝐵 ∈ ((limPt‘(TopOpen‘ℂfld))‘(𝐴 ∩ (-∞(,)𝐵))) ↔ ∀𝑢 ∈ ℝ+𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵})(abs‘(𝑎𝐵)) < 𝑢))
8886, 87mpbid 222 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → ∀𝑢 ∈ ℝ+𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵})(abs‘(𝑎𝐵)) < 𝑢)
89883ad2ant1 1127 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑧 ∈ ℝ+𝑣 ∈ ℝ+) → ∀𝑢 ∈ ℝ+𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵})(abs‘(𝑎𝐵)) < 𝑢)
90 breq2 4790 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑢 = if(𝑧𝑣, 𝑧, 𝑣) → ((abs‘(𝑎𝐵)) < 𝑢 ↔ (abs‘(𝑎𝐵)) < if(𝑧𝑣, 𝑧, 𝑣)))
9190rexbidv 3200 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑢 = if(𝑧𝑣, 𝑧, 𝑣) → (∃𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵})(abs‘(𝑎𝐵)) < 𝑢 ↔ ∃𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵})(abs‘(𝑎𝐵)) < if(𝑧𝑣, 𝑧, 𝑣)))
9291rspcva 3458 . . . . . . . . . . . . . . . . . . . . . . 23 ((if(𝑧𝑣, 𝑧, 𝑣) ∈ ℝ+ ∧ ∀𝑢 ∈ ℝ+𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵})(abs‘(𝑎𝐵)) < 𝑢) → ∃𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵})(abs‘(𝑎𝐵)) < if(𝑧𝑣, 𝑧, 𝑣))
9365, 89, 92syl2anc 573 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑧 ∈ ℝ+𝑣 ∈ ℝ+) → ∃𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵})(abs‘(𝑎𝐵)) < if(𝑧𝑣, 𝑧, 𝑣))
94 eldifi 3883 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵}) → 𝑎 ∈ (𝐴 ∩ (-∞(,)𝐵)))
9547, 94sseldi 3750 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵}) → 𝑎 ∈ ℝ)
9672sselda 3752 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑𝑎 ∈ ℝ) → 𝑎 ∈ ℂ)
9755adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑𝑎 ∈ ℝ) → 𝐵 ∈ ℂ)
9896, 97subcld 10594 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑𝑎 ∈ ℝ) → (𝑎𝐵) ∈ ℂ)
9998abscld 14383 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑎 ∈ ℝ) → (abs‘(𝑎𝐵)) ∈ ℝ)
100993ad2antl1 1200 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑𝑧 ∈ ℝ+𝑣 ∈ ℝ+) ∧ 𝑎 ∈ ℝ) → (abs‘(𝑎𝐵)) ∈ ℝ)
101100adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑𝑧 ∈ ℝ+𝑣 ∈ ℝ+) ∧ 𝑎 ∈ ℝ) ∧ (abs‘(𝑎𝐵)) < if(𝑧𝑣, 𝑧, 𝑣)) → (abs‘(𝑎𝐵)) ∈ ℝ)
10265rpred 12075 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑧 ∈ ℝ+𝑣 ∈ ℝ+) → if(𝑧𝑣, 𝑧, 𝑣) ∈ ℝ)
103102ad2antrr 705 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑𝑧 ∈ ℝ+𝑣 ∈ ℝ+) ∧ 𝑎 ∈ ℝ) ∧ (abs‘(𝑎𝐵)) < if(𝑧𝑣, 𝑧, 𝑣)) → if(𝑧𝑣, 𝑧, 𝑣) ∈ ℝ)
104 rpre 12042 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑧 ∈ ℝ+𝑧 ∈ ℝ)
1051043ad2ant2 1128 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑧 ∈ ℝ+𝑣 ∈ ℝ+) → 𝑧 ∈ ℝ)
106105ad2antrr 705 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑𝑧 ∈ ℝ+𝑣 ∈ ℝ+) ∧ 𝑎 ∈ ℝ) ∧ (abs‘(𝑎𝐵)) < if(𝑧𝑣, 𝑧, 𝑣)) → 𝑧 ∈ ℝ)
107 simpr 471 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑𝑧 ∈ ℝ+𝑣 ∈ ℝ+) ∧ 𝑎 ∈ ℝ) ∧ (abs‘(𝑎𝐵)) < if(𝑧𝑣, 𝑧, 𝑣)) → (abs‘(𝑎𝐵)) < if(𝑧𝑣, 𝑧, 𝑣))
108 rpre 12042 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑣 ∈ ℝ+𝑣 ∈ ℝ)
109 min1 12225 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑧 ∈ ℝ ∧ 𝑣 ∈ ℝ) → if(𝑧𝑣, 𝑧, 𝑣) ≤ 𝑧)
110104, 108, 109syl2an 583 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑧 ∈ ℝ+𝑣 ∈ ℝ+) → if(𝑧𝑣, 𝑧, 𝑣) ≤ 𝑧)
1111103adant1 1124 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑧 ∈ ℝ+𝑣 ∈ ℝ+) → if(𝑧𝑣, 𝑧, 𝑣) ≤ 𝑧)
112111ad2antrr 705 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑𝑧 ∈ ℝ+𝑣 ∈ ℝ+) ∧ 𝑎 ∈ ℝ) ∧ (abs‘(𝑎𝐵)) < if(𝑧𝑣, 𝑧, 𝑣)) → if(𝑧𝑣, 𝑧, 𝑣) ≤ 𝑧)
113101, 103, 106, 107, 112ltletrd 10399 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑𝑧 ∈ ℝ+𝑣 ∈ ℝ+) ∧ 𝑎 ∈ ℝ) ∧ (abs‘(𝑎𝐵)) < if(𝑧𝑣, 𝑧, 𝑣)) → (abs‘(𝑎𝐵)) < 𝑧)
114108adantl 467 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑧 ∈ ℝ+𝑣 ∈ ℝ+) → 𝑣 ∈ ℝ)
1151143adant1 1124 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑧 ∈ ℝ+𝑣 ∈ ℝ+) → 𝑣 ∈ ℝ)
116115ad2antrr 705 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑𝑧 ∈ ℝ+𝑣 ∈ ℝ+) ∧ 𝑎 ∈ ℝ) ∧ (abs‘(𝑎𝐵)) < if(𝑧𝑣, 𝑧, 𝑣)) → 𝑣 ∈ ℝ)
117 min2 12226 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑧 ∈ ℝ ∧ 𝑣 ∈ ℝ) → if(𝑧𝑣, 𝑧, 𝑣) ≤ 𝑣)
118104, 108, 117syl2an 583 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑧 ∈ ℝ+𝑣 ∈ ℝ+) → if(𝑧𝑣, 𝑧, 𝑣) ≤ 𝑣)
1191183adant1 1124 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑧 ∈ ℝ+𝑣 ∈ ℝ+) → if(𝑧𝑣, 𝑧, 𝑣) ≤ 𝑣)
120119ad2antrr 705 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑𝑧 ∈ ℝ+𝑣 ∈ ℝ+) ∧ 𝑎 ∈ ℝ) ∧ (abs‘(𝑎𝐵)) < if(𝑧𝑣, 𝑧, 𝑣)) → if(𝑧𝑣, 𝑧, 𝑣) ≤ 𝑣)
121101, 103, 116, 107, 120ltletrd 10399 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑𝑧 ∈ ℝ+𝑣 ∈ ℝ+) ∧ 𝑎 ∈ ℝ) ∧ (abs‘(𝑎𝐵)) < if(𝑧𝑣, 𝑧, 𝑣)) → (abs‘(𝑎𝐵)) < 𝑣)
122113, 121jca 501 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑧 ∈ ℝ+𝑣 ∈ ℝ+) ∧ 𝑎 ∈ ℝ) ∧ (abs‘(𝑎𝐵)) < if(𝑧𝑣, 𝑧, 𝑣)) → ((abs‘(𝑎𝐵)) < 𝑧 ∧ (abs‘(𝑎𝐵)) < 𝑣))
123122ex 397 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑧 ∈ ℝ+𝑣 ∈ ℝ+) ∧ 𝑎 ∈ ℝ) → ((abs‘(𝑎𝐵)) < if(𝑧𝑣, 𝑧, 𝑣) → ((abs‘(𝑎𝐵)) < 𝑧 ∧ (abs‘(𝑎𝐵)) < 𝑣)))
12495, 123sylan2 580 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑧 ∈ ℝ+𝑣 ∈ ℝ+) ∧ 𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵})) → ((abs‘(𝑎𝐵)) < if(𝑧𝑣, 𝑧, 𝑣) → ((abs‘(𝑎𝐵)) < 𝑧 ∧ (abs‘(𝑎𝐵)) < 𝑣)))
125124reximdva 3165 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑧 ∈ ℝ+𝑣 ∈ ℝ+) → (∃𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵})(abs‘(𝑎𝐵)) < if(𝑧𝑣, 𝑧, 𝑣) → ∃𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵})((abs‘(𝑎𝐵)) < 𝑧 ∧ (abs‘(𝑎𝐵)) < 𝑣)))
12693, 125mpd 15 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑧 ∈ ℝ+𝑣 ∈ ℝ+) → ∃𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵})((abs‘(𝑎𝐵)) < 𝑧 ∧ (abs‘(𝑎𝐵)) < 𝑣))
12761, 62, 63, 126syl3anc 1476 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) → ∃𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵})((abs‘(𝑎𝐵)) < 𝑧 ∧ (abs‘(𝑎𝐵)) < 𝑣))
128 nfv 1995 . . . . . . . . . . . . . . . . . . . . 21 𝑎(((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦))
129 nfre1 3153 . . . . . . . . . . . . . . . . . . . . 21 𝑎𝑎𝐴 ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)
130 inss1 3981 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝐴 ∩ (-∞(,)𝐵)) ⊆ 𝐴
131130, 94sseldi 3750 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵}) → 𝑎𝐴)
1321313ad2ant2 1128 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) ∧ 𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵}) ∧ ((abs‘(𝑎𝐵)) < 𝑧 ∧ (abs‘(𝑎𝐵)) < 𝑣)) → 𝑎𝐴)
133 simp113 1388 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) ∧ 𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵}) ∧ ((abs‘(𝑎𝐵)) < 𝑧 ∧ (abs‘(𝑎𝐵)) < 𝑣)) → ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦))
134 eldifsni 4457 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵}) → 𝑎𝐵)
135134adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵}) ∧ ((abs‘(𝑎𝐵)) < 𝑧 ∧ (abs‘(𝑎𝐵)) < 𝑣)) → 𝑎𝐵)
136 simprl 754 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵}) ∧ ((abs‘(𝑎𝐵)) < 𝑧 ∧ (abs‘(𝑎𝐵)) < 𝑣)) → (abs‘(𝑎𝐵)) < 𝑧)
137135, 136jca 501 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵}) ∧ ((abs‘(𝑎𝐵)) < 𝑧 ∧ (abs‘(𝑎𝐵)) < 𝑣)) → (𝑎𝐵 ∧ (abs‘(𝑎𝐵)) < 𝑧))
1381373adant1 1124 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) ∧ 𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵}) ∧ ((abs‘(𝑎𝐵)) < 𝑧 ∧ (abs‘(𝑎𝐵)) < 𝑣)) → (𝑎𝐵 ∧ (abs‘(𝑎𝐵)) < 𝑧))
139 neeq1 3005 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑤 = 𝑎 → (𝑤𝐵𝑎𝐵))
140 fvoveq1 6816 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑤 = 𝑎 → (abs‘(𝑤𝐵)) = (abs‘(𝑎𝐵)))
141140breq1d 4796 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑤 = 𝑎 → ((abs‘(𝑤𝐵)) < 𝑧 ↔ (abs‘(𝑎𝐵)) < 𝑧))
142139, 141anbi12d 616 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑤 = 𝑎 → ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) ↔ (𝑎𝐵 ∧ (abs‘(𝑎𝐵)) < 𝑧)))
143 fveq2 6332 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑤 = 𝑎 → (𝐹𝑤) = (𝐹𝑎))
144143fvoveq1d 6815 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑤 = 𝑎 → (abs‘((𝐹𝑤) − 𝑥)) = (abs‘((𝐹𝑎) − 𝑥)))
145144breq1d 4796 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑤 = 𝑎 → ((abs‘((𝐹𝑤) − 𝑥)) < 𝑦 ↔ (abs‘((𝐹𝑎) − 𝑥)) < 𝑦))
146142, 145imbi12d 333 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑤 = 𝑎 → (((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦) ↔ ((𝑎𝐵 ∧ (abs‘(𝑎𝐵)) < 𝑧) → (abs‘((𝐹𝑎) − 𝑥)) < 𝑦)))
147146rspcva 3458 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑎𝐴 ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) → ((𝑎𝐵 ∧ (abs‘(𝑎𝐵)) < 𝑧) → (abs‘((𝐹𝑎) − 𝑥)) < 𝑦))
148147imp 393 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑎𝐴 ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ (𝑎𝐵 ∧ (abs‘(𝑎𝐵)) < 𝑧)) → (abs‘((𝐹𝑎) − 𝑥)) < 𝑦)
149132, 133, 138, 148syl21anc 1475 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) ∧ 𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵}) ∧ ((abs‘(𝑎𝐵)) < 𝑧 ∧ (abs‘(𝑎𝐵)) < 𝑣)) → (abs‘((𝐹𝑎) − 𝑥)) < 𝑦)
150943ad2ant2 1128 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) ∧ 𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵}) ∧ ((abs‘(𝑎𝐵)) < 𝑧 ∧ (abs‘(𝑎𝐵)) < 𝑣)) → 𝑎 ∈ (𝐴 ∩ (-∞(,)𝐵)))
151613ad2ant1 1127 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) ∧ 𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵}) ∧ ((abs‘(𝑎𝐵)) < 𝑧 ∧ (abs‘(𝑎𝐵)) < 𝑣)) → 𝜑)
152 simp13 1247 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) ∧ 𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵}) ∧ ((abs‘(𝑎𝐵)) < 𝑧 ∧ (abs‘(𝑎𝐵)) < 𝑣)) → ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦))
153 nfv 1995 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 𝑤𝜑
154 nfra1 3090 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 𝑤𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)
155153, 154nfan 1980 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝑤(𝜑 ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦))
156 elinel2 3951 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵)) → 𝑤 ∈ (-∞(,)𝐵))
157 fvres 6348 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑤 ∈ (-∞(,)𝐵) → ((𝐹 ↾ (-∞(,)𝐵))‘𝑤) = (𝐹𝑤))
158156, 157syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵)) → ((𝐹 ↾ (-∞(,)𝐵))‘𝑤) = (𝐹𝑤))
159158eqcomd 2777 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵)) → (𝐹𝑤) = ((𝐹 ↾ (-∞(,)𝐵))‘𝑤))
160159fvoveq1d 6815 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵)) → (abs‘((𝐹𝑤) − 𝐿)) = (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)))
1611603ad2ant2 1128 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑 ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) ∧ 𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵)) ∧ (𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣)) → (abs‘((𝐹𝑤) − 𝐿)) = (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)))
162 rspa 3079 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦) ∧ 𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))) → ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦))
1631623impia 1109 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦) ∧ 𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵)) ∧ (𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣)) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)
1641633adant1l 1185 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑 ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) ∧ 𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵)) ∧ (𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣)) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)
165161, 164eqbrtrd 4808 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑 ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) ∧ 𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵)) ∧ (𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣)) → (abs‘((𝐹𝑤) − 𝐿)) < 𝑦)
1661653exp 1112 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑 ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) → (𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵)) → ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘((𝐹𝑤) − 𝐿)) < 𝑦)))
167155, 166ralrimi 3106 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) → ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘((𝐹𝑤) − 𝐿)) < 𝑦))
168151, 152, 167syl2anc 573 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) ∧ 𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵}) ∧ ((abs‘(𝑎𝐵)) < 𝑧 ∧ (abs‘(𝑎𝐵)) < 𝑣)) → ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘((𝐹𝑤) − 𝐿)) < 𝑦))
169134anim1i 602 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵}) ∧ (abs‘(𝑎𝐵)) < 𝑣) → (𝑎𝐵 ∧ (abs‘(𝑎𝐵)) < 𝑣))
170169adantrl 695 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵}) ∧ ((abs‘(𝑎𝐵)) < 𝑧 ∧ (abs‘(𝑎𝐵)) < 𝑣)) → (𝑎𝐵 ∧ (abs‘(𝑎𝐵)) < 𝑣))
1711703adant1 1124 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) ∧ 𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵}) ∧ ((abs‘(𝑎𝐵)) < 𝑧 ∧ (abs‘(𝑎𝐵)) < 𝑣)) → (𝑎𝐵 ∧ (abs‘(𝑎𝐵)) < 𝑣))
172140breq1d 4796 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑤 = 𝑎 → ((abs‘(𝑤𝐵)) < 𝑣 ↔ (abs‘(𝑎𝐵)) < 𝑣))
173139, 172anbi12d 616 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑤 = 𝑎 → ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) ↔ (𝑎𝐵 ∧ (abs‘(𝑎𝐵)) < 𝑣)))
174143fvoveq1d 6815 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑤 = 𝑎 → (abs‘((𝐹𝑤) − 𝐿)) = (abs‘((𝐹𝑎) − 𝐿)))
175174breq1d 4796 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑤 = 𝑎 → ((abs‘((𝐹𝑤) − 𝐿)) < 𝑦 ↔ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦))
176173, 175imbi12d 333 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑤 = 𝑎 → (((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘((𝐹𝑤) − 𝐿)) < 𝑦) ↔ ((𝑎𝐵 ∧ (abs‘(𝑎𝐵)) < 𝑣) → (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)))
177176rspcva 3458 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑎 ∈ (𝐴 ∩ (-∞(,)𝐵)) ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘((𝐹𝑤) − 𝐿)) < 𝑦)) → ((𝑎𝐵 ∧ (abs‘(𝑎𝐵)) < 𝑣) → (abs‘((𝐹𝑎) − 𝐿)) < 𝑦))
178177imp 393 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑎 ∈ (𝐴 ∩ (-∞(,)𝐵)) ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘((𝐹𝑤) − 𝐿)) < 𝑦)) ∧ (𝑎𝐵 ∧ (abs‘(𝑎𝐵)) < 𝑣)) → (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)
179150, 168, 171, 178syl21anc 1475 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) ∧ 𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵}) ∧ ((abs‘(𝑎𝐵)) < 𝑧 ∧ (abs‘(𝑎𝐵)) < 𝑣)) → (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)
180 rspe 3151 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑎𝐴 ∧ ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)) → ∃𝑎𝐴 ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦))
181132, 149, 179, 180syl12anc 1474 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) ∧ 𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵}) ∧ ((abs‘(𝑎𝐵)) < 𝑧 ∧ (abs‘(𝑎𝐵)) < 𝑣)) → ∃𝑎𝐴 ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦))
1821813exp 1112 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) → (𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵}) → (((abs‘(𝑎𝐵)) < 𝑧 ∧ (abs‘(𝑎𝐵)) < 𝑣) → ∃𝑎𝐴 ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦))))
183128, 129, 182rexlimd 3174 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) → (∃𝑎 ∈ ((𝐴 ∩ (-∞(,)𝐵)) ∖ {𝐵})((abs‘(𝑎𝐵)) < 𝑧 ∧ (abs‘(𝑎𝐵)) < 𝑣) → ∃𝑎𝐴 ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)))
184127, 183mpd 15 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦)) → ∃𝑎𝐴 ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦))
1851843exp 1112 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) → (𝑣 ∈ ℝ+ → (∀𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦) → ∃𝑎𝐴 ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦))))
186185rexlimdv 3178 . . . . . . . . . . . . . . . . 17 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) → (∃𝑣 ∈ ℝ+𝑤 ∈ (𝐴 ∩ (-∞(,)𝐵))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (-∞(,)𝐵))‘𝑤) − 𝐿)) < 𝑦) → ∃𝑎𝐴 ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)))
18760, 186mpd 15 . . . . . . . . . . . . . . . 16 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) → ∃𝑎𝐴 ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦))
1881873exp 1112 . . . . . . . . . . . . . . 15 ((𝜑𝑦 ∈ ℝ+) → (𝑧 ∈ ℝ+ → (∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦) → ∃𝑎𝐴 ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦))))
189188rexlimdv 3178 . . . . . . . . . . . . . 14 ((𝜑𝑦 ∈ ℝ+) → (∃𝑧 ∈ ℝ+𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦) → ∃𝑎𝐴 ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)))
190189imp 393 . . . . . . . . . . . . 13 (((𝜑𝑦 ∈ ℝ+) ∧ ∃𝑧 ∈ ℝ+𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) → ∃𝑎𝐴 ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦))
191190adantllr 698 . . . . . . . . . . . 12 ((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ ∃𝑧 ∈ ℝ+𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) → ∃𝑎𝐴 ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦))
192 fresin 6213 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝐹:𝐴⟶ℂ → (𝐹 ↾ (𝐵(,)+∞)):(𝐴 ∩ (𝐵(,)+∞))⟶ℂ)
19336, 192syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → (𝐹 ↾ (𝐵(,)+∞)):(𝐴 ∩ (𝐵(,)+∞))⟶ℂ)
194 inss2 3982 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝐴 ∩ (𝐵(,)+∞)) ⊆ (𝐵(,)+∞)
195 ioosscn 40237 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝐵(,)+∞) ⊆ ℂ
196194, 195sstri 3761 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝐴 ∩ (𝐵(,)+∞)) ⊆ ℂ
197196a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → (𝐴 ∩ (𝐵(,)+∞)) ⊆ ℂ)
198193, 197, 55ellimc3 23863 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → (𝑅 ∈ ((𝐹 ↾ (𝐵(,)+∞)) lim 𝐵) ↔ (𝑅 ∈ ℂ ∧ ∀𝑦 ∈ ℝ+𝑣 ∈ ℝ+𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦))))
1992, 198mpbid 222 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (𝑅 ∈ ℂ ∧ ∀𝑦 ∈ ℝ+𝑣 ∈ ℝ+𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)))
200199simprd 483 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → ∀𝑦 ∈ ℝ+𝑣 ∈ ℝ+𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦))
201200r19.21bi 3081 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑦 ∈ ℝ+) → ∃𝑣 ∈ ℝ+𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦))
2022013ad2ant1 1127 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) → ∃𝑣 ∈ ℝ+𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦))
203 simp11l 1368 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) → 𝜑)
204 simp12 1246 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) → 𝑧 ∈ ℝ+)
205 simp2 1131 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) → 𝑣 ∈ ℝ+)
206 inss1 3981 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((limPt‘𝐾)‘(𝐴 ∩ (𝐵(,)+∞))) ∩ ℝ) ⊆ ((limPt‘𝐾)‘(𝐴 ∩ (𝐵(,)+∞)))
207206a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝜑 → (((limPt‘𝐾)‘(𝐴 ∩ (𝐵(,)+∞))) ∩ ℝ) ⊆ ((limPt‘𝐾)‘(𝐴 ∩ (𝐵(,)+∞))))
208 ioossre 12440 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝐵(,)+∞) ⊆ ℝ
209194, 208sstri 3761 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝐴 ∩ (𝐵(,)+∞)) ⊆ ℝ
210209a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝜑 → (𝐴 ∩ (𝐵(,)+∞)) ⊆ ℝ)
21176, 78restlp 21208 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝐾 ∈ Top ∧ ℝ ⊆ ℂ ∧ (𝐴 ∩ (𝐵(,)+∞)) ⊆ ℝ) → ((limPt‘𝐽)‘(𝐴 ∩ (𝐵(,)+∞))) = (((limPt‘𝐾)‘(𝐴 ∩ (𝐵(,)+∞))) ∩ ℝ))
21270, 72, 210, 211syl3anc 1476 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝜑 → ((limPt‘𝐽)‘(𝐴 ∩ (𝐵(,)+∞))) = (((limPt‘𝐾)‘(𝐴 ∩ (𝐵(,)+∞))) ∩ ℝ))
21382fveq1i 6333 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((limPt‘(TopOpen‘ℂfld))‘(𝐴 ∩ (𝐵(,)+∞))) = ((limPt‘𝐾)‘(𝐴 ∩ (𝐵(,)+∞)))
214213a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝜑 → ((limPt‘(TopOpen‘ℂfld))‘(𝐴 ∩ (𝐵(,)+∞))) = ((limPt‘𝐾)‘(𝐴 ∩ (𝐵(,)+∞))))
215207, 212, 2143sstr4d 3797 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝜑 → ((limPt‘𝐽)‘(𝐴 ∩ (𝐵(,)+∞))) ⊆ ((limPt‘(TopOpen‘ℂfld))‘(𝐴 ∩ (𝐵(,)+∞))))
216 limclner.blp2 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝜑𝐵 ∈ ((limPt‘𝐽)‘(𝐴 ∩ (𝐵(,)+∞))))
217215, 216sseldd 3753 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝜑𝐵 ∈ ((limPt‘(TopOpen‘ℂfld))‘(𝐴 ∩ (𝐵(,)+∞))))
218197, 55islpcn 40389 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝜑 → (𝐵 ∈ ((limPt‘(TopOpen‘ℂfld))‘(𝐴 ∩ (𝐵(,)+∞))) ↔ ∀𝑢 ∈ ℝ+𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵})(abs‘(𝑏𝐵)) < 𝑢))
219217, 218mpbid 222 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑 → ∀𝑢 ∈ ℝ+𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵})(abs‘(𝑏𝐵)) < 𝑢)
2202193ad2ant1 1127 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑧 ∈ ℝ+𝑣 ∈ ℝ+) → ∀𝑢 ∈ ℝ+𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵})(abs‘(𝑏𝐵)) < 𝑢)
221 breq2 4790 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑢 = if(𝑧𝑣, 𝑧, 𝑣) → ((abs‘(𝑏𝐵)) < 𝑢 ↔ (abs‘(𝑏𝐵)) < if(𝑧𝑣, 𝑧, 𝑣)))
222221rexbidv 3200 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑢 = if(𝑧𝑣, 𝑧, 𝑣) → (∃𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵})(abs‘(𝑏𝐵)) < 𝑢 ↔ ∃𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵})(abs‘(𝑏𝐵)) < if(𝑧𝑣, 𝑧, 𝑣)))
223222rspcva 3458 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((if(𝑧𝑣, 𝑧, 𝑣) ∈ ℝ+ ∧ ∀𝑢 ∈ ℝ+𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵})(abs‘(𝑏𝐵)) < 𝑢) → ∃𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵})(abs‘(𝑏𝐵)) < if(𝑧𝑣, 𝑧, 𝑣))
22465, 220, 223syl2anc 573 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑧 ∈ ℝ+𝑣 ∈ ℝ+) → ∃𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵})(abs‘(𝑏𝐵)) < if(𝑧𝑣, 𝑧, 𝑣))
225 eldifi 3883 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵}) → 𝑏 ∈ (𝐴 ∩ (𝐵(,)+∞)))
226209, 225sseldi 3750 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵}) → 𝑏 ∈ ℝ)
22772sselda 3752 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝜑𝑏 ∈ ℝ) → 𝑏 ∈ ℂ)
22855adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝜑𝑏 ∈ ℝ) → 𝐵 ∈ ℂ)
229227, 228subcld 10594 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝜑𝑏 ∈ ℝ) → (𝑏𝐵) ∈ ℂ)
230229abscld 14383 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝜑𝑏 ∈ ℝ) → (abs‘(𝑏𝐵)) ∈ ℝ)
2312303ad2antl1 1200 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝜑𝑧 ∈ ℝ+𝑣 ∈ ℝ+) ∧ 𝑏 ∈ ℝ) → (abs‘(𝑏𝐵)) ∈ ℝ)
232231adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝜑𝑧 ∈ ℝ+𝑣 ∈ ℝ+) ∧ 𝑏 ∈ ℝ) ∧ (abs‘(𝑏𝐵)) < if(𝑧𝑣, 𝑧, 𝑣)) → (abs‘(𝑏𝐵)) ∈ ℝ)
233102ad2antrr 705 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝜑𝑧 ∈ ℝ+𝑣 ∈ ℝ+) ∧ 𝑏 ∈ ℝ) ∧ (abs‘(𝑏𝐵)) < if(𝑧𝑣, 𝑧, 𝑣)) → if(𝑧𝑣, 𝑧, 𝑣) ∈ ℝ)
234105ad2antrr 705 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝜑𝑧 ∈ ℝ+𝑣 ∈ ℝ+) ∧ 𝑏 ∈ ℝ) ∧ (abs‘(𝑏𝐵)) < if(𝑧𝑣, 𝑧, 𝑣)) → 𝑧 ∈ ℝ)
235 simpr 471 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝜑𝑧 ∈ ℝ+𝑣 ∈ ℝ+) ∧ 𝑏 ∈ ℝ) ∧ (abs‘(𝑏𝐵)) < if(𝑧𝑣, 𝑧, 𝑣)) → (abs‘(𝑏𝐵)) < if(𝑧𝑣, 𝑧, 𝑣))
236111ad2antrr 705 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝜑𝑧 ∈ ℝ+𝑣 ∈ ℝ+) ∧ 𝑏 ∈ ℝ) ∧ (abs‘(𝑏𝐵)) < if(𝑧𝑣, 𝑧, 𝑣)) → if(𝑧𝑣, 𝑧, 𝑣) ≤ 𝑧)
237232, 233, 234, 235, 236ltletrd 10399 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝜑𝑧 ∈ ℝ+𝑣 ∈ ℝ+) ∧ 𝑏 ∈ ℝ) ∧ (abs‘(𝑏𝐵)) < if(𝑧𝑣, 𝑧, 𝑣)) → (abs‘(𝑏𝐵)) < 𝑧)
238115ad2antrr 705 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝜑𝑧 ∈ ℝ+𝑣 ∈ ℝ+) ∧ 𝑏 ∈ ℝ) ∧ (abs‘(𝑏𝐵)) < if(𝑧𝑣, 𝑧, 𝑣)) → 𝑣 ∈ ℝ)
239234, 238, 117syl2anc 573 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝜑𝑧 ∈ ℝ+𝑣 ∈ ℝ+) ∧ 𝑏 ∈ ℝ) ∧ (abs‘(𝑏𝐵)) < if(𝑧𝑣, 𝑧, 𝑣)) → if(𝑧𝑣, 𝑧, 𝑣) ≤ 𝑣)
240232, 233, 238, 235, 239ltletrd 10399 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝜑𝑧 ∈ ℝ+𝑣 ∈ ℝ+) ∧ 𝑏 ∈ ℝ) ∧ (abs‘(𝑏𝐵)) < if(𝑧𝑣, 𝑧, 𝑣)) → (abs‘(𝑏𝐵)) < 𝑣)
241237, 240jca 501 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑𝑧 ∈ ℝ+𝑣 ∈ ℝ+) ∧ 𝑏 ∈ ℝ) ∧ (abs‘(𝑏𝐵)) < if(𝑧𝑣, 𝑧, 𝑣)) → ((abs‘(𝑏𝐵)) < 𝑧 ∧ (abs‘(𝑏𝐵)) < 𝑣))
242241ex 397 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑𝑧 ∈ ℝ+𝑣 ∈ ℝ+) ∧ 𝑏 ∈ ℝ) → ((abs‘(𝑏𝐵)) < if(𝑧𝑣, 𝑧, 𝑣) → ((abs‘(𝑏𝐵)) < 𝑧 ∧ (abs‘(𝑏𝐵)) < 𝑣)))
243226, 242sylan2 580 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑧 ∈ ℝ+𝑣 ∈ ℝ+) ∧ 𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵})) → ((abs‘(𝑏𝐵)) < if(𝑧𝑣, 𝑧, 𝑣) → ((abs‘(𝑏𝐵)) < 𝑧 ∧ (abs‘(𝑏𝐵)) < 𝑣)))
244243reximdva 3165 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑧 ∈ ℝ+𝑣 ∈ ℝ+) → (∃𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵})(abs‘(𝑏𝐵)) < if(𝑧𝑣, 𝑧, 𝑣) → ∃𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵})((abs‘(𝑏𝐵)) < 𝑧 ∧ (abs‘(𝑏𝐵)) < 𝑣)))
245224, 244mpd 15 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑧 ∈ ℝ+𝑣 ∈ ℝ+) → ∃𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵})((abs‘(𝑏𝐵)) < 𝑧 ∧ (abs‘(𝑏𝐵)) < 𝑣))
246203, 204, 205, 245syl3anc 1476 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) → ∃𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵})((abs‘(𝑏𝐵)) < 𝑧 ∧ (abs‘(𝑏𝐵)) < 𝑣))
247 nfv 1995 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑏(((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦))
248 nfre1 3153 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑏𝑏𝐴 ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦)
249 inss1 3981 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝐴 ∩ (𝐵(,)+∞)) ⊆ 𝐴
250249, 225sseldi 3750 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵}) → 𝑏𝐴)
2512503ad2ant2 1128 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) ∧ 𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵}) ∧ ((abs‘(𝑏𝐵)) < 𝑧 ∧ (abs‘(𝑏𝐵)) < 𝑣)) → 𝑏𝐴)
252 simp113 1388 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) ∧ 𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵}) ∧ ((abs‘(𝑏𝐵)) < 𝑧 ∧ (abs‘(𝑏𝐵)) < 𝑣)) → ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦))
253 eldifsni 4457 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵}) → 𝑏𝐵)
254253adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵}) ∧ ((abs‘(𝑏𝐵)) < 𝑧 ∧ (abs‘(𝑏𝐵)) < 𝑣)) → 𝑏𝐵)
255 simprl 754 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵}) ∧ ((abs‘(𝑏𝐵)) < 𝑧 ∧ (abs‘(𝑏𝐵)) < 𝑣)) → (abs‘(𝑏𝐵)) < 𝑧)
256254, 255jca 501 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵}) ∧ ((abs‘(𝑏𝐵)) < 𝑧 ∧ (abs‘(𝑏𝐵)) < 𝑣)) → (𝑏𝐵 ∧ (abs‘(𝑏𝐵)) < 𝑧))
2572563adant1 1124 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) ∧ 𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵}) ∧ ((abs‘(𝑏𝐵)) < 𝑧 ∧ (abs‘(𝑏𝐵)) < 𝑣)) → (𝑏𝐵 ∧ (abs‘(𝑏𝐵)) < 𝑧))
258 neeq1 3005 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑤 = 𝑏 → (𝑤𝐵𝑏𝐵))
259 fvoveq1 6816 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑤 = 𝑏 → (abs‘(𝑤𝐵)) = (abs‘(𝑏𝐵)))
260259breq1d 4796 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑤 = 𝑏 → ((abs‘(𝑤𝐵)) < 𝑧 ↔ (abs‘(𝑏𝐵)) < 𝑧))
261258, 260anbi12d 616 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑤 = 𝑏 → ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) ↔ (𝑏𝐵 ∧ (abs‘(𝑏𝐵)) < 𝑧)))
262 fveq2 6332 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑤 = 𝑏 → (𝐹𝑤) = (𝐹𝑏))
263262fvoveq1d 6815 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑤 = 𝑏 → (abs‘((𝐹𝑤) − 𝑥)) = (abs‘((𝐹𝑏) − 𝑥)))
264263breq1d 4796 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑤 = 𝑏 → ((abs‘((𝐹𝑤) − 𝑥)) < 𝑦 ↔ (abs‘((𝐹𝑏) − 𝑥)) < 𝑦))
265261, 264imbi12d 333 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑤 = 𝑏 → (((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦) ↔ ((𝑏𝐵 ∧ (abs‘(𝑏𝐵)) < 𝑧) → (abs‘((𝐹𝑏) − 𝑥)) < 𝑦)))
266265rspcva 3458 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑏𝐴 ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) → ((𝑏𝐵 ∧ (abs‘(𝑏𝐵)) < 𝑧) → (abs‘((𝐹𝑏) − 𝑥)) < 𝑦))
267266imp 393 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝑏𝐴 ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ (𝑏𝐵 ∧ (abs‘(𝑏𝐵)) < 𝑧)) → (abs‘((𝐹𝑏) − 𝑥)) < 𝑦)
268251, 252, 257, 267syl21anc 1475 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) ∧ 𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵}) ∧ ((abs‘(𝑏𝐵)) < 𝑧 ∧ (abs‘(𝑏𝐵)) < 𝑣)) → (abs‘((𝐹𝑏) − 𝑥)) < 𝑦)
2692253ad2ant2 1128 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) ∧ 𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵}) ∧ ((abs‘(𝑏𝐵)) < 𝑧 ∧ (abs‘(𝑏𝐵)) < 𝑣)) → 𝑏 ∈ (𝐴 ∩ (𝐵(,)+∞)))
2702033ad2ant1 1127 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) ∧ 𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵}) ∧ ((abs‘(𝑏𝐵)) < 𝑧 ∧ (abs‘(𝑏𝐵)) < 𝑣)) → 𝜑)
271 simp13 1247 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) ∧ 𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵}) ∧ ((abs‘(𝑏𝐵)) < 𝑧 ∧ (abs‘(𝑏𝐵)) < 𝑣)) → ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦))
272 nfra1 3090 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 𝑤𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)
273153, 272nfan 1980 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 𝑤(𝜑 ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦))
274 elinel2 3951 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞)) → 𝑤 ∈ (𝐵(,)+∞))
275 fvres 6348 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑤 ∈ (𝐵(,)+∞) → ((𝐹 ↾ (𝐵(,)+∞))‘𝑤) = (𝐹𝑤))
276274, 275syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞)) → ((𝐹 ↾ (𝐵(,)+∞))‘𝑤) = (𝐹𝑤))
277276eqcomd 2777 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞)) → (𝐹𝑤) = ((𝐹 ↾ (𝐵(,)+∞))‘𝑤))
278277fvoveq1d 6815 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞)) → (abs‘((𝐹𝑤) − 𝑅)) = (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)))
2792783ad2ant2 1128 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝜑 ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) ∧ 𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞)) ∧ (𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣)) → (abs‘((𝐹𝑤) − 𝑅)) = (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)))
280 rspa 3079 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦) ∧ 𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))) → ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦))
2812803impia 1109 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦) ∧ 𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞)) ∧ (𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣)) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)
2822813adant1l 1185 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝜑 ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) ∧ 𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞)) ∧ (𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣)) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)
283279, 282eqbrtrd 4808 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝜑 ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) ∧ 𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞)) ∧ (𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣)) → (abs‘((𝐹𝑤) − 𝑅)) < 𝑦)
2842833exp 1112 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑 ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) → (𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞)) → ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘((𝐹𝑤) − 𝑅)) < 𝑦)))
285273, 284ralrimi 3106 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑 ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) → ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘((𝐹𝑤) − 𝑅)) < 𝑦))
286270, 271, 285syl2anc 573 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) ∧ 𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵}) ∧ ((abs‘(𝑏𝐵)) < 𝑧 ∧ (abs‘(𝑏𝐵)) < 𝑣)) → ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘((𝐹𝑤) − 𝑅)) < 𝑦))
287253anim1i 602 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵}) ∧ (abs‘(𝑏𝐵)) < 𝑣) → (𝑏𝐵 ∧ (abs‘(𝑏𝐵)) < 𝑣))
288287adantrl 695 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵}) ∧ ((abs‘(𝑏𝐵)) < 𝑧 ∧ (abs‘(𝑏𝐵)) < 𝑣)) → (𝑏𝐵 ∧ (abs‘(𝑏𝐵)) < 𝑣))
2892883adant1 1124 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) ∧ 𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵}) ∧ ((abs‘(𝑏𝐵)) < 𝑧 ∧ (abs‘(𝑏𝐵)) < 𝑣)) → (𝑏𝐵 ∧ (abs‘(𝑏𝐵)) < 𝑣))
290259breq1d 4796 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑤 = 𝑏 → ((abs‘(𝑤𝐵)) < 𝑣 ↔ (abs‘(𝑏𝐵)) < 𝑣))
291258, 290anbi12d 616 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑤 = 𝑏 → ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) ↔ (𝑏𝐵 ∧ (abs‘(𝑏𝐵)) < 𝑣)))
292262fvoveq1d 6815 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑤 = 𝑏 → (abs‘((𝐹𝑤) − 𝑅)) = (abs‘((𝐹𝑏) − 𝑅)))
293292breq1d 4796 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑤 = 𝑏 → ((abs‘((𝐹𝑤) − 𝑅)) < 𝑦 ↔ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦))
294291, 293imbi12d 333 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑤 = 𝑏 → (((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘((𝐹𝑤) − 𝑅)) < 𝑦) ↔ ((𝑏𝐵 ∧ (abs‘(𝑏𝐵)) < 𝑣) → (abs‘((𝐹𝑏) − 𝑅)) < 𝑦)))
295294rspcva 3458 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑏 ∈ (𝐴 ∩ (𝐵(,)+∞)) ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘((𝐹𝑤) − 𝑅)) < 𝑦)) → ((𝑏𝐵 ∧ (abs‘(𝑏𝐵)) < 𝑣) → (abs‘((𝐹𝑏) − 𝑅)) < 𝑦))
296295imp 393 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝑏 ∈ (𝐴 ∩ (𝐵(,)+∞)) ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘((𝐹𝑤) − 𝑅)) < 𝑦)) ∧ (𝑏𝐵 ∧ (abs‘(𝑏𝐵)) < 𝑣)) → (abs‘((𝐹𝑏) − 𝑅)) < 𝑦)
297269, 286, 289, 296syl21anc 1475 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) ∧ 𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵}) ∧ ((abs‘(𝑏𝐵)) < 𝑧 ∧ (abs‘(𝑏𝐵)) < 𝑣)) → (abs‘((𝐹𝑏) − 𝑅)) < 𝑦)
298 rspe 3151 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑏𝐴 ∧ ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦)) → ∃𝑏𝐴 ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦))
299251, 268, 297, 298syl12anc 1474 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) ∧ 𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵}) ∧ ((abs‘(𝑏𝐵)) < 𝑧 ∧ (abs‘(𝑏𝐵)) < 𝑣)) → ∃𝑏𝐴 ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦))
3002993exp 1112 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) → (𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵}) → (((abs‘(𝑏𝐵)) < 𝑧 ∧ (abs‘(𝑏𝐵)) < 𝑣) → ∃𝑏𝐴 ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦))))
301247, 248, 300rexlimd 3174 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) → (∃𝑏 ∈ ((𝐴 ∩ (𝐵(,)+∞)) ∖ {𝐵})((abs‘(𝑏𝐵)) < 𝑧 ∧ (abs‘(𝑏𝐵)) < 𝑣) → ∃𝑏𝐴 ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦)))
302246, 301mpd 15 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦)) → ∃𝑏𝐴 ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦))
3033023exp 1112 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) → (𝑣 ∈ ℝ+ → (∀𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦) → ∃𝑏𝐴 ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦))))
304303rexlimdv 3178 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) → (∃𝑣 ∈ ℝ+𝑤 ∈ (𝐴 ∩ (𝐵(,)+∞))((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑣) → (abs‘(((𝐹 ↾ (𝐵(,)+∞))‘𝑤) − 𝑅)) < 𝑦) → ∃𝑏𝐴 ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦)))
305202, 304mpd 15 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ ∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) → ∃𝑏𝐴 ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦))
3063053exp 1112 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑦 ∈ ℝ+) → (𝑧 ∈ ℝ+ → (∀𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦) → ∃𝑏𝐴 ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦))))
307306rexlimdv 3178 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑦 ∈ ℝ+) → (∃𝑧 ∈ ℝ+𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦) → ∃𝑏𝐴 ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦)))
308307imp 393 . . . . . . . . . . . . . . . . 17 (((𝜑𝑦 ∈ ℝ+) ∧ ∃𝑧 ∈ ℝ+𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) → ∃𝑏𝐴 ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦))
309308adantllr 698 . . . . . . . . . . . . . . . 16 ((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ ∃𝑧 ∈ ℝ+𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) → ∃𝑏𝐴 ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦))
310309ad2antrr 705 . . . . . . . . . . . . . . 15 ((((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ ∃𝑧 ∈ ℝ+𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ 𝑎𝐴) ∧ ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)) → ∃𝑏𝐴 ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦))
3113ad6antr 720 . . . . . . . . . . . . . . . . . . . . 21 (((((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎𝐴) ∧ ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏𝐴) ∧ ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦)) → 𝑅 ∈ ℂ)
3127ad6antr 720 . . . . . . . . . . . . . . . . . . . . 21 (((((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎𝐴) ∧ ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏𝐴) ∧ ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦)) → 𝐿 ∈ ℂ)
313311, 312subcld 10594 . . . . . . . . . . . . . . . . . . . 20 (((((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎𝐴) ∧ ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏𝐴) ∧ ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦)) → (𝑅𝐿) ∈ ℂ)
314313abscld 14383 . . . . . . . . . . . . . . . . . . 19 (((((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎𝐴) ∧ ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏𝐴) ∧ ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦)) → (abs‘(𝑅𝐿)) ∈ ℝ)
315 simp-6l 776 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎𝐴) ∧ ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏𝐴) ∧ ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦)) → 𝜑)
316 simplr 752 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎𝐴) ∧ ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏𝐴) ∧ ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦)) → 𝑏𝐴)
31736ffvelrnda 6502 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑏𝐴) → (𝐹𝑏) ∈ ℂ)
318315, 316, 317syl2anc 573 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎𝐴) ∧ ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏𝐴) ∧ ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦)) → (𝐹𝑏) ∈ ℂ)
319311, 318subcld 10594 . . . . . . . . . . . . . . . . . . . . . . 23 (((((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎𝐴) ∧ ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏𝐴) ∧ ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦)) → (𝑅 − (𝐹𝑏)) ∈ ℂ)
320319abscld 14383 . . . . . . . . . . . . . . . . . . . . . 22 (((((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎𝐴) ∧ ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏𝐴) ∧ ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦)) → (abs‘(𝑅 − (𝐹𝑏))) ∈ ℝ)
321 simp-6r 778 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎𝐴) ∧ ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏𝐴) ∧ ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦)) → 𝑥 ∈ ℂ)
322318, 321subcld 10594 . . . . . . . . . . . . . . . . . . . . . . 23 (((((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎𝐴) ∧ ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏𝐴) ∧ ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦)) → ((𝐹𝑏) − 𝑥) ∈ ℂ)
323322abscld 14383 . . . . . . . . . . . . . . . . . . . . . 22 (((((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎𝐴) ∧ ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏𝐴) ∧ ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦)) → (abs‘((𝐹𝑏) − 𝑥)) ∈ ℝ)
324320, 323readdcld 10271 . . . . . . . . . . . . . . . . . . . . 21 (((((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎𝐴) ∧ ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏𝐴) ∧ ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦)) → ((abs‘(𝑅 − (𝐹𝑏))) + (abs‘((𝐹𝑏) − 𝑥))) ∈ ℝ)
325 simp-4r 770 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎𝐴) ∧ ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏𝐴) ∧ ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦)) → 𝑎𝐴)
32636ffvelrnda 6502 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑎𝐴) → (𝐹𝑎) ∈ ℂ)
327315, 325, 326syl2anc 573 . . . . . . . . . . . . . . . . . . . . . . 23 (((((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎𝐴) ∧ ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏𝐴) ∧ ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦)) → (𝐹𝑎) ∈ ℂ)
328321, 327subcld 10594 . . . . . . . . . . . . . . . . . . . . . 22 (((((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎𝐴) ∧ ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏𝐴) ∧ ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦)) → (𝑥 − (𝐹𝑎)) ∈ ℂ)
329328abscld 14383 . . . . . . . . . . . . . . . . . . . . 21 (((((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎𝐴) ∧ ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏𝐴) ∧ ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦)) → (abs‘(𝑥 − (𝐹𝑎))) ∈ ℝ)
330324, 329readdcld 10271 . . . . . . . . . . . . . . . . . . . 20 (((((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎𝐴) ∧ ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏𝐴) ∧ ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦)) → (((abs‘(𝑅 − (𝐹𝑏))) + (abs‘((𝐹𝑏) − 𝑥))) + (abs‘(𝑥 − (𝐹𝑎)))) ∈ ℝ)
331327, 312subcld 10594 . . . . . . . . . . . . . . . . . . . . 21 (((((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎𝐴) ∧ ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏𝐴) ∧ ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦)) → ((𝐹𝑎) − 𝐿) ∈ ℂ)
332331abscld 14383 . . . . . . . . . . . . . . . . . . . 20 (((((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎𝐴) ∧ ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏𝐴) ∧ ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦)) → (abs‘((𝐹𝑎) − 𝐿)) ∈ ℝ)
333330, 332readdcld 10271 . . . . . . . . . . . . . . . . . . 19 (((((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎𝐴) ∧ ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏𝐴) ∧ ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦)) → ((((abs‘(𝑅 − (𝐹𝑏))) + (abs‘((𝐹𝑏) − 𝑥))) + (abs‘(𝑥 − (𝐹𝑎)))) + (abs‘((𝐹𝑎) − 𝐿))) ∈ ℝ)
33415a1i 11 . . . . . . . . . . . . . . . . . . . 20 (((((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎𝐴) ∧ ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏𝐴) ∧ ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦)) → 4 ∈ ℝ)
335 rpre 12042 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 ∈ ℝ+𝑦 ∈ ℝ)
336335ad5antlr 718 . . . . . . . . . . . . . . . . . . . 20 (((((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎𝐴) ∧ ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏𝐴) ∧ ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦)) → 𝑦 ∈ ℝ)
337334, 336remulcld 10272 . . . . . . . . . . . . . . . . . . 19 (((((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎𝐴) ∧ ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏𝐴) ∧ ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦)) → (4 · 𝑦) ∈ ℝ)
338311, 318, 321, 327, 312absnpncan3d 40038 . . . . . . . . . . . . . . . . . . 19 (((((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎𝐴) ∧ ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏𝐴) ∧ ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦)) → (abs‘(𝑅𝐿)) ≤ ((((abs‘(𝑅 − (𝐹𝑏))) + (abs‘((𝐹𝑏) − 𝑥))) + (abs‘(𝑥 − (𝐹𝑎)))) + (abs‘((𝐹𝑎) − 𝐿))))
339311, 318abssubd 14400 . . . . . . . . . . . . . . . . . . . . 21 (((((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎𝐴) ∧ ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏𝐴) ∧ ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦)) → (abs‘(𝑅 − (𝐹𝑏))) = (abs‘((𝐹𝑏) − 𝑅)))
340 simprr 756 . . . . . . . . . . . . . . . . . . . . 21 (((((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎𝐴) ∧ ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏𝐴) ∧ ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦)) → (abs‘((𝐹𝑏) − 𝑅)) < 𝑦)
341339, 340eqbrtrd 4808 . . . . . . . . . . . . . . . . . . . 20 (((((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎𝐴) ∧ ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏𝐴) ∧ ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦)) → (abs‘(𝑅 − (𝐹𝑏))) < 𝑦)
342 simprl 754 . . . . . . . . . . . . . . . . . . . 20 (((((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎𝐴) ∧ ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏𝐴) ∧ ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦)) → (abs‘((𝐹𝑏) − 𝑥)) < 𝑦)
343 simp-5r 774 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎𝐴) ∧ ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏𝐴) → 𝑥 ∈ ℂ)
344 simp-4l 768 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎𝐴) ∧ ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)) → 𝜑)
345 simplr 752 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎𝐴) ∧ ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)) → 𝑎𝐴)
346344, 345, 326syl2anc 573 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎𝐴) ∧ ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)) → (𝐹𝑎) ∈ ℂ)
347346adantr 466 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎𝐴) ∧ ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏𝐴) → (𝐹𝑎) ∈ ℂ)
348343, 347abssubd 14400 . . . . . . . . . . . . . . . . . . . . . 22 ((((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎𝐴) ∧ ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏𝐴) → (abs‘(𝑥 − (𝐹𝑎))) = (abs‘((𝐹𝑎) − 𝑥)))
349 simplrl 762 . . . . . . . . . . . . . . . . . . . . . 22 ((((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎𝐴) ∧ ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏𝐴) → (abs‘((𝐹𝑎) − 𝑥)) < 𝑦)
350348, 349eqbrtrd 4808 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎𝐴) ∧ ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏𝐴) → (abs‘(𝑥 − (𝐹𝑎))) < 𝑦)
351350adantr 466 . . . . . . . . . . . . . . . . . . . 20 (((((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎𝐴) ∧ ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏𝐴) ∧ ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦)) → (abs‘(𝑥 − (𝐹𝑎))) < 𝑦)
352 simplrr 763 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎𝐴) ∧ ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏𝐴) → (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)
353352adantr 466 . . . . . . . . . . . . . . . . . . . 20 (((((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎𝐴) ∧ ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏𝐴) ∧ ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦)) → (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)
354320, 323, 329, 332, 336, 341, 342, 351, 353lt4addmuld 40037 . . . . . . . . . . . . . . . . . . 19 (((((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎𝐴) ∧ ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏𝐴) ∧ ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦)) → ((((abs‘(𝑅 − (𝐹𝑏))) + (abs‘((𝐹𝑏) − 𝑥))) + (abs‘(𝑥 − (𝐹𝑎)))) + (abs‘((𝐹𝑎) − 𝐿))) < (4 · 𝑦))
355314, 333, 337, 338, 354lelttrd 10397 . . . . . . . . . . . . . . . . . 18 (((((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎𝐴) ∧ ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏𝐴) ∧ ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦)) → (abs‘(𝑅𝐿)) < (4 · 𝑦))
356355ex 397 . . . . . . . . . . . . . . . . 17 ((((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ 𝑎𝐴) ∧ ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏𝐴) → (((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦) → (abs‘(𝑅𝐿)) < (4 · 𝑦)))
357356adantl3r 744 . . . . . . . . . . . . . . . 16 (((((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ ∃𝑧 ∈ ℝ+𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ 𝑎𝐴) ∧ ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)) ∧ 𝑏𝐴) → (((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦) → (abs‘(𝑅𝐿)) < (4 · 𝑦)))
358357reximdva 3165 . . . . . . . . . . . . . . 15 ((((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ ∃𝑧 ∈ ℝ+𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ 𝑎𝐴) ∧ ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)) → (∃𝑏𝐴 ((abs‘((𝐹𝑏) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑏) − 𝑅)) < 𝑦) → ∃𝑏𝐴 (abs‘(𝑅𝐿)) < (4 · 𝑦)))
359310, 358mpd 15 . . . . . . . . . . . . . 14 ((((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ ∃𝑧 ∈ ℝ+𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ 𝑎𝐴) ∧ ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦)) → ∃𝑏𝐴 (abs‘(𝑅𝐿)) < (4 · 𝑦))
360359ex 397 . . . . . . . . . . . . 13 (((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ ∃𝑧 ∈ ℝ+𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ 𝑎𝐴) → (((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦) → ∃𝑏𝐴 (abs‘(𝑅𝐿)) < (4 · 𝑦)))
361360reximdva 3165 . . . . . . . . . . . 12 ((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ ∃𝑧 ∈ ℝ+𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) → (∃𝑎𝐴 ((abs‘((𝐹𝑎) − 𝑥)) < 𝑦 ∧ (abs‘((𝐹𝑎) − 𝐿)) < 𝑦) → ∃𝑎𝐴𝑏𝐴 (abs‘(𝑅𝐿)) < (4 · 𝑦)))
362191, 361mpd 15 . . . . . . . . . . 11 ((((𝜑𝑥 ∈ ℂ) ∧ 𝑦 ∈ ℝ+) ∧ ∃𝑧 ∈ ℝ+𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) → ∃𝑎𝐴𝑏𝐴 (abs‘(𝑅𝐿)) < (4 · 𝑦))
36332, 33, 35, 362syl21anc 1475 . . . . . . . . . 10 ((((𝜑𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ∧ 𝑦 ∈ ℝ+) → ∃𝑎𝐴𝑏𝐴 (abs‘(𝑅𝐿)) < (4 · 𝑦))
364363ex 397 . . . . . . . . 9 (((𝜑𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) → (𝑦 ∈ ℝ+ → ∃𝑎𝐴𝑏𝐴 (abs‘(𝑅𝐿)) < (4 · 𝑦)))
36524, 25, 31, 364vtoclf 3409 . . . . . . . 8 (((𝜑𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) → (((abs‘(𝑅𝐿)) / 4) ∈ ℝ+ → ∃𝑎𝐴𝑏𝐴 (abs‘(𝑅𝐿)) < (4 · ((abs‘(𝑅𝐿)) / 4))))
36619, 365mpd 15 . . . . . . 7 (((𝜑𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) → ∃𝑎𝐴𝑏𝐴 (abs‘(𝑅𝐿)) < (4 · ((abs‘(𝑅𝐿)) / 4)))
367 simpr 471 . . . . . . . . . . . 12 ((𝜑 ∧ (abs‘(𝑅𝐿)) < (4 · ((abs‘(𝑅𝐿)) / 4))) → (abs‘(𝑅𝐿)) < (4 · ((abs‘(𝑅𝐿)) / 4)))
368 abssubrp 40005 . . . . . . . . . . . . . . . 16 ((𝑅 ∈ ℂ ∧ 𝐿 ∈ ℂ ∧ 𝑅𝐿) → (abs‘(𝑅𝐿)) ∈ ℝ+)
3693, 7, 11, 368syl3anc 1476 . . . . . . . . . . . . . . 15 (𝜑 → (abs‘(𝑅𝐿)) ∈ ℝ+)
370369rpcnd 12077 . . . . . . . . . . . . . 14 (𝜑 → (abs‘(𝑅𝐿)) ∈ ℂ)
371370adantr 466 . . . . . . . . . . . . 13 ((𝜑 ∧ (abs‘(𝑅𝐿)) < (4 · ((abs‘(𝑅𝐿)) / 4))) → (abs‘(𝑅𝐿)) ∈ ℂ)
372 4cn 11300 . . . . . . . . . . . . . 14 4 ∈ ℂ
373372a1i 11 . . . . . . . . . . . . 13 ((𝜑 ∧ (abs‘(𝑅𝐿)) < (4 · ((abs‘(𝑅𝐿)) / 4))) → 4 ∈ ℂ)
374 4ne0 11319 . . . . . . . . . . . . . 14 4 ≠ 0
375374a1i 11 . . . . . . . . . . . . 13 ((𝜑 ∧ (abs‘(𝑅𝐿)) < (4 · ((abs‘(𝑅𝐿)) / 4))) → 4 ≠ 0)
376371, 373, 375divcan2d 11005 . . . . . . . . . . . 12 ((𝜑 ∧ (abs‘(𝑅𝐿)) < (4 · ((abs‘(𝑅𝐿)) / 4))) → (4 · ((abs‘(𝑅𝐿)) / 4)) = (abs‘(𝑅𝐿)))
377367, 376breqtrd 4812 . . . . . . . . . . 11 ((𝜑 ∧ (abs‘(𝑅𝐿)) < (4 · ((abs‘(𝑅𝐿)) / 4))) → (abs‘(𝑅𝐿)) < (abs‘(𝑅𝐿)))
378377ex 397 . . . . . . . . . 10 (𝜑 → ((abs‘(𝑅𝐿)) < (4 · ((abs‘(𝑅𝐿)) / 4)) → (abs‘(𝑅𝐿)) < (abs‘(𝑅𝐿))))
379378a1d 25 . . . . . . . . 9 (𝜑 → ((𝑎𝐴𝑏𝐴) → ((abs‘(𝑅𝐿)) < (4 · ((abs‘(𝑅𝐿)) / 4)) → (abs‘(𝑅𝐿)) < (abs‘(𝑅𝐿)))))
380379ad2antrr 705 . . . . . . . 8 (((𝜑𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) → ((𝑎𝐴𝑏𝐴) → ((abs‘(𝑅𝐿)) < (4 · ((abs‘(𝑅𝐿)) / 4)) → (abs‘(𝑅𝐿)) < (abs‘(𝑅𝐿)))))
381380rexlimdvv 3185 . . . . . . 7 (((𝜑𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) → (∃𝑎𝐴𝑏𝐴 (abs‘(𝑅𝐿)) < (4 · ((abs‘(𝑅𝐿)) / 4)) → (abs‘(𝑅𝐿)) < (abs‘(𝑅𝐿))))
382366, 381mpd 15 . . . . . 6 (((𝜑𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) → (abs‘(𝑅𝐿)) < (abs‘(𝑅𝐿)))
3839abscld 14383 . . . . . . 7 (((𝜑𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) → (abs‘(𝑅𝐿)) ∈ ℝ)
384383ltnrd 10373 . . . . . 6 (((𝜑𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) → ¬ (abs‘(𝑅𝐿)) < (abs‘(𝑅𝐿)))
385382, 384pm2.65da 818 . . . . 5 ((𝜑𝑥 ∈ ℂ) → ¬ ∀𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦))
386385ex 397 . . . 4 (𝜑 → (𝑥 ∈ ℂ → ¬ ∀𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)))
387 imnan 386 . . . 4 ((𝑥 ∈ ℂ → ¬ ∀𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)) ↔ ¬ (𝑥 ∈ ℂ ∧ ∀𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)))
388386, 387sylib 208 . . 3 (𝜑 → ¬ (𝑥 ∈ ℂ ∧ ∀𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦)))
389 limclner.a . . . . 5 (𝜑𝐴 ⊆ ℝ)
390389, 72sstrd 3762 . . . 4 (𝜑𝐴 ⊆ ℂ)
39136, 390, 55ellimc3 23863 . . 3 (𝜑 → (𝑥 ∈ (𝐹 lim 𝐵) ↔ (𝑥 ∈ ℂ ∧ ∀𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝐴 ((𝑤𝐵 ∧ (abs‘(𝑤𝐵)) < 𝑧) → (abs‘((𝐹𝑤) − 𝑥)) < 𝑦))))
392388, 391mtbird 314 . 2 (𝜑 → ¬ 𝑥 ∈ (𝐹 lim 𝐵))
393392eq0rdv 4123 1 (𝜑 → (𝐹 lim 𝐵) = ∅)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 382  w3a 1071   = wceq 1631  wcel 2145  wne 2943  wral 3061  wrex 3062  cdif 3720  cin 3722  wss 3723  c0 4063  ifcif 4225  {csn 4316   cuni 4574   class class class wbr 4786  ran crn 5250  cres 5251  wf 6027  cfv 6031  (class class class)co 6793  cc 10136  cr 10137  0cc0 10138   + caddc 10141   · cmul 10143  +∞cpnf 10273  -∞cmnf 10274   < clt 10276  cle 10277  cmin 10468   / cdiv 10886  4c4 11274  +crp 12035  (,)cioo 12380  abscabs 14182  t crest 16289  TopOpenctopn 16290  topGenctg 16306  fldccnfld 19961  Topctop 20918  limPtclp 21159   lim climc 23846
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-8 2147  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-rep 4904  ax-sep 4915  ax-nul 4923  ax-pow 4974  ax-pr 5034  ax-un 7096  ax-cnex 10194  ax-resscn 10195  ax-1cn 10196  ax-icn 10197  ax-addcl 10198  ax-addrcl 10199  ax-mulcl 10200  ax-mulrcl 10201  ax-mulcom 10202  ax-addass 10203  ax-mulass 10204  ax-distr 10205  ax-i2m1 10206  ax-1ne0 10207  ax-1rid 10208  ax-rnegex 10209  ax-rrecex 10210  ax-cnre 10211  ax-pre-lttri 10212  ax-pre-lttrn 10213  ax-pre-ltadd 10214  ax-pre-mulgt0 10215  ax-pre-sup 10216
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-3or 1072  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ne 2944  df-nel 3047  df-ral 3066  df-rex 3067  df-reu 3068  df-rmo 3069  df-rab 3070  df-v 3353  df-sbc 3588  df-csb 3683  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-pss 3739  df-nul 4064  df-if 4226  df-pw 4299  df-sn 4317  df-pr 4319  df-tp 4321  df-op 4323  df-uni 4575  df-int 4612  df-iun 4656  df-iin 4657  df-br 4787  df-opab 4847  df-mpt 4864  df-tr 4887  df-id 5157  df-eprel 5162  df-po 5170  df-so 5171  df-fr 5208  df-we 5210  df-xp 5255  df-rel 5256  df-cnv 5257  df-co 5258  df-dm 5259  df-rn 5260  df-res 5261  df-ima 5262  df-pred 5823  df-ord 5869  df-on 5870  df-lim 5871  df-suc 5872  df-iota 5994  df-fun 6033  df-fn 6034  df-f 6035  df-f1 6036  df-fo 6037  df-f1o 6038  df-fv 6039  df-riota 6754  df-ov 6796  df-oprab 6797  df-mpt2 6798  df-om 7213  df-1st 7315  df-2nd 7316  df-wrecs 7559  df-recs 7621  df-rdg 7659  df-1o 7713  df-oadd 7717  df-er 7896  df-map 8011  df-pm 8012  df-en 8110  df-dom 8111  df-sdom 8112  df-fin 8113  df-fi 8473  df-sup 8504  df-inf 8505  df-pnf 10278  df-mnf 10279  df-xr 10280  df-ltxr 10281  df-le 10282  df-sub 10470  df-neg 10471  df-div 10887  df-nn 11223  df-2 11281  df-3 11282  df-4 11283  df-5 11284  df-6 11285  df-7 11286  df-8 11287  df-9 11288  df-n0 11495  df-z 11580  df-dec 11696  df-uz 11889  df-q 11992  df-rp 12036  df-xneg 12151  df-xadd 12152  df-xmul 12153  df-ioo 12384  df-fz 12534  df-seq 13009  df-exp 13068  df-cj 14047  df-re 14048  df-im 14049  df-sqrt 14183  df-abs 14184  df-struct 16066  df-ndx 16067  df-slot 16068  df-base 16070  df-plusg 16162  df-mulr 16163  df-starv 16164  df-tset 16168  df-ple 16169  df-ds 16172  df-unif 16173  df-rest 16291  df-topn 16292  df-topgen 16312  df-psmet 19953  df-xmet 19954  df-met 19955  df-bl 19956  df-mopn 19957  df-cnfld 19962  df-top 20919  df-topon 20936  df-topsp 20958  df-bases 20971  df-cld 21044  df-ntr 21045  df-cls 21046  df-nei 21123  df-lp 21161  df-cnp 21253  df-xms 22345  df-ms 22346  df-limc 23850
This theorem is referenced by:  limclr  40405  jumpncnp  40629
  Copyright terms: Public domain W3C validator