Metamath Proof Explorer

Theorem unblimceq0

Description: If F is unbounded near A it has no limit at A . (Contributed by Asger C. Ipsen, 12-May-2021)

Ref Expression
Hypotheses unblimceq0.0 ⊢ ( 𝜑 → 𝑆 ⊆ ℂ )
unblimceq0.1 ⊢ ( 𝜑 → 𝐹 : 𝑆 ⟶ ℂ )
unblimceq0.2 ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
unblimceq0.3 ⊢ ( 𝜑 → ∀ 𝑏 ∈ ℝ+ ∀ 𝑑 ∈ ℝ+ ∃ 𝑥 ∈ 𝑆 ( ( abs ‘ ( 𝑥 − 𝐴 ) ) < 𝑑 ∧ 𝑏 ≤ ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ) )
Assertion unblimceq0 ( 𝜑 → ( 𝐹 limℂ 𝐴 ) = ∅ )

Proof

Step Hyp Ref Expression
1 unblimceq0.0 ⊢ ( 𝜑 → 𝑆 ⊆ ℂ )
2 unblimceq0.1 ⊢ ( 𝜑 → 𝐹 : 𝑆 ⟶ ℂ )
3 unblimceq0.2 ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
4 unblimceq0.3 ⊢ ( 𝜑 → ∀ 𝑏 ∈ ℝ+ ∀ 𝑑 ∈ ℝ+ ∃ 𝑥 ∈ 𝑆 ( ( abs ‘ ( 𝑥 − 𝐴 ) ) < 𝑑 ∧ 𝑏 ≤ ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ) )
5 1rp ⊢ 1 ∈ ℝ+
6 5 a1i ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) → 1 ∈ ℝ+ )
7 breq2 ⊢ ( 𝑒 = 1 → ( ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑦 ) ) < 𝑒 ↔ ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑦 ) ) < 1 ) )
8 7 imbi2d ⊢ ( 𝑒 = 1 → ( ( ( 𝑧 ≠ 𝐴 ∧ ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑐 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑦 ) ) < 𝑒 ) ↔ ( ( 𝑧 ≠ 𝐴 ∧ ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑐 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑦 ) ) < 1 ) ) )
9 8 rexralbidv ⊢ ( 𝑒 = 1 → ( ∃ 𝑐 ∈ ℝ+ ∀ 𝑧 ∈ 𝑆 ( ( 𝑧 ≠ 𝐴 ∧ ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑐 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑦 ) ) < 𝑒 ) ↔ ∃ 𝑐 ∈ ℝ+ ∀ 𝑧 ∈ 𝑆 ( ( 𝑧 ≠ 𝐴 ∧ ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑐 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑦 ) ) < 1 ) ) )
10 9 notbid ⊢ ( 𝑒 = 1 → ( ¬ ∃ 𝑐 ∈ ℝ+ ∀ 𝑧 ∈ 𝑆 ( ( 𝑧 ≠ 𝐴 ∧ ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑐 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑦 ) ) < 𝑒 ) ↔ ¬ ∃ 𝑐 ∈ ℝ+ ∀ 𝑧 ∈ 𝑆 ( ( 𝑧 ≠ 𝐴 ∧ ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑐 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑦 ) ) < 1 ) ) )
11 10 adantl ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) ∧ 𝑒 = 1 ) → ( ¬ ∃ 𝑐 ∈ ℝ+ ∀ 𝑧 ∈ 𝑆 ( ( 𝑧 ≠ 𝐴 ∧ ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑐 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑦 ) ) < 𝑒 ) ↔ ¬ ∃ 𝑐 ∈ ℝ+ ∀ 𝑧 ∈ 𝑆 ( ( 𝑧 ≠ 𝐴 ∧ ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑐 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑦 ) ) < 1 ) ) )
12 simprr1 ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) ∧ 𝑐 ∈ ℝ+ ) ∧ ( 𝑧 ∈ 𝑆 ∧ ( 𝑧 ≠ 𝐴 ∧ ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑐 ∧ ( 1 + ( abs ‘ 𝑦 ) ) ≤ ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ) ) ) → 𝑧 ≠ 𝐴 )
13 simprr2 ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) ∧ 𝑐 ∈ ℝ+ ) ∧ ( 𝑧 ∈ 𝑆 ∧ ( 𝑧 ≠ 𝐴 ∧ ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑐 ∧ ( 1 + ( abs ‘ 𝑦 ) ) ≤ ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ) ) ) → ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑐 )
14 12 13 jca ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) ∧ 𝑐 ∈ ℝ+ ) ∧ ( 𝑧 ∈ 𝑆 ∧ ( 𝑧 ≠ 𝐴 ∧ ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑐 ∧ ( 1 + ( abs ‘ 𝑦 ) ) ≤ ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ) ) ) → ( 𝑧 ≠ 𝐴 ∧ ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑐 ) )
15 1red ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) ∧ 𝑐 ∈ ℝ+ ) ∧ ( 𝑧 ∈ 𝑆 ∧ ( 𝑧 ≠ 𝐴 ∧ ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑐 ∧ ( 1 + ( abs ‘ 𝑦 ) ) ≤ ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ) ) ) → 1 ∈ ℝ )
16 2 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) ∧ 𝑐 ∈ ℝ+ ) → 𝐹 : 𝑆 ⟶ ℂ )
17 16 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) ∧ 𝑐 ∈ ℝ+ ) ∧ ( 𝑧 ∈ 𝑆 ∧ ( 𝑧 ≠ 𝐴 ∧ ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑐 ∧ ( 1 + ( abs ‘ 𝑦 ) ) ≤ ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ) ) ) → 𝐹 : 𝑆 ⟶ ℂ )
18 simprl ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) ∧ 𝑐 ∈ ℝ+ ) ∧ ( 𝑧 ∈ 𝑆 ∧ ( 𝑧 ≠ 𝐴 ∧ ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑐 ∧ ( 1 + ( abs ‘ 𝑦 ) ) ≤ ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ) ) ) → 𝑧 ∈ 𝑆 )
19 17 18 ffvelrnd ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) ∧ 𝑐 ∈ ℝ+ ) ∧ ( 𝑧 ∈ 𝑆 ∧ ( 𝑧 ≠ 𝐴 ∧ ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑐 ∧ ( 1 + ( abs ‘ 𝑦 ) ) ≤ ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ) ) ) → ( 𝐹 ‘ 𝑧 ) ∈ ℂ )
20 simplr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) ∧ 𝑐 ∈ ℝ+ ) → 𝑦 ∈ ℂ )
21 20 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) ∧ 𝑐 ∈ ℝ+ ) ∧ ( 𝑧 ∈ 𝑆 ∧ ( 𝑧 ≠ 𝐴 ∧ ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑐 ∧ ( 1 + ( abs ‘ 𝑦 ) ) ≤ ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ) ) ) → 𝑦 ∈ ℂ )
22 19 21 subcld ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) ∧ 𝑐 ∈ ℝ+ ) ∧ ( 𝑧 ∈ 𝑆 ∧ ( 𝑧 ≠ 𝐴 ∧ ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑐 ∧ ( 1 + ( abs ‘ 𝑦 ) ) ≤ ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ) ) ) → ( ( 𝐹 ‘ 𝑧 ) − 𝑦 ) ∈ ℂ )
23 22 abscld ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) ∧ 𝑐 ∈ ℝ+ ) ∧ ( 𝑧 ∈ 𝑆 ∧ ( 𝑧 ≠ 𝐴 ∧ ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑐 ∧ ( 1 + ( abs ‘ 𝑦 ) ) ≤ ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ) ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑦 ) ) ∈ ℝ )
24 19 abscld ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) ∧ 𝑐 ∈ ℝ+ ) ∧ ( 𝑧 ∈ 𝑆 ∧ ( 𝑧 ≠ 𝐴 ∧ ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑐 ∧ ( 1 + ( abs ‘ 𝑦 ) ) ≤ ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ) ) ) → ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ∈ ℝ )
25 20 abscld ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) ∧ 𝑐 ∈ ℝ+ ) → ( abs ‘ 𝑦 ) ∈ ℝ )
26 25 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) ∧ 𝑐 ∈ ℝ+ ) ∧ ( 𝑧 ∈ 𝑆 ∧ ( 𝑧 ≠ 𝐴 ∧ ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑐 ∧ ( 1 + ( abs ‘ 𝑦 ) ) ≤ ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ) ) ) → ( abs ‘ 𝑦 ) ∈ ℝ )
27 24 26 resubcld ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) ∧ 𝑐 ∈ ℝ+ ) ∧ ( 𝑧 ∈ 𝑆 ∧ ( 𝑧 ≠ 𝐴 ∧ ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑐 ∧ ( 1 + ( abs ‘ 𝑦 ) ) ≤ ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ) ) ) → ( ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) − ( abs ‘ 𝑦 ) ) ∈ ℝ )
28 1cnd ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) ∧ 𝑐 ∈ ℝ+ ) ∧ ( 𝑧 ∈ 𝑆 ∧ ( 𝑧 ≠ 𝐴 ∧ ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑐 ∧ ( 1 + ( abs ‘ 𝑦 ) ) ≤ ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ) ) ) → 1 ∈ ℂ )
29 26 recnd ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) ∧ 𝑐 ∈ ℝ+ ) ∧ ( 𝑧 ∈ 𝑆 ∧ ( 𝑧 ≠ 𝐴 ∧ ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑐 ∧ ( 1 + ( abs ‘ 𝑦 ) ) ≤ ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ) ) ) → ( abs ‘ 𝑦 ) ∈ ℂ )
30 28 29 pncand ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) ∧ 𝑐 ∈ ℝ+ ) ∧ ( 𝑧 ∈ 𝑆 ∧ ( 𝑧 ≠ 𝐴 ∧ ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑐 ∧ ( 1 + ( abs ‘ 𝑦 ) ) ≤ ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ) ) ) → ( ( 1 + ( abs ‘ 𝑦 ) ) − ( abs ‘ 𝑦 ) ) = 1 )
31 1red ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) ∧ 𝑐 ∈ ℝ+ ) → 1 ∈ ℝ )
32 31 25 readdcld ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) ∧ 𝑐 ∈ ℝ+ ) → ( 1 + ( abs ‘ 𝑦 ) ) ∈ ℝ )
33 32 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) ∧ 𝑐 ∈ ℝ+ ) ∧ ( 𝑧 ∈ 𝑆 ∧ ( 𝑧 ≠ 𝐴 ∧ ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑐 ∧ ( 1 + ( abs ‘ 𝑦 ) ) ≤ ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ) ) ) → ( 1 + ( abs ‘ 𝑦 ) ) ∈ ℝ )
34 simprr3 ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) ∧ 𝑐 ∈ ℝ+ ) ∧ ( 𝑧 ∈ 𝑆 ∧ ( 𝑧 ≠ 𝐴 ∧ ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑐 ∧ ( 1 + ( abs ‘ 𝑦 ) ) ≤ ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ) ) ) → ( 1 + ( abs ‘ 𝑦 ) ) ≤ ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) )
35 33 24 26 34 lesub1dd ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) ∧ 𝑐 ∈ ℝ+ ) ∧ ( 𝑧 ∈ 𝑆 ∧ ( 𝑧 ≠ 𝐴 ∧ ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑐 ∧ ( 1 + ( abs ‘ 𝑦 ) ) ≤ ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ) ) ) → ( ( 1 + ( abs ‘ 𝑦 ) ) − ( abs ‘ 𝑦 ) ) ≤ ( ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) − ( abs ‘ 𝑦 ) ) )
36 30 35 eqbrtrrd ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) ∧ 𝑐 ∈ ℝ+ ) ∧ ( 𝑧 ∈ 𝑆 ∧ ( 𝑧 ≠ 𝐴 ∧ ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑐 ∧ ( 1 + ( abs ‘ 𝑦 ) ) ≤ ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ) ) ) → 1 ≤ ( ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) − ( abs ‘ 𝑦 ) ) )
37 19 21 abs2difd ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) ∧ 𝑐 ∈ ℝ+ ) ∧ ( 𝑧 ∈ 𝑆 ∧ ( 𝑧 ≠ 𝐴 ∧ ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑐 ∧ ( 1 + ( abs ‘ 𝑦 ) ) ≤ ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ) ) ) → ( ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) − ( abs ‘ 𝑦 ) ) ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑦 ) ) )
38 15 27 23 36 37 letrd ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) ∧ 𝑐 ∈ ℝ+ ) ∧ ( 𝑧 ∈ 𝑆 ∧ ( 𝑧 ≠ 𝐴 ∧ ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑐 ∧ ( 1 + ( abs ‘ 𝑦 ) ) ≤ ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ) ) ) → 1 ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑦 ) ) )
39 15 23 38 lensymd ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) ∧ 𝑐 ∈ ℝ+ ) ∧ ( 𝑧 ∈ 𝑆 ∧ ( 𝑧 ≠ 𝐴 ∧ ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑐 ∧ ( 1 + ( abs ‘ 𝑦 ) ) ≤ ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ) ) ) → ¬ ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑦 ) ) < 1 )
40 14 39 jcnd ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) ∧ 𝑐 ∈ ℝ+ ) ∧ ( 𝑧 ∈ 𝑆 ∧ ( 𝑧 ≠ 𝐴 ∧ ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑐 ∧ ( 1 + ( abs ‘ 𝑦 ) ) ≤ ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ) ) ) → ¬ ( ( 𝑧 ≠ 𝐴 ∧ ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑐 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑦 ) ) < 1 ) )
41 breq2 ⊢ ( 𝑑 = 𝑐 → ( ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑑 ↔ ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑐 ) )
42 41 3anbi2d ⊢ ( 𝑑 = 𝑐 → ( ( 𝑧 ≠ 𝐴 ∧ ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑑 ∧ ( 1 + ( abs ‘ 𝑦 ) ) ≤ ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ) ↔ ( 𝑧 ≠ 𝐴 ∧ ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑐 ∧ ( 1 + ( abs ‘ 𝑦 ) ) ≤ ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ) ) )
43 42 rexbidv ⊢ ( 𝑑 = 𝑐 → ( ∃ 𝑧 ∈ 𝑆 ( 𝑧 ≠ 𝐴 ∧ ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑑 ∧ ( 1 + ( abs ‘ 𝑦 ) ) ≤ ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ) ↔ ∃ 𝑧 ∈ 𝑆 ( 𝑧 ≠ 𝐴 ∧ ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑐 ∧ ( 1 + ( abs ‘ 𝑦 ) ) ≤ ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ) ) )
44 breq1 ⊢ ( 𝑎 = ( 1 + ( abs ‘ 𝑦 ) ) → ( 𝑎 ≤ ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ↔ ( 1 + ( abs ‘ 𝑦 ) ) ≤ ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ) )
45 44 3anbi3d ⊢ ( 𝑎 = ( 1 + ( abs ‘ 𝑦 ) ) → ( ( 𝑧 ≠ 𝐴 ∧ ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑑 ∧ 𝑎 ≤ ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ) ↔ ( 𝑧 ≠ 𝐴 ∧ ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑑 ∧ ( 1 + ( abs ‘ 𝑦 ) ) ≤ ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ) ) )
46 45 rexbidv ⊢ ( 𝑎 = ( 1 + ( abs ‘ 𝑦 ) ) → ( ∃ 𝑧 ∈ 𝑆 ( 𝑧 ≠ 𝐴 ∧ ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑑 ∧ 𝑎 ≤ ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ) ↔ ∃ 𝑧 ∈ 𝑆 ( 𝑧 ≠ 𝐴 ∧ ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑑 ∧ ( 1 + ( abs ‘ 𝑦 ) ) ≤ ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ) ) )
47 46 ralbidv ⊢ ( 𝑎 = ( 1 + ( abs ‘ 𝑦 ) ) → ( ∀ 𝑑 ∈ ℝ+ ∃ 𝑧 ∈ 𝑆 ( 𝑧 ≠ 𝐴 ∧ ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑑 ∧ 𝑎 ≤ ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ) ↔ ∀ 𝑑 ∈ ℝ+ ∃ 𝑧 ∈ 𝑆 ( 𝑧 ≠ 𝐴 ∧ ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑑 ∧ ( 1 + ( abs ‘ 𝑦 ) ) ≤ ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ) ) )
48 1 2 3 4 unblimceq0lem ⊢ ( 𝜑 → ∀ 𝑎 ∈ ℝ+ ∀ 𝑑 ∈ ℝ+ ∃ 𝑧 ∈ 𝑆 ( 𝑧 ≠ 𝐴 ∧ ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑑 ∧ 𝑎 ≤ ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ) )
49 48 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) ∧ 𝑐 ∈ ℝ+ ) → ∀ 𝑎 ∈ ℝ+ ∀ 𝑑 ∈ ℝ+ ∃ 𝑧 ∈ 𝑆 ( 𝑧 ≠ 𝐴 ∧ ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑑 ∧ 𝑎 ≤ ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ) )
50 0lt1 ⊢ 0 < 1
51 50 a1i ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) ∧ 𝑐 ∈ ℝ+ ) → 0 < 1 )
52 20 absge0d ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) ∧ 𝑐 ∈ ℝ+ ) → 0 ≤ ( abs ‘ 𝑦 ) )
53 31 25 51 52 addgtge0d ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) ∧ 𝑐 ∈ ℝ+ ) → 0 < ( 1 + ( abs ‘ 𝑦 ) ) )
54 32 53 elrpd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) ∧ 𝑐 ∈ ℝ+ ) → ( 1 + ( abs ‘ 𝑦 ) ) ∈ ℝ+ )
55 47 49 54 rspcdva ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) ∧ 𝑐 ∈ ℝ+ ) → ∀ 𝑑 ∈ ℝ+ ∃ 𝑧 ∈ 𝑆 ( 𝑧 ≠ 𝐴 ∧ ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑑 ∧ ( 1 + ( abs ‘ 𝑦 ) ) ≤ ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ) )
56 simpr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) ∧ 𝑐 ∈ ℝ+ ) → 𝑐 ∈ ℝ+ )
57 43 55 56 rspcdva ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) ∧ 𝑐 ∈ ℝ+ ) → ∃ 𝑧 ∈ 𝑆 ( 𝑧 ≠ 𝐴 ∧ ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑐 ∧ ( 1 + ( abs ‘ 𝑦 ) ) ≤ ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ) )
58 40 57 reximddv ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) ∧ 𝑐 ∈ ℝ+ ) → ∃ 𝑧 ∈ 𝑆 ¬ ( ( 𝑧 ≠ 𝐴 ∧ ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑐 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑦 ) ) < 1 ) )
59 rexnal ⊢ ( ∃ 𝑧 ∈ 𝑆 ¬ ( ( 𝑧 ≠ 𝐴 ∧ ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑐 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑦 ) ) < 1 ) ↔ ¬ ∀ 𝑧 ∈ 𝑆 ( ( 𝑧 ≠ 𝐴 ∧ ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑐 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑦 ) ) < 1 ) )
60 58 59 sylib ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) ∧ 𝑐 ∈ ℝ+ ) → ¬ ∀ 𝑧 ∈ 𝑆 ( ( 𝑧 ≠ 𝐴 ∧ ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑐 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑦 ) ) < 1 ) )
61 60 nrexdv ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) → ¬ ∃ 𝑐 ∈ ℝ+ ∀ 𝑧 ∈ 𝑆 ( ( 𝑧 ≠ 𝐴 ∧ ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑐 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑦 ) ) < 1 ) )
62 6 11 61 rspcedvd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) → ∃ 𝑒 ∈ ℝ+ ¬ ∃ 𝑐 ∈ ℝ+ ∀ 𝑧 ∈ 𝑆 ( ( 𝑧 ≠ 𝐴 ∧ ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑐 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑦 ) ) < 𝑒 ) )
63 rexnal ⊢ ( ∃ 𝑒 ∈ ℝ+ ¬ ∃ 𝑐 ∈ ℝ+ ∀ 𝑧 ∈ 𝑆 ( ( 𝑧 ≠ 𝐴 ∧ ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑐 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑦 ) ) < 𝑒 ) ↔ ¬ ∀ 𝑒 ∈ ℝ+ ∃ 𝑐 ∈ ℝ+ ∀ 𝑧 ∈ 𝑆 ( ( 𝑧 ≠ 𝐴 ∧ ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑐 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑦 ) ) < 𝑒 ) )
64 62 63 sylib ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) → ¬ ∀ 𝑒 ∈ ℝ+ ∃ 𝑐 ∈ ℝ+ ∀ 𝑧 ∈ 𝑆 ( ( 𝑧 ≠ 𝐴 ∧ ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑐 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑦 ) ) < 𝑒 ) )
65 64 ex ⊢ ( 𝜑 → ( 𝑦 ∈ ℂ → ¬ ∀ 𝑒 ∈ ℝ+ ∃ 𝑐 ∈ ℝ+ ∀ 𝑧 ∈ 𝑆 ( ( 𝑧 ≠ 𝐴 ∧ ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑐 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑦 ) ) < 𝑒 ) ) )
66 imnan ⊢ ( ( 𝑦 ∈ ℂ → ¬ ∀ 𝑒 ∈ ℝ+ ∃ 𝑐 ∈ ℝ+ ∀ 𝑧 ∈ 𝑆 ( ( 𝑧 ≠ 𝐴 ∧ ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑐 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑦 ) ) < 𝑒 ) ) ↔ ¬ ( 𝑦 ∈ ℂ ∧ ∀ 𝑒 ∈ ℝ+ ∃ 𝑐 ∈ ℝ+ ∀ 𝑧 ∈ 𝑆 ( ( 𝑧 ≠ 𝐴 ∧ ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑐 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑦 ) ) < 𝑒 ) ) )
67 65 66 sylib ⊢ ( 𝜑 → ¬ ( 𝑦 ∈ ℂ ∧ ∀ 𝑒 ∈ ℝ+ ∃ 𝑐 ∈ ℝ+ ∀ 𝑧 ∈ 𝑆 ( ( 𝑧 ≠ 𝐴 ∧ ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑐 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑦 ) ) < 𝑒 ) ) )
68 2 1 3 ellimc3 ⊢ ( 𝜑 → ( 𝑦 ∈ ( 𝐹 limℂ 𝐴 ) ↔ ( 𝑦 ∈ ℂ ∧ ∀ 𝑒 ∈ ℝ+ ∃ 𝑐 ∈ ℝ+ ∀ 𝑧 ∈ 𝑆 ( ( 𝑧 ≠ 𝐴 ∧ ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑐 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑦 ) ) < 𝑒 ) ) ) )
69 67 68 mtbird ⊢ ( 𝜑 → ¬ 𝑦 ∈ ( 𝐹 limℂ 𝐴 ) )
70 69 eq0rdv ⊢ ( 𝜑 → ( 𝐹 limℂ 𝐴 ) = ∅ )