Metamath Proof Explorer

Theorem aaliou2b

Description: Liouville's approximation theorem extended to complex A . (Contributed by Stefan O'Rear, 20-Nov-2014)

Ref Expression
Assertion aaliou2b 
|- ( A e. AA -> 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 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 ) ) ) ) )
3 1 2 sylbir 
 |-  ( ( 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 ) ) ) ) )
4 1nn 
 |-  1 e. NN
5 aacn 
 |-  ( A e. AA -> A e. CC )
6 5 adantr 
 |-  ( ( A e. AA /\ -. A e. RR ) -> A e. CC )
7 6 imcld 
 |-  ( ( A e. AA /\ -. A e. RR ) -> ( Im ` A ) e. RR )
8 7 recnd 
 |-  ( ( A e. AA /\ -. A e. RR ) -> ( Im ` A ) e. CC )
9 reim0b 
 |-  ( A e. CC -> ( A e. RR <-> ( Im ` A ) = 0 ) )
10 5 9 syl 
 |-  ( A e. AA -> ( A e. RR <-> ( Im ` A ) = 0 ) )
11 10 necon3bbid 
 |-  ( A e. AA -> ( -. A e. RR <-> ( Im ` A ) =/= 0 ) )
12 11 biimpa 
 |-  ( ( A e. AA /\ -. A e. RR ) -> ( Im ` A ) =/= 0 )
13 8 12 absrpcld 
 |-  ( ( A e. AA /\ -. A e. RR ) -> ( abs ` ( Im ` A ) ) e. RR+ )
14 13 rphalfcld 
 |-  ( ( A e. AA /\ -. A e. RR ) -> ( ( abs ` ( Im ` A ) ) / 2 ) e. RR+ )
15 14 adantr 
 |-  ( ( ( A e. AA /\ -. A e. RR ) /\ ( p e. ZZ /\ q e. NN ) ) -> ( ( abs ` ( Im ` A ) ) / 2 ) e. RR+ )
16 1nn0 
 |-  1 e. NN0
17 nnexpcl 
 |-  ( ( q e. NN /\ 1 e. NN0 ) -> ( q ^ 1 ) e. NN )
18 16 17 mpan2 
 |-  ( q e. NN -> ( q ^ 1 ) e. NN )
19 18 ad2antll 
 |-  ( ( ( A e. AA /\ -. A e. RR ) /\ ( p e. ZZ /\ q e. NN ) ) -> ( q ^ 1 ) e. NN )
20 19 nnrpd 
 |-  ( ( ( A e. AA /\ -. A e. RR ) /\ ( p e. ZZ /\ q e. NN ) ) -> ( q ^ 1 ) e. RR+ )
21 15 20 rpdivcld 
 |-  ( ( ( A e. AA /\ -. A e. RR ) /\ ( p e. ZZ /\ q e. NN ) ) -> ( ( ( abs ` ( Im ` A ) ) / 2 ) / ( q ^ 1 ) ) e. RR+ )
22 21 rpred 
 |-  ( ( ( A e. AA /\ -. A e. RR ) /\ ( p e. ZZ /\ q e. NN ) ) -> ( ( ( abs ` ( Im ` A ) ) / 2 ) / ( q ^ 1 ) ) e. RR )
23 15 rpred 
 |-  ( ( ( A e. AA /\ -. A e. RR ) /\ ( p e. ZZ /\ q e. NN ) ) -> ( ( abs ` ( Im ` A ) ) / 2 ) e. RR )
24 6 adantr 
 |-  ( ( ( A e. AA /\ -. A e. RR ) /\ ( p e. ZZ /\ q e. NN ) ) -> A e. CC )
25 znq 
 |-  ( ( p e. ZZ /\ q e. NN ) -> ( p / q ) e. QQ )
26 25 adantl 
 |-  ( ( ( A e. AA /\ -. A e. RR ) /\ ( p e. ZZ /\ q e. NN ) ) -> ( p / q ) e. QQ )
27 qre 
 |-  ( ( p / q ) e. QQ -> ( p / q ) e. RR )
28 26 27 syl 
 |-  ( ( ( A e. AA /\ -. A e. RR ) /\ ( p e. ZZ /\ q e. NN ) ) -> ( p / q ) e. RR )
29 28 recnd 
 |-  ( ( ( A e. AA /\ -. A e. RR ) /\ ( p e. ZZ /\ q e. NN ) ) -> ( p / q ) e. CC )
30 24 29 subcld 
 |-  ( ( ( A e. AA /\ -. A e. RR ) /\ ( p e. ZZ /\ q e. NN ) ) -> ( A - ( p / q ) ) e. CC )
31 30 abscld 
 |-  ( ( ( A e. AA /\ -. A e. RR ) /\ ( p e. ZZ /\ q e. NN ) ) -> ( abs ` ( A - ( p / q ) ) ) e. RR )
32 19 nnge1d 
 |-  ( ( ( A e. AA /\ -. A e. RR ) /\ ( p e. ZZ /\ q e. NN ) ) -> 1 <_ ( q ^ 1 ) )
33 1rp 
 |-  1 e. RR+
34 rpregt0 
 |-  ( 1 e. RR+ -> ( 1 e. RR /\ 0 < 1 ) )
35 33 34 mp1i 
 |-  ( ( ( A e. AA /\ -. A e. RR ) /\ ( p e. ZZ /\ q e. NN ) ) -> ( 1 e. RR /\ 0 < 1 ) )
36 20 rpregt0d 
 |-  ( ( ( A e. AA /\ -. A e. RR ) /\ ( p e. ZZ /\ q e. NN ) ) -> ( ( q ^ 1 ) e. RR /\ 0 < ( q ^ 1 ) ) )
37 15 rpregt0d 
 |-  ( ( ( A e. AA /\ -. A e. RR ) /\ ( p e. ZZ /\ q e. NN ) ) -> ( ( ( abs ` ( Im ` A ) ) / 2 ) e. RR /\ 0 < ( ( abs ` ( Im ` A ) ) / 2 ) ) )
38 lediv2 
 |-  ( ( ( 1 e. RR /\ 0 < 1 ) /\ ( ( q ^ 1 ) e. RR /\ 0 < ( q ^ 1 ) ) /\ ( ( ( abs ` ( Im ` A ) ) / 2 ) e. RR /\ 0 < ( ( abs ` ( Im ` A ) ) / 2 ) ) ) -> ( 1 <_ ( q ^ 1 ) <-> ( ( ( abs ` ( Im ` A ) ) / 2 ) / ( q ^ 1 ) ) <_ ( ( ( abs ` ( Im ` A ) ) / 2 ) / 1 ) ) )
39 35 36 37 38 syl3anc 
 |-  ( ( ( A e. AA /\ -. A e. RR ) /\ ( p e. ZZ /\ q e. NN ) ) -> ( 1 <_ ( q ^ 1 ) <-> ( ( ( abs ` ( Im ` A ) ) / 2 ) / ( q ^ 1 ) ) <_ ( ( ( abs ` ( Im ` A ) ) / 2 ) / 1 ) ) )
40 32 39 mpbid 
 |-  ( ( ( A e. AA /\ -. A e. RR ) /\ ( p e. ZZ /\ q e. NN ) ) -> ( ( ( abs ` ( Im ` A ) ) / 2 ) / ( q ^ 1 ) ) <_ ( ( ( abs ` ( Im ` A ) ) / 2 ) / 1 ) )
41 15 rpcnd 
 |-  ( ( ( A e. AA /\ -. A e. RR ) /\ ( p e. ZZ /\ q e. NN ) ) -> ( ( abs ` ( Im ` A ) ) / 2 ) e. CC )
42 41 div1d 
 |-  ( ( ( A e. AA /\ -. A e. RR ) /\ ( p e. ZZ /\ q e. NN ) ) -> ( ( ( abs ` ( Im ` A ) ) / 2 ) / 1 ) = ( ( abs ` ( Im ` A ) ) / 2 ) )
43 40 42 breqtrd 
 |-  ( ( ( A e. AA /\ -. A e. RR ) /\ ( p e. ZZ /\ q e. NN ) ) -> ( ( ( abs ` ( Im ` A ) ) / 2 ) / ( q ^ 1 ) ) <_ ( ( abs ` ( Im ` A ) ) / 2 ) )
44 13 adantr 
 |-  ( ( ( A e. AA /\ -. A e. RR ) /\ ( p e. ZZ /\ q e. NN ) ) -> ( abs ` ( Im ` A ) ) e. RR+ )
45 44 rpred 
 |-  ( ( ( A e. AA /\ -. A e. RR ) /\ ( p e. ZZ /\ q e. NN ) ) -> ( abs ` ( Im ` A ) ) e. RR )
46 rphalflt 
 |-  ( ( abs ` ( Im ` A ) ) e. RR+ -> ( ( abs ` ( Im ` A ) ) / 2 ) < ( abs ` ( Im ` A ) ) )
47 44 46 syl 
 |-  ( ( ( A e. AA /\ -. A e. RR ) /\ ( p e. ZZ /\ q e. NN ) ) -> ( ( abs ` ( Im ` A ) ) / 2 ) < ( abs ` ( Im ` A ) ) )
48 24 29 imsubd 
 |-  ( ( ( A e. AA /\ -. A e. RR ) /\ ( p e. ZZ /\ q e. NN ) ) -> ( Im ` ( A - ( p / q ) ) ) = ( ( Im ` A ) - ( Im ` ( p / q ) ) ) )
49 28 reim0d 
 |-  ( ( ( A e. AA /\ -. A e. RR ) /\ ( p e. ZZ /\ q e. NN ) ) -> ( Im ` ( p / q ) ) = 0 )
50 49 oveq2d 
 |-  ( ( ( A e. AA /\ -. A e. RR ) /\ ( p e. ZZ /\ q e. NN ) ) -> ( ( Im ` A ) - ( Im ` ( p / q ) ) ) = ( ( Im ` A ) - 0 ) )
51 8 adantr 
 |-  ( ( ( A e. AA /\ -. A e. RR ) /\ ( p e. ZZ /\ q e. NN ) ) -> ( Im ` A ) e. CC )
52 51 subid1d 
 |-  ( ( ( A e. AA /\ -. A e. RR ) /\ ( p e. ZZ /\ q e. NN ) ) -> ( ( Im ` A ) - 0 ) = ( Im ` A ) )
53 48 50 52 3eqtrd 
 |-  ( ( ( A e. AA /\ -. A e. RR ) /\ ( p e. ZZ /\ q e. NN ) ) -> ( Im ` ( A - ( p / q ) ) ) = ( Im ` A ) )
54 53 fveq2d 
 |-  ( ( ( A e. AA /\ -. A e. RR ) /\ ( p e. ZZ /\ q e. NN ) ) -> ( abs ` ( Im ` ( A - ( p / q ) ) ) ) = ( abs ` ( Im ` A ) ) )
55 absimle 
 |-  ( ( A - ( p / q ) ) e. CC -> ( abs ` ( Im ` ( A - ( p / q ) ) ) ) <_ ( abs ` ( A - ( p / q ) ) ) )
56 30 55 syl 
 |-  ( ( ( A e. AA /\ -. A e. RR ) /\ ( p e. ZZ /\ q e. NN ) ) -> ( abs ` ( Im ` ( A - ( p / q ) ) ) ) <_ ( abs ` ( A - ( p / q ) ) ) )
57 54 56 eqbrtrrd 
 |-  ( ( ( A e. AA /\ -. A e. RR ) /\ ( p e. ZZ /\ q e. NN ) ) -> ( abs ` ( Im ` A ) ) <_ ( abs ` ( A - ( p / q ) ) ) )
58 23 45 31 47 57 ltletrd 
 |-  ( ( ( A e. AA /\ -. A e. RR ) /\ ( p e. ZZ /\ q e. NN ) ) -> ( ( abs ` ( Im ` A ) ) / 2 ) < ( abs ` ( A - ( p / q ) ) ) )
59 22 23 31 43 58 lelttrd 
 |-  ( ( ( A e. AA /\ -. A e. RR ) /\ ( p e. ZZ /\ q e. NN ) ) -> ( ( ( abs ` ( Im ` A ) ) / 2 ) / ( q ^ 1 ) ) < ( abs ` ( A - ( p / q ) ) ) )
60 59 olcd 
 |-  ( ( ( A e. AA /\ -. A e. RR ) /\ ( p e. ZZ /\ q e. NN ) ) -> ( A = ( p / q ) \/ ( ( ( abs ` ( Im ` A ) ) / 2 ) / ( q ^ 1 ) ) < ( abs ` ( A - ( p / q ) ) ) ) )
61 60 ralrimivva 
 |-  ( ( A e. AA /\ -. A e. RR ) -> A. p e. ZZ A. q e. NN ( A = ( p / q ) \/ ( ( ( abs ` ( Im ` A ) ) / 2 ) / ( q ^ 1 ) ) < ( abs ` ( A - ( p / q ) ) ) ) )
62 oveq2 
 |-  ( k = 1 -> ( q ^ k ) = ( q ^ 1 ) )
63 62 oveq2d 
 |-  ( k = 1 -> ( x / ( q ^ k ) ) = ( x / ( q ^ 1 ) ) )
64 63 breq1d 
 |-  ( k = 1 -> ( ( x / ( q ^ k ) ) < ( abs ` ( A - ( p / q ) ) ) <-> ( x / ( q ^ 1 ) ) < ( abs ` ( A - ( p / q ) ) ) ) )
65 64 orbi2d 
 |-  ( k = 1 -> ( ( A = ( p / q ) \/ ( x / ( q ^ k ) ) < ( abs ` ( A - ( p / q ) ) ) ) <-> ( A = ( p / q ) \/ ( x / ( q ^ 1 ) ) < ( abs ` ( A - ( p / q ) ) ) ) ) )
66 65 2ralbidv 
 |-  ( k = 1 -> ( 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 ^ 1 ) ) < ( abs ` ( A - ( p / q ) ) ) ) ) )
67 oveq1 
 |-  ( x = ( ( abs ` ( Im ` A ) ) / 2 ) -> ( x / ( q ^ 1 ) ) = ( ( ( abs ` ( Im ` A ) ) / 2 ) / ( q ^ 1 ) ) )
68 67 breq1d 
 |-  ( x = ( ( abs ` ( Im ` A ) ) / 2 ) -> ( ( x / ( q ^ 1 ) ) < ( abs ` ( A - ( p / q ) ) ) <-> ( ( ( abs ` ( Im ` A ) ) / 2 ) / ( q ^ 1 ) ) < ( abs ` ( A - ( p / q ) ) ) ) )
69 68 orbi2d 
 |-  ( x = ( ( abs ` ( Im ` A ) ) / 2 ) -> ( ( A = ( p / q ) \/ ( x / ( q ^ 1 ) ) < ( abs ` ( A - ( p / q ) ) ) ) <-> ( A = ( p / q ) \/ ( ( ( abs ` ( Im ` A ) ) / 2 ) / ( q ^ 1 ) ) < ( abs ` ( A - ( p / q ) ) ) ) ) )
70 69 2ralbidv 
 |-  ( x = ( ( abs ` ( Im ` A ) ) / 2 ) -> ( A. p e. ZZ A. q e. NN ( A = ( p / q ) \/ ( x / ( q ^ 1 ) ) < ( abs ` ( A - ( p / q ) ) ) ) <-> A. p e. ZZ A. q e. NN ( A = ( p / q ) \/ ( ( ( abs ` ( Im ` A ) ) / 2 ) / ( q ^ 1 ) ) < ( abs ` ( A - ( p / q ) ) ) ) ) )
71 66 70 rspc2ev 
 |-  ( ( 1 e. NN /\ ( ( abs ` ( Im ` A ) ) / 2 ) e. RR+ /\ A. p e. ZZ A. q e. NN ( A = ( p / q ) \/ ( ( ( abs ` ( Im ` A ) ) / 2 ) / ( q ^ 1 ) ) < ( 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 ) ) ) ) )
72 4 14 61 71 mp3an2i 
 |-  ( ( 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 ) ) ) ) )
73 3 72 pm2.61dan 
 |-  ( A e. AA -> 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 ) ) ) ) )