Metamath Proof Explorer

Theorem aalioulem5

Description: Lemma for aaliou . (Contributed by Stefan O'Rear, 16-Nov-2014)

Ref Expression
Hypotheses aalioulem2.a 
|- N = ( deg ` F )
aalioulem2.b 
|- ( ph -> F e. ( Poly ` ZZ ) )
aalioulem2.c 
|- ( ph -> N e. NN )
aalioulem2.d 
|- ( ph -> A e. RR )
aalioulem3.e 
|- ( ph -> ( F ` A ) = 0 )
Assertion aalioulem5 
|- ( ph -> E. x e. RR+ A. p e. ZZ A. q e. NN ( ( F ` ( p / q ) ) =/= 0 -> ( A = ( p / q ) \/ ( x / ( q ^ N ) ) <_ ( abs ` ( A - ( p / q ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 aalioulem2.a 
 |-  N = ( deg ` F )
2 aalioulem2.b 
 |-  ( ph -> F e. ( Poly ` ZZ ) )
3 aalioulem2.c 
 |-  ( ph -> N e. NN )
4 aalioulem2.d 
 |-  ( ph -> A e. RR )
5 aalioulem3.e 
 |-  ( ph -> ( F ` A ) = 0 )
6 1 2 3 4 5 aalioulem4 
 |-  ( ph -> E. a e. RR+ A. p e. ZZ A. q e. NN ( ( ( F ` ( p / q ) ) =/= 0 /\ ( abs ` ( A - ( p / q ) ) ) <_ 1 ) -> ( A = ( p / q ) \/ ( a / ( q ^ N ) ) <_ ( abs ` ( A - ( p / q ) ) ) ) ) )
7 simpr 
 |-  ( ( ph /\ a e. RR+ ) -> a e. RR+ )
8 1rp 
 |-  1 e. RR+
9 ifcl 
 |-  ( ( a e. RR+ /\ 1 e. RR+ ) -> if ( a <_ 1 , a , 1 ) e. RR+ )
10 7 8 9 sylancl 
 |-  ( ( ph /\ a e. RR+ ) -> if ( a <_ 1 , a , 1 ) e. RR+ )
11 10 adantr 
 |-  ( ( ( ph /\ a e. RR+ ) /\ ( p e. ZZ /\ q e. NN ) ) -> if ( a <_ 1 , a , 1 ) e. RR+ )
12 simprr 
 |-  ( ( ( ph /\ a e. RR+ ) /\ ( p e. ZZ /\ q e. NN ) ) -> q e. NN )
13 12 nnrpd 
 |-  ( ( ( ph /\ a e. RR+ ) /\ ( p e. ZZ /\ q e. NN ) ) -> q e. RR+ )
14 3 ad2antrr 
 |-  ( ( ( ph /\ a e. RR+ ) /\ ( p e. ZZ /\ q e. NN ) ) -> N e. NN )
15 14 nnzd 
 |-  ( ( ( ph /\ a e. RR+ ) /\ ( p e. ZZ /\ q e. NN ) ) -> N e. ZZ )
16 13 15 rpexpcld 
 |-  ( ( ( ph /\ a e. RR+ ) /\ ( p e. ZZ /\ q e. NN ) ) -> ( q ^ N ) e. RR+ )
17 11 16 rpdivcld 
 |-  ( ( ( ph /\ a e. RR+ ) /\ ( p e. ZZ /\ q e. NN ) ) -> ( if ( a <_ 1 , a , 1 ) / ( q ^ N ) ) e. RR+ )
18 17 rpred 
 |-  ( ( ( ph /\ a e. RR+ ) /\ ( p e. ZZ /\ q e. NN ) ) -> ( if ( a <_ 1 , a , 1 ) / ( q ^ N ) ) e. RR )
19 1re 
 |-  1 e. RR
20 19 a1i 
 |-  ( ( ( ph /\ a e. RR+ ) /\ ( p e. ZZ /\ q e. NN ) ) -> 1 e. RR )
21 4 ad2antrr 
 |-  ( ( ( ph /\ a e. RR+ ) /\ ( p e. ZZ /\ q e. NN ) ) -> A e. RR )
22 znq 
 |-  ( ( p e. ZZ /\ q e. NN ) -> ( p / q ) e. QQ )
23 qre 
 |-  ( ( p / q ) e. QQ -> ( p / q ) e. RR )
24 22 23 syl 
 |-  ( ( p e. ZZ /\ q e. NN ) -> ( p / q ) e. RR )
25 24 adantl 
 |-  ( ( ( ph /\ a e. RR+ ) /\ ( p e. ZZ /\ q e. NN ) ) -> ( p / q ) e. RR )
26 21 25 resubcld 
 |-  ( ( ( ph /\ a e. RR+ ) /\ ( p e. ZZ /\ q e. NN ) ) -> ( A - ( p / q ) ) e. RR )
27 26 recnd 
 |-  ( ( ( ph /\ a e. RR+ ) /\ ( p e. ZZ /\ q e. NN ) ) -> ( A - ( p / q ) ) e. CC )
28 27 abscld 
 |-  ( ( ( ph /\ a e. RR+ ) /\ ( p e. ZZ /\ q e. NN ) ) -> ( abs ` ( A - ( p / q ) ) ) e. RR )
29 18 20 28 3jca 
 |-  ( ( ( ph /\ a e. RR+ ) /\ ( p e. ZZ /\ q e. NN ) ) -> ( ( if ( a <_ 1 , a , 1 ) / ( q ^ N ) ) e. RR /\ 1 e. RR /\ ( abs ` ( A - ( p / q ) ) ) e. RR ) )
30 29 adantr 
 |-  ( ( ( ( ph /\ a e. RR+ ) /\ ( p e. ZZ /\ q e. NN ) ) /\ 1 < ( abs ` ( A - ( p / q ) ) ) ) -> ( ( if ( a <_ 1 , a , 1 ) / ( q ^ N ) ) e. RR /\ 1 e. RR /\ ( abs ` ( A - ( p / q ) ) ) e. RR ) )
31 16 rprecred 
 |-  ( ( ( ph /\ a e. RR+ ) /\ ( p e. ZZ /\ q e. NN ) ) -> ( 1 / ( q ^ N ) ) e. RR )
32 11 rpred 
 |-  ( ( ( ph /\ a e. RR+ ) /\ ( p e. ZZ /\ q e. NN ) ) -> if ( a <_ 1 , a , 1 ) e. RR )
33 simplr 
 |-  ( ( ( ph /\ a e. RR+ ) /\ ( p e. ZZ /\ q e. NN ) ) -> a e. RR+ )
34 33 rpred 
 |-  ( ( ( ph /\ a e. RR+ ) /\ ( p e. ZZ /\ q e. NN ) ) -> a e. RR )
35 min2 
 |-  ( ( a e. RR /\ 1 e. RR ) -> if ( a <_ 1 , a , 1 ) <_ 1 )
36 34 19 35 sylancl 
 |-  ( ( ( ph /\ a e. RR+ ) /\ ( p e. ZZ /\ q e. NN ) ) -> if ( a <_ 1 , a , 1 ) <_ 1 )
37 32 20 16 36 lediv1dd 
 |-  ( ( ( ph /\ a e. RR+ ) /\ ( p e. ZZ /\ q e. NN ) ) -> ( if ( a <_ 1 , a , 1 ) / ( q ^ N ) ) <_ ( 1 / ( q ^ N ) ) )
38 14 nnnn0d 
 |-  ( ( ( ph /\ a e. RR+ ) /\ ( p e. ZZ /\ q e. NN ) ) -> N e. NN0 )
39 12 38 nnexpcld 
 |-  ( ( ( ph /\ a e. RR+ ) /\ ( p e. ZZ /\ q e. NN ) ) -> ( q ^ N ) e. NN )
40 1nn 
 |-  1 e. NN
41 40 a1i 
 |-  ( ( ( ph /\ a e. RR+ ) /\ ( p e. ZZ /\ q e. NN ) ) -> 1 e. NN )
42 39 41 nnmulcld 
 |-  ( ( ( ph /\ a e. RR+ ) /\ ( p e. ZZ /\ q e. NN ) ) -> ( ( q ^ N ) x. 1 ) e. NN )
43 42 nnge1d 
 |-  ( ( ( ph /\ a e. RR+ ) /\ ( p e. ZZ /\ q e. NN ) ) -> 1 <_ ( ( q ^ N ) x. 1 ) )
44 20 20 16 ledivmuld 
 |-  ( ( ( ph /\ a e. RR+ ) /\ ( p e. ZZ /\ q e. NN ) ) -> ( ( 1 / ( q ^ N ) ) <_ 1 <-> 1 <_ ( ( q ^ N ) x. 1 ) ) )
45 43 44 mpbird 
 |-  ( ( ( ph /\ a e. RR+ ) /\ ( p e. ZZ /\ q e. NN ) ) -> ( 1 / ( q ^ N ) ) <_ 1 )
46 18 31 20 37 45 letrd 
 |-  ( ( ( ph /\ a e. RR+ ) /\ ( p e. ZZ /\ q e. NN ) ) -> ( if ( a <_ 1 , a , 1 ) / ( q ^ N ) ) <_ 1 )
47 46 adantr 
 |-  ( ( ( ( ph /\ a e. RR+ ) /\ ( p e. ZZ /\ q e. NN ) ) /\ 1 < ( abs ` ( A - ( p / q ) ) ) ) -> ( if ( a <_ 1 , a , 1 ) / ( q ^ N ) ) <_ 1 )
48 ltle 
 |-  ( ( 1 e. RR /\ ( abs ` ( A - ( p / q ) ) ) e. RR ) -> ( 1 < ( abs ` ( A - ( p / q ) ) ) -> 1 <_ ( abs ` ( A - ( p / q ) ) ) ) )
49 19 28 48 sylancr 
 |-  ( ( ( ph /\ a e. RR+ ) /\ ( p e. ZZ /\ q e. NN ) ) -> ( 1 < ( abs ` ( A - ( p / q ) ) ) -> 1 <_ ( abs ` ( A - ( p / q ) ) ) ) )
50 49 imp 
 |-  ( ( ( ( ph /\ a e. RR+ ) /\ ( p e. ZZ /\ q e. NN ) ) /\ 1 < ( abs ` ( A - ( p / q ) ) ) ) -> 1 <_ ( abs ` ( A - ( p / q ) ) ) )
51 47 50 jca 
 |-  ( ( ( ( ph /\ a e. RR+ ) /\ ( p e. ZZ /\ q e. NN ) ) /\ 1 < ( abs ` ( A - ( p / q ) ) ) ) -> ( ( if ( a <_ 1 , a , 1 ) / ( q ^ N ) ) <_ 1 /\ 1 <_ ( abs ` ( A - ( p / q ) ) ) ) )
52 letr 
 |-  ( ( ( if ( a <_ 1 , a , 1 ) / ( q ^ N ) ) e. RR /\ 1 e. RR /\ ( abs ` ( A - ( p / q ) ) ) e. RR ) -> ( ( ( if ( a <_ 1 , a , 1 ) / ( q ^ N ) ) <_ 1 /\ 1 <_ ( abs ` ( A - ( p / q ) ) ) ) -> ( if ( a <_ 1 , a , 1 ) / ( q ^ N ) ) <_ ( abs ` ( A - ( p / q ) ) ) ) )
53 30 51 52 sylc 
 |-  ( ( ( ( ph /\ a e. RR+ ) /\ ( p e. ZZ /\ q e. NN ) ) /\ 1 < ( abs ` ( A - ( p / q ) ) ) ) -> ( if ( a <_ 1 , a , 1 ) / ( q ^ N ) ) <_ ( abs ` ( A - ( p / q ) ) ) )
54 53 olcd 
 |-  ( ( ( ( ph /\ a e. RR+ ) /\ ( p e. ZZ /\ q e. NN ) ) /\ 1 < ( abs ` ( A - ( p / q ) ) ) ) -> ( A = ( p / q ) \/ ( if ( a <_ 1 , a , 1 ) / ( q ^ N ) ) <_ ( abs ` ( A - ( p / q ) ) ) ) )
55 54 2a1d 
 |-  ( ( ( ( ph /\ a e. RR+ ) /\ ( p e. ZZ /\ q e. NN ) ) /\ 1 < ( abs ` ( A - ( p / q ) ) ) ) -> ( ( ( ( F ` ( p / q ) ) =/= 0 /\ ( abs ` ( A - ( p / q ) ) ) <_ 1 ) -> ( A = ( p / q ) \/ ( a / ( q ^ N ) ) <_ ( abs ` ( A - ( p / q ) ) ) ) ) -> ( ( F ` ( p / q ) ) =/= 0 -> ( A = ( p / q ) \/ ( if ( a <_ 1 , a , 1 ) / ( q ^ N ) ) <_ ( abs ` ( A - ( p / q ) ) ) ) ) ) )
56 pm3.21 
 |-  ( ( abs ` ( A - ( p / q ) ) ) <_ 1 -> ( ( F ` ( p / q ) ) =/= 0 -> ( ( F ` ( p / q ) ) =/= 0 /\ ( abs ` ( A - ( p / q ) ) ) <_ 1 ) ) )
57 56 adantl 
 |-  ( ( ( ( ph /\ a e. RR+ ) /\ ( p e. ZZ /\ q e. NN ) ) /\ ( abs ` ( A - ( p / q ) ) ) <_ 1 ) -> ( ( F ` ( p / q ) ) =/= 0 -> ( ( F ` ( p / q ) ) =/= 0 /\ ( abs ` ( A - ( p / q ) ) ) <_ 1 ) ) )
58 33 16 rpdivcld 
 |-  ( ( ( ph /\ a e. RR+ ) /\ ( p e. ZZ /\ q e. NN ) ) -> ( a / ( q ^ N ) ) e. RR+ )
59 58 rpred 
 |-  ( ( ( ph /\ a e. RR+ ) /\ ( p e. ZZ /\ q e. NN ) ) -> ( a / ( q ^ N ) ) e. RR )
60 18 59 28 3jca 
 |-  ( ( ( ph /\ a e. RR+ ) /\ ( p e. ZZ /\ q e. NN ) ) -> ( ( if ( a <_ 1 , a , 1 ) / ( q ^ N ) ) e. RR /\ ( a / ( q ^ N ) ) e. RR /\ ( abs ` ( A - ( p / q ) ) ) e. RR ) )
61 60 adantr 
 |-  ( ( ( ( ph /\ a e. RR+ ) /\ ( p e. ZZ /\ q e. NN ) ) /\ ( a / ( q ^ N ) ) <_ ( abs ` ( A - ( p / q ) ) ) ) -> ( ( if ( a <_ 1 , a , 1 ) / ( q ^ N ) ) e. RR /\ ( a / ( q ^ N ) ) e. RR /\ ( abs ` ( A - ( p / q ) ) ) e. RR ) )
62 min1 
 |-  ( ( a e. RR /\ 1 e. RR ) -> if ( a <_ 1 , a , 1 ) <_ a )
63 34 19 62 sylancl 
 |-  ( ( ( ph /\ a e. RR+ ) /\ ( p e. ZZ /\ q e. NN ) ) -> if ( a <_ 1 , a , 1 ) <_ a )
64 32 34 16 63 lediv1dd 
 |-  ( ( ( ph /\ a e. RR+ ) /\ ( p e. ZZ /\ q e. NN ) ) -> ( if ( a <_ 1 , a , 1 ) / ( q ^ N ) ) <_ ( a / ( q ^ N ) ) )
65 64 anim1i 
 |-  ( ( ( ( ph /\ a e. RR+ ) /\ ( p e. ZZ /\ q e. NN ) ) /\ ( a / ( q ^ N ) ) <_ ( abs ` ( A - ( p / q ) ) ) ) -> ( ( if ( a <_ 1 , a , 1 ) / ( q ^ N ) ) <_ ( a / ( q ^ N ) ) /\ ( a / ( q ^ N ) ) <_ ( abs ` ( A - ( p / q ) ) ) ) )
66 letr 
 |-  ( ( ( if ( a <_ 1 , a , 1 ) / ( q ^ N ) ) e. RR /\ ( a / ( q ^ N ) ) e. RR /\ ( abs ` ( A - ( p / q ) ) ) e. RR ) -> ( ( ( if ( a <_ 1 , a , 1 ) / ( q ^ N ) ) <_ ( a / ( q ^ N ) ) /\ ( a / ( q ^ N ) ) <_ ( abs ` ( A - ( p / q ) ) ) ) -> ( if ( a <_ 1 , a , 1 ) / ( q ^ N ) ) <_ ( abs ` ( A - ( p / q ) ) ) ) )
67 61 65 66 sylc 
 |-  ( ( ( ( ph /\ a e. RR+ ) /\ ( p e. ZZ /\ q e. NN ) ) /\ ( a / ( q ^ N ) ) <_ ( abs ` ( A - ( p / q ) ) ) ) -> ( if ( a <_ 1 , a , 1 ) / ( q ^ N ) ) <_ ( abs ` ( A - ( p / q ) ) ) )
68 67 ex 
 |-  ( ( ( ph /\ a e. RR+ ) /\ ( p e. ZZ /\ q e. NN ) ) -> ( ( a / ( q ^ N ) ) <_ ( abs ` ( A - ( p / q ) ) ) -> ( if ( a <_ 1 , a , 1 ) / ( q ^ N ) ) <_ ( abs ` ( A - ( p / q ) ) ) ) )
69 68 adantr 
 |-  ( ( ( ( ph /\ a e. RR+ ) /\ ( p e. ZZ /\ q e. NN ) ) /\ ( abs ` ( A - ( p / q ) ) ) <_ 1 ) -> ( ( a / ( q ^ N ) ) <_ ( abs ` ( A - ( p / q ) ) ) -> ( if ( a <_ 1 , a , 1 ) / ( q ^ N ) ) <_ ( abs ` ( A - ( p / q ) ) ) ) )
70 69 orim2d 
 |-  ( ( ( ( ph /\ a e. RR+ ) /\ ( p e. ZZ /\ q e. NN ) ) /\ ( abs ` ( A - ( p / q ) ) ) <_ 1 ) -> ( ( A = ( p / q ) \/ ( a / ( q ^ N ) ) <_ ( abs ` ( A - ( p / q ) ) ) ) -> ( A = ( p / q ) \/ ( if ( a <_ 1 , a , 1 ) / ( q ^ N ) ) <_ ( abs ` ( A - ( p / q ) ) ) ) ) )
71 57 70 imim12d 
 |-  ( ( ( ( ph /\ a e. RR+ ) /\ ( p e. ZZ /\ q e. NN ) ) /\ ( abs ` ( A - ( p / q ) ) ) <_ 1 ) -> ( ( ( ( F ` ( p / q ) ) =/= 0 /\ ( abs ` ( A - ( p / q ) ) ) <_ 1 ) -> ( A = ( p / q ) \/ ( a / ( q ^ N ) ) <_ ( abs ` ( A - ( p / q ) ) ) ) ) -> ( ( F ` ( p / q ) ) =/= 0 -> ( A = ( p / q ) \/ ( if ( a <_ 1 , a , 1 ) / ( q ^ N ) ) <_ ( abs ` ( A - ( p / q ) ) ) ) ) ) )
72 55 71 20 28 ltlecasei 
 |-  ( ( ( ph /\ a e. RR+ ) /\ ( p e. ZZ /\ q e. NN ) ) -> ( ( ( ( F ` ( p / q ) ) =/= 0 /\ ( abs ` ( A - ( p / q ) ) ) <_ 1 ) -> ( A = ( p / q ) \/ ( a / ( q ^ N ) ) <_ ( abs ` ( A - ( p / q ) ) ) ) ) -> ( ( F ` ( p / q ) ) =/= 0 -> ( A = ( p / q ) \/ ( if ( a <_ 1 , a , 1 ) / ( q ^ N ) ) <_ ( abs ` ( A - ( p / q ) ) ) ) ) ) )
73 72 ralimdvva 
 |-  ( ( ph /\ a e. RR+ ) -> ( A. p e. ZZ A. q e. NN ( ( ( F ` ( p / q ) ) =/= 0 /\ ( abs ` ( A - ( p / q ) ) ) <_ 1 ) -> ( A = ( p / q ) \/ ( a / ( q ^ N ) ) <_ ( abs ` ( A - ( p / q ) ) ) ) ) -> A. p e. ZZ A. q e. NN ( ( F ` ( p / q ) ) =/= 0 -> ( A = ( p / q ) \/ ( if ( a <_ 1 , a , 1 ) / ( q ^ N ) ) <_ ( abs ` ( A - ( p / q ) ) ) ) ) ) )
74 oveq1 
 |-  ( x = if ( a <_ 1 , a , 1 ) -> ( x / ( q ^ N ) ) = ( if ( a <_ 1 , a , 1 ) / ( q ^ N ) ) )
75 74 breq1d 
 |-  ( x = if ( a <_ 1 , a , 1 ) -> ( ( x / ( q ^ N ) ) <_ ( abs ` ( A - ( p / q ) ) ) <-> ( if ( a <_ 1 , a , 1 ) / ( q ^ N ) ) <_ ( abs ` ( A - ( p / q ) ) ) ) )
76 75 orbi2d 
 |-  ( x = if ( a <_ 1 , a , 1 ) -> ( ( A = ( p / q ) \/ ( x / ( q ^ N ) ) <_ ( abs ` ( A - ( p / q ) ) ) ) <-> ( A = ( p / q ) \/ ( if ( a <_ 1 , a , 1 ) / ( q ^ N ) ) <_ ( abs ` ( A - ( p / q ) ) ) ) ) )
77 76 imbi2d 
 |-  ( x = if ( a <_ 1 , a , 1 ) -> ( ( ( F ` ( p / q ) ) =/= 0 -> ( A = ( p / q ) \/ ( x / ( q ^ N ) ) <_ ( abs ` ( A - ( p / q ) ) ) ) ) <-> ( ( F ` ( p / q ) ) =/= 0 -> ( A = ( p / q ) \/ ( if ( a <_ 1 , a , 1 ) / ( q ^ N ) ) <_ ( abs ` ( A - ( p / q ) ) ) ) ) ) )
78 77 2ralbidv 
 |-  ( x = if ( a <_ 1 , a , 1 ) -> ( A. p e. ZZ A. q e. NN ( ( F ` ( p / q ) ) =/= 0 -> ( A = ( p / q ) \/ ( x / ( q ^ N ) ) <_ ( abs ` ( A - ( p / q ) ) ) ) ) <-> A. p e. ZZ A. q e. NN ( ( F ` ( p / q ) ) =/= 0 -> ( A = ( p / q ) \/ ( if ( a <_ 1 , a , 1 ) / ( q ^ N ) ) <_ ( abs ` ( A - ( p / q ) ) ) ) ) ) )
79 78 rspcev 
 |-  ( ( if ( a <_ 1 , a , 1 ) e. RR+ /\ A. p e. ZZ A. q e. NN ( ( F ` ( p / q ) ) =/= 0 -> ( A = ( p / q ) \/ ( if ( a <_ 1 , a , 1 ) / ( q ^ N ) ) <_ ( abs ` ( A - ( p / q ) ) ) ) ) ) -> E. x e. RR+ A. p e. ZZ A. q e. NN ( ( F ` ( p / q ) ) =/= 0 -> ( A = ( p / q ) \/ ( x / ( q ^ N ) ) <_ ( abs ` ( A - ( p / q ) ) ) ) ) )
80 10 73 79 syl6an 
 |-  ( ( ph /\ a e. RR+ ) -> ( A. p e. ZZ A. q e. NN ( ( ( F ` ( p / q ) ) =/= 0 /\ ( abs ` ( A - ( p / q ) ) ) <_ 1 ) -> ( A = ( p / q ) \/ ( a / ( q ^ N ) ) <_ ( abs ` ( A - ( p / q ) ) ) ) ) -> E. x e. RR+ A. p e. ZZ A. q e. NN ( ( F ` ( p / q ) ) =/= 0 -> ( A = ( p / q ) \/ ( x / ( q ^ N ) ) <_ ( abs ` ( A - ( p / q ) ) ) ) ) ) )
81 80 rexlimdva 
 |-  ( ph -> ( E. a e. RR+ A. p e. ZZ A. q e. NN ( ( ( F ` ( p / q ) ) =/= 0 /\ ( abs ` ( A - ( p / q ) ) ) <_ 1 ) -> ( A = ( p / q ) \/ ( a / ( q ^ N ) ) <_ ( abs ` ( A - ( p / q ) ) ) ) ) -> E. x e. RR+ A. p e. ZZ A. q e. NN ( ( F ` ( p / q ) ) =/= 0 -> ( A = ( p / q ) \/ ( x / ( q ^ N ) ) <_ ( abs ` ( A - ( p / q ) ) ) ) ) ) )
82 6 81 mpd 
 |-  ( ph -> E. x e. RR+ A. p e. ZZ A. q e. NN ( ( F ` ( p / q ) ) =/= 0 -> ( A = ( p / q ) \/ ( x / ( q ^ N ) ) <_ ( abs ` ( A - ( p / q ) ) ) ) ) )