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