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 mulridd 
 |-  ( ( ( 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 biimtrid 
 |-  ( ( 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 ) ) )