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 ffvelrnda ⊒ ( ( πœ‘ ∧ 𝑧 ∈ 𝐴 ) β†’ ( 𝐹 β€˜ 𝑧 ) ∈ ℝ )
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 ⊒ ( πœ‘ β†’ 𝐿 ∈ ℝ )