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 / 𝐴 ) ) ) < 𝐵 ) )