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 
|- 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 mulridd 
 |-  ( ( ( 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 mulridd 
 |-  ( ( ( 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 mullidd 
 |-  ( ( ( 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 ) )