limclner

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)

	Ref	Expression
Hypotheses	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	limclner	⊢ ( 𝜑 → ( 𝐹 lim_ℂ 𝐵 ) = ∅ )

Proof

Step	Hyp	Ref	Expression
1		limclner.k	⊢ 𝐾 = ( TopOpen ‘ ℂ_fld )
2		limclner.a	⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
3		limclner.j	⊢ 𝐽 = ( topGen ‘ ran (,) )
4		limclner.f	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℂ )
5		limclner.blp1	⊢ ( 𝜑 → 𝐵 ∈ ( ( limPt ‘ 𝐽 ) ‘ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ) )
6		limclner.blp2	⊢ ( 𝜑 → 𝐵 ∈ ( ( limPt ‘ 𝐽 ) ‘ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ) )
7		limclner.l	⊢ ( 𝜑 → 𝐿 ∈ ( ( 𝐹 ↾ ( -∞ (,) 𝐵 ) ) lim_ℂ 𝐵 ) )
8		limclner.r	⊢ ( 𝜑 → 𝑅 ∈ ( ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) lim_ℂ 𝐵 ) )
9		limclner.lner	⊢ ( 𝜑 → 𝐿 ≠ 𝑅 )
10		limccl	⊢ ( ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) lim_ℂ 𝐵 ) ⊆ ℂ
11	10 8	sselid	⊢ ( 𝜑 → 𝑅 ∈ ℂ )
12	11	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ ∀ 𝑦 ∈ ℝ⁺ ∃ 𝑧 ∈ ℝ⁺ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) ) → 𝑅 ∈ ℂ )
13		limccl	⊢ ( ( 𝐹 ↾ ( -∞ (,) 𝐵 ) ) lim_ℂ 𝐵 ) ⊆ ℂ
14	13 7	sselid	⊢ ( 𝜑 → 𝐿 ∈ ℂ )
15	14	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ ∀ 𝑦 ∈ ℝ⁺ ∃ 𝑧 ∈ ℝ⁺ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) ) → 𝐿 ∈ ℂ )
16	12 15	subcld	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ ∀ 𝑦 ∈ ℝ⁺ ∃ 𝑧 ∈ ℝ⁺ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) ) → ( 𝑅 − 𝐿 ) ∈ ℂ )
17	9	necomd	⊢ ( 𝜑 → 𝑅 ≠ 𝐿 )
18	17	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ ∀ 𝑦 ∈ ℝ⁺ ∃ 𝑧 ∈ ℝ⁺ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) ) → 𝑅 ≠ 𝐿 )
19	12 15 18	subne0d	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ ∀ 𝑦 ∈ ℝ⁺ ∃ 𝑧 ∈ ℝ⁺ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) ) → ( 𝑅 − 𝐿 ) ≠ 0 )
20	16 19	absrpcld	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ ∀ 𝑦 ∈ ℝ⁺ ∃ 𝑧 ∈ ℝ⁺ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) ) → ( abs ‘ ( 𝑅 − 𝐿 ) ) ∈ ℝ⁺ )
21		4re	⊢ 4 ∈ ℝ
22		4pos	⊢ 0 < 4
23	21 22	elrpii	⊢ 4 ∈ ℝ⁺
24	23	a1i	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ ∀ 𝑦 ∈ ℝ⁺ ∃ 𝑧 ∈ ℝ⁺ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) ) → 4 ∈ ℝ⁺ )
25	20 24	rpdivcld	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ ∀ 𝑦 ∈ ℝ⁺ ∃ 𝑧 ∈ ℝ⁺ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) ) → ( ( abs ‘ ( 𝑅 − 𝐿 ) ) / 4 ) ∈ ℝ⁺ )
26		nfv	⊢ Ⅎ 𝑦 ( 𝜑 ∧ 𝑥 ∈ ℂ )
27		nfra1	⊢ Ⅎ 𝑦 ∀ 𝑦 ∈ ℝ⁺ ∃ 𝑧 ∈ ℝ⁺ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 )
28	26 27	nfan	⊢ Ⅎ 𝑦 ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ ∀ 𝑦 ∈ ℝ⁺ ∃ 𝑧 ∈ ℝ⁺ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) )
29		nfv	⊢ Ⅎ 𝑦 ( ( ( abs ‘ ( 𝑅 − 𝐿 ) ) / 4 ) ∈ ℝ⁺ → ∃ 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ 𝐴 ( abs ‘ ( 𝑅 − 𝐿 ) ) < ( 4 · ( ( abs ‘ ( 𝑅 − 𝐿 ) ) / 4 ) ) )
30	28 29	nfim	⊢ Ⅎ 𝑦 ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ ∀ 𝑦 ∈ ℝ⁺ ∃ 𝑧 ∈ ℝ⁺ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) ) → ( ( ( abs ‘ ( 𝑅 − 𝐿 ) ) / 4 ) ∈ ℝ⁺ → ∃ 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ 𝐴 ( abs ‘ ( 𝑅 − 𝐿 ) ) < ( 4 · ( ( abs ‘ ( 𝑅 − 𝐿 ) ) / 4 ) ) ) )
31		ovex	⊢ ( ( abs ‘ ( 𝑅 − 𝐿 ) ) / 4 ) ∈ V
32		eleq1	⊢ ( 𝑦 = ( ( abs ‘ ( 𝑅 − 𝐿 ) ) / 4 ) → ( 𝑦 ∈ ℝ⁺ ↔ ( ( abs ‘ ( 𝑅 − 𝐿 ) ) / 4 ) ∈ ℝ⁺ ) )
33		oveq2	⊢ ( 𝑦 = ( ( abs ‘ ( 𝑅 − 𝐿 ) ) / 4 ) → ( 4 · 𝑦 ) = ( 4 · ( ( abs ‘ ( 𝑅 − 𝐿 ) ) / 4 ) ) )
34	33	breq2d	⊢ ( 𝑦 = ( ( abs ‘ ( 𝑅 − 𝐿 ) ) / 4 ) → ( ( abs ‘ ( 𝑅 − 𝐿 ) ) < ( 4 · 𝑦 ) ↔ ( abs ‘ ( 𝑅 − 𝐿 ) ) < ( 4 · ( ( abs ‘ ( 𝑅 − 𝐿 ) ) / 4 ) ) ) )
35	34	2rexbidv	⊢ ( 𝑦 = ( ( abs ‘ ( 𝑅 − 𝐿 ) ) / 4 ) → ( ∃ 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ 𝐴 ( abs ‘ ( 𝑅 − 𝐿 ) ) < ( 4 · 𝑦 ) ↔ ∃ 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ 𝐴 ( abs ‘ ( 𝑅 − 𝐿 ) ) < ( 4 · ( ( abs ‘ ( 𝑅 − 𝐿 ) ) / 4 ) ) ) )
36	32 35	imbi12d	⊢ ( 𝑦 = ( ( abs ‘ ( 𝑅 − 𝐿 ) ) / 4 ) → ( ( 𝑦 ∈ ℝ⁺ → ∃ 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ 𝐴 ( abs ‘ ( 𝑅 − 𝐿 ) ) < ( 4 · 𝑦 ) ) ↔ ( ( ( abs ‘ ( 𝑅 − 𝐿 ) ) / 4 ) ∈ ℝ⁺ → ∃ 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ 𝐴 ( abs ‘ ( 𝑅 − 𝐿 ) ) < ( 4 · ( ( abs ‘ ( 𝑅 − 𝐿 ) ) / 4 ) ) ) ) )
37	36	imbi2d	⊢ ( 𝑦 = ( ( abs ‘ ( 𝑅 − 𝐿 ) ) / 4 ) → ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ ∀ 𝑦 ∈ ℝ⁺ ∃ 𝑧 ∈ ℝ⁺ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) ) → ( 𝑦 ∈ ℝ⁺ → ∃ 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ 𝐴 ( abs ‘ ( 𝑅 − 𝐿 ) ) < ( 4 · 𝑦 ) ) ) ↔ ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ ∀ 𝑦 ∈ ℝ⁺ ∃ 𝑧 ∈ ℝ⁺ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) ) → ( ( ( abs ‘ ( 𝑅 − 𝐿 ) ) / 4 ) ∈ ℝ⁺ → ∃ 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ 𝐴 ( abs ‘ ( 𝑅 − 𝐿 ) ) < ( 4 · ( ( abs ‘ ( 𝑅 − 𝐿 ) ) / 4 ) ) ) ) ) )
38		simpll	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ ∀ 𝑦 ∈ ℝ⁺ ∃ 𝑧 ∈ ℝ⁺ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) ) ∧ 𝑦 ∈ ℝ⁺ ) → ( 𝜑 ∧ 𝑥 ∈ ℂ ) )
39		simpr	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ ∀ 𝑦 ∈ ℝ⁺ ∃ 𝑧 ∈ ℝ⁺ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) ) ∧ 𝑦 ∈ ℝ⁺ ) → 𝑦 ∈ ℝ⁺ )
40		rspa	⊢ ( ( ∀ 𝑦 ∈ ℝ⁺ ∃ 𝑧 ∈ ℝ⁺ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) ∧ 𝑦 ∈ ℝ⁺ ) → ∃ 𝑧 ∈ ℝ⁺ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) )
41	40	adantll	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ ∀ 𝑦 ∈ ℝ⁺ ∃ 𝑧 ∈ ℝ⁺ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) ) ∧ 𝑦 ∈ ℝ⁺ ) → ∃ 𝑧 ∈ ℝ⁺ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) )
42		fresin	⊢ ( 𝐹 : 𝐴 ⟶ ℂ → ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) : ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ⟶ ℂ )
43	4 42	syl	⊢ ( 𝜑 → ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) : ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ⟶ ℂ )
44		inss2	⊢ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ⊆ ( 𝐵 (,) +∞ )
45		ioosscn	⊢ ( 𝐵 (,) +∞ ) ⊆ ℂ
46	44 45	sstri	⊢ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ⊆ ℂ
47	46	a1i	⊢ ( 𝜑 → ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ⊆ ℂ )
48		retop	⊢ ( topGen ‘ ran (,) ) ∈ Top
49	3 48	eqeltri	⊢ 𝐽 ∈ Top
50		inss2	⊢ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ⊆ ( -∞ (,) 𝐵 )
51		ioossre	⊢ ( -∞ (,) 𝐵 ) ⊆ ℝ
52	50 51	sstri	⊢ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ⊆ ℝ
53		uniretop	⊢ ℝ = ∪ ( topGen ‘ ran (,) )
54	3	unieqi	⊢ ∪ 𝐽 = ∪ ( topGen ‘ ran (,) )
55	53 54	eqtr4i	⊢ ℝ = ∪ 𝐽
56	55	lpss	⊢ ( ( 𝐽 ∈ Top ∧ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ⊆ ℝ ) → ( ( limPt ‘ 𝐽 ) ‘ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ) ⊆ ℝ )
57	49 52 56	mp2an	⊢ ( ( limPt ‘ 𝐽 ) ‘ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ) ⊆ ℝ
58	57 5	sselid	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
59	58	recnd	⊢ ( 𝜑 → 𝐵 ∈ ℂ )
60	43 47 59	ellimc3	⊢ ( 𝜑 → ( 𝑅 ∈ ( ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) lim_ℂ 𝐵 ) ↔ ( 𝑅 ∈ ℂ ∧ ∀ 𝑦 ∈ ℝ⁺ ∃ 𝑣 ∈ ℝ⁺ ∀ 𝑤 ∈ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) ‘ 𝑤 ) − 𝑅 ) ) < 𝑦 ) ) ) )
61	8 60	mpbid	⊢ ( 𝜑 → ( 𝑅 ∈ ℂ ∧ ∀ 𝑦 ∈ ℝ⁺ ∃ 𝑣 ∈ ℝ⁺ ∀ 𝑤 ∈ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) ‘ 𝑤 ) − 𝑅 ) ) < 𝑦 ) ) )
62	61	simprd	⊢ ( 𝜑 → ∀ 𝑦 ∈ ℝ⁺ ∃ 𝑣 ∈ ℝ⁺ ∀ 𝑤 ∈ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) ‘ 𝑤 ) − 𝑅 ) ) < 𝑦 ) )
63	62	r19.21bi	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) → ∃ 𝑣 ∈ ℝ⁺ ∀ 𝑤 ∈ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) ‘ 𝑤 ) − 𝑅 ) ) < 𝑦 ) )
64	63	3ad2ant1	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) ) → ∃ 𝑣 ∈ ℝ⁺ ∀ 𝑤 ∈ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) ‘ 𝑤 ) − 𝑅 ) ) < 𝑦 ) )
65		simp11l	⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) ) ∧ 𝑣 ∈ ℝ⁺ ∧ ∀ 𝑤 ∈ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) ‘ 𝑤 ) − 𝑅 ) ) < 𝑦 ) ) → 𝜑 )
66		simp12	⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) ) ∧ 𝑣 ∈ ℝ⁺ ∧ ∀ 𝑤 ∈ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) ‘ 𝑤 ) − 𝑅 ) ) < 𝑦 ) ) → 𝑧 ∈ ℝ⁺ )
67		simp2	⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) ) ∧ 𝑣 ∈ ℝ⁺ ∧ ∀ 𝑤 ∈ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) ‘ 𝑤 ) − 𝑅 ) ) < 𝑦 ) ) → 𝑣 ∈ ℝ⁺ )
68		breq2	⊢ ( 𝑢 = if ( 𝑧 ≤ 𝑣 , 𝑧 , 𝑣 ) → ( ( abs ‘ ( 𝑏 − 𝐵 ) ) < 𝑢 ↔ ( abs ‘ ( 𝑏 − 𝐵 ) ) < if ( 𝑧 ≤ 𝑣 , 𝑧 , 𝑣 ) ) )
69	68	rexbidv	⊢ ( 𝑢 = if ( 𝑧 ≤ 𝑣 , 𝑧 , 𝑣 ) → ( ∃ 𝑏 ∈ ( ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ∖ { 𝐵 } ) ( abs ‘ ( 𝑏 − 𝐵 ) ) < 𝑢 ↔ ∃ 𝑏 ∈ ( ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ∖ { 𝐵 } ) ( abs ‘ ( 𝑏 − 𝐵 ) ) < if ( 𝑧 ≤ 𝑣 , 𝑧 , 𝑣 ) ) )
70		inss1	⊢ ( ( ( limPt ‘ 𝐾 ) ‘ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ) ∩ ℝ ) ⊆ ( ( limPt ‘ 𝐾 ) ‘ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) )
71	70	a1i	⊢ ( 𝜑 → ( ( ( limPt ‘ 𝐾 ) ‘ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ) ∩ ℝ ) ⊆ ( ( limPt ‘ 𝐾 ) ‘ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ) )
72	1	cnfldtop	⊢ 𝐾 ∈ Top
73	72	a1i	⊢ ( 𝜑 → 𝐾 ∈ Top )
74		ax-resscn	⊢ ℝ ⊆ ℂ
75	74	a1i	⊢ ( 𝜑 → ℝ ⊆ ℂ )
76		ioossre	⊢ ( 𝐵 (,) +∞ ) ⊆ ℝ
77	44 76	sstri	⊢ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ⊆ ℝ
78	77	a1i	⊢ ( 𝜑 → ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ⊆ ℝ )
79		unicntop	⊢ ℂ = ∪ ( TopOpen ‘ ℂ_fld )
80	1	unieqi	⊢ ∪ 𝐾 = ∪ ( TopOpen ‘ ℂ_fld )
81	79 80	eqtr4i	⊢ ℂ = ∪ 𝐾
82	1	tgioo2	⊢ ( topGen ‘ ran (,) ) = ( 𝐾 ↾_t ℝ )
83	3 82	eqtri	⊢ 𝐽 = ( 𝐾 ↾_t ℝ )
84	81 83	restlp	⊢ ( ( 𝐾 ∈ Top ∧ ℝ ⊆ ℂ ∧ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ⊆ ℝ ) → ( ( limPt ‘ 𝐽 ) ‘ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ) = ( ( ( limPt ‘ 𝐾 ) ‘ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ) ∩ ℝ ) )
85	73 75 78 84	syl3anc	⊢ ( 𝜑 → ( ( limPt ‘ 𝐽 ) ‘ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ) = ( ( ( limPt ‘ 𝐾 ) ‘ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ) ∩ ℝ ) )
86	1	eqcomi	⊢ ( TopOpen ‘ ℂ_fld ) = 𝐾
87	86	fveq2i	⊢ ( limPt ‘ ( TopOpen ‘ ℂ_fld ) ) = ( limPt ‘ 𝐾 )
88	87	fveq1i	⊢ ( ( limPt ‘ ( TopOpen ‘ ℂ_fld ) ) ‘ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ) = ( ( limPt ‘ 𝐾 ) ‘ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) )
89	88	a1i	⊢ ( 𝜑 → ( ( limPt ‘ ( TopOpen ‘ ℂ_fld ) ) ‘ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ) = ( ( limPt ‘ 𝐾 ) ‘ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ) )
90	71 85 89	3sstr4d	⊢ ( 𝜑 → ( ( limPt ‘ 𝐽 ) ‘ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ) ⊆ ( ( limPt ‘ ( TopOpen ‘ ℂ_fld ) ) ‘ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ) )
91	90 6	sseldd	⊢ ( 𝜑 → 𝐵 ∈ ( ( limPt ‘ ( TopOpen ‘ ℂ_fld ) ) ‘ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ) )
92	47 59	islpcn	⊢ ( 𝜑 → ( 𝐵 ∈ ( ( limPt ‘ ( TopOpen ‘ ℂ_fld ) ) ‘ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ) ↔ ∀ 𝑢 ∈ ℝ⁺ ∃ 𝑏 ∈ ( ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ∖ { 𝐵 } ) ( abs ‘ ( 𝑏 − 𝐵 ) ) < 𝑢 ) )
93	91 92	mpbid	⊢ ( 𝜑 → ∀ 𝑢 ∈ ℝ⁺ ∃ 𝑏 ∈ ( ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ∖ { 𝐵 } ) ( abs ‘ ( 𝑏 − 𝐵 ) ) < 𝑢 )
94	93	3ad2ant1	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℝ⁺ ∧ 𝑣 ∈ ℝ⁺ ) → ∀ 𝑢 ∈ ℝ⁺ ∃ 𝑏 ∈ ( ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ∖ { 𝐵 } ) ( abs ‘ ( 𝑏 − 𝐵 ) ) < 𝑢 )
95		ifcl	⊢ ( ( 𝑧 ∈ ℝ⁺ ∧ 𝑣 ∈ ℝ⁺ ) → if ( 𝑧 ≤ 𝑣 , 𝑧 , 𝑣 ) ∈ ℝ⁺ )
96	95	3adant1	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℝ⁺ ∧ 𝑣 ∈ ℝ⁺ ) → if ( 𝑧 ≤ 𝑣 , 𝑧 , 𝑣 ) ∈ ℝ⁺ )
97	69 94 96	rspcdva	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℝ⁺ ∧ 𝑣 ∈ ℝ⁺ ) → ∃ 𝑏 ∈ ( ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ∖ { 𝐵 } ) ( abs ‘ ( 𝑏 − 𝐵 ) ) < if ( 𝑧 ≤ 𝑣 , 𝑧 , 𝑣 ) )
98		eldifi	⊢ ( 𝑏 ∈ ( ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ∖ { 𝐵 } ) → 𝑏 ∈ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) )
99	77 98	sselid	⊢ ( 𝑏 ∈ ( ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ∖ { 𝐵 } ) → 𝑏 ∈ ℝ )
100	75	sselda	⊢ ( ( 𝜑 ∧ 𝑏 ∈ ℝ ) → 𝑏 ∈ ℂ )
101	59	adantr	⊢ ( ( 𝜑 ∧ 𝑏 ∈ ℝ ) → 𝐵 ∈ ℂ )
102	100 101	subcld	⊢ ( ( 𝜑 ∧ 𝑏 ∈ ℝ ) → ( 𝑏 − 𝐵 ) ∈ ℂ )
103	102	abscld	⊢ ( ( 𝜑 ∧ 𝑏 ∈ ℝ ) → ( abs ‘ ( 𝑏 − 𝐵 ) ) ∈ ℝ )
104	103	3ad2antl1	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℝ⁺ ∧ 𝑣 ∈ ℝ⁺ ) ∧ 𝑏 ∈ ℝ ) → ( abs ‘ ( 𝑏 − 𝐵 ) ) ∈ ℝ )
105	104	adantr	⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ℝ⁺ ∧ 𝑣 ∈ ℝ⁺ ) ∧ 𝑏 ∈ ℝ ) ∧ ( abs ‘ ( 𝑏 − 𝐵 ) ) < if ( 𝑧 ≤ 𝑣 , 𝑧 , 𝑣 ) ) → ( abs ‘ ( 𝑏 − 𝐵 ) ) ∈ ℝ )
106	96	rpred	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℝ⁺ ∧ 𝑣 ∈ ℝ⁺ ) → if ( 𝑧 ≤ 𝑣 , 𝑧 , 𝑣 ) ∈ ℝ )
107	106	ad2antrr	⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ℝ⁺ ∧ 𝑣 ∈ ℝ⁺ ) ∧ 𝑏 ∈ ℝ ) ∧ ( abs ‘ ( 𝑏 − 𝐵 ) ) < if ( 𝑧 ≤ 𝑣 , 𝑧 , 𝑣 ) ) → if ( 𝑧 ≤ 𝑣 , 𝑧 , 𝑣 ) ∈ ℝ )
108		rpre	⊢ ( 𝑧 ∈ ℝ⁺ → 𝑧 ∈ ℝ )
109	108	3ad2ant2	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℝ⁺ ∧ 𝑣 ∈ ℝ⁺ ) → 𝑧 ∈ ℝ )
110	109	ad2antrr	⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ℝ⁺ ∧ 𝑣 ∈ ℝ⁺ ) ∧ 𝑏 ∈ ℝ ) ∧ ( abs ‘ ( 𝑏 − 𝐵 ) ) < if ( 𝑧 ≤ 𝑣 , 𝑧 , 𝑣 ) ) → 𝑧 ∈ ℝ )
111		simpr	⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ℝ⁺ ∧ 𝑣 ∈ ℝ⁺ ) ∧ 𝑏 ∈ ℝ ) ∧ ( abs ‘ ( 𝑏 − 𝐵 ) ) < if ( 𝑧 ≤ 𝑣 , 𝑧 , 𝑣 ) ) → ( abs ‘ ( 𝑏 − 𝐵 ) ) < if ( 𝑧 ≤ 𝑣 , 𝑧 , 𝑣 ) )
112		rpre	⊢ ( 𝑣 ∈ ℝ⁺ → 𝑣 ∈ ℝ )
113		min1	⊢ ( ( 𝑧 ∈ ℝ ∧ 𝑣 ∈ ℝ ) → if ( 𝑧 ≤ 𝑣 , 𝑧 , 𝑣 ) ≤ 𝑧 )
114	108 112 113	syl2an	⊢ ( ( 𝑧 ∈ ℝ⁺ ∧ 𝑣 ∈ ℝ⁺ ) → if ( 𝑧 ≤ 𝑣 , 𝑧 , 𝑣 ) ≤ 𝑧 )
115	114	3adant1	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℝ⁺ ∧ 𝑣 ∈ ℝ⁺ ) → if ( 𝑧 ≤ 𝑣 , 𝑧 , 𝑣 ) ≤ 𝑧 )
116	115	ad2antrr	⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ℝ⁺ ∧ 𝑣 ∈ ℝ⁺ ) ∧ 𝑏 ∈ ℝ ) ∧ ( abs ‘ ( 𝑏 − 𝐵 ) ) < if ( 𝑧 ≤ 𝑣 , 𝑧 , 𝑣 ) ) → if ( 𝑧 ≤ 𝑣 , 𝑧 , 𝑣 ) ≤ 𝑧 )
117	105 107 110 111 116	ltletrd	⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ℝ⁺ ∧ 𝑣 ∈ ℝ⁺ ) ∧ 𝑏 ∈ ℝ ) ∧ ( abs ‘ ( 𝑏 − 𝐵 ) ) < if ( 𝑧 ≤ 𝑣 , 𝑧 , 𝑣 ) ) → ( abs ‘ ( 𝑏 − 𝐵 ) ) < 𝑧 )
118	112	3ad2ant3	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℝ⁺ ∧ 𝑣 ∈ ℝ⁺ ) → 𝑣 ∈ ℝ )
119	118	ad2antrr	⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ℝ⁺ ∧ 𝑣 ∈ ℝ⁺ ) ∧ 𝑏 ∈ ℝ ) ∧ ( abs ‘ ( 𝑏 − 𝐵 ) ) < if ( 𝑧 ≤ 𝑣 , 𝑧 , 𝑣 ) ) → 𝑣 ∈ ℝ )
120	110 119	min2d	⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ℝ⁺ ∧ 𝑣 ∈ ℝ⁺ ) ∧ 𝑏 ∈ ℝ ) ∧ ( abs ‘ ( 𝑏 − 𝐵 ) ) < if ( 𝑧 ≤ 𝑣 , 𝑧 , 𝑣 ) ) → if ( 𝑧 ≤ 𝑣 , 𝑧 , 𝑣 ) ≤ 𝑣 )
121	105 107 119 111 120	ltletrd	⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ℝ⁺ ∧ 𝑣 ∈ ℝ⁺ ) ∧ 𝑏 ∈ ℝ ) ∧ ( abs ‘ ( 𝑏 − 𝐵 ) ) < if ( 𝑧 ≤ 𝑣 , 𝑧 , 𝑣 ) ) → ( abs ‘ ( 𝑏 − 𝐵 ) ) < 𝑣 )
122	117 121	jca	⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ℝ⁺ ∧ 𝑣 ∈ ℝ⁺ ) ∧ 𝑏 ∈ ℝ ) ∧ ( abs ‘ ( 𝑏 − 𝐵 ) ) < if ( 𝑧 ≤ 𝑣 , 𝑧 , 𝑣 ) ) → ( ( abs ‘ ( 𝑏 − 𝐵 ) ) < 𝑧 ∧ ( abs ‘ ( 𝑏 − 𝐵 ) ) < 𝑣 ) )
123	122	ex	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℝ⁺ ∧ 𝑣 ∈ ℝ⁺ ) ∧ 𝑏 ∈ ℝ ) → ( ( abs ‘ ( 𝑏 − 𝐵 ) ) < if ( 𝑧 ≤ 𝑣 , 𝑧 , 𝑣 ) → ( ( abs ‘ ( 𝑏 − 𝐵 ) ) < 𝑧 ∧ ( abs ‘ ( 𝑏 − 𝐵 ) ) < 𝑣 ) ) )
124	99 123	sylan2	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℝ⁺ ∧ 𝑣 ∈ ℝ⁺ ) ∧ 𝑏 ∈ ( ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ∖ { 𝐵 } ) ) → ( ( abs ‘ ( 𝑏 − 𝐵 ) ) < if ( 𝑧 ≤ 𝑣 , 𝑧 , 𝑣 ) → ( ( abs ‘ ( 𝑏 − 𝐵 ) ) < 𝑧 ∧ ( abs ‘ ( 𝑏 − 𝐵 ) ) < 𝑣 ) ) )
125	124	reximdva	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℝ⁺ ∧ 𝑣 ∈ ℝ⁺ ) → ( ∃ 𝑏 ∈ ( ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ∖ { 𝐵 } ) ( abs ‘ ( 𝑏 − 𝐵 ) ) < if ( 𝑧 ≤ 𝑣 , 𝑧 , 𝑣 ) → ∃ 𝑏 ∈ ( ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ∖ { 𝐵 } ) ( ( abs ‘ ( 𝑏 − 𝐵 ) ) < 𝑧 ∧ ( abs ‘ ( 𝑏 − 𝐵 ) ) < 𝑣 ) ) )
126	97 125	mpd	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℝ⁺ ∧ 𝑣 ∈ ℝ⁺ ) → ∃ 𝑏 ∈ ( ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ∖ { 𝐵 } ) ( ( abs ‘ ( 𝑏 − 𝐵 ) ) < 𝑧 ∧ ( abs ‘ ( 𝑏 − 𝐵 ) ) < 𝑣 ) )
127	65 66 67 126	syl3anc	⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) ) ∧ 𝑣 ∈ ℝ⁺ ∧ ∀ 𝑤 ∈ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) ‘ 𝑤 ) − 𝑅 ) ) < 𝑦 ) ) → ∃ 𝑏 ∈ ( ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ∖ { 𝐵 } ) ( ( abs ‘ ( 𝑏 − 𝐵 ) ) < 𝑧 ∧ ( abs ‘ ( 𝑏 − 𝐵 ) ) < 𝑣 ) )
128		nfv	⊢ Ⅎ 𝑏 ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) ) ∧ 𝑣 ∈ ℝ⁺ ∧ ∀ 𝑤 ∈ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) ‘ 𝑤 ) − 𝑅 ) ) < 𝑦 ) )
129		nfre1	⊢ Ⅎ 𝑏 ∃ 𝑏 ∈ 𝐴 ( ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑅 ) ) < 𝑦 )
130	98	elin1d	⊢ ( 𝑏 ∈ ( ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ∖ { 𝐵 } ) → 𝑏 ∈ 𝐴 )
131	130	3ad2ant2	⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) ) ∧ 𝑣 ∈ ℝ⁺ ∧ ∀ 𝑤 ∈ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) ‘ 𝑤 ) − 𝑅 ) ) < 𝑦 ) ) ∧ 𝑏 ∈ ( ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ∖ { 𝐵 } ) ∧ ( ( abs ‘ ( 𝑏 − 𝐵 ) ) < 𝑧 ∧ ( abs ‘ ( 𝑏 − 𝐵 ) ) < 𝑣 ) ) → 𝑏 ∈ 𝐴 )
132		simp113	⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) ) ∧ 𝑣 ∈ ℝ⁺ ∧ ∀ 𝑤 ∈ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) ‘ 𝑤 ) − 𝑅 ) ) < 𝑦 ) ) ∧ 𝑏 ∈ ( ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ∖ { 𝐵 } ) ∧ ( ( abs ‘ ( 𝑏 − 𝐵 ) ) < 𝑧 ∧ ( abs ‘ ( 𝑏 − 𝐵 ) ) < 𝑣 ) ) → ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) )
133		eldifsni	⊢ ( 𝑏 ∈ ( ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ∖ { 𝐵 } ) → 𝑏 ≠ 𝐵 )
134	133	adantr	⊢ ( ( 𝑏 ∈ ( ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ∖ { 𝐵 } ) ∧ ( ( abs ‘ ( 𝑏 − 𝐵 ) ) < 𝑧 ∧ ( abs ‘ ( 𝑏 − 𝐵 ) ) < 𝑣 ) ) → 𝑏 ≠ 𝐵 )
135		simprl	⊢ ( ( 𝑏 ∈ ( ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ∖ { 𝐵 } ) ∧ ( ( abs ‘ ( 𝑏 − 𝐵 ) ) < 𝑧 ∧ ( abs ‘ ( 𝑏 − 𝐵 ) ) < 𝑣 ) ) → ( abs ‘ ( 𝑏 − 𝐵 ) ) < 𝑧 )
136	134 135	jca	⊢ ( ( 𝑏 ∈ ( ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ∖ { 𝐵 } ) ∧ ( ( abs ‘ ( 𝑏 − 𝐵 ) ) < 𝑧 ∧ ( abs ‘ ( 𝑏 − 𝐵 ) ) < 𝑣 ) ) → ( 𝑏 ≠ 𝐵 ∧ ( abs ‘ ( 𝑏 − 𝐵 ) ) < 𝑧 ) )
137	136	3adant1	⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) ) ∧ 𝑣 ∈ ℝ⁺ ∧ ∀ 𝑤 ∈ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) ‘ 𝑤 ) − 𝑅 ) ) < 𝑦 ) ) ∧ 𝑏 ∈ ( ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ∖ { 𝐵 } ) ∧ ( ( abs ‘ ( 𝑏 − 𝐵 ) ) < 𝑧 ∧ ( abs ‘ ( 𝑏 − 𝐵 ) ) < 𝑣 ) ) → ( 𝑏 ≠ 𝐵 ∧ ( abs ‘ ( 𝑏 − 𝐵 ) ) < 𝑧 ) )
138		neeq1	⊢ ( 𝑤 = 𝑏 → ( 𝑤 ≠ 𝐵 ↔ 𝑏 ≠ 𝐵 ) )
139		fvoveq1	⊢ ( 𝑤 = 𝑏 → ( abs ‘ ( 𝑤 − 𝐵 ) ) = ( abs ‘ ( 𝑏 − 𝐵 ) ) )
140	139	breq1d	⊢ ( 𝑤 = 𝑏 → ( ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ↔ ( abs ‘ ( 𝑏 − 𝐵 ) ) < 𝑧 ) )
141	138 140	anbi12d	⊢ ( 𝑤 = 𝑏 → ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) ↔ ( 𝑏 ≠ 𝐵 ∧ ( abs ‘ ( 𝑏 − 𝐵 ) ) < 𝑧 ) ) )
142	141	imbrov2fvoveq	⊢ ( 𝑤 = 𝑏 → ( ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) ↔ ( ( 𝑏 ≠ 𝐵 ∧ ( abs ‘ ( 𝑏 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑥 ) ) < 𝑦 ) ) )
143	142	rspcva	⊢ ( ( 𝑏 ∈ 𝐴 ∧ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) ) → ( ( 𝑏 ≠ 𝐵 ∧ ( abs ‘ ( 𝑏 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑥 ) ) < 𝑦 ) )
144	143	imp	⊢ ( ( ( 𝑏 ∈ 𝐴 ∧ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) ) ∧ ( 𝑏 ≠ 𝐵 ∧ ( abs ‘ ( 𝑏 − 𝐵 ) ) < 𝑧 ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑥 ) ) < 𝑦 )
145	131 132 137 144	syl21anc	⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) ) ∧ 𝑣 ∈ ℝ⁺ ∧ ∀ 𝑤 ∈ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) ‘ 𝑤 ) − 𝑅 ) ) < 𝑦 ) ) ∧ 𝑏 ∈ ( ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ∖ { 𝐵 } ) ∧ ( ( abs ‘ ( 𝑏 − 𝐵 ) ) < 𝑧 ∧ ( abs ‘ ( 𝑏 − 𝐵 ) ) < 𝑣 ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑥 ) ) < 𝑦 )
146	98	3ad2ant2	⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) ) ∧ 𝑣 ∈ ℝ⁺ ∧ ∀ 𝑤 ∈ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) ‘ 𝑤 ) − 𝑅 ) ) < 𝑦 ) ) ∧ 𝑏 ∈ ( ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ∖ { 𝐵 } ) ∧ ( ( abs ‘ ( 𝑏 − 𝐵 ) ) < 𝑧 ∧ ( abs ‘ ( 𝑏 − 𝐵 ) ) < 𝑣 ) ) → 𝑏 ∈ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) )
147	65	3ad2ant1	⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) ) ∧ 𝑣 ∈ ℝ⁺ ∧ ∀ 𝑤 ∈ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) ‘ 𝑤 ) − 𝑅 ) ) < 𝑦 ) ) ∧ 𝑏 ∈ ( ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ∖ { 𝐵 } ) ∧ ( ( abs ‘ ( 𝑏 − 𝐵 ) ) < 𝑧 ∧ ( abs ‘ ( 𝑏 − 𝐵 ) ) < 𝑣 ) ) → 𝜑 )
148		simp13	⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) ) ∧ 𝑣 ∈ ℝ⁺ ∧ ∀ 𝑤 ∈ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) ‘ 𝑤 ) − 𝑅 ) ) < 𝑦 ) ) ∧ 𝑏 ∈ ( ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ∖ { 𝐵 } ) ∧ ( ( abs ‘ ( 𝑏 − 𝐵 ) ) < 𝑧 ∧ ( abs ‘ ( 𝑏 − 𝐵 ) ) < 𝑣 ) ) → ∀ 𝑤 ∈ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) ‘ 𝑤 ) − 𝑅 ) ) < 𝑦 ) )
149		nfv	⊢ Ⅎ 𝑤 𝜑
150		nfra1	⊢ Ⅎ 𝑤 ∀ 𝑤 ∈ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) ‘ 𝑤 ) − 𝑅 ) ) < 𝑦 )
151	149 150	nfan	⊢ Ⅎ 𝑤 ( 𝜑 ∧ ∀ 𝑤 ∈ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) ‘ 𝑤 ) − 𝑅 ) ) < 𝑦 ) )
152		elinel2	⊢ ( 𝑤 ∈ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) → 𝑤 ∈ ( 𝐵 (,) +∞ ) )
153	152	fvresd	⊢ ( 𝑤 ∈ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) → ( ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) ‘ 𝑤 ) = ( 𝐹 ‘ 𝑤 ) )
154	153	eqcomd	⊢ ( 𝑤 ∈ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) → ( 𝐹 ‘ 𝑤 ) = ( ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) ‘ 𝑤 ) )
155	154	fvoveq1d	⊢ ( 𝑤 ∈ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑅 ) ) = ( abs ‘ ( ( ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) ‘ 𝑤 ) − 𝑅 ) ) )
156	155	3ad2ant2	⊢ ( ( ( 𝜑 ∧ ∀ 𝑤 ∈ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) ‘ 𝑤 ) − 𝑅 ) ) < 𝑦 ) ) ∧ 𝑤 ∈ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ∧ ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑅 ) ) = ( abs ‘ ( ( ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) ‘ 𝑤 ) − 𝑅 ) ) )
157		rspa	⊢ ( ( ∀ 𝑤 ∈ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) ‘ 𝑤 ) − 𝑅 ) ) < 𝑦 ) ∧ 𝑤 ∈ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ) → ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) ‘ 𝑤 ) − 𝑅 ) ) < 𝑦 ) )
158	157	3impia	⊢ ( ( ∀ 𝑤 ∈ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) ‘ 𝑤 ) − 𝑅 ) ) < 𝑦 ) ∧ 𝑤 ∈ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ∧ ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) ) → ( abs ‘ ( ( ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) ‘ 𝑤 ) − 𝑅 ) ) < 𝑦 )
159	158	3adant1l	⊢ ( ( ( 𝜑 ∧ ∀ 𝑤 ∈ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) ‘ 𝑤 ) − 𝑅 ) ) < 𝑦 ) ) ∧ 𝑤 ∈ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ∧ ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) ) → ( abs ‘ ( ( ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) ‘ 𝑤 ) − 𝑅 ) ) < 𝑦 )
160	156 159	eqbrtrd	⊢ ( ( ( 𝜑 ∧ ∀ 𝑤 ∈ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) ‘ 𝑤 ) − 𝑅 ) ) < 𝑦 ) ) ∧ 𝑤 ∈ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ∧ ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑅 ) ) < 𝑦 )
161	160	3exp	⊢ ( ( 𝜑 ∧ ∀ 𝑤 ∈ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) ‘ 𝑤 ) − 𝑅 ) ) < 𝑦 ) ) → ( 𝑤 ∈ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) → ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑅 ) ) < 𝑦 ) ) )
162	151 161	ralrimi	⊢ ( ( 𝜑 ∧ ∀ 𝑤 ∈ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) ‘ 𝑤 ) − 𝑅 ) ) < 𝑦 ) ) → ∀ 𝑤 ∈ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑅 ) ) < 𝑦 ) )
163	147 148 162	syl2anc	⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) ) ∧ 𝑣 ∈ ℝ⁺ ∧ ∀ 𝑤 ∈ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) ‘ 𝑤 ) − 𝑅 ) ) < 𝑦 ) ) ∧ 𝑏 ∈ ( ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ∖ { 𝐵 } ) ∧ ( ( abs ‘ ( 𝑏 − 𝐵 ) ) < 𝑧 ∧ ( abs ‘ ( 𝑏 − 𝐵 ) ) < 𝑣 ) ) → ∀ 𝑤 ∈ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑅 ) ) < 𝑦 ) )
164	133	anim1i	⊢ ( ( 𝑏 ∈ ( ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ∖ { 𝐵 } ) ∧ ( abs ‘ ( 𝑏 − 𝐵 ) ) < 𝑣 ) → ( 𝑏 ≠ 𝐵 ∧ ( abs ‘ ( 𝑏 − 𝐵 ) ) < 𝑣 ) )
165	164	adantrl	⊢ ( ( 𝑏 ∈ ( ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ∖ { 𝐵 } ) ∧ ( ( abs ‘ ( 𝑏 − 𝐵 ) ) < 𝑧 ∧ ( abs ‘ ( 𝑏 − 𝐵 ) ) < 𝑣 ) ) → ( 𝑏 ≠ 𝐵 ∧ ( abs ‘ ( 𝑏 − 𝐵 ) ) < 𝑣 ) )
166	165	3adant1	⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) ) ∧ 𝑣 ∈ ℝ⁺ ∧ ∀ 𝑤 ∈ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) ‘ 𝑤 ) − 𝑅 ) ) < 𝑦 ) ) ∧ 𝑏 ∈ ( ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ∖ { 𝐵 } ) ∧ ( ( abs ‘ ( 𝑏 − 𝐵 ) ) < 𝑧 ∧ ( abs ‘ ( 𝑏 − 𝐵 ) ) < 𝑣 ) ) → ( 𝑏 ≠ 𝐵 ∧ ( abs ‘ ( 𝑏 − 𝐵 ) ) < 𝑣 ) )
167	139	breq1d	⊢ ( 𝑤 = 𝑏 → ( ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ↔ ( abs ‘ ( 𝑏 − 𝐵 ) ) < 𝑣 ) )
168	138 167	anbi12d	⊢ ( 𝑤 = 𝑏 → ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) ↔ ( 𝑏 ≠ 𝐵 ∧ ( abs ‘ ( 𝑏 − 𝐵 ) ) < 𝑣 ) ) )
169	168	imbrov2fvoveq	⊢ ( 𝑤 = 𝑏 → ( ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑅 ) ) < 𝑦 ) ↔ ( ( 𝑏 ≠ 𝐵 ∧ ( abs ‘ ( 𝑏 − 𝐵 ) ) < 𝑣 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑅 ) ) < 𝑦 ) ) )
170	169	rspcva	⊢ ( ( 𝑏 ∈ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ∧ ∀ 𝑤 ∈ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑅 ) ) < 𝑦 ) ) → ( ( 𝑏 ≠ 𝐵 ∧ ( abs ‘ ( 𝑏 − 𝐵 ) ) < 𝑣 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑅 ) ) < 𝑦 ) )
171	170	imp	⊢ ( ( ( 𝑏 ∈ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ∧ ∀ 𝑤 ∈ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑅 ) ) < 𝑦 ) ) ∧ ( 𝑏 ≠ 𝐵 ∧ ( abs ‘ ( 𝑏 − 𝐵 ) ) < 𝑣 ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑅 ) ) < 𝑦 )
172	146 163 166 171	syl21anc	⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) ) ∧ 𝑣 ∈ ℝ⁺ ∧ ∀ 𝑤 ∈ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) ‘ 𝑤 ) − 𝑅 ) ) < 𝑦 ) ) ∧ 𝑏 ∈ ( ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ∖ { 𝐵 } ) ∧ ( ( abs ‘ ( 𝑏 − 𝐵 ) ) < 𝑧 ∧ ( abs ‘ ( 𝑏 − 𝐵 ) ) < 𝑣 ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑅 ) ) < 𝑦 )
173		rspe	⊢ ( ( 𝑏 ∈ 𝐴 ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑅 ) ) < 𝑦 ) ) → ∃ 𝑏 ∈ 𝐴 ( ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑅 ) ) < 𝑦 ) )
174	131 145 172 173	syl12anc	⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) ) ∧ 𝑣 ∈ ℝ⁺ ∧ ∀ 𝑤 ∈ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) ‘ 𝑤 ) − 𝑅 ) ) < 𝑦 ) ) ∧ 𝑏 ∈ ( ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ∖ { 𝐵 } ) ∧ ( ( abs ‘ ( 𝑏 − 𝐵 ) ) < 𝑧 ∧ ( abs ‘ ( 𝑏 − 𝐵 ) ) < 𝑣 ) ) → ∃ 𝑏 ∈ 𝐴 ( ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑅 ) ) < 𝑦 ) )
175	174	3exp	⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) ) ∧ 𝑣 ∈ ℝ⁺ ∧ ∀ 𝑤 ∈ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) ‘ 𝑤 ) − 𝑅 ) ) < 𝑦 ) ) → ( 𝑏 ∈ ( ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ∖ { 𝐵 } ) → ( ( ( abs ‘ ( 𝑏 − 𝐵 ) ) < 𝑧 ∧ ( abs ‘ ( 𝑏 − 𝐵 ) ) < 𝑣 ) → ∃ 𝑏 ∈ 𝐴 ( ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑅 ) ) < 𝑦 ) ) ) )
176	128 129 175	rexlimd	⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) ) ∧ 𝑣 ∈ ℝ⁺ ∧ ∀ 𝑤 ∈ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) ‘ 𝑤 ) − 𝑅 ) ) < 𝑦 ) ) → ( ∃ 𝑏 ∈ ( ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ∖ { 𝐵 } ) ( ( abs ‘ ( 𝑏 − 𝐵 ) ) < 𝑧 ∧ ( abs ‘ ( 𝑏 − 𝐵 ) ) < 𝑣 ) → ∃ 𝑏 ∈ 𝐴 ( ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑅 ) ) < 𝑦 ) ) )
177	127 176	mpd	⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) ) ∧ 𝑣 ∈ ℝ⁺ ∧ ∀ 𝑤 ∈ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) ‘ 𝑤 ) − 𝑅 ) ) < 𝑦 ) ) → ∃ 𝑏 ∈ 𝐴 ( ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑅 ) ) < 𝑦 ) )
178	177	3exp	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) ) → ( 𝑣 ∈ ℝ⁺ → ( ∀ 𝑤 ∈ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) ‘ 𝑤 ) − 𝑅 ) ) < 𝑦 ) → ∃ 𝑏 ∈ 𝐴 ( ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑅 ) ) < 𝑦 ) ) ) )
179	178	rexlimdv	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) ) → ( ∃ 𝑣 ∈ ℝ⁺ ∀ 𝑤 ∈ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) ‘ 𝑤 ) − 𝑅 ) ) < 𝑦 ) → ∃ 𝑏 ∈ 𝐴 ( ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑅 ) ) < 𝑦 ) ) )
180	64 179	mpd	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) ) → ∃ 𝑏 ∈ 𝐴 ( ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑅 ) ) < 𝑦 ) )
181	180	3exp	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) → ( 𝑧 ∈ ℝ⁺ → ( ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) → ∃ 𝑏 ∈ 𝐴 ( ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑅 ) ) < 𝑦 ) ) ) )
182	181	rexlimdv	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) → ( ∃ 𝑧 ∈ ℝ⁺ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) → ∃ 𝑏 ∈ 𝐴 ( ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑅 ) ) < 𝑦 ) ) )
183	182	imp	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) ∧ ∃ 𝑧 ∈ ℝ⁺ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) ) → ∃ 𝑏 ∈ 𝐴 ( ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑅 ) ) < 𝑦 ) )
184	183	adantllr	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑦 ∈ ℝ⁺ ) ∧ ∃ 𝑧 ∈ ℝ⁺ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) ) → ∃ 𝑏 ∈ 𝐴 ( ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑅 ) ) < 𝑦 ) )
185	184	ad2antrr	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑦 ∈ ℝ⁺ ) ∧ ∃ 𝑧 ∈ ℝ⁺ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) ) ∧ 𝑎 ∈ 𝐴 ) ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝐿 ) ) < 𝑦 ) ) → ∃ 𝑏 ∈ 𝐴 ( ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑅 ) ) < 𝑦 ) )
186	11	ad6antr	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑎 ∈ 𝐴 ) ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝐿 ) ) < 𝑦 ) ) ∧ 𝑏 ∈ 𝐴 ) ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑅 ) ) < 𝑦 ) ) → 𝑅 ∈ ℂ )
187	14	ad6antr	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑎 ∈ 𝐴 ) ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝐿 ) ) < 𝑦 ) ) ∧ 𝑏 ∈ 𝐴 ) ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑅 ) ) < 𝑦 ) ) → 𝐿 ∈ ℂ )
188	186 187	subcld	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑎 ∈ 𝐴 ) ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝐿 ) ) < 𝑦 ) ) ∧ 𝑏 ∈ 𝐴 ) ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑅 ) ) < 𝑦 ) ) → ( 𝑅 − 𝐿 ) ∈ ℂ )
189	188	abscld	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑎 ∈ 𝐴 ) ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝐿 ) ) < 𝑦 ) ) ∧ 𝑏 ∈ 𝐴 ) ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑅 ) ) < 𝑦 ) ) → ( abs ‘ ( 𝑅 − 𝐿 ) ) ∈ ℝ )
190		simp-6l	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑎 ∈ 𝐴 ) ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝐿 ) ) < 𝑦 ) ) ∧ 𝑏 ∈ 𝐴 ) ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑅 ) ) < 𝑦 ) ) → 𝜑 )
191		simplr	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑎 ∈ 𝐴 ) ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝐿 ) ) < 𝑦 ) ) ∧ 𝑏 ∈ 𝐴 ) ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑅 ) ) < 𝑦 ) ) → 𝑏 ∈ 𝐴 )
192	4	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑏 ) ∈ ℂ )
193	190 191 192	syl2anc	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑎 ∈ 𝐴 ) ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝐿 ) ) < 𝑦 ) ) ∧ 𝑏 ∈ 𝐴 ) ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑅 ) ) < 𝑦 ) ) → ( 𝐹 ‘ 𝑏 ) ∈ ℂ )
194	186 193	subcld	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑎 ∈ 𝐴 ) ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝐿 ) ) < 𝑦 ) ) ∧ 𝑏 ∈ 𝐴 ) ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑅 ) ) < 𝑦 ) ) → ( 𝑅 − ( 𝐹 ‘ 𝑏 ) ) ∈ ℂ )
195	194	abscld	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑎 ∈ 𝐴 ) ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝐿 ) ) < 𝑦 ) ) ∧ 𝑏 ∈ 𝐴 ) ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑅 ) ) < 𝑦 ) ) → ( abs ‘ ( 𝑅 − ( 𝐹 ‘ 𝑏 ) ) ) ∈ ℝ )
196		simp-6r	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑎 ∈ 𝐴 ) ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝐿 ) ) < 𝑦 ) ) ∧ 𝑏 ∈ 𝐴 ) ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑅 ) ) < 𝑦 ) ) → 𝑥 ∈ ℂ )
197	193 196	subcld	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑎 ∈ 𝐴 ) ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝐿 ) ) < 𝑦 ) ) ∧ 𝑏 ∈ 𝐴 ) ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑅 ) ) < 𝑦 ) ) → ( ( 𝐹 ‘ 𝑏 ) − 𝑥 ) ∈ ℂ )
198	197	abscld	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑎 ∈ 𝐴 ) ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝐿 ) ) < 𝑦 ) ) ∧ 𝑏 ∈ 𝐴 ) ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑅 ) ) < 𝑦 ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑥 ) ) ∈ ℝ )
199	195 198	readdcld	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑎 ∈ 𝐴 ) ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝐿 ) ) < 𝑦 ) ) ∧ 𝑏 ∈ 𝐴 ) ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑅 ) ) < 𝑦 ) ) → ( ( abs ‘ ( 𝑅 − ( 𝐹 ‘ 𝑏 ) ) ) + ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑥 ) ) ) ∈ ℝ )
200		simp-4r	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑎 ∈ 𝐴 ) ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝐿 ) ) < 𝑦 ) ) ∧ 𝑏 ∈ 𝐴 ) ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑅 ) ) < 𝑦 ) ) → 𝑎 ∈ 𝐴 )
201	4	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑎 ) ∈ ℂ )
202	190 200 201	syl2anc	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑎 ∈ 𝐴 ) ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝐿 ) ) < 𝑦 ) ) ∧ 𝑏 ∈ 𝐴 ) ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑅 ) ) < 𝑦 ) ) → ( 𝐹 ‘ 𝑎 ) ∈ ℂ )
203	196 202	subcld	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑎 ∈ 𝐴 ) ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝐿 ) ) < 𝑦 ) ) ∧ 𝑏 ∈ 𝐴 ) ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑅 ) ) < 𝑦 ) ) → ( 𝑥 − ( 𝐹 ‘ 𝑎 ) ) ∈ ℂ )
204	203	abscld	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑎 ∈ 𝐴 ) ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝐿 ) ) < 𝑦 ) ) ∧ 𝑏 ∈ 𝐴 ) ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑅 ) ) < 𝑦 ) ) → ( abs ‘ ( 𝑥 − ( 𝐹 ‘ 𝑎 ) ) ) ∈ ℝ )
205	199 204	readdcld	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑎 ∈ 𝐴 ) ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝐿 ) ) < 𝑦 ) ) ∧ 𝑏 ∈ 𝐴 ) ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑅 ) ) < 𝑦 ) ) → ( ( ( abs ‘ ( 𝑅 − ( 𝐹 ‘ 𝑏 ) ) ) + ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑥 ) ) ) + ( abs ‘ ( 𝑥 − ( 𝐹 ‘ 𝑎 ) ) ) ) ∈ ℝ )
206	202 187	subcld	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑎 ∈ 𝐴 ) ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝐿 ) ) < 𝑦 ) ) ∧ 𝑏 ∈ 𝐴 ) ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑅 ) ) < 𝑦 ) ) → ( ( 𝐹 ‘ 𝑎 ) − 𝐿 ) ∈ ℂ )
207	206	abscld	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑎 ∈ 𝐴 ) ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝐿 ) ) < 𝑦 ) ) ∧ 𝑏 ∈ 𝐴 ) ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑅 ) ) < 𝑦 ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝐿 ) ) ∈ ℝ )
208	205 207	readdcld	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑎 ∈ 𝐴 ) ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝐿 ) ) < 𝑦 ) ) ∧ 𝑏 ∈ 𝐴 ) ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑅 ) ) < 𝑦 ) ) → ( ( ( ( abs ‘ ( 𝑅 − ( 𝐹 ‘ 𝑏 ) ) ) + ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑥 ) ) ) + ( abs ‘ ( 𝑥 − ( 𝐹 ‘ 𝑎 ) ) ) ) + ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝐿 ) ) ) ∈ ℝ )
209	21	a1i	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑎 ∈ 𝐴 ) ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝐿 ) ) < 𝑦 ) ) ∧ 𝑏 ∈ 𝐴 ) ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑅 ) ) < 𝑦 ) ) → 4 ∈ ℝ )
210		rpre	⊢ ( 𝑦 ∈ ℝ⁺ → 𝑦 ∈ ℝ )
211	210	ad5antlr	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑎 ∈ 𝐴 ) ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝐿 ) ) < 𝑦 ) ) ∧ 𝑏 ∈ 𝐴 ) ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑅 ) ) < 𝑦 ) ) → 𝑦 ∈ ℝ )
212	209 211	remulcld	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑎 ∈ 𝐴 ) ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝐿 ) ) < 𝑦 ) ) ∧ 𝑏 ∈ 𝐴 ) ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑅 ) ) < 𝑦 ) ) → ( 4 · 𝑦 ) ∈ ℝ )
213	186 193 196 202 187	absnpncan3d	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑎 ∈ 𝐴 ) ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝐿 ) ) < 𝑦 ) ) ∧ 𝑏 ∈ 𝐴 ) ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑅 ) ) < 𝑦 ) ) → ( abs ‘ ( 𝑅 − 𝐿 ) ) ≤ ( ( ( ( abs ‘ ( 𝑅 − ( 𝐹 ‘ 𝑏 ) ) ) + ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑥 ) ) ) + ( abs ‘ ( 𝑥 − ( 𝐹 ‘ 𝑎 ) ) ) ) + ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝐿 ) ) ) )
214	186 193	abssubd	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑎 ∈ 𝐴 ) ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝐿 ) ) < 𝑦 ) ) ∧ 𝑏 ∈ 𝐴 ) ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑅 ) ) < 𝑦 ) ) → ( abs ‘ ( 𝑅 − ( 𝐹 ‘ 𝑏 ) ) ) = ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑅 ) ) )
215		simprr	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑎 ∈ 𝐴 ) ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝐿 ) ) < 𝑦 ) ) ∧ 𝑏 ∈ 𝐴 ) ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑅 ) ) < 𝑦 ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑅 ) ) < 𝑦 )
216	214 215	eqbrtrd	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑎 ∈ 𝐴 ) ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝐿 ) ) < 𝑦 ) ) ∧ 𝑏 ∈ 𝐴 ) ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑅 ) ) < 𝑦 ) ) → ( abs ‘ ( 𝑅 − ( 𝐹 ‘ 𝑏 ) ) ) < 𝑦 )
217		simprl	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑎 ∈ 𝐴 ) ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝐿 ) ) < 𝑦 ) ) ∧ 𝑏 ∈ 𝐴 ) ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑅 ) ) < 𝑦 ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑥 ) ) < 𝑦 )
218		simp-5r	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑎 ∈ 𝐴 ) ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝐿 ) ) < 𝑦 ) ) ∧ 𝑏 ∈ 𝐴 ) → 𝑥 ∈ ℂ )
219	201	ad5ant14	⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑎 ∈ 𝐴 ) ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝐿 ) ) < 𝑦 ) ) → ( 𝐹 ‘ 𝑎 ) ∈ ℂ )
220	219	adantr	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑎 ∈ 𝐴 ) ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝐿 ) ) < 𝑦 ) ) ∧ 𝑏 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑎 ) ∈ ℂ )
221	218 220	abssubd	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑎 ∈ 𝐴 ) ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝐿 ) ) < 𝑦 ) ) ∧ 𝑏 ∈ 𝐴 ) → ( abs ‘ ( 𝑥 − ( 𝐹 ‘ 𝑎 ) ) ) = ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝑥 ) ) )
222		simplrl	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑎 ∈ 𝐴 ) ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝐿 ) ) < 𝑦 ) ) ∧ 𝑏 ∈ 𝐴 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝑥 ) ) < 𝑦 )
223	221 222	eqbrtrd	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑎 ∈ 𝐴 ) ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝐿 ) ) < 𝑦 ) ) ∧ 𝑏 ∈ 𝐴 ) → ( abs ‘ ( 𝑥 − ( 𝐹 ‘ 𝑎 ) ) ) < 𝑦 )
224	223	adantr	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑎 ∈ 𝐴 ) ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝐿 ) ) < 𝑦 ) ) ∧ 𝑏 ∈ 𝐴 ) ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑅 ) ) < 𝑦 ) ) → ( abs ‘ ( 𝑥 − ( 𝐹 ‘ 𝑎 ) ) ) < 𝑦 )
225		simplrr	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑎 ∈ 𝐴 ) ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝐿 ) ) < 𝑦 ) ) ∧ 𝑏 ∈ 𝐴 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝐿 ) ) < 𝑦 )
226	225	adantr	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑎 ∈ 𝐴 ) ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝐿 ) ) < 𝑦 ) ) ∧ 𝑏 ∈ 𝐴 ) ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑅 ) ) < 𝑦 ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝐿 ) ) < 𝑦 )
227	195 198 204 207 211 216 217 224 226	lt4addmuld	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑎 ∈ 𝐴 ) ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝐿 ) ) < 𝑦 ) ) ∧ 𝑏 ∈ 𝐴 ) ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑅 ) ) < 𝑦 ) ) → ( ( ( ( abs ‘ ( 𝑅 − ( 𝐹 ‘ 𝑏 ) ) ) + ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑥 ) ) ) + ( abs ‘ ( 𝑥 − ( 𝐹 ‘ 𝑎 ) ) ) ) + ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝐿 ) ) ) < ( 4 · 𝑦 ) )
228	189 208 212 213 227	lelttrd	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑎 ∈ 𝐴 ) ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝐿 ) ) < 𝑦 ) ) ∧ 𝑏 ∈ 𝐴 ) ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑅 ) ) < 𝑦 ) ) → ( abs ‘ ( 𝑅 − 𝐿 ) ) < ( 4 · 𝑦 ) )
229	228	ex	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑎 ∈ 𝐴 ) ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝐿 ) ) < 𝑦 ) ) ∧ 𝑏 ∈ 𝐴 ) → ( ( ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑅 ) ) < 𝑦 ) → ( abs ‘ ( 𝑅 − 𝐿 ) ) < ( 4 · 𝑦 ) ) )
230	229	adantl3r	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑦 ∈ ℝ⁺ ) ∧ ∃ 𝑧 ∈ ℝ⁺ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) ) ∧ 𝑎 ∈ 𝐴 ) ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝐿 ) ) < 𝑦 ) ) ∧ 𝑏 ∈ 𝐴 ) → ( ( ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑅 ) ) < 𝑦 ) → ( abs ‘ ( 𝑅 − 𝐿 ) ) < ( 4 · 𝑦 ) ) )
231	230	reximdva	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑦 ∈ ℝ⁺ ) ∧ ∃ 𝑧 ∈ ℝ⁺ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) ) ∧ 𝑎 ∈ 𝐴 ) ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝐿 ) ) < 𝑦 ) ) → ( ∃ 𝑏 ∈ 𝐴 ( ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑏 ) − 𝑅 ) ) < 𝑦 ) → ∃ 𝑏 ∈ 𝐴 ( abs ‘ ( 𝑅 − 𝐿 ) ) < ( 4 · 𝑦 ) ) )
232	185 231	mpd	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑦 ∈ ℝ⁺ ) ∧ ∃ 𝑧 ∈ ℝ⁺ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) ) ∧ 𝑎 ∈ 𝐴 ) ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝐿 ) ) < 𝑦 ) ) → ∃ 𝑏 ∈ 𝐴 ( abs ‘ ( 𝑅 − 𝐿 ) ) < ( 4 · 𝑦 ) )
233		fresin	⊢ ( 𝐹 : 𝐴 ⟶ ℂ → ( 𝐹 ↾ ( -∞ (,) 𝐵 ) ) : ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ⟶ ℂ )
234	4 233	syl	⊢ ( 𝜑 → ( 𝐹 ↾ ( -∞ (,) 𝐵 ) ) : ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ⟶ ℂ )
235		ioosscn	⊢ ( -∞ (,) 𝐵 ) ⊆ ℂ
236	50 235	sstri	⊢ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ⊆ ℂ
237	236	a1i	⊢ ( 𝜑 → ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ⊆ ℂ )
238	234 237 59	ellimc3	⊢ ( 𝜑 → ( 𝐿 ∈ ( ( 𝐹 ↾ ( -∞ (,) 𝐵 ) ) lim_ℂ 𝐵 ) ↔ ( 𝐿 ∈ ℂ ∧ ∀ 𝑦 ∈ ℝ⁺ ∃ 𝑣 ∈ ℝ⁺ ∀ 𝑤 ∈ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( -∞ (,) 𝐵 ) ) ‘ 𝑤 ) − 𝐿 ) ) < 𝑦 ) ) ) )
239	7 238	mpbid	⊢ ( 𝜑 → ( 𝐿 ∈ ℂ ∧ ∀ 𝑦 ∈ ℝ⁺ ∃ 𝑣 ∈ ℝ⁺ ∀ 𝑤 ∈ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( -∞ (,) 𝐵 ) ) ‘ 𝑤 ) − 𝐿 ) ) < 𝑦 ) ) )
240	239	simprd	⊢ ( 𝜑 → ∀ 𝑦 ∈ ℝ⁺ ∃ 𝑣 ∈ ℝ⁺ ∀ 𝑤 ∈ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( -∞ (,) 𝐵 ) ) ‘ 𝑤 ) − 𝐿 ) ) < 𝑦 ) )
241	240	r19.21bi	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) → ∃ 𝑣 ∈ ℝ⁺ ∀ 𝑤 ∈ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( -∞ (,) 𝐵 ) ) ‘ 𝑤 ) − 𝐿 ) ) < 𝑦 ) )
242	241	3ad2ant1	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) ) → ∃ 𝑣 ∈ ℝ⁺ ∀ 𝑤 ∈ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( -∞ (,) 𝐵 ) ) ‘ 𝑤 ) − 𝐿 ) ) < 𝑦 ) )
243		simp11l	⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) ) ∧ 𝑣 ∈ ℝ⁺ ∧ ∀ 𝑤 ∈ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( -∞ (,) 𝐵 ) ) ‘ 𝑤 ) − 𝐿 ) ) < 𝑦 ) ) → 𝜑 )
244		simp12	⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) ) ∧ 𝑣 ∈ ℝ⁺ ∧ ∀ 𝑤 ∈ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( -∞ (,) 𝐵 ) ) ‘ 𝑤 ) − 𝐿 ) ) < 𝑦 ) ) → 𝑧 ∈ ℝ⁺ )
245		simp2	⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) ) ∧ 𝑣 ∈ ℝ⁺ ∧ ∀ 𝑤 ∈ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( -∞ (,) 𝐵 ) ) ‘ 𝑤 ) − 𝐿 ) ) < 𝑦 ) ) → 𝑣 ∈ ℝ⁺ )
246		breq2	⊢ ( 𝑢 = if ( 𝑧 ≤ 𝑣 , 𝑧 , 𝑣 ) → ( ( abs ‘ ( 𝑎 − 𝐵 ) ) < 𝑢 ↔ ( abs ‘ ( 𝑎 − 𝐵 ) ) < if ( 𝑧 ≤ 𝑣 , 𝑧 , 𝑣 ) ) )
247	246	rexbidv	⊢ ( 𝑢 = if ( 𝑧 ≤ 𝑣 , 𝑧 , 𝑣 ) → ( ∃ 𝑎 ∈ ( ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ∖ { 𝐵 } ) ( abs ‘ ( 𝑎 − 𝐵 ) ) < 𝑢 ↔ ∃ 𝑎 ∈ ( ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ∖ { 𝐵 } ) ( abs ‘ ( 𝑎 − 𝐵 ) ) < if ( 𝑧 ≤ 𝑣 , 𝑧 , 𝑣 ) ) )
248		inss1	⊢ ( ( ( limPt ‘ 𝐾 ) ‘ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ) ∩ ℝ ) ⊆ ( ( limPt ‘ 𝐾 ) ‘ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) )
249	248	a1i	⊢ ( 𝜑 → ( ( ( limPt ‘ 𝐾 ) ‘ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ) ∩ ℝ ) ⊆ ( ( limPt ‘ 𝐾 ) ‘ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ) )
250	52	a1i	⊢ ( 𝜑 → ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ⊆ ℝ )
251	81 83	restlp	⊢ ( ( 𝐾 ∈ Top ∧ ℝ ⊆ ℂ ∧ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ⊆ ℝ ) → ( ( limPt ‘ 𝐽 ) ‘ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ) = ( ( ( limPt ‘ 𝐾 ) ‘ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ) ∩ ℝ ) )
252	73 75 250 251	syl3anc	⊢ ( 𝜑 → ( ( limPt ‘ 𝐽 ) ‘ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ) = ( ( ( limPt ‘ 𝐾 ) ‘ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ) ∩ ℝ ) )
253	87	fveq1i	⊢ ( ( limPt ‘ ( TopOpen ‘ ℂ_fld ) ) ‘ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ) = ( ( limPt ‘ 𝐾 ) ‘ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) )
254	253	a1i	⊢ ( 𝜑 → ( ( limPt ‘ ( TopOpen ‘ ℂ_fld ) ) ‘ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ) = ( ( limPt ‘ 𝐾 ) ‘ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ) )
255	249 252 254	3sstr4d	⊢ ( 𝜑 → ( ( limPt ‘ 𝐽 ) ‘ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ) ⊆ ( ( limPt ‘ ( TopOpen ‘ ℂ_fld ) ) ‘ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ) )
256	255 5	sseldd	⊢ ( 𝜑 → 𝐵 ∈ ( ( limPt ‘ ( TopOpen ‘ ℂ_fld ) ) ‘ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ) )
257	237 59	islpcn	⊢ ( 𝜑 → ( 𝐵 ∈ ( ( limPt ‘ ( TopOpen ‘ ℂ_fld ) ) ‘ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ) ↔ ∀ 𝑢 ∈ ℝ⁺ ∃ 𝑎 ∈ ( ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ∖ { 𝐵 } ) ( abs ‘ ( 𝑎 − 𝐵 ) ) < 𝑢 ) )
258	256 257	mpbid	⊢ ( 𝜑 → ∀ 𝑢 ∈ ℝ⁺ ∃ 𝑎 ∈ ( ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ∖ { 𝐵 } ) ( abs ‘ ( 𝑎 − 𝐵 ) ) < 𝑢 )
259	258	3ad2ant1	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℝ⁺ ∧ 𝑣 ∈ ℝ⁺ ) → ∀ 𝑢 ∈ ℝ⁺ ∃ 𝑎 ∈ ( ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ∖ { 𝐵 } ) ( abs ‘ ( 𝑎 − 𝐵 ) ) < 𝑢 )
260	247 259 96	rspcdva	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℝ⁺ ∧ 𝑣 ∈ ℝ⁺ ) → ∃ 𝑎 ∈ ( ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ∖ { 𝐵 } ) ( abs ‘ ( 𝑎 − 𝐵 ) ) < if ( 𝑧 ≤ 𝑣 , 𝑧 , 𝑣 ) )
261		eldifi	⊢ ( 𝑎 ∈ ( ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ∖ { 𝐵 } ) → 𝑎 ∈ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) )
262	52 261	sselid	⊢ ( 𝑎 ∈ ( ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ∖ { 𝐵 } ) → 𝑎 ∈ ℝ )
263	75	sselda	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → 𝑎 ∈ ℂ )
264	59	adantr	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → 𝐵 ∈ ℂ )
265	263 264	subcld	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → ( 𝑎 − 𝐵 ) ∈ ℂ )
266	265	abscld	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → ( abs ‘ ( 𝑎 − 𝐵 ) ) ∈ ℝ )
267	266	3ad2antl1	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℝ⁺ ∧ 𝑣 ∈ ℝ⁺ ) ∧ 𝑎 ∈ ℝ ) → ( abs ‘ ( 𝑎 − 𝐵 ) ) ∈ ℝ )
268	267	adantr	⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ℝ⁺ ∧ 𝑣 ∈ ℝ⁺ ) ∧ 𝑎 ∈ ℝ ) ∧ ( abs ‘ ( 𝑎 − 𝐵 ) ) < if ( 𝑧 ≤ 𝑣 , 𝑧 , 𝑣 ) ) → ( abs ‘ ( 𝑎 − 𝐵 ) ) ∈ ℝ )
269	106	ad2antrr	⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ℝ⁺ ∧ 𝑣 ∈ ℝ⁺ ) ∧ 𝑎 ∈ ℝ ) ∧ ( abs ‘ ( 𝑎 − 𝐵 ) ) < if ( 𝑧 ≤ 𝑣 , 𝑧 , 𝑣 ) ) → if ( 𝑧 ≤ 𝑣 , 𝑧 , 𝑣 ) ∈ ℝ )
270	109	ad2antrr	⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ℝ⁺ ∧ 𝑣 ∈ ℝ⁺ ) ∧ 𝑎 ∈ ℝ ) ∧ ( abs ‘ ( 𝑎 − 𝐵 ) ) < if ( 𝑧 ≤ 𝑣 , 𝑧 , 𝑣 ) ) → 𝑧 ∈ ℝ )
271		simpr	⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ℝ⁺ ∧ 𝑣 ∈ ℝ⁺ ) ∧ 𝑎 ∈ ℝ ) ∧ ( abs ‘ ( 𝑎 − 𝐵 ) ) < if ( 𝑧 ≤ 𝑣 , 𝑧 , 𝑣 ) ) → ( abs ‘ ( 𝑎 − 𝐵 ) ) < if ( 𝑧 ≤ 𝑣 , 𝑧 , 𝑣 ) )
272	115	ad2antrr	⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ℝ⁺ ∧ 𝑣 ∈ ℝ⁺ ) ∧ 𝑎 ∈ ℝ ) ∧ ( abs ‘ ( 𝑎 − 𝐵 ) ) < if ( 𝑧 ≤ 𝑣 , 𝑧 , 𝑣 ) ) → if ( 𝑧 ≤ 𝑣 , 𝑧 , 𝑣 ) ≤ 𝑧 )
273	268 269 270 271 272	ltletrd	⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ℝ⁺ ∧ 𝑣 ∈ ℝ⁺ ) ∧ 𝑎 ∈ ℝ ) ∧ ( abs ‘ ( 𝑎 − 𝐵 ) ) < if ( 𝑧 ≤ 𝑣 , 𝑧 , 𝑣 ) ) → ( abs ‘ ( 𝑎 − 𝐵 ) ) < 𝑧 )
274	118	ad2antrr	⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ℝ⁺ ∧ 𝑣 ∈ ℝ⁺ ) ∧ 𝑎 ∈ ℝ ) ∧ ( abs ‘ ( 𝑎 − 𝐵 ) ) < if ( 𝑧 ≤ 𝑣 , 𝑧 , 𝑣 ) ) → 𝑣 ∈ ℝ )
275		min2	⊢ ( ( 𝑧 ∈ ℝ ∧ 𝑣 ∈ ℝ ) → if ( 𝑧 ≤ 𝑣 , 𝑧 , 𝑣 ) ≤ 𝑣 )
276	108 112 275	syl2an	⊢ ( ( 𝑧 ∈ ℝ⁺ ∧ 𝑣 ∈ ℝ⁺ ) → if ( 𝑧 ≤ 𝑣 , 𝑧 , 𝑣 ) ≤ 𝑣 )
277	276	3adant1	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℝ⁺ ∧ 𝑣 ∈ ℝ⁺ ) → if ( 𝑧 ≤ 𝑣 , 𝑧 , 𝑣 ) ≤ 𝑣 )
278	277	ad2antrr	⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ℝ⁺ ∧ 𝑣 ∈ ℝ⁺ ) ∧ 𝑎 ∈ ℝ ) ∧ ( abs ‘ ( 𝑎 − 𝐵 ) ) < if ( 𝑧 ≤ 𝑣 , 𝑧 , 𝑣 ) ) → if ( 𝑧 ≤ 𝑣 , 𝑧 , 𝑣 ) ≤ 𝑣 )
279	268 269 274 271 278	ltletrd	⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ℝ⁺ ∧ 𝑣 ∈ ℝ⁺ ) ∧ 𝑎 ∈ ℝ ) ∧ ( abs ‘ ( 𝑎 − 𝐵 ) ) < if ( 𝑧 ≤ 𝑣 , 𝑧 , 𝑣 ) ) → ( abs ‘ ( 𝑎 − 𝐵 ) ) < 𝑣 )
280	273 279	jca	⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ℝ⁺ ∧ 𝑣 ∈ ℝ⁺ ) ∧ 𝑎 ∈ ℝ ) ∧ ( abs ‘ ( 𝑎 − 𝐵 ) ) < if ( 𝑧 ≤ 𝑣 , 𝑧 , 𝑣 ) ) → ( ( abs ‘ ( 𝑎 − 𝐵 ) ) < 𝑧 ∧ ( abs ‘ ( 𝑎 − 𝐵 ) ) < 𝑣 ) )
281	280	ex	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℝ⁺ ∧ 𝑣 ∈ ℝ⁺ ) ∧ 𝑎 ∈ ℝ ) → ( ( abs ‘ ( 𝑎 − 𝐵 ) ) < if ( 𝑧 ≤ 𝑣 , 𝑧 , 𝑣 ) → ( ( abs ‘ ( 𝑎 − 𝐵 ) ) < 𝑧 ∧ ( abs ‘ ( 𝑎 − 𝐵 ) ) < 𝑣 ) ) )
282	262 281	sylan2	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℝ⁺ ∧ 𝑣 ∈ ℝ⁺ ) ∧ 𝑎 ∈ ( ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ∖ { 𝐵 } ) ) → ( ( abs ‘ ( 𝑎 − 𝐵 ) ) < if ( 𝑧 ≤ 𝑣 , 𝑧 , 𝑣 ) → ( ( abs ‘ ( 𝑎 − 𝐵 ) ) < 𝑧 ∧ ( abs ‘ ( 𝑎 − 𝐵 ) ) < 𝑣 ) ) )
283	282	reximdva	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℝ⁺ ∧ 𝑣 ∈ ℝ⁺ ) → ( ∃ 𝑎 ∈ ( ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ∖ { 𝐵 } ) ( abs ‘ ( 𝑎 − 𝐵 ) ) < if ( 𝑧 ≤ 𝑣 , 𝑧 , 𝑣 ) → ∃ 𝑎 ∈ ( ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ∖ { 𝐵 } ) ( ( abs ‘ ( 𝑎 − 𝐵 ) ) < 𝑧 ∧ ( abs ‘ ( 𝑎 − 𝐵 ) ) < 𝑣 ) ) )
284	260 283	mpd	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℝ⁺ ∧ 𝑣 ∈ ℝ⁺ ) → ∃ 𝑎 ∈ ( ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ∖ { 𝐵 } ) ( ( abs ‘ ( 𝑎 − 𝐵 ) ) < 𝑧 ∧ ( abs ‘ ( 𝑎 − 𝐵 ) ) < 𝑣 ) )
285	243 244 245 284	syl3anc	⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) ) ∧ 𝑣 ∈ ℝ⁺ ∧ ∀ 𝑤 ∈ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( -∞ (,) 𝐵 ) ) ‘ 𝑤 ) − 𝐿 ) ) < 𝑦 ) ) → ∃ 𝑎 ∈ ( ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ∖ { 𝐵 } ) ( ( abs ‘ ( 𝑎 − 𝐵 ) ) < 𝑧 ∧ ( abs ‘ ( 𝑎 − 𝐵 ) ) < 𝑣 ) )
286		nfv	⊢ Ⅎ 𝑎 ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) ) ∧ 𝑣 ∈ ℝ⁺ ∧ ∀ 𝑤 ∈ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( -∞ (,) 𝐵 ) ) ‘ 𝑤 ) − 𝐿 ) ) < 𝑦 ) )
287		nfre1	⊢ Ⅎ 𝑎 ∃ 𝑎 ∈ 𝐴 ( ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝐿 ) ) < 𝑦 )
288	261	elin1d	⊢ ( 𝑎 ∈ ( ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ∖ { 𝐵 } ) → 𝑎 ∈ 𝐴 )
289	288	3ad2ant2	⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) ) ∧ 𝑣 ∈ ℝ⁺ ∧ ∀ 𝑤 ∈ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( -∞ (,) 𝐵 ) ) ‘ 𝑤 ) − 𝐿 ) ) < 𝑦 ) ) ∧ 𝑎 ∈ ( ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ∖ { 𝐵 } ) ∧ ( ( abs ‘ ( 𝑎 − 𝐵 ) ) < 𝑧 ∧ ( abs ‘ ( 𝑎 − 𝐵 ) ) < 𝑣 ) ) → 𝑎 ∈ 𝐴 )
290		simp113	⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) ) ∧ 𝑣 ∈ ℝ⁺ ∧ ∀ 𝑤 ∈ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( -∞ (,) 𝐵 ) ) ‘ 𝑤 ) − 𝐿 ) ) < 𝑦 ) ) ∧ 𝑎 ∈ ( ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ∖ { 𝐵 } ) ∧ ( ( abs ‘ ( 𝑎 − 𝐵 ) ) < 𝑧 ∧ ( abs ‘ ( 𝑎 − 𝐵 ) ) < 𝑣 ) ) → ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) )
291		eldifsni	⊢ ( 𝑎 ∈ ( ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ∖ { 𝐵 } ) → 𝑎 ≠ 𝐵 )
292	291	adantr	⊢ ( ( 𝑎 ∈ ( ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ∖ { 𝐵 } ) ∧ ( ( abs ‘ ( 𝑎 − 𝐵 ) ) < 𝑧 ∧ ( abs ‘ ( 𝑎 − 𝐵 ) ) < 𝑣 ) ) → 𝑎 ≠ 𝐵 )
293		simprl	⊢ ( ( 𝑎 ∈ ( ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ∖ { 𝐵 } ) ∧ ( ( abs ‘ ( 𝑎 − 𝐵 ) ) < 𝑧 ∧ ( abs ‘ ( 𝑎 − 𝐵 ) ) < 𝑣 ) ) → ( abs ‘ ( 𝑎 − 𝐵 ) ) < 𝑧 )
294	292 293	jca	⊢ ( ( 𝑎 ∈ ( ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ∖ { 𝐵 } ) ∧ ( ( abs ‘ ( 𝑎 − 𝐵 ) ) < 𝑧 ∧ ( abs ‘ ( 𝑎 − 𝐵 ) ) < 𝑣 ) ) → ( 𝑎 ≠ 𝐵 ∧ ( abs ‘ ( 𝑎 − 𝐵 ) ) < 𝑧 ) )
295	294	3adant1	⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) ) ∧ 𝑣 ∈ ℝ⁺ ∧ ∀ 𝑤 ∈ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( -∞ (,) 𝐵 ) ) ‘ 𝑤 ) − 𝐿 ) ) < 𝑦 ) ) ∧ 𝑎 ∈ ( ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ∖ { 𝐵 } ) ∧ ( ( abs ‘ ( 𝑎 − 𝐵 ) ) < 𝑧 ∧ ( abs ‘ ( 𝑎 − 𝐵 ) ) < 𝑣 ) ) → ( 𝑎 ≠ 𝐵 ∧ ( abs ‘ ( 𝑎 − 𝐵 ) ) < 𝑧 ) )
296		neeq1	⊢ ( 𝑤 = 𝑎 → ( 𝑤 ≠ 𝐵 ↔ 𝑎 ≠ 𝐵 ) )
297		fvoveq1	⊢ ( 𝑤 = 𝑎 → ( abs ‘ ( 𝑤 − 𝐵 ) ) = ( abs ‘ ( 𝑎 − 𝐵 ) ) )
298	297	breq1d	⊢ ( 𝑤 = 𝑎 → ( ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ↔ ( abs ‘ ( 𝑎 − 𝐵 ) ) < 𝑧 ) )
299	296 298	anbi12d	⊢ ( 𝑤 = 𝑎 → ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) ↔ ( 𝑎 ≠ 𝐵 ∧ ( abs ‘ ( 𝑎 − 𝐵 ) ) < 𝑧 ) ) )
300	299	imbrov2fvoveq	⊢ ( 𝑤 = 𝑎 → ( ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) ↔ ( ( 𝑎 ≠ 𝐵 ∧ ( abs ‘ ( 𝑎 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝑥 ) ) < 𝑦 ) ) )
301	300	rspcva	⊢ ( ( 𝑎 ∈ 𝐴 ∧ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) ) → ( ( 𝑎 ≠ 𝐵 ∧ ( abs ‘ ( 𝑎 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝑥 ) ) < 𝑦 ) )
302	301	imp	⊢ ( ( ( 𝑎 ∈ 𝐴 ∧ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) ) ∧ ( 𝑎 ≠ 𝐵 ∧ ( abs ‘ ( 𝑎 − 𝐵 ) ) < 𝑧 ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝑥 ) ) < 𝑦 )
303	289 290 295 302	syl21anc	⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) ) ∧ 𝑣 ∈ ℝ⁺ ∧ ∀ 𝑤 ∈ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( -∞ (,) 𝐵 ) ) ‘ 𝑤 ) − 𝐿 ) ) < 𝑦 ) ) ∧ 𝑎 ∈ ( ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ∖ { 𝐵 } ) ∧ ( ( abs ‘ ( 𝑎 − 𝐵 ) ) < 𝑧 ∧ ( abs ‘ ( 𝑎 − 𝐵 ) ) < 𝑣 ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝑥 ) ) < 𝑦 )
304	261	3ad2ant2	⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) ) ∧ 𝑣 ∈ ℝ⁺ ∧ ∀ 𝑤 ∈ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( -∞ (,) 𝐵 ) ) ‘ 𝑤 ) − 𝐿 ) ) < 𝑦 ) ) ∧ 𝑎 ∈ ( ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ∖ { 𝐵 } ) ∧ ( ( abs ‘ ( 𝑎 − 𝐵 ) ) < 𝑧 ∧ ( abs ‘ ( 𝑎 − 𝐵 ) ) < 𝑣 ) ) → 𝑎 ∈ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) )
305	243	3ad2ant1	⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) ) ∧ 𝑣 ∈ ℝ⁺ ∧ ∀ 𝑤 ∈ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( -∞ (,) 𝐵 ) ) ‘ 𝑤 ) − 𝐿 ) ) < 𝑦 ) ) ∧ 𝑎 ∈ ( ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ∖ { 𝐵 } ) ∧ ( ( abs ‘ ( 𝑎 − 𝐵 ) ) < 𝑧 ∧ ( abs ‘ ( 𝑎 − 𝐵 ) ) < 𝑣 ) ) → 𝜑 )
306		simp13	⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) ) ∧ 𝑣 ∈ ℝ⁺ ∧ ∀ 𝑤 ∈ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( -∞ (,) 𝐵 ) ) ‘ 𝑤 ) − 𝐿 ) ) < 𝑦 ) ) ∧ 𝑎 ∈ ( ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ∖ { 𝐵 } ) ∧ ( ( abs ‘ ( 𝑎 − 𝐵 ) ) < 𝑧 ∧ ( abs ‘ ( 𝑎 − 𝐵 ) ) < 𝑣 ) ) → ∀ 𝑤 ∈ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( -∞ (,) 𝐵 ) ) ‘ 𝑤 ) − 𝐿 ) ) < 𝑦 ) )
307		nfra1	⊢ Ⅎ 𝑤 ∀ 𝑤 ∈ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( -∞ (,) 𝐵 ) ) ‘ 𝑤 ) − 𝐿 ) ) < 𝑦 )
308	149 307	nfan	⊢ Ⅎ 𝑤 ( 𝜑 ∧ ∀ 𝑤 ∈ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( -∞ (,) 𝐵 ) ) ‘ 𝑤 ) − 𝐿 ) ) < 𝑦 ) )
309		elinel2	⊢ ( 𝑤 ∈ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) → 𝑤 ∈ ( -∞ (,) 𝐵 ) )
310	309	fvresd	⊢ ( 𝑤 ∈ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) → ( ( 𝐹 ↾ ( -∞ (,) 𝐵 ) ) ‘ 𝑤 ) = ( 𝐹 ‘ 𝑤 ) )
311	310	eqcomd	⊢ ( 𝑤 ∈ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) → ( 𝐹 ‘ 𝑤 ) = ( ( 𝐹 ↾ ( -∞ (,) 𝐵 ) ) ‘ 𝑤 ) )
312	311	fvoveq1d	⊢ ( 𝑤 ∈ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝐿 ) ) = ( abs ‘ ( ( ( 𝐹 ↾ ( -∞ (,) 𝐵 ) ) ‘ 𝑤 ) − 𝐿 ) ) )
313	312	3ad2ant2	⊢ ( ( ( 𝜑 ∧ ∀ 𝑤 ∈ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( -∞ (,) 𝐵 ) ) ‘ 𝑤 ) − 𝐿 ) ) < 𝑦 ) ) ∧ 𝑤 ∈ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ∧ ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝐿 ) ) = ( abs ‘ ( ( ( 𝐹 ↾ ( -∞ (,) 𝐵 ) ) ‘ 𝑤 ) − 𝐿 ) ) )
314		rspa	⊢ ( ( ∀ 𝑤 ∈ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( -∞ (,) 𝐵 ) ) ‘ 𝑤 ) − 𝐿 ) ) < 𝑦 ) ∧ 𝑤 ∈ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ) → ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( -∞ (,) 𝐵 ) ) ‘ 𝑤 ) − 𝐿 ) ) < 𝑦 ) )
315	314	3impia	⊢ ( ( ∀ 𝑤 ∈ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( -∞ (,) 𝐵 ) ) ‘ 𝑤 ) − 𝐿 ) ) < 𝑦 ) ∧ 𝑤 ∈ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ∧ ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) ) → ( abs ‘ ( ( ( 𝐹 ↾ ( -∞ (,) 𝐵 ) ) ‘ 𝑤 ) − 𝐿 ) ) < 𝑦 )
316	315	3adant1l	⊢ ( ( ( 𝜑 ∧ ∀ 𝑤 ∈ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( -∞ (,) 𝐵 ) ) ‘ 𝑤 ) − 𝐿 ) ) < 𝑦 ) ) ∧ 𝑤 ∈ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ∧ ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) ) → ( abs ‘ ( ( ( 𝐹 ↾ ( -∞ (,) 𝐵 ) ) ‘ 𝑤 ) − 𝐿 ) ) < 𝑦 )
317	313 316	eqbrtrd	⊢ ( ( ( 𝜑 ∧ ∀ 𝑤 ∈ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( -∞ (,) 𝐵 ) ) ‘ 𝑤 ) − 𝐿 ) ) < 𝑦 ) ) ∧ 𝑤 ∈ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ∧ ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝐿 ) ) < 𝑦 )
318	317	3exp	⊢ ( ( 𝜑 ∧ ∀ 𝑤 ∈ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( -∞ (,) 𝐵 ) ) ‘ 𝑤 ) − 𝐿 ) ) < 𝑦 ) ) → ( 𝑤 ∈ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) → ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝐿 ) ) < 𝑦 ) ) )
319	308 318	ralrimi	⊢ ( ( 𝜑 ∧ ∀ 𝑤 ∈ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( -∞ (,) 𝐵 ) ) ‘ 𝑤 ) − 𝐿 ) ) < 𝑦 ) ) → ∀ 𝑤 ∈ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝐿 ) ) < 𝑦 ) )
320	305 306 319	syl2anc	⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) ) ∧ 𝑣 ∈ ℝ⁺ ∧ ∀ 𝑤 ∈ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( -∞ (,) 𝐵 ) ) ‘ 𝑤 ) − 𝐿 ) ) < 𝑦 ) ) ∧ 𝑎 ∈ ( ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ∖ { 𝐵 } ) ∧ ( ( abs ‘ ( 𝑎 − 𝐵 ) ) < 𝑧 ∧ ( abs ‘ ( 𝑎 − 𝐵 ) ) < 𝑣 ) ) → ∀ 𝑤 ∈ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝐿 ) ) < 𝑦 ) )
321	291	anim1i	⊢ ( ( 𝑎 ∈ ( ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ∖ { 𝐵 } ) ∧ ( abs ‘ ( 𝑎 − 𝐵 ) ) < 𝑣 ) → ( 𝑎 ≠ 𝐵 ∧ ( abs ‘ ( 𝑎 − 𝐵 ) ) < 𝑣 ) )
322	321	adantrl	⊢ ( ( 𝑎 ∈ ( ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ∖ { 𝐵 } ) ∧ ( ( abs ‘ ( 𝑎 − 𝐵 ) ) < 𝑧 ∧ ( abs ‘ ( 𝑎 − 𝐵 ) ) < 𝑣 ) ) → ( 𝑎 ≠ 𝐵 ∧ ( abs ‘ ( 𝑎 − 𝐵 ) ) < 𝑣 ) )
323	322	3adant1	⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) ) ∧ 𝑣 ∈ ℝ⁺ ∧ ∀ 𝑤 ∈ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( -∞ (,) 𝐵 ) ) ‘ 𝑤 ) − 𝐿 ) ) < 𝑦 ) ) ∧ 𝑎 ∈ ( ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ∖ { 𝐵 } ) ∧ ( ( abs ‘ ( 𝑎 − 𝐵 ) ) < 𝑧 ∧ ( abs ‘ ( 𝑎 − 𝐵 ) ) < 𝑣 ) ) → ( 𝑎 ≠ 𝐵 ∧ ( abs ‘ ( 𝑎 − 𝐵 ) ) < 𝑣 ) )
324	297	breq1d	⊢ ( 𝑤 = 𝑎 → ( ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ↔ ( abs ‘ ( 𝑎 − 𝐵 ) ) < 𝑣 ) )
325	296 324	anbi12d	⊢ ( 𝑤 = 𝑎 → ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) ↔ ( 𝑎 ≠ 𝐵 ∧ ( abs ‘ ( 𝑎 − 𝐵 ) ) < 𝑣 ) ) )
326	325	imbrov2fvoveq	⊢ ( 𝑤 = 𝑎 → ( ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝐿 ) ) < 𝑦 ) ↔ ( ( 𝑎 ≠ 𝐵 ∧ ( abs ‘ ( 𝑎 − 𝐵 ) ) < 𝑣 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝐿 ) ) < 𝑦 ) ) )
327	326	rspcva	⊢ ( ( 𝑎 ∈ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ∧ ∀ 𝑤 ∈ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝐿 ) ) < 𝑦 ) ) → ( ( 𝑎 ≠ 𝐵 ∧ ( abs ‘ ( 𝑎 − 𝐵 ) ) < 𝑣 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝐿 ) ) < 𝑦 ) )
328	327	imp	⊢ ( ( ( 𝑎 ∈ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ∧ ∀ 𝑤 ∈ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝐿 ) ) < 𝑦 ) ) ∧ ( 𝑎 ≠ 𝐵 ∧ ( abs ‘ ( 𝑎 − 𝐵 ) ) < 𝑣 ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝐿 ) ) < 𝑦 )
329	304 320 323 328	syl21anc	⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) ) ∧ 𝑣 ∈ ℝ⁺ ∧ ∀ 𝑤 ∈ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( -∞ (,) 𝐵 ) ) ‘ 𝑤 ) − 𝐿 ) ) < 𝑦 ) ) ∧ 𝑎 ∈ ( ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ∖ { 𝐵 } ) ∧ ( ( abs ‘ ( 𝑎 − 𝐵 ) ) < 𝑧 ∧ ( abs ‘ ( 𝑎 − 𝐵 ) ) < 𝑣 ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝐿 ) ) < 𝑦 )
330		rspe	⊢ ( ( 𝑎 ∈ 𝐴 ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝐿 ) ) < 𝑦 ) ) → ∃ 𝑎 ∈ 𝐴 ( ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝐿 ) ) < 𝑦 ) )
331	289 303 329 330	syl12anc	⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) ) ∧ 𝑣 ∈ ℝ⁺ ∧ ∀ 𝑤 ∈ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( -∞ (,) 𝐵 ) ) ‘ 𝑤 ) − 𝐿 ) ) < 𝑦 ) ) ∧ 𝑎 ∈ ( ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ∖ { 𝐵 } ) ∧ ( ( abs ‘ ( 𝑎 − 𝐵 ) ) < 𝑧 ∧ ( abs ‘ ( 𝑎 − 𝐵 ) ) < 𝑣 ) ) → ∃ 𝑎 ∈ 𝐴 ( ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝐿 ) ) < 𝑦 ) )
332	331	3exp	⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) ) ∧ 𝑣 ∈ ℝ⁺ ∧ ∀ 𝑤 ∈ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( -∞ (,) 𝐵 ) ) ‘ 𝑤 ) − 𝐿 ) ) < 𝑦 ) ) → ( 𝑎 ∈ ( ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ∖ { 𝐵 } ) → ( ( ( abs ‘ ( 𝑎 − 𝐵 ) ) < 𝑧 ∧ ( abs ‘ ( 𝑎 − 𝐵 ) ) < 𝑣 ) → ∃ 𝑎 ∈ 𝐴 ( ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝐿 ) ) < 𝑦 ) ) ) )
333	286 287 332	rexlimd	⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) ) ∧ 𝑣 ∈ ℝ⁺ ∧ ∀ 𝑤 ∈ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( -∞ (,) 𝐵 ) ) ‘ 𝑤 ) − 𝐿 ) ) < 𝑦 ) ) → ( ∃ 𝑎 ∈ ( ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ∖ { 𝐵 } ) ( ( abs ‘ ( 𝑎 − 𝐵 ) ) < 𝑧 ∧ ( abs ‘ ( 𝑎 − 𝐵 ) ) < 𝑣 ) → ∃ 𝑎 ∈ 𝐴 ( ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝐿 ) ) < 𝑦 ) ) )
334	285 333	mpd	⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) ) ∧ 𝑣 ∈ ℝ⁺ ∧ ∀ 𝑤 ∈ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( -∞ (,) 𝐵 ) ) ‘ 𝑤 ) − 𝐿 ) ) < 𝑦 ) ) → ∃ 𝑎 ∈ 𝐴 ( ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝐿 ) ) < 𝑦 ) )
335	334	3exp	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) ) → ( 𝑣 ∈ ℝ⁺ → ( ∀ 𝑤 ∈ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( -∞ (,) 𝐵 ) ) ‘ 𝑤 ) − 𝐿 ) ) < 𝑦 ) → ∃ 𝑎 ∈ 𝐴 ( ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝐿 ) ) < 𝑦 ) ) ) )
336	335	rexlimdv	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) ) → ( ∃ 𝑣 ∈ ℝ⁺ ∀ 𝑤 ∈ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑣 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( -∞ (,) 𝐵 ) ) ‘ 𝑤 ) − 𝐿 ) ) < 𝑦 ) → ∃ 𝑎 ∈ 𝐴 ( ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝐿 ) ) < 𝑦 ) ) )
337	242 336	mpd	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) ) → ∃ 𝑎 ∈ 𝐴 ( ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝐿 ) ) < 𝑦 ) )
338	337	3exp	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) → ( 𝑧 ∈ ℝ⁺ → ( ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) → ∃ 𝑎 ∈ 𝐴 ( ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝐿 ) ) < 𝑦 ) ) ) )
339	338	rexlimdv	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) → ( ∃ 𝑧 ∈ ℝ⁺ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) → ∃ 𝑎 ∈ 𝐴 ( ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝐿 ) ) < 𝑦 ) ) )
340	339	imp	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) ∧ ∃ 𝑧 ∈ ℝ⁺ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) ) → ∃ 𝑎 ∈ 𝐴 ( ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝐿 ) ) < 𝑦 ) )
341	340	adantllr	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑦 ∈ ℝ⁺ ) ∧ ∃ 𝑧 ∈ ℝ⁺ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) ) → ∃ 𝑎 ∈ 𝐴 ( ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝑥 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑎 ) − 𝐿 ) ) < 𝑦 ) )
342	232 341	reximddv3	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑦 ∈ ℝ⁺ ) ∧ ∃ 𝑧 ∈ ℝ⁺ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) ) → ∃ 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ 𝐴 ( abs ‘ ( 𝑅 − 𝐿 ) ) < ( 4 · 𝑦 ) )
343	38 39 41 342	syl21anc	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ ∀ 𝑦 ∈ ℝ⁺ ∃ 𝑧 ∈ ℝ⁺ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) ) ∧ 𝑦 ∈ ℝ⁺ ) → ∃ 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ 𝐴 ( abs ‘ ( 𝑅 − 𝐿 ) ) < ( 4 · 𝑦 ) )
344	343	ex	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ ∀ 𝑦 ∈ ℝ⁺ ∃ 𝑧 ∈ ℝ⁺ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) ) → ( 𝑦 ∈ ℝ⁺ → ∃ 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ 𝐴 ( abs ‘ ( 𝑅 − 𝐿 ) ) < ( 4 · 𝑦 ) ) )
345	30 31 37 344	vtoclf	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ ∀ 𝑦 ∈ ℝ⁺ ∃ 𝑧 ∈ ℝ⁺ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) ) → ( ( ( abs ‘ ( 𝑅 − 𝐿 ) ) / 4 ) ∈ ℝ⁺ → ∃ 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ 𝐴 ( abs ‘ ( 𝑅 − 𝐿 ) ) < ( 4 · ( ( abs ‘ ( 𝑅 − 𝐿 ) ) / 4 ) ) ) )
346	25 345	mpd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ ∀ 𝑦 ∈ ℝ⁺ ∃ 𝑧 ∈ ℝ⁺ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) ) → ∃ 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ 𝐴 ( abs ‘ ( 𝑅 − 𝐿 ) ) < ( 4 · ( ( abs ‘ ( 𝑅 − 𝐿 ) ) / 4 ) ) )
347		simpr	⊢ ( ( 𝜑 ∧ ( abs ‘ ( 𝑅 − 𝐿 ) ) < ( 4 · ( ( abs ‘ ( 𝑅 − 𝐿 ) ) / 4 ) ) ) → ( abs ‘ ( 𝑅 − 𝐿 ) ) < ( 4 · ( ( abs ‘ ( 𝑅 − 𝐿 ) ) / 4 ) ) )
348		abssubrp	⊢ ( ( 𝑅 ∈ ℂ ∧ 𝐿 ∈ ℂ ∧ 𝑅 ≠ 𝐿 ) → ( abs ‘ ( 𝑅 − 𝐿 ) ) ∈ ℝ⁺ )
349	11 14 17 348	syl3anc	⊢ ( 𝜑 → ( abs ‘ ( 𝑅 − 𝐿 ) ) ∈ ℝ⁺ )
350	349	rpcnd	⊢ ( 𝜑 → ( abs ‘ ( 𝑅 − 𝐿 ) ) ∈ ℂ )
351	350	adantr	⊢ ( ( 𝜑 ∧ ( abs ‘ ( 𝑅 − 𝐿 ) ) < ( 4 · ( ( abs ‘ ( 𝑅 − 𝐿 ) ) / 4 ) ) ) → ( abs ‘ ( 𝑅 − 𝐿 ) ) ∈ ℂ )
352		4cn	⊢ 4 ∈ ℂ
353	352	a1i	⊢ ( ( 𝜑 ∧ ( abs ‘ ( 𝑅 − 𝐿 ) ) < ( 4 · ( ( abs ‘ ( 𝑅 − 𝐿 ) ) / 4 ) ) ) → 4 ∈ ℂ )
354		4ne0	⊢ 4 ≠ 0
355	354	a1i	⊢ ( ( 𝜑 ∧ ( abs ‘ ( 𝑅 − 𝐿 ) ) < ( 4 · ( ( abs ‘ ( 𝑅 − 𝐿 ) ) / 4 ) ) ) → 4 ≠ 0 )
356	351 353 355	divcan2d	⊢ ( ( 𝜑 ∧ ( abs ‘ ( 𝑅 − 𝐿 ) ) < ( 4 · ( ( abs ‘ ( 𝑅 − 𝐿 ) ) / 4 ) ) ) → ( 4 · ( ( abs ‘ ( 𝑅 − 𝐿 ) ) / 4 ) ) = ( abs ‘ ( 𝑅 − 𝐿 ) ) )
357	347 356	breqtrd	⊢ ( ( 𝜑 ∧ ( abs ‘ ( 𝑅 − 𝐿 ) ) < ( 4 · ( ( abs ‘ ( 𝑅 − 𝐿 ) ) / 4 ) ) ) → ( abs ‘ ( 𝑅 − 𝐿 ) ) < ( abs ‘ ( 𝑅 − 𝐿 ) ) )
358	357	ex	⊢ ( 𝜑 → ( ( abs ‘ ( 𝑅 − 𝐿 ) ) < ( 4 · ( ( abs ‘ ( 𝑅 − 𝐿 ) ) / 4 ) ) → ( abs ‘ ( 𝑅 − 𝐿 ) ) < ( abs ‘ ( 𝑅 − 𝐿 ) ) ) )
359	358	a1d	⊢ ( 𝜑 → ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ) → ( ( abs ‘ ( 𝑅 − 𝐿 ) ) < ( 4 · ( ( abs ‘ ( 𝑅 − 𝐿 ) ) / 4 ) ) → ( abs ‘ ( 𝑅 − 𝐿 ) ) < ( abs ‘ ( 𝑅 − 𝐿 ) ) ) ) )
360	359	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ ∀ 𝑦 ∈ ℝ⁺ ∃ 𝑧 ∈ ℝ⁺ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) ) → ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ) → ( ( abs ‘ ( 𝑅 − 𝐿 ) ) < ( 4 · ( ( abs ‘ ( 𝑅 − 𝐿 ) ) / 4 ) ) → ( abs ‘ ( 𝑅 − 𝐿 ) ) < ( abs ‘ ( 𝑅 − 𝐿 ) ) ) ) )
361	360	rexlimdvv	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ ∀ 𝑦 ∈ ℝ⁺ ∃ 𝑧 ∈ ℝ⁺ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) ) → ( ∃ 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ 𝐴 ( abs ‘ ( 𝑅 − 𝐿 ) ) < ( 4 · ( ( abs ‘ ( 𝑅 − 𝐿 ) ) / 4 ) ) → ( abs ‘ ( 𝑅 − 𝐿 ) ) < ( abs ‘ ( 𝑅 − 𝐿 ) ) ) )
362	346 361	mpd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ ∀ 𝑦 ∈ ℝ⁺ ∃ 𝑧 ∈ ℝ⁺ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) ) → ( abs ‘ ( 𝑅 − 𝐿 ) ) < ( abs ‘ ( 𝑅 − 𝐿 ) ) )
363	16	abscld	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ ∀ 𝑦 ∈ ℝ⁺ ∃ 𝑧 ∈ ℝ⁺ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) ) → ( abs ‘ ( 𝑅 − 𝐿 ) ) ∈ ℝ )
364	363	ltnrd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ ∀ 𝑦 ∈ ℝ⁺ ∃ 𝑧 ∈ ℝ⁺ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) ) → ¬ ( abs ‘ ( 𝑅 − 𝐿 ) ) < ( abs ‘ ( 𝑅 − 𝐿 ) ) )
365	362 364	pm2.65da	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → ¬ ∀ 𝑦 ∈ ℝ⁺ ∃ 𝑧 ∈ ℝ⁺ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) )
366	365	ex	⊢ ( 𝜑 → ( 𝑥 ∈ ℂ → ¬ ∀ 𝑦 ∈ ℝ⁺ ∃ 𝑧 ∈ ℝ⁺ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) ) )
367		imnan	⊢ ( ( 𝑥 ∈ ℂ → ¬ ∀ 𝑦 ∈ ℝ⁺ ∃ 𝑧 ∈ ℝ⁺ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) ) ↔ ¬ ( 𝑥 ∈ ℂ ∧ ∀ 𝑦 ∈ ℝ⁺ ∃ 𝑧 ∈ ℝ⁺ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) ) )
368	366 367	sylib	⊢ ( 𝜑 → ¬ ( 𝑥 ∈ ℂ ∧ ∀ 𝑦 ∈ ℝ⁺ ∃ 𝑧 ∈ ℝ⁺ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) ) )
369	2 75	sstrd	⊢ ( 𝜑 → 𝐴 ⊆ ℂ )
370	4 369 59	ellimc3	⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐹 lim_ℂ 𝐵 ) ↔ ( 𝑥 ∈ ℂ ∧ ∀ 𝑦 ∈ ℝ⁺ ∃ 𝑧 ∈ ℝ⁺ ∀ 𝑤 ∈ 𝐴 ( ( 𝑤 ≠ 𝐵 ∧ ( abs ‘ ( 𝑤 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝑥 ) ) < 𝑦 ) ) ) )
371	368 370	mtbird	⊢ ( 𝜑 → ¬ 𝑥 ∈ ( 𝐹 lim_ℂ 𝐵 ) )
372	371	eq0rdv	⊢ ( 𝜑 → ( 𝐹 lim_ℂ 𝐵 ) = ∅ )

Metamath Proof Explorer

Theorem limclner

Proof