Metamath Proof Explorer

Theorem ostth2

Description: - Lemma for ostth : regular case. (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 ) )
ostth.1 
|- ( ph -> F e. A )
ostth2.2 
|- ( ph -> N e. ( ZZ>= ` 2 ) )
ostth2.3 
|- ( ph -> 1 < ( F ` N ) )
ostth2.4 
|- R = ( ( log ` ( F ` N ) ) / ( log ` N ) )
Assertion ostth2 
|- ( ph -> E. a e. ( 0 (,] 1 ) F = ( y e. QQ |-> ( ( abs ` 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 ostth.1 
 |-  ( ph -> F e. A )
6 ostth2.2 
 |-  ( ph -> N e. ( ZZ>= ` 2 ) )
7 ostth2.3 
 |-  ( ph -> 1 < ( F ` N ) )
8 ostth2.4 
 |-  R = ( ( log ` ( F ` N ) ) / ( log ` N ) )
9 eluz2b2 
 |-  ( N e. ( ZZ>= ` 2 ) <-> ( N e. NN /\ 1 < N ) )
10 6 9 sylib 
 |-  ( ph -> ( N e. NN /\ 1 < N ) )
11 10 simpld 
 |-  ( ph -> N e. NN )
12 nnq 
 |-  ( N e. NN -> N e. QQ )
13 11 12 syl 
 |-  ( ph -> N e. QQ )
14 1 qrngbas 
 |-  QQ = ( Base ` Q )
15 2 14 abvcl 
 |-  ( ( F e. A /\ N e. QQ ) -> ( F ` N ) e. RR )
16 5 13 15 syl2anc 
 |-  ( ph -> ( F ` N ) e. RR )
17 16 7 rplogcld 
 |-  ( ph -> ( log ` ( F ` N ) ) e. RR+ )
18 11 nnred 
 |-  ( ph -> N e. RR )
19 10 simprd 
 |-  ( ph -> 1 < N )
20 18 19 rplogcld 
 |-  ( ph -> ( log ` N ) e. RR+ )
21 17 20 rpdivcld 
 |-  ( ph -> ( ( log ` ( F ` N ) ) / ( log ` N ) ) e. RR+ )
22 8 21 eqeltrid 
 |-  ( ph -> R e. RR+ )
23 22 rpred 
 |-  ( ph -> R e. RR )
24 22 rpgt0d 
 |-  ( ph -> 0 < R )
25 11 nnnn0d 
 |-  ( ph -> N e. NN0 )
26 1 2 qabvle 
 |-  ( ( F e. A /\ N e. NN0 ) -> ( F ` N ) <_ N )
27 5 25 26 syl2anc 
 |-  ( ph -> ( F ` N ) <_ N )
28 11 nnne0d 
 |-  ( ph -> N =/= 0 )
29 1 qrng0 
 |-  0 = ( 0g ` Q )
30 2 14 29 abvgt0 
 |-  ( ( F e. A /\ N e. QQ /\ N =/= 0 ) -> 0 < ( F ` N ) )
31 5 13 28 30 syl3anc 
 |-  ( ph -> 0 < ( F ` N ) )
32 16 31 elrpd 
 |-  ( ph -> ( F ` N ) e. RR+ )
33 32 reeflogd 
 |-  ( ph -> ( exp ` ( log ` ( F ` N ) ) ) = ( F ` N ) )
34 11 nnrpd 
 |-  ( ph -> N e. RR+ )
35 34 reeflogd 
 |-  ( ph -> ( exp ` ( log ` N ) ) = N )
36 27 33 35 3brtr4d 
 |-  ( ph -> ( exp ` ( log ` ( F ` N ) ) ) <_ ( exp ` ( log ` N ) ) )
37 17 rpred 
 |-  ( ph -> ( log ` ( F ` N ) ) e. RR )
38 34 relogcld 
 |-  ( ph -> ( log ` N ) e. RR )
39 efle 
 |-  ( ( ( log ` ( F ` N ) ) e. RR /\ ( log ` N ) e. RR ) -> ( ( log ` ( F ` N ) ) <_ ( log ` N ) <-> ( exp ` ( log ` ( F ` N ) ) ) <_ ( exp ` ( log ` N ) ) ) )
40 37 38 39 syl2anc 
 |-  ( ph -> ( ( log ` ( F ` N ) ) <_ ( log ` N ) <-> ( exp ` ( log ` ( F ` N ) ) ) <_ ( exp ` ( log ` N ) ) ) )
41 36 40 mpbird 
 |-  ( ph -> ( log ` ( F ` N ) ) <_ ( log ` N ) )
42 20 rpcnd 
 |-  ( ph -> ( log ` N ) e. CC )
43 42 mulridd 
 |-  ( ph -> ( ( log ` N ) x. 1 ) = ( log ` N ) )
44 41 43 breqtrrd 
 |-  ( ph -> ( log ` ( F ` N ) ) <_ ( ( log ` N ) x. 1 ) )
45 1red 
 |-  ( ph -> 1 e. RR )
46 37 45 20 ledivmuld 
 |-  ( ph -> ( ( ( log ` ( F ` N ) ) / ( log ` N ) ) <_ 1 <-> ( log ` ( F ` N ) ) <_ ( ( log ` N ) x. 1 ) ) )
47 44 46 mpbird 
 |-  ( ph -> ( ( log ` ( F ` N ) ) / ( log ` N ) ) <_ 1 )
48 8 47 eqbrtrid 
 |-  ( ph -> R <_ 1 )
49 0xr 
 |-  0 e. RR*
50 1re 
 |-  1 e. RR
51 elioc2 
 |-  ( ( 0 e. RR* /\ 1 e. RR ) -> ( R e. ( 0 (,] 1 ) <-> ( R e. RR /\ 0 < R /\ R <_ 1 ) ) )
52 49 50 51 mp2an 
 |-  ( R e. ( 0 (,] 1 ) <-> ( R e. RR /\ 0 < R /\ R <_ 1 ) )
53 23 24 48 52 syl3anbrc 
 |-  ( ph -> R e. ( 0 (,] 1 ) )
54 1 2 qabsabv 
 |-  ( abs |` QQ ) e. A
55 fvres 
 |-  ( y e. QQ -> ( ( abs |` QQ ) ` y ) = ( abs ` y ) )
56 55 oveq1d 
 |-  ( y e. QQ -> ( ( ( abs |` QQ ) ` y ) ^c R ) = ( ( abs ` y ) ^c R ) )
57 56 mpteq2ia 
 |-  ( y e. QQ |-> ( ( ( abs |` QQ ) ` y ) ^c R ) ) = ( y e. QQ |-> ( ( abs ` y ) ^c R ) )
58 57 eqcomi 
 |-  ( y e. QQ |-> ( ( abs ` y ) ^c R ) ) = ( y e. QQ |-> ( ( ( abs |` QQ ) ` y ) ^c R ) )
59 2 14 58 abvcxp 
 |-  ( ( ( abs |` QQ ) e. A /\ R e. ( 0 (,] 1 ) ) -> ( y e. QQ |-> ( ( abs ` y ) ^c R ) ) e. A )
60 54 53 59 sylancr 
 |-  ( ph -> ( y e. QQ |-> ( ( abs ` y ) ^c R ) ) e. A )
61 eluzelz 
 |-  ( z e. ( ZZ>= ` 2 ) -> z e. ZZ )
62 zq 
 |-  ( z e. ZZ -> z e. QQ )
63 fveq2 
 |-  ( y = z -> ( abs ` y ) = ( abs ` z ) )
64 63 oveq1d 
 |-  ( y = z -> ( ( abs ` y ) ^c R ) = ( ( abs ` z ) ^c R ) )
65 eqid 
 |-  ( y e. QQ |-> ( ( abs ` y ) ^c R ) ) = ( y e. QQ |-> ( ( abs ` y ) ^c R ) )
66 ovex 
 |-  ( ( abs ` z ) ^c R ) e. _V
67 64 65 66 fvmpt 
 |-  ( z e. QQ -> ( ( y e. QQ |-> ( ( abs ` y ) ^c R ) ) ` z ) = ( ( abs ` z ) ^c R ) )
68 61 62 67 3syl 
 |-  ( z e. ( ZZ>= ` 2 ) -> ( ( y e. QQ |-> ( ( abs ` y ) ^c R ) ) ` z ) = ( ( abs ` z ) ^c R ) )
69 68 adantl 
 |-  ( ( ph /\ z e. ( ZZ>= ` 2 ) ) -> ( ( y e. QQ |-> ( ( abs ` y ) ^c R ) ) ` z ) = ( ( abs ` z ) ^c R ) )
70 simpr 
 |-  ( ( ph /\ z e. ( ZZ>= ` 2 ) ) -> z e. ( ZZ>= ` 2 ) )
71 eluz2b2 
 |-  ( z e. ( ZZ>= ` 2 ) <-> ( z e. NN /\ 1 < z ) )
72 70 71 sylib 
 |-  ( ( ph /\ z e. ( ZZ>= ` 2 ) ) -> ( z e. NN /\ 1 < z ) )
73 72 simpld 
 |-  ( ( ph /\ z e. ( ZZ>= ` 2 ) ) -> z e. NN )
74 73 nnred 
 |-  ( ( ph /\ z e. ( ZZ>= ` 2 ) ) -> z e. RR )
75 73 nnnn0d 
 |-  ( ( ph /\ z e. ( ZZ>= ` 2 ) ) -> z e. NN0 )
76 75 nn0ge0d 
 |-  ( ( ph /\ z e. ( ZZ>= ` 2 ) ) -> 0 <_ z )
77 74 76 absidd 
 |-  ( ( ph /\ z e. ( ZZ>= ` 2 ) ) -> ( abs ` z ) = z )
78 77 oveq1d 
 |-  ( ( ph /\ z e. ( ZZ>= ` 2 ) ) -> ( ( abs ` z ) ^c R ) = ( z ^c R ) )
79 74 recnd 
 |-  ( ( ph /\ z e. ( ZZ>= ` 2 ) ) -> z e. CC )
80 73 nnne0d 
 |-  ( ( ph /\ z e. ( ZZ>= ` 2 ) ) -> z =/= 0 )
81 22 rpcnd 
 |-  ( ph -> R e. CC )
82 81 adantr 
 |-  ( ( ph /\ z e. ( ZZ>= ` 2 ) ) -> R e. CC )
83 79 80 82 cxpefd 
 |-  ( ( ph /\ z e. ( ZZ>= ` 2 ) ) -> ( z ^c R ) = ( exp ` ( R x. ( log ` z ) ) ) )
84 5 adantr 
 |-  ( ( ph /\ z e. ( ZZ>= ` 2 ) ) -> F e. A )
85 6 adantr 
 |-  ( ( ph /\ z e. ( ZZ>= ` 2 ) ) -> N e. ( ZZ>= ` 2 ) )
86 7 adantr 
 |-  ( ( ph /\ z e. ( ZZ>= ` 2 ) ) -> 1 < ( F ` N ) )
87 eqid 
 |-  ( ( log ` ( F ` z ) ) / ( log ` z ) ) = ( ( log ` ( F ` z ) ) / ( log ` z ) )
88 eqid 
 |-  if ( ( F ` z ) <_ 1 , 1 , ( F ` z ) ) = if ( ( F ` z ) <_ 1 , 1 , ( F ` z ) )
89 eqid 
 |-  ( ( log ` N ) / ( log ` z ) ) = ( ( log ` N ) / ( log ` z ) )
90 1 2 3 4 84 85 86 8 70 87 88 89 ostth2lem4 
 |-  ( ( ph /\ z e. ( ZZ>= ` 2 ) ) -> ( 1 < ( F ` z ) /\ R <_ ( ( log ` ( F ` z ) ) / ( log ` z ) ) ) )
91 90 simprd 
 |-  ( ( ph /\ z e. ( ZZ>= ` 2 ) ) -> R <_ ( ( log ` ( F ` z ) ) / ( log ` z ) ) )
92 90 simpld 
 |-  ( ( ph /\ z e. ( ZZ>= ` 2 ) ) -> 1 < ( F ` z ) )
93 eqid 
 |-  if ( ( F ` N ) <_ 1 , 1 , ( F ` N ) ) = if ( ( F ` N ) <_ 1 , 1 , ( F ` N ) )
94 eqid 
 |-  ( ( log ` z ) / ( log ` N ) ) = ( ( log ` z ) / ( log ` N ) )
95 1 2 3 4 84 70 92 87 85 8 93 94 ostth2lem4 
 |-  ( ( ph /\ z e. ( ZZ>= ` 2 ) ) -> ( 1 < ( F ` N ) /\ ( ( log ` ( F ` z ) ) / ( log ` z ) ) <_ R ) )
96 95 simprd 
 |-  ( ( ph /\ z e. ( ZZ>= ` 2 ) ) -> ( ( log ` ( F ` z ) ) / ( log ` z ) ) <_ R )
97 23 adantr 
 |-  ( ( ph /\ z e. ( ZZ>= ` 2 ) ) -> R e. RR )
98 61 adantl 
 |-  ( ( ph /\ z e. ( ZZ>= ` 2 ) ) -> z e. ZZ )
99 98 62 syl 
 |-  ( ( ph /\ z e. ( ZZ>= ` 2 ) ) -> z e. QQ )
100 2 14 abvcl 
 |-  ( ( F e. A /\ z e. QQ ) -> ( F ` z ) e. RR )
101 84 99 100 syl2anc 
 |-  ( ( ph /\ z e. ( ZZ>= ` 2 ) ) -> ( F ` z ) e. RR )
102 2 14 29 abvgt0 
 |-  ( ( F e. A /\ z e. QQ /\ z =/= 0 ) -> 0 < ( F ` z ) )
103 84 99 80 102 syl3anc 
 |-  ( ( ph /\ z e. ( ZZ>= ` 2 ) ) -> 0 < ( F ` z ) )
104 101 103 elrpd 
 |-  ( ( ph /\ z e. ( ZZ>= ` 2 ) ) -> ( F ` z ) e. RR+ )
105 104 relogcld 
 |-  ( ( ph /\ z e. ( ZZ>= ` 2 ) ) -> ( log ` ( F ` z ) ) e. RR )
106 73 nnrpd 
 |-  ( ( ph /\ z e. ( ZZ>= ` 2 ) ) -> z e. RR+ )
107 106 relogcld 
 |-  ( ( ph /\ z e. ( ZZ>= ` 2 ) ) -> ( log ` z ) e. RR )
108 ef0 
 |-  ( exp ` 0 ) = 1
109 72 simprd 
 |-  ( ( ph /\ z e. ( ZZ>= ` 2 ) ) -> 1 < z )
110 106 reeflogd 
 |-  ( ( ph /\ z e. ( ZZ>= ` 2 ) ) -> ( exp ` ( log ` z ) ) = z )
111 109 110 breqtrrd 
 |-  ( ( ph /\ z e. ( ZZ>= ` 2 ) ) -> 1 < ( exp ` ( log ` z ) ) )
112 108 111 eqbrtrid 
 |-  ( ( ph /\ z e. ( ZZ>= ` 2 ) ) -> ( exp ` 0 ) < ( exp ` ( log ` z ) ) )
113 0re 
 |-  0 e. RR
114 eflt 
 |-  ( ( 0 e. RR /\ ( log ` z ) e. RR ) -> ( 0 < ( log ` z ) <-> ( exp ` 0 ) < ( exp ` ( log ` z ) ) ) )
115 113 107 114 sylancr 
 |-  ( ( ph /\ z e. ( ZZ>= ` 2 ) ) -> ( 0 < ( log ` z ) <-> ( exp ` 0 ) < ( exp ` ( log ` z ) ) ) )
116 112 115 mpbird 
 |-  ( ( ph /\ z e. ( ZZ>= ` 2 ) ) -> 0 < ( log ` z ) )
117 116 gt0ne0d 
 |-  ( ( ph /\ z e. ( ZZ>= ` 2 ) ) -> ( log ` z ) =/= 0 )
118 105 107 117 redivcld 
 |-  ( ( ph /\ z e. ( ZZ>= ` 2 ) ) -> ( ( log ` ( F ` z ) ) / ( log ` z ) ) e. RR )
119 97 118 letri3d 
 |-  ( ( ph /\ z e. ( ZZ>= ` 2 ) ) -> ( R = ( ( log ` ( F ` z ) ) / ( log ` z ) ) <-> ( R <_ ( ( log ` ( F ` z ) ) / ( log ` z ) ) /\ ( ( log ` ( F ` z ) ) / ( log ` z ) ) <_ R ) ) )
120 91 96 119 mpbir2and 
 |-  ( ( ph /\ z e. ( ZZ>= ` 2 ) ) -> R = ( ( log ` ( F ` z ) ) / ( log ` z ) ) )
121 120 oveq1d 
 |-  ( ( ph /\ z e. ( ZZ>= ` 2 ) ) -> ( R x. ( log ` z ) ) = ( ( ( log ` ( F ` z ) ) / ( log ` z ) ) x. ( log ` z ) ) )
122 105 recnd 
 |-  ( ( ph /\ z e. ( ZZ>= ` 2 ) ) -> ( log ` ( F ` z ) ) e. CC )
123 107 recnd 
 |-  ( ( ph /\ z e. ( ZZ>= ` 2 ) ) -> ( log ` z ) e. CC )
124 122 123 117 divcan1d 
 |-  ( ( ph /\ z e. ( ZZ>= ` 2 ) ) -> ( ( ( log ` ( F ` z ) ) / ( log ` z ) ) x. ( log ` z ) ) = ( log ` ( F ` z ) ) )
125 121 124 eqtrd 
 |-  ( ( ph /\ z e. ( ZZ>= ` 2 ) ) -> ( R x. ( log ` z ) ) = ( log ` ( F ` z ) ) )
126 125 fveq2d 
 |-  ( ( ph /\ z e. ( ZZ>= ` 2 ) ) -> ( exp ` ( R x. ( log ` z ) ) ) = ( exp ` ( log ` ( F ` z ) ) ) )
127 104 reeflogd 
 |-  ( ( ph /\ z e. ( ZZ>= ` 2 ) ) -> ( exp ` ( log ` ( F ` z ) ) ) = ( F ` z ) )
128 83 126 127 3eqtrd 
 |-  ( ( ph /\ z e. ( ZZ>= ` 2 ) ) -> ( z ^c R ) = ( F ` z ) )
129 69 78 128 3eqtrrd 
 |-  ( ( ph /\ z e. ( ZZ>= ` 2 ) ) -> ( F ` z ) = ( ( y e. QQ |-> ( ( abs ` y ) ^c R ) ) ` z ) )
130 1 2 5 60 129 ostthlem1 
 |-  ( ph -> F = ( y e. QQ |-> ( ( abs ` y ) ^c R ) ) )
131 oveq2 
 |-  ( a = R -> ( ( abs ` y ) ^c a ) = ( ( abs ` y ) ^c R ) )
132 131 mpteq2dv 
 |-  ( a = R -> ( y e. QQ |-> ( ( abs ` y ) ^c a ) ) = ( y e. QQ |-> ( ( abs ` y ) ^c R ) ) )
133 132 rspceeqv 
 |-  ( ( R e. ( 0 (,] 1 ) /\ F = ( y e. QQ |-> ( ( abs ` y ) ^c R ) ) ) -> E. a e. ( 0 (,] 1 ) F = ( y e. QQ |-> ( ( abs ` y ) ^c a ) ) )
134 53 130 133 syl2anc 
 |-  ( ph -> E. a e. ( 0 (,] 1 ) F = ( y e. QQ |-> ( ( abs ` y ) ^c a ) ) )