Metamath Proof Explorer

Theorem aalioulem2

Description: Lemma for aaliou . (Contributed by Stefan O'Rear, 15-Nov-2014) (Proof shortened by AV, 28-Sep-2020)

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 )
Assertion aalioulem2 
|- ( 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 1rp 
 |-  1 e. RR+
6 snssi 
 |-  ( 1 e. RR+ -> { 1 } C_ RR+ )
7 5 6 ax-mp 
 |-  { 1 } C_ RR+
8 ssrab2 
 |-  { a e. RR+ | E. b e. ( `' F " { 0 } ) a = ( abs ` ( A - b ) ) } C_ RR+
9 7 8 unssi 
 |-  ( { 1 } u. { a e. RR+ | E. b e. ( `' F " { 0 } ) a = ( abs ` ( A - b ) ) } ) C_ RR+
10 ltso 
 |-  < Or RR
11 10 a1i 
 |-  ( ph -> < Or RR )
12 snfi 
 |-  { 1 } e. Fin
13 3 nnne0d 
 |-  ( ph -> N =/= 0 )
14 1 eqcomi 
 |-  ( deg ` F ) = N
15 dgr0 
 |-  ( deg ` 0p ) = 0
16 13 14 15 3netr4g 
 |-  ( ph -> ( deg ` F ) =/= ( deg ` 0p ) )
17 fveq2 
 |-  ( F = 0p -> ( deg ` F ) = ( deg ` 0p ) )
18 17 necon3i 
 |-  ( ( deg ` F ) =/= ( deg ` 0p ) -> F =/= 0p )
19 16 18 syl 
 |-  ( ph -> F =/= 0p )
20 eqid 
 |-  ( `' F " { 0 } ) = ( `' F " { 0 } )
21 20 fta1 
 |-  ( ( F e. ( Poly ` ZZ ) /\ F =/= 0p ) -> ( ( `' F " { 0 } ) e. Fin /\ ( # ` ( `' F " { 0 } ) ) <_ ( deg ` F ) ) )
22 2 19 21 syl2anc 
 |-  ( ph -> ( ( `' F " { 0 } ) e. Fin /\ ( # ` ( `' F " { 0 } ) ) <_ ( deg ` F ) ) )
23 22 simpld 
 |-  ( ph -> ( `' F " { 0 } ) e. Fin )
24 abrexfi 
 |-  ( ( `' F " { 0 } ) e. Fin -> { a | E. b e. ( `' F " { 0 } ) a = ( abs ` ( A - b ) ) } e. Fin )
25 23 24 syl 
 |-  ( ph -> { a | E. b e. ( `' F " { 0 } ) a = ( abs ` ( A - b ) ) } e. Fin )
26 rabssab 
 |-  { a e. RR+ | E. b e. ( `' F " { 0 } ) a = ( abs ` ( A - b ) ) } C_ { a | E. b e. ( `' F " { 0 } ) a = ( abs ` ( A - b ) ) }
27 ssfi 
 |-  ( ( { a | E. b e. ( `' F " { 0 } ) a = ( abs ` ( A - b ) ) } e. Fin /\ { a e. RR+ | E. b e. ( `' F " { 0 } ) a = ( abs ` ( A - b ) ) } C_ { a | E. b e. ( `' F " { 0 } ) a = ( abs ` ( A - b ) ) } ) -> { a e. RR+ | E. b e. ( `' F " { 0 } ) a = ( abs ` ( A - b ) ) } e. Fin )
28 25 26 27 sylancl 
 |-  ( ph -> { a e. RR+ | E. b e. ( `' F " { 0 } ) a = ( abs ` ( A - b ) ) } e. Fin )
29 unfi 
 |-  ( ( { 1 } e. Fin /\ { a e. RR+ | E. b e. ( `' F " { 0 } ) a = ( abs ` ( A - b ) ) } e. Fin ) -> ( { 1 } u. { a e. RR+ | E. b e. ( `' F " { 0 } ) a = ( abs ` ( A - b ) ) } ) e. Fin )
30 12 28 29 sylancr 
 |-  ( ph -> ( { 1 } u. { a e. RR+ | E. b e. ( `' F " { 0 } ) a = ( abs ` ( A - b ) ) } ) e. Fin )
31 1ex 
 |-  1 e. _V
32 31 snid 
 |-  1 e. { 1 }
33 elun1 
 |-  ( 1 e. { 1 } -> 1 e. ( { 1 } u. { a e. RR+ | E. b e. ( `' F " { 0 } ) a = ( abs ` ( A - b ) ) } ) )
34 ne0i 
 |-  ( 1 e. ( { 1 } u. { a e. RR+ | E. b e. ( `' F " { 0 } ) a = ( abs ` ( A - b ) ) } ) -> ( { 1 } u. { a e. RR+ | E. b e. ( `' F " { 0 } ) a = ( abs ` ( A - b ) ) } ) =/= (/) )
35 32 33 34 mp2b 
 |-  ( { 1 } u. { a e. RR+ | E. b e. ( `' F " { 0 } ) a = ( abs ` ( A - b ) ) } ) =/= (/)
36 35 a1i 
 |-  ( ph -> ( { 1 } u. { a e. RR+ | E. b e. ( `' F " { 0 } ) a = ( abs ` ( A - b ) ) } ) =/= (/) )
37 rpssre 
 |-  RR+ C_ RR
38 9 37 sstri 
 |-  ( { 1 } u. { a e. RR+ | E. b e. ( `' F " { 0 } ) a = ( abs ` ( A - b ) ) } ) C_ RR
39 38 a1i 
 |-  ( ph -> ( { 1 } u. { a e. RR+ | E. b e. ( `' F " { 0 } ) a = ( abs ` ( A - b ) ) } ) C_ RR )
40 fiinfcl 
 |-  ( ( < Or RR /\ ( ( { 1 } u. { a e. RR+ | E. b e. ( `' F " { 0 } ) a = ( abs ` ( A - b ) ) } ) e. Fin /\ ( { 1 } u. { a e. RR+ | E. b e. ( `' F " { 0 } ) a = ( abs ` ( A - b ) ) } ) =/= (/) /\ ( { 1 } u. { a e. RR+ | E. b e. ( `' F " { 0 } ) a = ( abs ` ( A - b ) ) } ) C_ RR ) ) -> inf ( ( { 1 } u. { a e. RR+ | E. b e. ( `' F " { 0 } ) a = ( abs ` ( A - b ) ) } ) , RR , < ) e. ( { 1 } u. { a e. RR+ | E. b e. ( `' F " { 0 } ) a = ( abs ` ( A - b ) ) } ) )
41 11 30 36 39 40 syl13anc 
 |-  ( ph -> inf ( ( { 1 } u. { a e. RR+ | E. b e. ( `' F " { 0 } ) a = ( abs ` ( A - b ) ) } ) , RR , < ) e. ( { 1 } u. { a e. RR+ | E. b e. ( `' F " { 0 } ) a = ( abs ` ( A - b ) ) } ) )
42 9 41 sselid 
 |-  ( ph -> inf ( ( { 1 } u. { a e. RR+ | E. b e. ( `' F " { 0 } ) a = ( abs ` ( A - b ) ) } ) , RR , < ) e. RR+ )
43 0re 
 |-  0 e. RR
44 rpge0 
 |-  ( d e. RR+ -> 0 <_ d )
45 44 rgen 
 |-  A. d e. RR+ 0 <_ d
46 breq1 
 |-  ( c = 0 -> ( c <_ d <-> 0 <_ d ) )
47 46 ralbidv 
 |-  ( c = 0 -> ( A. d e. RR+ c <_ d <-> A. d e. RR+ 0 <_ d ) )
48 47 rspcev 
 |-  ( ( 0 e. RR /\ A. d e. RR+ 0 <_ d ) -> E. c e. RR A. d e. RR+ c <_ d )
49 43 45 48 mp2an 
 |-  E. c e. RR A. d e. RR+ c <_ d
50 ssralv 
 |-  ( ( { 1 } u. { a e. RR+ | E. b e. ( `' F " { 0 } ) a = ( abs ` ( A - b ) ) } ) C_ RR+ -> ( A. d e. RR+ c <_ d -> A. d e. ( { 1 } u. { a e. RR+ | E. b e. ( `' F " { 0 } ) a = ( abs ` ( A - b ) ) } ) c <_ d ) )
51 9 50 ax-mp 
 |-  ( A. d e. RR+ c <_ d -> A. d e. ( { 1 } u. { a e. RR+ | E. b e. ( `' F " { 0 } ) a = ( abs ` ( A - b ) ) } ) c <_ d )
52 51 reximi 
 |-  ( E. c e. RR A. d e. RR+ c <_ d -> E. c e. RR A. d e. ( { 1 } u. { a e. RR+ | E. b e. ( `' F " { 0 } ) a = ( abs ` ( A - b ) ) } ) c <_ d )
53 49 52 ax-mp 
 |-  E. c e. RR A. d e. ( { 1 } u. { a e. RR+ | E. b e. ( `' F " { 0 } ) a = ( abs ` ( A - b ) ) } ) c <_ d
54 eqeq1 
 |-  ( a = ( abs ` ( A - r ) ) -> ( a = ( abs ` ( A - b ) ) <-> ( abs ` ( A - r ) ) = ( abs ` ( A - b ) ) ) )
55 54 rexbidv 
 |-  ( a = ( abs ` ( A - r ) ) -> ( E. b e. ( `' F " { 0 } ) a = ( abs ` ( A - b ) ) <-> E. b e. ( `' F " { 0 } ) ( abs ` ( A - r ) ) = ( abs ` ( A - b ) ) ) )
56 4 ad2antrr 
 |-  ( ( ( ph /\ r e. RR ) /\ ( ( F ` r ) = 0 /\ -. A = r ) ) -> A e. RR )
57 simplr 
 |-  ( ( ( ph /\ r e. RR ) /\ ( ( F ` r ) = 0 /\ -. A = r ) ) -> r e. RR )
58 56 57 resubcld 
 |-  ( ( ( ph /\ r e. RR ) /\ ( ( F ` r ) = 0 /\ -. A = r ) ) -> ( A - r ) e. RR )
59 58 recnd 
 |-  ( ( ( ph /\ r e. RR ) /\ ( ( F ` r ) = 0 /\ -. A = r ) ) -> ( A - r ) e. CC )
60 4 ad2antrr 
 |-  ( ( ( ph /\ r e. RR ) /\ ( F ` r ) = 0 ) -> A e. RR )
61 60 recnd 
 |-  ( ( ( ph /\ r e. RR ) /\ ( F ` r ) = 0 ) -> A e. CC )
62 simplr 
 |-  ( ( ( ph /\ r e. RR ) /\ ( F ` r ) = 0 ) -> r e. RR )
63 62 recnd 
 |-  ( ( ( ph /\ r e. RR ) /\ ( F ` r ) = 0 ) -> r e. CC )
64 61 63 subeq0ad 
 |-  ( ( ( ph /\ r e. RR ) /\ ( F ` r ) = 0 ) -> ( ( A - r ) = 0 <-> A = r ) )
65 64 necon3abid 
 |-  ( ( ( ph /\ r e. RR ) /\ ( F ` r ) = 0 ) -> ( ( A - r ) =/= 0 <-> -. A = r ) )
66 65 biimprd 
 |-  ( ( ( ph /\ r e. RR ) /\ ( F ` r ) = 0 ) -> ( -. A = r -> ( A - r ) =/= 0 ) )
67 66 impr 
 |-  ( ( ( ph /\ r e. RR ) /\ ( ( F ` r ) = 0 /\ -. A = r ) ) -> ( A - r ) =/= 0 )
68 59 67 absrpcld 
 |-  ( ( ( ph /\ r e. RR ) /\ ( ( F ` r ) = 0 /\ -. A = r ) ) -> ( abs ` ( A - r ) ) e. RR+ )
69 57 recnd 
 |-  ( ( ( ph /\ r e. RR ) /\ ( ( F ` r ) = 0 /\ -. A = r ) ) -> r e. CC )
70 simprl 
 |-  ( ( ( ph /\ r e. RR ) /\ ( ( F ` r ) = 0 /\ -. A = r ) ) -> ( F ` r ) = 0 )
71 plyf 
 |-  ( F e. ( Poly ` ZZ ) -> F : CC --> CC )
72 2 71 syl 
 |-  ( ph -> F : CC --> CC )
73 72 ffnd 
 |-  ( ph -> F Fn CC )
74 73 ad2antrr 
 |-  ( ( ( ph /\ r e. RR ) /\ ( ( F ` r ) = 0 /\ -. A = r ) ) -> F Fn CC )
75 fniniseg 
 |-  ( F Fn CC -> ( r e. ( `' F " { 0 } ) <-> ( r e. CC /\ ( F ` r ) = 0 ) ) )
76 74 75 syl 
 |-  ( ( ( ph /\ r e. RR ) /\ ( ( F ` r ) = 0 /\ -. A = r ) ) -> ( r e. ( `' F " { 0 } ) <-> ( r e. CC /\ ( F ` r ) = 0 ) ) )
77 69 70 76 mpbir2and 
 |-  ( ( ( ph /\ r e. RR ) /\ ( ( F ` r ) = 0 /\ -. A = r ) ) -> r e. ( `' F " { 0 } ) )
78 eqid 
 |-  ( abs ` ( A - r ) ) = ( abs ` ( A - r ) )
79 oveq2 
 |-  ( b = r -> ( A - b ) = ( A - r ) )
80 79 fveq2d 
 |-  ( b = r -> ( abs ` ( A - b ) ) = ( abs ` ( A - r ) ) )
81 80 rspceeqv 
 |-  ( ( r e. ( `' F " { 0 } ) /\ ( abs ` ( A - r ) ) = ( abs ` ( A - r ) ) ) -> E. b e. ( `' F " { 0 } ) ( abs ` ( A - r ) ) = ( abs ` ( A - b ) ) )
82 77 78 81 sylancl 
 |-  ( ( ( ph /\ r e. RR ) /\ ( ( F ` r ) = 0 /\ -. A = r ) ) -> E. b e. ( `' F " { 0 } ) ( abs ` ( A - r ) ) = ( abs ` ( A - b ) ) )
83 55 68 82 elrabd 
 |-  ( ( ( ph /\ r e. RR ) /\ ( ( F ` r ) = 0 /\ -. A = r ) ) -> ( abs ` ( A - r ) ) e. { a e. RR+ | E. b e. ( `' F " { 0 } ) a = ( abs ` ( A - b ) ) } )
84 elun2 
 |-  ( ( abs ` ( A - r ) ) e. { a e. RR+ | E. b e. ( `' F " { 0 } ) a = ( abs ` ( A - b ) ) } -> ( abs ` ( A - r ) ) e. ( { 1 } u. { a e. RR+ | E. b e. ( `' F " { 0 } ) a = ( abs ` ( A - b ) ) } ) )
85 83 84 syl 
 |-  ( ( ( ph /\ r e. RR ) /\ ( ( F ` r ) = 0 /\ -. A = r ) ) -> ( abs ` ( A - r ) ) e. ( { 1 } u. { a e. RR+ | E. b e. ( `' F " { 0 } ) a = ( abs ` ( A - b ) ) } ) )
86 infrelb 
 |-  ( ( ( { 1 } u. { a e. RR+ | E. b e. ( `' F " { 0 } ) a = ( abs ` ( A - b ) ) } ) C_ RR /\ E. c e. RR A. d e. ( { 1 } u. { a e. RR+ | E. b e. ( `' F " { 0 } ) a = ( abs ` ( A - b ) ) } ) c <_ d /\ ( abs ` ( A - r ) ) e. ( { 1 } u. { a e. RR+ | E. b e. ( `' F " { 0 } ) a = ( abs ` ( A - b ) ) } ) ) -> inf ( ( { 1 } u. { a e. RR+ | E. b e. ( `' F " { 0 } ) a = ( abs ` ( A - b ) ) } ) , RR , < ) <_ ( abs ` ( A - r ) ) )
87 38 53 85 86 mp3an12i 
 |-  ( ( ( ph /\ r e. RR ) /\ ( ( F ` r ) = 0 /\ -. A = r ) ) -> inf ( ( { 1 } u. { a e. RR+ | E. b e. ( `' F " { 0 } ) a = ( abs ` ( A - b ) ) } ) , RR , < ) <_ ( abs ` ( A - r ) ) )
88 87 expr 
 |-  ( ( ( ph /\ r e. RR ) /\ ( F ` r ) = 0 ) -> ( -. A = r -> inf ( ( { 1 } u. { a e. RR+ | E. b e. ( `' F " { 0 } ) a = ( abs ` ( A - b ) ) } ) , RR , < ) <_ ( abs ` ( A - r ) ) ) )
89 88 orrd 
 |-  ( ( ( ph /\ r e. RR ) /\ ( F ` r ) = 0 ) -> ( A = r \/ inf ( ( { 1 } u. { a e. RR+ | E. b e. ( `' F " { 0 } ) a = ( abs ` ( A - b ) ) } ) , RR , < ) <_ ( abs ` ( A - r ) ) ) )
90 89 ex 
 |-  ( ( ph /\ r e. RR ) -> ( ( F ` r ) = 0 -> ( A = r \/ inf ( ( { 1 } u. { a e. RR+ | E. b e. ( `' F " { 0 } ) a = ( abs ` ( A - b ) ) } ) , RR , < ) <_ ( abs ` ( A - r ) ) ) ) )
91 90 ralrimiva 
 |-  ( ph -> A. r e. RR ( ( F ` r ) = 0 -> ( A = r \/ inf ( ( { 1 } u. { a e. RR+ | E. b e. ( `' F " { 0 } ) a = ( abs ` ( A - b ) ) } ) , RR , < ) <_ ( abs ` ( A - r ) ) ) ) )
92 breq1 
 |-  ( x = inf ( ( { 1 } u. { a e. RR+ | E. b e. ( `' F " { 0 } ) a = ( abs ` ( A - b ) ) } ) , RR , < ) -> ( x <_ ( abs ` ( A - r ) ) <-> inf ( ( { 1 } u. { a e. RR+ | E. b e. ( `' F " { 0 } ) a = ( abs ` ( A - b ) ) } ) , RR , < ) <_ ( abs ` ( A - r ) ) ) )
93 92 orbi2d 
 |-  ( x = inf ( ( { 1 } u. { a e. RR+ | E. b e. ( `' F " { 0 } ) a = ( abs ` ( A - b ) ) } ) , RR , < ) -> ( ( A = r \/ x <_ ( abs ` ( A - r ) ) ) <-> ( A = r \/ inf ( ( { 1 } u. { a e. RR+ | E. b e. ( `' F " { 0 } ) a = ( abs ` ( A - b ) ) } ) , RR , < ) <_ ( abs ` ( A - r ) ) ) ) )
94 93 imbi2d 
 |-  ( x = inf ( ( { 1 } u. { a e. RR+ | E. b e. ( `' F " { 0 } ) a = ( abs ` ( A - b ) ) } ) , RR , < ) -> ( ( ( F ` r ) = 0 -> ( A = r \/ x <_ ( abs ` ( A - r ) ) ) ) <-> ( ( F ` r ) = 0 -> ( A = r \/ inf ( ( { 1 } u. { a e. RR+ | E. b e. ( `' F " { 0 } ) a = ( abs ` ( A - b ) ) } ) , RR , < ) <_ ( abs ` ( A - r ) ) ) ) ) )
95 94 ralbidv 
 |-  ( x = inf ( ( { 1 } u. { a e. RR+ | E. b e. ( `' F " { 0 } ) a = ( abs ` ( A - b ) ) } ) , RR , < ) -> ( A. r e. RR ( ( F ` r ) = 0 -> ( A = r \/ x <_ ( abs ` ( A - r ) ) ) ) <-> A. r e. RR ( ( F ` r ) = 0 -> ( A = r \/ inf ( ( { 1 } u. { a e. RR+ | E. b e. ( `' F " { 0 } ) a = ( abs ` ( A - b ) ) } ) , RR , < ) <_ ( abs ` ( A - r ) ) ) ) ) )
96 95 rspcev 
 |-  ( ( inf ( ( { 1 } u. { a e. RR+ | E. b e. ( `' F " { 0 } ) a = ( abs ` ( A - b ) ) } ) , RR , < ) e. RR+ /\ A. r e. RR ( ( F ` r ) = 0 -> ( A = r \/ inf ( ( { 1 } u. { a e. RR+ | E. b e. ( `' F " { 0 } ) a = ( abs ` ( A - b ) ) } ) , RR , < ) <_ ( abs ` ( A - r ) ) ) ) ) -> E. x e. RR+ A. r e. RR ( ( F ` r ) = 0 -> ( A = r \/ x <_ ( abs ` ( A - r ) ) ) ) )
97 42 91 96 syl2anc 
 |-  ( ph -> E. x e. RR+ A. r e. RR ( ( F ` r ) = 0 -> ( A = r \/ x <_ ( abs ` ( A - r ) ) ) ) )
98 fveqeq2 
 |-  ( r = ( p / q ) -> ( ( F ` r ) = 0 <-> ( F ` ( p / q ) ) = 0 ) )
99 eqeq2 
 |-  ( r = ( p / q ) -> ( A = r <-> A = ( p / q ) ) )
100 oveq2 
 |-  ( r = ( p / q ) -> ( A - r ) = ( A - ( p / q ) ) )
101 100 fveq2d 
 |-  ( r = ( p / q ) -> ( abs ` ( A - r ) ) = ( abs ` ( A - ( p / q ) ) ) )
102 101 breq2d 
 |-  ( r = ( p / q ) -> ( x <_ ( abs ` ( A - r ) ) <-> x <_ ( abs ` ( A - ( p / q ) ) ) ) )
103 99 102 orbi12d 
 |-  ( r = ( p / q ) -> ( ( A = r \/ x <_ ( abs ` ( A - r ) ) ) <-> ( A = ( p / q ) \/ x <_ ( abs ` ( A - ( p / q ) ) ) ) ) )
104 98 103 imbi12d 
 |-  ( r = ( p / q ) -> ( ( ( F ` r ) = 0 -> ( A = r \/ x <_ ( abs ` ( A - r ) ) ) ) <-> ( ( F ` ( p / q ) ) = 0 -> ( A = ( p / q ) \/ x <_ ( abs ` ( A - ( p / q ) ) ) ) ) ) )
105 104 rspcv 
 |-  ( ( p / q ) e. RR -> ( A. r e. RR ( ( F ` r ) = 0 -> ( A = r \/ x <_ ( abs ` ( A - r ) ) ) ) -> ( ( F ` ( p / q ) ) = 0 -> ( A = ( p / q ) \/ x <_ ( abs ` ( A - ( p / q ) ) ) ) ) ) )
106 znq 
 |-  ( ( p e. ZZ /\ q e. NN ) -> ( p / q ) e. QQ )
107 qre 
 |-  ( ( p / q ) e. QQ -> ( p / q ) e. RR )
108 106 107 syl 
 |-  ( ( p e. ZZ /\ q e. NN ) -> ( p / q ) e. RR )
109 105 108 syl11 
 |-  ( A. r e. RR ( ( F ` r ) = 0 -> ( A = r \/ x <_ ( abs ` ( A - r ) ) ) ) -> ( ( p e. ZZ /\ q e. NN ) -> ( ( F ` ( p / q ) ) = 0 -> ( A = ( p / q ) \/ x <_ ( abs ` ( A - ( p / q ) ) ) ) ) ) )
110 109 ralrimivv 
 |-  ( A. r e. RR ( ( F ` r ) = 0 -> ( A = r \/ x <_ ( abs ` ( A - r ) ) ) ) -> A. p e. ZZ A. q e. NN ( ( F ` ( p / q ) ) = 0 -> ( A = ( p / q ) \/ x <_ ( abs ` ( A - ( p / q ) ) ) ) ) )
111 110 reximi 
 |-  ( E. x e. RR+ A. r e. RR ( ( F ` r ) = 0 -> ( A = r \/ x <_ ( abs ` ( A - r ) ) ) ) -> E. x e. RR+ A. p e. ZZ A. q e. NN ( ( F ` ( p / q ) ) = 0 -> ( A = ( p / q ) \/ x <_ ( abs ` ( A - ( p / q ) ) ) ) ) )
112 97 111 syl 
 |-  ( ph -> E. x e. RR+ A. p e. ZZ A. q e. NN ( ( F ` ( p / q ) ) = 0 -> ( A = ( p / q ) \/ x <_ ( abs ` ( A - ( p / q ) ) ) ) ) )
113 simplr 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( p e. ZZ /\ q e. NN ) ) -> x e. RR+ )
114 simprr 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( p e. ZZ /\ q e. NN ) ) -> q e. NN )
115 3 nnnn0d 
 |-  ( ph -> N e. NN0 )
116 115 ad2antrr 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( p e. ZZ /\ q e. NN ) ) -> N e. NN0 )
117 114 116 nnexpcld 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( p e. ZZ /\ q e. NN ) ) -> ( q ^ N ) e. NN )
118 117 nnrpd 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( p e. ZZ /\ q e. NN ) ) -> ( q ^ N ) e. RR+ )
119 113 118 rpdivcld 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( p e. ZZ /\ q e. NN ) ) -> ( x / ( q ^ N ) ) e. RR+ )
120 119 rpred 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( p e. ZZ /\ q e. NN ) ) -> ( x / ( q ^ N ) ) e. RR )
121 120 adantr 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ ( p e. ZZ /\ q e. NN ) ) /\ x <_ ( abs ` ( A - ( p / q ) ) ) ) -> ( x / ( q ^ N ) ) e. RR )
122 simpllr 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ ( p e. ZZ /\ q e. NN ) ) /\ x <_ ( abs ` ( A - ( p / q ) ) ) ) -> x e. RR+ )
123 122 rpred 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ ( p e. ZZ /\ q e. NN ) ) /\ x <_ ( abs ` ( A - ( p / q ) ) ) ) -> x e. RR )
124 4 ad2antrr 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( p e. ZZ /\ q e. NN ) ) -> A e. RR )
125 108 adantl 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( p e. ZZ /\ q e. NN ) ) -> ( p / q ) e. RR )
126 124 125 resubcld 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( p e. ZZ /\ q e. NN ) ) -> ( A - ( p / q ) ) e. RR )
127 126 recnd 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( p e. ZZ /\ q e. NN ) ) -> ( A - ( p / q ) ) e. CC )
128 127 abscld 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( p e. ZZ /\ q e. NN ) ) -> ( abs ` ( A - ( p / q ) ) ) e. RR )
129 128 adantr 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ ( p e. ZZ /\ q e. NN ) ) /\ x <_ ( abs ` ( A - ( p / q ) ) ) ) -> ( abs ` ( A - ( p / q ) ) ) e. RR )
130 rpre 
 |-  ( x e. RR+ -> x e. RR )
131 130 ad2antlr 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( p e. ZZ /\ q e. NN ) ) -> x e. RR )
132 113 rpcnne0d 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( p e. ZZ /\ q e. NN ) ) -> ( x e. CC /\ x =/= 0 ) )
133 divid 
 |-  ( ( x e. CC /\ x =/= 0 ) -> ( x / x ) = 1 )
134 132 133 syl 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( p e. ZZ /\ q e. NN ) ) -> ( x / x ) = 1 )
135 117 nnge1d 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( p e. ZZ /\ q e. NN ) ) -> 1 <_ ( q ^ N ) )
136 134 135 eqbrtrd 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( p e. ZZ /\ q e. NN ) ) -> ( x / x ) <_ ( q ^ N ) )
137 131 113 118 136 lediv23d 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( p e. ZZ /\ q e. NN ) ) -> ( x / ( q ^ N ) ) <_ x )
138 137 adantr 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ ( p e. ZZ /\ q e. NN ) ) /\ x <_ ( abs ` ( A - ( p / q ) ) ) ) -> ( x / ( q ^ N ) ) <_ x )
139 simpr 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ ( p e. ZZ /\ q e. NN ) ) /\ x <_ ( abs ` ( A - ( p / q ) ) ) ) -> x <_ ( abs ` ( A - ( p / q ) ) ) )
140 121 123 129 138 139 letrd 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ ( p e. ZZ /\ q e. NN ) ) /\ x <_ ( abs ` ( A - ( p / q ) ) ) ) -> ( x / ( q ^ N ) ) <_ ( abs ` ( A - ( p / q ) ) ) )
141 140 ex 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( p e. ZZ /\ q e. NN ) ) -> ( x <_ ( abs ` ( A - ( p / q ) ) ) -> ( x / ( q ^ N ) ) <_ ( abs ` ( A - ( p / q ) ) ) ) )
142 141 orim2d 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( p e. ZZ /\ q e. NN ) ) -> ( ( A = ( p / q ) \/ x <_ ( abs ` ( A - ( p / q ) ) ) ) -> ( A = ( p / q ) \/ ( x / ( q ^ N ) ) <_ ( abs ` ( A - ( p / q ) ) ) ) ) )
143 142 imim2d 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( p e. ZZ /\ q e. NN ) ) -> ( ( ( F ` ( p / q ) ) = 0 -> ( A = ( p / q ) \/ x <_ ( abs ` ( A - ( p / q ) ) ) ) ) -> ( ( F ` ( p / q ) ) = 0 -> ( A = ( p / q ) \/ ( x / ( q ^ N ) ) <_ ( abs ` ( A - ( p / q ) ) ) ) ) ) )
144 143 ralimdvva 
 |-  ( ( ph /\ x e. RR+ ) -> ( A. p e. ZZ A. q e. NN ( ( F ` ( p / q ) ) = 0 -> ( A = ( p / q ) \/ x <_ ( abs ` ( A - ( p / q ) ) ) ) ) -> A. p e. ZZ A. q e. NN ( ( F ` ( p / q ) ) = 0 -> ( A = ( p / q ) \/ ( x / ( q ^ N ) ) <_ ( abs ` ( A - ( p / q ) ) ) ) ) ) )
145 144 reximdva 
 |-  ( ph -> ( E. x e. RR+ A. p e. ZZ A. q e. NN ( ( F ` ( p / q ) ) = 0 -> ( A = ( p / q ) \/ x <_ ( 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 ) ) ) ) ) ) )
146 112 145 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 ) ) ) ) ) )