Metamath Proof Explorer


Theorem ostth2lem2

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 ) )
Assertion ostth2lem2
|- ( ( ph /\ X e. NN0 /\ Y e. ( 0 ... ( ( M ^ X ) - 1 ) ) ) -> ( F ` Y ) <_ ( ( M x. X ) x. ( T ^ X ) ) )

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 oveq2
 |-  ( x = 0 -> ( M ^ x ) = ( M ^ 0 ) )
13 12 oveq1d
 |-  ( x = 0 -> ( ( M ^ x ) - 1 ) = ( ( M ^ 0 ) - 1 ) )
14 13 oveq2d
 |-  ( x = 0 -> ( 0 ... ( ( M ^ x ) - 1 ) ) = ( 0 ... ( ( M ^ 0 ) - 1 ) ) )
15 oveq2
 |-  ( x = 0 -> ( M x. x ) = ( M x. 0 ) )
16 oveq2
 |-  ( x = 0 -> ( T ^ x ) = ( T ^ 0 ) )
17 15 16 oveq12d
 |-  ( x = 0 -> ( ( M x. x ) x. ( T ^ x ) ) = ( ( M x. 0 ) x. ( T ^ 0 ) ) )
18 17 breq2d
 |-  ( x = 0 -> ( ( F ` k ) <_ ( ( M x. x ) x. ( T ^ x ) ) <-> ( F ` k ) <_ ( ( M x. 0 ) x. ( T ^ 0 ) ) ) )
19 14 18 raleqbidv
 |-  ( x = 0 -> ( A. k e. ( 0 ... ( ( M ^ x ) - 1 ) ) ( F ` k ) <_ ( ( M x. x ) x. ( T ^ x ) ) <-> A. k e. ( 0 ... ( ( M ^ 0 ) - 1 ) ) ( F ` k ) <_ ( ( M x. 0 ) x. ( T ^ 0 ) ) ) )
20 19 imbi2d
 |-  ( x = 0 -> ( ( ph -> A. k e. ( 0 ... ( ( M ^ x ) - 1 ) ) ( F ` k ) <_ ( ( M x. x ) x. ( T ^ x ) ) ) <-> ( ph -> A. k e. ( 0 ... ( ( M ^ 0 ) - 1 ) ) ( F ` k ) <_ ( ( M x. 0 ) x. ( T ^ 0 ) ) ) ) )
21 oveq2
 |-  ( x = n -> ( M ^ x ) = ( M ^ n ) )
22 21 oveq1d
 |-  ( x = n -> ( ( M ^ x ) - 1 ) = ( ( M ^ n ) - 1 ) )
23 22 oveq2d
 |-  ( x = n -> ( 0 ... ( ( M ^ x ) - 1 ) ) = ( 0 ... ( ( M ^ n ) - 1 ) ) )
24 oveq2
 |-  ( x = n -> ( M x. x ) = ( M x. n ) )
25 oveq2
 |-  ( x = n -> ( T ^ x ) = ( T ^ n ) )
26 24 25 oveq12d
 |-  ( x = n -> ( ( M x. x ) x. ( T ^ x ) ) = ( ( M x. n ) x. ( T ^ n ) ) )
27 26 breq2d
 |-  ( x = n -> ( ( F ` k ) <_ ( ( M x. x ) x. ( T ^ x ) ) <-> ( F ` k ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) )
28 23 27 raleqbidv
 |-  ( x = n -> ( A. k e. ( 0 ... ( ( M ^ x ) - 1 ) ) ( F ` k ) <_ ( ( M x. x ) x. ( T ^ x ) ) <-> A. k e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` k ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) )
29 28 imbi2d
 |-  ( x = n -> ( ( ph -> A. k e. ( 0 ... ( ( M ^ x ) - 1 ) ) ( F ` k ) <_ ( ( M x. x ) x. ( T ^ x ) ) ) <-> ( ph -> A. k e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` k ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) )
30 oveq2
 |-  ( x = ( n + 1 ) -> ( M ^ x ) = ( M ^ ( n + 1 ) ) )
31 30 oveq1d
 |-  ( x = ( n + 1 ) -> ( ( M ^ x ) - 1 ) = ( ( M ^ ( n + 1 ) ) - 1 ) )
32 31 oveq2d
 |-  ( x = ( n + 1 ) -> ( 0 ... ( ( M ^ x ) - 1 ) ) = ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) )
33 oveq2
 |-  ( x = ( n + 1 ) -> ( M x. x ) = ( M x. ( n + 1 ) ) )
34 oveq2
 |-  ( x = ( n + 1 ) -> ( T ^ x ) = ( T ^ ( n + 1 ) ) )
35 33 34 oveq12d
 |-  ( x = ( n + 1 ) -> ( ( M x. x ) x. ( T ^ x ) ) = ( ( M x. ( n + 1 ) ) x. ( T ^ ( n + 1 ) ) ) )
36 35 breq2d
 |-  ( x = ( n + 1 ) -> ( ( F ` k ) <_ ( ( M x. x ) x. ( T ^ x ) ) <-> ( F ` k ) <_ ( ( M x. ( n + 1 ) ) x. ( T ^ ( n + 1 ) ) ) ) )
37 32 36 raleqbidv
 |-  ( x = ( n + 1 ) -> ( A. k e. ( 0 ... ( ( M ^ x ) - 1 ) ) ( F ` k ) <_ ( ( M x. x ) x. ( T ^ x ) ) <-> A. k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) ( F ` k ) <_ ( ( M x. ( n + 1 ) ) x. ( T ^ ( n + 1 ) ) ) ) )
38 37 imbi2d
 |-  ( x = ( n + 1 ) -> ( ( ph -> A. k e. ( 0 ... ( ( M ^ x ) - 1 ) ) ( F ` k ) <_ ( ( M x. x ) x. ( T ^ x ) ) ) <-> ( ph -> A. k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) ( F ` k ) <_ ( ( M x. ( n + 1 ) ) x. ( T ^ ( n + 1 ) ) ) ) ) )
39 oveq2
 |-  ( x = X -> ( M ^ x ) = ( M ^ X ) )
40 39 oveq1d
 |-  ( x = X -> ( ( M ^ x ) - 1 ) = ( ( M ^ X ) - 1 ) )
41 40 oveq2d
 |-  ( x = X -> ( 0 ... ( ( M ^ x ) - 1 ) ) = ( 0 ... ( ( M ^ X ) - 1 ) ) )
42 oveq2
 |-  ( x = X -> ( M x. x ) = ( M x. X ) )
43 oveq2
 |-  ( x = X -> ( T ^ x ) = ( T ^ X ) )
44 42 43 oveq12d
 |-  ( x = X -> ( ( M x. x ) x. ( T ^ x ) ) = ( ( M x. X ) x. ( T ^ X ) ) )
45 44 breq2d
 |-  ( x = X -> ( ( F ` k ) <_ ( ( M x. x ) x. ( T ^ x ) ) <-> ( F ` k ) <_ ( ( M x. X ) x. ( T ^ X ) ) ) )
46 41 45 raleqbidv
 |-  ( x = X -> ( A. k e. ( 0 ... ( ( M ^ x ) - 1 ) ) ( F ` k ) <_ ( ( M x. x ) x. ( T ^ x ) ) <-> A. k e. ( 0 ... ( ( M ^ X ) - 1 ) ) ( F ` k ) <_ ( ( M x. X ) x. ( T ^ X ) ) ) )
47 46 imbi2d
 |-  ( x = X -> ( ( ph -> A. k e. ( 0 ... ( ( M ^ x ) - 1 ) ) ( F ` k ) <_ ( ( M x. x ) x. ( T ^ x ) ) ) <-> ( ph -> A. k e. ( 0 ... ( ( M ^ X ) - 1 ) ) ( F ` k ) <_ ( ( M x. X ) x. ( T ^ X ) ) ) ) )
48 eluz2nn
 |-  ( M e. ( ZZ>= ` 2 ) -> M e. NN )
49 9 48 syl
 |-  ( ph -> M e. NN )
50 49 nncnd
 |-  ( ph -> M e. CC )
51 50 exp0d
 |-  ( ph -> ( M ^ 0 ) = 1 )
52 51 oveq1d
 |-  ( ph -> ( ( M ^ 0 ) - 1 ) = ( 1 - 1 ) )
53 1m1e0
 |-  ( 1 - 1 ) = 0
54 52 53 eqtrdi
 |-  ( ph -> ( ( M ^ 0 ) - 1 ) = 0 )
55 54 oveq2d
 |-  ( ph -> ( 0 ... ( ( M ^ 0 ) - 1 ) ) = ( 0 ... 0 ) )
56 55 eleq2d
 |-  ( ph -> ( k e. ( 0 ... ( ( M ^ 0 ) - 1 ) ) <-> k e. ( 0 ... 0 ) ) )
57 0le0
 |-  0 <_ 0
58 57 a1i
 |-  ( ph -> 0 <_ 0 )
59 1 qrng0
 |-  0 = ( 0g ` Q )
60 2 59 abv0
 |-  ( F e. A -> ( F ` 0 ) = 0 )
61 5 60 syl
 |-  ( ph -> ( F ` 0 ) = 0 )
62 50 mul01d
 |-  ( ph -> ( M x. 0 ) = 0 )
63 62 oveq1d
 |-  ( ph -> ( ( M x. 0 ) x. ( T ^ 0 ) ) = ( 0 x. ( T ^ 0 ) ) )
64 1re
 |-  1 e. RR
65 nnq
 |-  ( M e. NN -> M e. QQ )
66 49 65 syl
 |-  ( ph -> M e. QQ )
67 1 qrngbas
 |-  QQ = ( Base ` Q )
68 2 67 abvcl
 |-  ( ( F e. A /\ M e. QQ ) -> ( F ` M ) e. RR )
69 5 66 68 syl2anc
 |-  ( ph -> ( F ` M ) e. RR )
70 ifcl
 |-  ( ( 1 e. RR /\ ( F ` M ) e. RR ) -> if ( ( F ` M ) <_ 1 , 1 , ( F ` M ) ) e. RR )
71 64 69 70 sylancr
 |-  ( ph -> if ( ( F ` M ) <_ 1 , 1 , ( F ` M ) ) e. RR )
72 11 71 eqeltrid
 |-  ( ph -> T e. RR )
73 72 recnd
 |-  ( ph -> T e. CC )
74 0nn0
 |-  0 e. NN0
75 expcl
 |-  ( ( T e. CC /\ 0 e. NN0 ) -> ( T ^ 0 ) e. CC )
76 73 74 75 sylancl
 |-  ( ph -> ( T ^ 0 ) e. CC )
77 76 mul02d
 |-  ( ph -> ( 0 x. ( T ^ 0 ) ) = 0 )
78 63 77 eqtrd
 |-  ( ph -> ( ( M x. 0 ) x. ( T ^ 0 ) ) = 0 )
79 58 61 78 3brtr4d
 |-  ( ph -> ( F ` 0 ) <_ ( ( M x. 0 ) x. ( T ^ 0 ) ) )
80 elfz1eq
 |-  ( k e. ( 0 ... 0 ) -> k = 0 )
81 80 fveq2d
 |-  ( k e. ( 0 ... 0 ) -> ( F ` k ) = ( F ` 0 ) )
82 81 breq1d
 |-  ( k e. ( 0 ... 0 ) -> ( ( F ` k ) <_ ( ( M x. 0 ) x. ( T ^ 0 ) ) <-> ( F ` 0 ) <_ ( ( M x. 0 ) x. ( T ^ 0 ) ) ) )
83 79 82 syl5ibrcom
 |-  ( ph -> ( k e. ( 0 ... 0 ) -> ( F ` k ) <_ ( ( M x. 0 ) x. ( T ^ 0 ) ) ) )
84 56 83 sylbid
 |-  ( ph -> ( k e. ( 0 ... ( ( M ^ 0 ) - 1 ) ) -> ( F ` k ) <_ ( ( M x. 0 ) x. ( T ^ 0 ) ) ) )
85 84 ralrimiv
 |-  ( ph -> A. k e. ( 0 ... ( ( M ^ 0 ) - 1 ) ) ( F ` k ) <_ ( ( M x. 0 ) x. ( T ^ 0 ) ) )
86 fveq2
 |-  ( k = j -> ( F ` k ) = ( F ` j ) )
87 86 breq1d
 |-  ( k = j -> ( ( F ` k ) <_ ( ( M x. n ) x. ( T ^ n ) ) <-> ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) )
88 87 cbvralvw
 |-  ( A. k e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` k ) <_ ( ( M x. n ) x. ( T ^ n ) ) <-> A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) )
89 5 ad2antrr
 |-  ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> F e. A )
90 elfzelz
 |-  ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) -> k e. ZZ )
91 90 ad2antrl
 |-  ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> k e. ZZ )
92 zq
 |-  ( k e. ZZ -> k e. QQ )
93 91 92 syl
 |-  ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> k e. QQ )
94 2 67 abvcl
 |-  ( ( F e. A /\ k e. QQ ) -> ( F ` k ) e. RR )
95 89 93 94 syl2anc
 |-  ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> ( F ` k ) e. RR )
96 49 ad2antrr
 |-  ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> M e. NN )
97 simplr
 |-  ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> n e. NN0 )
98 96 97 nnexpcld
 |-  ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> ( M ^ n ) e. NN )
99 91 98 zmodcld
 |-  ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> ( k mod ( M ^ n ) ) e. NN0 )
100 99 nn0zd
 |-  ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> ( k mod ( M ^ n ) ) e. ZZ )
101 zq
 |-  ( ( k mod ( M ^ n ) ) e. ZZ -> ( k mod ( M ^ n ) ) e. QQ )
102 100 101 syl
 |-  ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> ( k mod ( M ^ n ) ) e. QQ )
103 2 67 abvcl
 |-  ( ( F e. A /\ ( k mod ( M ^ n ) ) e. QQ ) -> ( F ` ( k mod ( M ^ n ) ) ) e. RR )
104 89 102 103 syl2anc
 |-  ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> ( F ` ( k mod ( M ^ n ) ) ) e. RR )
105 96 65 syl
 |-  ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> M e. QQ )
106 89 105 68 syl2anc
 |-  ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> ( F ` M ) e. RR )
107 106 97 reexpcld
 |-  ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> ( ( F ` M ) ^ n ) e. RR )
108 91 zred
 |-  ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> k e. RR )
109 108 98 nndivred
 |-  ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> ( k / ( M ^ n ) ) e. RR )
110 109 flcld
 |-  ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> ( |_ ` ( k / ( M ^ n ) ) ) e. ZZ )
111 zq
 |-  ( ( |_ ` ( k / ( M ^ n ) ) ) e. ZZ -> ( |_ ` ( k / ( M ^ n ) ) ) e. QQ )
112 110 111 syl
 |-  ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> ( |_ ` ( k / ( M ^ n ) ) ) e. QQ )
113 2 67 abvcl
 |-  ( ( F e. A /\ ( |_ ` ( k / ( M ^ n ) ) ) e. QQ ) -> ( F ` ( |_ ` ( k / ( M ^ n ) ) ) ) e. RR )
114 89 112 113 syl2anc
 |-  ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> ( F ` ( |_ ` ( k / ( M ^ n ) ) ) ) e. RR )
115 107 114 remulcld
 |-  ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> ( ( ( F ` M ) ^ n ) x. ( F ` ( |_ ` ( k / ( M ^ n ) ) ) ) ) e. RR )
116 104 115 readdcld
 |-  ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> ( ( F ` ( k mod ( M ^ n ) ) ) + ( ( ( F ` M ) ^ n ) x. ( F ` ( |_ ` ( k / ( M ^ n ) ) ) ) ) ) e. RR )
117 96 nnred
 |-  ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> M e. RR )
118 nn0p1nn
 |-  ( n e. NN0 -> ( n + 1 ) e. NN )
119 118 ad2antlr
 |-  ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> ( n + 1 ) e. NN )
120 119 nnred
 |-  ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> ( n + 1 ) e. RR )
121 117 120 remulcld
 |-  ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> ( M x. ( n + 1 ) ) e. RR )
122 72 ad2antrr
 |-  ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> T e. RR )
123 peano2nn0
 |-  ( n e. NN0 -> ( n + 1 ) e. NN0 )
124 123 ad2antlr
 |-  ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> ( n + 1 ) e. NN0 )
125 122 124 reexpcld
 |-  ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> ( T ^ ( n + 1 ) ) e. RR )
126 121 125 remulcld
 |-  ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> ( ( M x. ( n + 1 ) ) x. ( T ^ ( n + 1 ) ) ) e. RR )
127 nnq
 |-  ( ( M ^ n ) e. NN -> ( M ^ n ) e. QQ )
128 98 127 syl
 |-  ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> ( M ^ n ) e. QQ )
129 qmulcl
 |-  ( ( ( M ^ n ) e. QQ /\ ( |_ ` ( k / ( M ^ n ) ) ) e. QQ ) -> ( ( M ^ n ) x. ( |_ ` ( k / ( M ^ n ) ) ) ) e. QQ )
130 128 112 129 syl2anc
 |-  ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> ( ( M ^ n ) x. ( |_ ` ( k / ( M ^ n ) ) ) ) e. QQ )
131 qex
 |-  QQ e. _V
132 cnfldadd
 |-  + = ( +g ` CCfld )
133 1 132 ressplusg
 |-  ( QQ e. _V -> + = ( +g ` Q ) )
134 131 133 ax-mp
 |-  + = ( +g ` Q )
135 2 67 134 abvtri
 |-  ( ( F e. A /\ ( k mod ( M ^ n ) ) e. QQ /\ ( ( M ^ n ) x. ( |_ ` ( k / ( M ^ n ) ) ) ) e. QQ ) -> ( F ` ( ( k mod ( M ^ n ) ) + ( ( M ^ n ) x. ( |_ ` ( k / ( M ^ n ) ) ) ) ) ) <_ ( ( F ` ( k mod ( M ^ n ) ) ) + ( F ` ( ( M ^ n ) x. ( |_ ` ( k / ( M ^ n ) ) ) ) ) ) )
136 89 102 130 135 syl3anc
 |-  ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> ( F ` ( ( k mod ( M ^ n ) ) + ( ( M ^ n ) x. ( |_ ` ( k / ( M ^ n ) ) ) ) ) ) <_ ( ( F ` ( k mod ( M ^ n ) ) ) + ( F ` ( ( M ^ n ) x. ( |_ ` ( k / ( M ^ n ) ) ) ) ) ) )
137 98 nnrpd
 |-  ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> ( M ^ n ) e. RR+ )
138 modval
 |-  ( ( k e. RR /\ ( M ^ n ) e. RR+ ) -> ( k mod ( M ^ n ) ) = ( k - ( ( M ^ n ) x. ( |_ ` ( k / ( M ^ n ) ) ) ) ) )
139 108 137 138 syl2anc
 |-  ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> ( k mod ( M ^ n ) ) = ( k - ( ( M ^ n ) x. ( |_ ` ( k / ( M ^ n ) ) ) ) ) )
140 139 oveq1d
 |-  ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> ( ( k mod ( M ^ n ) ) + ( ( M ^ n ) x. ( |_ ` ( k / ( M ^ n ) ) ) ) ) = ( ( k - ( ( M ^ n ) x. ( |_ ` ( k / ( M ^ n ) ) ) ) ) + ( ( M ^ n ) x. ( |_ ` ( k / ( M ^ n ) ) ) ) ) )
141 108 recnd
 |-  ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> k e. CC )
142 qcn
 |-  ( ( ( M ^ n ) x. ( |_ ` ( k / ( M ^ n ) ) ) ) e. QQ -> ( ( M ^ n ) x. ( |_ ` ( k / ( M ^ n ) ) ) ) e. CC )
143 130 142 syl
 |-  ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> ( ( M ^ n ) x. ( |_ ` ( k / ( M ^ n ) ) ) ) e. CC )
144 141 143 npcand
 |-  ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> ( ( k - ( ( M ^ n ) x. ( |_ ` ( k / ( M ^ n ) ) ) ) ) + ( ( M ^ n ) x. ( |_ ` ( k / ( M ^ n ) ) ) ) ) = k )
145 140 144 eqtrd
 |-  ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> ( ( k mod ( M ^ n ) ) + ( ( M ^ n ) x. ( |_ ` ( k / ( M ^ n ) ) ) ) ) = k )
146 145 fveq2d
 |-  ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> ( F ` ( ( k mod ( M ^ n ) ) + ( ( M ^ n ) x. ( |_ ` ( k / ( M ^ n ) ) ) ) ) ) = ( F ` k ) )
147 cnfldmul
 |-  x. = ( .r ` CCfld )
148 1 147 ressmulr
 |-  ( QQ e. _V -> x. = ( .r ` Q ) )
149 131 148 ax-mp
 |-  x. = ( .r ` Q )
150 2 67 149 abvmul
 |-  ( ( F e. A /\ ( M ^ n ) e. QQ /\ ( |_ ` ( k / ( M ^ n ) ) ) e. QQ ) -> ( F ` ( ( M ^ n ) x. ( |_ ` ( k / ( M ^ n ) ) ) ) ) = ( ( F ` ( M ^ n ) ) x. ( F ` ( |_ ` ( k / ( M ^ n ) ) ) ) ) )
151 89 128 112 150 syl3anc
 |-  ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> ( F ` ( ( M ^ n ) x. ( |_ ` ( k / ( M ^ n ) ) ) ) ) = ( ( F ` ( M ^ n ) ) x. ( F ` ( |_ ` ( k / ( M ^ n ) ) ) ) ) )
152 1 2 qabvexp
 |-  ( ( F e. A /\ M e. QQ /\ n e. NN0 ) -> ( F ` ( M ^ n ) ) = ( ( F ` M ) ^ n ) )
153 89 105 97 152 syl3anc
 |-  ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> ( F ` ( M ^ n ) ) = ( ( F ` M ) ^ n ) )
154 153 oveq1d
 |-  ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> ( ( F ` ( M ^ n ) ) x. ( F ` ( |_ ` ( k / ( M ^ n ) ) ) ) ) = ( ( ( F ` M ) ^ n ) x. ( F ` ( |_ ` ( k / ( M ^ n ) ) ) ) ) )
155 151 154 eqtrd
 |-  ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> ( F ` ( ( M ^ n ) x. ( |_ ` ( k / ( M ^ n ) ) ) ) ) = ( ( ( F ` M ) ^ n ) x. ( F ` ( |_ ` ( k / ( M ^ n ) ) ) ) ) )
156 155 oveq2d
 |-  ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> ( ( F ` ( k mod ( M ^ n ) ) ) + ( F ` ( ( M ^ n ) x. ( |_ ` ( k / ( M ^ n ) ) ) ) ) ) = ( ( F ` ( k mod ( M ^ n ) ) ) + ( ( ( F ` M ) ^ n ) x. ( F ` ( |_ ` ( k / ( M ^ n ) ) ) ) ) ) )
157 136 146 156 3brtr3d
 |-  ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> ( F ` k ) <_ ( ( F ` ( k mod ( M ^ n ) ) ) + ( ( ( F ` M ) ^ n ) x. ( F ` ( |_ ` ( k / ( M ^ n ) ) ) ) ) ) )
158 122 97 reexpcld
 |-  ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> ( T ^ n ) e. RR )
159 121 158 remulcld
 |-  ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> ( ( M x. ( n + 1 ) ) x. ( T ^ n ) ) e. RR )
160 nn0re
 |-  ( n e. NN0 -> n e. RR )
161 160 ad2antlr
 |-  ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> n e. RR )
162 117 161 remulcld
 |-  ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> ( M x. n ) e. RR )
163 162 158 remulcld
 |-  ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> ( ( M x. n ) x. ( T ^ n ) ) e. RR )
164 117 158 remulcld
 |-  ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> ( M x. ( T ^ n ) ) e. RR )
165 fveq2
 |-  ( j = ( k mod ( M ^ n ) ) -> ( F ` j ) = ( F ` ( k mod ( M ^ n ) ) ) )
166 165 breq1d
 |-  ( j = ( k mod ( M ^ n ) ) -> ( ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) <-> ( F ` ( k mod ( M ^ n ) ) ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) )
167 simprr
 |-  ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) )
168 zmodfz
 |-  ( ( k e. ZZ /\ ( M ^ n ) e. NN ) -> ( k mod ( M ^ n ) ) e. ( 0 ... ( ( M ^ n ) - 1 ) ) )
169 91 98 168 syl2anc
 |-  ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> ( k mod ( M ^ n ) ) e. ( 0 ... ( ( M ^ n ) - 1 ) ) )
170 166 167 169 rspcdva
 |-  ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> ( F ` ( k mod ( M ^ n ) ) ) <_ ( ( M x. n ) x. ( T ^ n ) ) )
171 117 107 remulcld
 |-  ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> ( M x. ( ( F ` M ) ^ n ) ) e. RR )
172 107 recnd
 |-  ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> ( ( F ` M ) ^ n ) e. CC )
173 114 recnd
 |-  ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> ( F ` ( |_ ` ( k / ( M ^ n ) ) ) ) e. CC )
174 172 173 mulcomd
 |-  ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> ( ( ( F ` M ) ^ n ) x. ( F ` ( |_ ` ( k / ( M ^ n ) ) ) ) ) = ( ( F ` ( |_ ` ( k / ( M ^ n ) ) ) ) x. ( ( F ` M ) ^ n ) ) )
175 2 67 abvge0
 |-  ( ( F e. A /\ M e. QQ ) -> 0 <_ ( F ` M ) )
176 89 105 175 syl2anc
 |-  ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> 0 <_ ( F ` M ) )
177 106 97 176 expge0d
 |-  ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> 0 <_ ( ( F ` M ) ^ n ) )
178 110 zred
 |-  ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> ( |_ ` ( k / ( M ^ n ) ) ) e. RR )
179 elfzle1
 |-  ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) -> 0 <_ k )
180 179 ad2antrl
 |-  ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> 0 <_ k )
181 98 nnred
 |-  ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> ( M ^ n ) e. RR )
182 98 nngt0d
 |-  ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> 0 < ( M ^ n ) )
183 divge0
 |-  ( ( ( k e. RR /\ 0 <_ k ) /\ ( ( M ^ n ) e. RR /\ 0 < ( M ^ n ) ) ) -> 0 <_ ( k / ( M ^ n ) ) )
184 108 180 181 182 183 syl22anc
 |-  ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> 0 <_ ( k / ( M ^ n ) ) )
185 flge0nn0
 |-  ( ( ( k / ( M ^ n ) ) e. RR /\ 0 <_ ( k / ( M ^ n ) ) ) -> ( |_ ` ( k / ( M ^ n ) ) ) e. NN0 )
186 109 184 185 syl2anc
 |-  ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> ( |_ ` ( k / ( M ^ n ) ) ) e. NN0 )
187 1 2 qabvle
 |-  ( ( F e. A /\ ( |_ ` ( k / ( M ^ n ) ) ) e. NN0 ) -> ( F ` ( |_ ` ( k / ( M ^ n ) ) ) ) <_ ( |_ ` ( k / ( M ^ n ) ) ) )
188 89 186 187 syl2anc
 |-  ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> ( F ` ( |_ ` ( k / ( M ^ n ) ) ) ) <_ ( |_ ` ( k / ( M ^ n ) ) ) )
189 simprl
 |-  ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) )
190 0z
 |-  0 e. ZZ
191 96 124 nnexpcld
 |-  ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> ( M ^ ( n + 1 ) ) e. NN )
192 191 nnzd
 |-  ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> ( M ^ ( n + 1 ) ) e. ZZ )
193 elfzm11
 |-  ( ( 0 e. ZZ /\ ( M ^ ( n + 1 ) ) e. ZZ ) -> ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) <-> ( k e. ZZ /\ 0 <_ k /\ k < ( M ^ ( n + 1 ) ) ) ) )
194 190 192 193 sylancr
 |-  ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) <-> ( k e. ZZ /\ 0 <_ k /\ k < ( M ^ ( n + 1 ) ) ) ) )
195 189 194 mpbid
 |-  ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> ( k e. ZZ /\ 0 <_ k /\ k < ( M ^ ( n + 1 ) ) ) )
196 195 simp3d
 |-  ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> k < ( M ^ ( n + 1 ) ) )
197 96 nncnd
 |-  ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> M e. CC )
198 197 97 expp1d
 |-  ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> ( M ^ ( n + 1 ) ) = ( ( M ^ n ) x. M ) )
199 196 198 breqtrd
 |-  ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> k < ( ( M ^ n ) x. M ) )
200 ltdivmul
 |-  ( ( k e. RR /\ M e. RR /\ ( ( M ^ n ) e. RR /\ 0 < ( M ^ n ) ) ) -> ( ( k / ( M ^ n ) ) < M <-> k < ( ( M ^ n ) x. M ) ) )
201 108 117 181 182 200 syl112anc
 |-  ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> ( ( k / ( M ^ n ) ) < M <-> k < ( ( M ^ n ) x. M ) ) )
202 199 201 mpbird
 |-  ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> ( k / ( M ^ n ) ) < M )
203 96 nnzd
 |-  ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> M e. ZZ )
204 fllt
 |-  ( ( ( k / ( M ^ n ) ) e. RR /\ M e. ZZ ) -> ( ( k / ( M ^ n ) ) < M <-> ( |_ ` ( k / ( M ^ n ) ) ) < M ) )
205 109 203 204 syl2anc
 |-  ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> ( ( k / ( M ^ n ) ) < M <-> ( |_ ` ( k / ( M ^ n ) ) ) < M ) )
206 202 205 mpbid
 |-  ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> ( |_ ` ( k / ( M ^ n ) ) ) < M )
207 178 117 206 ltled
 |-  ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> ( |_ ` ( k / ( M ^ n ) ) ) <_ M )
208 114 178 117 188 207 letrd
 |-  ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> ( F ` ( |_ ` ( k / ( M ^ n ) ) ) ) <_ M )
209 114 117 107 177 208 lemul1ad
 |-  ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> ( ( F ` ( |_ ` ( k / ( M ^ n ) ) ) ) x. ( ( F ` M ) ^ n ) ) <_ ( M x. ( ( F ` M ) ^ n ) ) )
210 174 209 eqbrtrd
 |-  ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> ( ( ( F ` M ) ^ n ) x. ( F ` ( |_ ` ( k / ( M ^ n ) ) ) ) ) <_ ( M x. ( ( F ` M ) ^ n ) ) )
211 96 nnnn0d
 |-  ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> M e. NN0 )
212 211 nn0ge0d
 |-  ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> 0 <_ M )
213 max1
 |-  ( ( ( F ` M ) e. RR /\ 1 e. RR ) -> ( F ` M ) <_ if ( ( F ` M ) <_ 1 , 1 , ( F ` M ) ) )
214 106 64 213 sylancl
 |-  ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> ( F ` M ) <_ if ( ( F ` M ) <_ 1 , 1 , ( F ` M ) ) )
215 214 11 breqtrrdi
 |-  ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> ( F ` M ) <_ T )
216 leexp1a
 |-  ( ( ( ( F ` M ) e. RR /\ T e. RR /\ n e. NN0 ) /\ ( 0 <_ ( F ` M ) /\ ( F ` M ) <_ T ) ) -> ( ( F ` M ) ^ n ) <_ ( T ^ n ) )
217 106 122 97 176 215 216 syl32anc
 |-  ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> ( ( F ` M ) ^ n ) <_ ( T ^ n ) )
218 107 158 117 212 217 lemul2ad
 |-  ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> ( M x. ( ( F ` M ) ^ n ) ) <_ ( M x. ( T ^ n ) ) )
219 115 171 164 210 218 letrd
 |-  ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> ( ( ( F ` M ) ^ n ) x. ( F ` ( |_ ` ( k / ( M ^ n ) ) ) ) ) <_ ( M x. ( T ^ n ) ) )
220 104 115 163 164 170 219 le2addd
 |-  ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> ( ( F ` ( k mod ( M ^ n ) ) ) + ( ( ( F ` M ) ^ n ) x. ( F ` ( |_ ` ( k / ( M ^ n ) ) ) ) ) ) <_ ( ( ( M x. n ) x. ( T ^ n ) ) + ( M x. ( T ^ n ) ) ) )
221 nn0cn
 |-  ( n e. NN0 -> n e. CC )
222 221 ad2antlr
 |-  ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> n e. CC )
223 1cnd
 |-  ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> 1 e. CC )
224 197 222 223 adddid
 |-  ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> ( M x. ( n + 1 ) ) = ( ( M x. n ) + ( M x. 1 ) ) )
225 197 mulid1d
 |-  ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> ( M x. 1 ) = M )
226 225 oveq2d
 |-  ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> ( ( M x. n ) + ( M x. 1 ) ) = ( ( M x. n ) + M ) )
227 224 226 eqtrd
 |-  ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> ( M x. ( n + 1 ) ) = ( ( M x. n ) + M ) )
228 227 oveq1d
 |-  ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> ( ( M x. ( n + 1 ) ) x. ( T ^ n ) ) = ( ( ( M x. n ) + M ) x. ( T ^ n ) ) )
229 197 222 mulcld
 |-  ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> ( M x. n ) e. CC )
230 158 recnd
 |-  ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> ( T ^ n ) e. CC )
231 229 197 230 adddird
 |-  ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> ( ( ( M x. n ) + M ) x. ( T ^ n ) ) = ( ( ( M x. n ) x. ( T ^ n ) ) + ( M x. ( T ^ n ) ) ) )
232 228 231 eqtrd
 |-  ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> ( ( M x. ( n + 1 ) ) x. ( T ^ n ) ) = ( ( ( M x. n ) x. ( T ^ n ) ) + ( M x. ( T ^ n ) ) ) )
233 220 232 breqtrrd
 |-  ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> ( ( F ` ( k mod ( M ^ n ) ) ) + ( ( ( F ` M ) ^ n ) x. ( F ` ( |_ ` ( k / ( M ^ n ) ) ) ) ) ) <_ ( ( M x. ( n + 1 ) ) x. ( T ^ n ) ) )
234 max2
 |-  ( ( ( F ` M ) e. RR /\ 1 e. RR ) -> 1 <_ if ( ( F ` M ) <_ 1 , 1 , ( F ` M ) ) )
235 106 64 234 sylancl
 |-  ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> 1 <_ if ( ( F ` M ) <_ 1 , 1 , ( F ` M ) ) )
236 235 11 breqtrrdi
 |-  ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> 1 <_ T )
237 nn0z
 |-  ( n e. NN0 -> n e. ZZ )
238 237 ad2antlr
 |-  ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> n e. ZZ )
239 uzid
 |-  ( n e. ZZ -> n e. ( ZZ>= ` n ) )
240 238 239 syl
 |-  ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> n e. ( ZZ>= ` n ) )
241 peano2uz
 |-  ( n e. ( ZZ>= ` n ) -> ( n + 1 ) e. ( ZZ>= ` n ) )
242 240 241 syl
 |-  ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> ( n + 1 ) e. ( ZZ>= ` n ) )
243 122 236 242 leexp2ad
 |-  ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> ( T ^ n ) <_ ( T ^ ( n + 1 ) ) )
244 96 119 nnmulcld
 |-  ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> ( M x. ( n + 1 ) ) e. NN )
245 244 nngt0d
 |-  ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> 0 < ( M x. ( n + 1 ) ) )
246 lemul2
 |-  ( ( ( T ^ n ) e. RR /\ ( T ^ ( n + 1 ) ) e. RR /\ ( ( M x. ( n + 1 ) ) e. RR /\ 0 < ( M x. ( n + 1 ) ) ) ) -> ( ( T ^ n ) <_ ( T ^ ( n + 1 ) ) <-> ( ( M x. ( n + 1 ) ) x. ( T ^ n ) ) <_ ( ( M x. ( n + 1 ) ) x. ( T ^ ( n + 1 ) ) ) ) )
247 158 125 121 245 246 syl112anc
 |-  ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> ( ( T ^ n ) <_ ( T ^ ( n + 1 ) ) <-> ( ( M x. ( n + 1 ) ) x. ( T ^ n ) ) <_ ( ( M x. ( n + 1 ) ) x. ( T ^ ( n + 1 ) ) ) ) )
248 243 247 mpbid
 |-  ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> ( ( M x. ( n + 1 ) ) x. ( T ^ n ) ) <_ ( ( M x. ( n + 1 ) ) x. ( T ^ ( n + 1 ) ) ) )
249 116 159 126 233 248 letrd
 |-  ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> ( ( F ` ( k mod ( M ^ n ) ) ) + ( ( ( F ` M ) ^ n ) x. ( F ` ( |_ ` ( k / ( M ^ n ) ) ) ) ) ) <_ ( ( M x. ( n + 1 ) ) x. ( T ^ ( n + 1 ) ) ) )
250 95 116 126 157 249 letrd
 |-  ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> ( F ` k ) <_ ( ( M x. ( n + 1 ) ) x. ( T ^ ( n + 1 ) ) ) )
251 250 expr
 |-  ( ( ( ph /\ n e. NN0 ) /\ k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) ) -> ( A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) -> ( F ` k ) <_ ( ( M x. ( n + 1 ) ) x. ( T ^ ( n + 1 ) ) ) ) )
252 251 ralrimdva
 |-  ( ( ph /\ n e. NN0 ) -> ( A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) -> A. k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) ( F ` k ) <_ ( ( M x. ( n + 1 ) ) x. ( T ^ ( n + 1 ) ) ) ) )
253 88 252 syl5bi
 |-  ( ( ph /\ n e. NN0 ) -> ( A. k e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` k ) <_ ( ( M x. n ) x. ( T ^ n ) ) -> A. k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) ( F ` k ) <_ ( ( M x. ( n + 1 ) ) x. ( T ^ ( n + 1 ) ) ) ) )
254 253 expcom
 |-  ( n e. NN0 -> ( ph -> ( A. k e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` k ) <_ ( ( M x. n ) x. ( T ^ n ) ) -> A. k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) ( F ` k ) <_ ( ( M x. ( n + 1 ) ) x. ( T ^ ( n + 1 ) ) ) ) ) )
255 254 a2d
 |-  ( n e. NN0 -> ( ( ph -> A. k e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` k ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) -> ( ph -> A. k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) ( F ` k ) <_ ( ( M x. ( n + 1 ) ) x. ( T ^ ( n + 1 ) ) ) ) ) )
256 20 29 38 47 85 255 nn0ind
 |-  ( X e. NN0 -> ( ph -> A. k e. ( 0 ... ( ( M ^ X ) - 1 ) ) ( F ` k ) <_ ( ( M x. X ) x. ( T ^ X ) ) ) )
257 256 impcom
 |-  ( ( ph /\ X e. NN0 ) -> A. k e. ( 0 ... ( ( M ^ X ) - 1 ) ) ( F ` k ) <_ ( ( M x. X ) x. ( T ^ X ) ) )
258 fveq2
 |-  ( k = Y -> ( F ` k ) = ( F ` Y ) )
259 258 breq1d
 |-  ( k = Y -> ( ( F ` k ) <_ ( ( M x. X ) x. ( T ^ X ) ) <-> ( F ` Y ) <_ ( ( M x. X ) x. ( T ^ X ) ) ) )
260 259 rspccv
 |-  ( A. k e. ( 0 ... ( ( M ^ X ) - 1 ) ) ( F ` k ) <_ ( ( M x. X ) x. ( T ^ X ) ) -> ( Y e. ( 0 ... ( ( M ^ X ) - 1 ) ) -> ( F ` Y ) <_ ( ( M x. X ) x. ( T ^ X ) ) ) )
261 257 260 syl
 |-  ( ( ph /\ X e. NN0 ) -> ( Y e. ( 0 ... ( ( M ^ X ) - 1 ) ) -> ( F ` Y ) <_ ( ( M x. X ) x. ( T ^ X ) ) ) )
262 261 3impia
 |-  ( ( ph /\ X e. NN0 /\ Y e. ( 0 ... ( ( M ^ X ) - 1 ) ) ) -> ( F ` Y ) <_ ( ( M x. X ) x. ( T ^ X ) ) )