Metamath Proof Explorer

Theorem aalioulem4

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 aalioulem4 
|- ( ph -> E. x e. RR+ A. p e. ZZ A. q e. NN ( ( ( F ` ( p / q ) ) =/= 0 /\ ( abs ` ( A - ( p / q ) ) ) <_ 1 ) -> ( 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 aalioulem3 
 |-  ( ph -> E. x e. RR+ A. a e. RR ( ( abs ` ( A - a ) ) <_ 1 -> ( x x. ( abs ` ( F ` a ) ) ) <_ ( abs ` ( A - a ) ) ) )
7 simp2l 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( p e. ZZ /\ q e. NN ) /\ ( ( F ` ( p / q ) ) =/= 0 /\ ( abs ` ( A - ( p / q ) ) ) <_ 1 ) ) -> p e. ZZ )
8 simp2r 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( p e. ZZ /\ q e. NN ) /\ ( ( F ` ( p / q ) ) =/= 0 /\ ( abs ` ( A - ( p / q ) ) ) <_ 1 ) ) -> q e. NN )
9 znq 
 |-  ( ( p e. ZZ /\ q e. NN ) -> ( p / q ) e. QQ )
10 7 8 9 syl2anc 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( p e. ZZ /\ q e. NN ) /\ ( ( F ` ( p / q ) ) =/= 0 /\ ( abs ` ( A - ( p / q ) ) ) <_ 1 ) ) -> ( p / q ) e. QQ )
11 qre 
 |-  ( ( p / q ) e. QQ -> ( p / q ) e. RR )
12 10 11 syl 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( p e. ZZ /\ q e. NN ) /\ ( ( F ` ( p / q ) ) =/= 0 /\ ( abs ` ( A - ( p / q ) ) ) <_ 1 ) ) -> ( p / q ) e. RR )
13 simp3r 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( p e. ZZ /\ q e. NN ) /\ ( ( F ` ( p / q ) ) =/= 0 /\ ( abs ` ( A - ( p / q ) ) ) <_ 1 ) ) -> ( abs ` ( A - ( p / q ) ) ) <_ 1 )
14 oveq2 
 |-  ( a = ( p / q ) -> ( A - a ) = ( A - ( p / q ) ) )
15 14 fveq2d 
 |-  ( a = ( p / q ) -> ( abs ` ( A - a ) ) = ( abs ` ( A - ( p / q ) ) ) )
16 15 breq1d 
 |-  ( a = ( p / q ) -> ( ( abs ` ( A - a ) ) <_ 1 <-> ( abs ` ( A - ( p / q ) ) ) <_ 1 ) )
17 2fveq3 
 |-  ( a = ( p / q ) -> ( abs ` ( F ` a ) ) = ( abs ` ( F ` ( p / q ) ) ) )
18 17 oveq2d 
 |-  ( a = ( p / q ) -> ( x x. ( abs ` ( F ` a ) ) ) = ( x x. ( abs ` ( F ` ( p / q ) ) ) ) )
19 18 15 breq12d 
 |-  ( a = ( p / q ) -> ( ( x x. ( abs ` ( F ` a ) ) ) <_ ( abs ` ( A - a ) ) <-> ( x x. ( abs ` ( F ` ( p / q ) ) ) ) <_ ( abs ` ( A - ( p / q ) ) ) ) )
20 16 19 imbi12d 
 |-  ( a = ( p / q ) -> ( ( ( abs ` ( A - a ) ) <_ 1 -> ( x x. ( abs ` ( F ` a ) ) ) <_ ( abs ` ( A - a ) ) ) <-> ( ( abs ` ( A - ( p / q ) ) ) <_ 1 -> ( x x. ( abs ` ( F ` ( p / q ) ) ) ) <_ ( abs ` ( A - ( p / q ) ) ) ) ) )
21 20 rspcv 
 |-  ( ( p / q ) e. RR -> ( A. a e. RR ( ( abs ` ( A - a ) ) <_ 1 -> ( x x. ( abs ` ( F ` a ) ) ) <_ ( abs ` ( A - a ) ) ) -> ( ( abs ` ( A - ( p / q ) ) ) <_ 1 -> ( x x. ( abs ` ( F ` ( p / q ) ) ) ) <_ ( abs ` ( A - ( p / q ) ) ) ) ) )
22 21 com23 
 |-  ( ( p / q ) e. RR -> ( ( abs ` ( A - ( p / q ) ) ) <_ 1 -> ( A. a e. RR ( ( abs ` ( A - a ) ) <_ 1 -> ( x x. ( abs ` ( F ` a ) ) ) <_ ( abs ` ( A - a ) ) ) -> ( x x. ( abs ` ( F ` ( p / q ) ) ) ) <_ ( abs ` ( A - ( p / q ) ) ) ) ) )
23 12 13 22 sylc 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( p e. ZZ /\ q e. NN ) /\ ( ( F ` ( p / q ) ) =/= 0 /\ ( abs ` ( A - ( p / q ) ) ) <_ 1 ) ) -> ( A. a e. RR ( ( abs ` ( A - a ) ) <_ 1 -> ( x x. ( abs ` ( F ` a ) ) ) <_ ( abs ` ( A - a ) ) ) -> ( x x. ( abs ` ( F ` ( p / q ) ) ) ) <_ ( abs ` ( A - ( p / q ) ) ) ) )
24 simp1r 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( p e. ZZ /\ q e. NN ) /\ ( ( F ` ( p / q ) ) =/= 0 /\ ( abs ` ( A - ( p / q ) ) ) <_ 1 ) ) -> x e. RR+ )
25 8 nnrpd 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( p e. ZZ /\ q e. NN ) /\ ( ( F ` ( p / q ) ) =/= 0 /\ ( abs ` ( A - ( p / q ) ) ) <_ 1 ) ) -> q e. RR+ )
26 simp1l 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( p e. ZZ /\ q e. NN ) /\ ( ( F ` ( p / q ) ) =/= 0 /\ ( abs ` ( A - ( p / q ) ) ) <_ 1 ) ) -> ph )
27 26 3 syl 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( p e. ZZ /\ q e. NN ) /\ ( ( F ` ( p / q ) ) =/= 0 /\ ( abs ` ( A - ( p / q ) ) ) <_ 1 ) ) -> N e. NN )
28 27 nnzd 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( p e. ZZ /\ q e. NN ) /\ ( ( F ` ( p / q ) ) =/= 0 /\ ( abs ` ( A - ( p / q ) ) ) <_ 1 ) ) -> N e. ZZ )
29 25 28 rpexpcld 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( p e. ZZ /\ q e. NN ) /\ ( ( F ` ( p / q ) ) =/= 0 /\ ( abs ` ( A - ( p / q ) ) ) <_ 1 ) ) -> ( q ^ N ) e. RR+ )
30 24 29 rpdivcld 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( p e. ZZ /\ q e. NN ) /\ ( ( F ` ( p / q ) ) =/= 0 /\ ( abs ` ( A - ( p / q ) ) ) <_ 1 ) ) -> ( x / ( q ^ N ) ) e. RR+ )
31 30 rpred 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( p e. ZZ /\ q e. NN ) /\ ( ( F ` ( p / q ) ) =/= 0 /\ ( abs ` ( A - ( p / q ) ) ) <_ 1 ) ) -> ( x / ( q ^ N ) ) e. RR )
32 31 adantr 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ ( p e. ZZ /\ q e. NN ) /\ ( ( F ` ( p / q ) ) =/= 0 /\ ( abs ` ( A - ( p / q ) ) ) <_ 1 ) ) /\ ( x x. ( abs ` ( F ` ( p / q ) ) ) ) <_ ( abs ` ( A - ( p / q ) ) ) ) -> ( x / ( q ^ N ) ) e. RR )
33 24 rpred 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( p e. ZZ /\ q e. NN ) /\ ( ( F ` ( p / q ) ) =/= 0 /\ ( abs ` ( A - ( p / q ) ) ) <_ 1 ) ) -> x e. RR )
34 26 2 syl 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( p e. ZZ /\ q e. NN ) /\ ( ( F ` ( p / q ) ) =/= 0 /\ ( abs ` ( A - ( p / q ) ) ) <_ 1 ) ) -> F e. ( Poly ` ZZ ) )
35 plyf 
 |-  ( F e. ( Poly ` ZZ ) -> F : CC --> CC )
36 34 35 syl 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( p e. ZZ /\ q e. NN ) /\ ( ( F ` ( p / q ) ) =/= 0 /\ ( abs ` ( A - ( p / q ) ) ) <_ 1 ) ) -> F : CC --> CC )
37 12 recnd 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( p e. ZZ /\ q e. NN ) /\ ( ( F ` ( p / q ) ) =/= 0 /\ ( abs ` ( A - ( p / q ) ) ) <_ 1 ) ) -> ( p / q ) e. CC )
38 36 37 ffvelcdmd 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( p e. ZZ /\ q e. NN ) /\ ( ( F ` ( p / q ) ) =/= 0 /\ ( abs ` ( A - ( p / q ) ) ) <_ 1 ) ) -> ( F ` ( p / q ) ) e. CC )
39 38 abscld 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( p e. ZZ /\ q e. NN ) /\ ( ( F ` ( p / q ) ) =/= 0 /\ ( abs ` ( A - ( p / q ) ) ) <_ 1 ) ) -> ( abs ` ( F ` ( p / q ) ) ) e. RR )
40 33 39 remulcld 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( p e. ZZ /\ q e. NN ) /\ ( ( F ` ( p / q ) ) =/= 0 /\ ( abs ` ( A - ( p / q ) ) ) <_ 1 ) ) -> ( x x. ( abs ` ( F ` ( p / q ) ) ) ) e. RR )
41 40 adantr 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ ( p e. ZZ /\ q e. NN ) /\ ( ( F ` ( p / q ) ) =/= 0 /\ ( abs ` ( A - ( p / q ) ) ) <_ 1 ) ) /\ ( x x. ( abs ` ( F ` ( p / q ) ) ) ) <_ ( abs ` ( A - ( p / q ) ) ) ) -> ( x x. ( abs ` ( F ` ( p / q ) ) ) ) e. RR )
42 26 4 syl 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( p e. ZZ /\ q e. NN ) /\ ( ( F ` ( p / q ) ) =/= 0 /\ ( abs ` ( A - ( p / q ) ) ) <_ 1 ) ) -> A e. RR )
43 42 12 resubcld 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( p e. ZZ /\ q e. NN ) /\ ( ( F ` ( p / q ) ) =/= 0 /\ ( abs ` ( A - ( p / q ) ) ) <_ 1 ) ) -> ( A - ( p / q ) ) e. RR )
44 43 recnd 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( p e. ZZ /\ q e. NN ) /\ ( ( F ` ( p / q ) ) =/= 0 /\ ( abs ` ( A - ( p / q ) ) ) <_ 1 ) ) -> ( A - ( p / q ) ) e. CC )
45 44 abscld 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( p e. ZZ /\ q e. NN ) /\ ( ( F ` ( p / q ) ) =/= 0 /\ ( abs ` ( A - ( p / q ) ) ) <_ 1 ) ) -> ( abs ` ( A - ( p / q ) ) ) e. RR )
46 45 adantr 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ ( p e. ZZ /\ q e. NN ) /\ ( ( F ` ( p / q ) ) =/= 0 /\ ( abs ` ( A - ( p / q ) ) ) <_ 1 ) ) /\ ( x x. ( abs ` ( F ` ( p / q ) ) ) ) <_ ( abs ` ( A - ( p / q ) ) ) ) -> ( abs ` ( A - ( p / q ) ) ) e. RR )
47 24 rpcnd 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( p e. ZZ /\ q e. NN ) /\ ( ( F ` ( p / q ) ) =/= 0 /\ ( abs ` ( A - ( p / q ) ) ) <_ 1 ) ) -> x e. CC )
48 29 rpcnd 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( p e. ZZ /\ q e. NN ) /\ ( ( F ` ( p / q ) ) =/= 0 /\ ( abs ` ( A - ( p / q ) ) ) <_ 1 ) ) -> ( q ^ N ) e. CC )
49 29 rpne0d 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( p e. ZZ /\ q e. NN ) /\ ( ( F ` ( p / q ) ) =/= 0 /\ ( abs ` ( A - ( p / q ) ) ) <_ 1 ) ) -> ( q ^ N ) =/= 0 )
50 47 48 49 divrecd 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( p e. ZZ /\ q e. NN ) /\ ( ( F ` ( p / q ) ) =/= 0 /\ ( abs ` ( A - ( p / q ) ) ) <_ 1 ) ) -> ( x / ( q ^ N ) ) = ( x x. ( 1 / ( q ^ N ) ) ) )
51 48 38 absmuld 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( p e. ZZ /\ q e. NN ) /\ ( ( F ` ( p / q ) ) =/= 0 /\ ( abs ` ( A - ( p / q ) ) ) <_ 1 ) ) -> ( abs ` ( ( q ^ N ) x. ( F ` ( p / q ) ) ) ) = ( ( abs ` ( q ^ N ) ) x. ( abs ` ( F ` ( p / q ) ) ) ) )
52 29 rpred 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( p e. ZZ /\ q e. NN ) /\ ( ( F ` ( p / q ) ) =/= 0 /\ ( abs ` ( A - ( p / q ) ) ) <_ 1 ) ) -> ( q ^ N ) e. RR )
53 29 rpge0d 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( p e. ZZ /\ q e. NN ) /\ ( ( F ` ( p / q ) ) =/= 0 /\ ( abs ` ( A - ( p / q ) ) ) <_ 1 ) ) -> 0 <_ ( q ^ N ) )
54 52 53 absidd 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( p e. ZZ /\ q e. NN ) /\ ( ( F ` ( p / q ) ) =/= 0 /\ ( abs ` ( A - ( p / q ) ) ) <_ 1 ) ) -> ( abs ` ( q ^ N ) ) = ( q ^ N ) )
55 54 oveq1d 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( p e. ZZ /\ q e. NN ) /\ ( ( F ` ( p / q ) ) =/= 0 /\ ( abs ` ( A - ( p / q ) ) ) <_ 1 ) ) -> ( ( abs ` ( q ^ N ) ) x. ( abs ` ( F ` ( p / q ) ) ) ) = ( ( q ^ N ) x. ( abs ` ( F ` ( p / q ) ) ) ) )
56 51 55 eqtrd 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( p e. ZZ /\ q e. NN ) /\ ( ( F ` ( p / q ) ) =/= 0 /\ ( abs ` ( A - ( p / q ) ) ) <_ 1 ) ) -> ( abs ` ( ( q ^ N ) x. ( F ` ( p / q ) ) ) ) = ( ( q ^ N ) x. ( abs ` ( F ` ( p / q ) ) ) ) )
57 48 38 mulcomd 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( p e. ZZ /\ q e. NN ) /\ ( ( F ` ( p / q ) ) =/= 0 /\ ( abs ` ( A - ( p / q ) ) ) <_ 1 ) ) -> ( ( q ^ N ) x. ( F ` ( p / q ) ) ) = ( ( F ` ( p / q ) ) x. ( q ^ N ) ) )
58 1 oveq2i 
 |-  ( q ^ N ) = ( q ^ ( deg ` F ) )
59 58 oveq2i 
 |-  ( ( F ` ( p / q ) ) x. ( q ^ N ) ) = ( ( F ` ( p / q ) ) x. ( q ^ ( deg ` F ) ) )
60 57 59 eqtrdi 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( p e. ZZ /\ q e. NN ) /\ ( ( F ` ( p / q ) ) =/= 0 /\ ( abs ` ( A - ( p / q ) ) ) <_ 1 ) ) -> ( ( q ^ N ) x. ( F ` ( p / q ) ) ) = ( ( F ` ( p / q ) ) x. ( q ^ ( deg ` F ) ) ) )
61 34 7 8 aalioulem1 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( p e. ZZ /\ q e. NN ) /\ ( ( F ` ( p / q ) ) =/= 0 /\ ( abs ` ( A - ( p / q ) ) ) <_ 1 ) ) -> ( ( F ` ( p / q ) ) x. ( q ^ ( deg ` F ) ) ) e. ZZ )
62 60 61 eqeltrd 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( p e. ZZ /\ q e. NN ) /\ ( ( F ` ( p / q ) ) =/= 0 /\ ( abs ` ( A - ( p / q ) ) ) <_ 1 ) ) -> ( ( q ^ N ) x. ( F ` ( p / q ) ) ) e. ZZ )
63 simp3l 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( p e. ZZ /\ q e. NN ) /\ ( ( F ` ( p / q ) ) =/= 0 /\ ( abs ` ( A - ( p / q ) ) ) <_ 1 ) ) -> ( F ` ( p / q ) ) =/= 0 )
64 48 38 49 63 mulne0d 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( p e. ZZ /\ q e. NN ) /\ ( ( F ` ( p / q ) ) =/= 0 /\ ( abs ` ( A - ( p / q ) ) ) <_ 1 ) ) -> ( ( q ^ N ) x. ( F ` ( p / q ) ) ) =/= 0 )
65 nnabscl 
 |-  ( ( ( ( q ^ N ) x. ( F ` ( p / q ) ) ) e. ZZ /\ ( ( q ^ N ) x. ( F ` ( p / q ) ) ) =/= 0 ) -> ( abs ` ( ( q ^ N ) x. ( F ` ( p / q ) ) ) ) e. NN )
66 62 64 65 syl2anc 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( p e. ZZ /\ q e. NN ) /\ ( ( F ` ( p / q ) ) =/= 0 /\ ( abs ` ( A - ( p / q ) ) ) <_ 1 ) ) -> ( abs ` ( ( q ^ N ) x. ( F ` ( p / q ) ) ) ) e. NN )
67 56 66 eqeltrrd 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( p e. ZZ /\ q e. NN ) /\ ( ( F ` ( p / q ) ) =/= 0 /\ ( abs ` ( A - ( p / q ) ) ) <_ 1 ) ) -> ( ( q ^ N ) x. ( abs ` ( F ` ( p / q ) ) ) ) e. NN )
68 67 nnge1d 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( p e. ZZ /\ q e. NN ) /\ ( ( F ` ( p / q ) ) =/= 0 /\ ( abs ` ( A - ( p / q ) ) ) <_ 1 ) ) -> 1 <_ ( ( q ^ N ) x. ( abs ` ( F ` ( p / q ) ) ) ) )
69 1red 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( p e. ZZ /\ q e. NN ) /\ ( ( F ` ( p / q ) ) =/= 0 /\ ( abs ` ( A - ( p / q ) ) ) <_ 1 ) ) -> 1 e. RR )
70 69 39 29 ledivmuld 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( p e. ZZ /\ q e. NN ) /\ ( ( F ` ( p / q ) ) =/= 0 /\ ( abs ` ( A - ( p / q ) ) ) <_ 1 ) ) -> ( ( 1 / ( q ^ N ) ) <_ ( abs ` ( F ` ( p / q ) ) ) <-> 1 <_ ( ( q ^ N ) x. ( abs ` ( F ` ( p / q ) ) ) ) ) )
71 68 70 mpbird 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( p e. ZZ /\ q e. NN ) /\ ( ( F ` ( p / q ) ) =/= 0 /\ ( abs ` ( A - ( p / q ) ) ) <_ 1 ) ) -> ( 1 / ( q ^ N ) ) <_ ( abs ` ( F ` ( p / q ) ) ) )
72 29 rprecred 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( p e. ZZ /\ q e. NN ) /\ ( ( F ` ( p / q ) ) =/= 0 /\ ( abs ` ( A - ( p / q ) ) ) <_ 1 ) ) -> ( 1 / ( q ^ N ) ) e. RR )
73 72 39 24 lemul2d 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( p e. ZZ /\ q e. NN ) /\ ( ( F ` ( p / q ) ) =/= 0 /\ ( abs ` ( A - ( p / q ) ) ) <_ 1 ) ) -> ( ( 1 / ( q ^ N ) ) <_ ( abs ` ( F ` ( p / q ) ) ) <-> ( x x. ( 1 / ( q ^ N ) ) ) <_ ( x x. ( abs ` ( F ` ( p / q ) ) ) ) ) )
74 71 73 mpbid 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( p e. ZZ /\ q e. NN ) /\ ( ( F ` ( p / q ) ) =/= 0 /\ ( abs ` ( A - ( p / q ) ) ) <_ 1 ) ) -> ( x x. ( 1 / ( q ^ N ) ) ) <_ ( x x. ( abs ` ( F ` ( p / q ) ) ) ) )
75 50 74 eqbrtrd 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( p e. ZZ /\ q e. NN ) /\ ( ( F ` ( p / q ) ) =/= 0 /\ ( abs ` ( A - ( p / q ) ) ) <_ 1 ) ) -> ( x / ( q ^ N ) ) <_ ( x x. ( abs ` ( F ` ( p / q ) ) ) ) )
76 75 adantr 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ ( p e. ZZ /\ q e. NN ) /\ ( ( F ` ( p / q ) ) =/= 0 /\ ( abs ` ( A - ( p / q ) ) ) <_ 1 ) ) /\ ( x x. ( abs ` ( F ` ( p / q ) ) ) ) <_ ( abs ` ( A - ( p / q ) ) ) ) -> ( x / ( q ^ N ) ) <_ ( x x. ( abs ` ( F ` ( p / q ) ) ) ) )
77 simpr 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ ( p e. ZZ /\ q e. NN ) /\ ( ( F ` ( p / q ) ) =/= 0 /\ ( abs ` ( A - ( p / q ) ) ) <_ 1 ) ) /\ ( x x. ( abs ` ( F ` ( p / q ) ) ) ) <_ ( abs ` ( A - ( p / q ) ) ) ) -> ( x x. ( abs ` ( F ` ( p / q ) ) ) ) <_ ( abs ` ( A - ( p / q ) ) ) )
78 32 41 46 76 77 letrd 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ ( p e. ZZ /\ q e. NN ) /\ ( ( F ` ( p / q ) ) =/= 0 /\ ( abs ` ( A - ( p / q ) ) ) <_ 1 ) ) /\ ( x x. ( abs ` ( F ` ( p / q ) ) ) ) <_ ( abs ` ( A - ( p / q ) ) ) ) -> ( x / ( q ^ N ) ) <_ ( abs ` ( A - ( p / q ) ) ) )
79 78 olcd 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ ( p e. ZZ /\ q e. NN ) /\ ( ( F ` ( p / q ) ) =/= 0 /\ ( abs ` ( A - ( p / q ) ) ) <_ 1 ) ) /\ ( x x. ( abs ` ( F ` ( p / q ) ) ) ) <_ ( abs ` ( A - ( p / q ) ) ) ) -> ( A = ( p / q ) \/ ( x / ( q ^ N ) ) <_ ( abs ` ( A - ( p / q ) ) ) ) )
80 79 ex 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( p e. ZZ /\ q e. NN ) /\ ( ( F ` ( p / q ) ) =/= 0 /\ ( abs ` ( A - ( p / q ) ) ) <_ 1 ) ) -> ( ( x x. ( abs ` ( F ` ( p / q ) ) ) ) <_ ( abs ` ( A - ( p / q ) ) ) -> ( A = ( p / q ) \/ ( x / ( q ^ N ) ) <_ ( abs ` ( A - ( p / q ) ) ) ) ) )
81 23 80 syld 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( p e. ZZ /\ q e. NN ) /\ ( ( F ` ( p / q ) ) =/= 0 /\ ( abs ` ( A - ( p / q ) ) ) <_ 1 ) ) -> ( A. a e. RR ( ( abs ` ( A - a ) ) <_ 1 -> ( x x. ( abs ` ( F ` a ) ) ) <_ ( abs ` ( A - a ) ) ) -> ( A = ( p / q ) \/ ( x / ( q ^ N ) ) <_ ( abs ` ( A - ( p / q ) ) ) ) ) )
82 81 3exp 
 |-  ( ( ph /\ x e. RR+ ) -> ( ( p e. ZZ /\ q e. NN ) -> ( ( ( F ` ( p / q ) ) =/= 0 /\ ( abs ` ( A - ( p / q ) ) ) <_ 1 ) -> ( A. a e. RR ( ( abs ` ( A - a ) ) <_ 1 -> ( x x. ( abs ` ( F ` a ) ) ) <_ ( abs ` ( A - a ) ) ) -> ( A = ( p / q ) \/ ( x / ( q ^ N ) ) <_ ( abs ` ( A - ( p / q ) ) ) ) ) ) ) )
83 82 com34 
 |-  ( ( ph /\ x e. RR+ ) -> ( ( p e. ZZ /\ q e. NN ) -> ( A. a e. RR ( ( abs ` ( A - a ) ) <_ 1 -> ( x x. ( abs ` ( F ` a ) ) ) <_ ( abs ` ( A - a ) ) ) -> ( ( ( F ` ( p / q ) ) =/= 0 /\ ( abs ` ( A - ( p / q ) ) ) <_ 1 ) -> ( A = ( p / q ) \/ ( x / ( q ^ N ) ) <_ ( abs ` ( A - ( p / q ) ) ) ) ) ) ) )
84 83 com23 
 |-  ( ( ph /\ x e. RR+ ) -> ( A. a e. RR ( ( abs ` ( A - a ) ) <_ 1 -> ( x x. ( abs ` ( F ` a ) ) ) <_ ( abs ` ( A - a ) ) ) -> ( ( p e. ZZ /\ q e. NN ) -> ( ( ( F ` ( p / q ) ) =/= 0 /\ ( abs ` ( A - ( p / q ) ) ) <_ 1 ) -> ( A = ( p / q ) \/ ( x / ( q ^ N ) ) <_ ( abs ` ( A - ( p / q ) ) ) ) ) ) ) )
85 84 ralrimdvv 
 |-  ( ( ph /\ x e. RR+ ) -> ( A. a e. RR ( ( abs ` ( A - a ) ) <_ 1 -> ( x x. ( abs ` ( F ` a ) ) ) <_ ( abs ` ( A - a ) ) ) -> A. p e. ZZ A. q e. NN ( ( ( F ` ( p / q ) ) =/= 0 /\ ( abs ` ( A - ( p / q ) ) ) <_ 1 ) -> ( A = ( p / q ) \/ ( x / ( q ^ N ) ) <_ ( abs ` ( A - ( p / q ) ) ) ) ) ) )
86 85 reximdva 
 |-  ( ph -> ( E. x e. RR+ A. a e. RR ( ( abs ` ( A - a ) ) <_ 1 -> ( x x. ( abs ` ( F ` a ) ) ) <_ ( abs ` ( A - a ) ) ) -> E. x e. RR+ A. p e. ZZ A. q e. NN ( ( ( F ` ( p / q ) ) =/= 0 /\ ( abs ` ( A - ( p / q ) ) ) <_ 1 ) -> ( A = ( p / q ) \/ ( x / ( q ^ N ) ) <_ ( abs ` ( A - ( p / q ) ) ) ) ) ) )
87 6 86 mpd 
 |-  ( ph -> E. x e. RR+ A. p e. ZZ A. q e. NN ( ( ( F ` ( p / q ) ) =/= 0 /\ ( abs ` ( A - ( p / q ) ) ) <_ 1 ) -> ( A = ( p / q ) \/ ( x / ( q ^ N ) ) <_ ( abs ` ( A - ( p / q ) ) ) ) ) )