Metamath Proof Explorer

Theorem ostth2lem4

Description: Lemma for ostth2 . (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 ) )
ostth2.5 
|- ( ph -> M e. ( ZZ>= ` 2 ) )
ostth2.6 
|- S = ( ( log ` ( F ` M ) ) / ( log ` M ) )
ostth2.7 
|- T = if ( ( F ` M ) <_ 1 , 1 , ( F ` M ) )
ostth2.8 
|- U = ( ( log ` N ) / ( log ` M ) )
Assertion ostth2lem4 
|- ( ph -> ( 1 < ( F ` M ) /\ R <_ S ) )

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 ostth2.5 
 |-  ( ph -> M e. ( ZZ>= ` 2 ) )
10 ostth2.6 
 |-  S = ( ( log ` ( F ` M ) ) / ( log ` M ) )
11 ostth2.7 
 |-  T = if ( ( F ` M ) <_ 1 , 1 , ( F ` M ) )
12 ostth2.8 
 |-  U = ( ( log ` N ) / ( log ` M ) )
13 1re 
 |-  1 e. RR
14 eluz2b2 
 |-  ( N e. ( ZZ>= ` 2 ) <-> ( N e. NN /\ 1 < N ) )
15 6 14 sylib 
 |-  ( ph -> ( N e. NN /\ 1 < N ) )
16 15 simpld 
 |-  ( ph -> N e. NN )
17 nnq 
 |-  ( N e. NN -> N e. QQ )
18 16 17 syl 
 |-  ( ph -> N e. QQ )
19 1 qrngbas 
 |-  QQ = ( Base ` Q )
20 2 19 abvcl 
 |-  ( ( F e. A /\ N e. QQ ) -> ( F ` N ) e. RR )
21 5 18 20 syl2anc 
 |-  ( ph -> ( F ` N ) e. RR )
22 ltnle 
 |-  ( ( 1 e. RR /\ ( F ` N ) e. RR ) -> ( 1 < ( F ` N ) <-> -. ( F ` N ) <_ 1 ) )
23 13 21 22 sylancr 
 |-  ( ph -> ( 1 < ( F ` N ) <-> -. ( F ` N ) <_ 1 ) )
24 7 23 mpbid 
 |-  ( ph -> -. ( F ` N ) <_ 1 )
25 eluz2b2 
 |-  ( M e. ( ZZ>= ` 2 ) <-> ( M e. NN /\ 1 < M ) )
26 9 25 sylib 
 |-  ( ph -> ( M e. NN /\ 1 < M ) )
27 26 simpld 
 |-  ( ph -> M e. NN )
28 nnq 
 |-  ( M e. NN -> M e. QQ )
29 27 28 syl 
 |-  ( ph -> M e. QQ )
30 2 19 abvcl 
 |-  ( ( F e. A /\ M e. QQ ) -> ( F ` M ) e. RR )
31 5 29 30 syl2anc 
 |-  ( ph -> ( F ` M ) e. RR )
32 ifcl 
 |-  ( ( 1 e. RR /\ ( F ` M ) e. RR ) -> if ( ( F ` M ) <_ 1 , 1 , ( F ` M ) ) e. RR )
33 13 31 32 sylancr 
 |-  ( ph -> if ( ( F ` M ) <_ 1 , 1 , ( F ` M ) ) e. RR )
34 11 33 eqeltrid 
 |-  ( ph -> T e. RR )
35 0red 
 |-  ( ph -> 0 e. RR )
36 13 a1i 
 |-  ( ph -> 1 e. RR )
37 0lt1 
 |-  0 < 1
38 37 a1i 
 |-  ( ph -> 0 < 1 )
39 max2 
 |-  ( ( ( F ` M ) e. RR /\ 1 e. RR ) -> 1 <_ if ( ( F ` M ) <_ 1 , 1 , ( F ` M ) ) )
40 31 13 39 sylancl 
 |-  ( ph -> 1 <_ if ( ( F ` M ) <_ 1 , 1 , ( F ` M ) ) )
41 40 11 breqtrrdi 
 |-  ( ph -> 1 <_ T )
42 35 36 34 38 41 ltletrd 
 |-  ( ph -> 0 < T )
43 34 42 elrpd 
 |-  ( ph -> T e. RR+ )
44 16 nnrpd 
 |-  ( ph -> N e. RR+ )
45 44 relogcld 
 |-  ( ph -> ( log ` N ) e. RR )
46 27 nnred 
 |-  ( ph -> M e. RR )
47 26 simprd 
 |-  ( ph -> 1 < M )
48 46 47 rplogcld 
 |-  ( ph -> ( log ` M ) e. RR+ )
49 45 48 rerpdivcld 
 |-  ( ph -> ( ( log ` N ) / ( log ` M ) ) e. RR )
50 12 49 eqeltrid 
 |-  ( ph -> U e. RR )
51 43 50 rpcxpcld 
 |-  ( ph -> ( T ^c U ) e. RR+ )
52 21 51 rerpdivcld 
 |-  ( ph -> ( ( F ` N ) / ( T ^c U ) ) e. RR )
53 46 34 remulcld 
 |-  ( ph -> ( M x. T ) e. RR )
54 peano2re 
 |-  ( U e. RR -> ( U + 1 ) e. RR )
55 50 54 syl 
 |-  ( ph -> ( U + 1 ) e. RR )
56 53 55 remulcld 
 |-  ( ph -> ( ( M x. T ) x. ( U + 1 ) ) e. RR )
57 1 2 3 4 5 6 7 8 9 10 11 12 ostth2lem3 
 |-  ( ( ph /\ n e. NN ) -> ( ( ( F ` N ) / ( T ^c U ) ) ^ n ) <_ ( n x. ( ( M x. T ) x. ( U + 1 ) ) ) )
58 52 56 57 ostth2lem1 
 |-  ( ph -> ( ( F ` N ) / ( T ^c U ) ) <_ 1 )
59 21 36 51 ledivmuld 
 |-  ( ph -> ( ( ( F ` N ) / ( T ^c U ) ) <_ 1 <-> ( F ` N ) <_ ( ( T ^c U ) x. 1 ) ) )
60 58 59 mpbid 
 |-  ( ph -> ( F ` N ) <_ ( ( T ^c U ) x. 1 ) )
61 51 rpcnd 
 |-  ( ph -> ( T ^c U ) e. CC )
62 61 mulid1d 
 |-  ( ph -> ( ( T ^c U ) x. 1 ) = ( T ^c U ) )
63 60 62 breqtrd 
 |-  ( ph -> ( F ` N ) <_ ( T ^c U ) )
64 63 adantr 
 |-  ( ( ph /\ ( F ` M ) <_ 1 ) -> ( F ` N ) <_ ( T ^c U ) )
65 iftrue 
 |-  ( ( F ` M ) <_ 1 -> if ( ( F ` M ) <_ 1 , 1 , ( F ` M ) ) = 1 )
66 11 65 syl5eq 
 |-  ( ( F ` M ) <_ 1 -> T = 1 )
67 66 oveq1d 
 |-  ( ( F ` M ) <_ 1 -> ( T ^c U ) = ( 1 ^c U ) )
68 50 recnd 
 |-  ( ph -> U e. CC )
69 68 1cxpd 
 |-  ( ph -> ( 1 ^c U ) = 1 )
70 67 69 sylan9eqr 
 |-  ( ( ph /\ ( F ` M ) <_ 1 ) -> ( T ^c U ) = 1 )
71 64 70 breqtrd 
 |-  ( ( ph /\ ( F ` M ) <_ 1 ) -> ( F ` N ) <_ 1 )
72 24 71 mtand 
 |-  ( ph -> -. ( F ` M ) <_ 1 )
73 ltnle 
 |-  ( ( 1 e. RR /\ ( F ` M ) e. RR ) -> ( 1 < ( F ` M ) <-> -. ( F ` M ) <_ 1 ) )
74 13 31 73 sylancr 
 |-  ( ph -> ( 1 < ( F ` M ) <-> -. ( F ` M ) <_ 1 ) )
75 72 74 mpbird 
 |-  ( ph -> 1 < ( F ` M ) )
76 35 36 21 38 7 lttrd 
 |-  ( ph -> 0 < ( F ` N ) )
77 21 76 elrpd 
 |-  ( ph -> ( F ` N ) e. RR+ )
78 77 reeflogd 
 |-  ( ph -> ( exp ` ( log ` ( F ` N ) ) ) = ( F ` N ) )
79 iffalse 
 |-  ( -. ( F ` M ) <_ 1 -> if ( ( F ` M ) <_ 1 , 1 , ( F ` M ) ) = ( F ` M ) )
80 11 79 syl5eq 
 |-  ( -. ( F ` M ) <_ 1 -> T = ( F ` M ) )
81 72 80 syl 
 |-  ( ph -> T = ( F ` M ) )
82 81 oveq1d 
 |-  ( ph -> ( T ^c U ) = ( ( F ` M ) ^c U ) )
83 31 recnd 
 |-  ( ph -> ( F ` M ) e. CC )
84 35 36 31 38 75 lttrd 
 |-  ( ph -> 0 < ( F ` M ) )
85 31 84 elrpd 
 |-  ( ph -> ( F ` M ) e. RR+ )
86 85 rpne0d 
 |-  ( ph -> ( F ` M ) =/= 0 )
87 83 86 68 cxpefd 
 |-  ( ph -> ( ( F ` M ) ^c U ) = ( exp ` ( U x. ( log ` ( F ` M ) ) ) ) )
88 82 87 eqtr2d 
 |-  ( ph -> ( exp ` ( U x. ( log ` ( F ` M ) ) ) ) = ( T ^c U ) )
89 63 78 88 3brtr4d 
 |-  ( ph -> ( exp ` ( log ` ( F ` N ) ) ) <_ ( exp ` ( U x. ( log ` ( F ` M ) ) ) ) )
90 77 relogcld 
 |-  ( ph -> ( log ` ( F ` N ) ) e. RR )
91 85 relogcld 
 |-  ( ph -> ( log ` ( F ` M ) ) e. RR )
92 50 91 remulcld 
 |-  ( ph -> ( U x. ( log ` ( F ` M ) ) ) e. RR )
93 efle 
 |-  ( ( ( log ` ( F ` N ) ) e. RR /\ ( U x. ( log ` ( F ` M ) ) ) e. RR ) -> ( ( log ` ( F ` N ) ) <_ ( U x. ( log ` ( F ` M ) ) ) <-> ( exp ` ( log ` ( F ` N ) ) ) <_ ( exp ` ( U x. ( log ` ( F ` M ) ) ) ) ) )
94 90 92 93 syl2anc 
 |-  ( ph -> ( ( log ` ( F ` N ) ) <_ ( U x. ( log ` ( F ` M ) ) ) <-> ( exp ` ( log ` ( F ` N ) ) ) <_ ( exp ` ( U x. ( log ` ( F ` M ) ) ) ) ) )
95 89 94 mpbird 
 |-  ( ph -> ( log ` ( F ` N ) ) <_ ( U x. ( log ` ( F ` M ) ) ) )
96 45 recnd 
 |-  ( ph -> ( log ` N ) e. CC )
97 91 recnd 
 |-  ( ph -> ( log ` ( F ` M ) ) e. CC )
98 48 rpcnd 
 |-  ( ph -> ( log ` M ) e. CC )
99 48 rpne0d 
 |-  ( ph -> ( log ` M ) =/= 0 )
100 96 97 98 99 div12d 
 |-  ( ph -> ( ( log ` N ) x. ( ( log ` ( F ` M ) ) / ( log ` M ) ) ) = ( ( log ` ( F ` M ) ) x. ( ( log ` N ) / ( log ` M ) ) ) )
101 12 oveq2i 
 |-  ( ( log ` ( F ` M ) ) x. U ) = ( ( log ` ( F ` M ) ) x. ( ( log ` N ) / ( log ` M ) ) )
102 100 101 eqtr4di 
 |-  ( ph -> ( ( log ` N ) x. ( ( log ` ( F ` M ) ) / ( log ` M ) ) ) = ( ( log ` ( F ` M ) ) x. U ) )
103 97 68 mulcomd 
 |-  ( ph -> ( ( log ` ( F ` M ) ) x. U ) = ( U x. ( log ` ( F ` M ) ) ) )
104 102 103 eqtrd 
 |-  ( ph -> ( ( log ` N ) x. ( ( log ` ( F ` M ) ) / ( log ` M ) ) ) = ( U x. ( log ` ( F ` M ) ) ) )
105 95 104 breqtrrd 
 |-  ( ph -> ( log ` ( F ` N ) ) <_ ( ( log ` N ) x. ( ( log ` ( F ` M ) ) / ( log ` M ) ) ) )
106 91 48 rerpdivcld 
 |-  ( ph -> ( ( log ` ( F ` M ) ) / ( log ` M ) ) e. RR )
107 16 nnred 
 |-  ( ph -> N e. RR )
108 15 simprd 
 |-  ( ph -> 1 < N )
109 107 108 rplogcld 
 |-  ( ph -> ( log ` N ) e. RR+ )
110 90 106 109 ledivmuld 
 |-  ( ph -> ( ( ( log ` ( F ` N ) ) / ( log ` N ) ) <_ ( ( log ` ( F ` M ) ) / ( log ` M ) ) <-> ( log ` ( F ` N ) ) <_ ( ( log ` N ) x. ( ( log ` ( F ` M ) ) / ( log ` M ) ) ) ) )
111 105 110 mpbird 
 |-  ( ph -> ( ( log ` ( F ` N ) ) / ( log ` N ) ) <_ ( ( log ` ( F ` M ) ) / ( log ` M ) ) )
112 111 8 10 3brtr4g 
 |-  ( ph -> R <_ S )
113 75 112 jca 
 |-  ( ph -> ( 1 < ( F ` M ) /\ R <_ S ) )