This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem reccn2

Description: The reciprocal function is continuous. (Contributed by Mario Carneiro, 9-Feb-2014) (Revised by Mario Carneiro, 22-Sep-2014)

Ref Expression
Hypothesis reccn2.t ⊢ 𝑇 = ( if ( 1 ≤ ( ( abs ‘ 𝐴 ) · 𝐵 ) , 1 , ( ( abs ‘ 𝐴 ) · 𝐵 ) ) · ( ( abs ‘ 𝐴 ) / 2 ) )
Assertion reccn2 ( ( 𝐴 ∈ ( ℂ ∖ { 0 } ) ∧ 𝐵 ∈ ℝ+ ) → ∃ 𝑦 ∈ ℝ+ ∀ 𝑧 ∈ ( ℂ ∖ { 0 } ) ( ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑦 → ( abs ‘ ( ( 1 / 𝑧 ) − ( 1 / 𝐴 ) ) ) < 𝐵 ) )

Proof

Step Hyp Ref Expression
1 reccn2.t ⊢ 𝑇 = ( if ( 1 ≤ ( ( abs ‘ 𝐴 ) · 𝐵 ) , 1 , ( ( abs ‘ 𝐴 ) · 𝐵 ) ) · ( ( abs ‘ 𝐴 ) / 2 ) )
2 1rp ⊢ 1 ∈ ℝ+
3 simpl ⊢ ( ( 𝐴 ∈ ( ℂ ∖ { 0 } ) ∧ 𝐵 ∈ ℝ+ ) → 𝐴 ∈ ( ℂ ∖ { 0 } ) )
4 eldifsn ⊢ ( 𝐴 ∈ ( ℂ ∖ { 0 } ) ↔ ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) )
5 3 4 sylib ⊢ ( ( 𝐴 ∈ ( ℂ ∖ { 0 } ) ∧ 𝐵 ∈ ℝ+ ) → ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) )
6 absrpcl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( abs ‘ 𝐴 ) ∈ ℝ+ )
7 5 6 syl ⊢ ( ( 𝐴 ∈ ( ℂ ∖ { 0 } ) ∧ 𝐵 ∈ ℝ+ ) → ( abs ‘ 𝐴 ) ∈ ℝ+ )
8 rpmulcl ⊢ ( ( ( abs ‘ 𝐴 ) ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) → ( ( abs ‘ 𝐴 ) · 𝐵 ) ∈ ℝ+ )
9 7 8 sylancom ⊢ ( ( 𝐴 ∈ ( ℂ ∖ { 0 } ) ∧ 𝐵 ∈ ℝ+ ) → ( ( abs ‘ 𝐴 ) · 𝐵 ) ∈ ℝ+ )
10 ifcl ⊢ ( ( 1 ∈ ℝ+ ∧ ( ( abs ‘ 𝐴 ) · 𝐵 ) ∈ ℝ+ ) → if ( 1 ≤ ( ( abs ‘ 𝐴 ) · 𝐵 ) , 1 , ( ( abs ‘ 𝐴 ) · 𝐵 ) ) ∈ ℝ+ )
11 2 9 10 sylancr ⊢ ( ( 𝐴 ∈ ( ℂ ∖ { 0 } ) ∧ 𝐵 ∈ ℝ+ ) → if ( 1 ≤ ( ( abs ‘ 𝐴 ) · 𝐵 ) , 1 , ( ( abs ‘ 𝐴 ) · 𝐵 ) ) ∈ ℝ+ )
12 7 rphalfcld ⊢ ( ( 𝐴 ∈ ( ℂ ∖ { 0 } ) ∧ 𝐵 ∈ ℝ+ ) → ( ( abs ‘ 𝐴 ) / 2 ) ∈ ℝ+ )
13 11 12 rpmulcld ⊢ ( ( 𝐴 ∈ ( ℂ ∖ { 0 } ) ∧ 𝐵 ∈ ℝ+ ) → ( if ( 1 ≤ ( ( abs ‘ 𝐴 ) · 𝐵 ) , 1 , ( ( abs ‘ 𝐴 ) · 𝐵 ) ) · ( ( abs ‘ 𝐴 ) / 2 ) ) ∈ ℝ+ )
14 1 13 eqeltrid ⊢ ( ( 𝐴 ∈ ( ℂ ∖ { 0 } ) ∧ 𝐵 ∈ ℝ+ ) → 𝑇 ∈ ℝ+ )
15 5 adantr ⊢ ( ( ( 𝐴 ∈ ( ℂ ∖ { 0 } ) ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ∧ ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑇 ) ) → ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) )
16 15 simpld ⊢ ( ( ( 𝐴 ∈ ( ℂ ∖ { 0 } ) ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ∧ ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑇 ) ) → 𝐴 ∈ ℂ )
17 simprl ⊢ ( ( ( 𝐴 ∈ ( ℂ ∖ { 0 } ) ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ∧ ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑇 ) ) → 𝑧 ∈ ( ℂ ∖ { 0 } ) )
18 eldifsn ⊢ ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ↔ ( 𝑧 ∈ ℂ ∧ 𝑧 ≠ 0 ) )
19 17 18 sylib ⊢ ( ( ( 𝐴 ∈ ( ℂ ∖ { 0 } ) ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ∧ ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑇 ) ) → ( 𝑧 ∈ ℂ ∧ 𝑧 ≠ 0 ) )
20 19 simpld ⊢ ( ( ( 𝐴 ∈ ( ℂ ∖ { 0 } ) ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ∧ ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑇 ) ) → 𝑧 ∈ ℂ )
21 16 20 mulcld ⊢ ( ( ( 𝐴 ∈ ( ℂ ∖ { 0 } ) ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ∧ ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑇 ) ) → ( 𝐴 · 𝑧 ) ∈ ℂ )
22 mulne0 ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑧 ∈ ℂ ∧ 𝑧 ≠ 0 ) ) → ( 𝐴 · 𝑧 ) ≠ 0 )
23 15 19 22 syl2anc ⊢ ( ( ( 𝐴 ∈ ( ℂ ∖ { 0 } ) ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ∧ ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑇 ) ) → ( 𝐴 · 𝑧 ) ≠ 0 )
24 16 20 21 23 divsubdird ⊢ ( ( ( 𝐴 ∈ ( ℂ ∖ { 0 } ) ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ∧ ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑇 ) ) → ( ( 𝐴 − 𝑧 ) / ( 𝐴 · 𝑧 ) ) = ( ( 𝐴 / ( 𝐴 · 𝑧 ) ) − ( 𝑧 / ( 𝐴 · 𝑧 ) ) ) )
25 16 mulridd ⊢ ( ( ( 𝐴 ∈ ( ℂ ∖ { 0 } ) ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ∧ ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑇 ) ) → ( 𝐴 · 1 ) = 𝐴 )
26 25 oveq1d ⊢ ( ( ( 𝐴 ∈ ( ℂ ∖ { 0 } ) ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ∧ ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑇 ) ) → ( ( 𝐴 · 1 ) / ( 𝐴 · 𝑧 ) ) = ( 𝐴 / ( 𝐴 · 𝑧 ) ) )
27 1cnd ⊢ ( ( ( 𝐴 ∈ ( ℂ ∖ { 0 } ) ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ∧ ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑇 ) ) → 1 ∈ ℂ )
28 divcan5 ⊢ ( ( 1 ∈ ℂ ∧ ( 𝑧 ∈ ℂ ∧ 𝑧 ≠ 0 ) ∧ ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ) → ( ( 𝐴 · 1 ) / ( 𝐴 · 𝑧 ) ) = ( 1 / 𝑧 ) )
29 27 19 15 28 syl3anc ⊢ ( ( ( 𝐴 ∈ ( ℂ ∖ { 0 } ) ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ∧ ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑇 ) ) → ( ( 𝐴 · 1 ) / ( 𝐴 · 𝑧 ) ) = ( 1 / 𝑧 ) )
30 26 29 eqtr3d ⊢ ( ( ( 𝐴 ∈ ( ℂ ∖ { 0 } ) ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ∧ ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑇 ) ) → ( 𝐴 / ( 𝐴 · 𝑧 ) ) = ( 1 / 𝑧 ) )
31 20 mulridd ⊢ ( ( ( 𝐴 ∈ ( ℂ ∖ { 0 } ) ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ∧ ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑇 ) ) → ( 𝑧 · 1 ) = 𝑧 )
32 20 16 mulcomd ⊢ ( ( ( 𝐴 ∈ ( ℂ ∖ { 0 } ) ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ∧ ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑇 ) ) → ( 𝑧 · 𝐴 ) = ( 𝐴 · 𝑧 ) )
33 31 32 oveq12d ⊢ ( ( ( 𝐴 ∈ ( ℂ ∖ { 0 } ) ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ∧ ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑇 ) ) → ( ( 𝑧 · 1 ) / ( 𝑧 · 𝐴 ) ) = ( 𝑧 / ( 𝐴 · 𝑧 ) ) )
34 divcan5 ⊢ ( ( 1 ∈ ℂ ∧ ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑧 ∈ ℂ ∧ 𝑧 ≠ 0 ) ) → ( ( 𝑧 · 1 ) / ( 𝑧 · 𝐴 ) ) = ( 1 / 𝐴 ) )
35 27 15 19 34 syl3anc ⊢ ( ( ( 𝐴 ∈ ( ℂ ∖ { 0 } ) ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ∧ ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑇 ) ) → ( ( 𝑧 · 1 ) / ( 𝑧 · 𝐴 ) ) = ( 1 / 𝐴 ) )
36 33 35 eqtr3d ⊢ ( ( ( 𝐴 ∈ ( ℂ ∖ { 0 } ) ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ∧ ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑇 ) ) → ( 𝑧 / ( 𝐴 · 𝑧 ) ) = ( 1 / 𝐴 ) )
37 30 36 oveq12d ⊢ ( ( ( 𝐴 ∈ ( ℂ ∖ { 0 } ) ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ∧ ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑇 ) ) → ( ( 𝐴 / ( 𝐴 · 𝑧 ) ) − ( 𝑧 / ( 𝐴 · 𝑧 ) ) ) = ( ( 1 / 𝑧 ) − ( 1 / 𝐴 ) ) )
38 24 37 eqtrd ⊢ ( ( ( 𝐴 ∈ ( ℂ ∖ { 0 } ) ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ∧ ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑇 ) ) → ( ( 𝐴 − 𝑧 ) / ( 𝐴 · 𝑧 ) ) = ( ( 1 / 𝑧 ) − ( 1 / 𝐴 ) ) )
39 38 fveq2d ⊢ ( ( ( 𝐴 ∈ ( ℂ ∖ { 0 } ) ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ∧ ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑇 ) ) → ( abs ‘ ( ( 𝐴 − 𝑧 ) / ( 𝐴 · 𝑧 ) ) ) = ( abs ‘ ( ( 1 / 𝑧 ) − ( 1 / 𝐴 ) ) ) )
40 16 20 subcld ⊢ ( ( ( 𝐴 ∈ ( ℂ ∖ { 0 } ) ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ∧ ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑇 ) ) → ( 𝐴 − 𝑧 ) ∈ ℂ )
41 40 21 23 absdivd ⊢ ( ( ( 𝐴 ∈ ( ℂ ∖ { 0 } ) ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ∧ ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑇 ) ) → ( abs ‘ ( ( 𝐴 − 𝑧 ) / ( 𝐴 · 𝑧 ) ) ) = ( ( abs ‘ ( 𝐴 − 𝑧 ) ) / ( abs ‘ ( 𝐴 · 𝑧 ) ) ) )
42 39 41 eqtr3d ⊢ ( ( ( 𝐴 ∈ ( ℂ ∖ { 0 } ) ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ∧ ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑇 ) ) → ( abs ‘ ( ( 1 / 𝑧 ) − ( 1 / 𝐴 ) ) ) = ( ( abs ‘ ( 𝐴 − 𝑧 ) ) / ( abs ‘ ( 𝐴 · 𝑧 ) ) ) )
43 16 20 abssubd ⊢ ( ( ( 𝐴 ∈ ( ℂ ∖ { 0 } ) ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ∧ ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑇 ) ) → ( abs ‘ ( 𝐴 − 𝑧 ) ) = ( abs ‘ ( 𝑧 − 𝐴 ) ) )
44 20 16 subcld ⊢ ( ( ( 𝐴 ∈ ( ℂ ∖ { 0 } ) ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ∧ ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑇 ) ) → ( 𝑧 − 𝐴 ) ∈ ℂ )
45 44 abscld ⊢ ( ( ( 𝐴 ∈ ( ℂ ∖ { 0 } ) ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ∧ ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑇 ) ) → ( abs ‘ ( 𝑧 − 𝐴 ) ) ∈ ℝ )
46 43 45 eqeltrd ⊢ ( ( ( 𝐴 ∈ ( ℂ ∖ { 0 } ) ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ∧ ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑇 ) ) → ( abs ‘ ( 𝐴 − 𝑧 ) ) ∈ ℝ )
47 14 adantr ⊢ ( ( ( 𝐴 ∈ ( ℂ ∖ { 0 } ) ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ∧ ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑇 ) ) → 𝑇 ∈ ℝ+ )
48 47 rpred ⊢ ( ( ( 𝐴 ∈ ( ℂ ∖ { 0 } ) ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ∧ ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑇 ) ) → 𝑇 ∈ ℝ )
49 21 abscld ⊢ ( ( ( 𝐴 ∈ ( ℂ ∖ { 0 } ) ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ∧ ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑇 ) ) → ( abs ‘ ( 𝐴 · 𝑧 ) ) ∈ ℝ )
50 rpre ⊢ ( 𝐵 ∈ ℝ+ → 𝐵 ∈ ℝ )
51 50 ad2antlr ⊢ ( ( ( 𝐴 ∈ ( ℂ ∖ { 0 } ) ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ∧ ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑇 ) ) → 𝐵 ∈ ℝ )
52 49 51 remulcld ⊢ ( ( ( 𝐴 ∈ ( ℂ ∖ { 0 } ) ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ∧ ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑇 ) ) → ( ( abs ‘ ( 𝐴 · 𝑧 ) ) · 𝐵 ) ∈ ℝ )
53 simprr ⊢ ( ( ( 𝐴 ∈ ( ℂ ∖ { 0 } ) ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ∧ ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑇 ) ) → ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑇 )
54 43 53 eqbrtrd ⊢ ( ( ( 𝐴 ∈ ( ℂ ∖ { 0 } ) ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ∧ ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑇 ) ) → ( abs ‘ ( 𝐴 − 𝑧 ) ) < 𝑇 )
55 9 adantr ⊢ ( ( ( 𝐴 ∈ ( ℂ ∖ { 0 } ) ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ∧ ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑇 ) ) → ( ( abs ‘ 𝐴 ) · 𝐵 ) ∈ ℝ+ )
56 55 rpred ⊢ ( ( ( 𝐴 ∈ ( ℂ ∖ { 0 } ) ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ∧ ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑇 ) ) → ( ( abs ‘ 𝐴 ) · 𝐵 ) ∈ ℝ )
57 12 adantr ⊢ ( ( ( 𝐴 ∈ ( ℂ ∖ { 0 } ) ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ∧ ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑇 ) ) → ( ( abs ‘ 𝐴 ) / 2 ) ∈ ℝ+ )
58 57 rpred ⊢ ( ( ( 𝐴 ∈ ( ℂ ∖ { 0 } ) ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ∧ ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑇 ) ) → ( ( abs ‘ 𝐴 ) / 2 ) ∈ ℝ )
59 56 58 remulcld ⊢ ( ( ( 𝐴 ∈ ( ℂ ∖ { 0 } ) ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ∧ ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑇 ) ) → ( ( ( abs ‘ 𝐴 ) · 𝐵 ) · ( ( abs ‘ 𝐴 ) / 2 ) ) ∈ ℝ )
60 1re ⊢ 1 ∈ ℝ
61 min2 ⊢ ( ( 1 ∈ ℝ ∧ ( ( abs ‘ 𝐴 ) · 𝐵 ) ∈ ℝ ) → if ( 1 ≤ ( ( abs ‘ 𝐴 ) · 𝐵 ) , 1 , ( ( abs ‘ 𝐴 ) · 𝐵 ) ) ≤ ( ( abs ‘ 𝐴 ) · 𝐵 ) )
62 60 56 61 sylancr ⊢ ( ( ( 𝐴 ∈ ( ℂ ∖ { 0 } ) ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ∧ ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑇 ) ) → if ( 1 ≤ ( ( abs ‘ 𝐴 ) · 𝐵 ) , 1 , ( ( abs ‘ 𝐴 ) · 𝐵 ) ) ≤ ( ( abs ‘ 𝐴 ) · 𝐵 ) )
63 11 adantr ⊢ ( ( ( 𝐴 ∈ ( ℂ ∖ { 0 } ) ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ∧ ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑇 ) ) → if ( 1 ≤ ( ( abs ‘ 𝐴 ) · 𝐵 ) , 1 , ( ( abs ‘ 𝐴 ) · 𝐵 ) ) ∈ ℝ+ )
64 63 rpred ⊢ ( ( ( 𝐴 ∈ ( ℂ ∖ { 0 } ) ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ∧ ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑇 ) ) → if ( 1 ≤ ( ( abs ‘ 𝐴 ) · 𝐵 ) , 1 , ( ( abs ‘ 𝐴 ) · 𝐵 ) ) ∈ ℝ )
65 64 56 57 lemul1d ⊢ ( ( ( 𝐴 ∈ ( ℂ ∖ { 0 } ) ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ∧ ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑇 ) ) → ( if ( 1 ≤ ( ( abs ‘ 𝐴 ) · 𝐵 ) , 1 , ( ( abs ‘ 𝐴 ) · 𝐵 ) ) ≤ ( ( abs ‘ 𝐴 ) · 𝐵 ) ↔ ( if ( 1 ≤ ( ( abs ‘ 𝐴 ) · 𝐵 ) , 1 , ( ( abs ‘ 𝐴 ) · 𝐵 ) ) · ( ( abs ‘ 𝐴 ) / 2 ) ) ≤ ( ( ( abs ‘ 𝐴 ) · 𝐵 ) · ( ( abs ‘ 𝐴 ) / 2 ) ) ) )
66 62 65 mpbid ⊢ ( ( ( 𝐴 ∈ ( ℂ ∖ { 0 } ) ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ∧ ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑇 ) ) → ( if ( 1 ≤ ( ( abs ‘ 𝐴 ) · 𝐵 ) , 1 , ( ( abs ‘ 𝐴 ) · 𝐵 ) ) · ( ( abs ‘ 𝐴 ) / 2 ) ) ≤ ( ( ( abs ‘ 𝐴 ) · 𝐵 ) · ( ( abs ‘ 𝐴 ) / 2 ) ) )
67 1 66 eqbrtrid ⊢ ( ( ( 𝐴 ∈ ( ℂ ∖ { 0 } ) ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ∧ ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑇 ) ) → 𝑇 ≤ ( ( ( abs ‘ 𝐴 ) · 𝐵 ) · ( ( abs ‘ 𝐴 ) / 2 ) ) )
68 20 abscld ⊢ ( ( ( 𝐴 ∈ ( ℂ ∖ { 0 } ) ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ∧ ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑇 ) ) → ( abs ‘ 𝑧 ) ∈ ℝ )
69 16 abscld ⊢ ( ( ( 𝐴 ∈ ( ℂ ∖ { 0 } ) ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ∧ ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑇 ) ) → ( abs ‘ 𝐴 ) ∈ ℝ )
70 69 recnd ⊢ ( ( ( 𝐴 ∈ ( ℂ ∖ { 0 } ) ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ∧ ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑇 ) ) → ( abs ‘ 𝐴 ) ∈ ℂ )
71 70 2halvesd ⊢ ( ( ( 𝐴 ∈ ( ℂ ∖ { 0 } ) ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ∧ ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑇 ) ) → ( ( ( abs ‘ 𝐴 ) / 2 ) + ( ( abs ‘ 𝐴 ) / 2 ) ) = ( abs ‘ 𝐴 ) )
72 69 68 resubcld ⊢ ( ( ( 𝐴 ∈ ( ℂ ∖ { 0 } ) ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ∧ ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑇 ) ) → ( ( abs ‘ 𝐴 ) − ( abs ‘ 𝑧 ) ) ∈ ℝ )
73 16 20 abs2difd ⊢ ( ( ( 𝐴 ∈ ( ℂ ∖ { 0 } ) ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ∧ ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑇 ) ) → ( ( abs ‘ 𝐴 ) − ( abs ‘ 𝑧 ) ) ≤ ( abs ‘ ( 𝐴 − 𝑧 ) ) )
74 min1 ⊢ ( ( 1 ∈ ℝ ∧ ( ( abs ‘ 𝐴 ) · 𝐵 ) ∈ ℝ ) → if ( 1 ≤ ( ( abs ‘ 𝐴 ) · 𝐵 ) , 1 , ( ( abs ‘ 𝐴 ) · 𝐵 ) ) ≤ 1 )
75 60 56 74 sylancr ⊢ ( ( ( 𝐴 ∈ ( ℂ ∖ { 0 } ) ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ∧ ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑇 ) ) → if ( 1 ≤ ( ( abs ‘ 𝐴 ) · 𝐵 ) , 1 , ( ( abs ‘ 𝐴 ) · 𝐵 ) ) ≤ 1 )
76 1red ⊢ ( ( ( 𝐴 ∈ ( ℂ ∖ { 0 } ) ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ∧ ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑇 ) ) → 1 ∈ ℝ )
77 64 76 57 lemul1d ⊢ ( ( ( 𝐴 ∈ ( ℂ ∖ { 0 } ) ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ∧ ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑇 ) ) → ( if ( 1 ≤ ( ( abs ‘ 𝐴 ) · 𝐵 ) , 1 , ( ( abs ‘ 𝐴 ) · 𝐵 ) ) ≤ 1 ↔ ( if ( 1 ≤ ( ( abs ‘ 𝐴 ) · 𝐵 ) , 1 , ( ( abs ‘ 𝐴 ) · 𝐵 ) ) · ( ( abs ‘ 𝐴 ) / 2 ) ) ≤ ( 1 · ( ( abs ‘ 𝐴 ) / 2 ) ) ) )
78 75 77 mpbid ⊢ ( ( ( 𝐴 ∈ ( ℂ ∖ { 0 } ) ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ∧ ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑇 ) ) → ( if ( 1 ≤ ( ( abs ‘ 𝐴 ) · 𝐵 ) , 1 , ( ( abs ‘ 𝐴 ) · 𝐵 ) ) · ( ( abs ‘ 𝐴 ) / 2 ) ) ≤ ( 1 · ( ( abs ‘ 𝐴 ) / 2 ) ) )
79 1 78 eqbrtrid ⊢ ( ( ( 𝐴 ∈ ( ℂ ∖ { 0 } ) ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ∧ ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑇 ) ) → 𝑇 ≤ ( 1 · ( ( abs ‘ 𝐴 ) / 2 ) ) )
80 58 recnd ⊢ ( ( ( 𝐴 ∈ ( ℂ ∖ { 0 } ) ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ∧ ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑇 ) ) → ( ( abs ‘ 𝐴 ) / 2 ) ∈ ℂ )
81 80 mullidd ⊢ ( ( ( 𝐴 ∈ ( ℂ ∖ { 0 } ) ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ∧ ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑇 ) ) → ( 1 · ( ( abs ‘ 𝐴 ) / 2 ) ) = ( ( abs ‘ 𝐴 ) / 2 ) )
82 79 81 breqtrd ⊢ ( ( ( 𝐴 ∈ ( ℂ ∖ { 0 } ) ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ∧ ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑇 ) ) → 𝑇 ≤ ( ( abs ‘ 𝐴 ) / 2 ) )
83 46 48 58 54 82 ltletrd ⊢ ( ( ( 𝐴 ∈ ( ℂ ∖ { 0 } ) ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ∧ ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑇 ) ) → ( abs ‘ ( 𝐴 − 𝑧 ) ) < ( ( abs ‘ 𝐴 ) / 2 ) )
84 72 46 58 73 83 lelttrd ⊢ ( ( ( 𝐴 ∈ ( ℂ ∖ { 0 } ) ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ∧ ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑇 ) ) → ( ( abs ‘ 𝐴 ) − ( abs ‘ 𝑧 ) ) < ( ( abs ‘ 𝐴 ) / 2 ) )
85 69 68 58 ltsubadd2d ⊢ ( ( ( 𝐴 ∈ ( ℂ ∖ { 0 } ) ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ∧ ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑇 ) ) → ( ( ( abs ‘ 𝐴 ) − ( abs ‘ 𝑧 ) ) < ( ( abs ‘ 𝐴 ) / 2 ) ↔ ( abs ‘ 𝐴 ) < ( ( abs ‘ 𝑧 ) + ( ( abs ‘ 𝐴 ) / 2 ) ) ) )
86 84 85 mpbid ⊢ ( ( ( 𝐴 ∈ ( ℂ ∖ { 0 } ) ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ∧ ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑇 ) ) → ( abs ‘ 𝐴 ) < ( ( abs ‘ 𝑧 ) + ( ( abs ‘ 𝐴 ) / 2 ) ) )
87 71 86 eqbrtrd ⊢ ( ( ( 𝐴 ∈ ( ℂ ∖ { 0 } ) ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ∧ ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑇 ) ) → ( ( ( abs ‘ 𝐴 ) / 2 ) + ( ( abs ‘ 𝐴 ) / 2 ) ) < ( ( abs ‘ 𝑧 ) + ( ( abs ‘ 𝐴 ) / 2 ) ) )
88 58 68 58 ltadd1d ⊢ ( ( ( 𝐴 ∈ ( ℂ ∖ { 0 } ) ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ∧ ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑇 ) ) → ( ( ( abs ‘ 𝐴 ) / 2 ) < ( abs ‘ 𝑧 ) ↔ ( ( ( abs ‘ 𝐴 ) / 2 ) + ( ( abs ‘ 𝐴 ) / 2 ) ) < ( ( abs ‘ 𝑧 ) + ( ( abs ‘ 𝐴 ) / 2 ) ) ) )
89 87 88 mpbird ⊢ ( ( ( 𝐴 ∈ ( ℂ ∖ { 0 } ) ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ∧ ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑇 ) ) → ( ( abs ‘ 𝐴 ) / 2 ) < ( abs ‘ 𝑧 ) )
90 58 68 55 89 ltmul2dd ⊢ ( ( ( 𝐴 ∈ ( ℂ ∖ { 0 } ) ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ∧ ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑇 ) ) → ( ( ( abs ‘ 𝐴 ) · 𝐵 ) · ( ( abs ‘ 𝐴 ) / 2 ) ) < ( ( ( abs ‘ 𝐴 ) · 𝐵 ) · ( abs ‘ 𝑧 ) ) )
91 16 20 absmuld ⊢ ( ( ( 𝐴 ∈ ( ℂ ∖ { 0 } ) ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ∧ ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑇 ) ) → ( abs ‘ ( 𝐴 · 𝑧 ) ) = ( ( abs ‘ 𝐴 ) · ( abs ‘ 𝑧 ) ) )
92 91 oveq1d ⊢ ( ( ( 𝐴 ∈ ( ℂ ∖ { 0 } ) ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ∧ ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑇 ) ) → ( ( abs ‘ ( 𝐴 · 𝑧 ) ) · 𝐵 ) = ( ( ( abs ‘ 𝐴 ) · ( abs ‘ 𝑧 ) ) · 𝐵 ) )
93 68 recnd ⊢ ( ( ( 𝐴 ∈ ( ℂ ∖ { 0 } ) ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ∧ ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑇 ) ) → ( abs ‘ 𝑧 ) ∈ ℂ )
94 51 recnd ⊢ ( ( ( 𝐴 ∈ ( ℂ ∖ { 0 } ) ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ∧ ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑇 ) ) → 𝐵 ∈ ℂ )
95 70 93 94 mul32d ⊢ ( ( ( 𝐴 ∈ ( ℂ ∖ { 0 } ) ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ∧ ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑇 ) ) → ( ( ( abs ‘ 𝐴 ) · ( abs ‘ 𝑧 ) ) · 𝐵 ) = ( ( ( abs ‘ 𝐴 ) · 𝐵 ) · ( abs ‘ 𝑧 ) ) )
96 92 95 eqtrd ⊢ ( ( ( 𝐴 ∈ ( ℂ ∖ { 0 } ) ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ∧ ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑇 ) ) → ( ( abs ‘ ( 𝐴 · 𝑧 ) ) · 𝐵 ) = ( ( ( abs ‘ 𝐴 ) · 𝐵 ) · ( abs ‘ 𝑧 ) ) )
97 90 96 breqtrrd ⊢ ( ( ( 𝐴 ∈ ( ℂ ∖ { 0 } ) ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ∧ ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑇 ) ) → ( ( ( abs ‘ 𝐴 ) · 𝐵 ) · ( ( abs ‘ 𝐴 ) / 2 ) ) < ( ( abs ‘ ( 𝐴 · 𝑧 ) ) · 𝐵 ) )
98 48 59 52 67 97 lelttrd ⊢ ( ( ( 𝐴 ∈ ( ℂ ∖ { 0 } ) ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ∧ ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑇 ) ) → 𝑇 < ( ( abs ‘ ( 𝐴 · 𝑧 ) ) · 𝐵 ) )
99 46 48 52 54 98 lttrd ⊢ ( ( ( 𝐴 ∈ ( ℂ ∖ { 0 } ) ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ∧ ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑇 ) ) → ( abs ‘ ( 𝐴 − 𝑧 ) ) < ( ( abs ‘ ( 𝐴 · 𝑧 ) ) · 𝐵 ) )
100 21 23 absrpcld ⊢ ( ( ( 𝐴 ∈ ( ℂ ∖ { 0 } ) ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ∧ ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑇 ) ) → ( abs ‘ ( 𝐴 · 𝑧 ) ) ∈ ℝ+ )
101 46 51 100 ltdivmuld ⊢ ( ( ( 𝐴 ∈ ( ℂ ∖ { 0 } ) ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ∧ ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑇 ) ) → ( ( ( abs ‘ ( 𝐴 − 𝑧 ) ) / ( abs ‘ ( 𝐴 · 𝑧 ) ) ) < 𝐵 ↔ ( abs ‘ ( 𝐴 − 𝑧 ) ) < ( ( abs ‘ ( 𝐴 · 𝑧 ) ) · 𝐵 ) ) )
102 99 101 mpbird ⊢ ( ( ( 𝐴 ∈ ( ℂ ∖ { 0 } ) ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ∧ ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑇 ) ) → ( ( abs ‘ ( 𝐴 − 𝑧 ) ) / ( abs ‘ ( 𝐴 · 𝑧 ) ) ) < 𝐵 )
103 42 102 eqbrtrd ⊢ ( ( ( 𝐴 ∈ ( ℂ ∖ { 0 } ) ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ∧ ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑇 ) ) → ( abs ‘ ( ( 1 / 𝑧 ) − ( 1 / 𝐴 ) ) ) < 𝐵 )
104 103 expr ⊢ ( ( ( 𝐴 ∈ ( ℂ ∖ { 0 } ) ∧ 𝐵 ∈ ℝ+ ) ∧ 𝑧 ∈ ( ℂ ∖ { 0 } ) ) → ( ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑇 → ( abs ‘ ( ( 1 / 𝑧 ) − ( 1 / 𝐴 ) ) ) < 𝐵 ) )
105 104 ralrimiva ⊢ ( ( 𝐴 ∈ ( ℂ ∖ { 0 } ) ∧ 𝐵 ∈ ℝ+ ) → ∀ 𝑧 ∈ ( ℂ ∖ { 0 } ) ( ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑇 → ( abs ‘ ( ( 1 / 𝑧 ) − ( 1 / 𝐴 ) ) ) < 𝐵 ) )
106 breq2 ⊢ ( 𝑦 = 𝑇 → ( ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑦 ↔ ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑇 ) )
107 106 rspceaimv ⊢ ( ( 𝑇 ∈ ℝ+ ∧ ∀ 𝑧 ∈ ( ℂ ∖ { 0 } ) ( ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑇 → ( abs ‘ ( ( 1 / 𝑧 ) − ( 1 / 𝐴 ) ) ) < 𝐵 ) ) → ∃ 𝑦 ∈ ℝ+ ∀ 𝑧 ∈ ( ℂ ∖ { 0 } ) ( ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑦 → ( abs ‘ ( ( 1 / 𝑧 ) − ( 1 / 𝐴 ) ) ) < 𝐵 ) )
108 14 105 107 syl2anc ⊢ ( ( 𝐴 ∈ ( ℂ ∖ { 0 } ) ∧ 𝐵 ∈ ℝ+ ) → ∃ 𝑦 ∈ ℝ+ ∀ 𝑧 ∈ ( ℂ ∖ { 0 } ) ( ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑦 → ( abs ‘ ( ( 1 / 𝑧 ) − ( 1 / 𝐴 ) ) ) < 𝐵 ) )