Metamath Proof Explorer

Theorem ostth2lem3

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 ostth2lem3 
|- ( ( ph /\ X e. NN ) -> ( ( ( F ` N ) / ( T ^c U ) ) ^ X ) <_ ( X x. ( ( M x. T ) x. ( U + 1 ) ) ) )

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 eluz2b2 
 |-  ( N e. ( ZZ>= ` 2 ) <-> ( N e. NN /\ 1 < N ) )
14 6 13 sylib 
 |-  ( ph -> ( N e. NN /\ 1 < N ) )
15 14 simpld 
 |-  ( ph -> N e. NN )
16 nnq 
 |-  ( N e. NN -> N e. QQ )
17 15 16 syl 
 |-  ( ph -> N e. QQ )
18 1 qrngbas 
 |-  QQ = ( Base ` Q )
19 2 18 abvcl 
 |-  ( ( F e. A /\ N e. QQ ) -> ( F ` N ) e. RR )
20 5 17 19 syl2anc 
 |-  ( ph -> ( F ` N ) e. RR )
21 20 adantr 
 |-  ( ( ph /\ X e. NN ) -> ( F ` N ) e. RR )
22 21 recnd 
 |-  ( ( ph /\ X e. NN ) -> ( F ` N ) e. CC )
23 1re 
 |-  1 e. RR
24 eluz2b2 
 |-  ( M e. ( ZZ>= ` 2 ) <-> ( M e. NN /\ 1 < M ) )
25 9 24 sylib 
 |-  ( ph -> ( M e. NN /\ 1 < M ) )
26 25 simpld 
 |-  ( ph -> M e. NN )
27 nnq 
 |-  ( M e. NN -> M e. QQ )
28 26 27 syl 
 |-  ( ph -> M e. QQ )
29 2 18 abvcl 
 |-  ( ( F e. A /\ M e. QQ ) -> ( F ` M ) e. RR )
30 5 28 29 syl2anc 
 |-  ( ph -> ( F ` M ) e. RR )
31 ifcl 
 |-  ( ( 1 e. RR /\ ( F ` M ) e. RR ) -> if ( ( F ` M ) <_ 1 , 1 , ( F ` M ) ) e. RR )
32 23 30 31 sylancr 
 |-  ( ph -> if ( ( F ` M ) <_ 1 , 1 , ( F ` M ) ) e. RR )
33 11 32 eqeltrid 
 |-  ( ph -> T e. RR )
34 33 adantr 
 |-  ( ( ph /\ X e. NN ) -> T e. RR )
35 0red 
 |-  ( ph -> 0 e. RR )
36 1red 
 |-  ( 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 30 36 39 syl2anc 
 |-  ( ph -> 1 <_ if ( ( F ` M ) <_ 1 , 1 , ( F ` M ) ) )
41 40 11 breqtrrdi 
 |-  ( ph -> 1 <_ T )
42 35 36 33 38 41 ltletrd 
 |-  ( ph -> 0 < T )
43 42 adantr 
 |-  ( ( ph /\ X e. NN ) -> 0 < T )
44 34 43 elrpd 
 |-  ( ( ph /\ X e. NN ) -> T e. RR+ )
45 44 rpge0d 
 |-  ( ( ph /\ X e. NN ) -> 0 <_ T )
46 15 nnred 
 |-  ( ph -> N e. RR )
47 14 simprd 
 |-  ( ph -> 1 < N )
48 46 47 rplogcld 
 |-  ( ph -> ( log ` N ) e. RR+ )
49 26 nnred 
 |-  ( ph -> M e. RR )
50 25 simprd 
 |-  ( ph -> 1 < M )
51 49 50 rplogcld 
 |-  ( ph -> ( log ` M ) e. RR+ )
52 48 51 rpdivcld 
 |-  ( ph -> ( ( log ` N ) / ( log ` M ) ) e. RR+ )
53 12 52 eqeltrid 
 |-  ( ph -> U e. RR+ )
54 53 rpred 
 |-  ( ph -> U e. RR )
55 54 adantr 
 |-  ( ( ph /\ X e. NN ) -> U e. RR )
56 34 45 55 recxpcld 
 |-  ( ( ph /\ X e. NN ) -> ( T ^c U ) e. RR )
57 56 recnd 
 |-  ( ( ph /\ X e. NN ) -> ( T ^c U ) e. CC )
58 44 55 rpcxpcld 
 |-  ( ( ph /\ X e. NN ) -> ( T ^c U ) e. RR+ )
59 58 rpne0d 
 |-  ( ( ph /\ X e. NN ) -> ( T ^c U ) =/= 0 )
60 nnnn0 
 |-  ( X e. NN -> X e. NN0 )
61 60 adantl 
 |-  ( ( ph /\ X e. NN ) -> X e. NN0 )
62 22 57 59 61 expdivd 
 |-  ( ( ph /\ X e. NN ) -> ( ( ( F ` N ) / ( T ^c U ) ) ^ X ) = ( ( ( F ` N ) ^ X ) / ( ( T ^c U ) ^ X ) ) )
63 reexpcl 
 |-  ( ( ( F ` N ) e. RR /\ X e. NN0 ) -> ( ( F ` N ) ^ X ) e. RR )
64 20 60 63 syl2an 
 |-  ( ( ph /\ X e. NN ) -> ( ( F ` N ) ^ X ) e. RR )
65 26 adantr 
 |-  ( ( ph /\ X e. NN ) -> M e. NN )
66 65 nnred 
 |-  ( ( ph /\ X e. NN ) -> M e. RR )
67 nnre 
 |-  ( X e. NN -> X e. RR )
68 67 adantl 
 |-  ( ( ph /\ X e. NN ) -> X e. RR )
69 68 55 remulcld 
 |-  ( ( ph /\ X e. NN ) -> ( X x. U ) e. RR )
70 61 nn0ge0d 
 |-  ( ( ph /\ X e. NN ) -> 0 <_ X )
71 53 rpge0d 
 |-  ( ph -> 0 <_ U )
72 71 adantr 
 |-  ( ( ph /\ X e. NN ) -> 0 <_ U )
73 68 55 70 72 mulge0d 
 |-  ( ( ph /\ X e. NN ) -> 0 <_ ( X x. U ) )
74 flge0nn0 
 |-  ( ( ( X x. U ) e. RR /\ 0 <_ ( X x. U ) ) -> ( |_ ` ( X x. U ) ) e. NN0 )
75 69 73 74 syl2anc 
 |-  ( ( ph /\ X e. NN ) -> ( |_ ` ( X x. U ) ) e. NN0 )
76 peano2nn0 
 |-  ( ( |_ ` ( X x. U ) ) e. NN0 -> ( ( |_ ` ( X x. U ) ) + 1 ) e. NN0 )
77 75 76 syl 
 |-  ( ( ph /\ X e. NN ) -> ( ( |_ ` ( X x. U ) ) + 1 ) e. NN0 )
78 77 nn0red 
 |-  ( ( ph /\ X e. NN ) -> ( ( |_ ` ( X x. U ) ) + 1 ) e. RR )
79 66 78 remulcld 
 |-  ( ( ph /\ X e. NN ) -> ( M x. ( ( |_ ` ( X x. U ) ) + 1 ) ) e. RR )
80 34 77 reexpcld 
 |-  ( ( ph /\ X e. NN ) -> ( T ^ ( ( |_ ` ( X x. U ) ) + 1 ) ) e. RR )
81 79 80 remulcld 
 |-  ( ( ph /\ X e. NN ) -> ( ( M x. ( ( |_ ` ( X x. U ) ) + 1 ) ) x. ( T ^ ( ( |_ ` ( X x. U ) ) + 1 ) ) ) e. RR )
82 peano2re 
 |-  ( U e. RR -> ( U + 1 ) e. RR )
83 55 82 syl 
 |-  ( ( ph /\ X e. NN ) -> ( U + 1 ) e. RR )
84 68 83 remulcld 
 |-  ( ( ph /\ X e. NN ) -> ( X x. ( U + 1 ) ) e. RR )
85 66 84 remulcld 
 |-  ( ( ph /\ X e. NN ) -> ( M x. ( X x. ( U + 1 ) ) ) e. RR )
86 56 61 reexpcld 
 |-  ( ( ph /\ X e. NN ) -> ( ( T ^c U ) ^ X ) e. RR )
87 86 34 remulcld 
 |-  ( ( ph /\ X e. NN ) -> ( ( ( T ^c U ) ^ X ) x. T ) e. RR )
88 85 87 remulcld 
 |-  ( ( ph /\ X e. NN ) -> ( ( M x. ( X x. ( U + 1 ) ) ) x. ( ( ( T ^c U ) ^ X ) x. T ) ) e. RR )
89 1 2 qabvexp 
 |-  ( ( F e. A /\ N e. QQ /\ X e. NN0 ) -> ( F ` ( N ^ X ) ) = ( ( F ` N ) ^ X ) )
90 5 17 60 89 syl2an3an 
 |-  ( ( ph /\ X e. NN ) -> ( F ` ( N ^ X ) ) = ( ( F ` N ) ^ X ) )
91 68 recnd 
 |-  ( ( ph /\ X e. NN ) -> X e. CC )
92 48 rpred 
 |-  ( ph -> ( log ` N ) e. RR )
93 92 recnd 
 |-  ( ph -> ( log ` N ) e. CC )
94 93 adantr 
 |-  ( ( ph /\ X e. NN ) -> ( log ` N ) e. CC )
95 51 rpred 
 |-  ( ph -> ( log ` M ) e. RR )
96 95 recnd 
 |-  ( ph -> ( log ` M ) e. CC )
97 96 adantr 
 |-  ( ( ph /\ X e. NN ) -> ( log ` M ) e. CC )
98 51 adantr 
 |-  ( ( ph /\ X e. NN ) -> ( log ` M ) e. RR+ )
99 98 rpne0d 
 |-  ( ( ph /\ X e. NN ) -> ( log ` M ) =/= 0 )
100 91 94 97 99 divassd 
 |-  ( ( ph /\ X e. NN ) -> ( ( X x. ( log ` N ) ) / ( log ` M ) ) = ( X x. ( ( log ` N ) / ( log ` M ) ) ) )
101 12 oveq2i 
 |-  ( X x. U ) = ( X x. ( ( log ` N ) / ( log ` M ) ) )
102 100 101 eqtr4di 
 |-  ( ( ph /\ X e. NN ) -> ( ( X x. ( log ` N ) ) / ( log ` M ) ) = ( X x. U ) )
103 102 oveq1d 
 |-  ( ( ph /\ X e. NN ) -> ( ( ( X x. ( log ` N ) ) / ( log ` M ) ) x. ( log ` M ) ) = ( ( X x. U ) x. ( log ` M ) ) )
104 91 94 mulcld 
 |-  ( ( ph /\ X e. NN ) -> ( X x. ( log ` N ) ) e. CC )
105 104 97 99 divcan1d 
 |-  ( ( ph /\ X e. NN ) -> ( ( ( X x. ( log ` N ) ) / ( log ` M ) ) x. ( log ` M ) ) = ( X x. ( log ` N ) ) )
106 103 105 eqtr3d 
 |-  ( ( ph /\ X e. NN ) -> ( ( X x. U ) x. ( log ` M ) ) = ( X x. ( log ` N ) ) )
107 flltp1 
 |-  ( ( X x. U ) e. RR -> ( X x. U ) < ( ( |_ ` ( X x. U ) ) + 1 ) )
108 69 107 syl 
 |-  ( ( ph /\ X e. NN ) -> ( X x. U ) < ( ( |_ ` ( X x. U ) ) + 1 ) )
109 69 78 98 108 ltmul1dd 
 |-  ( ( ph /\ X e. NN ) -> ( ( X x. U ) x. ( log ` M ) ) < ( ( ( |_ ` ( X x. U ) ) + 1 ) x. ( log ` M ) ) )
110 106 109 eqbrtrrd 
 |-  ( ( ph /\ X e. NN ) -> ( X x. ( log ` N ) ) < ( ( ( |_ ` ( X x. U ) ) + 1 ) x. ( log ` M ) ) )
111 92 adantr 
 |-  ( ( ph /\ X e. NN ) -> ( log ` N ) e. RR )
112 68 111 remulcld 
 |-  ( ( ph /\ X e. NN ) -> ( X x. ( log ` N ) ) e. RR )
113 95 adantr 
 |-  ( ( ph /\ X e. NN ) -> ( log ` M ) e. RR )
114 78 113 remulcld 
 |-  ( ( ph /\ X e. NN ) -> ( ( ( |_ ` ( X x. U ) ) + 1 ) x. ( log ` M ) ) e. RR )
115 eflt 
 |-  ( ( ( X x. ( log ` N ) ) e. RR /\ ( ( ( |_ ` ( X x. U ) ) + 1 ) x. ( log ` M ) ) e. RR ) -> ( ( X x. ( log ` N ) ) < ( ( ( |_ ` ( X x. U ) ) + 1 ) x. ( log ` M ) ) <-> ( exp ` ( X x. ( log ` N ) ) ) < ( exp ` ( ( ( |_ ` ( X x. U ) ) + 1 ) x. ( log ` M ) ) ) ) )
116 112 114 115 syl2anc 
 |-  ( ( ph /\ X e. NN ) -> ( ( X x. ( log ` N ) ) < ( ( ( |_ ` ( X x. U ) ) + 1 ) x. ( log ` M ) ) <-> ( exp ` ( X x. ( log ` N ) ) ) < ( exp ` ( ( ( |_ ` ( X x. U ) ) + 1 ) x. ( log ` M ) ) ) ) )
117 110 116 mpbid 
 |-  ( ( ph /\ X e. NN ) -> ( exp ` ( X x. ( log ` N ) ) ) < ( exp ` ( ( ( |_ ` ( X x. U ) ) + 1 ) x. ( log ` M ) ) ) )
118 15 nnrpd 
 |-  ( ph -> N e. RR+ )
119 nnz 
 |-  ( X e. NN -> X e. ZZ )
120 reexplog 
 |-  ( ( N e. RR+ /\ X e. ZZ ) -> ( N ^ X ) = ( exp ` ( X x. ( log ` N ) ) ) )
121 118 119 120 syl2an 
 |-  ( ( ph /\ X e. NN ) -> ( N ^ X ) = ( exp ` ( X x. ( log ` N ) ) ) )
122 65 nnrpd 
 |-  ( ( ph /\ X e. NN ) -> M e. RR+ )
123 77 nn0zd 
 |-  ( ( ph /\ X e. NN ) -> ( ( |_ ` ( X x. U ) ) + 1 ) e. ZZ )
124 reexplog 
 |-  ( ( M e. RR+ /\ ( ( |_ ` ( X x. U ) ) + 1 ) e. ZZ ) -> ( M ^ ( ( |_ ` ( X x. U ) ) + 1 ) ) = ( exp ` ( ( ( |_ ` ( X x. U ) ) + 1 ) x. ( log ` M ) ) ) )
125 122 123 124 syl2anc 
 |-  ( ( ph /\ X e. NN ) -> ( M ^ ( ( |_ ` ( X x. U ) ) + 1 ) ) = ( exp ` ( ( ( |_ ` ( X x. U ) ) + 1 ) x. ( log ` M ) ) ) )
126 117 121 125 3brtr4d 
 |-  ( ( ph /\ X e. NN ) -> ( N ^ X ) < ( M ^ ( ( |_ ` ( X x. U ) ) + 1 ) ) )
127 nnexpcl 
 |-  ( ( N e. NN /\ X e. NN0 ) -> ( N ^ X ) e. NN )
128 15 60 127 syl2an 
 |-  ( ( ph /\ X e. NN ) -> ( N ^ X ) e. NN )
129 65 77 nnexpcld 
 |-  ( ( ph /\ X e. NN ) -> ( M ^ ( ( |_ ` ( X x. U ) ) + 1 ) ) e. NN )
130 nnltlem1 
 |-  ( ( ( N ^ X ) e. NN /\ ( M ^ ( ( |_ ` ( X x. U ) ) + 1 ) ) e. NN ) -> ( ( N ^ X ) < ( M ^ ( ( |_ ` ( X x. U ) ) + 1 ) ) <-> ( N ^ X ) <_ ( ( M ^ ( ( |_ ` ( X x. U ) ) + 1 ) ) - 1 ) ) )
131 128 129 130 syl2anc 
 |-  ( ( ph /\ X e. NN ) -> ( ( N ^ X ) < ( M ^ ( ( |_ ` ( X x. U ) ) + 1 ) ) <-> ( N ^ X ) <_ ( ( M ^ ( ( |_ ` ( X x. U ) ) + 1 ) ) - 1 ) ) )
132 126 131 mpbid 
 |-  ( ( ph /\ X e. NN ) -> ( N ^ X ) <_ ( ( M ^ ( ( |_ ` ( X x. U ) ) + 1 ) ) - 1 ) )
133 128 nnnn0d 
 |-  ( ( ph /\ X e. NN ) -> ( N ^ X ) e. NN0 )
134 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
135 133 134 eleqtrdi 
 |-  ( ( ph /\ X e. NN ) -> ( N ^ X ) e. ( ZZ>= ` 0 ) )
136 129 nnzd 
 |-  ( ( ph /\ X e. NN ) -> ( M ^ ( ( |_ ` ( X x. U ) ) + 1 ) ) e. ZZ )
137 peano2zm 
 |-  ( ( M ^ ( ( |_ ` ( X x. U ) ) + 1 ) ) e. ZZ -> ( ( M ^ ( ( |_ ` ( X x. U ) ) + 1 ) ) - 1 ) e. ZZ )
138 136 137 syl 
 |-  ( ( ph /\ X e. NN ) -> ( ( M ^ ( ( |_ ` ( X x. U ) ) + 1 ) ) - 1 ) e. ZZ )
139 elfz5 
 |-  ( ( ( N ^ X ) e. ( ZZ>= ` 0 ) /\ ( ( M ^ ( ( |_ ` ( X x. U ) ) + 1 ) ) - 1 ) e. ZZ ) -> ( ( N ^ X ) e. ( 0 ... ( ( M ^ ( ( |_ ` ( X x. U ) ) + 1 ) ) - 1 ) ) <-> ( N ^ X ) <_ ( ( M ^ ( ( |_ ` ( X x. U ) ) + 1 ) ) - 1 ) ) )
140 135 138 139 syl2anc 
 |-  ( ( ph /\ X e. NN ) -> ( ( N ^ X ) e. ( 0 ... ( ( M ^ ( ( |_ ` ( X x. U ) ) + 1 ) ) - 1 ) ) <-> ( N ^ X ) <_ ( ( M ^ ( ( |_ ` ( X x. U ) ) + 1 ) ) - 1 ) ) )
141 132 140 mpbird 
 |-  ( ( ph /\ X e. NN ) -> ( N ^ X ) e. ( 0 ... ( ( M ^ ( ( |_ ` ( X x. U ) ) + 1 ) ) - 1 ) ) )
142 1 2 3 4 5 6 7 8 9 10 11 ostth2lem2 
 |-  ( ( ph /\ ( ( |_ ` ( X x. U ) ) + 1 ) e. NN0 /\ ( N ^ X ) e. ( 0 ... ( ( M ^ ( ( |_ ` ( X x. U ) ) + 1 ) ) - 1 ) ) ) -> ( F ` ( N ^ X ) ) <_ ( ( M x. ( ( |_ ` ( X x. U ) ) + 1 ) ) x. ( T ^ ( ( |_ ` ( X x. U ) ) + 1 ) ) ) )
143 142 3expia 
 |-  ( ( ph /\ ( ( |_ ` ( X x. U ) ) + 1 ) e. NN0 ) -> ( ( N ^ X ) e. ( 0 ... ( ( M ^ ( ( |_ ` ( X x. U ) ) + 1 ) ) - 1 ) ) -> ( F ` ( N ^ X ) ) <_ ( ( M x. ( ( |_ ` ( X x. U ) ) + 1 ) ) x. ( T ^ ( ( |_ ` ( X x. U ) ) + 1 ) ) ) ) )
144 77 143 syldan 
 |-  ( ( ph /\ X e. NN ) -> ( ( N ^ X ) e. ( 0 ... ( ( M ^ ( ( |_ ` ( X x. U ) ) + 1 ) ) - 1 ) ) -> ( F ` ( N ^ X ) ) <_ ( ( M x. ( ( |_ ` ( X x. U ) ) + 1 ) ) x. ( T ^ ( ( |_ ` ( X x. U ) ) + 1 ) ) ) ) )
145 141 144 mpd 
 |-  ( ( ph /\ X e. NN ) -> ( F ` ( N ^ X ) ) <_ ( ( M x. ( ( |_ ` ( X x. U ) ) + 1 ) ) x. ( T ^ ( ( |_ ` ( X x. U ) ) + 1 ) ) ) )
146 90 145 eqbrtrrd 
 |-  ( ( ph /\ X e. NN ) -> ( ( F ` N ) ^ X ) <_ ( ( M x. ( ( |_ ` ( X x. U ) ) + 1 ) ) x. ( T ^ ( ( |_ ` ( X x. U ) ) + 1 ) ) ) )
147 85 80 remulcld 
 |-  ( ( ph /\ X e. NN ) -> ( ( M x. ( X x. ( U + 1 ) ) ) x. ( T ^ ( ( |_ ` ( X x. U ) ) + 1 ) ) ) e. RR )
148 peano2re 
 |-  ( ( X x. U ) e. RR -> ( ( X x. U ) + 1 ) e. RR )
149 69 148 syl 
 |-  ( ( ph /\ X e. NN ) -> ( ( X x. U ) + 1 ) e. RR )
150 75 nn0red 
 |-  ( ( ph /\ X e. NN ) -> ( |_ ` ( X x. U ) ) e. RR )
151 1red 
 |-  ( ( ph /\ X e. NN ) -> 1 e. RR )
152 flle 
 |-  ( ( X x. U ) e. RR -> ( |_ ` ( X x. U ) ) <_ ( X x. U ) )
153 69 152 syl 
 |-  ( ( ph /\ X e. NN ) -> ( |_ ` ( X x. U ) ) <_ ( X x. U ) )
154 150 69 151 153 leadd1dd 
 |-  ( ( ph /\ X e. NN ) -> ( ( |_ ` ( X x. U ) ) + 1 ) <_ ( ( X x. U ) + 1 ) )
155 nnge1 
 |-  ( X e. NN -> 1 <_ X )
156 155 adantl 
 |-  ( ( ph /\ X e. NN ) -> 1 <_ X )
157 151 68 69 156 leadd2dd 
 |-  ( ( ph /\ X e. NN ) -> ( ( X x. U ) + 1 ) <_ ( ( X x. U ) + X ) )
158 55 recnd 
 |-  ( ( ph /\ X e. NN ) -> U e. CC )
159 151 recnd 
 |-  ( ( ph /\ X e. NN ) -> 1 e. CC )
160 91 158 159 adddid 
 |-  ( ( ph /\ X e. NN ) -> ( X x. ( U + 1 ) ) = ( ( X x. U ) + ( X x. 1 ) ) )
161 91 mulridd 
 |-  ( ( ph /\ X e. NN ) -> ( X x. 1 ) = X )
162 161 oveq2d 
 |-  ( ( ph /\ X e. NN ) -> ( ( X x. U ) + ( X x. 1 ) ) = ( ( X x. U ) + X ) )
163 160 162 eqtrd 
 |-  ( ( ph /\ X e. NN ) -> ( X x. ( U + 1 ) ) = ( ( X x. U ) + X ) )
164 157 163 breqtrrd 
 |-  ( ( ph /\ X e. NN ) -> ( ( X x. U ) + 1 ) <_ ( X x. ( U + 1 ) ) )
165 78 149 84 154 164 letrd 
 |-  ( ( ph /\ X e. NN ) -> ( ( |_ ` ( X x. U ) ) + 1 ) <_ ( X x. ( U + 1 ) ) )
166 65 nngt0d 
 |-  ( ( ph /\ X e. NN ) -> 0 < M )
167 lemul2 
 |-  ( ( ( ( |_ ` ( X x. U ) ) + 1 ) e. RR /\ ( X x. ( U + 1 ) ) e. RR /\ ( M e. RR /\ 0 < M ) ) -> ( ( ( |_ ` ( X x. U ) ) + 1 ) <_ ( X x. ( U + 1 ) ) <-> ( M x. ( ( |_ ` ( X x. U ) ) + 1 ) ) <_ ( M x. ( X x. ( U + 1 ) ) ) ) )
168 78 84 66 166 167 syl112anc 
 |-  ( ( ph /\ X e. NN ) -> ( ( ( |_ ` ( X x. U ) ) + 1 ) <_ ( X x. ( U + 1 ) ) <-> ( M x. ( ( |_ ` ( X x. U ) ) + 1 ) ) <_ ( M x. ( X x. ( U + 1 ) ) ) ) )
169 165 168 mpbid 
 |-  ( ( ph /\ X e. NN ) -> ( M x. ( ( |_ ` ( X x. U ) ) + 1 ) ) <_ ( M x. ( X x. ( U + 1 ) ) ) )
170 expgt0 
 |-  ( ( T e. RR /\ ( ( |_ ` ( X x. U ) ) + 1 ) e. ZZ /\ 0 < T ) -> 0 < ( T ^ ( ( |_ ` ( X x. U ) ) + 1 ) ) )
171 34 123 43 170 syl3anc 
 |-  ( ( ph /\ X e. NN ) -> 0 < ( T ^ ( ( |_ ` ( X x. U ) ) + 1 ) ) )
172 lemul1 
 |-  ( ( ( M x. ( ( |_ ` ( X x. U ) ) + 1 ) ) e. RR /\ ( M x. ( X x. ( U + 1 ) ) ) e. RR /\ ( ( T ^ ( ( |_ ` ( X x. U ) ) + 1 ) ) e. RR /\ 0 < ( T ^ ( ( |_ ` ( X x. U ) ) + 1 ) ) ) ) -> ( ( M x. ( ( |_ ` ( X x. U ) ) + 1 ) ) <_ ( M x. ( X x. ( U + 1 ) ) ) <-> ( ( M x. ( ( |_ ` ( X x. U ) ) + 1 ) ) x. ( T ^ ( ( |_ ` ( X x. U ) ) + 1 ) ) ) <_ ( ( M x. ( X x. ( U + 1 ) ) ) x. ( T ^ ( ( |_ ` ( X x. U ) ) + 1 ) ) ) ) )
173 79 85 80 171 172 syl112anc 
 |-  ( ( ph /\ X e. NN ) -> ( ( M x. ( ( |_ ` ( X x. U ) ) + 1 ) ) <_ ( M x. ( X x. ( U + 1 ) ) ) <-> ( ( M x. ( ( |_ ` ( X x. U ) ) + 1 ) ) x. ( T ^ ( ( |_ ` ( X x. U ) ) + 1 ) ) ) <_ ( ( M x. ( X x. ( U + 1 ) ) ) x. ( T ^ ( ( |_ ` ( X x. U ) ) + 1 ) ) ) ) )
174 169 173 mpbid 
 |-  ( ( ph /\ X e. NN ) -> ( ( M x. ( ( |_ ` ( X x. U ) ) + 1 ) ) x. ( T ^ ( ( |_ ` ( X x. U ) ) + 1 ) ) ) <_ ( ( M x. ( X x. ( U + 1 ) ) ) x. ( T ^ ( ( |_ ` ( X x. U ) ) + 1 ) ) ) )
175 34 recnd 
 |-  ( ( ph /\ X e. NN ) -> T e. CC )
176 175 75 expp1d 
 |-  ( ( ph /\ X e. NN ) -> ( T ^ ( ( |_ ` ( X x. U ) ) + 1 ) ) = ( ( T ^ ( |_ ` ( X x. U ) ) ) x. T ) )
177 41 adantr 
 |-  ( ( ph /\ X e. NN ) -> 1 <_ T )
178 remulcl 
 |-  ( ( U e. RR /\ X e. RR ) -> ( U x. X ) e. RR )
179 54 67 178 syl2an 
 |-  ( ( ph /\ X e. NN ) -> ( U x. X ) e. RR )
180 91 158 mulcomd 
 |-  ( ( ph /\ X e. NN ) -> ( X x. U ) = ( U x. X ) )
181 153 180 breqtrd 
 |-  ( ( ph /\ X e. NN ) -> ( |_ ` ( X x. U ) ) <_ ( U x. X ) )
182 34 177 150 179 181 cxplead 
 |-  ( ( ph /\ X e. NN ) -> ( T ^c ( |_ ` ( X x. U ) ) ) <_ ( T ^c ( U x. X ) ) )
183 cxpexp 
 |-  ( ( T e. CC /\ ( |_ ` ( X x. U ) ) e. NN0 ) -> ( T ^c ( |_ ` ( X x. U ) ) ) = ( T ^ ( |_ ` ( X x. U ) ) ) )
184 175 75 183 syl2anc 
 |-  ( ( ph /\ X e. NN ) -> ( T ^c ( |_ ` ( X x. U ) ) ) = ( T ^ ( |_ ` ( X x. U ) ) ) )
185 44 55 91 cxpmuld 
 |-  ( ( ph /\ X e. NN ) -> ( T ^c ( U x. X ) ) = ( ( T ^c U ) ^c X ) )
186 cxpexp 
 |-  ( ( ( T ^c U ) e. CC /\ X e. NN0 ) -> ( ( T ^c U ) ^c X ) = ( ( T ^c U ) ^ X ) )
187 57 61 186 syl2anc 
 |-  ( ( ph /\ X e. NN ) -> ( ( T ^c U ) ^c X ) = ( ( T ^c U ) ^ X ) )
188 185 187 eqtrd 
 |-  ( ( ph /\ X e. NN ) -> ( T ^c ( U x. X ) ) = ( ( T ^c U ) ^ X ) )
189 182 184 188 3brtr3d 
 |-  ( ( ph /\ X e. NN ) -> ( T ^ ( |_ ` ( X x. U ) ) ) <_ ( ( T ^c U ) ^ X ) )
190 34 75 reexpcld 
 |-  ( ( ph /\ X e. NN ) -> ( T ^ ( |_ ` ( X x. U ) ) ) e. RR )
191 190 86 44 lemul1d 
 |-  ( ( ph /\ X e. NN ) -> ( ( T ^ ( |_ ` ( X x. U ) ) ) <_ ( ( T ^c U ) ^ X ) <-> ( ( T ^ ( |_ ` ( X x. U ) ) ) x. T ) <_ ( ( ( T ^c U ) ^ X ) x. T ) ) )
192 189 191 mpbid 
 |-  ( ( ph /\ X e. NN ) -> ( ( T ^ ( |_ ` ( X x. U ) ) ) x. T ) <_ ( ( ( T ^c U ) ^ X ) x. T ) )
193 176 192 eqbrtrd 
 |-  ( ( ph /\ X e. NN ) -> ( T ^ ( ( |_ ` ( X x. U ) ) + 1 ) ) <_ ( ( ( T ^c U ) ^ X ) x. T ) )
194 nngt0 
 |-  ( X e. NN -> 0 < X )
195 194 adantl 
 |-  ( ( ph /\ X e. NN ) -> 0 < X )
196 0red 
 |-  ( ( ph /\ X e. NN ) -> 0 e. RR )
197 53 adantr 
 |-  ( ( ph /\ X e. NN ) -> U e. RR+ )
198 197 rpgt0d 
 |-  ( ( ph /\ X e. NN ) -> 0 < U )
199 55 ltp1d 
 |-  ( ( ph /\ X e. NN ) -> U < ( U + 1 ) )
200 196 55 83 198 199 lttrd 
 |-  ( ( ph /\ X e. NN ) -> 0 < ( U + 1 ) )
201 68 83 195 200 mulgt0d 
 |-  ( ( ph /\ X e. NN ) -> 0 < ( X x. ( U + 1 ) ) )
202 66 84 166 201 mulgt0d 
 |-  ( ( ph /\ X e. NN ) -> 0 < ( M x. ( X x. ( U + 1 ) ) ) )
203 lemul2 
 |-  ( ( ( T ^ ( ( |_ ` ( X x. U ) ) + 1 ) ) e. RR /\ ( ( ( T ^c U ) ^ X ) x. T ) e. RR /\ ( ( M x. ( X x. ( U + 1 ) ) ) e. RR /\ 0 < ( M x. ( X x. ( U + 1 ) ) ) ) ) -> ( ( T ^ ( ( |_ ` ( X x. U ) ) + 1 ) ) <_ ( ( ( T ^c U ) ^ X ) x. T ) <-> ( ( M x. ( X x. ( U + 1 ) ) ) x. ( T ^ ( ( |_ ` ( X x. U ) ) + 1 ) ) ) <_ ( ( M x. ( X x. ( U + 1 ) ) ) x. ( ( ( T ^c U ) ^ X ) x. T ) ) ) )
204 80 87 85 202 203 syl112anc 
 |-  ( ( ph /\ X e. NN ) -> ( ( T ^ ( ( |_ ` ( X x. U ) ) + 1 ) ) <_ ( ( ( T ^c U ) ^ X ) x. T ) <-> ( ( M x. ( X x. ( U + 1 ) ) ) x. ( T ^ ( ( |_ ` ( X x. U ) ) + 1 ) ) ) <_ ( ( M x. ( X x. ( U + 1 ) ) ) x. ( ( ( T ^c U ) ^ X ) x. T ) ) ) )
205 193 204 mpbid 
 |-  ( ( ph /\ X e. NN ) -> ( ( M x. ( X x. ( U + 1 ) ) ) x. ( T ^ ( ( |_ ` ( X x. U ) ) + 1 ) ) ) <_ ( ( M x. ( X x. ( U + 1 ) ) ) x. ( ( ( T ^c U ) ^ X ) x. T ) ) )
206 81 147 88 174 205 letrd 
 |-  ( ( ph /\ X e. NN ) -> ( ( M x. ( ( |_ ` ( X x. U ) ) + 1 ) ) x. ( T ^ ( ( |_ ` ( X x. U ) ) + 1 ) ) ) <_ ( ( M x. ( X x. ( U + 1 ) ) ) x. ( ( ( T ^c U ) ^ X ) x. T ) ) )
207 64 81 88 146 206 letrd 
 |-  ( ( ph /\ X e. NN ) -> ( ( F ` N ) ^ X ) <_ ( ( M x. ( X x. ( U + 1 ) ) ) x. ( ( ( T ^c U ) ^ X ) x. T ) ) )
208 85 recnd 
 |-  ( ( ph /\ X e. NN ) -> ( M x. ( X x. ( U + 1 ) ) ) e. CC )
209 86 recnd 
 |-  ( ( ph /\ X e. NN ) -> ( ( T ^c U ) ^ X ) e. CC )
210 208 209 175 mul12d 
 |-  ( ( ph /\ X e. NN ) -> ( ( M x. ( X x. ( U + 1 ) ) ) x. ( ( ( T ^c U ) ^ X ) x. T ) ) = ( ( ( T ^c U ) ^ X ) x. ( ( M x. ( X x. ( U + 1 ) ) ) x. T ) ) )
211 66 recnd 
 |-  ( ( ph /\ X e. NN ) -> M e. CC )
212 84 recnd 
 |-  ( ( ph /\ X e. NN ) -> ( X x. ( U + 1 ) ) e. CC )
213 211 212 175 mul32d 
 |-  ( ( ph /\ X e. NN ) -> ( ( M x. ( X x. ( U + 1 ) ) ) x. T ) = ( ( M x. T ) x. ( X x. ( U + 1 ) ) ) )
214 211 175 mulcld 
 |-  ( ( ph /\ X e. NN ) -> ( M x. T ) e. CC )
215 83 recnd 
 |-  ( ( ph /\ X e. NN ) -> ( U + 1 ) e. CC )
216 214 91 215 mul12d 
 |-  ( ( ph /\ X e. NN ) -> ( ( M x. T ) x. ( X x. ( U + 1 ) ) ) = ( X x. ( ( M x. T ) x. ( U + 1 ) ) ) )
217 213 216 eqtrd 
 |-  ( ( ph /\ X e. NN ) -> ( ( M x. ( X x. ( U + 1 ) ) ) x. T ) = ( X x. ( ( M x. T ) x. ( U + 1 ) ) ) )
218 217 oveq2d 
 |-  ( ( ph /\ X e. NN ) -> ( ( ( T ^c U ) ^ X ) x. ( ( M x. ( X x. ( U + 1 ) ) ) x. T ) ) = ( ( ( T ^c U ) ^ X ) x. ( X x. ( ( M x. T ) x. ( U + 1 ) ) ) ) )
219 210 218 eqtrd 
 |-  ( ( ph /\ X e. NN ) -> ( ( M x. ( X x. ( U + 1 ) ) ) x. ( ( ( T ^c U ) ^ X ) x. T ) ) = ( ( ( T ^c U ) ^ X ) x. ( X x. ( ( M x. T ) x. ( U + 1 ) ) ) ) )
220 207 219 breqtrd 
 |-  ( ( ph /\ X e. NN ) -> ( ( F ` N ) ^ X ) <_ ( ( ( T ^c U ) ^ X ) x. ( X x. ( ( M x. T ) x. ( U + 1 ) ) ) ) )
221 66 34 remulcld 
 |-  ( ( ph /\ X e. NN ) -> ( M x. T ) e. RR )
222 221 83 remulcld 
 |-  ( ( ph /\ X e. NN ) -> ( ( M x. T ) x. ( U + 1 ) ) e. RR )
223 68 222 remulcld 
 |-  ( ( ph /\ X e. NN ) -> ( X x. ( ( M x. T ) x. ( U + 1 ) ) ) e. RR )
224 119 adantl 
 |-  ( ( ph /\ X e. NN ) -> X e. ZZ )
225 58 224 rpexpcld 
 |-  ( ( ph /\ X e. NN ) -> ( ( T ^c U ) ^ X ) e. RR+ )
226 64 223 225 ledivmuld 
 |-  ( ( ph /\ X e. NN ) -> ( ( ( ( F ` N ) ^ X ) / ( ( T ^c U ) ^ X ) ) <_ ( X x. ( ( M x. T ) x. ( U + 1 ) ) ) <-> ( ( F ` N ) ^ X ) <_ ( ( ( T ^c U ) ^ X ) x. ( X x. ( ( M x. T ) x. ( U + 1 ) ) ) ) ) )
227 220 226 mpbird 
 |-  ( ( ph /\ X e. NN ) -> ( ( ( F ` N ) ^ X ) / ( ( T ^c U ) ^ X ) ) <_ ( X x. ( ( M x. T ) x. ( U + 1 ) ) ) )
228 62 227 eqbrtrd 
 |-  ( ( ph /\ X e. NN ) -> ( ( ( F ` N ) / ( T ^c U ) ) ^ X ) <_ ( X x. ( ( M x. T ) x. ( U + 1 ) ) ) )