Metamath Proof Explorer

Theorem irrapxlem5

Description: Lemma for irrapx1 . Switching to real intervals and fraction syntax. (Contributed by Stefan O'Rear, 13-Sep-2014)

Ref Expression
Assertion irrapxlem5 
|- ( ( A e. RR+ /\ B e. RR+ ) -> E. x e. QQ ( 0 < x /\ ( abs ` ( x - A ) ) < B /\ ( abs ` ( x - A ) ) < ( ( denom ` x ) ^ -u 2 ) ) )

Proof

Step Hyp Ref Expression
1 simpr 
 |-  ( ( A e. RR+ /\ B e. RR+ ) -> B e. RR+ )
2 1 rpreccld 
 |-  ( ( A e. RR+ /\ B e. RR+ ) -> ( 1 / B ) e. RR+ )
3 2 rprege0d 
 |-  ( ( A e. RR+ /\ B e. RR+ ) -> ( ( 1 / B ) e. RR /\ 0 <_ ( 1 / B ) ) )
4 flge0nn0 
 |-  ( ( ( 1 / B ) e. RR /\ 0 <_ ( 1 / B ) ) -> ( |_ ` ( 1 / B ) ) e. NN0 )
5 nn0p1nn 
 |-  ( ( |_ ` ( 1 / B ) ) e. NN0 -> ( ( |_ ` ( 1 / B ) ) + 1 ) e. NN )
6 3 4 5 3syl 
 |-  ( ( A e. RR+ /\ B e. RR+ ) -> ( ( |_ ` ( 1 / B ) ) + 1 ) e. NN )
7 irrapxlem4 
 |-  ( ( A e. RR+ /\ ( ( |_ ` ( 1 / B ) ) + 1 ) e. NN ) -> E. a e. NN E. b e. NN ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( a <_ ( ( |_ ` ( 1 / B ) ) + 1 ) , ( ( |_ ` ( 1 / B ) ) + 1 ) , a ) ) )
8 6 7 syldan 
 |-  ( ( A e. RR+ /\ B e. RR+ ) -> E. a e. NN E. b e. NN ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( a <_ ( ( |_ ` ( 1 / B ) ) + 1 ) , ( ( |_ ` ( 1 / B ) ) + 1 ) , a ) ) )
9 simplrr 
 |-  ( ( ( ( A e. RR+ /\ B e. RR+ ) /\ ( a e. NN /\ b e. NN ) ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( a <_ ( ( |_ ` ( 1 / B ) ) + 1 ) , ( ( |_ ` ( 1 / B ) ) + 1 ) , a ) ) ) -> b e. NN )
10 nnq 
 |-  ( b e. NN -> b e. QQ )
11 9 10 syl 
 |-  ( ( ( ( A e. RR+ /\ B e. RR+ ) /\ ( a e. NN /\ b e. NN ) ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( a <_ ( ( |_ ` ( 1 / B ) ) + 1 ) , ( ( |_ ` ( 1 / B ) ) + 1 ) , a ) ) ) -> b e. QQ )
12 simplrl 
 |-  ( ( ( ( A e. RR+ /\ B e. RR+ ) /\ ( a e. NN /\ b e. NN ) ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( a <_ ( ( |_ ` ( 1 / B ) ) + 1 ) , ( ( |_ ` ( 1 / B ) ) + 1 ) , a ) ) ) -> a e. NN )
13 nnq 
 |-  ( a e. NN -> a e. QQ )
14 12 13 syl 
 |-  ( ( ( ( A e. RR+ /\ B e. RR+ ) /\ ( a e. NN /\ b e. NN ) ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( a <_ ( ( |_ ` ( 1 / B ) ) + 1 ) , ( ( |_ ` ( 1 / B ) ) + 1 ) , a ) ) ) -> a e. QQ )
15 12 nnne0d 
 |-  ( ( ( ( A e. RR+ /\ B e. RR+ ) /\ ( a e. NN /\ b e. NN ) ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( a <_ ( ( |_ ` ( 1 / B ) ) + 1 ) , ( ( |_ ` ( 1 / B ) ) + 1 ) , a ) ) ) -> a =/= 0 )
16 qdivcl 
 |-  ( ( b e. QQ /\ a e. QQ /\ a =/= 0 ) -> ( b / a ) e. QQ )
17 11 14 15 16 syl3anc 
 |-  ( ( ( ( A e. RR+ /\ B e. RR+ ) /\ ( a e. NN /\ b e. NN ) ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( a <_ ( ( |_ ` ( 1 / B ) ) + 1 ) , ( ( |_ ` ( 1 / B ) ) + 1 ) , a ) ) ) -> ( b / a ) e. QQ )
18 9 nnrpd 
 |-  ( ( ( ( A e. RR+ /\ B e. RR+ ) /\ ( a e. NN /\ b e. NN ) ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( a <_ ( ( |_ ` ( 1 / B ) ) + 1 ) , ( ( |_ ` ( 1 / B ) ) + 1 ) , a ) ) ) -> b e. RR+ )
19 12 nnrpd 
 |-  ( ( ( ( A e. RR+ /\ B e. RR+ ) /\ ( a e. NN /\ b e. NN ) ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( a <_ ( ( |_ ` ( 1 / B ) ) + 1 ) , ( ( |_ ` ( 1 / B ) ) + 1 ) , a ) ) ) -> a e. RR+ )
20 18 19 rpdivcld 
 |-  ( ( ( ( A e. RR+ /\ B e. RR+ ) /\ ( a e. NN /\ b e. NN ) ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( a <_ ( ( |_ ` ( 1 / B ) ) + 1 ) , ( ( |_ ` ( 1 / B ) ) + 1 ) , a ) ) ) -> ( b / a ) e. RR+ )
21 20 rpgt0d 
 |-  ( ( ( ( A e. RR+ /\ B e. RR+ ) /\ ( a e. NN /\ b e. NN ) ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( a <_ ( ( |_ ` ( 1 / B ) ) + 1 ) , ( ( |_ ` ( 1 / B ) ) + 1 ) , a ) ) ) -> 0 < ( b / a ) )
22 12 nnred 
 |-  ( ( ( ( A e. RR+ /\ B e. RR+ ) /\ ( a e. NN /\ b e. NN ) ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( a <_ ( ( |_ ` ( 1 / B ) ) + 1 ) , ( ( |_ ` ( 1 / B ) ) + 1 ) , a ) ) ) -> a e. RR )
23 12 nnnn0d 
 |-  ( ( ( ( A e. RR+ /\ B e. RR+ ) /\ ( a e. NN /\ b e. NN ) ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( a <_ ( ( |_ ` ( 1 / B ) ) + 1 ) , ( ( |_ ` ( 1 / B ) ) + 1 ) , a ) ) ) -> a e. NN0 )
24 23 nn0ge0d 
 |-  ( ( ( ( A e. RR+ /\ B e. RR+ ) /\ ( a e. NN /\ b e. NN ) ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( a <_ ( ( |_ ` ( 1 / B ) ) + 1 ) , ( ( |_ ` ( 1 / B ) ) + 1 ) , a ) ) ) -> 0 <_ a )
25 22 24 absidd 
 |-  ( ( ( ( A e. RR+ /\ B e. RR+ ) /\ ( a e. NN /\ b e. NN ) ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( a <_ ( ( |_ ` ( 1 / B ) ) + 1 ) , ( ( |_ ` ( 1 / B ) ) + 1 ) , a ) ) ) -> ( abs ` a ) = a )
26 25 eqcomd 
 |-  ( ( ( ( A e. RR+ /\ B e. RR+ ) /\ ( a e. NN /\ b e. NN ) ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( a <_ ( ( |_ ` ( 1 / B ) ) + 1 ) , ( ( |_ ` ( 1 / B ) ) + 1 ) , a ) ) ) -> a = ( abs ` a ) )
27 26 oveq1d 
 |-  ( ( ( ( A e. RR+ /\ B e. RR+ ) /\ ( a e. NN /\ b e. NN ) ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( a <_ ( ( |_ ` ( 1 / B ) ) + 1 ) , ( ( |_ ` ( 1 / B ) ) + 1 ) , a ) ) ) -> ( a x. ( abs ` ( ( b / a ) - A ) ) ) = ( ( abs ` a ) x. ( abs ` ( ( b / a ) - A ) ) ) )
28 12 nncnd 
 |-  ( ( ( ( A e. RR+ /\ B e. RR+ ) /\ ( a e. NN /\ b e. NN ) ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( a <_ ( ( |_ ` ( 1 / B ) ) + 1 ) , ( ( |_ ` ( 1 / B ) ) + 1 ) , a ) ) ) -> a e. CC )
29 qre 
 |-  ( ( b / a ) e. QQ -> ( b / a ) e. RR )
30 17 29 syl 
 |-  ( ( ( ( A e. RR+ /\ B e. RR+ ) /\ ( a e. NN /\ b e. NN ) ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( a <_ ( ( |_ ` ( 1 / B ) ) + 1 ) , ( ( |_ ` ( 1 / B ) ) + 1 ) , a ) ) ) -> ( b / a ) e. RR )
31 rpre 
 |-  ( A e. RR+ -> A e. RR )
32 31 ad3antrrr 
 |-  ( ( ( ( A e. RR+ /\ B e. RR+ ) /\ ( a e. NN /\ b e. NN ) ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( a <_ ( ( |_ ` ( 1 / B ) ) + 1 ) , ( ( |_ ` ( 1 / B ) ) + 1 ) , a ) ) ) -> A e. RR )
33 30 32 resubcld 
 |-  ( ( ( ( A e. RR+ /\ B e. RR+ ) /\ ( a e. NN /\ b e. NN ) ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( a <_ ( ( |_ ` ( 1 / B ) ) + 1 ) , ( ( |_ ` ( 1 / B ) ) + 1 ) , a ) ) ) -> ( ( b / a ) - A ) e. RR )
34 33 recnd 
 |-  ( ( ( ( A e. RR+ /\ B e. RR+ ) /\ ( a e. NN /\ b e. NN ) ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( a <_ ( ( |_ ` ( 1 / B ) ) + 1 ) , ( ( |_ ` ( 1 / B ) ) + 1 ) , a ) ) ) -> ( ( b / a ) - A ) e. CC )
35 28 34 absmuld 
 |-  ( ( ( ( A e. RR+ /\ B e. RR+ ) /\ ( a e. NN /\ b e. NN ) ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( a <_ ( ( |_ ` ( 1 / B ) ) + 1 ) , ( ( |_ ` ( 1 / B ) ) + 1 ) , a ) ) ) -> ( abs ` ( a x. ( ( b / a ) - A ) ) ) = ( ( abs ` a ) x. ( abs ` ( ( b / a ) - A ) ) ) )
36 27 35 eqtr4d 
 |-  ( ( ( ( A e. RR+ /\ B e. RR+ ) /\ ( a e. NN /\ b e. NN ) ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( a <_ ( ( |_ ` ( 1 / B ) ) + 1 ) , ( ( |_ ` ( 1 / B ) ) + 1 ) , a ) ) ) -> ( a x. ( abs ` ( ( b / a ) - A ) ) ) = ( abs ` ( a x. ( ( b / a ) - A ) ) ) )
37 qcn 
 |-  ( ( b / a ) e. QQ -> ( b / a ) e. CC )
38 17 37 syl 
 |-  ( ( ( ( A e. RR+ /\ B e. RR+ ) /\ ( a e. NN /\ b e. NN ) ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( a <_ ( ( |_ ` ( 1 / B ) ) + 1 ) , ( ( |_ ` ( 1 / B ) ) + 1 ) , a ) ) ) -> ( b / a ) e. CC )
39 rpcn 
 |-  ( A e. RR+ -> A e. CC )
40 39 ad3antrrr 
 |-  ( ( ( ( A e. RR+ /\ B e. RR+ ) /\ ( a e. NN /\ b e. NN ) ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( a <_ ( ( |_ ` ( 1 / B ) ) + 1 ) , ( ( |_ ` ( 1 / B ) ) + 1 ) , a ) ) ) -> A e. CC )
41 28 38 40 subdid 
 |-  ( ( ( ( A e. RR+ /\ B e. RR+ ) /\ ( a e. NN /\ b e. NN ) ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( a <_ ( ( |_ ` ( 1 / B ) ) + 1 ) , ( ( |_ ` ( 1 / B ) ) + 1 ) , a ) ) ) -> ( a x. ( ( b / a ) - A ) ) = ( ( a x. ( b / a ) ) - ( a x. A ) ) )
42 9 nncnd 
 |-  ( ( ( ( A e. RR+ /\ B e. RR+ ) /\ ( a e. NN /\ b e. NN ) ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( a <_ ( ( |_ ` ( 1 / B ) ) + 1 ) , ( ( |_ ` ( 1 / B ) ) + 1 ) , a ) ) ) -> b e. CC )
43 42 28 15 divcan2d 
 |-  ( ( ( ( A e. RR+ /\ B e. RR+ ) /\ ( a e. NN /\ b e. NN ) ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( a <_ ( ( |_ ` ( 1 / B ) ) + 1 ) , ( ( |_ ` ( 1 / B ) ) + 1 ) , a ) ) ) -> ( a x. ( b / a ) ) = b )
44 28 40 mulcomd 
 |-  ( ( ( ( A e. RR+ /\ B e. RR+ ) /\ ( a e. NN /\ b e. NN ) ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( a <_ ( ( |_ ` ( 1 / B ) ) + 1 ) , ( ( |_ ` ( 1 / B ) ) + 1 ) , a ) ) ) -> ( a x. A ) = ( A x. a ) )
45 43 44 oveq12d 
 |-  ( ( ( ( A e. RR+ /\ B e. RR+ ) /\ ( a e. NN /\ b e. NN ) ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( a <_ ( ( |_ ` ( 1 / B ) ) + 1 ) , ( ( |_ ` ( 1 / B ) ) + 1 ) , a ) ) ) -> ( ( a x. ( b / a ) ) - ( a x. A ) ) = ( b - ( A x. a ) ) )
46 41 45 eqtrd 
 |-  ( ( ( ( A e. RR+ /\ B e. RR+ ) /\ ( a e. NN /\ b e. NN ) ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( a <_ ( ( |_ ` ( 1 / B ) ) + 1 ) , ( ( |_ ` ( 1 / B ) ) + 1 ) , a ) ) ) -> ( a x. ( ( b / a ) - A ) ) = ( b - ( A x. a ) ) )
47 46 fveq2d 
 |-  ( ( ( ( A e. RR+ /\ B e. RR+ ) /\ ( a e. NN /\ b e. NN ) ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( a <_ ( ( |_ ` ( 1 / B ) ) + 1 ) , ( ( |_ ` ( 1 / B ) ) + 1 ) , a ) ) ) -> ( abs ` ( a x. ( ( b / a ) - A ) ) ) = ( abs ` ( b - ( A x. a ) ) ) )
48 32 22 remulcld 
 |-  ( ( ( ( A e. RR+ /\ B e. RR+ ) /\ ( a e. NN /\ b e. NN ) ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( a <_ ( ( |_ ` ( 1 / B ) ) + 1 ) , ( ( |_ ` ( 1 / B ) ) + 1 ) , a ) ) ) -> ( A x. a ) e. RR )
49 48 recnd 
 |-  ( ( ( ( A e. RR+ /\ B e. RR+ ) /\ ( a e. NN /\ b e. NN ) ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( a <_ ( ( |_ ` ( 1 / B ) ) + 1 ) , ( ( |_ ` ( 1 / B ) ) + 1 ) , a ) ) ) -> ( A x. a ) e. CC )
50 42 49 abssubd 
 |-  ( ( ( ( A e. RR+ /\ B e. RR+ ) /\ ( a e. NN /\ b e. NN ) ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( a <_ ( ( |_ ` ( 1 / B ) ) + 1 ) , ( ( |_ ` ( 1 / B ) ) + 1 ) , a ) ) ) -> ( abs ` ( b - ( A x. a ) ) ) = ( abs ` ( ( A x. a ) - b ) ) )
51 36 47 50 3eqtrd 
 |-  ( ( ( ( A e. RR+ /\ B e. RR+ ) /\ ( a e. NN /\ b e. NN ) ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( a <_ ( ( |_ ` ( 1 / B ) ) + 1 ) , ( ( |_ ` ( 1 / B ) ) + 1 ) , a ) ) ) -> ( a x. ( abs ` ( ( b / a ) - A ) ) ) = ( abs ` ( ( A x. a ) - b ) ) )
52 9 nnred 
 |-  ( ( ( ( A e. RR+ /\ B e. RR+ ) /\ ( a e. NN /\ b e. NN ) ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( a <_ ( ( |_ ` ( 1 / B ) ) + 1 ) , ( ( |_ ` ( 1 / B ) ) + 1 ) , a ) ) ) -> b e. RR )
53 48 52 resubcld 
 |-  ( ( ( ( A e. RR+ /\ B e. RR+ ) /\ ( a e. NN /\ b e. NN ) ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( a <_ ( ( |_ ` ( 1 / B ) ) + 1 ) , ( ( |_ ` ( 1 / B ) ) + 1 ) , a ) ) ) -> ( ( A x. a ) - b ) e. RR )
54 53 recnd 
 |-  ( ( ( ( A e. RR+ /\ B e. RR+ ) /\ ( a e. NN /\ b e. NN ) ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( a <_ ( ( |_ ` ( 1 / B ) ) + 1 ) , ( ( |_ ` ( 1 / B ) ) + 1 ) , a ) ) ) -> ( ( A x. a ) - b ) e. CC )
55 54 abscld 
 |-  ( ( ( ( A e. RR+ /\ B e. RR+ ) /\ ( a e. NN /\ b e. NN ) ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( a <_ ( ( |_ ` ( 1 / B ) ) + 1 ) , ( ( |_ ` ( 1 / B ) ) + 1 ) , a ) ) ) -> ( abs ` ( ( A x. a ) - b ) ) e. RR )
56 simpllr 
 |-  ( ( ( ( A e. RR+ /\ B e. RR+ ) /\ ( a e. NN /\ b e. NN ) ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( a <_ ( ( |_ ` ( 1 / B ) ) + 1 ) , ( ( |_ ` ( 1 / B ) ) + 1 ) , a ) ) ) -> B e. RR+ )
57 56 rprecred 
 |-  ( ( ( ( A e. RR+ /\ B e. RR+ ) /\ ( a e. NN /\ b e. NN ) ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( a <_ ( ( |_ ` ( 1 / B ) ) + 1 ) , ( ( |_ ` ( 1 / B ) ) + 1 ) , a ) ) ) -> ( 1 / B ) e. RR )
58 56 rpreccld 
 |-  ( ( ( ( A e. RR+ /\ B e. RR+ ) /\ ( a e. NN /\ b e. NN ) ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( a <_ ( ( |_ ` ( 1 / B ) ) + 1 ) , ( ( |_ ` ( 1 / B ) ) + 1 ) , a ) ) ) -> ( 1 / B ) e. RR+ )
59 58 rpge0d 
 |-  ( ( ( ( A e. RR+ /\ B e. RR+ ) /\ ( a e. NN /\ b e. NN ) ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( a <_ ( ( |_ ` ( 1 / B ) ) + 1 ) , ( ( |_ ` ( 1 / B ) ) + 1 ) , a ) ) ) -> 0 <_ ( 1 / B ) )
60 57 59 4 syl2anc 
 |-  ( ( ( ( A e. RR+ /\ B e. RR+ ) /\ ( a e. NN /\ b e. NN ) ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( a <_ ( ( |_ ` ( 1 / B ) ) + 1 ) , ( ( |_ ` ( 1 / B ) ) + 1 ) , a ) ) ) -> ( |_ ` ( 1 / B ) ) e. NN0 )
61 60 5 syl 
 |-  ( ( ( ( A e. RR+ /\ B e. RR+ ) /\ ( a e. NN /\ b e. NN ) ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( a <_ ( ( |_ ` ( 1 / B ) ) + 1 ) , ( ( |_ ` ( 1 / B ) ) + 1 ) , a ) ) ) -> ( ( |_ ` ( 1 / B ) ) + 1 ) e. NN )
62 61 nnrpd 
 |-  ( ( ( ( A e. RR+ /\ B e. RR+ ) /\ ( a e. NN /\ b e. NN ) ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( a <_ ( ( |_ ` ( 1 / B ) ) + 1 ) , ( ( |_ ` ( 1 / B ) ) + 1 ) , a ) ) ) -> ( ( |_ ` ( 1 / B ) ) + 1 ) e. RR+ )
63 62 19 ifcld 
 |-  ( ( ( ( A e. RR+ /\ B e. RR+ ) /\ ( a e. NN /\ b e. NN ) ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( a <_ ( ( |_ ` ( 1 / B ) ) + 1 ) , ( ( |_ ` ( 1 / B ) ) + 1 ) , a ) ) ) -> if ( a <_ ( ( |_ ` ( 1 / B ) ) + 1 ) , ( ( |_ ` ( 1 / B ) ) + 1 ) , a ) e. RR+ )
64 63 rprecred 
 |-  ( ( ( ( A e. RR+ /\ B e. RR+ ) /\ ( a e. NN /\ b e. NN ) ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( a <_ ( ( |_ ` ( 1 / B ) ) + 1 ) , ( ( |_ ` ( 1 / B ) ) + 1 ) , a ) ) ) -> ( 1 / if ( a <_ ( ( |_ ` ( 1 / B ) ) + 1 ) , ( ( |_ ` ( 1 / B ) ) + 1 ) , a ) ) e. RR )
65 56 rpred 
 |-  ( ( ( ( A e. RR+ /\ B e. RR+ ) /\ ( a e. NN /\ b e. NN ) ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( a <_ ( ( |_ ` ( 1 / B ) ) + 1 ) , ( ( |_ ` ( 1 / B ) ) + 1 ) , a ) ) ) -> B e. RR )
66 22 65 remulcld 
 |-  ( ( ( ( A e. RR+ /\ B e. RR+ ) /\ ( a e. NN /\ b e. NN ) ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( a <_ ( ( |_ ` ( 1 / B ) ) + 1 ) , ( ( |_ ` ( 1 / B ) ) + 1 ) , a ) ) ) -> ( a x. B ) e. RR )
67 simpr 
 |-  ( ( ( ( A e. RR+ /\ B e. RR+ ) /\ ( a e. NN /\ b e. NN ) ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( a <_ ( ( |_ ` ( 1 / B ) ) + 1 ) , ( ( |_ ` ( 1 / B ) ) + 1 ) , a ) ) ) -> ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( a <_ ( ( |_ ` ( 1 / B ) ) + 1 ) , ( ( |_ ` ( 1 / B ) ) + 1 ) , a ) ) )
68 58 rprecred 
 |-  ( ( ( ( A e. RR+ /\ B e. RR+ ) /\ ( a e. NN /\ b e. NN ) ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( a <_ ( ( |_ ` ( 1 / B ) ) + 1 ) , ( ( |_ ` ( 1 / B ) ) + 1 ) , a ) ) ) -> ( 1 / ( 1 / B ) ) e. RR )
69 61 nnred 
 |-  ( ( ( ( A e. RR+ /\ B e. RR+ ) /\ ( a e. NN /\ b e. NN ) ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( a <_ ( ( |_ ` ( 1 / B ) ) + 1 ) , ( ( |_ ` ( 1 / B ) ) + 1 ) , a ) ) ) -> ( ( |_ ` ( 1 / B ) ) + 1 ) e. RR )
70 69 22 ifcld 
 |-  ( ( ( ( A e. RR+ /\ B e. RR+ ) /\ ( a e. NN /\ b e. NN ) ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( a <_ ( ( |_ ` ( 1 / B ) ) + 1 ) , ( ( |_ ` ( 1 / B ) ) + 1 ) , a ) ) ) -> if ( a <_ ( ( |_ ` ( 1 / B ) ) + 1 ) , ( ( |_ ` ( 1 / B ) ) + 1 ) , a ) e. RR )
71 fllep1 
 |-  ( ( 1 / B ) e. RR -> ( 1 / B ) <_ ( ( |_ ` ( 1 / B ) ) + 1 ) )
72 57 71 syl 
 |-  ( ( ( ( A e. RR+ /\ B e. RR+ ) /\ ( a e. NN /\ b e. NN ) ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( a <_ ( ( |_ ` ( 1 / B ) ) + 1 ) , ( ( |_ ` ( 1 / B ) ) + 1 ) , a ) ) ) -> ( 1 / B ) <_ ( ( |_ ` ( 1 / B ) ) + 1 ) )
73 max2 
 |-  ( ( a e. RR /\ ( ( |_ ` ( 1 / B ) ) + 1 ) e. RR ) -> ( ( |_ ` ( 1 / B ) ) + 1 ) <_ if ( a <_ ( ( |_ ` ( 1 / B ) ) + 1 ) , ( ( |_ ` ( 1 / B ) ) + 1 ) , a ) )
74 22 69 73 syl2anc 
 |-  ( ( ( ( A e. RR+ /\ B e. RR+ ) /\ ( a e. NN /\ b e. NN ) ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( a <_ ( ( |_ ` ( 1 / B ) ) + 1 ) , ( ( |_ ` ( 1 / B ) ) + 1 ) , a ) ) ) -> ( ( |_ ` ( 1 / B ) ) + 1 ) <_ if ( a <_ ( ( |_ ` ( 1 / B ) ) + 1 ) , ( ( |_ ` ( 1 / B ) ) + 1 ) , a ) )
75 57 69 70 72 74 letrd 
 |-  ( ( ( ( A e. RR+ /\ B e. RR+ ) /\ ( a e. NN /\ b e. NN ) ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( a <_ ( ( |_ ` ( 1 / B ) ) + 1 ) , ( ( |_ ` ( 1 / B ) ) + 1 ) , a ) ) ) -> ( 1 / B ) <_ if ( a <_ ( ( |_ ` ( 1 / B ) ) + 1 ) , ( ( |_ ` ( 1 / B ) ) + 1 ) , a ) )
76 58 63 lerecd 
 |-  ( ( ( ( A e. RR+ /\ B e. RR+ ) /\ ( a e. NN /\ b e. NN ) ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( a <_ ( ( |_ ` ( 1 / B ) ) + 1 ) , ( ( |_ ` ( 1 / B ) ) + 1 ) , a ) ) ) -> ( ( 1 / B ) <_ if ( a <_ ( ( |_ ` ( 1 / B ) ) + 1 ) , ( ( |_ ` ( 1 / B ) ) + 1 ) , a ) <-> ( 1 / if ( a <_ ( ( |_ ` ( 1 / B ) ) + 1 ) , ( ( |_ ` ( 1 / B ) ) + 1 ) , a ) ) <_ ( 1 / ( 1 / B ) ) ) )
77 75 76 mpbid 
 |-  ( ( ( ( A e. RR+ /\ B e. RR+ ) /\ ( a e. NN /\ b e. NN ) ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( a <_ ( ( |_ ` ( 1 / B ) ) + 1 ) , ( ( |_ ` ( 1 / B ) ) + 1 ) , a ) ) ) -> ( 1 / if ( a <_ ( ( |_ ` ( 1 / B ) ) + 1 ) , ( ( |_ ` ( 1 / B ) ) + 1 ) , a ) ) <_ ( 1 / ( 1 / B ) ) )
78 65 recnd 
 |-  ( ( ( ( A e. RR+ /\ B e. RR+ ) /\ ( a e. NN /\ b e. NN ) ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( a <_ ( ( |_ ` ( 1 / B ) ) + 1 ) , ( ( |_ ` ( 1 / B ) ) + 1 ) , a ) ) ) -> B e. CC )
79 56 rpne0d 
 |-  ( ( ( ( A e. RR+ /\ B e. RR+ ) /\ ( a e. NN /\ b e. NN ) ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( a <_ ( ( |_ ` ( 1 / B ) ) + 1 ) , ( ( |_ ` ( 1 / B ) ) + 1 ) , a ) ) ) -> B =/= 0 )
80 78 79 recrecd 
 |-  ( ( ( ( A e. RR+ /\ B e. RR+ ) /\ ( a e. NN /\ b e. NN ) ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( a <_ ( ( |_ ` ( 1 / B ) ) + 1 ) , ( ( |_ ` ( 1 / B ) ) + 1 ) , a ) ) ) -> ( 1 / ( 1 / B ) ) = B )
81 78 mullidd 
 |-  ( ( ( ( A e. RR+ /\ B e. RR+ ) /\ ( a e. NN /\ b e. NN ) ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( a <_ ( ( |_ ` ( 1 / B ) ) + 1 ) , ( ( |_ ` ( 1 / B ) ) + 1 ) , a ) ) ) -> ( 1 x. B ) = B )
82 80 81 eqtr4d 
 |-  ( ( ( ( A e. RR+ /\ B e. RR+ ) /\ ( a e. NN /\ b e. NN ) ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( a <_ ( ( |_ ` ( 1 / B ) ) + 1 ) , ( ( |_ ` ( 1 / B ) ) + 1 ) , a ) ) ) -> ( 1 / ( 1 / B ) ) = ( 1 x. B ) )
83 12 nnge1d 
 |-  ( ( ( ( A e. RR+ /\ B e. RR+ ) /\ ( a e. NN /\ b e. NN ) ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( a <_ ( ( |_ ` ( 1 / B ) ) + 1 ) , ( ( |_ ` ( 1 / B ) ) + 1 ) , a ) ) ) -> 1 <_ a )
84 1red 
 |-  ( ( ( ( A e. RR+ /\ B e. RR+ ) /\ ( a e. NN /\ b e. NN ) ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( a <_ ( ( |_ ` ( 1 / B ) ) + 1 ) , ( ( |_ ` ( 1 / B ) ) + 1 ) , a ) ) ) -> 1 e. RR )
85 84 22 56 lemul1d 
 |-  ( ( ( ( A e. RR+ /\ B e. RR+ ) /\ ( a e. NN /\ b e. NN ) ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( a <_ ( ( |_ ` ( 1 / B ) ) + 1 ) , ( ( |_ ` ( 1 / B ) ) + 1 ) , a ) ) ) -> ( 1 <_ a <-> ( 1 x. B ) <_ ( a x. B ) ) )
86 83 85 mpbid 
 |-  ( ( ( ( A e. RR+ /\ B e. RR+ ) /\ ( a e. NN /\ b e. NN ) ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( a <_ ( ( |_ ` ( 1 / B ) ) + 1 ) , ( ( |_ ` ( 1 / B ) ) + 1 ) , a ) ) ) -> ( 1 x. B ) <_ ( a x. B ) )
87 82 86 eqbrtrd 
 |-  ( ( ( ( A e. RR+ /\ B e. RR+ ) /\ ( a e. NN /\ b e. NN ) ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( a <_ ( ( |_ ` ( 1 / B ) ) + 1 ) , ( ( |_ ` ( 1 / B ) ) + 1 ) , a ) ) ) -> ( 1 / ( 1 / B ) ) <_ ( a x. B ) )
88 64 68 66 77 87 letrd 
 |-  ( ( ( ( A e. RR+ /\ B e. RR+ ) /\ ( a e. NN /\ b e. NN ) ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( a <_ ( ( |_ ` ( 1 / B ) ) + 1 ) , ( ( |_ ` ( 1 / B ) ) + 1 ) , a ) ) ) -> ( 1 / if ( a <_ ( ( |_ ` ( 1 / B ) ) + 1 ) , ( ( |_ ` ( 1 / B ) ) + 1 ) , a ) ) <_ ( a x. B ) )
89 55 64 66 67 88 ltletrd 
 |-  ( ( ( ( A e. RR+ /\ B e. RR+ ) /\ ( a e. NN /\ b e. NN ) ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( a <_ ( ( |_ ` ( 1 / B ) ) + 1 ) , ( ( |_ ` ( 1 / B ) ) + 1 ) , a ) ) ) -> ( abs ` ( ( A x. a ) - b ) ) < ( a x. B ) )
90 51 89 eqbrtrd 
 |-  ( ( ( ( A e. RR+ /\ B e. RR+ ) /\ ( a e. NN /\ b e. NN ) ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( a <_ ( ( |_ ` ( 1 / B ) ) + 1 ) , ( ( |_ ` ( 1 / B ) ) + 1 ) , a ) ) ) -> ( a x. ( abs ` ( ( b / a ) - A ) ) ) < ( a x. B ) )
91 34 abscld 
 |-  ( ( ( ( A e. RR+ /\ B e. RR+ ) /\ ( a e. NN /\ b e. NN ) ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( a <_ ( ( |_ ` ( 1 / B ) ) + 1 ) , ( ( |_ ` ( 1 / B ) ) + 1 ) , a ) ) ) -> ( abs ` ( ( b / a ) - A ) ) e. RR )
92 12 nngt0d 
 |-  ( ( ( ( A e. RR+ /\ B e. RR+ ) /\ ( a e. NN /\ b e. NN ) ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( a <_ ( ( |_ ` ( 1 / B ) ) + 1 ) , ( ( |_ ` ( 1 / B ) ) + 1 ) , a ) ) ) -> 0 < a )
93 ltmul2 
 |-  ( ( ( abs ` ( ( b / a ) - A ) ) e. RR /\ B e. RR /\ ( a e. RR /\ 0 < a ) ) -> ( ( abs ` ( ( b / a ) - A ) ) < B <-> ( a x. ( abs ` ( ( b / a ) - A ) ) ) < ( a x. B ) ) )
94 91 65 22 92 93 syl112anc 
 |-  ( ( ( ( A e. RR+ /\ B e. RR+ ) /\ ( a e. NN /\ b e. NN ) ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( a <_ ( ( |_ ` ( 1 / B ) ) + 1 ) , ( ( |_ ` ( 1 / B ) ) + 1 ) , a ) ) ) -> ( ( abs ` ( ( b / a ) - A ) ) < B <-> ( a x. ( abs ` ( ( b / a ) - A ) ) ) < ( a x. B ) ) )
95 90 94 mpbird 
 |-  ( ( ( ( A e. RR+ /\ B e. RR+ ) /\ ( a e. NN /\ b e. NN ) ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( a <_ ( ( |_ ` ( 1 / B ) ) + 1 ) , ( ( |_ ` ( 1 / B ) ) + 1 ) , a ) ) ) -> ( abs ` ( ( b / a ) - A ) ) < B )
96 22 22 remulcld 
 |-  ( ( ( ( A e. RR+ /\ B e. RR+ ) /\ ( a e. NN /\ b e. NN ) ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( a <_ ( ( |_ ` ( 1 / B ) ) + 1 ) , ( ( |_ ` ( 1 / B ) ) + 1 ) , a ) ) ) -> ( a x. a ) e. RR )
97 22 15 msqgt0d 
 |-  ( ( ( ( A e. RR+ /\ B e. RR+ ) /\ ( a e. NN /\ b e. NN ) ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( a <_ ( ( |_ ` ( 1 / B ) ) + 1 ) , ( ( |_ ` ( 1 / B ) ) + 1 ) , a ) ) ) -> 0 < ( a x. a ) )
98 97 gt0ne0d 
 |-  ( ( ( ( A e. RR+ /\ B e. RR+ ) /\ ( a e. NN /\ b e. NN ) ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( a <_ ( ( |_ ` ( 1 / B ) ) + 1 ) , ( ( |_ ` ( 1 / B ) ) + 1 ) , a ) ) ) -> ( a x. a ) =/= 0 )
99 96 98 rereccld 
 |-  ( ( ( ( A e. RR+ /\ B e. RR+ ) /\ ( a e. NN /\ b e. NN ) ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( a <_ ( ( |_ ` ( 1 / B ) ) + 1 ) , ( ( |_ ` ( 1 / B ) ) + 1 ) , a ) ) ) -> ( 1 / ( a x. a ) ) e. RR )
100 qdencl 
 |-  ( ( b / a ) e. QQ -> ( denom ` ( b / a ) ) e. NN )
101 17 100 syl 
 |-  ( ( ( ( A e. RR+ /\ B e. RR+ ) /\ ( a e. NN /\ b e. NN ) ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( a <_ ( ( |_ ` ( 1 / B ) ) + 1 ) , ( ( |_ ` ( 1 / B ) ) + 1 ) , a ) ) ) -> ( denom ` ( b / a ) ) e. NN )
102 101 nnred 
 |-  ( ( ( ( A e. RR+ /\ B e. RR+ ) /\ ( a e. NN /\ b e. NN ) ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( a <_ ( ( |_ ` ( 1 / B ) ) + 1 ) , ( ( |_ ` ( 1 / B ) ) + 1 ) , a ) ) ) -> ( denom ` ( b / a ) ) e. RR )
103 102 102 remulcld 
 |-  ( ( ( ( A e. RR+ /\ B e. RR+ ) /\ ( a e. NN /\ b e. NN ) ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( a <_ ( ( |_ ` ( 1 / B ) ) + 1 ) , ( ( |_ ` ( 1 / B ) ) + 1 ) , a ) ) ) -> ( ( denom ` ( b / a ) ) x. ( denom ` ( b / a ) ) ) e. RR )
104 101 nnne0d 
 |-  ( ( ( ( A e. RR+ /\ B e. RR+ ) /\ ( a e. NN /\ b e. NN ) ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( a <_ ( ( |_ ` ( 1 / B ) ) + 1 ) , ( ( |_ ` ( 1 / B ) ) + 1 ) , a ) ) ) -> ( denom ` ( b / a ) ) =/= 0 )
105 102 104 msqgt0d 
 |-  ( ( ( ( A e. RR+ /\ B e. RR+ ) /\ ( a e. NN /\ b e. NN ) ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( a <_ ( ( |_ ` ( 1 / B ) ) + 1 ) , ( ( |_ ` ( 1 / B ) ) + 1 ) , a ) ) ) -> 0 < ( ( denom ` ( b / a ) ) x. ( denom ` ( b / a ) ) ) )
106 105 gt0ne0d 
 |-  ( ( ( ( A e. RR+ /\ B e. RR+ ) /\ ( a e. NN /\ b e. NN ) ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( a <_ ( ( |_ ` ( 1 / B ) ) + 1 ) , ( ( |_ ` ( 1 / B ) ) + 1 ) , a ) ) ) -> ( ( denom ` ( b / a ) ) x. ( denom ` ( b / a ) ) ) =/= 0 )
107 103 106 rereccld 
 |-  ( ( ( ( A e. RR+ /\ B e. RR+ ) /\ ( a e. NN /\ b e. NN ) ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( a <_ ( ( |_ ` ( 1 / B ) ) + 1 ) , ( ( |_ ` ( 1 / B ) ) + 1 ) , a ) ) ) -> ( 1 / ( ( denom ` ( b / a ) ) x. ( denom ` ( b / a ) ) ) ) e. RR )
108 22 15 rereccld 
 |-  ( ( ( ( A e. RR+ /\ B e. RR+ ) /\ ( a e. NN /\ b e. NN ) ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( a <_ ( ( |_ ` ( 1 / B ) ) + 1 ) , ( ( |_ ` ( 1 / B ) ) + 1 ) , a ) ) ) -> ( 1 / a ) e. RR )
109 max1 
 |-  ( ( a e. RR /\ ( ( |_ ` ( 1 / B ) ) + 1 ) e. RR ) -> a <_ if ( a <_ ( ( |_ ` ( 1 / B ) ) + 1 ) , ( ( |_ ` ( 1 / B ) ) + 1 ) , a ) )
110 22 69 109 syl2anc 
 |-  ( ( ( ( A e. RR+ /\ B e. RR+ ) /\ ( a e. NN /\ b e. NN ) ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( a <_ ( ( |_ ` ( 1 / B ) ) + 1 ) , ( ( |_ ` ( 1 / B ) ) + 1 ) , a ) ) ) -> a <_ if ( a <_ ( ( |_ ` ( 1 / B ) ) + 1 ) , ( ( |_ ` ( 1 / B ) ) + 1 ) , a ) )
111 19 63 lerecd 
 |-  ( ( ( ( A e. RR+ /\ B e. RR+ ) /\ ( a e. NN /\ b e. NN ) ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( a <_ ( ( |_ ` ( 1 / B ) ) + 1 ) , ( ( |_ ` ( 1 / B ) ) + 1 ) , a ) ) ) -> ( a <_ if ( a <_ ( ( |_ ` ( 1 / B ) ) + 1 ) , ( ( |_ ` ( 1 / B ) ) + 1 ) , a ) <-> ( 1 / if ( a <_ ( ( |_ ` ( 1 / B ) ) + 1 ) , ( ( |_ ` ( 1 / B ) ) + 1 ) , a ) ) <_ ( 1 / a ) ) )
112 110 111 mpbid 
 |-  ( ( ( ( A e. RR+ /\ B e. RR+ ) /\ ( a e. NN /\ b e. NN ) ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( a <_ ( ( |_ ` ( 1 / B ) ) + 1 ) , ( ( |_ ` ( 1 / B ) ) + 1 ) , a ) ) ) -> ( 1 / if ( a <_ ( ( |_ ` ( 1 / B ) ) + 1 ) , ( ( |_ ` ( 1 / B ) ) + 1 ) , a ) ) <_ ( 1 / a ) )
113 55 64 108 67 112 ltletrd 
 |-  ( ( ( ( A e. RR+ /\ B e. RR+ ) /\ ( a e. NN /\ b e. NN ) ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( a <_ ( ( |_ ` ( 1 / B ) ) + 1 ) , ( ( |_ ` ( 1 / B ) ) + 1 ) , a ) ) ) -> ( abs ` ( ( A x. a ) - b ) ) < ( 1 / a ) )
114 28 28 28 15 15 divdiv1d 
 |-  ( ( ( ( A e. RR+ /\ B e. RR+ ) /\ ( a e. NN /\ b e. NN ) ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( a <_ ( ( |_ ` ( 1 / B ) ) + 1 ) , ( ( |_ ` ( 1 / B ) ) + 1 ) , a ) ) ) -> ( ( a / a ) / a ) = ( a / ( a x. a ) ) )
115 28 15 dividd 
 |-  ( ( ( ( A e. RR+ /\ B e. RR+ ) /\ ( a e. NN /\ b e. NN ) ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( a <_ ( ( |_ ` ( 1 / B ) ) + 1 ) , ( ( |_ ` ( 1 / B ) ) + 1 ) , a ) ) ) -> ( a / a ) = 1 )
116 115 oveq1d 
 |-  ( ( ( ( A e. RR+ /\ B e. RR+ ) /\ ( a e. NN /\ b e. NN ) ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( a <_ ( ( |_ ` ( 1 / B ) ) + 1 ) , ( ( |_ ` ( 1 / B ) ) + 1 ) , a ) ) ) -> ( ( a / a ) / a ) = ( 1 / a ) )
117 96 recnd 
 |-  ( ( ( ( A e. RR+ /\ B e. RR+ ) /\ ( a e. NN /\ b e. NN ) ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( a <_ ( ( |_ ` ( 1 / B ) ) + 1 ) , ( ( |_ ` ( 1 / B ) ) + 1 ) , a ) ) ) -> ( a x. a ) e. CC )
118 28 117 98 divrecd 
 |-  ( ( ( ( A e. RR+ /\ B e. RR+ ) /\ ( a e. NN /\ b e. NN ) ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( a <_ ( ( |_ ` ( 1 / B ) ) + 1 ) , ( ( |_ ` ( 1 / B ) ) + 1 ) , a ) ) ) -> ( a / ( a x. a ) ) = ( a x. ( 1 / ( a x. a ) ) ) )
119 114 116 118 3eqtr3rd 
 |-  ( ( ( ( A e. RR+ /\ B e. RR+ ) /\ ( a e. NN /\ b e. NN ) ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( a <_ ( ( |_ ` ( 1 / B ) ) + 1 ) , ( ( |_ ` ( 1 / B ) ) + 1 ) , a ) ) ) -> ( a x. ( 1 / ( a x. a ) ) ) = ( 1 / a ) )
120 113 51 119 3brtr4d 
 |-  ( ( ( ( A e. RR+ /\ B e. RR+ ) /\ ( a e. NN /\ b e. NN ) ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( a <_ ( ( |_ ` ( 1 / B ) ) + 1 ) , ( ( |_ ` ( 1 / B ) ) + 1 ) , a ) ) ) -> ( a x. ( abs ` ( ( b / a ) - A ) ) ) < ( a x. ( 1 / ( a x. a ) ) ) )
121 ltmul2 
 |-  ( ( ( abs ` ( ( b / a ) - A ) ) e. RR /\ ( 1 / ( a x. a ) ) e. RR /\ ( a e. RR /\ 0 < a ) ) -> ( ( abs ` ( ( b / a ) - A ) ) < ( 1 / ( a x. a ) ) <-> ( a x. ( abs ` ( ( b / a ) - A ) ) ) < ( a x. ( 1 / ( a x. a ) ) ) ) )
122 91 99 22 92 121 syl112anc 
 |-  ( ( ( ( A e. RR+ /\ B e. RR+ ) /\ ( a e. NN /\ b e. NN ) ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( a <_ ( ( |_ ` ( 1 / B ) ) + 1 ) , ( ( |_ ` ( 1 / B ) ) + 1 ) , a ) ) ) -> ( ( abs ` ( ( b / a ) - A ) ) < ( 1 / ( a x. a ) ) <-> ( a x. ( abs ` ( ( b / a ) - A ) ) ) < ( a x. ( 1 / ( a x. a ) ) ) ) )
123 120 122 mpbird 
 |-  ( ( ( ( A e. RR+ /\ B e. RR+ ) /\ ( a e. NN /\ b e. NN ) ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( a <_ ( ( |_ ` ( 1 / B ) ) + 1 ) , ( ( |_ ` ( 1 / B ) ) + 1 ) , a ) ) ) -> ( abs ` ( ( b / a ) - A ) ) < ( 1 / ( a x. a ) ) )
124 9 nnzd 
 |-  ( ( ( ( A e. RR+ /\ B e. RR+ ) /\ ( a e. NN /\ b e. NN ) ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( a <_ ( ( |_ ` ( 1 / B ) ) + 1 ) , ( ( |_ ` ( 1 / B ) ) + 1 ) , a ) ) ) -> b e. ZZ )
125 divdenle 
 |-  ( ( b e. ZZ /\ a e. NN ) -> ( denom ` ( b / a ) ) <_ a )
126 124 12 125 syl2anc 
 |-  ( ( ( ( A e. RR+ /\ B e. RR+ ) /\ ( a e. NN /\ b e. NN ) ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( a <_ ( ( |_ ` ( 1 / B ) ) + 1 ) , ( ( |_ ` ( 1 / B ) ) + 1 ) , a ) ) ) -> ( denom ` ( b / a ) ) <_ a )
127 101 nnnn0d 
 |-  ( ( ( ( A e. RR+ /\ B e. RR+ ) /\ ( a e. NN /\ b e. NN ) ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( a <_ ( ( |_ ` ( 1 / B ) ) + 1 ) , ( ( |_ ` ( 1 / B ) ) + 1 ) , a ) ) ) -> ( denom ` ( b / a ) ) e. NN0 )
128 127 nn0ge0d 
 |-  ( ( ( ( A e. RR+ /\ B e. RR+ ) /\ ( a e. NN /\ b e. NN ) ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( a <_ ( ( |_ ` ( 1 / B ) ) + 1 ) , ( ( |_ ` ( 1 / B ) ) + 1 ) , a ) ) ) -> 0 <_ ( denom ` ( b / a ) ) )
129 le2msq 
 |-  ( ( ( ( denom ` ( b / a ) ) e. RR /\ 0 <_ ( denom ` ( b / a ) ) ) /\ ( a e. RR /\ 0 <_ a ) ) -> ( ( denom ` ( b / a ) ) <_ a <-> ( ( denom ` ( b / a ) ) x. ( denom ` ( b / a ) ) ) <_ ( a x. a ) ) )
130 102 128 22 24 129 syl22anc 
 |-  ( ( ( ( A e. RR+ /\ B e. RR+ ) /\ ( a e. NN /\ b e. NN ) ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( a <_ ( ( |_ ` ( 1 / B ) ) + 1 ) , ( ( |_ ` ( 1 / B ) ) + 1 ) , a ) ) ) -> ( ( denom ` ( b / a ) ) <_ a <-> ( ( denom ` ( b / a ) ) x. ( denom ` ( b / a ) ) ) <_ ( a x. a ) ) )
131 126 130 mpbid 
 |-  ( ( ( ( A e. RR+ /\ B e. RR+ ) /\ ( a e. NN /\ b e. NN ) ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( a <_ ( ( |_ ` ( 1 / B ) ) + 1 ) , ( ( |_ ` ( 1 / B ) ) + 1 ) , a ) ) ) -> ( ( denom ` ( b / a ) ) x. ( denom ` ( b / a ) ) ) <_ ( a x. a ) )
132 lerec 
 |-  ( ( ( ( ( denom ` ( b / a ) ) x. ( denom ` ( b / a ) ) ) e. RR /\ 0 < ( ( denom ` ( b / a ) ) x. ( denom ` ( b / a ) ) ) ) /\ ( ( a x. a ) e. RR /\ 0 < ( a x. a ) ) ) -> ( ( ( denom ` ( b / a ) ) x. ( denom ` ( b / a ) ) ) <_ ( a x. a ) <-> ( 1 / ( a x. a ) ) <_ ( 1 / ( ( denom ` ( b / a ) ) x. ( denom ` ( b / a ) ) ) ) ) )
133 103 105 96 97 132 syl22anc 
 |-  ( ( ( ( A e. RR+ /\ B e. RR+ ) /\ ( a e. NN /\ b e. NN ) ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( a <_ ( ( |_ ` ( 1 / B ) ) + 1 ) , ( ( |_ ` ( 1 / B ) ) + 1 ) , a ) ) ) -> ( ( ( denom ` ( b / a ) ) x. ( denom ` ( b / a ) ) ) <_ ( a x. a ) <-> ( 1 / ( a x. a ) ) <_ ( 1 / ( ( denom ` ( b / a ) ) x. ( denom ` ( b / a ) ) ) ) ) )
134 131 133 mpbid 
 |-  ( ( ( ( A e. RR+ /\ B e. RR+ ) /\ ( a e. NN /\ b e. NN ) ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( a <_ ( ( |_ ` ( 1 / B ) ) + 1 ) , ( ( |_ ` ( 1 / B ) ) + 1 ) , a ) ) ) -> ( 1 / ( a x. a ) ) <_ ( 1 / ( ( denom ` ( b / a ) ) x. ( denom ` ( b / a ) ) ) ) )
135 91 99 107 123 134 ltletrd 
 |-  ( ( ( ( A e. RR+ /\ B e. RR+ ) /\ ( a e. NN /\ b e. NN ) ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( a <_ ( ( |_ ` ( 1 / B ) ) + 1 ) , ( ( |_ ` ( 1 / B ) ) + 1 ) , a ) ) ) -> ( abs ` ( ( b / a ) - A ) ) < ( 1 / ( ( denom ` ( b / a ) ) x. ( denom ` ( b / a ) ) ) ) )
136 101 nncnd 
 |-  ( ( ( ( A e. RR+ /\ B e. RR+ ) /\ ( a e. NN /\ b e. NN ) ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( a <_ ( ( |_ ` ( 1 / B ) ) + 1 ) , ( ( |_ ` ( 1 / B ) ) + 1 ) , a ) ) ) -> ( denom ` ( b / a ) ) e. CC )
137 2nn0 
 |-  2 e. NN0
138 expneg 
 |-  ( ( ( denom ` ( b / a ) ) e. CC /\ 2 e. NN0 ) -> ( ( denom ` ( b / a ) ) ^ -u 2 ) = ( 1 / ( ( denom ` ( b / a ) ) ^ 2 ) ) )
139 136 137 138 sylancl 
 |-  ( ( ( ( A e. RR+ /\ B e. RR+ ) /\ ( a e. NN /\ b e. NN ) ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( a <_ ( ( |_ ` ( 1 / B ) ) + 1 ) , ( ( |_ ` ( 1 / B ) ) + 1 ) , a ) ) ) -> ( ( denom ` ( b / a ) ) ^ -u 2 ) = ( 1 / ( ( denom ` ( b / a ) ) ^ 2 ) ) )
140 136 sqvald 
 |-  ( ( ( ( A e. RR+ /\ B e. RR+ ) /\ ( a e. NN /\ b e. NN ) ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( a <_ ( ( |_ ` ( 1 / B ) ) + 1 ) , ( ( |_ ` ( 1 / B ) ) + 1 ) , a ) ) ) -> ( ( denom ` ( b / a ) ) ^ 2 ) = ( ( denom ` ( b / a ) ) x. ( denom ` ( b / a ) ) ) )
141 140 oveq2d 
 |-  ( ( ( ( A e. RR+ /\ B e. RR+ ) /\ ( a e. NN /\ b e. NN ) ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( a <_ ( ( |_ ` ( 1 / B ) ) + 1 ) , ( ( |_ ` ( 1 / B ) ) + 1 ) , a ) ) ) -> ( 1 / ( ( denom ` ( b / a ) ) ^ 2 ) ) = ( 1 / ( ( denom ` ( b / a ) ) x. ( denom ` ( b / a ) ) ) ) )
142 139 141 eqtrd 
 |-  ( ( ( ( A e. RR+ /\ B e. RR+ ) /\ ( a e. NN /\ b e. NN ) ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( a <_ ( ( |_ ` ( 1 / B ) ) + 1 ) , ( ( |_ ` ( 1 / B ) ) + 1 ) , a ) ) ) -> ( ( denom ` ( b / a ) ) ^ -u 2 ) = ( 1 / ( ( denom ` ( b / a ) ) x. ( denom ` ( b / a ) ) ) ) )
143 135 142 breqtrrd 
 |-  ( ( ( ( A e. RR+ /\ B e. RR+ ) /\ ( a e. NN /\ b e. NN ) ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( a <_ ( ( |_ ` ( 1 / B ) ) + 1 ) , ( ( |_ ` ( 1 / B ) ) + 1 ) , a ) ) ) -> ( abs ` ( ( b / a ) - A ) ) < ( ( denom ` ( b / a ) ) ^ -u 2 ) )
144 breq2 
 |-  ( x = ( b / a ) -> ( 0 < x <-> 0 < ( b / a ) ) )
145 fvoveq1 
 |-  ( x = ( b / a ) -> ( abs ` ( x - A ) ) = ( abs ` ( ( b / a ) - A ) ) )
146 145 breq1d 
 |-  ( x = ( b / a ) -> ( ( abs ` ( x - A ) ) < B <-> ( abs ` ( ( b / a ) - A ) ) < B ) )
147 fveq2 
 |-  ( x = ( b / a ) -> ( denom ` x ) = ( denom ` ( b / a ) ) )
148 147 oveq1d 
 |-  ( x = ( b / a ) -> ( ( denom ` x ) ^ -u 2 ) = ( ( denom ` ( b / a ) ) ^ -u 2 ) )
149 145 148 breq12d 
 |-  ( x = ( b / a ) -> ( ( abs ` ( x - A ) ) < ( ( denom ` x ) ^ -u 2 ) <-> ( abs ` ( ( b / a ) - A ) ) < ( ( denom ` ( b / a ) ) ^ -u 2 ) ) )
150 144 146 149 3anbi123d 
 |-  ( x = ( b / a ) -> ( ( 0 < x /\ ( abs ` ( x - A ) ) < B /\ ( abs ` ( x - A ) ) < ( ( denom ` x ) ^ -u 2 ) ) <-> ( 0 < ( b / a ) /\ ( abs ` ( ( b / a ) - A ) ) < B /\ ( abs ` ( ( b / a ) - A ) ) < ( ( denom ` ( b / a ) ) ^ -u 2 ) ) ) )
151 150 rspcev 
 |-  ( ( ( b / a ) e. QQ /\ ( 0 < ( b / a ) /\ ( abs ` ( ( b / a ) - A ) ) < B /\ ( abs ` ( ( b / a ) - A ) ) < ( ( denom ` ( b / a ) ) ^ -u 2 ) ) ) -> E. x e. QQ ( 0 < x /\ ( abs ` ( x - A ) ) < B /\ ( abs ` ( x - A ) ) < ( ( denom ` x ) ^ -u 2 ) ) )
152 17 21 95 143 151 syl13anc 
 |-  ( ( ( ( A e. RR+ /\ B e. RR+ ) /\ ( a e. NN /\ b e. NN ) ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( a <_ ( ( |_ ` ( 1 / B ) ) + 1 ) , ( ( |_ ` ( 1 / B ) ) + 1 ) , a ) ) ) -> E. x e. QQ ( 0 < x /\ ( abs ` ( x - A ) ) < B /\ ( abs ` ( x - A ) ) < ( ( denom ` x ) ^ -u 2 ) ) )
153 152 ex 
 |-  ( ( ( A e. RR+ /\ B e. RR+ ) /\ ( a e. NN /\ b e. NN ) ) -> ( ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( a <_ ( ( |_ ` ( 1 / B ) ) + 1 ) , ( ( |_ ` ( 1 / B ) ) + 1 ) , a ) ) -> E. x e. QQ ( 0 < x /\ ( abs ` ( x - A ) ) < B /\ ( abs ` ( x - A ) ) < ( ( denom ` x ) ^ -u 2 ) ) ) )
154 153 rexlimdvva 
 |-  ( ( A e. RR+ /\ B e. RR+ ) -> ( E. a e. NN E. b e. NN ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( a <_ ( ( |_ ` ( 1 / B ) ) + 1 ) , ( ( |_ ` ( 1 / B ) ) + 1 ) , a ) ) -> E. x e. QQ ( 0 < x /\ ( abs ` ( x - A ) ) < B /\ ( abs ` ( x - A ) ) < ( ( denom ` x ) ^ -u 2 ) ) ) )
155 8 154 mpd 
 |-  ( ( A e. RR+ /\ B e. RR+ ) -> E. x e. QQ ( 0 < x /\ ( abs ` ( x - A ) ) < B /\ ( abs ` ( x - A ) ) < ( ( denom ` x ) ^ -u 2 ) ) )