Metamath Proof Explorer

Theorem aalioulem6

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 aalioulem6 
|- ( ph -> E. x e. RR+ A. p e. ZZ A. q e. NN ( 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 aalioulem2 
 |-  ( ph -> E. a e. RR+ A. p e. ZZ A. q e. NN ( ( F ` ( p / q ) ) = 0 -> ( A = ( p / q ) \/ ( a / ( q ^ N ) ) <_ ( abs ` ( A - ( p / q ) ) ) ) ) )
7 1 2 3 4 5 aalioulem5 
 |-  ( ph -> E. b e. RR+ A. p e. ZZ A. q e. NN ( ( F ` ( p / q ) ) =/= 0 -> ( A = ( p / q ) \/ ( b / ( q ^ N ) ) <_ ( abs ` ( A - ( p / q ) ) ) ) ) )
8 reeanv 
 |-  ( E. a e. RR+ E. b e. RR+ ( A. p e. ZZ A. q e. NN ( ( F ` ( p / q ) ) = 0 -> ( 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 ) \/ ( b / ( q ^ N ) ) <_ ( abs ` ( A - ( p / q ) ) ) ) ) ) <-> ( E. a e. RR+ A. p e. ZZ A. q e. NN ( ( F ` ( p / q ) ) = 0 -> ( A = ( p / q ) \/ ( a / ( q ^ N ) ) <_ ( abs ` ( A - ( p / q ) ) ) ) ) /\ E. b e. RR+ A. p e. ZZ A. q e. NN ( ( F ` ( p / q ) ) =/= 0 -> ( A = ( p / q ) \/ ( b / ( q ^ N ) ) <_ ( abs ` ( A - ( p / q ) ) ) ) ) ) )
9 6 7 8 sylanbrc 
 |-  ( ph -> E. a e. RR+ E. b e. RR+ ( A. p e. ZZ A. q e. NN ( ( F ` ( p / q ) ) = 0 -> ( 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 ) \/ ( b / ( q ^ N ) ) <_ ( abs ` ( A - ( p / q ) ) ) ) ) ) )
10 r19.26-2 
 |-  ( A. p e. ZZ A. q e. NN ( ( ( F ` ( p / q ) ) = 0 -> ( A = ( p / q ) \/ ( a / ( q ^ N ) ) <_ ( abs ` ( A - ( p / q ) ) ) ) ) /\ ( ( F ` ( p / q ) ) =/= 0 -> ( A = ( p / q ) \/ ( b / ( q ^ N ) ) <_ ( abs ` ( A - ( p / q ) ) ) ) ) ) <-> ( A. p e. ZZ A. q e. NN ( ( F ` ( p / q ) ) = 0 -> ( 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 ) \/ ( b / ( q ^ N ) ) <_ ( abs ` ( A - ( p / q ) ) ) ) ) ) )
11 ifcl 
 |-  ( ( a e. RR+ /\ b e. RR+ ) -> if ( a <_ b , a , b ) e. RR+ )
12 11 adantl 
 |-  ( ( ph /\ ( a e. RR+ /\ b e. RR+ ) ) -> if ( a <_ b , a , b ) e. RR+ )
13 simpr 
 |-  ( ( ( ( ph /\ ( a e. RR+ /\ b e. RR+ ) ) /\ ( p e. ZZ /\ q e. NN ) ) /\ ( F ` ( p / q ) ) = 0 ) -> ( F ` ( p / q ) ) = 0 )
14 11 ad2antlr 
 |-  ( ( ( ph /\ ( a e. RR+ /\ b e. RR+ ) ) /\ ( p e. ZZ /\ q e. NN ) ) -> if ( a <_ b , a , b ) e. RR+ )
15 nnrp 
 |-  ( q e. NN -> q e. RR+ )
16 15 ad2antll 
 |-  ( ( ( ph /\ ( a e. RR+ /\ b e. RR+ ) ) /\ ( p e. ZZ /\ q e. NN ) ) -> q e. RR+ )
17 3 ad2antrr 
 |-  ( ( ( ph /\ ( a e. RR+ /\ b e. RR+ ) ) /\ ( p e. ZZ /\ q e. NN ) ) -> N e. NN )
18 17 nnzd 
 |-  ( ( ( ph /\ ( a e. RR+ /\ b e. RR+ ) ) /\ ( p e. ZZ /\ q e. NN ) ) -> N e. ZZ )
19 16 18 rpexpcld 
 |-  ( ( ( ph /\ ( a e. RR+ /\ b e. RR+ ) ) /\ ( p e. ZZ /\ q e. NN ) ) -> ( q ^ N ) e. RR+ )
20 14 19 rpdivcld 
 |-  ( ( ( ph /\ ( a e. RR+ /\ b e. RR+ ) ) /\ ( p e. ZZ /\ q e. NN ) ) -> ( if ( a <_ b , a , b ) / ( q ^ N ) ) e. RR+ )
21 20 rpred 
 |-  ( ( ( ph /\ ( a e. RR+ /\ b e. RR+ ) ) /\ ( p e. ZZ /\ q e. NN ) ) -> ( if ( a <_ b , a , b ) / ( q ^ N ) ) e. RR )
22 simplrl 
 |-  ( ( ( ph /\ ( a e. RR+ /\ b e. RR+ ) ) /\ ( p e. ZZ /\ q e. NN ) ) -> a e. RR+ )
23 22 19 rpdivcld 
 |-  ( ( ( ph /\ ( a e. RR+ /\ b e. RR+ ) ) /\ ( p e. ZZ /\ q e. NN ) ) -> ( a / ( q ^ N ) ) e. RR+ )
24 23 rpred 
 |-  ( ( ( ph /\ ( a e. RR+ /\ b e. RR+ ) ) /\ ( p e. ZZ /\ q e. NN ) ) -> ( a / ( q ^ N ) ) e. RR )
25 4 ad2antrr 
 |-  ( ( ( ph /\ ( a e. RR+ /\ b e. RR+ ) ) /\ ( p e. ZZ /\ q e. NN ) ) -> A e. RR )
26 znq 
 |-  ( ( p e. ZZ /\ q e. NN ) -> ( p / q ) e. QQ )
27 qre 
 |-  ( ( p / q ) e. QQ -> ( p / q ) e. RR )
28 26 27 syl 
 |-  ( ( p e. ZZ /\ q e. NN ) -> ( p / q ) e. RR )
29 28 adantl 
 |-  ( ( ( ph /\ ( a e. RR+ /\ b e. RR+ ) ) /\ ( p e. ZZ /\ q e. NN ) ) -> ( p / q ) e. RR )
30 25 29 resubcld 
 |-  ( ( ( ph /\ ( a e. RR+ /\ b e. RR+ ) ) /\ ( p e. ZZ /\ q e. NN ) ) -> ( A - ( p / q ) ) e. RR )
31 30 recnd 
 |-  ( ( ( ph /\ ( a e. RR+ /\ b e. RR+ ) ) /\ ( p e. ZZ /\ q e. NN ) ) -> ( A - ( p / q ) ) e. CC )
32 31 abscld 
 |-  ( ( ( ph /\ ( a e. RR+ /\ b e. RR+ ) ) /\ ( p e. ZZ /\ q e. NN ) ) -> ( abs ` ( A - ( p / q ) ) ) e. RR )
33 21 24 32 3jca 
 |-  ( ( ( ph /\ ( a e. RR+ /\ b e. RR+ ) ) /\ ( p e. ZZ /\ q e. NN ) ) -> ( ( if ( a <_ b , a , b ) / ( q ^ N ) ) e. RR /\ ( a / ( q ^ N ) ) e. RR /\ ( abs ` ( A - ( p / q ) ) ) e. RR ) )
34 33 adantr 
 |-  ( ( ( ( ph /\ ( a e. RR+ /\ b e. RR+ ) ) /\ ( p e. ZZ /\ q e. NN ) ) /\ ( a / ( q ^ N ) ) <_ ( abs ` ( A - ( p / q ) ) ) ) -> ( ( if ( a <_ b , a , b ) / ( q ^ N ) ) e. RR /\ ( a / ( q ^ N ) ) e. RR /\ ( abs ` ( A - ( p / q ) ) ) e. RR ) )
35 14 rpred 
 |-  ( ( ( ph /\ ( a e. RR+ /\ b e. RR+ ) ) /\ ( p e. ZZ /\ q e. NN ) ) -> if ( a <_ b , a , b ) e. RR )
36 22 rpred 
 |-  ( ( ( ph /\ ( a e. RR+ /\ b e. RR+ ) ) /\ ( p e. ZZ /\ q e. NN ) ) -> a e. RR )
37 simplrr 
 |-  ( ( ( ph /\ ( a e. RR+ /\ b e. RR+ ) ) /\ ( p e. ZZ /\ q e. NN ) ) -> b e. RR+ )
38 37 rpred 
 |-  ( ( ( ph /\ ( a e. RR+ /\ b e. RR+ ) ) /\ ( p e. ZZ /\ q e. NN ) ) -> b e. RR )
39 min1 
 |-  ( ( a e. RR /\ b e. RR ) -> if ( a <_ b , a , b ) <_ a )
40 36 38 39 syl2anc 
 |-  ( ( ( ph /\ ( a e. RR+ /\ b e. RR+ ) ) /\ ( p e. ZZ /\ q e. NN ) ) -> if ( a <_ b , a , b ) <_ a )
41 35 36 19 40 lediv1dd 
 |-  ( ( ( ph /\ ( a e. RR+ /\ b e. RR+ ) ) /\ ( p e. ZZ /\ q e. NN ) ) -> ( if ( a <_ b , a , b ) / ( q ^ N ) ) <_ ( a / ( q ^ N ) ) )
42 41 anim1i 
 |-  ( ( ( ( ph /\ ( a e. RR+ /\ b e. RR+ ) ) /\ ( p e. ZZ /\ q e. NN ) ) /\ ( a / ( q ^ N ) ) <_ ( abs ` ( A - ( p / q ) ) ) ) -> ( ( if ( a <_ b , a , b ) / ( q ^ N ) ) <_ ( a / ( q ^ N ) ) /\ ( a / ( q ^ N ) ) <_ ( abs ` ( A - ( p / q ) ) ) ) )
43 letr 
 |-  ( ( ( if ( a <_ b , a , b ) / ( q ^ N ) ) e. RR /\ ( a / ( q ^ N ) ) e. RR /\ ( abs ` ( A - ( p / q ) ) ) e. RR ) -> ( ( ( if ( a <_ b , a , b ) / ( q ^ N ) ) <_ ( a / ( q ^ N ) ) /\ ( a / ( q ^ N ) ) <_ ( abs ` ( A - ( p / q ) ) ) ) -> ( if ( a <_ b , a , b ) / ( q ^ N ) ) <_ ( abs ` ( A - ( p / q ) ) ) ) )
44 34 42 43 sylc 
 |-  ( ( ( ( ph /\ ( a e. RR+ /\ b e. RR+ ) ) /\ ( p e. ZZ /\ q e. NN ) ) /\ ( a / ( q ^ N ) ) <_ ( abs ` ( A - ( p / q ) ) ) ) -> ( if ( a <_ b , a , b ) / ( q ^ N ) ) <_ ( abs ` ( A - ( p / q ) ) ) )
45 44 ex 
 |-  ( ( ( ph /\ ( a e. RR+ /\ b e. RR+ ) ) /\ ( p e. ZZ /\ q e. NN ) ) -> ( ( a / ( q ^ N ) ) <_ ( abs ` ( A - ( p / q ) ) ) -> ( if ( a <_ b , a , b ) / ( q ^ N ) ) <_ ( abs ` ( A - ( p / q ) ) ) ) )
46 45 adantr 
 |-  ( ( ( ( ph /\ ( a e. RR+ /\ b e. RR+ ) ) /\ ( p e. ZZ /\ q e. NN ) ) /\ ( F ` ( p / q ) ) = 0 ) -> ( ( a / ( q ^ N ) ) <_ ( abs ` ( A - ( p / q ) ) ) -> ( if ( a <_ b , a , b ) / ( q ^ N ) ) <_ ( abs ` ( A - ( p / q ) ) ) ) )
47 46 orim2d 
 |-  ( ( ( ( ph /\ ( a e. RR+ /\ b e. RR+ ) ) /\ ( p e. ZZ /\ q e. NN ) ) /\ ( F ` ( p / q ) ) = 0 ) -> ( ( A = ( p / q ) \/ ( a / ( q ^ N ) ) <_ ( abs ` ( A - ( p / q ) ) ) ) -> ( A = ( p / q ) \/ ( if ( a <_ b , a , b ) / ( q ^ N ) ) <_ ( abs ` ( A - ( p / q ) ) ) ) ) )
48 13 47 embantd 
 |-  ( ( ( ( ph /\ ( a e. RR+ /\ b e. RR+ ) ) /\ ( p e. ZZ /\ q e. NN ) ) /\ ( F ` ( p / q ) ) = 0 ) -> ( ( ( F ` ( p / q ) ) = 0 -> ( A = ( p / q ) \/ ( a / ( q ^ N ) ) <_ ( abs ` ( A - ( p / q ) ) ) ) ) -> ( A = ( p / q ) \/ ( if ( a <_ b , a , b ) / ( q ^ N ) ) <_ ( abs ` ( A - ( p / q ) ) ) ) ) )
49 48 adantrd 
 |-  ( ( ( ( ph /\ ( a e. RR+ /\ b e. RR+ ) ) /\ ( p e. ZZ /\ q e. NN ) ) /\ ( F ` ( p / q ) ) = 0 ) -> ( ( ( ( F ` ( p / q ) ) = 0 -> ( A = ( p / q ) \/ ( a / ( q ^ N ) ) <_ ( abs ` ( A - ( p / q ) ) ) ) ) /\ ( ( F ` ( p / q ) ) =/= 0 -> ( A = ( p / q ) \/ ( b / ( q ^ N ) ) <_ ( abs ` ( A - ( p / q ) ) ) ) ) ) -> ( A = ( p / q ) \/ ( if ( a <_ b , a , b ) / ( q ^ N ) ) <_ ( abs ` ( A - ( p / q ) ) ) ) ) )
50 simpr 
 |-  ( ( ( ( ph /\ ( a e. RR+ /\ b e. RR+ ) ) /\ ( p e. ZZ /\ q e. NN ) ) /\ ( F ` ( p / q ) ) =/= 0 ) -> ( F ` ( p / q ) ) =/= 0 )
51 37 19 rpdivcld 
 |-  ( ( ( ph /\ ( a e. RR+ /\ b e. RR+ ) ) /\ ( p e. ZZ /\ q e. NN ) ) -> ( b / ( q ^ N ) ) e. RR+ )
52 51 rpred 
 |-  ( ( ( ph /\ ( a e. RR+ /\ b e. RR+ ) ) /\ ( p e. ZZ /\ q e. NN ) ) -> ( b / ( q ^ N ) ) e. RR )
53 21 52 32 3jca 
 |-  ( ( ( ph /\ ( a e. RR+ /\ b e. RR+ ) ) /\ ( p e. ZZ /\ q e. NN ) ) -> ( ( if ( a <_ b , a , b ) / ( q ^ N ) ) e. RR /\ ( b / ( q ^ N ) ) e. RR /\ ( abs ` ( A - ( p / q ) ) ) e. RR ) )
54 53 adantr 
 |-  ( ( ( ( ph /\ ( a e. RR+ /\ b e. RR+ ) ) /\ ( p e. ZZ /\ q e. NN ) ) /\ ( b / ( q ^ N ) ) <_ ( abs ` ( A - ( p / q ) ) ) ) -> ( ( if ( a <_ b , a , b ) / ( q ^ N ) ) e. RR /\ ( b / ( q ^ N ) ) e. RR /\ ( abs ` ( A - ( p / q ) ) ) e. RR ) )
55 min2 
 |-  ( ( a e. RR /\ b e. RR ) -> if ( a <_ b , a , b ) <_ b )
56 36 38 55 syl2anc 
 |-  ( ( ( ph /\ ( a e. RR+ /\ b e. RR+ ) ) /\ ( p e. ZZ /\ q e. NN ) ) -> if ( a <_ b , a , b ) <_ b )
57 35 38 19 56 lediv1dd 
 |-  ( ( ( ph /\ ( a e. RR+ /\ b e. RR+ ) ) /\ ( p e. ZZ /\ q e. NN ) ) -> ( if ( a <_ b , a , b ) / ( q ^ N ) ) <_ ( b / ( q ^ N ) ) )
58 57 anim1i 
 |-  ( ( ( ( ph /\ ( a e. RR+ /\ b e. RR+ ) ) /\ ( p e. ZZ /\ q e. NN ) ) /\ ( b / ( q ^ N ) ) <_ ( abs ` ( A - ( p / q ) ) ) ) -> ( ( if ( a <_ b , a , b ) / ( q ^ N ) ) <_ ( b / ( q ^ N ) ) /\ ( b / ( q ^ N ) ) <_ ( abs ` ( A - ( p / q ) ) ) ) )
59 letr 
 |-  ( ( ( if ( a <_ b , a , b ) / ( q ^ N ) ) e. RR /\ ( b / ( q ^ N ) ) e. RR /\ ( abs ` ( A - ( p / q ) ) ) e. RR ) -> ( ( ( if ( a <_ b , a , b ) / ( q ^ N ) ) <_ ( b / ( q ^ N ) ) /\ ( b / ( q ^ N ) ) <_ ( abs ` ( A - ( p / q ) ) ) ) -> ( if ( a <_ b , a , b ) / ( q ^ N ) ) <_ ( abs ` ( A - ( p / q ) ) ) ) )
60 54 58 59 sylc 
 |-  ( ( ( ( ph /\ ( a e. RR+ /\ b e. RR+ ) ) /\ ( p e. ZZ /\ q e. NN ) ) /\ ( b / ( q ^ N ) ) <_ ( abs ` ( A - ( p / q ) ) ) ) -> ( if ( a <_ b , a , b ) / ( q ^ N ) ) <_ ( abs ` ( A - ( p / q ) ) ) )
61 60 ex 
 |-  ( ( ( ph /\ ( a e. RR+ /\ b e. RR+ ) ) /\ ( p e. ZZ /\ q e. NN ) ) -> ( ( b / ( q ^ N ) ) <_ ( abs ` ( A - ( p / q ) ) ) -> ( if ( a <_ b , a , b ) / ( q ^ N ) ) <_ ( abs ` ( A - ( p / q ) ) ) ) )
62 61 adantr 
 |-  ( ( ( ( ph /\ ( a e. RR+ /\ b e. RR+ ) ) /\ ( p e. ZZ /\ q e. NN ) ) /\ ( F ` ( p / q ) ) =/= 0 ) -> ( ( b / ( q ^ N ) ) <_ ( abs ` ( A - ( p / q ) ) ) -> ( if ( a <_ b , a , b ) / ( q ^ N ) ) <_ ( abs ` ( A - ( p / q ) ) ) ) )
63 62 orim2d 
 |-  ( ( ( ( ph /\ ( a e. RR+ /\ b e. RR+ ) ) /\ ( p e. ZZ /\ q e. NN ) ) /\ ( F ` ( p / q ) ) =/= 0 ) -> ( ( A = ( p / q ) \/ ( b / ( q ^ N ) ) <_ ( abs ` ( A - ( p / q ) ) ) ) -> ( A = ( p / q ) \/ ( if ( a <_ b , a , b ) / ( q ^ N ) ) <_ ( abs ` ( A - ( p / q ) ) ) ) ) )
64 50 63 embantd 
 |-  ( ( ( ( ph /\ ( a e. RR+ /\ b e. RR+ ) ) /\ ( p e. ZZ /\ q e. NN ) ) /\ ( F ` ( p / q ) ) =/= 0 ) -> ( ( ( F ` ( p / q ) ) =/= 0 -> ( A = ( p / q ) \/ ( b / ( q ^ N ) ) <_ ( abs ` ( A - ( p / q ) ) ) ) ) -> ( A = ( p / q ) \/ ( if ( a <_ b , a , b ) / ( q ^ N ) ) <_ ( abs ` ( A - ( p / q ) ) ) ) ) )
65 64 adantld 
 |-  ( ( ( ( ph /\ ( a e. RR+ /\ b e. RR+ ) ) /\ ( p e. ZZ /\ q e. NN ) ) /\ ( F ` ( p / q ) ) =/= 0 ) -> ( ( ( ( F ` ( p / q ) ) = 0 -> ( A = ( p / q ) \/ ( a / ( q ^ N ) ) <_ ( abs ` ( A - ( p / q ) ) ) ) ) /\ ( ( F ` ( p / q ) ) =/= 0 -> ( A = ( p / q ) \/ ( b / ( q ^ N ) ) <_ ( abs ` ( A - ( p / q ) ) ) ) ) ) -> ( A = ( p / q ) \/ ( if ( a <_ b , a , b ) / ( q ^ N ) ) <_ ( abs ` ( A - ( p / q ) ) ) ) ) )
66 49 65 pm2.61dane 
 |-  ( ( ( ph /\ ( a e. RR+ /\ b e. RR+ ) ) /\ ( p e. ZZ /\ q e. NN ) ) -> ( ( ( ( F ` ( p / q ) ) = 0 -> ( A = ( p / q ) \/ ( a / ( q ^ N ) ) <_ ( abs ` ( A - ( p / q ) ) ) ) ) /\ ( ( F ` ( p / q ) ) =/= 0 -> ( A = ( p / q ) \/ ( b / ( q ^ N ) ) <_ ( abs ` ( A - ( p / q ) ) ) ) ) ) -> ( A = ( p / q ) \/ ( if ( a <_ b , a , b ) / ( q ^ N ) ) <_ ( abs ` ( A - ( p / q ) ) ) ) ) )
67 66 ralimdvva 
 |-  ( ( ph /\ ( a e. RR+ /\ b e. RR+ ) ) -> ( A. p e. ZZ A. q e. NN ( ( ( F ` ( p / q ) ) = 0 -> ( A = ( p / q ) \/ ( a / ( q ^ N ) ) <_ ( abs ` ( A - ( p / q ) ) ) ) ) /\ ( ( F ` ( p / q ) ) =/= 0 -> ( A = ( p / q ) \/ ( b / ( q ^ N ) ) <_ ( abs ` ( A - ( p / q ) ) ) ) ) ) -> A. p e. ZZ A. q e. NN ( A = ( p / q ) \/ ( if ( a <_ b , a , b ) / ( q ^ N ) ) <_ ( abs ` ( A - ( p / q ) ) ) ) ) )
68 oveq1 
 |-  ( x = if ( a <_ b , a , b ) -> ( x / ( q ^ N ) ) = ( if ( a <_ b , a , b ) / ( q ^ N ) ) )
69 68 breq1d 
 |-  ( x = if ( a <_ b , a , b ) -> ( ( x / ( q ^ N ) ) <_ ( abs ` ( A - ( p / q ) ) ) <-> ( if ( a <_ b , a , b ) / ( q ^ N ) ) <_ ( abs ` ( A - ( p / q ) ) ) ) )
70 69 orbi2d 
 |-  ( x = if ( a <_ b , a , b ) -> ( ( A = ( p / q ) \/ ( x / ( q ^ N ) ) <_ ( abs ` ( A - ( p / q ) ) ) ) <-> ( A = ( p / q ) \/ ( if ( a <_ b , a , b ) / ( q ^ N ) ) <_ ( abs ` ( A - ( p / q ) ) ) ) ) )
71 70 2ralbidv 
 |-  ( x = if ( a <_ b , a , b ) -> ( A. p e. ZZ A. q e. NN ( A = ( p / q ) \/ ( x / ( q ^ N ) ) <_ ( abs ` ( A - ( p / q ) ) ) ) <-> A. p e. ZZ A. q e. NN ( A = ( p / q ) \/ ( if ( a <_ b , a , b ) / ( q ^ N ) ) <_ ( abs ` ( A - ( p / q ) ) ) ) ) )
72 71 rspcev 
 |-  ( ( if ( a <_ b , a , b ) e. RR+ /\ A. p e. ZZ A. q e. NN ( A = ( p / q ) \/ ( if ( a <_ b , a , b ) / ( q ^ N ) ) <_ ( abs ` ( A - ( p / q ) ) ) ) ) -> E. x e. RR+ A. p e. ZZ A. q e. NN ( A = ( p / q ) \/ ( x / ( q ^ N ) ) <_ ( abs ` ( A - ( p / q ) ) ) ) )
73 12 67 72 syl6an 
 |-  ( ( ph /\ ( a e. RR+ /\ b e. RR+ ) ) -> ( A. p e. ZZ A. q e. NN ( ( ( F ` ( p / q ) ) = 0 -> ( A = ( p / q ) \/ ( a / ( q ^ N ) ) <_ ( abs ` ( A - ( p / q ) ) ) ) ) /\ ( ( F ` ( p / q ) ) =/= 0 -> ( A = ( p / q ) \/ ( b / ( q ^ N ) ) <_ ( abs ` ( A - ( p / q ) ) ) ) ) ) -> E. x e. RR+ A. p e. ZZ A. q e. NN ( A = ( p / q ) \/ ( x / ( q ^ N ) ) <_ ( abs ` ( A - ( p / q ) ) ) ) ) )
74 10 73 biimtrrid 
 |-  ( ( ph /\ ( a e. RR+ /\ b e. RR+ ) ) -> ( ( A. p e. ZZ A. q e. NN ( ( F ` ( p / q ) ) = 0 -> ( 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 ) \/ ( b / ( q ^ N ) ) <_ ( abs ` ( A - ( p / q ) ) ) ) ) ) -> E. x e. RR+ A. p e. ZZ A. q e. NN ( A = ( p / q ) \/ ( x / ( q ^ N ) ) <_ ( abs ` ( A - ( p / q ) ) ) ) ) )
75 74 rexlimdvva 
 |-  ( ph -> ( E. a e. RR+ E. b e. RR+ ( A. p e. ZZ A. q e. NN ( ( F ` ( p / q ) ) = 0 -> ( 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 ) \/ ( b / ( q ^ N ) ) <_ ( abs ` ( A - ( p / q ) ) ) ) ) ) -> E. x e. RR+ A. p e. ZZ A. q e. NN ( A = ( p / q ) \/ ( x / ( q ^ N ) ) <_ ( abs ` ( A - ( p / q ) ) ) ) ) )
76 9 75 mpd 
 |-  ( ph -> E. x e. RR+ A. p e. ZZ A. q e. NN ( A = ( p / q ) \/ ( x / ( q ^ N ) ) <_ ( abs ` ( A - ( p / q ) ) ) ) )