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
|- T = ( if ( 1 <_ ( ( abs ` A ) x. B ) , 1 , ( ( abs ` A ) x. B ) ) x. ( ( abs ` A ) / 2 ) )
Assertion reccn2
|- ( ( A e. ( CC \ { 0 } ) /\ B e. RR+ ) -> E. y e. RR+ A. z e. ( CC \ { 0 } ) ( ( abs ` ( z - A ) ) < y -> ( abs ` ( ( 1 / z ) - ( 1 / A ) ) ) < B ) )

Proof

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