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 syl5bir
 |-  ( ( 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 syl5bir
 |-  ( 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 ) ) ) )