Metamath Proof Explorer

Theorem ostth

Description: Ostrowski's theorem, which classifies all absolute values on QQ . Any such absolute value must either be the trivial absolute value K , a constant exponent 0 < a <_ 1 times the regular absolute value, or a positive exponent times the p-adic absolute value. (Contributed by Mario Carneiro, 10-Sep-2014)

Ref Expression
Hypotheses qrng.q 
|- Q = ( CCfld |`s QQ )
qabsabv.a 
|- A = ( AbsVal ` Q )
padic.j 
|- J = ( q e. Prime |-> ( x e. QQ |-> if ( x = 0 , 0 , ( q ^ -u ( q pCnt x ) ) ) ) )
ostth.k 
|- K = ( x e. QQ |-> if ( x = 0 , 0 , 1 ) )
Assertion ostth 
|- ( F e. A <-> ( F = K \/ E. a e. ( 0 (,] 1 ) F = ( y e. QQ |-> ( ( abs ` y ) ^c a ) ) \/ E. a e. RR+ E. g e. ran J F = ( y e. QQ |-> ( ( g ` y ) ^c a ) ) ) )

Proof

Step Hyp Ref Expression
1 qrng.q 
 |-  Q = ( CCfld |`s QQ )
2 qabsabv.a 
 |-  A = ( AbsVal ` Q )
3 padic.j 
 |-  J = ( q e. Prime |-> ( x e. QQ |-> if ( x = 0 , 0 , ( q ^ -u ( q pCnt x ) ) ) ) )
4 ostth.k 
 |-  K = ( x e. QQ |-> if ( x = 0 , 0 , 1 ) )
5 simpl 
 |-  ( ( F e. A /\ ( n e. NN /\ 1 < ( F ` n ) ) ) -> F e. A )
6 1re 
 |-  1 e. RR
7 6 ltnri 
 |-  -. 1 < 1
8 ax-1ne0 
 |-  1 =/= 0
9 1 qrng1 
 |-  1 = ( 1r ` Q )
10 1 qrng0 
 |-  0 = ( 0g ` Q )
11 2 9 10 abv1z 
 |-  ( ( F e. A /\ 1 =/= 0 ) -> ( F ` 1 ) = 1 )
12 8 11 mpan2 
 |-  ( F e. A -> ( F ` 1 ) = 1 )
13 12 breq2d 
 |-  ( F e. A -> ( 1 < ( F ` 1 ) <-> 1 < 1 ) )
14 7 13 mtbiri 
 |-  ( F e. A -> -. 1 < ( F ` 1 ) )
15 14 adantr 
 |-  ( ( F e. A /\ ( n e. NN /\ 1 < ( F ` n ) ) ) -> -. 1 < ( F ` 1 ) )
16 simprr 
 |-  ( ( F e. A /\ ( n e. NN /\ 1 < ( F ` n ) ) ) -> 1 < ( F ` n ) )
17 fveq2 
 |-  ( n = 1 -> ( F ` n ) = ( F ` 1 ) )
18 17 breq2d 
 |-  ( n = 1 -> ( 1 < ( F ` n ) <-> 1 < ( F ` 1 ) ) )
19 16 18 syl5ibcom 
 |-  ( ( F e. A /\ ( n e. NN /\ 1 < ( F ` n ) ) ) -> ( n = 1 -> 1 < ( F ` 1 ) ) )
20 15 19 mtod 
 |-  ( ( F e. A /\ ( n e. NN /\ 1 < ( F ` n ) ) ) -> -. n = 1 )
21 simprl 
 |-  ( ( F e. A /\ ( n e. NN /\ 1 < ( F ` n ) ) ) -> n e. NN )
22 elnn1uz2 
 |-  ( n e. NN <-> ( n = 1 \/ n e. ( ZZ>= ` 2 ) ) )
23 21 22 sylib 
 |-  ( ( F e. A /\ ( n e. NN /\ 1 < ( F ` n ) ) ) -> ( n = 1 \/ n e. ( ZZ>= ` 2 ) ) )
24 23 ord 
 |-  ( ( F e. A /\ ( n e. NN /\ 1 < ( F ` n ) ) ) -> ( -. n = 1 -> n e. ( ZZ>= ` 2 ) ) )
25 20 24 mpd 
 |-  ( ( F e. A /\ ( n e. NN /\ 1 < ( F ` n ) ) ) -> n e. ( ZZ>= ` 2 ) )
26 eqid 
 |-  ( ( log ` ( F ` n ) ) / ( log ` n ) ) = ( ( log ` ( F ` n ) ) / ( log ` n ) )
27 1 2 3 4 5 25 16 26 ostth2 
 |-  ( ( F e. A /\ ( n e. NN /\ 1 < ( F ` n ) ) ) -> E. a e. ( 0 (,] 1 ) F = ( y e. QQ |-> ( ( abs ` y ) ^c a ) ) )
28 27 rexlimdvaa 
 |-  ( F e. A -> ( E. n e. NN 1 < ( F ` n ) -> E. a e. ( 0 (,] 1 ) F = ( y e. QQ |-> ( ( abs ` y ) ^c a ) ) ) )
29 3mix2 
 |-  ( E. a e. ( 0 (,] 1 ) F = ( y e. QQ |-> ( ( abs ` y ) ^c a ) ) -> ( F = K \/ E. a e. ( 0 (,] 1 ) F = ( y e. QQ |-> ( ( abs ` y ) ^c a ) ) \/ E. a e. RR+ E. g e. ran J F = ( y e. QQ |-> ( ( g ` y ) ^c a ) ) ) )
30 28 29 syl6 
 |-  ( F e. A -> ( E. n e. NN 1 < ( F ` n ) -> ( F = K \/ E. a e. ( 0 (,] 1 ) F = ( y e. QQ |-> ( ( abs ` y ) ^c a ) ) \/ E. a e. RR+ E. g e. ran J F = ( y e. QQ |-> ( ( g ` y ) ^c a ) ) ) ) )
31 ralnex 
 |-  ( A. n e. NN -. 1 < ( F ` n ) <-> -. E. n e. NN 1 < ( F ` n ) )
32 simpll 
 |-  ( ( ( F e. A /\ A. n e. NN -. 1 < ( F ` n ) ) /\ ( p e. Prime /\ ( F ` p ) < 1 ) ) -> F e. A )
33 simplr 
 |-  ( ( ( F e. A /\ A. n e. NN -. 1 < ( F ` n ) ) /\ ( p e. Prime /\ ( F ` p ) < 1 ) ) -> A. n e. NN -. 1 < ( F ` n ) )
34 fveq2 
 |-  ( n = k -> ( F ` n ) = ( F ` k ) )
35 34 breq2d 
 |-  ( n = k -> ( 1 < ( F ` n ) <-> 1 < ( F ` k ) ) )
36 35 notbid 
 |-  ( n = k -> ( -. 1 < ( F ` n ) <-> -. 1 < ( F ` k ) ) )
37 36 cbvralvw 
 |-  ( A. n e. NN -. 1 < ( F ` n ) <-> A. k e. NN -. 1 < ( F ` k ) )
38 33 37 sylib 
 |-  ( ( ( F e. A /\ A. n e. NN -. 1 < ( F ` n ) ) /\ ( p e. Prime /\ ( F ` p ) < 1 ) ) -> A. k e. NN -. 1 < ( F ` k ) )
39 simprl 
 |-  ( ( ( F e. A /\ A. n e. NN -. 1 < ( F ` n ) ) /\ ( p e. Prime /\ ( F ` p ) < 1 ) ) -> p e. Prime )
40 simprr 
 |-  ( ( ( F e. A /\ A. n e. NN -. 1 < ( F ` n ) ) /\ ( p e. Prime /\ ( F ` p ) < 1 ) ) -> ( F ` p ) < 1 )
41 eqid 
 |-  -u ( ( log ` ( F ` p ) ) / ( log ` p ) ) = -u ( ( log ` ( F ` p ) ) / ( log ` p ) )
42 eqid 
 |-  if ( ( F ` p ) <_ ( F ` z ) , ( F ` z ) , ( F ` p ) ) = if ( ( F ` p ) <_ ( F ` z ) , ( F ` z ) , ( F ` p ) )
43 1 2 3 4 32 38 39 40 41 42 ostth3 
 |-  ( ( ( F e. A /\ A. n e. NN -. 1 < ( F ` n ) ) /\ ( p e. Prime /\ ( F ` p ) < 1 ) ) -> E. a e. RR+ F = ( y e. QQ |-> ( ( ( J ` p ) ` y ) ^c a ) ) )
44 43 expr 
 |-  ( ( ( F e. A /\ A. n e. NN -. 1 < ( F ` n ) ) /\ p e. Prime ) -> ( ( F ` p ) < 1 -> E. a e. RR+ F = ( y e. QQ |-> ( ( ( J ` p ) ` y ) ^c a ) ) ) )
45 44 reximdva 
 |-  ( ( F e. A /\ A. n e. NN -. 1 < ( F ` n ) ) -> ( E. p e. Prime ( F ` p ) < 1 -> E. p e. Prime E. a e. RR+ F = ( y e. QQ |-> ( ( ( J ` p ) ` y ) ^c a ) ) ) )
46 1 2 3 padicabvf 
 |-  J : Prime --> A
47 ffn 
 |-  ( J : Prime --> A -> J Fn Prime )
48 fveq1 
 |-  ( g = ( J ` p ) -> ( g ` y ) = ( ( J ` p ) ` y ) )
49 48 oveq1d 
 |-  ( g = ( J ` p ) -> ( ( g ` y ) ^c a ) = ( ( ( J ` p ) ` y ) ^c a ) )
50 49 mpteq2dv 
 |-  ( g = ( J ` p ) -> ( y e. QQ |-> ( ( g ` y ) ^c a ) ) = ( y e. QQ |-> ( ( ( J ` p ) ` y ) ^c a ) ) )
51 50 eqeq2d 
 |-  ( g = ( J ` p ) -> ( F = ( y e. QQ |-> ( ( g ` y ) ^c a ) ) <-> F = ( y e. QQ |-> ( ( ( J ` p ) ` y ) ^c a ) ) ) )
52 51 rexrn 
 |-  ( J Fn Prime -> ( E. g e. ran J F = ( y e. QQ |-> ( ( g ` y ) ^c a ) ) <-> E. p e. Prime F = ( y e. QQ |-> ( ( ( J ` p ) ` y ) ^c a ) ) ) )
53 46 47 52 mp2b 
 |-  ( E. g e. ran J F = ( y e. QQ |-> ( ( g ` y ) ^c a ) ) <-> E. p e. Prime F = ( y e. QQ |-> ( ( ( J ` p ) ` y ) ^c a ) ) )
54 53 rexbii 
 |-  ( E. a e. RR+ E. g e. ran J F = ( y e. QQ |-> ( ( g ` y ) ^c a ) ) <-> E. a e. RR+ E. p e. Prime F = ( y e. QQ |-> ( ( ( J ` p ) ` y ) ^c a ) ) )
55 rexcom 
 |-  ( E. a e. RR+ E. p e. Prime F = ( y e. QQ |-> ( ( ( J ` p ) ` y ) ^c a ) ) <-> E. p e. Prime E. a e. RR+ F = ( y e. QQ |-> ( ( ( J ` p ) ` y ) ^c a ) ) )
56 54 55 bitri 
 |-  ( E. a e. RR+ E. g e. ran J F = ( y e. QQ |-> ( ( g ` y ) ^c a ) ) <-> E. p e. Prime E. a e. RR+ F = ( y e. QQ |-> ( ( ( J ` p ) ` y ) ^c a ) ) )
57 3mix3 
 |-  ( E. a e. RR+ E. g e. ran J F = ( y e. QQ |-> ( ( g ` y ) ^c a ) ) -> ( F = K \/ E. a e. ( 0 (,] 1 ) F = ( y e. QQ |-> ( ( abs ` y ) ^c a ) ) \/ E. a e. RR+ E. g e. ran J F = ( y e. QQ |-> ( ( g ` y ) ^c a ) ) ) )
58 56 57 sylbir 
 |-  ( E. p e. Prime E. a e. RR+ F = ( y e. QQ |-> ( ( ( J ` p ) ` y ) ^c a ) ) -> ( F = K \/ E. a e. ( 0 (,] 1 ) F = ( y e. QQ |-> ( ( abs ` y ) ^c a ) ) \/ E. a e. RR+ E. g e. ran J F = ( y e. QQ |-> ( ( g ` y ) ^c a ) ) ) )
59 45 58 syl6 
 |-  ( ( F e. A /\ A. n e. NN -. 1 < ( F ` n ) ) -> ( E. p e. Prime ( F ` p ) < 1 -> ( F = K \/ E. a e. ( 0 (,] 1 ) F = ( y e. QQ |-> ( ( abs ` y ) ^c a ) ) \/ E. a e. RR+ E. g e. ran J F = ( y e. QQ |-> ( ( g ` y ) ^c a ) ) ) ) )
60 ralnex 
 |-  ( A. p e. Prime -. ( F ` p ) < 1 <-> -. E. p e. Prime ( F ` p ) < 1 )
61 simpl 
 |-  ( ( F e. A /\ ( A. n e. NN -. 1 < ( F ` n ) /\ A. p e. Prime -. ( F ` p ) < 1 ) ) -> F e. A )
62 simprl 
 |-  ( ( F e. A /\ ( A. n e. NN -. 1 < ( F ` n ) /\ A. p e. Prime -. ( F ` p ) < 1 ) ) -> A. n e. NN -. 1 < ( F ` n ) )
63 62 37 sylib 
 |-  ( ( F e. A /\ ( A. n e. NN -. 1 < ( F ` n ) /\ A. p e. Prime -. ( F ` p ) < 1 ) ) -> A. k e. NN -. 1 < ( F ` k ) )
64 simprr 
 |-  ( ( F e. A /\ ( A. n e. NN -. 1 < ( F ` n ) /\ A. p e. Prime -. ( F ` p ) < 1 ) ) -> A. p e. Prime -. ( F ` p ) < 1 )
65 fveq2 
 |-  ( p = k -> ( F ` p ) = ( F ` k ) )
66 65 breq1d 
 |-  ( p = k -> ( ( F ` p ) < 1 <-> ( F ` k ) < 1 ) )
67 66 notbid 
 |-  ( p = k -> ( -. ( F ` p ) < 1 <-> -. ( F ` k ) < 1 ) )
68 67 cbvralvw 
 |-  ( A. p e. Prime -. ( F ` p ) < 1 <-> A. k e. Prime -. ( F ` k ) < 1 )
69 64 68 sylib 
 |-  ( ( F e. A /\ ( A. n e. NN -. 1 < ( F ` n ) /\ A. p e. Prime -. ( F ` p ) < 1 ) ) -> A. k e. Prime -. ( F ` k ) < 1 )
70 1 2 3 4 61 63 69 ostth1 
 |-  ( ( F e. A /\ ( A. n e. NN -. 1 < ( F ` n ) /\ A. p e. Prime -. ( F ` p ) < 1 ) ) -> F = K )
71 70 3mix1d 
 |-  ( ( F e. A /\ ( A. n e. NN -. 1 < ( F ` n ) /\ A. p e. Prime -. ( F ` p ) < 1 ) ) -> ( F = K \/ E. a e. ( 0 (,] 1 ) F = ( y e. QQ |-> ( ( abs ` y ) ^c a ) ) \/ E. a e. RR+ E. g e. ran J F = ( y e. QQ |-> ( ( g ` y ) ^c a ) ) ) )
72 71 expr 
 |-  ( ( F e. A /\ A. n e. NN -. 1 < ( F ` n ) ) -> ( A. p e. Prime -. ( F ` p ) < 1 -> ( F = K \/ E. a e. ( 0 (,] 1 ) F = ( y e. QQ |-> ( ( abs ` y ) ^c a ) ) \/ E. a e. RR+ E. g e. ran J F = ( y e. QQ |-> ( ( g ` y ) ^c a ) ) ) ) )
73 60 72 biimtrrid 
 |-  ( ( F e. A /\ A. n e. NN -. 1 < ( F ` n ) ) -> ( -. E. p e. Prime ( F ` p ) < 1 -> ( F = K \/ E. a e. ( 0 (,] 1 ) F = ( y e. QQ |-> ( ( abs ` y ) ^c a ) ) \/ E. a e. RR+ E. g e. ran J F = ( y e. QQ |-> ( ( g ` y ) ^c a ) ) ) ) )
74 59 73 pm2.61d 
 |-  ( ( F e. A /\ A. n e. NN -. 1 < ( F ` n ) ) -> ( F = K \/ E. a e. ( 0 (,] 1 ) F = ( y e. QQ |-> ( ( abs ` y ) ^c a ) ) \/ E. a e. RR+ E. g e. ran J F = ( y e. QQ |-> ( ( g ` y ) ^c a ) ) ) )
75 74 ex 
 |-  ( F e. A -> ( A. n e. NN -. 1 < ( F ` n ) -> ( F = K \/ E. a e. ( 0 (,] 1 ) F = ( y e. QQ |-> ( ( abs ` y ) ^c a ) ) \/ E. a e. RR+ E. g e. ran J F = ( y e. QQ |-> ( ( g ` y ) ^c a ) ) ) ) )
76 31 75 biimtrrid 
 |-  ( F e. A -> ( -. E. n e. NN 1 < ( F ` n ) -> ( F = K \/ E. a e. ( 0 (,] 1 ) F = ( y e. QQ |-> ( ( abs ` y ) ^c a ) ) \/ E. a e. RR+ E. g e. ran J F = ( y e. QQ |-> ( ( g ` y ) ^c a ) ) ) ) )
77 30 76 pm2.61d 
 |-  ( F e. A -> ( F = K \/ E. a e. ( 0 (,] 1 ) F = ( y e. QQ |-> ( ( abs ` y ) ^c a ) ) \/ E. a e. RR+ E. g e. ran J F = ( y e. QQ |-> ( ( g ` y ) ^c a ) ) ) )
78 id 
 |-  ( F = K -> F = K )
79 1 qdrng 
 |-  Q e. DivRing
80 1 qrngbas 
 |-  QQ = ( Base ` Q )
81 2 80 10 4 abvtriv 
 |-  ( Q e. DivRing -> K e. A )
82 79 81 ax-mp 
 |-  K e. A
83 78 82 eqeltrdi 
 |-  ( F = K -> F e. A )
84 1 2 qabsabv 
 |-  ( abs |` QQ ) e. A
85 fvres 
 |-  ( y e. QQ -> ( ( abs |` QQ ) ` y ) = ( abs ` y ) )
86 85 oveq1d 
 |-  ( y e. QQ -> ( ( ( abs |` QQ ) ` y ) ^c a ) = ( ( abs ` y ) ^c a ) )
87 86 mpteq2ia 
 |-  ( y e. QQ |-> ( ( ( abs |` QQ ) ` y ) ^c a ) ) = ( y e. QQ |-> ( ( abs ` y ) ^c a ) )
88 87 eqcomi 
 |-  ( y e. QQ |-> ( ( abs ` y ) ^c a ) ) = ( y e. QQ |-> ( ( ( abs |` QQ ) ` y ) ^c a ) )
89 2 80 88 abvcxp 
 |-  ( ( ( abs |` QQ ) e. A /\ a e. ( 0 (,] 1 ) ) -> ( y e. QQ |-> ( ( abs ` y ) ^c a ) ) e. A )
90 84 89 mpan 
 |-  ( a e. ( 0 (,] 1 ) -> ( y e. QQ |-> ( ( abs ` y ) ^c a ) ) e. A )
91 eleq1 
 |-  ( F = ( y e. QQ |-> ( ( abs ` y ) ^c a ) ) -> ( F e. A <-> ( y e. QQ |-> ( ( abs ` y ) ^c a ) ) e. A ) )
92 90 91 syl5ibrcom 
 |-  ( a e. ( 0 (,] 1 ) -> ( F = ( y e. QQ |-> ( ( abs ` y ) ^c a ) ) -> F e. A ) )
93 92 rexlimiv 
 |-  ( E. a e. ( 0 (,] 1 ) F = ( y e. QQ |-> ( ( abs ` y ) ^c a ) ) -> F e. A )
94 1 2 3 padicabvcxp 
 |-  ( ( p e. Prime /\ a e. RR+ ) -> ( y e. QQ |-> ( ( ( J ` p ) ` y ) ^c a ) ) e. A )
95 94 ancoms 
 |-  ( ( a e. RR+ /\ p e. Prime ) -> ( y e. QQ |-> ( ( ( J ` p ) ` y ) ^c a ) ) e. A )
96 eleq1 
 |-  ( F = ( y e. QQ |-> ( ( ( J ` p ) ` y ) ^c a ) ) -> ( F e. A <-> ( y e. QQ |-> ( ( ( J ` p ) ` y ) ^c a ) ) e. A ) )
97 95 96 syl5ibrcom 
 |-  ( ( a e. RR+ /\ p e. Prime ) -> ( F = ( y e. QQ |-> ( ( ( J ` p ) ` y ) ^c a ) ) -> F e. A ) )
98 97 rexlimivv 
 |-  ( E. a e. RR+ E. p e. Prime F = ( y e. QQ |-> ( ( ( J ` p ) ` y ) ^c a ) ) -> F e. A )
99 54 98 sylbi 
 |-  ( E. a e. RR+ E. g e. ran J F = ( y e. QQ |-> ( ( g ` y ) ^c a ) ) -> F e. A )
100 83 93 99 3jaoi 
 |-  ( ( F = K \/ E. a e. ( 0 (,] 1 ) F = ( y e. QQ |-> ( ( abs ` y ) ^c a ) ) \/ E. a e. RR+ E. g e. ran J F = ( y e. QQ |-> ( ( g ` y ) ^c a ) ) ) -> F e. A )
101 77 100 impbii 
 |-  ( F e. A <-> ( F = K \/ E. a e. ( 0 (,] 1 ) F = ( y e. QQ |-> ( ( abs ` y ) ^c a ) ) \/ E. a e. RR+ E. g e. ran J F = ( y e. QQ |-> ( ( g ` y ) ^c a ) ) ) )