Metamath Proof Explorer

Theorem aaliou

Description: Liouville's theorem on diophantine approximation: Any algebraic number, being a root of a polynomial F in integer coefficients, is not approximable beyond order N = deg ( F ) by rational numbers. In this form, it also applies to rational numbers themselves, which are not well approximable by other rational numbers. This is Metamath 100 proof #18. (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 aaliou 
|- ( 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 5 aalioulem6 
 |-  ( ph -> E. a e. RR+ A. p e. ZZ A. q e. NN ( A = ( p / q ) \/ ( a / ( q ^ N ) ) <_ ( abs ` ( A - ( p / q ) ) ) ) )
7 rphalfcl 
 |-  ( a e. RR+ -> ( a / 2 ) e. RR+ )
8 7 adantl 
 |-  ( ( ph /\ a e. RR+ ) -> ( a / 2 ) e. RR+ )
9 7 ad2antlr 
 |-  ( ( ( ph /\ a e. RR+ ) /\ ( p e. ZZ /\ q e. NN ) ) -> ( a / 2 ) e. RR+ )
10 nnrp 
 |-  ( q e. NN -> q e. RR+ )
11 10 ad2antll 
 |-  ( ( ( ph /\ a e. RR+ ) /\ ( p e. ZZ /\ q e. NN ) ) -> q e. RR+ )
12 3 nnzd 
 |-  ( ph -> N e. ZZ )
13 12 ad2antrr 
 |-  ( ( ( ph /\ a e. RR+ ) /\ ( p e. ZZ /\ q e. NN ) ) -> N e. ZZ )
14 11 13 rpexpcld 
 |-  ( ( ( ph /\ a e. RR+ ) /\ ( p e. ZZ /\ q e. NN ) ) -> ( q ^ N ) e. RR+ )
15 9 14 rpdivcld 
 |-  ( ( ( ph /\ a e. RR+ ) /\ ( p e. ZZ /\ q e. NN ) ) -> ( ( a / 2 ) / ( q ^ N ) ) e. RR+ )
16 15 rpred 
 |-  ( ( ( ph /\ a e. RR+ ) /\ ( p e. ZZ /\ q e. NN ) ) -> ( ( a / 2 ) / ( q ^ N ) ) e. RR )
17 simplr 
 |-  ( ( ( ph /\ a e. RR+ ) /\ ( p e. ZZ /\ q e. NN ) ) -> a e. RR+ )
18 17 14 rpdivcld 
 |-  ( ( ( ph /\ a e. RR+ ) /\ ( p e. ZZ /\ q e. NN ) ) -> ( a / ( q ^ N ) ) e. RR+ )
19 18 rpred 
 |-  ( ( ( ph /\ a e. RR+ ) /\ ( p e. ZZ /\ q e. NN ) ) -> ( a / ( q ^ N ) ) e. RR )
20 4 adantr 
 |-  ( ( ph /\ a e. RR+ ) -> A e. RR )
21 znq 
 |-  ( ( p e. ZZ /\ q e. NN ) -> ( p / q ) e. QQ )
22 qre 
 |-  ( ( p / q ) e. QQ -> ( p / q ) e. RR )
23 21 22 syl 
 |-  ( ( p e. ZZ /\ q e. NN ) -> ( p / q ) e. RR )
24 resubcl 
 |-  ( ( A e. RR /\ ( p / q ) e. RR ) -> ( A - ( p / q ) ) e. RR )
25 20 23 24 syl2an 
 |-  ( ( ( ph /\ a e. RR+ ) /\ ( p e. ZZ /\ q e. NN ) ) -> ( A - ( p / q ) ) e. RR )
26 25 recnd 
 |-  ( ( ( ph /\ a e. RR+ ) /\ ( p e. ZZ /\ q e. NN ) ) -> ( A - ( p / q ) ) e. CC )
27 26 abscld 
 |-  ( ( ( ph /\ a e. RR+ ) /\ ( p e. ZZ /\ q e. NN ) ) -> ( abs ` ( A - ( p / q ) ) ) e. RR )
28 16 19 27 3jca 
 |-  ( ( ( ph /\ a e. RR+ ) /\ ( p e. ZZ /\ q e. NN ) ) -> ( ( ( a / 2 ) / ( q ^ N ) ) e. RR /\ ( a / ( q ^ N ) ) e. RR /\ ( abs ` ( A - ( p / q ) ) ) e. RR ) )
29 9 rpred 
 |-  ( ( ( ph /\ a e. RR+ ) /\ ( p e. ZZ /\ q e. NN ) ) -> ( a / 2 ) e. RR )
30 rpre 
 |-  ( a e. RR+ -> a e. RR )
31 30 ad2antlr 
 |-  ( ( ( ph /\ a e. RR+ ) /\ ( p e. ZZ /\ q e. NN ) ) -> a e. RR )
32 rphalflt 
 |-  ( a e. RR+ -> ( a / 2 ) < a )
33 32 ad2antlr 
 |-  ( ( ( ph /\ a e. RR+ ) /\ ( p e. ZZ /\ q e. NN ) ) -> ( a / 2 ) < a )
34 29 31 14 33 ltdiv1dd 
 |-  ( ( ( ph /\ a e. RR+ ) /\ ( p e. ZZ /\ q e. NN ) ) -> ( ( a / 2 ) / ( q ^ N ) ) < ( a / ( q ^ N ) ) )
35 34 anim1i 
 |-  ( ( ( ( ph /\ a e. RR+ ) /\ ( p e. ZZ /\ q e. NN ) ) /\ ( a / ( q ^ N ) ) <_ ( abs ` ( A - ( p / q ) ) ) ) -> ( ( ( a / 2 ) / ( q ^ N ) ) < ( a / ( q ^ N ) ) /\ ( a / ( q ^ N ) ) <_ ( abs ` ( A - ( p / q ) ) ) ) )
36 35 ex 
 |-  ( ( ( ph /\ a e. RR+ ) /\ ( p e. ZZ /\ q e. NN ) ) -> ( ( a / ( q ^ N ) ) <_ ( abs ` ( A - ( p / q ) ) ) -> ( ( ( a / 2 ) / ( q ^ N ) ) < ( a / ( q ^ N ) ) /\ ( a / ( q ^ N ) ) <_ ( abs ` ( A - ( p / q ) ) ) ) ) )
37 ltletr 
 |-  ( ( ( ( a / 2 ) / ( q ^ N ) ) e. RR /\ ( a / ( q ^ N ) ) e. RR /\ ( abs ` ( A - ( p / q ) ) ) e. RR ) -> ( ( ( ( a / 2 ) / ( q ^ N ) ) < ( a / ( q ^ N ) ) /\ ( a / ( q ^ N ) ) <_ ( abs ` ( A - ( p / q ) ) ) ) -> ( ( a / 2 ) / ( q ^ N ) ) < ( abs ` ( A - ( p / q ) ) ) ) )
38 28 36 37 sylsyld 
 |-  ( ( ( ph /\ a e. RR+ ) /\ ( p e. ZZ /\ q e. NN ) ) -> ( ( a / ( q ^ N ) ) <_ ( abs ` ( A - ( p / q ) ) ) -> ( ( a / 2 ) / ( q ^ N ) ) < ( abs ` ( A - ( p / q ) ) ) ) )
39 38 orim2d 
 |-  ( ( ( ph /\ a e. RR+ ) /\ ( p e. ZZ /\ q e. NN ) ) -> ( ( A = ( p / q ) \/ ( a / ( q ^ N ) ) <_ ( abs ` ( A - ( p / q ) ) ) ) -> ( A = ( p / q ) \/ ( ( a / 2 ) / ( q ^ N ) ) < ( abs ` ( A - ( p / q ) ) ) ) ) )
40 39 ralimdvva 
 |-  ( ( ph /\ a e. RR+ ) -> ( A. p e. ZZ A. q e. NN ( A = ( p / q ) \/ ( a / ( q ^ N ) ) <_ ( abs ` ( A - ( p / q ) ) ) ) -> A. p e. ZZ A. q e. NN ( A = ( p / q ) \/ ( ( a / 2 ) / ( q ^ N ) ) < ( abs ` ( A - ( p / q ) ) ) ) ) )
41 oveq1 
 |-  ( x = ( a / 2 ) -> ( x / ( q ^ N ) ) = ( ( a / 2 ) / ( q ^ N ) ) )
42 41 breq1d 
 |-  ( x = ( a / 2 ) -> ( ( x / ( q ^ N ) ) < ( abs ` ( A - ( p / q ) ) ) <-> ( ( a / 2 ) / ( q ^ N ) ) < ( abs ` ( A - ( p / q ) ) ) ) )
43 42 orbi2d 
 |-  ( x = ( a / 2 ) -> ( ( A = ( p / q ) \/ ( x / ( q ^ N ) ) < ( abs ` ( A - ( p / q ) ) ) ) <-> ( A = ( p / q ) \/ ( ( a / 2 ) / ( q ^ N ) ) < ( abs ` ( A - ( p / q ) ) ) ) ) )
44 43 2ralbidv 
 |-  ( x = ( a / 2 ) -> ( 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 ) \/ ( ( a / 2 ) / ( q ^ N ) ) < ( abs ` ( A - ( p / q ) ) ) ) ) )
45 44 rspcev 
 |-  ( ( ( a / 2 ) e. RR+ /\ A. p e. ZZ A. q e. NN ( A = ( p / q ) \/ ( ( a / 2 ) / ( 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 ) ) ) ) )
46 8 40 45 syl6an 
 |-  ( ( ph /\ a e. RR+ ) -> ( A. p e. ZZ A. q e. NN ( A = ( p / q ) \/ ( a / ( 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 ) ) ) ) ) )
47 46 rexlimdva 
 |-  ( ph -> ( E. a e. RR+ A. p e. ZZ A. q e. NN ( A = ( p / q ) \/ ( a / ( 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 ) ) ) ) ) )
48 6 47 mpd 
 |-  ( ph -> E. x e. RR+ A. p e. ZZ A. q e. NN ( A = ( p / q ) \/ ( x / ( q ^ N ) ) < ( abs ` ( A - ( p / q ) ) ) ) )