Metamath Proof Explorer

Theorem aaliou2

Description: Liouville's approximation theorem for algebraic numbers per se. (Contributed by Stefan O'Rear, 16-Nov-2014)

Ref Expression
Assertion aaliou2 
|- ( A e. ( AA i^i RR ) -> E. k e. NN E. x e. RR+ A. p e. ZZ A. q e. NN ( A = ( p / q ) \/ ( x / ( q ^ k ) ) < ( abs ` ( A - ( p / q ) ) ) ) )

Proof

Step Hyp Ref Expression
1 elin 
 |-  ( A e. ( AA i^i RR ) <-> ( A e. AA /\ A e. RR ) )
2 elaa 
 |-  ( A e. AA <-> ( A e. CC /\ E. a e. ( ( Poly ` ZZ ) \ { 0p } ) ( a ` A ) = 0 ) )
3 eldifn 
 |-  ( a e. ( ( Poly ` ZZ ) \ { 0p } ) -> -. a e. { 0p } )
4 3 3ad2ant1 
 |-  ( ( a e. ( ( Poly ` ZZ ) \ { 0p } ) /\ ( a ` A ) = 0 /\ A e. RR ) -> -. a e. { 0p } )
5 simpr 
 |-  ( ( ( a e. ( ( Poly ` ZZ ) \ { 0p } ) /\ ( a ` A ) = 0 /\ A e. RR ) /\ a = ( CC X. { ( a ` 0 ) } ) ) -> a = ( CC X. { ( a ` 0 ) } ) )
6 fveq1 
 |-  ( a = ( CC X. { ( a ` 0 ) } ) -> ( a ` A ) = ( ( CC X. { ( a ` 0 ) } ) ` A ) )
7 6 adantl 
 |-  ( ( ( a e. ( ( Poly ` ZZ ) \ { 0p } ) /\ ( a ` A ) = 0 /\ A e. RR ) /\ a = ( CC X. { ( a ` 0 ) } ) ) -> ( a ` A ) = ( ( CC X. { ( a ` 0 ) } ) ` A ) )
8 simpl2 
 |-  ( ( ( a e. ( ( Poly ` ZZ ) \ { 0p } ) /\ ( a ` A ) = 0 /\ A e. RR ) /\ a = ( CC X. { ( a ` 0 ) } ) ) -> ( a ` A ) = 0 )
9 simpl3 
 |-  ( ( ( a e. ( ( Poly ` ZZ ) \ { 0p } ) /\ ( a ` A ) = 0 /\ A e. RR ) /\ a = ( CC X. { ( a ` 0 ) } ) ) -> A e. RR )
10 9 recnd 
 |-  ( ( ( a e. ( ( Poly ` ZZ ) \ { 0p } ) /\ ( a ` A ) = 0 /\ A e. RR ) /\ a = ( CC X. { ( a ` 0 ) } ) ) -> A e. CC )
11 fvex 
 |-  ( a ` 0 ) e. _V
12 11 fvconst2 
 |-  ( A e. CC -> ( ( CC X. { ( a ` 0 ) } ) ` A ) = ( a ` 0 ) )
13 10 12 syl 
 |-  ( ( ( a e. ( ( Poly ` ZZ ) \ { 0p } ) /\ ( a ` A ) = 0 /\ A e. RR ) /\ a = ( CC X. { ( a ` 0 ) } ) ) -> ( ( CC X. { ( a ` 0 ) } ) ` A ) = ( a ` 0 ) )
14 7 8 13 3eqtr3rd 
 |-  ( ( ( a e. ( ( Poly ` ZZ ) \ { 0p } ) /\ ( a ` A ) = 0 /\ A e. RR ) /\ a = ( CC X. { ( a ` 0 ) } ) ) -> ( a ` 0 ) = 0 )
15 14 sneqd 
 |-  ( ( ( a e. ( ( Poly ` ZZ ) \ { 0p } ) /\ ( a ` A ) = 0 /\ A e. RR ) /\ a = ( CC X. { ( a ` 0 ) } ) ) -> { ( a ` 0 ) } = { 0 } )
16 15 xpeq2d 
 |-  ( ( ( a e. ( ( Poly ` ZZ ) \ { 0p } ) /\ ( a ` A ) = 0 /\ A e. RR ) /\ a = ( CC X. { ( a ` 0 ) } ) ) -> ( CC X. { ( a ` 0 ) } ) = ( CC X. { 0 } ) )
17 5 16 eqtrd 
 |-  ( ( ( a e. ( ( Poly ` ZZ ) \ { 0p } ) /\ ( a ` A ) = 0 /\ A e. RR ) /\ a = ( CC X. { ( a ` 0 ) } ) ) -> a = ( CC X. { 0 } ) )
18 df-0p 
 |-  0p = ( CC X. { 0 } )
19 17 18 eqtr4di 
 |-  ( ( ( a e. ( ( Poly ` ZZ ) \ { 0p } ) /\ ( a ` A ) = 0 /\ A e. RR ) /\ a = ( CC X. { ( a ` 0 ) } ) ) -> a = 0p )
20 velsn 
 |-  ( a e. { 0p } <-> a = 0p )
21 19 20 sylibr 
 |-  ( ( ( a e. ( ( Poly ` ZZ ) \ { 0p } ) /\ ( a ` A ) = 0 /\ A e. RR ) /\ a = ( CC X. { ( a ` 0 ) } ) ) -> a e. { 0p } )
22 4 21 mtand 
 |-  ( ( a e. ( ( Poly ` ZZ ) \ { 0p } ) /\ ( a ` A ) = 0 /\ A e. RR ) -> -. a = ( CC X. { ( a ` 0 ) } ) )
23 eldifi 
 |-  ( a e. ( ( Poly ` ZZ ) \ { 0p } ) -> a e. ( Poly ` ZZ ) )
24 23 3ad2ant1 
 |-  ( ( a e. ( ( Poly ` ZZ ) \ { 0p } ) /\ ( a ` A ) = 0 /\ A e. RR ) -> a e. ( Poly ` ZZ ) )
25 0dgrb 
 |-  ( a e. ( Poly ` ZZ ) -> ( ( deg ` a ) = 0 <-> a = ( CC X. { ( a ` 0 ) } ) ) )
26 24 25 syl 
 |-  ( ( a e. ( ( Poly ` ZZ ) \ { 0p } ) /\ ( a ` A ) = 0 /\ A e. RR ) -> ( ( deg ` a ) = 0 <-> a = ( CC X. { ( a ` 0 ) } ) ) )
27 22 26 mtbird 
 |-  ( ( a e. ( ( Poly ` ZZ ) \ { 0p } ) /\ ( a ` A ) = 0 /\ A e. RR ) -> -. ( deg ` a ) = 0 )
28 dgrcl 
 |-  ( a e. ( Poly ` ZZ ) -> ( deg ` a ) e. NN0 )
29 24 28 syl 
 |-  ( ( a e. ( ( Poly ` ZZ ) \ { 0p } ) /\ ( a ` A ) = 0 /\ A e. RR ) -> ( deg ` a ) e. NN0 )
30 elnn0 
 |-  ( ( deg ` a ) e. NN0 <-> ( ( deg ` a ) e. NN \/ ( deg ` a ) = 0 ) )
31 29 30 sylib 
 |-  ( ( a e. ( ( Poly ` ZZ ) \ { 0p } ) /\ ( a ` A ) = 0 /\ A e. RR ) -> ( ( deg ` a ) e. NN \/ ( deg ` a ) = 0 ) )
32 orel2 
 |-  ( -. ( deg ` a ) = 0 -> ( ( ( deg ` a ) e. NN \/ ( deg ` a ) = 0 ) -> ( deg ` a ) e. NN ) )
33 27 31 32 sylc 
 |-  ( ( a e. ( ( Poly ` ZZ ) \ { 0p } ) /\ ( a ` A ) = 0 /\ A e. RR ) -> ( deg ` a ) e. NN )
34 eqid 
 |-  ( deg ` a ) = ( deg ` a )
35 simp3 
 |-  ( ( a e. ( ( Poly ` ZZ ) \ { 0p } ) /\ ( a ` A ) = 0 /\ A e. RR ) -> A e. RR )
36 simp2 
 |-  ( ( a e. ( ( Poly ` ZZ ) \ { 0p } ) /\ ( a ` A ) = 0 /\ A e. RR ) -> ( a ` A ) = 0 )
37 34 24 33 35 36 aaliou 
 |-  ( ( a e. ( ( Poly ` ZZ ) \ { 0p } ) /\ ( a ` A ) = 0 /\ A e. RR ) -> E. x e. RR+ A. p e. ZZ A. q e. NN ( A = ( p / q ) \/ ( x / ( q ^ ( deg ` a ) ) ) < ( abs ` ( A - ( p / q ) ) ) ) )
38 oveq2 
 |-  ( k = ( deg ` a ) -> ( q ^ k ) = ( q ^ ( deg ` a ) ) )
39 38 oveq2d 
 |-  ( k = ( deg ` a ) -> ( x / ( q ^ k ) ) = ( x / ( q ^ ( deg ` a ) ) ) )
40 39 breq1d 
 |-  ( k = ( deg ` a ) -> ( ( x / ( q ^ k ) ) < ( abs ` ( A - ( p / q ) ) ) <-> ( x / ( q ^ ( deg ` a ) ) ) < ( abs ` ( A - ( p / q ) ) ) ) )
41 40 orbi2d 
 |-  ( k = ( deg ` a ) -> ( ( A = ( p / q ) \/ ( x / ( q ^ k ) ) < ( abs ` ( A - ( p / q ) ) ) ) <-> ( A = ( p / q ) \/ ( x / ( q ^ ( deg ` a ) ) ) < ( abs ` ( A - ( p / q ) ) ) ) ) )
42 41 2ralbidv 
 |-  ( k = ( deg ` a ) -> ( A. p e. ZZ A. q e. NN ( A = ( p / q ) \/ ( x / ( q ^ k ) ) < ( abs ` ( A - ( p / q ) ) ) ) <-> A. p e. ZZ A. q e. NN ( A = ( p / q ) \/ ( x / ( q ^ ( deg ` a ) ) ) < ( abs ` ( A - ( p / q ) ) ) ) ) )
43 42 rexbidv 
 |-  ( k = ( deg ` a ) -> ( E. x e. RR+ A. p e. ZZ A. q e. NN ( A = ( p / q ) \/ ( x / ( q ^ k ) ) < ( abs ` ( A - ( p / q ) ) ) ) <-> E. x e. RR+ A. p e. ZZ A. q e. NN ( A = ( p / q ) \/ ( x / ( q ^ ( deg ` a ) ) ) < ( abs ` ( A - ( p / q ) ) ) ) ) )
44 43 rspcev 
 |-  ( ( ( deg ` a ) e. NN /\ E. x e. RR+ A. p e. ZZ A. q e. NN ( A = ( p / q ) \/ ( x / ( q ^ ( deg ` a ) ) ) < ( abs ` ( A - ( p / q ) ) ) ) ) -> E. k e. NN E. x e. RR+ A. p e. ZZ A. q e. NN ( A = ( p / q ) \/ ( x / ( q ^ k ) ) < ( abs ` ( A - ( p / q ) ) ) ) )
45 33 37 44 syl2anc 
 |-  ( ( a e. ( ( Poly ` ZZ ) \ { 0p } ) /\ ( a ` A ) = 0 /\ A e. RR ) -> E. k e. NN E. x e. RR+ A. p e. ZZ A. q e. NN ( A = ( p / q ) \/ ( x / ( q ^ k ) ) < ( abs ` ( A - ( p / q ) ) ) ) )
46 45 3exp 
 |-  ( a e. ( ( Poly ` ZZ ) \ { 0p } ) -> ( ( a ` A ) = 0 -> ( A e. RR -> E. k e. NN E. x e. RR+ A. p e. ZZ A. q e. NN ( A = ( p / q ) \/ ( x / ( q ^ k ) ) < ( abs ` ( A - ( p / q ) ) ) ) ) ) )
47 46 rexlimiv 
 |-  ( E. a e. ( ( Poly ` ZZ ) \ { 0p } ) ( a ` A ) = 0 -> ( A e. RR -> E. k e. NN E. x e. RR+ A. p e. ZZ A. q e. NN ( A = ( p / q ) \/ ( x / ( q ^ k ) ) < ( abs ` ( A - ( p / q ) ) ) ) ) )
48 2 47 simplbiim 
 |-  ( A e. AA -> ( A e. RR -> E. k e. NN E. x e. RR+ A. p e. ZZ A. q e. NN ( A = ( p / q ) \/ ( x / ( q ^ k ) ) < ( abs ` ( A - ( p / q ) ) ) ) ) )
49 48 imp 
 |-  ( ( A e. AA /\ A e. RR ) -> E. k e. NN E. x e. RR+ A. p e. ZZ A. q e. NN ( A = ( p / q ) \/ ( x / ( q ^ k ) ) < ( abs ` ( A - ( p / q ) ) ) ) )
50 1 49 sylbi 
 |-  ( A e. ( AA i^i RR ) -> E. k e. NN E. x e. RR+ A. p e. ZZ A. q e. NN ( A = ( p / q ) \/ ( x / ( q ^ k ) ) < ( abs ` ( A - ( p / q ) ) ) ) )