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