Metamath Proof Explorer

Theorem limcrecl

Description: If F is a real-valued function, B is a limit point of its domain, and the limit of F at B exists, then this limit is real. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses limcrecl.1 ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℝ )
limcrecl.2 ⊢ ( 𝜑 → 𝐴 ⊆ ℂ )
limcrecl.3 ⊢ ( 𝜑 → 𝐵 ∈ ( ( limPt ‘ ( TopOpen ‘ ℂfld ) ) ‘ 𝐴 ) )
limcrecl.4 ⊢ ( 𝜑 → 𝐿 ∈ ( 𝐹 limℂ 𝐵 ) )
Assertion limcrecl ( 𝜑 → 𝐿 ∈ ℝ )

Proof

Step Hyp Ref Expression
1 limcrecl.1 ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℝ )
2 limcrecl.2 ⊢ ( 𝜑 → 𝐴 ⊆ ℂ )
3 limcrecl.3 ⊢ ( 𝜑 → 𝐵 ∈ ( ( limPt ‘ ( TopOpen ‘ ℂfld ) ) ‘ 𝐴 ) )
4 limcrecl.4 ⊢ ( 𝜑 → 𝐿 ∈ ( 𝐹 limℂ 𝐵 ) )
5 4 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝐿 ∈ ℝ ) → 𝐿 ∈ ( 𝐹 limℂ 𝐵 ) )
6 limccl ⊢ ( 𝐹 limℂ 𝐵 ) ⊆ ℂ
7 6 4 sselid ⊢ ( 𝜑 → 𝐿 ∈ ℂ )
8 7 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝐿 ∈ ℝ ) → 𝐿 ∈ ℂ )
9 simpr ⊢ ( ( 𝜑 ∧ ¬ 𝐿 ∈ ℝ ) → ¬ 𝐿 ∈ ℝ )
10 8 9 eldifd ⊢ ( ( 𝜑 ∧ ¬ 𝐿 ∈ ℝ ) → 𝐿 ∈ ( ℂ ∖ ℝ ) )
11 10 dstregt0 ⊢ ( ( 𝜑 ∧ ¬ 𝐿 ∈ ℝ ) → ∃ 𝑥 ∈ ℝ+ ∀ 𝑤 ∈ ℝ 𝑥 < ( abs ‘ ( 𝐿 − 𝑤 ) ) )
12 cnxmet ⊢ ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ )
13 12 a1i ⊢ ( ( ( ( ( 𝜑 ∧ ¬ 𝐿 ∈ ℝ ) ∧ 𝑥 ∈ ℝ+ ) ∧ ∀ 𝑤 ∈ ℝ 𝑥 < ( abs ‘ ( 𝐿 − 𝑤 ) ) ) ∧ 𝑦 ∈ ℝ+ ) → ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ ) )
14 2 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ ¬ 𝐿 ∈ ℝ ) ∧ 𝑥 ∈ ℝ+ ) ∧ ∀ 𝑤 ∈ ℝ 𝑥 < ( abs ‘ ( 𝐿 − 𝑤 ) ) ) ∧ 𝑦 ∈ ℝ+ ) → 𝐴 ⊆ ℂ )
15 14 ssdifssd ⊢ ( ( ( ( ( 𝜑 ∧ ¬ 𝐿 ∈ ℝ ) ∧ 𝑥 ∈ ℝ+ ) ∧ ∀ 𝑤 ∈ ℝ 𝑥 < ( abs ‘ ( 𝐿 − 𝑤 ) ) ) ∧ 𝑦 ∈ ℝ+ ) → ( 𝐴 ∖ { 𝐵 } ) ⊆ ℂ )
16 eqid ⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
17 16 cnfldtop ⊢ ( TopOpen ‘ ℂfld ) ∈ Top
18 17 a1i ⊢ ( 𝜑 → ( TopOpen ‘ ℂfld ) ∈ Top )
19 unicntop ⊢ ℂ = ∪ ( TopOpen ‘ ℂfld )
20 2 19 sseqtrdi ⊢ ( 𝜑 → 𝐴 ⊆ ∪ ( TopOpen ‘ ℂfld ) )
21 eqid ⊢ ∪ ( TopOpen ‘ ℂfld ) = ∪ ( TopOpen ‘ ℂfld )
22 21 lpdifsn ⊢ ( ( ( TopOpen ‘ ℂfld ) ∈ Top ∧ 𝐴 ⊆ ∪ ( TopOpen ‘ ℂfld ) ) → ( 𝐵 ∈ ( ( limPt ‘ ( TopOpen ‘ ℂfld ) ) ‘ 𝐴 ) ↔ 𝐵 ∈ ( ( limPt ‘ ( TopOpen ‘ ℂfld ) ) ‘ ( 𝐴 ∖ { 𝐵 } ) ) ) )
23 18 20 22 syl2anc ⊢ ( 𝜑 → ( 𝐵 ∈ ( ( limPt ‘ ( TopOpen ‘ ℂfld ) ) ‘ 𝐴 ) ↔ 𝐵 ∈ ( ( limPt ‘ ( TopOpen ‘ ℂfld ) ) ‘ ( 𝐴 ∖ { 𝐵 } ) ) ) )
24 3 23 mpbid ⊢ ( 𝜑 → 𝐵 ∈ ( ( limPt ‘ ( TopOpen ‘ ℂfld ) ) ‘ ( 𝐴 ∖ { 𝐵 } ) ) )
25 24 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ ¬ 𝐿 ∈ ℝ ) ∧ 𝑥 ∈ ℝ+ ) ∧ ∀ 𝑤 ∈ ℝ 𝑥 < ( abs ‘ ( 𝐿 − 𝑤 ) ) ) ∧ 𝑦 ∈ ℝ+ ) → 𝐵 ∈ ( ( limPt ‘ ( TopOpen ‘ ℂfld ) ) ‘ ( 𝐴 ∖ { 𝐵 } ) ) )
26 simpr ⊢ ( ( ( ( ( 𝜑 ∧ ¬ 𝐿 ∈ ℝ ) ∧ 𝑥 ∈ ℝ+ ) ∧ ∀ 𝑤 ∈ ℝ 𝑥 < ( abs ‘ ( 𝐿 − 𝑤 ) ) ) ∧ 𝑦 ∈ ℝ+ ) → 𝑦 ∈ ℝ+ )
27 16 cnfldtopn ⊢ ( TopOpen ‘ ℂfld ) = ( MetOpen ‘ ( abs ∘ − ) )
28 27 lpbl ⊢ ( ( ( ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ ) ∧ ( 𝐴 ∖ { 𝐵 } ) ⊆ ℂ ∧ 𝐵 ∈ ( ( limPt ‘ ( TopOpen ‘ ℂfld ) ) ‘ ( 𝐴 ∖ { 𝐵 } ) ) ) ∧ 𝑦 ∈ ℝ+ ) → ∃ 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) 𝑧 ∈ ( 𝐵 ( ball ‘ ( abs ∘ − ) ) 𝑦 ) )
29 13 15 25 26 28 syl31anc ⊢ ( ( ( ( ( 𝜑 ∧ ¬ 𝐿 ∈ ℝ ) ∧ 𝑥 ∈ ℝ+ ) ∧ ∀ 𝑤 ∈ ℝ 𝑥 < ( abs ‘ ( 𝐿 − 𝑤 ) ) ) ∧ 𝑦 ∈ ℝ+ ) → ∃ 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) 𝑧 ∈ ( 𝐵 ( ball ‘ ( abs ∘ − ) ) 𝑦 ) )
30 eldif ⊢ ( 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ↔ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ∈ { 𝐵 } ) )
31 30 anbi1i ⊢ ( ( 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ∧ 𝑧 ∈ ( 𝐵 ( ball ‘ ( abs ∘ − ) ) 𝑦 ) ) ↔ ( ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ∈ { 𝐵 } ) ∧ 𝑧 ∈ ( 𝐵 ( ball ‘ ( abs ∘ − ) ) 𝑦 ) ) )
32 anass ⊢ ( ( ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ∈ { 𝐵 } ) ∧ 𝑧 ∈ ( 𝐵 ( ball ‘ ( abs ∘ − ) ) 𝑦 ) ) ↔ ( 𝑧 ∈ 𝐴 ∧ ( ¬ 𝑧 ∈ { 𝐵 } ∧ 𝑧 ∈ ( 𝐵 ( ball ‘ ( abs ∘ − ) ) 𝑦 ) ) ) )
33 31 32 bitri ⊢ ( ( 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ∧ 𝑧 ∈ ( 𝐵 ( ball ‘ ( abs ∘ − ) ) 𝑦 ) ) ↔ ( 𝑧 ∈ 𝐴 ∧ ( ¬ 𝑧 ∈ { 𝐵 } ∧ 𝑧 ∈ ( 𝐵 ( ball ‘ ( abs ∘ − ) ) 𝑦 ) ) ) )
34 33 rexbii2 ⊢ ( ∃ 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) 𝑧 ∈ ( 𝐵 ( ball ‘ ( abs ∘ − ) ) 𝑦 ) ↔ ∃ 𝑧 ∈ 𝐴 ( ¬ 𝑧 ∈ { 𝐵 } ∧ 𝑧 ∈ ( 𝐵 ( ball ‘ ( abs ∘ − ) ) 𝑦 ) ) )
35 29 34 sylib ⊢ ( ( ( ( ( 𝜑 ∧ ¬ 𝐿 ∈ ℝ ) ∧ 𝑥 ∈ ℝ+ ) ∧ ∀ 𝑤 ∈ ℝ 𝑥 < ( abs ‘ ( 𝐿 − 𝑤 ) ) ) ∧ 𝑦 ∈ ℝ+ ) → ∃ 𝑧 ∈ 𝐴 ( ¬ 𝑧 ∈ { 𝐵 } ∧ 𝑧 ∈ ( 𝐵 ( ball ‘ ( abs ∘ − ) ) 𝑦 ) ) )
36 simprl ⊢ ( ( ( ( ( ( 𝜑 ∧ ¬ 𝐿 ∈ ℝ ) ∧ 𝑥 ∈ ℝ+ ) ∧ ∀ 𝑤 ∈ ℝ 𝑥 < ( abs ‘ ( 𝐿 − 𝑤 ) ) ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( ¬ 𝑧 ∈ { 𝐵 } ∧ 𝑧 ∈ ( 𝐵 ( ball ‘ ( abs ∘ − ) ) 𝑦 ) ) ) → ¬ 𝑧 ∈ { 𝐵 } )
37 velsn ⊢ ( 𝑧 ∈ { 𝐵 } ↔ 𝑧 = 𝐵 )
38 37 necon3bbii ⊢ ( ¬ 𝑧 ∈ { 𝐵 } ↔ 𝑧 ≠ 𝐵 )
39 36 38 sylib ⊢ ( ( ( ( ( ( 𝜑 ∧ ¬ 𝐿 ∈ ℝ ) ∧ 𝑥 ∈ ℝ+ ) ∧ ∀ 𝑤 ∈ ℝ 𝑥 < ( abs ‘ ( 𝐿 − 𝑤 ) ) ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( ¬ 𝑧 ∈ { 𝐵 } ∧ 𝑧 ∈ ( 𝐵 ( ball ‘ ( abs ∘ − ) ) 𝑦 ) ) ) → 𝑧 ≠ 𝐵 )
40 simp-5l ⊢ ( ( ( ( ( ( 𝜑 ∧ ¬ 𝐿 ∈ ℝ ) ∧ 𝑥 ∈ ℝ+ ) ∧ ∀ 𝑤 ∈ ℝ 𝑥 < ( abs ‘ ( 𝐿 − 𝑤 ) ) ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( ¬ 𝑧 ∈ { 𝐵 } ∧ 𝑧 ∈ ( 𝐵 ( ball ‘ ( abs ∘ − ) ) 𝑦 ) ) ) → 𝜑 )
41 simplr ⊢ ( ( ( ( ( ( 𝜑 ∧ ¬ 𝐿 ∈ ℝ ) ∧ 𝑥 ∈ ℝ+ ) ∧ ∀ 𝑤 ∈ ℝ 𝑥 < ( abs ‘ ( 𝐿 − 𝑤 ) ) ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( ¬ 𝑧 ∈ { 𝐵 } ∧ 𝑧 ∈ ( 𝐵 ( ball ‘ ( abs ∘ − ) ) 𝑦 ) ) ) → 𝑦 ∈ ℝ+ )
42 simprr ⊢ ( ( ( ( ( ( 𝜑 ∧ ¬ 𝐿 ∈ ℝ ) ∧ 𝑥 ∈ ℝ+ ) ∧ ∀ 𝑤 ∈ ℝ 𝑥 < ( abs ‘ ( 𝐿 − 𝑤 ) ) ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( ¬ 𝑧 ∈ { 𝐵 } ∧ 𝑧 ∈ ( 𝐵 ( ball ‘ ( abs ∘ − ) ) 𝑦 ) ) ) → 𝑧 ∈ ( 𝐵 ( ball ‘ ( abs ∘ − ) ) 𝑦 ) )
43 simp3 ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ∧ 𝑧 ∈ ( 𝐵 ( ball ‘ ( abs ∘ − ) ) 𝑦 ) ) → 𝑧 ∈ ( 𝐵 ( ball ‘ ( abs ∘ − ) ) 𝑦 ) )
44 12 a1i ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ∧ 𝑧 ∈ ( 𝐵 ( ball ‘ ( abs ∘ − ) ) 𝑦 ) ) → ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ ) )
45 19 lpss ⊢ ( ( ( TopOpen ‘ ℂfld ) ∈ Top ∧ 𝐴 ⊆ ℂ ) → ( ( limPt ‘ ( TopOpen ‘ ℂfld ) ) ‘ 𝐴 ) ⊆ ℂ )
46 18 2 45 syl2anc ⊢ ( 𝜑 → ( ( limPt ‘ ( TopOpen ‘ ℂfld ) ) ‘ 𝐴 ) ⊆ ℂ )
47 46 3 sseldd ⊢ ( 𝜑 → 𝐵 ∈ ℂ )
48 47 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ∧ 𝑧 ∈ ( 𝐵 ( ball ‘ ( abs ∘ − ) ) 𝑦 ) ) → 𝐵 ∈ ℂ )
49 rpxr ⊢ ( 𝑦 ∈ ℝ+ → 𝑦 ∈ ℝ* )
50 49 3ad2ant2 ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ∧ 𝑧 ∈ ( 𝐵 ( ball ‘ ( abs ∘ − ) ) 𝑦 ) ) → 𝑦 ∈ ℝ* )
51 elbl ⊢ ( ( ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ ) ∧ 𝐵 ∈ ℂ ∧ 𝑦 ∈ ℝ* ) → ( 𝑧 ∈ ( 𝐵 ( ball ‘ ( abs ∘ − ) ) 𝑦 ) ↔ ( 𝑧 ∈ ℂ ∧ ( 𝐵 ( abs ∘ − ) 𝑧 ) < 𝑦 ) ) )
52 44 48 50 51 syl3anc ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ∧ 𝑧 ∈ ( 𝐵 ( ball ‘ ( abs ∘ − ) ) 𝑦 ) ) → ( 𝑧 ∈ ( 𝐵 ( ball ‘ ( abs ∘ − ) ) 𝑦 ) ↔ ( 𝑧 ∈ ℂ ∧ ( 𝐵 ( abs ∘ − ) 𝑧 ) < 𝑦 ) ) )
53 43 52 mpbid ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ∧ 𝑧 ∈ ( 𝐵 ( ball ‘ ( abs ∘ − ) ) 𝑦 ) ) → ( 𝑧 ∈ ℂ ∧ ( 𝐵 ( abs ∘ − ) 𝑧 ) < 𝑦 ) )
54 53 simpld ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ∧ 𝑧 ∈ ( 𝐵 ( ball ‘ ( abs ∘ − ) ) 𝑦 ) ) → 𝑧 ∈ ℂ )
55 54 48 abssubd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ∧ 𝑧 ∈ ( 𝐵 ( ball ‘ ( abs ∘ − ) ) 𝑦 ) ) → ( abs ‘ ( 𝑧 − 𝐵 ) ) = ( abs ‘ ( 𝐵 − 𝑧 ) ) )
56 eqid ⊢ ( abs ∘ − ) = ( abs ∘ − )
57 56 cnmetdval ⊢ ( ( 𝐵 ∈ ℂ ∧ 𝑧 ∈ ℂ ) → ( 𝐵 ( abs ∘ − ) 𝑧 ) = ( abs ‘ ( 𝐵 − 𝑧 ) ) )
58 48 54 57 syl2anc ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ∧ 𝑧 ∈ ( 𝐵 ( ball ‘ ( abs ∘ − ) ) 𝑦 ) ) → ( 𝐵 ( abs ∘ − ) 𝑧 ) = ( abs ‘ ( 𝐵 − 𝑧 ) ) )
59 53 simprd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ∧ 𝑧 ∈ ( 𝐵 ( ball ‘ ( abs ∘ − ) ) 𝑦 ) ) → ( 𝐵 ( abs ∘ − ) 𝑧 ) < 𝑦 )
60 58 59 eqbrtrrd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ∧ 𝑧 ∈ ( 𝐵 ( ball ‘ ( abs ∘ − ) ) 𝑦 ) ) → ( abs ‘ ( 𝐵 − 𝑧 ) ) < 𝑦 )
61 55 60 eqbrtrd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ∧ 𝑧 ∈ ( 𝐵 ( ball ‘ ( abs ∘ − ) ) 𝑦 ) ) → ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑦 )
62 40 41 42 61 syl3anc ⊢ ( ( ( ( ( ( 𝜑 ∧ ¬ 𝐿 ∈ ℝ ) ∧ 𝑥 ∈ ℝ+ ) ∧ ∀ 𝑤 ∈ ℝ 𝑥 < ( abs ‘ ( 𝐿 − 𝑤 ) ) ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( ¬ 𝑧 ∈ { 𝐵 } ∧ 𝑧 ∈ ( 𝐵 ( ball ‘ ( abs ∘ − ) ) 𝑦 ) ) ) → ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑦 )
63 39 62 jca ⊢ ( ( ( ( ( ( 𝜑 ∧ ¬ 𝐿 ∈ ℝ ) ∧ 𝑥 ∈ ℝ+ ) ∧ ∀ 𝑤 ∈ ℝ 𝑥 < ( abs ‘ ( 𝐿 − 𝑤 ) ) ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( ¬ 𝑧 ∈ { 𝐵 } ∧ 𝑧 ∈ ( 𝐵 ( ball ‘ ( abs ∘ − ) ) 𝑦 ) ) ) → ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑦 ) )
64 63 adantlr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ¬ 𝐿 ∈ ℝ ) ∧ 𝑥 ∈ ℝ+ ) ∧ ∀ 𝑤 ∈ ℝ 𝑥 < ( abs ‘ ( 𝐿 − 𝑤 ) ) ) ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑧 ∈ 𝐴 ) ∧ ( ¬ 𝑧 ∈ { 𝐵 } ∧ 𝑧 ∈ ( 𝐵 ( ball ‘ ( abs ∘ − ) ) 𝑦 ) ) ) → ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑦 ) )
65 40 adantlr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ¬ 𝐿 ∈ ℝ ) ∧ 𝑥 ∈ ℝ+ ) ∧ ∀ 𝑤 ∈ ℝ 𝑥 < ( abs ‘ ( 𝐿 − 𝑤 ) ) ) ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑧 ∈ 𝐴 ) ∧ ( ¬ 𝑧 ∈ { 𝐵 } ∧ 𝑧 ∈ ( 𝐵 ( ball ‘ ( abs ∘ − ) ) 𝑦 ) ) ) → 𝜑 )
66 simplr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ¬ 𝐿 ∈ ℝ ) ∧ 𝑥 ∈ ℝ+ ) ∧ ∀ 𝑤 ∈ ℝ 𝑥 < ( abs ‘ ( 𝐿 − 𝑤 ) ) ) ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑧 ∈ 𝐴 ) ∧ ( ¬ 𝑧 ∈ { 𝐵 } ∧ 𝑧 ∈ ( 𝐵 ( ball ‘ ( abs ∘ − ) ) 𝑦 ) ) ) → 𝑧 ∈ 𝐴 )
67 65 66 jca ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ¬ 𝐿 ∈ ℝ ) ∧ 𝑥 ∈ ℝ+ ) ∧ ∀ 𝑤 ∈ ℝ 𝑥 < ( abs ‘ ( 𝐿 − 𝑤 ) ) ) ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑧 ∈ 𝐴 ) ∧ ( ¬ 𝑧 ∈ { 𝐵 } ∧ 𝑧 ∈ ( 𝐵 ( ball ‘ ( abs ∘ − ) ) 𝑦 ) ) ) → ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) )
68 simp-5r ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ¬ 𝐿 ∈ ℝ ) ∧ 𝑥 ∈ ℝ+ ) ∧ ∀ 𝑤 ∈ ℝ 𝑥 < ( abs ‘ ( 𝐿 − 𝑤 ) ) ) ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑧 ∈ 𝐴 ) ∧ ( ¬ 𝑧 ∈ { 𝐵 } ∧ 𝑧 ∈ ( 𝐵 ( ball ‘ ( abs ∘ − ) ) 𝑦 ) ) ) → 𝑥 ∈ ℝ+ )
69 simp-4r ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ¬ 𝐿 ∈ ℝ ) ∧ 𝑥 ∈ ℝ+ ) ∧ ∀ 𝑤 ∈ ℝ 𝑥 < ( abs ‘ ( 𝐿 − 𝑤 ) ) ) ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑧 ∈ 𝐴 ) ∧ ( ¬ 𝑧 ∈ { 𝐵 } ∧ 𝑧 ∈ ( 𝐵 ( ball ‘ ( abs ∘ − ) ) 𝑦 ) ) ) → ∀ 𝑤 ∈ ℝ 𝑥 < ( abs ‘ ( 𝐿 − 𝑤 ) ) )
70 rpre ⊢ ( 𝑥 ∈ ℝ+ → 𝑥 ∈ ℝ )
71 70 ad2antlr ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑥 ∈ ℝ+ ) ∧ ∀ 𝑤 ∈ ℝ 𝑥 < ( abs ‘ ( 𝐿 − 𝑤 ) ) ) → 𝑥 ∈ ℝ )
72 1 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑧 ) ∈ ℝ )
73 72 recnd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑧 ) ∈ ℂ )
74 73 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑥 ∈ ℝ+ ) ∧ ∀ 𝑤 ∈ ℝ 𝑥 < ( abs ‘ ( 𝐿 − 𝑤 ) ) ) → ( 𝐹 ‘ 𝑧 ) ∈ ℂ )
75 7 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑥 ∈ ℝ+ ) ∧ ∀ 𝑤 ∈ ℝ 𝑥 < ( abs ‘ ( 𝐿 − 𝑤 ) ) ) → 𝐿 ∈ ℂ )
76 74 75 subcld ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑥 ∈ ℝ+ ) ∧ ∀ 𝑤 ∈ ℝ 𝑥 < ( abs ‘ ( 𝐿 − 𝑤 ) ) ) → ( ( 𝐹 ‘ 𝑧 ) − 𝐿 ) ∈ ℂ )
77 76 abscld ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑥 ∈ ℝ+ ) ∧ ∀ 𝑤 ∈ ℝ 𝑥 < ( abs ‘ ( 𝐿 − 𝑤 ) ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝐿 ) ) ∈ ℝ )
78 72 adantr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) ∧ ∀ 𝑤 ∈ ℝ 𝑥 < ( abs ‘ ( 𝐿 − 𝑤 ) ) ) → ( 𝐹 ‘ 𝑧 ) ∈ ℝ )
79 nfv ⊢ Ⅎ 𝑤 𝜑
80 nfra1 ⊢ Ⅎ 𝑤 ∀ 𝑤 ∈ ℝ 𝑥 < ( abs ‘ ( 𝐿 − 𝑤 ) )
81 79 80 nfan ⊢ Ⅎ 𝑤 ( 𝜑 ∧ ∀ 𝑤 ∈ ℝ 𝑥 < ( abs ‘ ( 𝐿 − 𝑤 ) ) )
82 rspa ⊢ ( ( ∀ 𝑤 ∈ ℝ 𝑥 < ( abs ‘ ( 𝐿 − 𝑤 ) ) ∧ 𝑤 ∈ ℝ ) → 𝑥 < ( abs ‘ ( 𝐿 − 𝑤 ) ) )
83 82 adantll ⊢ ( ( ( 𝜑 ∧ ∀ 𝑤 ∈ ℝ 𝑥 < ( abs ‘ ( 𝐿 − 𝑤 ) ) ) ∧ 𝑤 ∈ ℝ ) → 𝑥 < ( abs ‘ ( 𝐿 − 𝑤 ) ) )
84 7 adantr ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ℝ ) → 𝐿 ∈ ℂ )
85 ax-resscn ⊢ ℝ ⊆ ℂ
86 85 a1i ⊢ ( 𝜑 → ℝ ⊆ ℂ )
87 86 sselda ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ℝ ) → 𝑤 ∈ ℂ )
88 84 87 abssubd ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ℝ ) → ( abs ‘ ( 𝐿 − 𝑤 ) ) = ( abs ‘ ( 𝑤 − 𝐿 ) ) )
89 88 adantlr ⊢ ( ( ( 𝜑 ∧ ∀ 𝑤 ∈ ℝ 𝑥 < ( abs ‘ ( 𝐿 − 𝑤 ) ) ) ∧ 𝑤 ∈ ℝ ) → ( abs ‘ ( 𝐿 − 𝑤 ) ) = ( abs ‘ ( 𝑤 − 𝐿 ) ) )
90 83 89 breqtrd ⊢ ( ( ( 𝜑 ∧ ∀ 𝑤 ∈ ℝ 𝑥 < ( abs ‘ ( 𝐿 − 𝑤 ) ) ) ∧ 𝑤 ∈ ℝ ) → 𝑥 < ( abs ‘ ( 𝑤 − 𝐿 ) ) )
91 90 ex ⊢ ( ( 𝜑 ∧ ∀ 𝑤 ∈ ℝ 𝑥 < ( abs ‘ ( 𝐿 − 𝑤 ) ) ) → ( 𝑤 ∈ ℝ → 𝑥 < ( abs ‘ ( 𝑤 − 𝐿 ) ) ) )
92 81 91 ralrimi ⊢ ( ( 𝜑 ∧ ∀ 𝑤 ∈ ℝ 𝑥 < ( abs ‘ ( 𝐿 − 𝑤 ) ) ) → ∀ 𝑤 ∈ ℝ 𝑥 < ( abs ‘ ( 𝑤 − 𝐿 ) ) )
93 92 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) ∧ ∀ 𝑤 ∈ ℝ 𝑥 < ( abs ‘ ( 𝐿 − 𝑤 ) ) ) → ∀ 𝑤 ∈ ℝ 𝑥 < ( abs ‘ ( 𝑤 − 𝐿 ) ) )
94 fvoveq1 ⊢ ( 𝑤 = ( 𝐹 ‘ 𝑧 ) → ( abs ‘ ( 𝑤 − 𝐿 ) ) = ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝐿 ) ) )
95 94 breq2d ⊢ ( 𝑤 = ( 𝐹 ‘ 𝑧 ) → ( 𝑥 < ( abs ‘ ( 𝑤 − 𝐿 ) ) ↔ 𝑥 < ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝐿 ) ) ) )
96 95 rspcv ⊢ ( ( 𝐹 ‘ 𝑧 ) ∈ ℝ → ( ∀ 𝑤 ∈ ℝ 𝑥 < ( abs ‘ ( 𝑤 − 𝐿 ) ) → 𝑥 < ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝐿 ) ) ) )
97 78 93 96 sylc ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) ∧ ∀ 𝑤 ∈ ℝ 𝑥 < ( abs ‘ ( 𝐿 − 𝑤 ) ) ) → 𝑥 < ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝐿 ) ) )
98 97 adantlr ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑥 ∈ ℝ+ ) ∧ ∀ 𝑤 ∈ ℝ 𝑥 < ( abs ‘ ( 𝐿 − 𝑤 ) ) ) → 𝑥 < ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝐿 ) ) )
99 71 77 98 ltnsymd ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑥 ∈ ℝ+ ) ∧ ∀ 𝑤 ∈ ℝ 𝑥 < ( abs ‘ ( 𝐿 − 𝑤 ) ) ) → ¬ ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝐿 ) ) < 𝑥 )
100 67 68 69 99 syl21anc ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ¬ 𝐿 ∈ ℝ ) ∧ 𝑥 ∈ ℝ+ ) ∧ ∀ 𝑤 ∈ ℝ 𝑥 < ( abs ‘ ( 𝐿 − 𝑤 ) ) ) ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑧 ∈ 𝐴 ) ∧ ( ¬ 𝑧 ∈ { 𝐵 } ∧ 𝑧 ∈ ( 𝐵 ( ball ‘ ( abs ∘ − ) ) 𝑦 ) ) ) → ¬ ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝐿 ) ) < 𝑥 )
101 64 100 jcnd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ¬ 𝐿 ∈ ℝ ) ∧ 𝑥 ∈ ℝ+ ) ∧ ∀ 𝑤 ∈ ℝ 𝑥 < ( abs ‘ ( 𝐿 − 𝑤 ) ) ) ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑧 ∈ 𝐴 ) ∧ ( ¬ 𝑧 ∈ { 𝐵 } ∧ 𝑧 ∈ ( 𝐵 ( ball ‘ ( abs ∘ − ) ) 𝑦 ) ) ) → ¬ ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑦 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝐿 ) ) < 𝑥 ) )
102 101 ex ⊢ ( ( ( ( ( ( 𝜑 ∧ ¬ 𝐿 ∈ ℝ ) ∧ 𝑥 ∈ ℝ+ ) ∧ ∀ 𝑤 ∈ ℝ 𝑥 < ( abs ‘ ( 𝐿 − 𝑤 ) ) ) ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑧 ∈ 𝐴 ) → ( ( ¬ 𝑧 ∈ { 𝐵 } ∧ 𝑧 ∈ ( 𝐵 ( ball ‘ ( abs ∘ − ) ) 𝑦 ) ) → ¬ ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑦 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝐿 ) ) < 𝑥 ) ) )
103 102 reximdva ⊢ ( ( ( ( ( 𝜑 ∧ ¬ 𝐿 ∈ ℝ ) ∧ 𝑥 ∈ ℝ+ ) ∧ ∀ 𝑤 ∈ ℝ 𝑥 < ( abs ‘ ( 𝐿 − 𝑤 ) ) ) ∧ 𝑦 ∈ ℝ+ ) → ( ∃ 𝑧 ∈ 𝐴 ( ¬ 𝑧 ∈ { 𝐵 } ∧ 𝑧 ∈ ( 𝐵 ( ball ‘ ( abs ∘ − ) ) 𝑦 ) ) → ∃ 𝑧 ∈ 𝐴 ¬ ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑦 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝐿 ) ) < 𝑥 ) ) )
104 35 103 mpd ⊢ ( ( ( ( ( 𝜑 ∧ ¬ 𝐿 ∈ ℝ ) ∧ 𝑥 ∈ ℝ+ ) ∧ ∀ 𝑤 ∈ ℝ 𝑥 < ( abs ‘ ( 𝐿 − 𝑤 ) ) ) ∧ 𝑦 ∈ ℝ+ ) → ∃ 𝑧 ∈ 𝐴 ¬ ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑦 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝐿 ) ) < 𝑥 ) )
105 rexnal ⊢ ( ∃ 𝑧 ∈ 𝐴 ¬ ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑦 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝐿 ) ) < 𝑥 ) ↔ ¬ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑦 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝐿 ) ) < 𝑥 ) )
106 104 105 sylib ⊢ ( ( ( ( ( 𝜑 ∧ ¬ 𝐿 ∈ ℝ ) ∧ 𝑥 ∈ ℝ+ ) ∧ ∀ 𝑤 ∈ ℝ 𝑥 < ( abs ‘ ( 𝐿 − 𝑤 ) ) ) ∧ 𝑦 ∈ ℝ+ ) → ¬ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑦 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝐿 ) ) < 𝑥 ) )
107 106 nrexdv ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝐿 ∈ ℝ ) ∧ 𝑥 ∈ ℝ+ ) ∧ ∀ 𝑤 ∈ ℝ 𝑥 < ( abs ‘ ( 𝐿 − 𝑤 ) ) ) → ¬ ∃ 𝑦 ∈ ℝ+ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑦 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝐿 ) ) < 𝑥 ) )
108 107 ex ⊢ ( ( ( 𝜑 ∧ ¬ 𝐿 ∈ ℝ ) ∧ 𝑥 ∈ ℝ+ ) → ( ∀ 𝑤 ∈ ℝ 𝑥 < ( abs ‘ ( 𝐿 − 𝑤 ) ) → ¬ ∃ 𝑦 ∈ ℝ+ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑦 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝐿 ) ) < 𝑥 ) ) )
109 108 reximdva ⊢ ( ( 𝜑 ∧ ¬ 𝐿 ∈ ℝ ) → ( ∃ 𝑥 ∈ ℝ+ ∀ 𝑤 ∈ ℝ 𝑥 < ( abs ‘ ( 𝐿 − 𝑤 ) ) → ∃ 𝑥 ∈ ℝ+ ¬ ∃ 𝑦 ∈ ℝ+ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑦 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝐿 ) ) < 𝑥 ) ) )
110 11 109 mpd ⊢ ( ( 𝜑 ∧ ¬ 𝐿 ∈ ℝ ) → ∃ 𝑥 ∈ ℝ+ ¬ ∃ 𝑦 ∈ ℝ+ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑦 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝐿 ) ) < 𝑥 ) )
111 rexnal ⊢ ( ∃ 𝑥 ∈ ℝ+ ¬ ∃ 𝑦 ∈ ℝ+ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑦 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝐿 ) ) < 𝑥 ) ↔ ¬ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ ℝ+ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑦 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝐿 ) ) < 𝑥 ) )
112 110 111 sylib ⊢ ( ( 𝜑 ∧ ¬ 𝐿 ∈ ℝ ) → ¬ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ ℝ+ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑦 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝐿 ) ) < 𝑥 ) )
113 112 intnand ⊢ ( ( 𝜑 ∧ ¬ 𝐿 ∈ ℝ ) → ¬ ( 𝐿 ∈ ℂ ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ ℝ+ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑦 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝐿 ) ) < 𝑥 ) ) )
114 1 86 fssd ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℂ )
115 114 2 47 ellimc3 ⊢ ( 𝜑 → ( 𝐿 ∈ ( 𝐹 limℂ 𝐵 ) ↔ ( 𝐿 ∈ ℂ ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ ℝ+ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑦 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝐿 ) ) < 𝑥 ) ) ) )
116 115 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝐿 ∈ ℝ ) → ( 𝐿 ∈ ( 𝐹 limℂ 𝐵 ) ↔ ( 𝐿 ∈ ℂ ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ ℝ+ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑦 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝐿 ) ) < 𝑥 ) ) ) )
117 113 116 mtbird ⊢ ( ( 𝜑 ∧ ¬ 𝐿 ∈ ℝ ) → ¬ 𝐿 ∈ ( 𝐹 limℂ 𝐵 ) )
118 5 117 condan ⊢ ( 𝜑 → 𝐿 ∈ ℝ )